:: Equivalent Expressions of Direct Sum Decomposition of Groups
:: by Kazuhisa Nakasho , Hiroyuki Okazaki , Hiroshi Yamazaki and Yasunari Shidama
::
:: Received February 26, 2015
:: Copyright (c) 2015-2017 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, XXREAL_0, GROUP_2, CARD_1, NUMBERS, FUNCT_4, GROUP_6, FUNCOP_1,
GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1,
ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3, FINSET_1, NEWTON, GROUP_4,
PRE_POLY, UPROOTS, GROUP_19, SEMI_AF1, QC_LANG1, VECTMETR, GROUP_20;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, DOMAIN_1, FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1,
CARD_1, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, FINSEQ_1, FUNCT_7, STRUCT_0,
ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, PRALG_1, GRSOLV_1,
GROUP_7, GROUP_12, GROUP_19;
constructors REALSET1, FUNCT_4, MONOID_0, PRALG_1, GROUP_4, FUNCT_7, RELSET_1,
INT_7, FUNCT_3, GROUP_17, GRSOLV_1, GROUP_19;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1,
FUNCT_2, FUNCOP_1, CARD_1, GROUP_7, GROUP_3, RELSET_1, SUBSET_1, INT_1,
FINSET_1, RELAT_1, FUNCT_1, NUMBERS, GROUP_12, GROUP_6, GROUP_19;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: 1. Internal Direct Sum Decomposition into Normal Subgroups
definition
let I be set, G be Group;
mode Subgroup-Family of I,G -> Group-Family of I means
:: GROUP_20:def 1
for i being object st i in I holds it.i is Subgroup of G;
end;
definition
let I be set, G be Group, F be Subgroup-Family of I,G;
attr F is component-commutative means
:: GROUP_20:def 2
for i,j be object, gi,gj be Element of G
st i in I & j in I & i <> j
ex Fi,Fj being Subgroup of G st Fi = F.i & Fj = F.j &
(gi in Fi & gj in Fj implies gi * gj = gj * gi);
end;
definition
let I be non empty set, G be Group, F be Subgroup-Family of I,G;
redefine attr F is component-commutative means
:: GROUP_20:def 3
for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi;
end;
registration
let I be non empty set, G be Group;
cluster component-commutative for Subgroup-Family of I,G;
end;
theorem :: GROUP_20:1
for G be Group, H be normal Subgroup of G, x,y be Element of G st y in H
holds x * y * x" in H & x * (y * x") in H;
theorem :: GROUP_20:2
for I be non empty set,
G be Group,
F be Group-Family of I,
x be Function of I,G
st x in product F
holds x is Function of I,Union(Carrier F);
theorem :: GROUP_20:3
for I be non empty set,
G be Group,
H be Subgroup of G,
x be Function of I,G,
y be Function of I,H
st x = y
holds support x = support y;
theorem :: GROUP_20:4
for I be non empty set,
G be Group,
H be Subgroup of G,
y be finite-support Function of I,H
holds y is finite-support Function of I,G;
theorem :: GROUP_20:5
for I be non empty set,
G be Group,
H be Subgroup of G,
x be finite-support Function of I,G
st rng x c= [#]H
holds x is finite-support Function of I,H;
theorem :: GROUP_20:6
for I be non empty set,
G be Group,
H be Subgroup of G,
x be finite-support Function of I,G,
y be finite-support Function of I,H
st x = y
holds Product x = Product y;
theorem :: GROUP_20:7
for f be Function, i,x be set
holds f = f +* (i,x) +* (i,f.i);
theorem :: GROUP_20:8
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
x,y be finite-support Function of I,G,
i be Element of I
st y = x +* (i,1_F.i) & x in product F
holds Product x = Product(y) * x.i = x.i * Product(y);
theorem :: GROUP_20:9
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G
holds
for i be Element of I, x,y be finite-support Function of I,gr UF
st y = x +* (i,1_F.i) & x in product F
holds Product x = Product(y) * x.i = x.i * Product(y);
theorem :: GROUP_20:10
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G
holds
for y be finite-support Function of I,gr UF,
i be Element of I, g be Element of gr UF
st y in product F & y.i = 1_F.i & g in F.i
holds Product(y) * g = g * Product(y);
theorem :: GROUP_20:11
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G
st UF = Union Carrier F
holds
for g be Element of G,
H be FinSequence of G,
K be FinSequence of INT
st len H = len K & rng H c= UF & Product(H|^K) = g
holds
ex f be finite-support Function of I,G
st f in product F & g = Product f;
theorem :: GROUP_20:12
for I be non empty set,
G be Group,
F be Subgroup-Family of I,G,
h,h0 be finite-support Function of I,G,
i be Element of I,
UFi be Subset of G
st UFi = Union((Carrier F) | (I \ {i}))
& h0 = h +* (i, 1_F.i)
& h in product F
holds Product h0 in gr UFi;
theorem :: GROUP_20:13
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G
st UF = Union Carrier F
holds
for g be Element of G st g in gr UF holds
ex f be finite-support Function of I,gr UF
st f in sum F & g = Product f;
theorem :: GROUP_20:14
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G
st UF = Union Carrier F
holds
for i be Element of I holds F.i is normal Subgroup of gr UF;
theorem :: GROUP_20:15
for I be non empty set,
G be Group,
F be component-commutative Subgroup-Family of I,G
st for i be Element of I holds
ex UFi be Subset of G
st UFi = Union((Carrier F) | (I \ {i}))
& [#]gr(UFi) /\ [#](F.i) = {1_G}
holds
for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product x1 = Product x2
holds x1 = x2;
theorem :: GROUP_20:16
for I be non empty set,
G be strict Group,
F be Group-Family of I
holds
F is internal DirectSumComponents of G,I
iff
(for i be Element of I holds F.i is normal Subgroup of G)
& (ex UF be Subset of G st UF = Union Carrier F & gr(UF) = G)
& for i be Element of I holds
ex UFi be Subset of G
st UFi = Union((Carrier F) | (I \ {i}))
& [#](gr(UFi)) /\ [#](F.i) = {1_G};
begin :: 2. Internal Direct Sum Decomposition for Commutative Group
theorem :: GROUP_20:17
for I be non empty set,
G be commutative Group,
F be Group-Family of I
holds
F is internal DirectSumComponents of G,I
iff
(for i be Element of I holds F.i is Subgroup of G)
&(for i,j be Element of I st i <> j holds
[#] (F.i) /\ [#] (F.j) = {1_G})
&(for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product(x))
&(for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product(x1) = Product(x2)
holds x1 = x2);
begin :: 3. Equivalence between Internal and External Direct Sum
theorem :: GROUP_20:18
for I be non empty set,
G be Group,
F be Subgroup-Family of I,G,
h be Homomorphism of sum F,G,
a be finite-support Function of I,G
st a in sum F
& for i be Element of I, x be Element of F.i
holds h.(1ProdHom(F,i).x) = x
holds h.a = Product a;
theorem :: GROUP_20:19
for I be non empty set,
G be Group,
M be DirectSumComponents of G,I
holds
ex f be Homomorphism of sum M,G,
N be internal DirectSumComponents of G,I
st f is bijective
& for i be Element of I holds
ex qi be Homomorphism of M.i,N.i
st qi = f * 1ProdHom(M,i)
& qi is bijective;