:: Normal Subgroup of Product of Groups
:: by Hiroyuki Okazaki , Kenichi Arai and Yasunari Shidama
::
:: Received July 2, 2010
:: Copyright (c) 2010-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, XXREAL_0, GROUP_2, CARD_1, NUMBERS, FUNCT_4, GROUP_6, GROUP_7,
FUNCOP_1, ALGSTR_0, GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0,
STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, CARD_3, ORDINAL1, NUMBERS,
FINSEQ_1, XXREAL_0, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3,
GROUP_4, GROUP_6, PRALG_1, GROUP_7, FUNCT_7;
constructors BINOP_1, REALSET1, FUNCT_4, GROUP_6, MONOID_0, PRALG_1, GROUP_4,
GROUP_7, FUNCT_7, RELSET_1;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1,
FUNCT_2, FUNCOP_1, CARD_1, CARD_3, GROUP_7, XXREAL_0, RELSET_1, FINSEQ_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
registration
let I be non empty set, F be Group-like multMagma-Family of I;
let i be Element of I;
cluster F.i -> Group-like for multMagma;
end;
registration
let I be non empty set, F be associative multMagma-Family of I;
let i be Element of I;
cluster F.i -> associative for multMagma;
end;
registration
let I be non empty set, F be commutative multMagma-Family of I;
let i be Element of I;
cluster F.i -> commutative for multMagma;
end;
reserve
I for non empty set,
F for associative Group-like multMagma-Family of I,
i, j for Element of I;
theorem :: GROUP_12:1
for x be Function, g be Element of F.i holds
( dom x = I & x.i = g & for j be Element of I st j <> i holds x.j = 1_F.j )
iff
x = (1_product F)+*(i,g);
definition
let I be non empty set,
F be associative Group-like multMagma-Family of I,
i be Element of I;
func ProjSet(F,i) -> Subset of product F means
:: GROUP_12:def 1
for x be set holds x in it iff
ex g be Element of F.i st x = 1_product F +* (i,g);
end;
registration
let I be non empty set,
F be associative Group-like multMagma-Family of I,
i be Element of I;
cluster ProjSet(F,i) -> non empty;
end;
theorem :: GROUP_12:2
for x0 be set holds x0 in ProjSet(F,i) iff
ex x be Function,g be Element of F.i st x = x0 & dom x = I & x.i = g
& for j be Element of I st j <> i holds x.j = 1_F.j;
theorem :: GROUP_12:3
for g1,g2 be Element of product F,
z1,z2 be Element of F.i st
g1 = (1_(product F))+* (i,z1) &
g2 = (1_(product F))+* (i,z2) holds
g1 * g2 = (1_product F)+* (i,z1*z2);
theorem :: GROUP_12:4
for g1 be Element of product F,
z1 be Element of F.i st
g1 = (1_product F)+* (i,z1) holds
g1" = (1_product F)+* (i,z1");
theorem :: GROUP_12:5
for g1,g2 be Element of product F
st g1 in ProjSet(F,i) & g2 in ProjSet(F,i)
holds g1 * g2 in ProjSet(F,i);
theorem :: GROUP_12:6
for g be Element of product F st g in ProjSet(F,i)
holds g" in ProjSet(F,i);
definition
let I be non empty set,
F be associative Group-like multMagma-Family of I,
i be Element of I;
func ProjGroup(F,i) -> strict Subgroup of product F means
:: GROUP_12:def 2
the carrier of it = ProjSet(F,i);
end;
definition let I, F, i;
func 1ProdHom (F,i) -> Homomorphism of F.i, ProjGroup(F,i) means
:: GROUP_12:def 3
for x be Element of F.i holds it.x = 1_product F +* (i,x);
end;
registration let I, F, i;
cluster 1ProdHom (F,i) -> bijective;
end;
registration
let I,F,i;
cluster ProjGroup(F,i) -> normal;
end;
theorem :: GROUP_12:7
for x,y be Element of product F st i <> j &
x in ProjGroup(F,i) & y in ProjGroup(F,j) holds x*y = y*x;
reserve n for non zero Nat;
theorem :: GROUP_12:8
for F being associative Group-like multMagma-Family of Seg n,
J be Nat,
GJ be Group
st 1 <= J & J <= n & GJ = F.J holds
for x be Element of product F,
s be FinSequence of product F st len s < J
& (for k be Element of Seg n st k in dom s holds s.k in ProjGroup(F,k))
& x = Product s holds x.J = 1_GJ;
theorem :: GROUP_12:9
for F be associative Group-like multMagma-Family of Seg n,
x be Element of product F,
s be FinSequence of product F st len s = n
& (for k be Element of Seg n holds s.k in ProjGroup(F,k))
& x = Product s holds
for i be Nat st
1<= i & i<= n holds
ex si be Element of product F st si=s.i & x.i = si.i;
theorem :: GROUP_12:10
for F be associative Group-like multMagma-Family of Seg n,
x be Element of product F,
s,t be FinSequence of product F st len s = n
& (for k be Element of Seg n holds s.k in ProjGroup(F,k)) &
x=Product s & len t = n
& (for k be Element of Seg n holds t.k in ProjGroup(F,k))
& x=Product t holds s=t;
theorem :: GROUP_12:11
for F be associative Group-like multMagma-Family of Seg n,
x be Element of product F
ex s be FinSequence of product F st len s = n &
(for k be Element of Seg n holds s.k in ProjGroup(F,k)) & x=Product s;
theorem :: GROUP_12:12
for G being commutative Group,
F being associative Group-like multMagma-Family of Seg n
st (for i be Element of Seg n holds F.i is Subgroup of G)
& (for x be Element of G
ex s be FinSequence of G st len s = n
& (for k be Element of Seg n holds s.k in F.k) & x=Product s )
& ( for s,t be FinSequence of G st
len s = n & (for k be Element of Seg n holds s.k in F.k) & len t = n
& (for k be Element of Seg n holds t.k in F.k)
& Product s=Product t holds s=t ) holds
ex f being Homomorphism of product F,G
st f is bijective &
for x be Element of product F
ex s be FinSequence of G st len s= n &
(for k be Element of Seg n holds s.k in F.k) & s=x & f.x = Product s;
theorem :: GROUP_12:13
for G,F being associative commutative Group-like multMagma-Family of Seg n
st
for k be Element of Seg n holds F.k = ProjGroup(G,k)
holds
ex f being Homomorphism of product F,product G
st f is bijective &
for x be Element of product F
ex s be FinSequence of product G st len s= n &
(for k be Element of Seg n holds s.k in F.k) & s=x & f.x = Product s;