:: Conservation Rules of Direct Sum Decomposition of Groups :: by Kazuhisa Nakasho , Hiroshi Yamazaki , Hiroyuki Okazaki and Yasunari Shidama :: :: Received December 31, 2015 :: Copyright (c) 2015-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1, GROUP_1, GROUP_2, CARD_1, FUNCT_4, GROUP_6, GROUP_7, FUNCT_7, FUNCOP_1, ALGSTR_0, GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1, FINSET_1, ZFMISC_1, PBOOLE, REALSET1, GROUP_4, PRE_POLY, UPROOTS, GROUP_19, GROUP_20, MSSUBFAM, SEMI_AF1, VECTMETR, PROB_2, MONOID_0, GROUP_21; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, CARD_3, FINSEQ_1, FUNCT_7, PROB_2, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_4, GROUP_6, MONOID_0, PRALG_1, GRSOLV_1, GROUP_7, GROUP_12, GROUP_17, GROUP_19, GROUP_20; constructors REALSET1, FUNCT_4, MONOID_0, PRALG_1, GROUP_4, FUNCT_7, RELSET_1, WELLORD2, FUNCT_3, GROUP_17, GRSOLV_1, PROB_2, GROUP_19, GROUP_20; registrations XBOOLE_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1, FUNCT_2, CARD_1, GROUP_7, MSAFREE, PARTFUN1, RELSET_1, REALSET1, FINSEQ_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1, PBOOLE, GROUP_6, GROUP_19; requirements NUMERALS, BOOLE, SUBSET; begin :: 1. Preliminaries definition let I,J be non empty set, a be Function of I,J, F be multMagma-Family of J; redefine func F * a -> multMagma-Family of I; end; definition let I,J be non empty set, a be Function of I,J, F be Group-Family of J; redefine func F * a -> Group-Family of I; end; definition let I,J be non empty set, a be Function of I,J, G be Group, F be Subgroup-Family of J,G; func F * a -> Subgroup-Family of I,G equals :: GROUP_21:def 1 F * a; end; scheme :: GROUP_21:sch 1 Sch1{A()->set, B()->1-sorted, F(Element of B())->set}: ex f being Function st dom f = A() & for x being Element of B() st x in A() holds f.x = F(x); registration let I be set; cluster non-empty disjoint_valued for ManySortedSet of I; end; theorem :: GROUP_21:1 for f being non-empty disjoint_valued Function st Union f is finite holds dom f is finite; theorem :: GROUP_21:2 for X,Y be non empty set, X0,Y0 be set, f be Function of X,Y st f is bijective & rng(f|X0) = Y0 holds (f|X0)" = f" | Y0; begin :: 2. Conservation rule of direct sum decomposition :: for substitution of subscript set theorem :: GROUP_21:3 for I,J be non empty set, a be Function of I,J, F be multMagma-Family of J, x be Element of product F holds x*a in product(F*a); definition let I,J be non empty set; let a be Function of I,J; let F be multMagma-Family of J; func trans_prod(F,a) -> Function of product F, product(F*a) means :: GROUP_21:def 2 for x be Element of product F holds it.x = x*a; end; theorem :: GROUP_21:4 for I,J be non empty set, a be Function of I,J, F be multMagma-Family of J holds trans_prod(F,a) is multiplicative; definition let I,J be non empty set; let a be Function of I,J; let F be Group-Family of J; redefine func trans_prod(F,a) -> Homomorphism of product F, product(F*a); end; theorem :: GROUP_21:5 for I,J be non empty set, a be Function of I,J, F be multMagma-Family of J, y be Element of product(F*a) st a is bijective holds y * a" in product F; theorem :: GROUP_21:6 for I,J be non empty set, a be Function of I,J, x,y be Function st dom x = I & dom y = J & a is bijective holds x = y * a iff y = x * a"; theorem :: GROUP_21:7 for I,J be non empty set, F be multMagma-Family of J, a be Function of I,J st a is bijective holds dom trans_prod(F,a) = [#] product(F) & rng trans_prod(F,a) = [#] product(F*a); theorem :: GROUP_21:8 for I,J be non empty set, a be Function of I,J, F be multMagma-Family of J st a is bijective holds trans_prod(F,a) is bijective; theorem :: GROUP_21:9 for I,J be non empty set, a be Function of I,J, F be Group-Family of J, x be Function holds a .: support(x*a, F*a) c= support(x,F); theorem :: GROUP_21:10 for I,J be non empty set, a be Function of I,J, F be Group-Family of J, x be Function st a is onto holds support(x,F) c= a .: support(x*a,F*a); theorem :: GROUP_21:11 for I,J be non empty set, a be Function of I,J, F be Group-Family of J, x be Function st a is one-to-one holds x in sum F implies x*a in sum(F*a); theorem :: GROUP_21:12 for I,J be non empty set, a be Function of I,J, F be Group-Family of J, x be Function st a is bijective holds x in sum F iff x*a in sum(F*a) & dom x = J; definition let I,J be non empty set; let a be Function of I,J; let F be Group-Family of J; assume a is bijective; func trans_sum(F,a) -> Function of sum F, sum(F*a) equals :: GROUP_21:def 3 trans_prod(F,a) | (sum F); end; theorem :: GROUP_21:13 for G,H be Group, H0 be Subgroup of H, f be Homomorphism of G,H st rng f c= [#]H0 holds f is Homomorphism of G,H0; theorem :: GROUP_21:14 for I,J be non empty set for a be Function of I,J for F be Group-Family of J st a is bijective holds trans_sum(F,a) is Homomorphism of sum F, sum(F*a); theorem :: GROUP_21:15 for I,J be non empty set, a be Function of I,J, F be Group-Family of J st a is bijective holds trans_sum(F,a) is bijective; :: independent from subscript set theorem :: GROUP_21:16 for G be Group, I,J be non empty set, F be DirectSumComponents of G,J, a be Function of I,J st a is bijective holds F * a is DirectSumComponents of G,I; theorem :: GROUP_21:17 for I be non empty set, G be Group, F be internal DirectSumComponents of G,I holds F is Subgroup-Family of I,G; theorem :: GROUP_21:18 for I,J be non empty set, G be Group, x be Function of I,G, y be Function of J,G, a be Function of I,J st a is onto & x = y * a holds support(y) = a .: support(x); theorem :: GROUP_21:19 for I,J be non empty set, G be commutative Group, x be finite-support Function of I,G, y be finite-support Function of J,G, a be Function of I,J st a is bijective & x = y * a holds Product x = Product y; theorem :: GROUP_21:20 for I,J be non empty set, G be Group, x be finite-support Function of I,G, y be finite-support Function of J,G, a be Function of I,J st a is bijective & x = y * a & for i,j be Element of I holds x.i * x.j = x.j * x.i holds Product x = Product y; theorem :: GROUP_21:21 for G be Group, I,J be non empty set, F be internal DirectSumComponents of G,J, a be Function of I,J st a is bijective holds F * a is internal DirectSumComponents of G,I; begin :: 3. Conservation rule of direct sum decomposition for flattening definition let I be non empty set; let J be ManySortedSet of I; mode multMagma-Family of I,J -> ManySortedSet of I means :: GROUP_21:def 4 for i be Element of I holds it.i is multMagma-Family of J.i; end; definition let I be non empty set; let J be ManySortedSet of I; mode Group-Family of I,J -> multMagma-Family of I,J means :: GROUP_21:def 5 for i be Element of I holds it.i is Group-Family of J.i; end; definition let I be non empty set; let J be ManySortedSet of I; let N be multMagma-Family of I,J; let i be Element of I; redefine func N.i -> multMagma-Family of J.i; end; definition let I be non empty set; let J be ManySortedSet of I; let N be Group-Family of I,J; let i be Element of I; redefine func N.i -> Group-Family of J.i; end; definition let I be non empty set; let J be disjoint_valued ManySortedSet of I; let F be Group-Family of I,J; redefine func Union F -> Group-Family of Union J; end; theorem :: GROUP_21:22 for I be non empty set, J be disjoint_valued ManySortedSet of I, F be Group-Family of I,J, j be Element of I, i be object st i in J.j holds (Union F).i = (F.j).i; definition let I be non empty set; let J be ManySortedSet of I; let F be multMagma-Family of I,J; func prod_bundle F -> multMagma-Family of I means :: GROUP_21:def 6 for i be Element of I holds it.i = product(F.i); end; definition let I be non empty set; let J be ManySortedSet of I; let F be Group-Family of I,J; redefine func prod_bundle F -> Group-Family of I; end; definition let I be non empty set; let J be ManySortedSet of I; let F be Group-Family of I,J; func sum_bundle F -> Group-Family of I means :: GROUP_21:def 7 for i be Element of I holds it.i = sum(F.i); end; definition let I be non empty set; let J be ManySortedSet of I; let F be multMagma-Family of I,J; func dprod F -> multMagma equals :: GROUP_21:def 8 product(prod_bundle F); end; registration let I be non empty set; let J be non-empty ManySortedSet of I; let F be multMagma-Family of I,J; cluster dprod F -> non empty constituted-Functions; end; registration let I be non empty set; let J be non-empty ManySortedSet of I; let F be Group-Family of I,J; cluster dprod F -> Group-like associative; end; definition let I be non empty set; let J be non-empty ManySortedSet of I; let F be Group-Family of I,J; func dsum F -> Group equals :: GROUP_21:def 9 sum(sum_bundle F); end; registration let I be non empty set; let J be non-empty ManySortedSet of I; let F be Group-Family of I,J; cluster dsum F -> non empty constituted-Functions; end; theorem :: GROUP_21:23 for I be non empty set, F1,F2 be Group-Family of I st for i be Element of I holds F1.i is Subgroup of F2.i holds product F1 is Subgroup of product F2; theorem :: GROUP_21:24 for I be non empty set, F1,F2 be Group-Family of I st for i be Element of I holds F1.i is Subgroup of F2.i holds sum F1 is Subgroup of sum F2; theorem :: GROUP_21:25 for I be non empty set, J be non-empty ManySortedSet of I, F be Group-Family of I,J holds dsum F is Subgroup of dprod F; definition let I be non empty set; let J be non-empty disjoint_valued ManySortedSet of I; let F be Group-Family of I,J; redefine func dsum F -> Subgroup of dprod F; end; definition let I be non empty set; let J be non-empty disjoint_valued ManySortedSet of I; let F be Group-Family of I,J; func dprod2prod F -> Homomorphism of dprod F, product(Union F) means :: GROUP_21:def 10 for x be Element of dprod F, i be Element of I holds x.i = it.x | (J.i); end; theorem :: GROUP_21:26 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J, y be Element of product(Union F), i be Element of I holds y | (J.i) in product(F.i); registration let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J; cluster dprod2prod F -> bijective; end; definition let I be non empty set; let J be non-empty disjoint_valued ManySortedSet of I; let F be Group-Family of I,J; func prod2dprod F -> Homomorphism of product(Union F), dprod F equals :: GROUP_21:def 11 (dprod2prod F)"; end; theorem :: GROUP_21:27 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J holds for x be Element of product(Union F), i be Element of I holds x | (J.i) = ((prod2dprod F).x).i; registration let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J; cluster prod2dprod F -> bijective; end; theorem :: GROUP_21:28 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J holds prod2dprod F = (dprod2prod F)"; definition let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J, x be Function; func supp_restr(x,F) -> disjoint_valued ManySortedSet of I means :: GROUP_21:def 12 for i be Element of I holds it.i = support(x | (J.i), F.i); end; theorem :: GROUP_21:29 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J, x be Function holds support(x,Union F) = Union supp_restr(x,F); theorem :: GROUP_21:30 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J, x,y,z be Function st z in dprod F & x = (dprod2prod F).z holds supp_restr(x,F) | support(z,sum_bundle F) is non-empty disjoint_valued ManySortedSet of support(z,sum_bundle F) & support(x,Union F) = Union(supp_restr(x,F) | support(z,sum_bundle F)); theorem :: GROUP_21:31 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J, y be Function st y in sum(Union F) ex x be Function st y = (dprod2prod F).x & x in dsum F; theorem :: GROUP_21:32 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J, x,y be Function st x in dsum F & x in dsum F holds (dprod2prod F).x in sum(Union F); theorem :: GROUP_21:33 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J holds rng((dprod2prod F) | (dsum F)) = [#] sum(Union F); definition let I be non empty set; let J be non-empty disjoint_valued ManySortedSet of I; let F be Group-Family of I,J; func dsum2sum F -> Homomorphism of dsum(F), sum(Union F) equals :: GROUP_21:def 13 (dprod2prod F) | (dsum F); end; registration let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J; cluster dsum2sum(F) -> bijective; end; definition let I be non empty set; let J be non-empty disjoint_valued ManySortedSet of I; let F be Group-Family of I,J; func sum2dsum F -> Homomorphism of sum(Union F), dsum F equals :: GROUP_21:def 14 (dsum2sum F)"; end; theorem :: GROUP_21:34 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J holds sum2dsum F = (prod2dprod F) | sum(Union F); registration let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J; cluster sum2dsum(F) -> bijective; end; theorem :: GROUP_21:35 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I,J holds dsum2sum(F) = (sum2dsum F)"; definition let I be non empty set; let G be Group; let F be internal DirectSumComponents of G,I; func InterHom F -> Homomorphism of sum F, G means :: GROUP_21:def 15 it is bijective & for x be finite-support Function of I,G st x in sum F holds it.x = Product x; end; definition let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be DirectSumComponents of G,I, N be Group-Family of I,J, h be ManySortedSet of I; assume for i be Element of I holds ex hi be Homomorphism of (sum_bundle N).i, M.i st hi = h.i & hi is bijective; func ProductHom(G,M,N,h) -> Homomorphism of dsum N, sum M means :: GROUP_21:def 16 it = SumMap(sum_bundle N,M,h) & it is bijective; end; theorem :: GROUP_21:36 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be DirectSumComponents of G,I, N be Group-Family of I,J st for i be Element of I holds N.i is DirectSumComponents of M.i,J.i holds Union N is DirectSumComponents of G,Union J; theorem :: GROUP_21:37 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be internal DirectSumComponents of G,I, N be Group-Family of I,J st for i be Element of I holds N.i is internal DirectSumComponents of M.i,J.i holds Union N is internal DirectSumComponents of G,Union J; begin :: 4. Conservation rule of direct sum decomposition for layering theorem :: GROUP_21:38 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be Group-Family of I for N be Group-Family of I,J st Union N is DirectSumComponents of G,Union J & for i be Element of I holds N.i is DirectSumComponents of M.i,J.i holds M is DirectSumComponents of G,I; theorem :: GROUP_21:39 for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be Subgroup-Family of I,G for N be Group-Family of I,J st Union N is internal DirectSumComponents of G,Union J & for i be Element of I holds N.i is internal DirectSumComponents of M.i,J.i holds M is internal DirectSumComponents of G,I; :: :: trivial groups addition preservance :: :: Corollary of Th39 :: theorem :: GROUP_21:40 for I2 be non empty set, F2 be Group-Family of I2 st for i be Element of I2 holds card (F2.i) = 1 holds card (the carrier of sum F2) = 1; theorem :: GROUP_21:41 for I be non empty set, G be Group, x be finite-support Function of I,G st for i be object st i in I holds x.i = 1_G holds Product x = 1_G; theorem :: GROUP_21:42 for I be non empty set, G be Group, x be finite-support Function of I,G, a be Element of G st I = {1,2} & x = <*a,1_G*> holds Product x = a; theorem :: GROUP_21:43 for G be Group, I1,I2 be non empty set, F1 be DirectSumComponents of G,I1, F2 be Group-Family of I2 st I1 misses I2 & for i be Element of I2 holds card(F2.i) = 1 holds F1 +* F2 is DirectSumComponents of G,I1 \/ I2; theorem :: GROUP_21:44 for G be Group, I1, I2 be non empty set, F1 be internal DirectSumComponents of G,I1, F2 be Subgroup-Family of I2,G st I1 misses I2 & F2 = I2 --> (1).G holds F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2;