:: Internal Direct Products and the Universal Property of Direct Product
:: Groups
:: by Alexander M. Nelson
::
:: Received June 30, 2023
:: Copyright (c) 2023-2026 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 PRE_POLY, SEMI_AF1, FINSET_1, WELLORD1, NEWTON, MSSUBFAM, TARSKI,
NAT_1, QC_LANG1, RLSUB_1, XXREAL_0, ORDINAL4, XXREAL_1, BINOP_1, BINOP_2,
RLVECT_2, ZFMISC_1, RELAT_1, STRUCT_0, UPROOTS, FINSEQ_1, FUNCT_1,
FUNCT_2, FUNCT_3, FUNCT_4, FUNCOP_1, NUMBERS, PRALG_1, ALGSTR_0,
PARTFUN1, CARD_1, CARD_3, GROUP_1, GROUP_2, GROUP_3, PRE_TOPC, GROUP_4,
GROUP_6, GROUP_7, GROUP_12, SUBSET_1, XBOOLE_0, PBOOLE, VECTMETR,
GROUP_19, GROUP_20, GROUP_23, SETFAM_1, REALSET1, GROUP_5, ARYTM_3,
GRNILP_1;
notations FINSET_1, CARD_1, ZFMISC_1, TARSKI, XBOOLE_0, RELAT_1, SUBSET_1,
RELSET_1, FUNCT_1, BINOP_1, BINOP_2, REALSET1, FUNCT_2, FUNCT_7,
FUNCOP_1, PBOOLE, NAT_1, CARD_3, ORDINAL1, NUMBERS, XXREAL_0, STRUCT_0,
PARTFUN1, ALGSTR_0, SETFAM_1, PRALG_1, GROUP_19, GROUP_12, GROUP_7,
FINSEQ_1, FINSEQOP, GRSOLV_1, GROUP_3, GROUP_5, GROUP_1, GROUP_2,
GROUP_6, FUNCT_4, GROUP_4, GROUP_20, GRNILP_1;
constructors BINOP_2, PBOOLE, REALSET1, MONOID_0, PRALG_1, FUNCT_7, RELSET_1,
GRSOLV_1, GROUP_19, FINSOP_1, FINSEQOP, GROUP_4, GROUP_20, FUNCT_6,
GRNILP_1;
registrations XBOOLE_0, STRUCT_0, GROUP_2, MONOID_0, RELAT_1, FUNCT_1,
REALSET1, RELSET_1, XXREAL_0, FUNCT_2, FUNCOP_1, CARD_3, FINSET_1,
CARD_1, ORDINAL1, INT_1, FUNCT_4, GROUP_3, GROUP_6, GROUP_7, GROUP_19;
requirements BOOLE, SUBSET, NUMERALS;
equalities ALGSTR_0, FINSEQ_1, STRUCT_0, GROUP_2, GROUP_6;
expansions STRUCT_0, FUNCT_1;
theorems TARSKI, FUNCT_1, FUNCT_2, FUNCT_7, FUNCOP_1, CARD_3, GROUP_1,
GROUP_2, GROUP_3, GROUP_5, GROUP_6, GROUP_7, GROUP_12, PARTFUN1, PRALG_1,
GROUP_19, SETFAM_1, XBOOLE_0, GROUP_21, SUBSET_1, PBOOLE, GRSOLV_1,
RELAT_1, GROUP_22, XBOOLE_1, BINOP_1, ZFMISC_1, REALSET1, FINSEQ_1,
FINSEQOP, GROUP_4, FINSEQ_2, PARTFUN2, FUNCT_4, GROUP_20, FUNCT_6,
GRNILP_1, FUNCT_3;
schemes FUNCT_1, FUNCT_2, PBOOLE, FINSEQ_1, FINSEQ_2, FINSET_1;
begin :: Preliminaries
theorem LmEqRng:
for X,Y,Z,W being set st Z <> {} & W <> {}
for f being Function of [:X,Y:],Z
for g being Function of [:X,Y:],W
st (for a being Element of X, b being Element of Y holds f.(a,b) = g.(a,b))
holds f = g
proof
let X,Y,Z,W be set;
assume A0: Z <> {} & W <> {};
let f be Function of [:X,Y:],Z;
let g be Function of [:X,Y:],W;
assume A1: for a being Element of X, b being Element of Y
holds f.(a,b) = g.(a,b);
A2: dom f = [:X,Y:] & dom g = [:X,Y:] by FUNCT_2:def 1,A0;
for x,y being object st x in X & y in Y holds f.(x,y) = g.(x,y) by A1;
hence thesis by A2,FUNCT_3:6;
end;
ThCoim:
for f being Function
for X being non empty set
for x,x0 being Element of X
holds f.x = f.x0 iff x in {x1 where x1 is Element of X : f.x0 = f.x1 }
proof
let f be Function;
let X be non empty set;
let x,x0 be Element of X;
thus f.x = f.x0 implies x in {x1 where x1 is Element of X : f.x0 = f.x1 };
assume x in {x1 where x1 is Element of X : f.x0 = f.x1 };
then ex x1 being Element of X st x = x1 & f.x0 = f.x1;
hence thesis;
end;
theorem ThCanFSIsMss:
for A being finite set
holds canFS A is ManySortedSet of Seg (card A)
proof
let A be finite set;
set f=canFS A;
len f = card A by FINSEQ_1:93;
then A1: dom f = Seg (card A) by FINSEQ_1:def 3;
then reconsider f as (Seg (card A))-defined Function by RELAT_1:def 18;
f is total by A1, PARTFUN1:def 2;
hence canFS A is ManySortedSet of Seg (card A);
end;
theorem
for X,Y being non empty set
for f being Function of X,Y
st f is onto
ex g being Function of Y,X
st f * g = id Y
proof
let X,Y be non empty set;
let f be Function of X,Y;
assume A1: f is onto;
defpred P[object, object] means $1 = f.$2;
A2: for y being object st y in Y
ex x being object st x in X & P[y, x]
proof
let y be object;
assume y in Y;
then reconsider yy=y as Element of Y;
consider x being Element of X such that
B1: f.x = yy by A1, GROUP_6:58;
take x;
thus x in X;
thus P[y, x] by B1;
end;
consider g being Function of Y,X such that
A3: for y being object st y in Y holds P[y, g.y]
from FUNCT_2:sch 1(A2);
take g;
for y being Element of Y holds (f * g).y = y
proof
let y be Element of Y;
B1: dom g = Y & dom (f * g) = dom g by FUNCT_2:123, FUNCT_2:def 1;
y = f.(g.y) by A3
.= (f * g).y by B1, FUNCT_1:12;
hence (f * g).y = y;
end;
hence f * g = id Y by FUNCT_2:124;
end;
:: This probably belongs in PBOOLE
definition
let I be non empty set;
let A, B be ManySortedSet of I;
let f be ManySortedFunction of A,B;
let i be Element of I;
redefine func f.i -> Function of A.i, B.i; :: redefines . (FUNCT_1, definition)
coherence by PBOOLE:def 15;
end;
:: This probably belongs in PRALG_1
definition
let I be non empty set;
let F1,F2 be 1-sorted-yielding ManySortedSet of I;
mode ManySortedFunction of F1,F2
is ManySortedFunction of Carrier F1, Carrier F2;
end;
:: This probably belongs in PRALG_1
definition
let I be non empty set;
let F1,F2 be 1-sorted-yielding ManySortedSet of I;
let phi be ManySortedFunction of F1,F2;
let i be Element of I;
redefine func phi.i -> Function of F1.i, F2.i; :: redefines . (FUNCT_1, definition)
correctness
proof
A1: ex R being 1-sorted
st (R = F1.i & (Carrier F1).i = the carrier of R) by PRALG_1:def 15;
ex R2 being 1-sorted st (R2 = F2.i & (Carrier F2).i = the carrier of R2)
by PRALG_1:def 15;
hence thesis by A1, PBOOLE:def 15;
end;
end;
theorem Th25:
for I being non empty set
for A, B being ManySortedSet of I
for f being ManySortedSet of I
holds f is ManySortedFunction of A,B
iff (for i being Element of I holds f.i is Function of A.i, B.i)
proof
let I be non empty set;
let A, B be ManySortedSet of I;
let f be ManySortedSet of I;
thus f is ManySortedFunction of A,B
implies (for i being Element of I holds f.i is Function of A.i, B.i)
by PBOOLE:def 15;
assume for i being Element of I holds f.i is Function of A.i, B.i;
then for i being object st i in I holds
f.i is Function of (A.i), (B.i);
hence f is ManySortedFunction of A,B by PBOOLE:def 15;
end;
registration
let I,X be set;
cluster (bool X)-valued for ManySortedSet of I;
existence
proof
take M = I --> X;
for a being object st a in rng M holds a in bool X
proof
let a be object;
assume a in rng M;
then ex x being object st x in dom M & a = M.x by FUNCT_1:def 3;
then a = X by FUNCOP_1:7;
hence thesis by ZFMISC_1:def 1;
end;
hence M is (bool X)-valued by RELAT_1:def 19, TARSKI:def 3;
end;
end;
definition
let I,X be set;
let M be (bool X)-valued ManySortedSet of I;
redefine func Union M -> Subset of X; :: redefines Union (CARD_3, definition)
correctness
proof
for A being set st A in rng M holds A c= X
proof
let A be set;
assume A1: A in rng M;
rng M c= bool X by RELAT_1:def 19;
hence A c= X by A1;
end;
then union (rng M) c= X by ZFMISC_1:76;
hence Union M is Subset of X by CARD_3:def 4;
end;
end;
registration
let I be set;
let J be Subset of I;
let F be ManySortedSet of I;
cluster F|J -> J-defined total;
coherence
proof
J c= I;
then J c= dom F by PARTFUN1:def 2;
then dom (F|J) = J by RELAT_1:62;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let I be set;
let J be Subset of I;
let F be 1-sorted-yielding ManySortedSet of I;
cluster F|J -> 1-sorted-yielding J-defined total;
coherence
proof
for x being object st x in dom (F|J) holds (F|J).x is 1-sorted
proof
let x be object;
assume A1: x in dom (F|J);
J c= I & dom F = I by PARTFUN1:def 2;
then dom (F|J) c= dom F by RELAT_1:62;
then (F|J).x = F.x & F.x is 1-sorted by A1, FUNCT_1:47, PRALG_1:def 12;
hence (F|J).x is 1-sorted;
end;
hence thesis by PRALG_1:def 12;
end;
end;
theorem MssRng:
for I being non empty set
for M being ManySortedSet of I
for y being object
holds y in rng M iff (ex i being Element of I st y = M.i)
proof
let I be non empty set;
let M be ManySortedSet of I;
let y be object;
hereby
assume y in rng M;
then consider i0 being object such that
A1: i0 in dom M & y = M.i0 by FUNCT_1:def 3;
reconsider i=i0 as Element of I by A1;
take i;
thus y = M.i by A1;
end;
given i being Element of I such that
A2: y = M.i;
dom M = I by PARTFUN1:def 2;
hence y in rng M by A2, FUNCT_1:3;
end;
begin :: Sequences of group elements under homomorphisms
theorem ThMappingFrobProdProperty:
for G1, G2 being Group
for phi being Homomorphism of G1, G2
for F1 being FinSequence of the carrier of G1
for F2 being FinSequence of the carrier of G2
st F2 = phi * F1
holds Product F2 = phi.(Product F1)
proof
let G1, G2 be Group;
let phi be Homomorphism of G1, G2;
let F1 be FinSequence of the carrier of G1;
let F2 be FinSequence of the carrier of G2;
assume A2: F2 = phi * F1;
set n1 = len F1;
defpred P1[FinSequence of the carrier of G1] means
phi.(Product $1) = Product (phi * $1);
A3: P1[ <*>(the carrier of G1) ]
proof
phi.(Product <*>(the carrier of G1))
= phi.(1_G1) by GROUP_4:8
.= 1_(G2) by GROUP_6:31
.= Product (<*>(the carrier of G2)) by GROUP_4:8;
hence thesis;
end;
A4: for p0 being FinSequence of the carrier of G1
for x being Element of the carrier of G1 st P1[p0]
holds P1[(p0 ^ <* x *>)]
proof
let p0 be FinSequence of the carrier of G1;
let x be Element of the carrier of G1;
assume B1: P1[p0];
Product (p0 ^ <* x *>) = (Product p0) * x by GROUP_4:6;
then phi.(Product (p0 ^ <* x *>))
= (phi.(Product p0)) * (phi.x) by GROUP_6:def 6
.= Product ((phi * p0) ^ <* phi.x *>) by B1,GROUP_4:6;
hence P1[(p0 ^ <* x *>)] by FINSEQOP:8;
end;
A5: for p0 being FinSequence of the carrier of G1 holds P1[p0]
from FINSEQ_2:sch 2(A3, A4);
thus Product F2 = phi.(Product F1) by A2, A5;
end;
theorem ThMappingFrobProd:
for G1, G2 being Group
for phi being Homomorphism of G1, G2
for F1 being FinSequence of the carrier of G1
ex F2 being FinSequence of the carrier of G2
st len F1 = len F2
& F2 = phi * F1
& Product F2 = phi.(Product F1)
proof
let G1, G2 be Group;
let phi be Homomorphism of G1, G2;
let F1 be FinSequence of the carrier of G1;
set n1 = len F1;
defpred P[object, object] means ex k being Nat st k = $1 &
$2 = phi.(F1.k);
A1: for k being Nat st k in Seg n1 holds ex x being object st P[k, x]
proof
let k be Nat;
assume k in Seg n1;
consider x being object such that
B1: x = phi.(F1.k);
take x;
thus P[k, x] by B1;
end;
consider p being FinSequence such that
A2: dom p = Seg n1 and
A3: for k being Nat st k in Seg n1 holds P[k, p.k]
from FINSEQ_1:sch 1(A1);
A4: len F1 = len p by A2, FINSEQ_1:def 3;
A5: p = phi * F1
proof
B1: len p = len (phi * F1) by A4, FINSEQ_2:33;
for k being Nat st 1 <= k & k <= len p holds p.k = (phi * F1).k
proof
let k be Nat;
assume B2: 1 <= k;
assume B3: k <= len p;
then k in Seg n1 by A4, B2;
then B4: k in dom F1 by FINSEQ_1:def 3;
P[k, p.k] by A3, A4, B2, B3, FINSEQ_1:1;
hence p.k = (phi * F1).k by B4, FUNCT_1:13;
end;
hence thesis by B1, FINSEQ_1:def 18;
end;
then reconsider p as FinSequence of the carrier of G2;
take F2 = p;
thus len F1 = len F2 by A4;
thus F2 = phi * F1 by A5;
thus thesis by A5,ThMappingFrobProdProperty;
end;
theorem ThMappingFrobProd2:
for G1, G2 being Group
for phi being Homomorphism of G1, G2
for F1 being FinSequence of the carrier of G1
for ks being FinSequence of INT
ex F2 being FinSequence of the carrier of G2
st len F1 = len F2
& F2 = phi * F1
& Product (F2 |^ ks) = phi.(Product (F1 |^ ks))
proof
let G1, G2 be Group;
let phi be Homomorphism of G1, G2;
let F1 be FinSequence of the carrier of G1;
let ks be FinSequence of INT;
consider F2 being FinSequence of the carrier of G2 such that
A2: len F1 = len F2 & F2 = phi * F1 & Product F2 = phi.(Product F1)
by ThMappingFrobProd;
take F2;
thus len F1 = len F2 & F2 = phi * F1 by A2;
A3: len (F1 |^ ks) = len (F1) by GROUP_4:def 3
.= len (F2 |^ ks) by A2, GROUP_4:def 3;
A4: len (phi * (F1 |^ ks)) = len (F1 |^ ks) by FINSEQ_2:33;
for k being Nat st k in dom (F2 |^ ks)
holds (phi * (F1 |^ ks)).k = (F2 |^ ks).k
proof
let k be Nat;
assume k in dom (F2 |^ ks);
then k in Seg (len (F1 |^ ks)) by A3, FINSEQ_1:def 3;
then B1: k in dom (F1 |^ ks) by FINSEQ_1:def 3;
then k in Seg (len (F1 |^ ks)) by FINSEQ_1:def 3;
then k in Seg (len (F1)) by GROUP_4:def 3;
then B2: k in dom F1 by FINSEQ_1:def 3;
then k in Seg (len (F2)) by A2, FINSEQ_1:def 3;
then B3: k in dom F2 by FINSEQ_1:def 3;
B4: F1 /. k in G1 & dom phi = the carrier of G1 by FUNCT_2:def 1;
set g = (F1 /. k);
set n = (@ (ks /. k));
(phi * (F1 |^ ks)).k = phi.((F1 |^ ks).k) by B1, FUNCT_1:13
.= phi.(g |^ n) by B2, GROUP_4:def 3
.= (phi /. g) |^ n by GROUP_6:37
.= ((phi * F1)/.k) |^ n by B2, B4, PARTFUN2:4
.= (F2 |^ ks).k by A2, B3, GROUP_4:def 3;
hence (phi * (F1 |^ ks)).k = (F2 |^ ks).k;
end;
hence thesis by A3, A4, ThMappingFrobProdProperty, FINSEQ_2:9;
end;
begin :: Preliminary Work about Group-Families and Group-Yielding Many Sorted Sets
definition
let IT be Relation;
attr IT is Group-yielding means :Def1:
for G being object st G in rng IT holds G is Group;
end;
registration
cluster Group-yielding -> 1-sorted-yielding for Function;
coherence
proof
let IT be Function;
assume IT is Group-yielding;
then for x being object st x in rng IT holds x is 1-sorted;
hence thesis by PRALG_1:def 11;
end;
cluster Group-yielding -> multMagma-yielding for Function;
coherence
proof
let IT be Function;
assume IT is Group-yielding;
then for x being set st x in rng IT holds x is non empty multMagma;
hence thesis by GROUP_7:def 1;
end;
end;
theorem Th4:
for I being set
for F being associative Group-like multMagma-Family of I
holds F is Group-yielding
proof
let I be set;
let F be associative Group-like multMagma-Family of I;
let y be object;
assume y in rng F;
then ex x being object st x in dom F & y = F.x by FUNCT_1:def 3;
hence y is Group by GROUP_19:1;
end;
registration
let I be set;
cluster Group-yielding for ManySortedSet of I;
existence
proof
set G = the trivial Group;
set f = I --> G;
take f;
let a be object;
assume a in rng f;
then ex x being object st x in dom f & a = f.x by FUNCT_1:def 3;
hence thesis by FUNCOP_1:7;
end;
end;
registration
let I be set;
cluster associative Group-like -> Group-yielding for multMagma-Family of I;
coherence by Th4;
end;
registration
cluster Group-yielding for Function;
existence
proof
set I = the set, f = the Group-yielding ManySortedSet of I;
take f;
thus thesis;
end;
end;
theorem Th5:
for I being non empty set
for F being Group-yielding ManySortedSet of I
for i being Element of I
holds F.i is Group
proof
let I be non empty set;
let F be Group-yielding ManySortedSet of I;
let i be Element of I;
i in I & dom F = I by PARTFUN1:def 2;
then F.i in rng F by FUNCT_1:3;
hence F.i is Group by Def1;
end;
registration
let I be non empty set;
let i be Element of I;
let F be Group-yielding ManySortedSet of I;
cluster (F . i) -> Group-like associative unital non empty for multMagma;
correctness by Th5;
end;
theorem
for I being set
for F being ManySortedSet of I
holds F is Group-yielding
iff (for i being object st i in I holds F.i is Group)
proof
let I be set;
let F be ManySortedSet of I;
hereby
assume A1: F is Group-yielding;
let i be object;
assume i in I;
then i in dom F by PARTFUN1:def 2;
hence F.i is Group by A1, FUNCT_1:3;
end;
assume A2: for i being object st i in I holds F.i is Group;
for y being object st y in rng F holds y is Group
proof
let y be object;
assume y in rng F;
then consider i being object such that
A3: i in dom F & y = F.i by FUNCT_1:def 3;
thus y is Group by A2, A3;
end;
hence F is Group-yielding;
end;
registration
let I be set;
cluster Group-yielding -> Group-like associative for multMagma-Family of I;
correctness
proof
thus for F being multMagma-Family of I st F is Group-yielding
holds F is Group-like associative
proof
let F be multMagma-Family of I;
assume A1: F is Group-yielding;
A2: dom F = I by PARTFUN1:def 2;
A3: for i being set st i in I
ex Fi being non empty Group-like multMagma st Fi = F.i
proof
let i be set;
assume i in I;
then F.i is Group by A1, A2, FUNCT_1:3;
hence thesis;
end;
for i being set st i in I
ex Fi being non empty associative multMagma st Fi = F.i
proof
let i be set;
assume i in I;
then F.i is Group by A1, A2, FUNCT_1:3;
hence thesis;
end;
hence F is Group-like associative by A3, GROUP_7:def 3,def 4;
end;
end;
end;
registration
let I be set;
cluster -> Group-yielding for Group-like associative multMagma-Family of I;
coherence;
end;
registration
let I be set;
cluster -> Group-like associative multMagma-yielding for
Group-yielding ManySortedSet of I;
coherence;
end;
reserve I for non empty set;
reserve i for Element of I;
reserve F for Group-Family of I;
reserve G for Group;
theorem
{} --> G is Group-Family of {};
theorem
for n being Nat holds Seg n --> G is Group-Family of Seg n;
registration
let G be Group;
let n be Nat;
cluster Seg n --> G -> Group-yielding;
correctness;
end;
theorem Th9:
(Carrier F).i = the carrier of F.i
proof
ex R being 1-sorted st R = F.i & (Carrier F).i = the carrier of R
by PRALG_1:def 15;
hence thesis;
end;
scheme GrFamSch { I1() -> non empty set,
Fun(Element of I1()) -> Group } :
ex Fam being Group-Family of I1()
st for i being Element of I1() holds Fam.i = Fun(i)
proof
consider F being ManySortedSet of I1() such that
A1: for i being Element of I1() holds F.i = Fun(i)
from PBOOLE:sch 5;
for y being object st y in rng F holds y is Group
proof
let y be object;
assume y in rng F;
then consider x being object such that
B2: x in dom F & y = F.x by FUNCT_1:def 3;
reconsider i=x as Element of I1() by B2;
y = Fun(i) by A1, B2;
hence y is Group;
end;
then F is Group-yielding;
then reconsider F as Group-Family of I1();
take F;
thus thesis by A1;
end;
begin :: Subgroup-Family of a Family of Groups
definition
let I be set;
let F, IT be Group-Family of I;
attr IT is F-Subgroup-yielding means :Def2:
for i being Element of I
for G being Group st G = F.i
holds IT.i is Subgroup of G;
end;
theorem
for S being Group-Family of I
holds S is F-Subgroup-yielding
iff (for i being Element of I holds S.i is Subgroup of F.i);
theorem ThSubYieldRefl:
for I being set
for F being Group-Family of I
holds F is F-Subgroup-yielding by GROUP_2:54;
registration
let I be set;
let F be Group-Family of I;
cluster F-Subgroup-yielding for Group-Family of I;
existence by ThSubYieldRefl;
end;
definition
let I be set;
let F be Group-Family of I;
mode Subgroup-Family of F is F-Subgroup-yielding Group-Family of I;
end;
definition
let I be non empty set;
let F be Group-Family of I;
let S be Subgroup-Family of F;
let i be Element of I;
redefine func S.i -> Subgroup of F.i; :: redefines . (FUNCT_1, definition)
correctness by Def2;
end;
reserve S for Subgroup-Family of F;
theorem
for S being Group-Family of I
holds S is Subgroup-Family of F
iff (for i being Element of I holds S.i is Subgroup of F.i)
proof
let S be Group-Family of I;
thus (S is Subgroup-Family of F) implies (for i being Element of I
holds S.i is Subgroup of F.i)
proof
assume A1: S is Subgroup-Family of F;
let i be Element of I;
reconsider SS=S as Subgroup-Family of F by A1;
S.i = SS.i;
hence thesis;
end;
assume for i being Element of I holds S.i is Subgroup of F.i;
then S is F-Subgroup-yielding;
hence S is Subgroup-Family of F;
end;
scheme SubFamSch { I1() -> non empty set,
Fam() -> Group-Family of I1(),
Sub(Group) -> Group } :
ex S being Subgroup-Family of Fam()
st for i being Element of I1() holds S.i = Sub(Fam().i)
provided
A1: for G being Group holds Sub(G) is Subgroup of G
proof
deffunc F2(Element of I1()) = Sub(Fam().$1);
consider S being ManySortedSet of I1() such that
A2: for i being Element of I1() holds S.i = F2(i)
from PBOOLE:sch 5;
for y being object st y in rng S holds y is Group
proof
let y be object;
assume y in rng S;
then consider x being object such that
B2: x in dom S & y = S.x by FUNCT_1:def 3;
reconsider i=x as Element of I1() by B2;
y = F2(i) by A2, B2;
hence y is Group;
end;
then S is Group-yielding;
then reconsider S as Group-Family of I1();
for i being Element of I1() holds S.i is Subgroup of Fam().i
proof
let i be Element of I1();
S.i = Sub(Fam().i) by A2;
hence S.i is Subgroup of Fam().i by A1;
end;
then S is Fam()-Subgroup-yielding;
then reconsider S as Subgroup-Family of Fam();
take S;
thus thesis by A2;
end;
:: Re-defining "strict" for Subgroup-Family seemed like a risky move,
:: so I opted to introduce an adjective which captured what was needed.
definition
let I be non empty set;
let IT be Group-Family of I;
attr IT is componentwise_strict means :Def3:
for i being Element of I holds IT.i is strict;
end;
registration
let I be non empty set;
cluster componentwise_strict for Group-Family of I;
existence
proof
reconsider G = multMagma (# REAL, addreal #) as strict Group
by GROUP_1:46;
deffunc Fun(Element of I) = G;
consider F being Group-Family of I such that
A1: for i being Element of I holds F.i = Fun(i)
from GrFamSch;
take F;
thus thesis by A1;
end;
end;
theorem Def4:
for I be non empty set
for F be Group-Family of I
for IT be Subgroup-Family of F holds
IT is componentwise_strict iff
for i being Element of I holds IT.i is strict Subgroup of F.i;
registration
let I be non empty set;
let F be Group-Family of I;
cluster componentwise_strict for Subgroup-Family of F;
existence
proof
deffunc Sub(Group) = (1).$1;
A1: for G being Group holds Sub(G) is Subgroup of G;
consider S being Subgroup-Family of F such that
A2: for i being Element of I holds S.i = Sub(F.i)
from SubFamSch(A1);
take S;
for i being Element of I holds S.i is strict Subgroup of F.i
proof
let i be Element of I;
S.i = (1).(F.i) by A2;
hence thesis;
end;
hence thesis;
end;
end;
registration
let I be non empty set;
let F be Group-Family of I;
let S be componentwise_strict Subgroup-Family of F;
let i be Element of I;
cluster (S . i) -> strict for Subgroup of F.i;
correctness by Def3;
end;
scheme StrSubFamSch { I1() -> non empty set,
Fam() -> Group-Family of I1(),
Sub(Group) -> Group } :
ex S being componentwise_strict Subgroup-Family of Fam()
st for i being Element of I1() holds S.i = Sub(Fam().i)
provided
A1: for G being Group holds Sub(G) is strict Subgroup of G
proof
A2: for G being Group holds Sub(G) is Subgroup of G by A1;
consider S being Subgroup-Family of Fam() such that
A3: for i being Element of I1() holds S.i = Sub(Fam().i)
from SubFamSch(A2);
for i being Element of I1()
holds S.i is strict Subgroup of Fam().i
proof
let i be Element of I1();
S.i = Sub(Fam().i) by A3;
hence S.i is strict Subgroup of Fam().i by A1;
end;
then S is componentwise_strict;
then reconsider S as componentwise_strict Subgroup-Family of Fam();
take S;
thus thesis by A3;
end;
theorem ThStrSubEq:
for A,B being Subgroup-Family of F
st (for i being Element of I holds A.i = B.i)
holds A = B
proof
let A,B be Subgroup-Family of F;
assume for i being Element of I holds A.i = B.i;
then for i being object st i in I holds A.i = B.i;
hence A = B by PBOOLE:3;
end;
definition
let I be non empty set;
let F be Group-Family of I;
func (1).F -> componentwise_strict Subgroup-Family of F means
:Def5:
for i being Element of I holds it.i = (1).(F.i);
existence
proof
deffunc Sub(Group) = (1).$1;
A1: for G being Group holds Sub(G) is strict Subgroup of G;
thus ex S being componentwise_strict Subgroup-Family of F
st for i being Element of I holds S.i = Sub(F.i)
from StrSubFamSch(A1);
end;
uniqueness
proof
thus for A,B being componentwise_strict Subgroup-Family of F
st (for i being Element of I holds A.i = (1).(F.i))
& (for i being Element of I holds B.i = (1).(F.i))
holds A = B
proof
let A,B be componentwise_strict Subgroup-Family of F;
assume A1: for i being Element of I holds A.i = (1).(F.i);
assume A2: for i being Element of I holds B.i = (1).(F.i);
for i being Element of I holds A.i = B.i
proof
let i be Element of I;
thus A.i = (1).(F.i) by A1
.= B.i by A2;
end;
hence thesis by ThStrSubEq;
end;
end;
end;
definition
let I be non empty set;
let F be Group-Family of I;
func (Omega).F -> componentwise_strict Subgroup-Family of F means
:Def6:
for i being Element of I holds it.i = (Omega).(F.i);
existence
proof
deffunc Sub(Group) = (Omega).$1;
A1: for G being Group holds Sub(G) is strict Subgroup of G;
thus ex S being componentwise_strict Subgroup-Family of F
st for i being Element of I holds S.i = Sub(F.i)
from StrSubFamSch(A1);
end;
uniqueness
proof
thus for A,B being componentwise_strict Subgroup-Family of F
st (for i being Element of I holds A.i = (Omega).(F.i))
& (for i being Element of I holds B.i = (Omega).(F.i))
holds A = B
proof
let A,B be componentwise_strict Subgroup-Family of F;
assume A1: for i being Element of I holds A.i = (Omega).(F.i);
assume A2: for i being Element of I holds B.i = (Omega).(F.i);
for i being Element of I holds A.i = B.i
proof
let i be Element of I;
thus A.i = (Omega).(F.i) by A1
.= B.i by A2;
end;
hence thesis by ThStrSubEq;
end;
end;
end;
definition
let I be non empty set;
let F be Group-Family of I;
let IT be Subgroup-Family of F;
attr IT is normal means :Def7:
for i being Element of I holds IT.i is normal Subgroup of F.i;
end;
registration
let I be non empty set;
let F be Group-Family of I;
cluster componentwise_strict normal for Subgroup-Family of F;
existence
proof
deffunc Sub(Group) = (1).$1;
A1: for G being Group holds Sub(G) is strict Subgroup of G;
consider S being componentwise_strict Subgroup-Family of F such that
A2: for i being Element of I holds S.i = Sub(F.i)
from StrSubFamSch(A1);
take S;
for i being Element of I holds S.i is normal Subgroup of F.i
proof
let i be Element of I;
S.i = (1).(F.i) by A2;
hence thesis;
end;
hence thesis;
end;
end;
registration
let I be non empty set;
let F be Group-Family of I;
let S be normal Subgroup-Family of F;
let i be Element of I;
cluster (S . i) -> normal for Subgroup of F.i;
correctness by Def7;
end;
registration
let I be non empty set;
let F be Group-Family of I;
let S be componentwise_strict Subgroup-Family of F;
let i be Element of I;
cluster (S . i) -> strict for Subgroup of F.i;
correctness;
end;
registration
let I be non empty set;
let F be Group-Family of I;
cluster (1).F -> normal;
correctness
proof
for i being Element of I holds ((1).F).i is normal Subgroup of F.i
proof
let i be Element of I;
((1).F).i = (1).(F.i) by Def5;
hence thesis;
end;
hence (1).F is normal;
end;
cluster (Omega).F -> normal;
correctness
proof
for i being Element of I holds ((Omega).F).i is normal Subgroup of F.i
proof
let i be Element of I;
((Omega).F).i = (Omega).(F.i) by Def6;
hence thesis;
end;
hence (Omega).F is normal;
end;
end;
definition
let I be non empty set;
let F be Group-Family of I;
let N be normal Subgroup-Family of F;
func F ./. N -> Group-Family of I means :Def8:
for i being Element of I
holds it.i = (F.i) ./. (N.i);
existence
proof
deffunc Fun(Element of I) = (F.$1) ./. (N.$1);
thus ex Fam being Group-Family of I
st for i being Element of I holds Fam.i = Fun(i)
from GrFamSch;
end;
uniqueness
proof
thus for A, B being Group-Family of I
st (for i being Element of I holds A.i = (F.i) ./. (N.i))
& (for i being Element of I holds B.i = (F.i) ./. (N.i))
holds A = B
proof
let A, B be Group-Family of I;
assume A1: for i being Element of I holds A.i = (F.i) ./. (N.i);
assume A2: for i being Element of I holds B.i = (F.i) ./. (N.i);
for i being object st i in I
holds A.i = B.i
proof
let i be object;
assume i in I;
then reconsider j=i as Element of I;
A.j = (F.j) ./. (N.j) by A1
.= B.j by A2;
hence thesis;
end;
hence A = B by PBOOLE:3;
end;
end;
end;
registration
let I be non empty set;
let F be Group-Family of I;
let N be normal Subgroup-Family of F;
cluster F ./. N -> componentwise_strict;
correctness
proof
for i being Element of I
holds (F ./. N).i is strict Group
proof
let i be Element of I;
(F ./. N).i = (F.i) ./. (N.i) by Def8;
hence thesis;
end;
hence thesis;
end;
end;
theorem
ex S being componentwise_strict normal Subgroup-Family of F
st for i being Element of I holds S.i = (F.i)`
proof
deffunc Fun(Group) = ($1)`;
A1: for G being Group holds Fun(G) is strict Subgroup of G;
consider S being componentwise_strict Subgroup-Family of F such that
A2: for i being Element of I holds S.i = Fun(F.i)
from StrSubFamSch(A1);
for i being Element of I holds S.i is normal Subgroup of F.i
proof
let i be Element of I;
S.i = (F.i)` by A2;
hence S.i is normal Subgroup of F.i;
end;
then reconsider S as componentwise_strict normal Subgroup-Family of F
by Def7;
take S;
thus thesis by A2;
end;
theorem LmTriv:
for M being strict multMagma
st (ex x being object st the carrier of M = {x})
ex G being strict trivial Group st M = G
proof
let M be strict multMagma;
given x being object such that
A1: the carrier of M = {x};
reconsider M as non empty multMagma by A1;
reconsider x as Element of M by A1, TARSKI:def 1;
A2: for a,b,c being Element of M holds (a * b) * c = a * (b * c)
proof
let a,b,c be Element of M;
(a * b) * c = x & a * (b * c) = x by A1, TARSKI:def 1;
hence (a * b) * c = a * (b * c);
end;
ex e being Element of M st
for h being Element of M holds
(h * e = h & e * h = h & ex g being Element of M st (h * g = e & g * h = e))
proof
take e = x;
let h be Element of M;
h = x by A1, TARSKI:def 1;
hence h * e = h & e * h = h by A1, TARSKI:def 1;
take g = x;
thus thesis by A1, TARSKI:def 1;
end;
then reconsider G=M as strict trivial Group by A1, A2, GROUP_1:def 2,def 3;
take G;
thus thesis;
end;
theorem
for I being empty set
for F being multMagma-Family of I
holds product F is trivial Group
proof
let I be empty set;
let F be multMagma-Family of I;
product (Carrier F) = {{}} by CARD_3:10;
then ex G being strict trivial Group st (product F)=G
by LmTriv, GROUP_7:def 2;
hence thesis;
end;
begin :: Inclusion Morphism
definition
let G, H be Group;
assume A1: H is Subgroup of G;
func incl (H, G) -> Homomorphism of H, G equals :Def9:
id (the carrier of H);
coherence
proof
set f = id (the carrier of H);
f is Function of the carrier of H, the carrier of G
proof
B1: dom f = the carrier of H;
rng f c= the carrier of G by A1, GROUP_2:def 5;
hence f is Function of the carrier of H, the carrier of G
by B1, FUNCT_2:2;
end;
then reconsider f as Function of H, G;
for g,h being Element of H
holds f.(g * h) = (f.g) * (f.h) by A1, GROUP_2:43;
hence id (the carrier of H) is Homomorphism of H, G by GROUP_6:def 6;
end;
end;
definition
let G be Group, H be Subgroup of G;
func incl H -> Homomorphism of H,G equals
incl (H, G);
coherence;
end;
theorem Th18:
for H being Group
for h being Element of H
st H is Subgroup of G
holds (incl (H, G)).h = h
proof
let H be Group;
let h be Element of H;
assume H is Subgroup of G;
hence (incl (H, G)).h = (id the carrier of H).h by Def9
.= h;
end;
theorem Th19:
for H being Subgroup of G
holds incl (H, G) is one-to-one
& Image (incl (H, G)) = the multMagma of H
proof
let H be Subgroup of G;
set f = incl (H, G);
A1: f = id (the carrier of H) by Def9; then
A2: the carrier of H = rng f
.= the carrier of (Image f) by GROUP_6:44;
Ker f = (1).H
proof
for h being Element of H holds h in Ker f iff h in (1).H
proof
let h be Element of H;
hereby
assume h in Ker f;
then f.h = 1_G by GROUP_6:41
.= 1_H by GROUP_2:44;
then h in {1_H} by A1, TARSKI:def 1;
hence h in (1).H by GROUP_2:def 7;
end;
assume h in (1).H;
then h in {1_H} by GROUP_2:def 7;
then h = 1_H by TARSKI:def 1;
then f.h = 1_G by GROUP_6:31;
hence h in Ker f by GROUP_6:41;
end;
hence thesis by GROUP_2:def 6;
end;
hence f is one-to-one by GROUP_6:56;
thus Image f = the multMagma of H by A2, GROUP_2:59;
end;
registration
let G be Group, H be Subgroup of G;
cluster incl (H, G) -> one-to-one;
correctness by Th19;
end;
theorem
for H,K being Group st H is Subgroup of G
for phi being Homomorphism of G,K
holds phi|(the carrier of H) = phi * (incl (H, G))
proof
let H,K be Group;
assume A1: H is Subgroup of G;
let phi be Homomorphism of G,K;
A2: dom (phi|(the carrier of H)) = the carrier of H
proof
dom phi = the carrier of G by FUNCT_2:def 1;
hence dom (phi|(the carrier of H)) = the carrier of H
by A1, GROUP_2:def 5, RELAT_1:62;
end;
for x being object st x in dom (phi|(the carrier of H))
holds (phi|(the carrier of H)).x = (phi * (incl (H, G))).x
proof
let x be object;
assume B1: x in dom (phi|(the carrier of H));
hence (phi * (incl (H, G))).x
= phi.((incl (H, G)).x) by A2, FUNCT_2:15
.= phi.x by A1, A2, B1, Th18
.= (phi|(the carrier of H)).x by B1, FUNCT_1:47;
end;
hence phi|(the carrier of H) = phi * (incl (H, G))
by A2, FUNCT_2:def 1;
end;
theorem
for K being Group
for H being Subgroup of G
for phi being Homomorphism of G,K
holds phi|H = phi * (incl H)
proof
let K be Group;
let H be Subgroup of G;
let phi be Homomorphism of G,K;
for h being Element of H holds
(phi|H).h = (phi * (incl H)).h
proof
let h be Element of H;
(incl H).h = (id (the carrier of H)).h
& dom (incl H) = the carrier of H by Def9, FUNCT_2:def 1;
then A1: (phi * (incl H)).h = phi.h by FUNCT_1:13;
h in G by GROUP_2:41;
then h in dom phi by FUNCT_2:def 1;
then h in (dom phi) /\ (the carrier of H) by XBOOLE_0:def 4;
then (phi|the carrier of H).h = phi.h by FUNCT_1:48;
hence (phi|H).h = (phi * (incl H)).h by A1, GRSOLV_1:def 2;
end;
hence phi|H = phi * (incl H) by FUNCT_2:def 8;
end;
theorem
for G being Group
for H being strict Subgroup of G
holds Image (incl H) = H
proof
let G be Group;
let H be strict Subgroup of G;
the carrier of H c= the carrier of H;
then the carrier of H
= (id the carrier of H) .: (the carrier of H) by FUNCT_1:92
.= (incl H) .: (the carrier of H) by Def9
.= the carrier of Image (incl H) by GROUP_6:def 10;
hence Image(incl H) = H by GROUP_2:59;
end;
begin :: Families of Homomorphisms
definition
let G be Group;
let I be non empty set;
let F be Group-Family of I;
mode Homomorphism-Family of G, F -> ManySortedFunction of I means
:Def10:
for i being Element of I holds
it.i is Homomorphism of G, F.i;
existence
proof
deffunc F1() = I;
deffunc F2(Element of I) = 1:(G, F.$1);
consider f being ManySortedSet of F1() such that
A1: for i being Element of F1() holds f.i = F2(i)
from PBOOLE:sch 5;
for x being object st x in dom f holds f.x is Function
proof
let x be object;
assume x in dom f;
then reconsider i=x as Element of I;
f.i = 1:(G,F.i) by A1;
hence f.x is Function;
end;
then reconsider f as ManySortedFunction of I by FUNCOP_1:def 6;
take f;
thus for i being Element of I holds f.i is Homomorphism of G, F.i
proof
let i be Element of I;
f.i = 1:(G, F.i) by A1;
hence f.i is Homomorphism of G, F.i;
end;
end;
end;
:: I hate this, but have no better alternative
definition
let G be Group;
let I be non empty set;
let F be Group-Family of I;
let f be Homomorphism-Family of G, F;
let i be Element of I;
redefine func f.i -> Homomorphism of G, F.i; :: redefines . (FUNCT_1, definition)
coherence by Def10;
end;
reserve f for Homomorphism-Family of G, F;
theorem
[i, f.i] in f
proof
i in I & f is ManySortedSet of I;
then i in dom f by PARTFUN1:def 2;
hence [i, f.i] in f by FUNCT_1:def 2;
end;
definition
let I be non empty set;
let F1,F2 be Group-Family of I;
mode Homomorphism-Family of F1,F2 -> ManySortedFunction of F1,F2 means
:Def11:
for i being Element of I
holds it.i is Homomorphism of F1.i,F2.i;
existence
proof
deffunc Fun(Element of I) = 1:(F1.$1, F2.$1);
consider phi being ManySortedSet of I such that
A1: for i being Element of I holds phi.i = Fun(i)
from PBOOLE:sch 5;
A2: for i being Element of I holds phi.i is Homomorphism of F1.i,F2.i
proof
let i be Element of I;
phi.i = 1:(F1.i, F2.i) by A1;
hence phi.i is Homomorphism of F1.i,F2.i;
end;
for i being Element of I
holds phi.i is Function of (Carrier F1).i, (Carrier F2).i
proof
let i be Element of I;
the carrier of F1.i = (Carrier F1).i
& the carrier of F2.i = (Carrier F2).i by Th9;
hence phi.i is Function of (Carrier F1).i, (Carrier F2).i by A2;
end;
then reconsider phi as ManySortedFunction of F1,F2 by Th25;
take phi;
thus thesis by A2;
end;
end;
registration
let I be non empty set;
let F1,F2 be Group-Family of I;
let i be Element of I;
let phi be Homomorphism-Family of F1,F2;
cluster (phi . i) -> multiplicative for Function of F1.i, F2.i;
correctness by Def11;
end;
theorem ThHom:
for I being non empty set
for A, B being Group-Family of I
for f being ManySortedSet of I
holds f is Homomorphism-Family of A,B
iff (for i being Element of I holds f.i is Homomorphism of A.i, B.i)
proof
let I be non empty set;
let A, B be Group-Family of I;
let f be ManySortedSet of I;
thus f is Homomorphism-Family of A,B
implies (for i being Element of I holds f.i is Homomorphism of A.i, B.i)
proof
assume A1: f is Homomorphism-Family of A,B;
let i be Element of I;
reconsider ff=f as Homomorphism-Family of A,B by A1;
ff.i = f.i & ff.i is Homomorphism of A.i, B.i;
hence thesis;
end;
thus (for i being Element of I holds f.i is Homomorphism of A.i, B.i)
implies f is Homomorphism-Family of A, B
proof
assume A1: for i being Element of I holds f.i is Homomorphism of A.i, B.i;
for i being object st i in I
holds f.i is Function of (Carrier A).i, (Carrier B).i
proof
let i be object;
assume i in I;
then reconsider ii=i as Element of I;
(Carrier A).i = the carrier of A.ii &
(Carrier B).i = the carrier of B.ii by Th9;
hence f.i is Function of (Carrier A).i, (Carrier B).i by A1;
end;
then f is ManySortedFunction of (Carrier A), (Carrier B) by PBOOLE:def 15;
hence thesis by A1, Def11;
end;
end;
scheme HomFamSch { I1() -> non empty set,
Dom() -> Group-Family of I1(),
Cod() -> Group-Family of I1(),
Fun(Element of I1()) -> Function } :
ex H being Homomorphism-Family of Dom(), Cod()
st for i being Element of I1() holds H.i = Fun(i)
provided
A1: for i being Element of I1()
holds Fun(i) is Homomorphism of Dom().i, Cod().i
proof
consider H being ManySortedSet of I1() such that
A2: for i being Element of I1() holds H.i = Fun(i)
from PBOOLE:sch 5;
for i being Element of I1()
holds H.i is Homomorphism of Dom().i, Cod().i
proof
let i be Element of I1();
H.i = Fun(i) by A2;
hence H.i is Homomorphism of Dom().i, Cod().i by A1;
end;
then reconsider H as Homomorphism-Family of Dom(), Cod() by ThHom;
take H;
thus thesis by A2;
end;
theorem ThRHom:
for G being Group
for I being non empty set
for F being Group-Family of I
for f being ManySortedSet of I
holds f is Homomorphism-Family of G,F
iff (for i being Element of I holds f.i is Homomorphism of G, F.i)
proof
let G be Group;
let I be non empty set;
let F be Group-Family of I;
let f be ManySortedSet of I;
thus f is Homomorphism-Family of G,F
implies (for i being Element of I holds f.i is Homomorphism of G, F.i)
by Def10;
assume A1: for i being Element of I
holds f.i is Homomorphism of G, F.i;
for i being object st i in dom f holds f.i is Function by A1;
then f is Function-yielding by FUNCOP_1:def 6;
hence f is Homomorphism-Family of G,F by A1, Def10;
end;
scheme RHomFamSch { I1() -> non empty set,
Dom() -> Group,
Cod() -> Group-Family of I1(),
Fun(Element of I1()) -> Function } :
ex H being Homomorphism-Family of Dom(), Cod()
st for i being Element of I1() holds H.i = Fun(i)
provided
A1: for i being Element of I1()
holds Fun(i) is Homomorphism of Dom(), Cod().i
proof
consider H being ManySortedSet of I1() such that
A2: for i being Element of I1() holds H.i = Fun(i)
from PBOOLE:sch 5;
for i being Element of I1()
holds H.i is Homomorphism of Dom(), Cod().i
proof
let i be Element of I1();
H.i = Fun(i) by A2;
hence H.i is Homomorphism of Dom(), Cod().i by A1;
end;
then reconsider H as Homomorphism-Family of Dom(), Cod() by ThRHom;
take H;
thus thesis by A2;
end;
theorem
for I being non empty set
for A, B being Group-Family of I
for f being ManySortedSet of I
holds f is Homomorphism-Family of A,B
iff (for i being Element of I holds f.i is Homomorphism of A.i, B.i)
proof
let I be non empty set;
let A, B be Group-Family of I;
let f be ManySortedSet of I;
thus f is Homomorphism-Family of A,B
implies (for i being Element of I holds f.i is Homomorphism of A.i, B.i)
proof
assume A1: f is Homomorphism-Family of A,B;
let i be Element of I;
reconsider ff=f as Homomorphism-Family of A,B by A1;
ff.i = f.i & ff.i is Homomorphism of A.i, B.i;
hence thesis;
end;
thus (for i being Element of I holds f.i is Homomorphism of A.i, B.i)
implies f is Homomorphism-Family of A, B
proof
assume A1: for i being Element of I holds f.i is Homomorphism of A.i, B.i;
for i being object st i in I holds f.i is Function of (Carrier A).i,
(Carrier B).i
proof
let i be object;
assume i in I;
then reconsider ii=i as Element of I;
(Carrier A).i = the carrier of A.ii &
(Carrier B).i = the carrier of B.ii by Th9;
hence f.i is Function of (Carrier A).i, (Carrier B).i by A1;
end;
then f is ManySortedFunction of (Carrier A), (Carrier B) by PBOOLE:def 15;
hence thesis by A1, Def11;
end;
end;
begin :: Projection Morphisms from Product Group to Direct Factors
theorem Th29:
for g being Element of product F
holds g.i is Element of F.i
proof
let g be Element of product F;
g is Function & g in product F;
then g.i in F.i by GROUP_19:5;
hence thesis;
end;
definition
let I be non empty set;
let F be Group-Family of I;
let g be Element of product F;
let i be Element of I;
func g/.i -> Element of F.i equals
g.i;
correctness by Th29;
end;
registration
let I be non empty set;
let F be Group-Family of I;
let g be Element of product F;
let i be Element of I;
identify g/.i with g.i;
correctness;
end;
definition
let I be non empty set;
let i be Element of I;
let F be Group-Family of I;
func proj (F, i) -> Homomorphism of (product F), F.i means
:Def13:
for h being Element of product F holds it.h = h.i;
existence
proof
deffunc F1() = product F;
deffunc F2() = F.i;
deffunc F3(Element of F1()) = $1/.i;
consider p being Function of F1(), F2() such that
A1: for x being Element of F1() holds p.x = F3(x)
from FUNCT_2:sch 4;
reconsider p as Function of product F, F.i;
for a, b being Element of product F
holds p.(a * b) = (p.a) * (p.b)
proof
let a, b be Element of product F;
(p.a) * (p.b) = (p.a) * (b/.i) by A1
.= (a/.i) * (b/.i) by A1
.= (a * b)/.i by GROUP_7:1
.= p.(a * b) by A1;
hence p.(a * b) = (p.a) * (p.b);
end;
then reconsider p as Homomorphism of product F,F.i by GROUP_6:def 6;
take p;
for h being Element of product F holds p.h = h.i
proof
let h be Element of product F;
p.h = h/.i by A1;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let p1,p2 be Homomorphism of (product F), F.i;
assume A1: for h being Element of product F holds p1.h = h.i;
assume A2: for h being Element of product F holds p2.h = h.i;
for x being Element of product F holds p1.x = p2.x
proof
let x be Element of product F;
p1.x = x.i by A1;
hence p1.x = p2.x by A2;
end;
hence p1 = p2 by FUNCT_2:def 8;
end;
end;
theorem Th30:
proj (F, i) is onto
proof
for y being object st y in the carrier of F.i
ex x being object st x in the carrier of product F & y = (proj (F,i)).x
proof
let y be object;
assume y in the carrier of F.i;
then reconsider yy=y as Element of F.i;
(1ProdHom (F, i)).yy in ProjGroup (F, i);
then (1ProdHom (F, i)).yy in ProjSet (F, i) by GROUP_12:def 2;
then consider x being Function, g being Element of F.i such that
A1: x = (1ProdHom (F, i)).yy & dom x = I & x.i = g &
for j being Element of I st j <> i holds x.j = 1_(F.j)
by GROUP_12:2;
the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
then dom (1_(product F)) = I by PARTFUN1:def 2;
then A2: y = ((1_(product F)) +* (i, y)).i by FUNCT_7:31
.= g by A1, GROUP_12:def 3;
A3: x in product F by A1,GROUP_2:41;
take x;
thus x in the carrier of product F by A3;
thus y = (proj (F,i)).x by Def13, A1, A2, A3;
end;
then rng (proj (F,i)) = the carrier of F.i by FUNCT_2:10;
hence proj (F, i) is onto by FUNCT_2:def 3;
end;
registration
let I be non empty set;
let F be Group-Family of I;
let i be Element of I;
cluster proj (F, i) -> onto;
correctness by Th30;
end;
theorem Th31:
proj (Carrier F, i) is Function of product (Carrier F), the carrier of F.i
proof
set X = product (Carrier F);
set Y = the carrier of F.i;
set f = proj (Carrier F, i);
A1: dom f = X by CARD_3:def 16;
for x being object st x in X holds f.x in Y
proof
let x be object;
assume A2: x in X;
then reconsider y=x as Element of product F by GROUP_7:def 2;
f.y = y/.i by A1, A2, CARD_3:def 16;
hence f.x in Y;
end;
hence f is Function of X,Y by A1, FUNCT_2:3;
end;
theorem Th32:
for g being Element of product F
holds proj (F, i) . g = proj (Carrier F, i) . g
proof
let g be Element of product F;
set X = product (Carrier F);
set f = proj (Carrier F, i);
A1: dom f = X by CARD_3:def 16;
g in product F;
then g in dom f by A1, GROUP_7:def 2;
then (proj (Carrier F, i)) . g = g.i by CARD_3:def 16;
hence (proj (F, i)) . g = (proj (Carrier F, i)) . g by Def13;
end;
theorem
proj (F, i) = proj (Carrier F, i)
proof
set X = product (Carrier F);
set Y = the carrier of F.i;
product (Carrier F) = the carrier of (product F) by GROUP_7:def 2;
then A1: proj (Carrier F, i) is Function of X,Y
& proj (F, i) is Function of X,Y by Th31;
for x being Element of X
holds (proj (F, i)) . x = (proj (Carrier F, i)) . x
proof
let x be Element of X;
x is Element of product F by GROUP_7:def 2;
hence thesis by Th32;
end;
hence thesis by A1, FUNCT_2:63;
end;
theorem Th34:
for g being Element of product F
for h being Element of F.i
holds g +* (i, h) in product F
proof
let g be Element of product F;
let h be Element of F.i;
g in product F;
hence thesis by GROUP_19:24;
end;
theorem
for i being Element of I
for g being Element of product F
holds (g +* (i, 1_(F.i))) in Ker (proj (F, i))
proof
let i be Element of I;
let g be Element of product F;
A1: dom g = I by GROUP_19:3;
(g +* (i, 1_(F.i))) in product F by Th34;
then reconsider h=(g +* (i, 1_(F.i))) as Element of product F;
(proj (F, i)).h = h.i by Def13
.= 1_(F.i) by A1, FUNCT_7:31;
hence (g +* (i, 1_(F.i))) in Ker (proj (F, i)) by GROUP_6:41;
end;
theorem InclByAnyOtherName:
for G1,G2 being Group
for f being Homomorphism of G1, G2
st (for g being Element of G1 holds f.g = g)
holds G1 is Subgroup of G2
proof
let G1,G2 be Group;
let f be Homomorphism of G1, G2;
assume A1: for g being Element of G1 holds f.g = g;
A2: the carrier of G1 c= the carrier of G2
proof
for g being object st g in the carrier of G1
holds g in the carrier of G2
proof
let g be object;
assume g in the carrier of G1;
then reconsider gg=g as Element of G1;
(f.gg) in the carrier of G2;
hence g in the carrier of G2 by A1;
end;
hence thesis by TARSKI:def 3;
end;
then reconsider U=the carrier of G1 as Subset of the carrier of G2;
set U1 = the carrier of G1;
set U2 = the carrier of G2;
A3: [: U1, U1 :] c= [: U2, U2 :] by A2, ZFMISC_1:96;
dom (the multF of G2) = [: U2, U2 :]
by FUNCT_2:def 1;
then A5: dom ((the multF of G2)|[: U1, U1 :]) = [: U1, U1 :]
by A2, ZFMISC_1:96, RELAT_1:62;
A5a: dom ((the multF of G2)||U1) = [: U1, U1 :] by A5, REALSET1:def 2;
A5b: ((the multF of G2)||U1)
= ((the multF of G2)|[: U1, U1 :]) by REALSET1:def 2;
A6: for a being Element of U1
for b being Element of U1
holds (the multF of G1).(a, b) = ((the multF of G2)||U1).(a, b)
proof
let a be Element of U1;
let b be Element of U1;
B2: (the multF of G2).([a, b])
= ((the multF of G2)|[: U1, U1 :]).([a, b]) by A5, ZFMISC_1:87, FUNCT_1:47
.= ((the multF of G2)||U1).([a, b]) by REALSET1:def 2
.= ((the multF of G2)||U1).(a, b) by BINOP_1:def 1;
set c = a * b;
B4: (the multF of G2).(f.a, f.b)
= (the multF of G2).(f.a, b) by A1
.= (the multF of G2).(a, b) by A1;
c = f.c by A1
.= (f.a) * (f.b) by GROUP_6:def 6
.= (the multF of G2).(a, b) by B4;
hence (the multF of G1).(a, b) = ((the multF of G2)||U1).(a, b)
by B2, BINOP_1:def 1;
end;
((the multF of G2)||U1) is BinOp of U1
proof
B1: rng (the multF of G1) c= U1 by RELAT_1:def 19;
B2a: ((the multF of G2)||U1) is Function of [:U1,U1:], U2
by A3, A5b, FUNCT_2:32;
B2: ((the multF of G2)||U1) is Function of [: U1, U1 :],
rng ((the multF of G2)||U1) by A5a, FUNCT_2:1;
B3: rng ((the multF of G2)||U1) c= U1 by B1, A6, B2a, LmEqRng;
[: U1, U1 :] <> {} implies (rng ((the multF of G2)||U1)) <> {}
proof
assume [: U1, U1 :] <> {};
then consider x being object such that
C2: x in [: U1, U1 :] by XBOOLE_0:def 1;
x in dom ((the multF of G2)||U1) by C2, A5, REALSET1:def 2;
hence (rng ((the multF of G2)||U1)) <> {} by FUNCT_1:3;
end;
hence thesis by B2, B3, FUNCT_2:6;
end;
hence G1 is Subgroup of G2 by A2, A6, BINOP_1:2, GROUP_2:def 5;
end;
theorem Th37:
for i,j being Element of I st i <> j
holds (proj (F,j)) * (1ProdHom (F,i)) = 1:(F.i, F.j)
proof
let i,j be Element of I;
assume A1: i <> j;
set U = the carrier of F.i;
A2: dom 1:(F.i, F.j) = U & dom ((proj (F,j)) * (1ProdHom (F,i))) = U
proof
thus dom 1:(F.i, F.j) = U;
B1: rng (1ProdHom (F,i)) c= the carrier of ProjGroup (F, i)
by RELAT_1:def 19;
the carrier of ProjGroup (F,i) c= the carrier of product F
by GROUP_2:def 5;
then (1ProdHom (F,i)) is (the carrier of product F)-valued
by B1, XBOOLE_1:1, RELAT_1:def 19;
then dom ((proj (F,j)) * (1ProdHom (F,i))) = dom (1ProdHom (F,i))
by FUNCT_2:123;
hence thesis by FUNCT_2:def 1;
end;
for x being Element of U
holds ((proj (F,j)) * (1ProdHom (F,i))).x = (1:(F.i, F.j)).x
proof
let x be Element of U;
B1: dom (1ProdHom (F,i)) = U by FUNCT_2:def 1;
(1ProdHom (F,i)).x in ProjGroup (F, i);
then (1_(product F) +* (i, x)) in ProjGroup (F, i) by GROUP_12:def 3;
then B2: (1_(product F) +* (i, x)) in product F by GROUP_2:40;
((proj (F,j)) * (1ProdHom (F,i))).x
= (proj (F,j)).((1ProdHom (F,i)).x) by B1, FUNCT_1:13
.= (proj (F,j)).(1_(product F) +* (i, x)) by GROUP_12:def 3
.= (1_(product F) +* (i, x)).j by Def13, B2
.= (1_(product F)).j by A1,FUNCT_7:32
.= (1:(F.i, F.j)).x by GROUP_7:6;
hence ((proj (F,j)) * (1ProdHom (F,i))).x = (1:(F.i, F.j)).x;
end;
hence (proj (F,j)) * (1ProdHom (F,i)) = 1:(F.i, F.j) by A2;
end;
theorem Th38:
(proj (F,i)) * (1ProdHom (F, i)) = id (the carrier of F.i)
proof
set U = the carrier of F.i;
A1: (1ProdHom (F, i)) is Homomorphism of F.i, product F by GROUP_19:6;
for x being Element of U
holds ((proj (F,i)) * (1ProdHom (F, i))).x = x
proof
let x be Element of U;
B1: dom (1_(product F)) = I by GROUP_19:3;
B2: (1ProdHom (F, i)).x = (1_(product F)) +* (i, x) by GROUP_12:def 3;
(1ProdHom (F, i)).x in (ProjGroup (F,i));
then (1ProdHom (F, i)).x in product F by GROUP_2:40;
then B3: (proj (F, i)).((1_(product F)) +* (i, x))
= ((1_(product F)) +* (i, x)).i by B2, Def13;
dom (1ProdHom (F, i)) = U by FUNCT_2:def 1;
then ((proj (F,i)) * (1ProdHom (F, i))).x
= (proj (F, i)).((1ProdHom (F, i)).x) by FUNCT_1:13
.= (proj (F, i)).((1_(product F)) +* (i, x)) by GROUP_12:def 3
.= x by B1, B3, FUNCT_7:31;
hence thesis;
end;
hence thesis by A1, FUNCT_2:124;
end;
begin :: Universal Property of Direct Products of Groups
:: Universal property of group product, explicit version.
theorem Th39:
for f being Homomorphism-Family of G, F
ex phi being Homomorphism of G, product F
st for g being Element of G
holds (for j being Element of I holds (f.j).g = (proj (F,j)) . (phi.g))
proof
let f be Homomorphism-Family of G, F;
defpred P[object, object] means ex g0 being Element of product F
st $2 = g0 & (for j being Element of I holds (f.j).$1 = g0.j);
deffunc F1() = the carrier of G;
A1: for x being object st x in F1()
ex y being object st y in the carrier of product F &
P[x,y]
proof
let x be object;
assume x in F1();
then reconsider xx=x as Element of G;
defpred P1[object, object] means ex i being Element of I st
i = $1 & $2 = ((f.i).xx);
B1: for i, y1, y2 being object st i in I & P1[i,y1] & P1[i,y2]
holds y1 = y2;
B2: for i being object st i in I holds ex y being object st P1[i,y]
proof
let i be object;
assume i in I;
then reconsider ii=i as Element of I;
consider y being object such that
C1: y = ((f.ii).xx);
take y;
thus P1[i,y] by C1;
end;
consider y being Function such that
B3: dom y = I and
B4: for j being object st j in I holds P1[j, y.j]
from FUNCT_1:sch 2(B1, B2);
take y;
thus y in the carrier of product F
proof
C1: dom y = dom (Carrier F) by B3, PARTFUN1:def 2;
for i being Element of I holds y.i in (Carrier F).i
proof
let i be Element of I;
P1[i, y.i] by B4;
then consider ii being Element of I such that
D1: ii=i & y.i = ((f.i).xx);
(Carrier F).i = the carrier of F.i by Th9;
hence thesis by D1;
end;
then for i being object st i in dom (Carrier F)
holds y.i in (Carrier F).i;
then y in product (Carrier F) by C1, CARD_3:9;
hence thesis by GROUP_7:def 2;
end;
then consider g0 being Element of product F such that
B5: g0 = y;
take g0;
thus y = g0 by B5;
let j be Element of I;
P1[j, g0.j] by B4, B5;
hence (f.j).x = g0.j;
end;
consider phi being Function of F1(), the carrier of (product F)
such that
A2: for x being object st x in F1() holds P[x, phi.x]
from FUNCT_2:sch 1(A1);
reconsider phi as Function of G, product F;
A3: for g being Element of G
for j being Element of I
holds (phi.g).j = (f.j).g
proof
let g be Element of G;
let j be Element of I;
P[g, phi.g] by A2;
hence (phi.g).j = (f.j).g;
end;
for a, b being Element of G holds phi.(a * b) = (phi.a) * (phi.b)
proof
let a, b be Element of G;
(phi.(a * b)) is Element of product (Carrier F)
& (phi.a)*(phi.b) is Element of product (Carrier F)
by GROUP_7:def 2;
then B1: dom (phi.(a * b)) = I & dom ((phi.a)*(phi.b)) = I
by PARTFUN1:def 2;
for j being Element of I holds (phi.(a * b)).j = ((phi.a) * (phi.b)).j
proof
let j be Element of I;
reconsider fj = f.j as Homomorphism of G, F.j;
(phi.(a * b)).j = fj.(a * b) by A3
.= (fj.a) * (fj.b) by GROUP_6:def 6
.= ((phi.a)/.j) * (fj.b) by A3
.= ((phi.a)/.j) * ((phi.b)/.j) by A3
.= ((phi.a) * (phi.b))/.j by GROUP_7:1;
hence (phi.(a * b)).j = ((phi.a) * (phi.b)).j;
end;
hence phi.(a * b) = (phi.a) * (phi.b) by B1;
end;
then reconsider phi as Homomorphism of G, product F by GROUP_6:def 6;
take phi;
let g be Element of G;
for j being Element of I holds (f.j).g = (proj (F, j)) . (phi.g)
proof
let j be Element of I;
(f.j).g = (phi.g).j by A3;
hence (f.j).g = (proj (F, j)).(phi.g) by Def13;
end;
hence thesis;
end;
:: Universal property of group product, as most people would recognize it.
theorem
for f being Homomorphism-Family of G, F
ex phi being Homomorphism of G, product F
st (for i being Element of I holds f.i = (proj (F,i)) * phi)
proof
let f be Homomorphism-Family of G, F;
consider phi being Homomorphism of G, product F such that
A1: for g being Element of G
holds (for j being Element of I holds (f.j).g = (proj (F,j)) . (phi.g))
by Th39;
take phi;
let i be Element of I;
for g being Element of G holds ((proj (F,i)) * phi).g = (f.i).g
proof
let g be Element of G;
(f.i).g = (proj (F,i)) . (phi.g) by A1
.= ((proj (F,i)) * phi).g by FUNCT_2:15;
hence (f.i).g = ((proj (F,i)) * phi).g;
end;
hence f.i = (proj (F,i)) * phi by FUNCT_2:def 8;
end;
theorem
for f being Homomorphism-Family of G, F
for phi1, phi2 being Homomorphism of G, product F
st (for i being Element of I holds f.i = (proj (F,i)) * phi1)
& (for i being Element of I holds f.i = (proj (F,i)) * phi2)
holds phi1 = phi2
proof
let f be Homomorphism-Family of G, F;
let phi1, phi2 be Homomorphism of G, product F;
assume A1: for i being Element of I holds f.i = (proj (F,i)) * phi1;
assume A2: for i being Element of I holds f.i = (proj (F,i)) * phi2;
for g being Element of G holds phi1.g = phi2.g
proof
let g be Element of G;
phi1.g is Element of product (Carrier F)
& phi2.g is Element of product (Carrier F) by GROUP_7:def 2;
then B1: dom (phi1.g) = I & dom (phi2.g) = I by PARTFUN1:def 2;
for j being Element of I holds (phi1.g).j = (phi2.g).j
proof
let j be Element of I;
C2: (f.j).g = ((proj (F, j)) * phi1).g by A1
.= (proj (F, j)) . (phi1.g) by FUNCT_2:15
.= (phi1.g).j by Def13;
(f.j).g = ((proj (F, j)) * phi2).g by A2
.= (proj (F, j)) . (phi2.g) by FUNCT_2:15
.= (phi2.g).j by Def13;
hence (phi1.g).j = (phi2.g).j by C2;
end;
hence phi1.g = phi2.g by B1;
end;
hence phi1 = phi2 by FUNCT_2:def 8;
end;
definition
let G be Group;
let I be non empty set;
let F be Group-Family of I;
let f be Homomorphism-Family of G, F;
func product f -> Homomorphism of G, product F means
:Def14:
for g being Element of G
for i being Element of I
holds (f.i).g = (it.g).i;
existence
proof
consider phi being Homomorphism of G, product F such that
A1: for g being Element of G
holds (for j being Element of I holds (f.j).g = (proj (F,j)) . (phi.g))
by Th39;
take phi;
for g being Element of G
for j being Element of I holds (f.j).g = (phi.g).j
proof
let g be Element of G;
let j be Element of I;
(f.j).g = (proj (F,j)) . (phi.g) by A1
.= (phi.g).j by Def13;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
for phi1, phi2 being Homomorphism of G,product F
st (for g being Element of G
for i being Element of I
holds (f.i).g = (phi1.g).i)
& (for g being Element of G
for i being Element of I
holds (f.i).g = (phi2.g).i)
holds phi1 = phi2
proof
let phi1,phi2 be Homomorphism of G,product F;
assume A1: for g being Element of G
for i being Element of I
holds (f.i).g = (phi1.g).i;
assume A2: for g being Element of G for i being Element of I
holds (f.i).g = (phi2.g).i;
for g being Element of G
holds phi1.g = phi2.g
proof
let g be Element of G;
phi1.g is Element of product (Carrier F)
& phi2.g is Element of product (Carrier F) by GROUP_7:def 2;
then A3: dom (phi1.g) = I & dom (phi2.g) = I by PARTFUN1:def 2;
for j being Element of I holds (phi1.g).j = (phi2.g).j
proof
let j be Element of I;
(phi1.g).j = (f.j).g by A1
.= (phi2.g).j by A2;
hence (phi1.g).j = (phi2.g).j;
end;
hence phi1.g = phi2.g by A3;
end;
hence phi1 = phi2 by FUNCT_2:def 8;
end;
hence thesis;
end;
end;
theorem Th42:
for g being Element of G
holds (for i being Element of I holds ((product f).g).i = 1_(F.i))
iff (product f).g = 1_(product F)
proof
let g be Element of G;
thus (for i being Element of I holds ((product f).g).i = 1_(F.i))
implies (product f).g = 1_(product F)
proof
assume A1: for i being Element of I holds ((product f).g).i = 1_(F.i);
set s = (product f).g;
A2: for i being set st i in I
holds (ex FG being non empty Group-like multMagma
st FG = F.i & s.i = (1_FG))
proof
let i be set;
assume i in I;
then reconsider ii=i as Element of I;
take FG = F.ii;
thus thesis by A1;
end;
s is ManySortedSet of I
proof
s is Element of product (Carrier F) by GROUP_7:def 2;
hence s is ManySortedSet of I;
end;
hence thesis by A2, GROUP_7:5;
end;
thus (product f).g = 1_(product F) implies
(for i being Element of I holds ((product f).g).i = 1_(F.i)) by GROUP_7:6;
end;
theorem Th43:
for g being Element of G
holds g in Ker (product f)
iff (for i being Element of I holds g in Ker (f.i))
proof
let g be Element of G;
thus g in Ker (product f)
implies (for i being Element of I holds g in Ker (f.i))
proof
assume A1: g in Ker (product f);
let i be Element of I;
(product f).g = 1_(product F) by A1, GROUP_6:41;
then 1_(F.i) = ((product f).g).i by Th42
.= (f.i).g by Def14;
hence g in Ker (f.i) by GROUP_6:41;
end;
thus (for i being Element of I holds g in Ker (f.i))
implies g in Ker (product f)
proof
assume A1: for i being Element of I holds g in Ker (f.i);
A2: for i being Element of I holds (f.i).g = 1_(F.i)
proof
let i be Element of I;
g in Ker (f.i) by A1;
hence (f.i).g = 1_(F.i) by GROUP_6:41;
end;
for i being Element of I holds ((product f).g).i = 1_(F.i)
proof
let i be Element of I;
((product f).g).i = (f.i).g by Def14
.= 1_(F.i) by A2;
hence thesis;
end;
then (product f).g = 1_(product F) by Th42;
hence g in Ker (product f) by GROUP_6:41;
end;
end;
theorem Th44:
for G1, G2, G3 being Group
for f1 being Homomorphism of G1, G2
for f2 being Homomorphism of G2, G3
for g being Element of G1
holds g in Ker (f2 * f1) iff f1.g in Ker(f2)
proof
let G1, G2, G3 be Group;
let f1 be Homomorphism of G1, G2;
let f2 be Homomorphism of G2, G3;
let g be Element of G1;
thus g in Ker (f2 * f1) implies f1.g in Ker(f2)
proof
assume g in Ker (f2 * f1);
then 1_(G3) = (f2 * f1).g by GROUP_6:41
.= f2.(f1.g) by FUNCT_2:15;
hence f1.g in Ker(f2) by GROUP_6:41;
end;
thus f1.g in Ker(f2) implies g in Ker (f2 * f1)
proof
assume f1.g in Ker(f2);
then 1_G3 = f2.(f1.g) by GROUP_6:41
.= (f2 * f1).g by FUNCT_2:15;
hence g in Ker (f2 * f1) by GROUP_6:41;
end;
end;
theorem
for G1, G2, G3 being Group
for f1 being Homomorphism of G1, G2
for f2 being Homomorphism of G2, G3
holds the carrier of Ker (f2 * f1) = f1" (the carrier of Ker f2)
proof
let G1, G2, G3 be Group;
let f1 be Homomorphism of G1, G2;
let f2 be Homomorphism of G2, G3;
A1: f1 "(the carrier of Ker f2) is Subset of G1
& the carrier of Ker (f2 * f1) is Subset of G1
by GROUP_2:def 5, FUNCT_2:39;
for g being Element of G1
st g in the carrier of Ker (f2 * f1)
holds g in f1 " (the carrier of (Ker f2))
proof
let g be Element of G1;
assume g in the carrier of Ker (f2 * f1);
then g in Ker (f2 * f1);
then f1.g in Ker f2 by Th44;
hence g in f1 " (the carrier of (Ker f2)) by FUNCT_2:38;
end; then
A2: the carrier of Ker (f2 * f1) c= f1" (the carrier of Ker f2)
by A1, SUBSET_1:2;
for g being Element of G1
st g in f1 " (the carrier of (Ker f2))
holds g in the carrier of Ker (f2 * f1)
proof
let g be Element of G1;
assume g in f1 " (the carrier of (Ker f2));
then f1.g in Ker f2 by FUNCT_2:38;
then g in Ker (f2 * f1) by Th44;
hence g in the carrier of Ker (f2 * f1);
end; then
A3: f1" (the carrier of Ker f2) c= the carrier of Ker (f2 * f1)
by A1, SUBSET_1:2;
thus the carrier of Ker (f2 * f1) = f1" (the carrier of Ker f2)
by A2, A3, XBOOLE_0:def 10;
end;
theorem
the carrier of Ker (product f) =
meet the set of all the carrier of Ker (f.i) where
i is Element of I
proof
set Fam = the set of all the carrier of Ker (f.i) where i is Element of I;
A1: Fam <> {}
proof
set i = the Element of I;
the carrier of Ker (f.i) in Fam;
hence thesis;
end;
A3: for g being object
holds g in Ker (product f)
iff (for A being set st A in Fam holds g in A)
proof
let g be object;
hereby
assume B1: g in Ker (product f);
let A be set;
assume A in Fam;
then consider i1 being Element of I such that
B2: A = the carrier of Ker(f.i1);
g in G & g in Ker (product f) by B1, GROUP_2:40;
then g in Ker (f.i1) by Th43;
hence g in A by B2;
end;
assume B1: for A being set st A in Fam holds g in A;
g in G & for i being Element of I holds g in Ker (f.i)
proof
ex x being object st x in Fam by A1, XBOOLE_0:def 1;
then consider A0 being set such that
B2: A0 in Fam;
consider i0 being Element of I such that
B3: A0 = the carrier of Ker (f.i0) by B2;
g in Ker (f.i0) by B1, B2, B3;
hence g in G by GROUP_2:40;
let i be Element of I;
the carrier of Ker (f.i) in Fam;
hence g in Ker (f.i) by B1;
end;
hence g in Ker (product f) by Th43;
end;
A4: for g being object holds g in Ker (product f) iff g in (meet Fam)
proof
let g be object;
g in Ker (product f) iff (for A being set st A in Fam holds g in A) by A3;
hence thesis by A1, SETFAM_1:def 1;
end;
for g being object
holds g in the carrier of Ker (product f) iff g in meet Fam
proof
let g be object;
g in the carrier of Ker (product f) iff g in Ker (product f);
hence thesis by A4;
end;
hence thesis by TARSKI:2;
end;
theorem Th47:
for f being Function,
I being non empty set,
F being Group-Family of I
st dom f = I & (for i being Element of I holds f.i in F.i)
holds f in product F
proof
let f be Function;
let I be non empty set;
let F be Group-Family of I;
assume A1: dom f = I;
assume A2: for i being Element of I holds f.i in F.i;
A3: dom (Carrier F) = I by PARTFUN1:def 2;
for i being object st i in dom (Carrier F) holds f.i in (Carrier F).i
proof
let i be object;
assume i in dom (Carrier F);
then reconsider ii=i as Element of I;
f.i in F.ii by A2;
hence f.i in (Carrier F).i by Th9;
end;
then f in product (Carrier F) by A1, A3, CARD_3:9;
hence f in product F by GROUP_7:def 2;
end;
theorem
for S being Group-Family of I
for g being Element of product F
holds g in product S iff (for i being Element of I
holds (proj (F,i)).g in S.i)
proof
let S be Group-Family of I;
let g be Element of product F;
hereby
assume A1: g in product S;
let i be Element of I;
g.i in S.i by A1, GROUP_19:5;
hence (proj (F,i)).g in S.i by Def13;
end;
assume Z2: for i being Element of I holds (proj (F,i)).g in S.i;
Z3: dom g = I by GROUP_19:3;
for i being Element of I holds g.i in S.i
proof
let i be Element of I;
(proj (F, i)).g in S.i by Z2;
hence g.i in S.i by Def13;
end;
hence g in product S by Z3, Th47;
end;
theorem Th49:
for F1,F2 being Group-Family of I
st (for i being Element of I holds F1.i is Subgroup of F2.i)
holds product F1 is Subgroup of product F2
proof
let F1,F2 be Group-Family of I;
assume A1: for i being Element of I holds F1.i is Subgroup of F2.i;
deffunc Fun(Element of I) = (incl (F1.$1, F2.$1)) * (proj (F1, $1));
A2: for i being Element of I
holds Fun(i) is Homomorphism of product F1, F2.i;
consider f being Homomorphism-Family of product F1, F2 such that
A3: for i being Element of I holds f.i = Fun(i)
from RHomFamSch(A2);
A4: for g being Element of product F1
for i being Element of I
holds (f.i).g = g.i
proof
let g be Element of product F1;
let i be Element of I;
B1: F1.i is Subgroup of F2.i by A1;
((proj (F1, i)).g) in F1.i;
then (g.i) is Element of F1.i by Def13;
then B2: (incl (F1.i, F2.i)).(g.i) = g.i by B1, Th18;
(f.i).g = ((incl (F1.i, F2.i)) * (proj (F1, i))).g by A3
.= (incl (F1.i, F2.i)).((proj (F1, i)).g) by FUNCT_2:15
.= (g.i) by B2, Def13;
hence (f.i).g = g.i;
end;
consider phi being Homomorphism of product F1, product F2 such that
A5: for g being Element of product F1
holds (for i being Element of I holds (f.i).g = (proj (F2,i)) . (phi.g))
by Th39;
for g being Element of product F1
holds phi.g = g
proof
let g be Element of product F1;
B1: for i being object st i in I holds (phi.g).i = g.i
proof
let i be object;
assume i in I;
then reconsider j=i as Element of I;
g.j = (f.j).g by A4
.= (proj (F2,j)) . (phi.g) by A5
.= (phi.g).j by Def13;
hence thesis;
end;
dom g = I by GROUP_19:3;
hence g = phi.g by B1, GROUP_19:3;
end;
hence product F1 is Subgroup of product F2 by InclByAnyOtherName;
end;
definition
let I be non empty set;
let F be Group-Family of I;
let S be Subgroup-Family of F;
func product S -> strict Subgroup of product F equals
product S;
coherence
proof
for i being Element of I holds S.i is Subgroup of F.i;
hence product S is strict Subgroup of product F by Th49;
end;
end;
theorem Th50:
Image (proj (F, i)) = the multMagma of F.i
proof
for g being object st g in the carrier of F.i
holds g in the carrier of Image (proj (F, i))
proof
let g be object;
assume g in the carrier of F.i;
then reconsider x=g as Element of F.i;
ex h being Element of product F st x = (proj (F, i)).h
proof
dom (1_(product F)) = I by GROUP_19:3;
then B1: ((1_(product F)) +* (i,x)).i = x by FUNCT_7:31;
(1_(product F)) +* (i,x) in ProjSet (F, i) by GROUP_12:def 1;
then reconsider h = ((1_(product F)) +* (i,x)) as Element of product F;
take h;
(proj (F, i)).((1_(product F)) +* (i,x))
= (proj (F, i)).h
.= x by B1, Def13;
hence thesis;
end;
then x in Image (proj (F, i)) by GROUP_6:45;
hence g in the carrier of Image (proj (F, i));
end;
hence thesis by GROUP_2:61, TARSKI:def 3;
end;
theorem
for F1,F2 being componentwise_strict Subgroup-Family of F
st (for i being Element of I
holds Image (proj (F1, i)) is Subgroup of Image (proj (F2, i)))
holds (product F1) is strict Subgroup of (product F2)
proof
let F1,F2 be componentwise_strict Subgroup-Family of F;
assume A1: for i being Element of I
holds Image (proj (F1, i)) is Subgroup of Image (proj (F2, i));
for i being Element of I holds F1.i is Subgroup of F2.i
proof
let i be Element of I;
Image (proj (F1, i)) is Subgroup of Image (proj (F2, i)) by A1;
hence F1.i is Subgroup of F2.i by Th50;
end;
hence thesis by Th49;
end;
theorem
for G being strict Subgroup of product F
for S st (for i being Element of I
holds S.i = Image ((proj (F,i)) * (incl G)))
for f being Homomorphism-Family of G, S
st (for i being Element of I holds f.i = ((proj (F,i)) * (incl G)))
holds product f = id the carrier of G
proof
let G be strict Subgroup of product F;
let S;
assume for i being Element of I
holds S.i = Image ((proj (F,i)) * (incl G));
let f be Homomorphism-Family of G, S;
assume A2: for i being Element of I holds f.i = ((proj (F,i)) * (incl G));
A3: for g being Element of G
for i being Element of I
holds ((proj (F,i)) * (incl G)).g = ((proj (F, i)) * (product f)).g
proof
let g be Element of G;
let i be Element of I;
((product f).g) in (product S);
then B2: ((product f).g) in (product F) by GROUP_2:40;
B3: ((product f).g).i = (proj (F, i)).((product f).g) by B2, Def13
.= ((proj (F, i)) * (product f)).g by FUNCT_2:15;
((proj (F,i)) * (incl G)).g = (f.i).g by A2
.= ((product f).g).i by Def14;
hence ((proj (F,i)) * (incl G)).g = ((proj (F, i)) * (product f)).g by B3;
end;
A4: for g being Element of product F st g in G
holds (product f).g = g
proof
let g be Element of product F;
assume B1: g in G;
((product f).g) in (product F)
proof
((product f).g) in (product S) by B1, FUNCT_2:5;
hence ((product f).g) in (product F) by GROUP_2:40;
end;
then reconsider foo=(product f).g as Element of product F;
B2: for i being Element of I
holds ((proj (F, i)) * (incl G)).g = g.i
proof
let i be Element of I;
((proj (F,i)) * (incl G)).g
= (proj (F, i)). ((incl G).g) by B1, FUNCT_2:15
.= (proj (F, i)).((id the carrier of G).g) by Def9
.= (proj (F, i)).g by B1, FUNCT_1:18
.= g.i by Def13;
hence thesis;
end;
B3: dom g = I & dom foo = I by GROUP_19:3;
for i being Element of I holds foo.i = g.i
proof
let i be Element of I;
(proj (F, i)).foo = ((proj (F,i)) * (product f)).g by B1, FUNCT_2:15
.= ((proj (F, i)) * (incl G)).g by B1, A3
.= g.i by B2;
hence thesis by Def13;
end;
then foo = g by B3;
hence (product f).g = g;
end;
A6: dom (product f) = the carrier of G by FUNCT_2:def 1;
for x being object st x in the carrier of G holds (product f).x = x
proof
let x be object;
assume x in the carrier of G;
then B1: x in G;
then x in product F by GROUP_2:40;
hence (product f).x = x by B1, A4;
end;
hence product f = id the carrier of G by A6, FUNCT_1:17;
end;
theorem ThMorphismOfCommutators:
for G1,G2 being Group
for phi being Homomorphism of G1, G2
for x being Element of G1 st x in commutators G1
holds phi.x in commutators G2
proof
let G1,G2 be Group;
let phi be Homomorphism of G1, G2;
let x be Element of G1;
assume x in commutators G1;
then consider a,b being Element of G1 such that
A2: x = [. a, b .] by GROUP_5:58;
phi.x = [. (phi.a), (phi.b) .] by A2, GROUP_6:34;
hence phi.x in commutators G2 by GROUP_5:58;
end;
theorem :: missing
for G1,G2,G3 being Group
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3
for g being Element of G1
holds (f2 * f1).g = f2.(f1.g)
proof
let G1,G2,G3 be Group;
let f1 be Homomorphism of G1,G2;
let f2 be Homomorphism of G2,G3;
let g be Element of G1;
dom f1 = the carrier of G1 by FUNCT_2:def 1;
hence (f2 * f1).g = f2.(f1.g) by FUNCT_1:13;
end;
theorem
for G1,G2 being Group
for H being Subgroup of G2
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G1,H
st f1 = f2
holds Image f1 = Image f2
proof
let G1,G2 be Group;
let H be Subgroup of G2;
let f1 be Homomorphism of G1,G2;
let f2 be Homomorphism of G1,H;
assume A1: f1 = f2;
A2: Image f2 is strict Subgroup of G2 by GROUP_2:56;
for g being Element of G2 holds g in Image f1 iff g in Image f2
proof
let g be Element of G2;
hereby
assume g in Image f1;
then ex a being Element of G1 st g = f1.a by GROUP_6:45;
hence g in Image f2 by A1, GROUP_6:45;
end;
assume g in Image f2;
then ex a being Element of G1 st g = f2.a by GROUP_6:45;
hence g in Image f1 by A1, GROUP_6:45;
end;
hence Image f1 = Image f2 by A2, GROUP_2:def 6;
end;
theorem Th57:
for a,b being Element of product F
for i
holds ([. a, b .]).i = [. a/.i, b/.i .]
proof
let a,b be Element of product F;
let i;
thus [. a/.i, b/.i .] = (((a/.i)")*((b/.i)"))*((a/.i)*(b/.i)) by GROUP_5:16
.= (((a")/.i) * ((b/.i)")) * ((a/.i) * (b/.i)) by GROUP_7:8
.= (((a")/.i) * ((b")/.i)) * ((a/.i) * (b/.i)) by GROUP_7:8
.= (((a")/.i) * ((b")/.i)) * ((a * b)/.i) by GROUP_7:1
.= (((a") * (b"))/.i) * ((a * b)/.i) by GROUP_7:1
.= (((a") * (b")) * (a * b))/.i by GROUP_7:1
.= ([. a, b .]).i by GROUP_5:16;
end;
scheme SubFamEx { I1() -> non empty set,
Fam() -> Group-Family of I1(),
P[object, object] } :
ex S being Subgroup-Family of Fam()
st for i being Element of I1() holds P[i, S.i]
provided
A1: for i being Element of I1() ex j being Subgroup of Fam().i st P[i, j]
proof
defpred P1[Element of I1(), object] means ex j being Subgroup of Fam().$1
st $2=j & P[$1, j];
A2: for i being Element of I1() ex j being object st P1[i, j]
proof
let i be Element of I1();
consider j being Subgroup of Fam().i such that
B1: P[i, j] by A1;
take j;
thus P1[i, j] by B1;
end;
consider S being ManySortedSet of I1() such that
A3: for i being Element of I1() holds P1[i, S.i]
from PBOOLE:sch 6(A2);
for y being object st y in rng S holds y is Group
proof
let y be object;
assume y in rng S;
then consider x being object such that
B2: x in dom S & y = S.x by FUNCT_1:def 3;
reconsider i=x as Element of I1() by B2;
P1[i, y] by A3, B2;
hence y is Group;
end;
then S is Group-yielding;
then reconsider S as Group-Family of I1();
for i being Element of I1() holds S.i is Subgroup of Fam().i
proof
let i be Element of I1();
P1[i, S.i] by A3;
hence S.i is Subgroup of Fam().i;
end;
then S is Fam()-Subgroup-yielding;
then reconsider S as Subgroup-Family of Fam();
take S;
thus for i being Element of I1() holds P[i, S.i]
proof
let i be Element of I1();
P1[i, S.i] by A3;
hence P[i, S.i];
end;
end;
theorem :: missing
for A being ManySortedSet of I
st (for i being Element of I holds A.i is Subset of F.i)
holds product A is Subset of product F
proof
let A be ManySortedSet of I;
assume A1: for i being Element of I holds A.i is Subset of F.i;
for x being object st x in product A holds x in the carrier of product F
proof
let x be object;
assume B1: x in product A;
reconsider x as Function by B1;
B2: dom x = dom A by B1, CARD_3:9;
B3: dom F = I & dom A = I by PARTFUN1:def 2;
for i being Element of I holds x.i in F.i
proof
let i be Element of I;
C1: A.i is Subset of F.i by A1;
x.i in A.i by B1, B3, CARD_3:9;
hence x.i in F.i by C1;
end;
then x in product F by B2, Th47, PARTFUN1:def 2;
hence thesis;
end;
hence product A is Subset of product F by TARSKI:def 3;
end;
theorem Th59:
for S being normal Subgroup-Family of F
holds product S is normal Subgroup of product F
proof
let S be normal Subgroup-Family of F;
for g being Element of product F
holds (product S) |^ g is Subgroup of product S
proof
let g be Element of product F;
for h being Element of product F st h in (product S) |^ g
holds h in product S
proof
let h be Element of product F;
assume h in (product S) |^ g;
then consider a being Element of product F such that
A2: h = a |^ g & a in product S by GROUP_3:58;
A3: dom h = I by GROUP_19:3;
for i being Element of I holds h.i in S.i
proof
let i be Element of I;
h.i = (((g") * a) * g).i by A2,GROUP_3:def 2
.= (((g") * a)/.i) * (g/.i) by GROUP_7:1
.= (((g")/.i) * (a/.i)) * (g/.i) by GROUP_7:1
.= (((g/.i)") * (a/.i)) * (g/.i) by GROUP_7:8
.= (a/.i) |^ (g/.i) by GROUP_3:def 2;
then h.i in (S.i) |^ (g/.i) by A2, GROUP_19:5, GROUP_3:58;
then h.i in the multMagma of S.i by GROUP_3:def 13;
hence thesis;
end;
hence h in product S by A3, Th47;
end;
hence (product S) |^ g is Subgroup of product S by GROUP_2:58;
end;
hence thesis by GROUP_3:122;
end;
registration
let I be non empty set;
let F be Group-Family of I;
let S be normal Subgroup-Family of F;
cluster product S -> normal for Subgroup of product F;
correctness by Th59;
end;
begin :: Commutator Subgroup and Center of Product Groups
:: Kurosh, Theory of Groups, volume I, result VI about Direct Products
theorem
for Z being Group-Family of I
st (for i being Element of I holds Z.i = center (F.i))
holds center (product F) = product Z
proof
let Z be Group-Family of I;
assume A1: for i being Element of I holds Z.i = center (F.i);
A2: for a being Element of product F
holds a in product Z iff (for b being Element of product F holds a*b = b*a)
proof
let a be Element of product F;
thus a in product Z implies (for b being Element of product F
holds a*b = b*a)
proof
assume B1: a in product Z;
let b be Element of product F;
reconsider ab=a*b, ba=b * a as Element of product F;
ab in product F & ba in product F;
then ab in product (Carrier F) & ba in product (Carrier F)
by GROUP_7:def 2;
then B3: dom ab = I & dom ba = I by PARTFUN1:def 2;
for i being Element of I holds (a * b).i = (b * a).i
proof
let i be Element of I;
a.i in Z.i by B1, GROUP_19:5;
then C1: a.i in center (F.i) by A1;
(a * b).i = (a/.i) * (b/.i) by GROUP_7:1
.= (b/.i) * (a/.i) by C1, GROUP_5:77
.= (b * a).i by GROUP_7:1;
hence thesis;
end;
hence a*b = b*a by B3;
end;
thus (for b being Element of product F holds a*b = b*a)
implies a in product Z
proof
assume B1: for b being Element of product F holds a*b = b*a;
B2: for i being Element of I holds a.i in Z.i
proof
let i be Element of I;
C1: for b being Element of product F
holds (a/.i)*(b/.i) = (b/.i) * (a /.i)
proof
let b be Element of product F;
(a * b).i = (a /. i) * (b /. i)
& (b * a).i = (b /. i) * (a /. i) by GROUP_7:1;
hence thesis by B1;
end;
for bi being Element of F.i holds (a/.i)*bi = bi*(a/.i)
proof
let bi be Element of F.i;
reconsider b = (1ProdHom (F, i)).bi as Element of product F
by GROUP_2:42;
D1: dom (1_(product F)) = I by GROUP_19:3;
b = (1_(product F)) +* (i, bi) by GROUP_12:def 3;
then b/.i = bi by D1, FUNCT_7:31;
hence thesis by C1;
end;
then a.i in center (F.i) by GROUP_5:77;
hence a.i in Z.i by A1;
end;
a in product F;
then a in product (Carrier F) by GROUP_7:def 2;
then dom a = I by PARTFUN1:def 2;
hence a in product Z by B2, Th47;
end;
end;
A3: for a being Element of product F
holds a in product Z iff a in center (product F)
proof
let a be Element of product F;
hereby
assume a in product Z;
then for b being Element of product F holds a*b = b*a by A2;
hence a in center (product F) by GROUP_5:77;
end;
assume a in center (product F);
then for b being Element of product F holds a*b = b*a by GROUP_5:77;
hence a in product Z by A2;
end;
for i being Element of I holds Z.i is Subgroup of F.i
proof
let i be Element of I;
Z.i = center (F.i) by A1;
hence Z.i is Subgroup of F.i;
end;
then product Z is Subgroup of product F by GROUP_21:23;
hence thesis by A3, GROUP_2:60;
end;
theorem Th61:
for D being Subgroup-Family of F
st (for i being Element of I holds D.i = (F.i)`)
holds (product F)` is strict Subgroup of product D
proof
let D be Subgroup-Family of F;
assume A1: for i being Element of I holds D.i = (F.i)`;
for a,b being Element of product F holds [. a, b .] in product D
proof
let a,b be Element of product F;
B1: dom ([. a, b .]) = I by GROUP_19:3;
for i being Element of I holds ([. a, b .]).i in D.i
proof
let i be Element of I;
a/.i in (Omega).(F.i) & b/.i in (Omega).(F.i);
then [. a/.i, b/.i .] in [. (Omega).(F.i),(Omega).(F.i) .] by GROUP_5:65;
then [. a/.i, b/.i .] in (F.i)` by GROUP_5:def 9;
then ([. a, b .]).i in (F.i)` by Th57;
hence ([. a, b .]).i in D.i by A1;
end;
hence [. a, b .] in product D by B1,Th47;
end;
hence (product F)` is strict Subgroup of product D by GROUP_6:7;
end;
LmHeartOf62:
for D being Subgroup-Family of F
st (for i being Element of I holds D.i = (F.i)`)
for g being Element of product F st g in sum D
for J being finite Subset of I
for b being ManySortedSet of J st
(for j being object st j in J holds g.j = b.j)
for x,B being set st (x in J & B c= J & not (x in B)
& (ex FS0 being FinSequence of the carrier of product F st
ex ks being FinSequence of INT
st (len FS0 = len ks & rng FS0 c= commutators (product F)
& ((1_(product F)) +* (b|B)) = Product (FS0 |^ ks))))
ex FS being FinSequence of the carrier of product F st
ex ks being FinSequence of INT
st (len FS = len ks & rng FS c= commutators (product F)
& ((1_(product F)) +* (b|(B \/ {x}))) = Product (FS |^ ks))
proof
let D be Subgroup-Family of F;
assume A1: for i being Element of I holds D.i = (F.i)`;
let g be Element of product F;
assume A2: g in sum D;
let J be finite Subset of I;
let b be ManySortedSet of J;
assume A5: for j being object st j in J holds g.j = b.j;
let x,B be set;
assume A6: x in J;
assume A7: B c= J;
assume A8: not x in B;
deffunc F1() = support (g, D);
defpred P[set]
means ex FS being FinSequence of the carrier of product F st
ex ks being FinSequence of INT
st (len FS = len ks & rng FS c= commutators (product F)
& ((1_(product F)) +* (b|$1)) = Product (FS |^ ks));
given FSB being FinSequence of the carrier of product F,
ksB being FinSequence of INT such that
A9: (len FSB = len ksB & rng FSB c= commutators (product F)
& ((1_(product F)) +* (b|B)) = Product (FSB |^ ksB));
reconsider ii=x as Element of I by A6;
g in product D by A2, GROUP_2:40;
then g.x = g.ii & g.ii in D.ii & D.ii = (F.ii)` by A1, GROUP_19:5;
then consider FSg being FinSequence of the carrier of (F.ii),
ksg being FinSequence of INT such that
A10: len FSg = len ksg & rng FSg c= commutators (F.ii)
& g.x = Product (FSg |^ ksg) by GROUP_5:73;
(1ProdHom (F,ii)) is Homomorphism of F.ii, product F by GROUP_19:6;
then consider F2 being FinSequence of the carrier of product F such that
A11: len F2 = len FSg & F2 = (1ProdHom (F,ii)) * FSg
& Product (F2 |^ ksg) = (1ProdHom (F,ii)).(Product (FSg |^ ksg))
by ThMappingFrobProd2;
for y being object st y in rng F2 holds y in commutators (product F)
proof
let y be object;
assume y in rng F2;
then consider xx being object such that
Z1: xx in dom F2 & y = F2.xx by FUNCT_1:def 3;
xx in dom FSg by Z1, A11, FUNCT_1:11;
then FSg.xx in rng FSg by FUNCT_1:3;
then Z2: FSg.xx in commutators (F.ii) by A10;
Z3: y = (1ProdHom (F,ii)).(FSg.xx) by A11, Z1, FUNCT_1:12;
(1ProdHom (F,ii)) is Homomorphism of F.ii, product F by GROUP_19:6;
hence y in commutators (product F)
by Z2,Z3,ThMorphismOfCommutators;
end;
then A12: rng F2 c= commutators (product F) by TARSKI:def 3;
set FS=FSB ^ F2;
set ks=ksB ^ ksg;
len ks = len ksB + len ksg & len FS = len FSB + len F2 by FINSEQ_1:22;
then E1: len ks = len FS by A9, A10, A11;
E2: rng FS c= commutators (product F)
proof
set X = rng FSB \/ commutators (product F);
rng FSB \/ rng F2 c= X
& X c= commutators (product F) \/ commutators (product F)
by A9, A12, XBOOLE_1:9;
then rng FSB \/ rng F2 c= commutators (product F) by XBOOLE_1:1;
hence thesis by FINSEQ_1:31;
end;
A13: dom (Product (FS |^ ks)) = I
& dom ((1_(product F)) +* (b|(B \/ {x}))) = I
proof
thus dom (Product (FS |^ ks)) = I by GROUP_19:3;
{x} c= J by A6,ZFMISC_1:31;
then Z1: (B \/ {x}) c= J by A7, XBOOLE_1:8;
Z2: dom b = J by PARTFUN1:def 2;
dom ((1_(product F)) +* (b|(B \/ {x})))
= dom (1_(product F)) \/ dom (b|(B \/ {x})) by FUNCT_4:def 1
.= I \/ dom (b|(B \/ {x})) by GROUP_19:3
.= I \/ (B \/ {x}) by Z1,Z2,RELAT_1:62
.= I by Z1, XBOOLE_1:1, XBOOLE_1:12;
hence thesis;
end;
for j being Element of I
holds ((1_(product F)) +* (b|(B \/ {x}))).j = (Product (FS |^ ks)).j
proof
let j be Element of I;
{x} c= J by A6, ZFMISC_1:31;
then A14: (B \/ {x}) c= J by A7, XBOOLE_1:8;
(FS |^ ks) = (FSB |^ ksB) ^ (F2 |^ ksg) by A9,A10,A11,GROUP_4:19;
then A15: Product (FS |^ ks) = Product (FSB |^ ksB) * Product(F2 |^ ksg)
by GROUP_4:5;
A16: dom (b|(B \/ {x})) = (B \/ {x}) by A14, PARTFUN1:def 2;
A17: not (j in B) implies (Product (FSB |^ ksB)).j = 1_(F.j)
proof
assume not j in B;
then not (j in dom (b|B));
then (1_(product F)).j = (Product (FSB |^ ksB)).j by A9,FUNCT_4:11;
hence thesis by GROUP_7:6;
end;
A18: not (j in {x}) implies (Product(F2 |^ ksg)).j = 1_(F.j)
proof
assume not (j in {x});
then Z1: j <> x by TARSKI:def 1;
Z2: dom (1ProdHom (F, ii)) = the carrier of F.ii by FUNCT_2:def 1;
(proj (F,j)).Product(F2 |^ ksg)
= ((proj (F,j)) * (1ProdHom (F, ii))).(Product (FSg |^ ksg))
by Z2, A11, FUNCT_1:13
.= (1:(F.ii, F.j)).(Product (FSg |^ ksg)) by Z1, Th37
.= 1_(F.j);
hence thesis by Def13;
end;
per cases by XBOOLE_0:def 3;
suppose A19: j in B;
Z1: dom b = J by PARTFUN1:def 2;
then Z2: j in dom (b|B) by A7, A19, RELAT_1:62;
dom (b|(B \/ {x})) = B \/ {x} by A14, Z1, RELAT_1:62;
then Z3: j in dom (b|(B \/ {x})) by A19, XBOOLE_0:def 3;
Z4: (proj (F,j)).(Product (FS |^ ks))
= ((proj (F,j)).(Product (FSB |^ ksB)))
* (proj (F,j)).(Product(F2 |^ ksg)) by A15,GROUP_6:def 6
.= ((proj (F,j)).(Product (FSB |^ ksB))) * (1_(F.j))
by A8,A19,A18,Def13,TARSKI:def 1
.= (proj (F,j)).(Product (FSB |^ ksB)) by GROUP_1:def 4
.= (Product (FSB |^ ksB)).j by Def13
.= (b|B).j by A9,Z2,FUNCT_4:13
.= b.j by A19, FUNCT_1:49;
((1_(product F)) +* (b|(B \/ {x}))).j
= (b|(B \/ {x})).j by Z3,FUNCT_4:13
.= b.j by Z3, FUNCT_1:49;
hence ((1_(product F)) +* (b|(B \/ {x}))).j
= (Product (FS |^ ks)).j by Z4, Def13;
end;
suppose A20: j in {x};
Z1: dom (1ProdHom (F,ii)) = the carrier of F.ii by FUNCT_2:def 1;
j = ii by A20, TARSKI:def 1;
then (Product(F2 |^ ksg)).j
= (proj (F, ii)).(Product(F2 |^ ksg)) by Def13
.= ((proj (F,ii)) * (1ProdHom (F,ii))).(Product (FSg |^ ksg))
by A11, Z1, FUNCT_1:13
.= (id (the carrier of F.ii)).(Product (FSg |^ ksg)) by Th38
.= g.j by A10, A20, TARSKI:def 1; then
Z5: ((proj (F,j)).(Product(F2 |^ ksg))) = g.j by Def13;
Z3: (Product (FS |^ ks)).j = b.j
proof
Z4: j in J by A6, A20, TARSKI:def 1;
Z6: ((proj (F,j)).(Product (FSB |^ ksB))) = 1_(F.j)
by Def13, A8, A17, A20,TARSKI:def 1;
(Product (FS |^ ks)).j
= (proj (F,j)).(Product (FSB |^ ksB) * Product(F2 |^ ksg))
by A15,Def13
.= (1_(F.j)) * (g/.j) by Z5, Z6, GROUP_6:def 6
.= g/.j by GROUP_1:def 4;
hence thesis by A5, Z4;
end;
((1_(product F)) +* (b|(B \/ {x}))).j = b.j
proof
j in (B \/ {x}) by A20,XBOOLE_0:def 3;
then ((1_(product F)) +* (b|(B \/ {x}))).j = (b|(B \/ {x})).j
& (b|(B \/ {x})).j = b.j by A16,FUNCT_1:49,FUNCT_4:13;
hence thesis;
end;
hence ((1_(product F)) +* (b|(B \/ {x}))).j = (Product (FS |^ ks)).j
by Z3;
end;
suppose A21: not (j in B \/ {x});
then not (j in dom (b|(B \/ {x})));
then A22: ((1_(product F)) +* (b|(B \/ {x}))).j
= (1_(product F)).j by FUNCT_4:11
.= 1_(F.j) by GROUP_7:6;
(Product (FS |^ ks)).j = 1_(F.j)
proof
(Product (FS |^ ks)).j
= (proj (F,j)).(Product (FSB |^ ksB) * Product(F2 |^ ksg))
by A15,Def13
.= ((proj (F,j)).(Product (FSB |^ ksB)))
* ((proj (F,j)).(Product(F2 |^ ksg))) by GROUP_6:def 6
.= ((proj (F,j)).(Product (FSB |^ ksB)))
* ((Product(F2 |^ ksg))/.j) by Def13
.= ((Product (FSB |^ ksB))/.j)*((Product(F2 |^ ksg))/.j) by Def13
.= 1_(F.j) by A17, A18, A21, GROUP_1:def 4, XBOOLE_0:def 3;
hence thesis;
end;
hence (1_(product F) +* (b|(B \/ {x}))).j = (Product (FS |^ ks)).j
by A22;
end;
end;
then 1_(product F) +* (b|(B \/ {x})) = Product (FS |^ ks) by A13;
hence P[B \/ {x}] by E1,E2;
end;
theorem Th62:
for D being Subgroup-Family of F
st (for i being Element of I holds D.i = (F.i)`)
holds sum D is strict Subgroup of (product F)`
proof
let D be Subgroup-Family of F;
assume A1: for i being Element of I holds D.i = (F.i)`;
sum D is Subgroup of product D & product D is Subgroup of product F;
then A2: sum D is Subgroup of product F;
for g being Element of product F st g in sum D holds g in (product F)`
proof
let g be Element of product F;
assume B1: g in sum D;
1_(product D) = 1_(product F) by GROUP_2:44;
then consider J being finite Subset of I, b being ManySortedSet of J
such that
B2: J = support (g,D) and
B3: g = ((1_(product F)) +* b) and
(for j being object for G being Group st j in I \ J & G = D.j
holds g.j = 1_G) and
B5: for j being object st j in J holds g.j = b.j
by B1, GROUP_19:7;
deffunc F1() = support (g, D);
defpred P[set]
means ex FS being FinSequence of the carrier of product F st
ex ks being FinSequence of INT
st (len FS = len ks & rng FS c= commutators (product F)
& ((1_(product F)) +* (b|$1)) = Product (FS |^ ks));
C1: F1() is finite by B1;
C2: P[ {} ]
proof
1_((product F)`) in (product F)`;
then 1_(product F) in (product F)` by GROUP_2:44;
hence thesis by GROUP_5:73;
end;
C3: for x,B being set st x in F1() & B c= F1() & P[B]
holds P[B \/ {x}]
proof
let x,B be set;
assume D1: x in F1();
assume D2: B c= F1();
assume D3: P[B];
per cases;
suppose x in B;
then B \/ {x} = B by XBOOLE_1:12,ZFMISC_1:31;
hence thesis by D3;
end;
suppose not (x in B);
hence thesis by A1,B1,B2,B5,D1,D2,D3,LmHeartOf62;
end;
end;
P[F1()] from FINSET_1:sch 2(C1, C2, C3);
hence g in (product F)` by B2, B3, GROUP_5:73;
end;
hence sum D is strict Subgroup of (product F)` by A2, GROUP_2:58;
end;
theorem
for I being finite non empty set
for F being Group-Family of I
for D being Subgroup-Family of F
st (for i being Element of I holds D.i = (F.i)`)
holds (product F)` = product D
proof
let I be finite non empty set;
let F be Group-Family of I;
let D be Subgroup-Family of F;
assume A1: for i being Element of I holds D.i = (F.i)`;
sum D = product D by GROUP_7:9;
then A2: product D is strict Subgroup of (product F)` by A1, Th62;
(product F)` is strict Subgroup of product D by A1, Th61;
hence thesis by A2, GROUP_2:55;
end;
begin :: Quotients of Product Groups
definition
let I be non empty set;
let F1, F2 be Group-Family of I;
let f be Homomorphism-Family of F1, F2;
func product f -> Homomorphism of product F1, product F2 means :Def15:
for i being Element of I
holds (proj (F2, i)) * it = (f.i) * (proj (F1, i));
existence
proof
deffunc Fun(Element of I) = (f.$1) * (proj (F1, $1));
A1: for i being Element of I
holds Fun(i) is Homomorphism of product F1, F2.i;
consider phi being Homomorphism-Family of product F1, F2 such that
A2: for i being Element of I holds phi.i = Fun(i)
from RHomFamSch(A1);
take psi = product phi;
thus for i being Element of I
holds (proj (F2, i)) * psi = (f.i) * (proj (F1, i))
proof
let i be Element of I;
for g being Element of product F1
holds ((proj (F2, i)) * psi).g = ((f.i) * (proj (F1, i))).g
proof
let g be Element of product F1;
B1: dom psi = the carrier of product F1 by FUNCT_2:def 1;
Fun(i).g = (phi.i).g by A2
.= (psi.g).i by Def14
.= (proj (F2, i)).(psi.g) by Def13
.= ((proj (F2, i)) * psi).g by B1, FUNCT_1:13;
hence ((proj (F2, i)) * psi).g = ((f.i) * (proj (F1, i))).g;
end;
hence (proj (F2, i)) * psi = (f.i) * (proj (F1, i)) by FUNCT_2:def 8;
end;
end;
uniqueness
proof
for phi1,phi2 being Homomorphism of product F1, product F2
st (for i being Element of I
holds (proj (F2, i)) * phi1 = (f.i) * (proj (F1, i)))
& (for i being Element of I
holds (proj (F2, i)) * phi2 = (f.i) * (proj (F1, i)))
holds phi1 = phi2
proof
let phi1,phi2 be Homomorphism of product F1, product F2;
assume A1: for i being Element of I
holds (proj (F2, i)) * phi1 = (f.i) * (proj (F1, i));
assume A2: for i being Element of I
holds (proj (F2, i)) * phi2 = (f.i) * (proj (F1, i));
A3: dom phi1 = the carrier of product F1
& dom phi2 = the carrier of product F1 by FUNCT_2:def 1;
for g being Element of product F1 holds phi1.g = phi2.g
proof
let g be Element of product F1;
A4: dom (phi1.g) = I & dom (phi2.g) = I by GROUP_19:3;
for i being Element of I holds (phi1.g).i = (phi2.g).i
proof
let i be Element of I;
thus (phi1.g).i = (proj (F2,i)).(phi1.g) by Def13
.= ((proj (F2, i)) * phi1).g by A3, FUNCT_1:13
.= ((f.i) * (proj (F1, i))).g by A1
.= ((proj (F2, i)) * phi2).g by A2
.= (proj (F2, i)).(phi2.g) by A3, FUNCT_1:13
.= (phi2.g).i by Def13;
end;
hence phi1.g = phi2.g by A4;
end;
hence phi1 = phi2 by FUNCT_2:def 8;
end;
hence thesis;
end;
end;
definition
let I be non empty set;
let F1, F2 be Group-Family of I;
let f be Homomorphism-Family of F1, F2;
func Ker f -> componentwise_strict normal Subgroup-Family of F1 means
:Def16:
for i being Element of I
holds it.i = Ker (f.i qua Homomorphism of F1.i,F2.i);
existence
proof
defpred P[Element of I, Group]
means $2 = Ker (f.$1 qua Homomorphism of F1.$1,F2.$1);
A1: for i being Element of I ex H being Subgroup of F1.i st P[i, H];
consider IT being Subgroup-Family of F1 such that
A2: for i being Element of I holds P[i, IT.i]
from SubFamEx(A1);
for i being Element of I holds IT.i is strict Subgroup of F1.i
& IT.i is normal Subgroup of F1.i
proof
let i be Element of I;
Ker (f.i qua Homomorphism of F1.i,F2.i)
is strict normal Subgroup of F1.i;
hence thesis by A2;
end;
then reconsider IT as componentwise_strict normal Subgroup-Family of F1
by Def7,Def4;
take IT;
thus thesis by A2;
end;
uniqueness
proof
thus for N1,N2 being componentwise_strict normal Subgroup-Family of F1
st (for i being Element of I
holds N1.i = Ker (f.i qua Homomorphism of F1.i,F2.i))
& (for i being Element of I
holds N2.i = Ker (f.i qua Homomorphism of F1.i,F2.i))
holds N1 = N2
proof
let N1,N2 be componentwise_strict normal Subgroup-Family of F1;
assume A1: for i being Element of I
holds N1.i = Ker (f.i qua Homomorphism of F1.i,F2.i);
assume A2: for i being Element of I
holds N2.i = Ker (f.i qua Homomorphism of F1.i,F2.i);
A3: dom N1 = I & dom N2 = I by PARTFUN1:def 2;
for i being Element of I holds N1.i = N2.i
proof
let i be Element of I;
thus N1.i = Ker (f.i qua Homomorphism of F1.i,F2.i) by A1
.= N2.i by A2;
end;
hence N1 = N2 by A3;
end;
end;
end;
definition
let I be non empty set;
let F1, F2 be Group-Family of I;
let f be Homomorphism-Family of F1, F2;
func Image f -> componentwise_strict Subgroup-Family of F2 means
:Def17:
for i being Element of I
holds it.i = Image (f.i qua Homomorphism of F1.i,F2.i);
existence
proof
defpred P[Element of I, Group]
means $2 = Image (f.$1 qua Homomorphism of F1.$1,F2.$1);
A1: for i being Element of I ex H being Subgroup of F2.i st P[i, H];
consider IT being Subgroup-Family of F2 such that
A2: for i being Element of I holds P[i, IT.i]
from SubFamEx(A1);
for i being Element of I holds IT.i is strict Subgroup of F2.i
proof
let i be Element of I;
Image (f.i qua Homomorphism of F1.i,F2.i) is strict Subgroup of F2.i;
hence thesis by A2;
end;
then reconsider IT as componentwise_strict Subgroup-Family of F2
by Def4;
take IT;
thus thesis by A2;
end;
uniqueness
proof
thus for N1,N2 being componentwise_strict Subgroup-Family of F2
st (for i being Element of I
holds N1.i = Image (f.i qua Homomorphism of F1.i,F2.i))
& (for i being Element of I
holds N2.i = Image (f.i qua Homomorphism of F1.i,F2.i))
holds N1 = N2
proof
let N1,N2 be componentwise_strict Subgroup-Family of F2;
assume A1: for i being Element of I
holds N1.i = Image (f.i qua Homomorphism of F1.i,F2.i);
assume A2: for i being Element of I
holds N2.i = Image (f.i qua Homomorphism of F1.i,F2.i);
A3: dom N1 = I & dom N2 = I by PARTFUN1:def 2;
for i being Element of I holds N1.i = N2.i
proof
let i be Element of I;
thus N1.i = Image (f.i qua Homomorphism of F1.i,F2.i) by A1
.= N2.i by A2;
end;
hence N1 = N2 by A3;
end;
end;
end;
:: Hungerford, Algebra, Chapter I, Section 8, Theorem 8.10
theorem Th64:
for F1,F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2
holds Ker (product f) = product (Ker f)
proof
let F1,F2 be Group-Family of I;
let f be Homomorphism-Family of F1,F2;
for g being Element of product F1
holds g in Ker (product f) iff g in product (Ker f)
proof
let g be Element of product F1;
hereby
assume A1: g in Ker (product f);
A2: dom g = I by GROUP_19:3;
for i being Element of I holds g.i in (Ker f).i
proof
let i be Element of I;
B1: dom (product f) = the carrier of product F1 & dom (proj
(F1,i)) = the carrier of product F1 by FUNCT_2:def 1;
B2: (proj (F2, i) * (product f)).g
= ((f.i) * (proj (F1, i))).g by Def15
.= (f.i).((proj (F1, i)).g) by B1, FUNCT_1:13
.= (f.i).(g.i) by Def13;
(proj (F2, i) * (product f)).g
= (proj (F2, i)).((product f).g) by B1, FUNCT_1:13
.= (proj (F2, i)).(1_(product F2)) by A1, GROUP_6:41
.= (1_(product F2)).i by Def13
.= 1_(F2.i) by GROUP_7:6;
then (g/.i) in Ker ((f.i) qua Homomorphism of F1.i,F2.i)
by B2, GROUP_6:41;
hence g.i in (Ker f).i by Def16;
end;
hence g in product (Ker f) by A2, Th47;
end;
assume A1: g in product (Ker f);
A2: dom (1_(product F2)) = I & dom ((product f).g) = I
& dom g = I by GROUP_19:3;
for i being Element of I holds ((product f).g).i = (1_(product F2)).i
proof
let i be Element of I;
B1: dom (proj (F1, i)) = the carrier of product F1
& dom (product f) = the carrier of product F1 by FUNCT_2:def 1;
g.i in (Ker f).i by A1, GROUP_19:5;
then B2: g.i in Ker (f.i qua Homomorphism of F1.i,F2.i) by Def16;
B3: (proj (F2, i) * (product f)).g
= ((f.i) * (proj (F1, i))).g by Def15
.= (f.i).((proj (F1, i)).g) by B1, FUNCT_1:13
.= (f.i).(g.i) by Def13;
(proj (F2, i) * (product f)).g
= (proj (F2, i)).((product f).g) by B1,FUNCT_1:13
.= ((product f).g).i by Def13;
then ((product f).g).i = (f.i).(g/.i) by B3
.= 1_(F2.i) by B2, GROUP_6:41;
hence thesis by GROUP_7:6;
end;
then ((product f).g) = 1_(product F2) by A2;
hence g in Ker (product f) by GROUP_6:41;
end;
hence Ker (product f) = product (Ker f) by GROUP_2:def 6;
end;
:: Hungerford, Algebra, Chapter I, Section 8, Theorem 8.10
theorem Th65:
for F1,F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2
holds Image (product f) = product (Image f)
proof
let F1,F2 be Group-Family of I;
let f be Homomorphism-Family of F1,F2;
for g being Element of product F2
holds g in Image (product f) iff g in product (Image f)
proof
let g be Element of product F2;
hereby
assume g in Image (product f);
then consider a being Element of product F1 such that
A2: g = (product f).a by GROUP_6:45;
A3: dom g = I & dom ((product f).a) = I by GROUP_19:3;
for i being Element of I holds g.i in (Image f).i
proof
let i be Element of I;
B1: dom (product f) = the carrier of product F1
& dom (proj (F1,i)) = the carrier of product F1 by FUNCT_2:def 1;
B2: g.i = (proj (F2, i)).((product f).a) by A2,Def13
.= ((proj (F2, i)) * (product f)).a by B1,FUNCT_1:13;
((f.i) * (proj (F1, i))).a = (f.i).((proj (F1, i)).a) by B1,FUNCT_1:13
.= (f.i).(a.i) by Def13;
then g.i = (f.i).(a/.i) by B2, Def15;
then g.i in Image (f.i qua Homomorphism of F1.i,F2.i) by GROUP_6:45;
hence g.i in (Image f).i by Def17;
end;
hence g in product (Image f) by A3, Th47;
end;
defpred P[Element of I, object]
means $2 is Element of F1.$1 & g.$1 = (f.$1).$2;
assume A1: g in product (Image f);
A2: for i being Element of I ex ai being object st P[i, ai]
proof
let i be Element of I;
g.i in (Image f).i by A1, GROUP_19:5;
then g.i in Image (f.i qua Homomorphism of F1.i,F2.i) by Def17;
then ex ai being Element of F1.i st g.i = (f.i) . ai by GROUP_6:45;
hence thesis;
end;
consider a being ManySortedSet of I such that
A3: for i being Element of I holds P[i, a.i]
from PBOOLE:sch 6(A2);
A4: dom a = I by PARTFUN1:def 2;
for i being Element of I holds a.i in F1.i
proof
let i be Element of I;
P[i, a.i] by A3;
hence a.i in F1.i;
end;
then a in product F1 by A4, Th47;
then reconsider a as Element of product F1;
A5: dom g = I & dom ((product f).a) = I by GROUP_19:3;
for i being Element of I holds g.i = ((product f).a).i
proof
let i be Element of I;
B1: dom (product f) = the carrier of product F1
& dom (proj (F1,i)) = the carrier of product F1 by FUNCT_2:def 1;
((product f).a).i = (proj (F2,i)).((product f).a) by Def13
.= ((proj (F2,i)) * (product f)).a by B1, FUNCT_1:13
.= ((f.i) * (proj (F1, i))).a by Def15
.= (f.i).((proj (F1, i)).a) by B1, FUNCT_1:13
.= (f.i).(a.i) by Def13
.= g.i by A3;
hence g.i = ((product f).a).i;
end;
then g = (product f).a by A5;
hence g in Image (product f) by GROUP_6:45;
end;
hence Image (product f) = product (Image f) by GROUP_2:def 6;
end;
theorem
for S being componentwise_strict normal Subgroup-Family of F
holds (product F)./.(product S), product (F./.S) are_isomorphic
proof
let S be componentwise_strict normal Subgroup-Family of F;
deffunc Fun(Element of I) = nat_hom (S.$1);
A1: for i being Element of I holds Fun(i) is Homomorphism of F.i, (F./.S).i
proof
let i be Element of I;
(F./.S).i = (F.i)./.(S.i) by Def8;
hence Fun(i) is Homomorphism of F.i, (F./.S).i;
end;
consider f being Homomorphism-Family of F, (F./.S) such that
A2: for i being Element of I holds f.i = Fun(i)
from HomFamSch(A1);
Ker f = S :: strictness needed for this particular claim
proof
B1: dom (Ker f) = I & dom S = I by PARTFUN1:def 2;
for i being Element of I holds (Ker f).i = S.i
proof
let i be Element of I;
C1: f.i = nat_hom (S.i) by A2;
S.i = Ker (nat_hom (S.i qua normal Subgroup of F.i)) by GROUP_6:43
.= Ker (f.i qua Homomorphism of F.i,(F./.S).i) by C1,Def8
.= (Ker f).i by Def16;
hence (Ker f).i = S.i;
end;
hence thesis by B1;
end;
then A3: Ker (product f) = product S by Th64;
A5: (Image f) = (F./.S)
proof
B1: dom (Image f) = I & dom (F./.S) = I by PARTFUN1:def 2;
for i being Element of I holds (Image f).i = (F./.S).i
proof
let i be Element of I;
C1: f.i = nat_hom (S.i) by A2;
thus (Image f).i = Image (f.i qua Homomorphism of F.i,(F./.S).i) by Def17
.= Image (nat_hom (S.i)) by C1,Def8
.= (F.i)./.(S.i) by GROUP_6:48
.= (F./.S).i by Def8;
end;
hence thesis by B1;
end;
Image (product f) = product (Image f) by Th65
.= product (F./.S) by A5;
hence (product F)./.(product S), product (F./.S) are_isomorphic
by A3, GROUP_6:78;
end;
begin :: Internal direct products
definition
let I be set;
let G be Group;
let IT be Subgroup-Family of I,G;
attr IT is normal means :Def18:
for i being object st i in I holds IT.i is normal Subgroup of G;
attr IT is componentwise_strict means :Def19:
for i being object st i in I holds IT.i is strict Subgroup of G;
end;
theorem ThS1:
for I being non empty set
for G being Group
for F being Subgroup-Family of I,G
holds F is normal
iff (for i being Element of I holds F.i is normal Subgroup of G);
theorem ThS2:
for I being non empty set
for G being Group
for F being Subgroup-Family of I,G
holds F is componentwise_strict
iff (for i being Element of I holds F.i is strict Subgroup of G);
registration
let I be set;
let G be Group;
cluster componentwise_strict normal for Subgroup-Family of I,G;
existence
proof
set F = I --> (1).G;
reconsider F as Group-Family of I;
for i being object st i in I holds F.i is Subgroup of G by FUNCOP_1:7;
then reconsider F as Subgroup-Family of I,G by GROUP_20:def 1;
take F;
thus thesis by FUNCOP_1:7;
end;
end;
definition
let I be non empty set;
let G be Group;
let F be Subgroup-Family of I,G;
let i be Element of I;
redefine func F.i -> Subgroup of G; :: redefines . (FUNCT_1, definition)
coherence by GROUP_20:def 1;
end;
registration
let I be non empty set;
let G be Group;
let F be normal Subgroup-Family of I,G;
let i be Element of I;
cluster F.i -> normal for Subgroup of G;
correctness by ThS1;
end;
theorem
for H1,H2 being Subgroup of G st [. H1, H2 .] = (1).G
for a,b being Element of G st a in H1 & b in H2
holds a*b = b*a
proof
let H1,H2 be Subgroup of G;
assume A1: [. H1, H2 .] = (1).G;
let a,b be Element of G;
assume A2: a in H1;
assume A3: b in H2;
[.a,b.] = 1_G by A1, A2, A3, GROUP_5:1, GROUP_5:65;
hence thesis by GROUP_5:36;
end;
:: Weaker form of GROUP_5:3, we don't really need N to be "strict"
::: Generalize GROUP_5:3
theorem ThNorm:
for N being normal Subgroup of G
for a,b being Element of G
st a in N holds a |^ b in N
proof
let N be normal Subgroup of G;
let a,b be Element of G;
assume a in N;
then a |^ b in N |^ b by GROUP_3:58;
then a |^ b in the multMagma of N by GROUP_3:def 13;
hence a |^ b in N;
end;
theorem
for H,K being normal Subgroup of G
st H /\ K = (1).G
for h,k being Element of G st h in H & k in K
holds h*k = k*h
proof
let H,K be normal Subgroup of G;
assume A1: H /\ K = (1).G;
let h,k be Element of G;
assume A2: h in H;
assume A3: k in K;
[. h, k .] in H /\ K
proof
A4: [. h, k .] in H
proof
h" in H & h |^ k in H by A2, ThNorm, GROUP_2:51;
then (h") * (h |^ k) in H by GROUP_2:50;
hence [. h, k .] in H by GROUP_5:18;
end;
[. h, k .] in K
proof
k" in K by A3, GROUP_2:51;
then (k") |^ h in K by ThNorm;
then ((k") |^ h) * k in K by A3, GROUP_2:50;
hence [. h, k .] in K by GROUP_5:18;
end;
hence thesis by A4, GROUP_2:82;
end;
then 1_G = [. h, k .] by A1, GROUP_5:1;
hence thesis by GROUP_5:36;
end;
theorem ThJoinNorm:
for F being normal Subgroup-Family of I,G
for A being Subset of G
st A = union {the carrier of F.i where i is Element of I :
not contradiction }
ex N being strict normal Subgroup of G
st N = gr A
proof
let F be normal Subgroup-Family of I,G;
let A be Subset of G;
set X = {the carrier of F.i where i is Element of I : not contradiction };
assume A1: A = union X;
reconsider N=gr A as strict Subgroup of G;
A2: for i being Element of I holds the carrier of F.i c= the carrier of N
proof
let i be Element of I;
(the carrier of F.i) in X;
then B1: the carrier of F.i c= A by A1,ZFMISC_1:74;
A c= the carrier of N by GROUP_4:def 4;
hence the carrier of F.i c= the carrier of N by B1, XBOOLE_1:1;
end;
for a being Element of G holds N |^ a is Subgroup of N
proof
let a be Element of G;
for g being Element of G st g in N |^ a holds g in N
proof
let g be Element of G;
assume g in N |^ a;
then consider x being Element of G such that
A4: g = x |^ a & x in N by GROUP_3:58;
consider FS being FinSequence of the carrier of G,
ks being FinSequence of INT such that
A5: len FS = len ks & rng FS c= A & Product (FS |^ ks) = x
by A4,GROUP_4:28;
A6: Product ((FS |^ ks) |^ a) = Product ((FS |^ a) |^ ks) by GROUP_5:15;
for y being object st y in rng ((FS |^ a) |^ ks)
holds y in carr N
proof
let y be object;
assume y in rng ((FS |^ a) |^ ks);
then consider xi being object such that
A7: xi in dom ((FS |^ a) |^ ks) & y = ((FS |^ a) |^ ks).xi
by FUNCT_1:def 3;
A8: len ((FS |^ a) |^ ks) = len ((FS |^ ks) |^ a) by GROUP_5:15
.= len (FS |^ ks) by GROUP_5:def 1;
A9: dom ((FS |^ a) |^ ks)
= Seg (len (FS |^ ks)) by A8, FINSEQ_1:def 3
.= dom (FS |^ ks) by FINSEQ_1:def 3;
reconsider xi as Nat by A7;
A10: dom (FS |^ ks) = Seg (len (FS |^ ks)) by FINSEQ_1:def 3
.= Seg (len FS) by GROUP_4:def 3
.= dom FS by FINSEQ_1:def 3;
FS.xi in rng FS by A7, A9, A10, FUNCT_1:3;
then consider Fi being set such that
A11: FS.xi in Fi & Fi in X by A1,A5,TARSKI:def 4;
consider i0 being Element of I such that
A12: Fi = the carrier of F.i0 by A11;
(FS /. xi) in F.i0 by A10, A7, A9, A11,A12, PARTFUN1:def 6;
then (FS /. xi) |^ (@ (ks /. xi)) in F.i0 by GROUP_4:4;
then (FS |^ ks) . xi in F.i0 by A7, A9, A10, GROUP_4:def 3;
then (FS |^ ks) /. xi in F.i0 by A7, A9, PARTFUN1:def 6;
then A14: ((FS |^ ks) /. xi) |^ a in F.i0 by ThNorm;
y = ((FS |^ ks) |^ a).xi by A7, GROUP_5:15
.= ((FS |^ ks) /. xi) |^ a by A7, A9, GROUP_5:def 1;
hence thesis by A2, A14, TARSKI:def 3;
end;
then Product ((FS |^ a) |^ ks) in N by GROUP_4:18, TARSKI:def 3;
hence g in N by A4,A5,A6,GROUP_5:14;
end;
hence N |^ a is Subgroup of N by GROUP_2:58;
end;
then reconsider N as strict normal Subgroup of G by GROUP_3:122;
take N;
thus N = gr A;
end;
registration
let I be set;
let J be Subset of I;
let F be Group-yielding ManySortedSet of I;
cluster F|J -> Group-yielding J-defined total;
correctness
proof
for y being object st y in rng (F|J) holds y is Group
proof
let y be object;
assume y in rng (F|J);
then consider j being object such that
A1: j in dom (F|J) & y = (F|J).j by FUNCT_1:def 3;
A2: y = F.j by A1, FUNCT_1:47;
dom (F|J) = J & dom F = I by PARTFUN1:def 2;
then F.j in rng F by A1, FUNCT_1:3;
hence y is Group by A2, Def1;
end;
hence thesis;
end;
end;
theorem ThSubFamRes:
for I being set
for F being Subgroup-Family of I,G
for J being set st J c= I
holds F|J is Subgroup-Family of J,G
proof
let I be set;
let F be Subgroup-Family of I,G;
let J be set;
assume A1: J c= I;
for j being object st j in J holds (F|J).j is Subgroup of G
proof
let j be object;
assume A2: j in J;
then F.j is Subgroup of G by A1, GROUP_20:def 1;
hence (F|J).j is Subgroup of G by A2, FUNCT_1:49;
end;
hence F|J is Subgroup-Family of J,G by A1,GROUP_20:def 1;
end;
definition
let I be set;
let G be Group;
let F be Subgroup-Family of I,G;
let J be Subset of I;
redefine func F|J -> Subgroup-Family of J,G; :: redefines | (RELAT_1, definition)
correctness by ThSubFamRes;
end;
registration
let I be set;
let G be Group;
let F be Subgroup-Family of I,G;
let J be Subset of I;
cluster F|J -> Group-yielding;
correctness;
end;
theorem
for F being normal Subgroup-Family of I,G
for A being Subset of G
for i being Element of I
st A = union { the carrier of F.j where j is Element of I : i <> j }
ex N being strict normal Subgroup of G
st N = gr A
proof
let F be normal Subgroup-Family of I,G;
let A be Subset of G;
let i be Element of I;
set X1 = {the carrier of F.j where j is Element of I : i <> j };
assume A1: A = union X1;
set J = I \ {i};
per cases;
suppose J is empty;
then I <> {} & I c= {i} by XBOOLE_1:37;
then A3: I = {i} by ZFMISC_1:33;
not ex x being object st x in X1
proof
given x be object such that
A0: x in X1;
ex j being Element of I st x = the carrier of F.j & i <> j by A0;
hence contradiction by A3, TARSKI:def 1;
end;
then X1 = {} by XBOOLE_0:def 1;
then A4: A = {} the carrier of G by A1, ZFMISC_1:2, SUBSET_1:def 2;
take N = (1).G;
thus thesis by A4, GROUP_4:30;
end;
suppose J is non empty;
then reconsider J as non empty set;
reconsider FF=F|J as Subgroup-Family of J,G by ThSubFamRes;
for j being Element of J holds FF.j is normal Subgroup of G
proof
let j be Element of J;
j in I by XBOOLE_0:def 5;
then F.j is normal Subgroup of G by ThS1;
hence FF.j is normal Subgroup of G by FUNCT_1:49;
end;
then reconsider FF as normal Subgroup-Family of J,G by ThS1;
set X2 = { the carrier of FF.j where j is Element of J :
not contradiction };
for x being object holds x in X1 iff x in X2
proof
let x be object;
hereby
assume x in X1;
then consider j being Element of I such that
Z1: x = the carrier of F.j & i <> j;
j in I & not j in {i} by Z1, TARSKI:def 1;
then reconsider jj=j as Element of J by XBOOLE_0:def 5;
F.j = FF.jj by FUNCT_1:49;
hence x in X2 by Z1;
end;
assume x in X2;
then consider j being Element of J such that
Z1: x = the carrier of FF.j;
j in I & not j in {i} by XBOOLE_0:def 5;
then Z2: j in I & j <> i by TARSKI:def 1;
then reconsider ii=j as Element of I;
the carrier of F.ii = x by Z1, FUNCT_1:49;
hence x in X1 by Z2;
end;
then A3: X1 = X2 by TARSKI:2;
then reconsider B = union X2 as Subset of G by A1;
consider N being strict normal Subgroup of G such that
A2: N = gr B by ThJoinNorm;
take N;
thus N = gr A by A1, A2, A3;
end;
end;
theorem
for J being non empty Subset of I
for F being normal Subgroup-Family of I,G
holds F|J is normal Subgroup-Family of J,G
proof
let J be non empty Subset of I;
let F be normal Subgroup-Family of I,G;
for j being Element of J holds (F|J).j is normal Subgroup of G
proof
let j be Element of J;
j in J;
then j in dom (F|J) by PARTFUN1:def 2;
then F.j = (F|J).j by FUNCT_1:47;
hence (F|J).j is normal Subgroup of G;
end;
hence F|J is normal Subgroup-Family of J,G by ThS1;
end;
theorem ThNormSubFamResIsNorm:
for I being set
for J being Subset of I
for F being normal Subgroup-Family of I,G
holds F|J is normal Subgroup-Family of J,G
proof
let I be set;
let J be Subset of I;
let F be normal Subgroup-Family of I,G;
for i being object st i in J holds (F|J).i is normal Subgroup of G
proof
let i be object;
assume A1: i in J;
then A2: F.i is normal Subgroup of G by Def18;
dom (F|J) = J by PARTFUN1:def 2;
hence (F|J).i is normal Subgroup of G by A1,A2,FUNCT_1:47;
end;
hence F|J is normal Subgroup-Family of J,G by Def18;
end;
registration
let I be set;
let J be Subset of I;
let G be Group;
let F be normal Subgroup-Family of I,G;
cluster F|J -> normal for Subgroup-Family of J,G;
correctness by ThNormSubFamResIsNorm;
end;
theorem ThStrSubFamResIsStr:
for I being set
for J being Subset of I
for F being componentwise_strict Subgroup-Family of I,G
holds F|J is componentwise_strict Subgroup-Family of J,G
proof
let I be set;
let J be Subset of I;
let F be componentwise_strict Subgroup-Family of I,G;
for i being object st i in J
holds (F|J).i is strict Subgroup of G
proof
let i be object;
assume A1: i in J;
then A2: F.i is strict Subgroup of G by Def19;
dom (F|J) = J by PARTFUN1:def 2;
hence (F|J).i is strict Subgroup of G by A1,A2,FUNCT_1:47;
end;
hence F|J is componentwise_strict Subgroup-Family of J,G by Def19;
end;
registration
let I be set;
let J be Subset of I;
let G be Group;
let F be componentwise_strict Subgroup-Family of I,G;
cluster F|J -> componentwise_strict for Subgroup-Family of J,G;
correctness by ThStrSubFamResIsStr;
end;
LmJoinNormUnionRes:
for J being non empty Subset of I
for F being normal Subgroup-Family of I,G
for A being Subset of G
st A = Union (Carrier (F|J))
ex N being strict normal Subgroup of G
st N = gr A
proof
let J be non empty Subset of I;
let F be normal Subgroup-Family of I,G;
let A be Subset of G;
assume A1: A = Union (Carrier (F|J));
set Fam = {the carrier of (F|J).j where j is Element of J : not
contradiction};
set X = union Fam;
for x being object holds x in A iff x in X
proof
let x be object;
hereby
assume x in A;
then x in union (rng (Carrier (F|J))) by A1, CARD_3:def 4;
then consider Uj being set such that
B1: x in Uj & Uj in rng (Carrier (F|J)) by TARSKI:def 4;
consider j being Element of J such that
B2: Uj = (Carrier (F|J)).j by B1, MssRng;
Uj = the carrier of (F|J).j by B2, Th9;
then Uj in Fam;
hence x in X by B1, TARSKI:def 4;
end;
assume x in X;
then consider Uj being set such that
B3: x in Uj & Uj in Fam by TARSKI:def 4;
consider j being Element of J such that
B4: Uj = the carrier of (F|J).j by B3;
B5: dom (Carrier (F|J)) = J by PARTFUN1:def 2;
Uj = (Carrier (F|J)).j by B4,Th9;
then Uj in rng (Carrier (F|J)) by B5, FUNCT_1:3;
then x in union (rng (Carrier (F|J))) by B3, TARSKI:def 4;
hence x in A by A1, CARD_3:def 4;
end;
hence thesis by ThJoinNorm, TARSKI:2;
end;
theorem
for I being set
for J being Subset of I st J is empty
for F being normal Subgroup-Family of I,G
holds Carrier (F|J) = {} --> (bool the carrier of G);
theorem ThJoinNormUnionRes:
for I being set
for J being Subset of I
for F being normal Subgroup-Family of I,G
for A being Subset of G
st A = Union (Carrier (F|J))
ex N being strict normal Subgroup of G
st N = gr A
proof
let I be set;
let J be Subset of I;
let F be normal Subgroup-Family of I,G;
let A be Subset of G;
assume A1: A = Union (Carrier (F|J));
per cases;
suppose J is empty;
then Carrier (F|J) = {} --> (bool the carrier of G);
then Union Carrier (F|J) = {} by FUNCT_6:26;
then A2: A = {} the carrier of G by A1, SUBSET_1:def 2;
take N = (1).G;
thus thesis by A2, GROUP_4:30;
end;
suppose A3: J is non empty;
then ex x being object st x in J by XBOOLE_0:def 1;
then reconsider I as non empty set;
reconsider J as non empty Subset of I by A3;
reconsider F as normal Subgroup-Family of I,G;
A = Union (Carrier (F|J)) by A1;
hence thesis by LmJoinNormUnionRes;
end;
end;
theorem
for I being set
for F being normal Subgroup-Family of I,G
for A being Subset of G
st A = Union (Carrier F)
ex N being strict normal Subgroup of G
st N = gr A
proof
let I be set;
let F be normal Subgroup-Family of I,G;
let A be Subset of G;
assume A1: A = Union (Carrier F);
reconsider J=[#] I as Subset of I;
I = J by SUBSET_1:def 3;
then A = Union (Carrier (F|J)) by A1;
hence thesis by ThJoinNormUnionRes;
end;
theorem CSSubFam:
for F being componentwise_strict Subgroup-Family of I, G
holds F is (Subgroups G)-valued
proof
let F be componentwise_strict Subgroup-Family of I, G;
for y being object st y in rng F holds y in Subgroups G
proof
let y be object;
assume y in rng F;
then consider i being Element of I such that
A1: y = F.i by MssRng;
y is strict Subgroup of G by A1, ThS2;
hence y in Subgroups G by GROUP_3:def 1;
end;
hence F is (Subgroups G)-valued by RELAT_1:def 19, TARSKI:def 3;
end;
registration
let I be non empty set;
let G be Group;
cluster -> (Subgroups G)-valued for componentwise_strict
Subgroup-Family of I,G;
correctness by CSSubFam;
end;
definition
let I be set;
let F be 1-sorted-yielding ManySortedSet of I;
mode Element of F is Element of Carrier F;
end;
theorem EltGF:
for F being Group-Family of I
for g being Element of F
for i being Element of I
holds g.i is Element of F.i
proof
let F be Group-Family of I;
let g be Element of F;
let i be Element of I;
g.i is Element of (Carrier F).i by PBOOLE:def 14;
hence g.i is Element of F.i by Th9;
end;
registration
let I be non empty set;
let G be Group;
let F be Subgroup-Family of I,G;
cluster -> (the carrier of G)-valued for Element of F;
correctness
proof
let g be Element of F;
for y being object st y in rng g holds y in the carrier of G
proof
let y be object;
assume y in rng g;
then consider i being Element of I such that
A1: y = g.i by MssRng;
g.i is Element of F.i by EltGF;
then g.i is Element of G by GROUP_2:42;
hence y in the carrier of G by A1;
end;
hence g is (the carrier of G)-valued by RELAT_1:def 19, TARSKI:def 3;
end;
end;
registration
let I be non empty set;
let G be Group;
let F be Subgroup-Family of I,G;
cluster -> I-defined Relation-like Function-like for Element of product F;
coherence
proof
let g be Element of product F;
dom g = I by GROUP_19:3;
hence thesis by RELAT_1:def 18;
end;
end;
registration
let I be non empty set;
let G be Group;
let F be Subgroup-Family of I,G;
cluster -> I-defined (the carrier of G)-valued total
for Element of product F;
correctness
proof
let g be Element of product F;
A1: dom g = I by GROUP_19:3;
for y being object st y in rng g holds y in the carrier of G
proof
let y be object;
assume y in rng g;
then consider i0 being object such that
A3: i0 in dom g & y = g.i0 by FUNCT_1:def 3;
reconsider i=i0 as Element of I by A3;
g in product F;
then y in F.i by A3, GROUP_19:5;
then y in G by GROUP_2:40;
hence y in the carrier of G;
end;
hence g is I-defined (the carrier of G)-valued total
by A1, PARTFUN1:def 2, TARSKI:def 3, RELAT_1:def 19;
end;
end;
theorem ThSubFamIsBoolValued:
for I being set
for G being Group
for F being Subgroup-Family of I,G
holds Carrier F is (bool the carrier of G)-valued
proof
let I be set;
let G be Group;
let F be Subgroup-Family of I,G;
per cases;
suppose I is empty;
then A1: Carrier F = {};
rng {} = {} & {} c= (bool the carrier of G) by XBOOLE_1:2;
hence Carrier F is (bool the carrier of G)-valued by A1,RELAT_1:def 19;
end;
suppose I is non empty;
then reconsider I as non empty set;
reconsider F as Subgroup-Family of I,G;
for z being object st z in rng (Carrier F)
holds z in bool the carrier of G
proof
let z be object;
assume A3: z in rng (Carrier F);
reconsider y=z as set by TARSKI:1;
consider i being object such that
A4: i in dom (Carrier F) & y = (Carrier F).i
by A3, FUNCT_1:def 3;
reconsider i as Element of I by A4;
y = the carrier of F.i by A4, Th9;
then y c= the carrier of G by GROUP_2:def 5;
hence thesis by ZFMISC_1:def 1;
end;
hence thesis by RELAT_1:def 19, TARSKI:def 3;
end;
end;
registration
let I be set;
let G be Group;
let F be Subgroup-Family of I,G;
cluster Carrier F -> (bool the carrier of G)-valued;
correctness by ThSubFamIsBoolValued;
end;
theorem ThCanSubgrFam:
for G being Group
for S being finite Subset of Subgroups G
for n being Nat st n = card S
holds canFS S is Subgroup-Family of Seg n, G
proof
let G be Group;
let S be finite Subset of Subgroups G;
let n be Nat;
assume A1: n = card S;
len (canFS S) = n by A1, FINSEQ_1:93;
then A2: dom (canFS S) = Seg n by FINSEQ_1:def 3;
for y being object st y in rng (canFS S) holds y is Subgroup of G
proof
let y be object;
assume y in rng (canFS S);
then y in S by FINSEQ_1:def 4, TARSKI:def 3;
hence thesis by GROUP_3:def 1;
end;
then canFS S is Group-yielding;
then A5: canFS S is Group-Family of Seg n by A1, ThCanFSIsMss;
for i being object st i in (Seg n) holds (canFS S).i is Subgroup of G
proof
let i be object;
assume i in Seg n;
then (canFS S).i in rng (canFS S) by A2, FUNCT_1:3;
then (canFS S).i in S by FINSEQ_1:def 4, TARSKI:def 3;
hence thesis by GROUP_3:def 1;
end;
hence thesis by A5, GROUP_20:def 1;
end;
theorem
for G being Group
for N being finite Subset of the_normal_subgroups_of G
for n being Nat st n = card N
holds canFS N is normal Subgroup-Family of Seg n, G
proof
let G be Group;
let N be finite Subset of the_normal_subgroups_of G;
let n be Nat;
assume A1: n = card N;
len (canFS N) = n by A1, FINSEQ_1:93;
then A2: dom (canFS N) = Seg n by FINSEQ_1:def 3;
the_normal_subgroups_of G c= Subgroups G by GRNILP_1:17;
then A3: N is finite Subset of Subgroups G by XBOOLE_1:1;
for i being object st i in Seg n
holds (canFS N).i is normal Subgroup of G
proof
let i be object;
assume i in Seg n;
then (canFS N).i in rng (canFS N) by A2, FUNCT_1:3;
then (canFS N).i in N by FINSEQ_1:def 4, TARSKI:def 3;
hence thesis by GRNILP_1:def 1;
end;
hence canFS N is normal Subgroup-Family of (Seg n), G
by A1, A3, Def18,ThCanSubgrFam;
end;
theorem ThJoinEmptyGr:
for G being Group
for I being empty set
for F being Subgroup-Family of I,G
holds gr Union (Carrier F) = (1).G
proof
let G be Group;
let I be empty set;
let F be Subgroup-Family of I,G;
Carrier F = {} --> (bool the carrier of G);
then Union Carrier F = {} by FUNCT_6:26;
then Union Carrier F = {} the carrier of G by SUBSET_1:def 2;
hence gr Union (Carrier F) = (1).G by GROUP_4:30;
end;
definition
let G be Group;
let I be set;
let F be Subgroup-Family of I,G;
let i be object;
assume A1: i in I;
func F/.i -> Subgroup of G equals :Def20: F.i;
coherence by A1, GROUP_20:def 1;
end;
definition
let G be Group;
let I be set;
let F be Subgroup-Family of I,G;
pred G is_internal_product_of F means
(for i being object st i in I holds F.i is normal Subgroup of G)
& (the multMagma of G = gr Union (Carrier F))
& (for i being object st i in I
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|(I \ {j where j is Element of I :
F.i = F.j}))))
holds F/.i /\ N = (1).G);
end;
theorem
for G being Group
for I being empty set
for F being Subgroup-Family of I,G
holds G is_internal_product_of F iff G is trivial
proof
let G be Group;
let I be empty set;
let F be Subgroup-Family of I,G;
thus G is_internal_product_of F implies G is trivial
by ThJoinEmptyGr;
assume G is trivial;
then the multMagma of G = (1).G by GROUP_22:6;
hence G is_internal_product_of F by ThJoinEmptyGr;
end;
theorem ThIPOa:
for G being Group
for I being non empty set
for F being Subgroup-Family of I,G
holds G is_internal_product_of F
iff ((for i being Element of I holds F.i is normal Subgroup of G)
& (the multMagma of G = gr Union (Carrier F))
& (for i being Element of I
for J being Subset of I st
J = I \ {j where j is Element of I : F.i = F.j}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G))
proof
let G be Group;
let I be non empty set;
let F be Subgroup-Family of I,G;
thus G is_internal_product_of F
implies ((for i being Element of I holds F.i is normal Subgroup of G)
& (the multMagma of G = gr Union (Carrier F))
& (for i being Element of I
for J being Subset of I st
J = I \ {j where j is Element of I : F.i = F.j}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G))
proof
assume A1: G is_internal_product_of F;
thus for i being Element of I holds F.i is normal Subgroup of G
by A1;
thus the multMagma of G = gr Union (Carrier F) by A1;
let i be Element of I;
let J be Subset of I;
assume A3: J = I \ {j where j is Element of I : F.i = F.j};
let N be strict normal Subgroup of G;
assume A4: N = gr (Union (Carrier (F|J)));
F/.i /\ N = (1).G by A1, A3, A4;
hence F.i /\ N = (1).G by Def20;
end;
assume A0: for i being Element of I holds F.i is normal Subgroup of G;
assume A1: the multMagma of G = gr Union (Carrier F);
assume A2: for i being Element of I
for J being Subset of I st J = I \ {j where j is Element of I : F.i = F.j}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G;
reconsider I0=I as set;
reconsider F0=F as Subgroup-Family of I0,G;
for i0 being Element of I0
for J0 being Subset of I0 st
J0 = I0 \ {j where j is Element of I : F.i0 = F.j}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F0|J0)))
holds (F0/.i0) /\ N = (1).G
proof
let i0 be Element of I0;
let J0 be Subset of I0;
assume B2: J0 = I0 \ {j where j is Element of I : F.i0 = F.j};
let N be strict normal Subgroup of G;
assume B3: N = gr (Union (Carrier (F0|J0)));
reconsider i=i0 as Element of I;
reconsider J=I \ {j where j is Element of I : F.i = F.j} as Subset of I;
F.i /\ N = (1).G by A2, B2, B3;
hence (F0/.i0) /\ N = (1).G by Def20;
end;
hence G is_internal_product_of F by A0, A1;
end;
definition
let G be Group;
let I be set;
let F be normal Subgroup-Family of I,G;
redefine pred G is_internal_product_of F means :: redefines is_internal_product_of (GROUP_23, definition)
the multMagma of G = gr Union (Carrier F)
& (for i being object st i in I
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|(I \ {j where
j is Element of I : F.i = F.j}))))
holds F/.i /\ N = (1).G);
correctness by Def18;
end;
theorem ThIPO:
for G being Group
for I being non empty set
for F being normal Subgroup-Family of I,G
holds G is_internal_product_of F
iff ((the multMagma of G = gr Union (Carrier F))
& (for i being Element of I
for J being Subset of I st
J = I \ {j where j is Element of I : F.i = F.j}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G))
proof
let G be Group;
let I be non empty set;
let F be normal Subgroup-Family of I,G;
thus G is_internal_product_of F
implies ((the multMagma of G = gr Union (Carrier F))
& (for i being Element of I
for J being Subset of I st
J = I \ {j where j is Element of I : F.i = F.j}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G)) by ThIPOa;
assume A1: the multMagma of G = gr Union (Carrier F);
assume A2: for i being Element of I
for J being Subset of I st J = I \ {j where j is Element of I : F.i = F.j}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G;
for i being Element of I holds F.i is normal Subgroup of G;
hence thesis by A1,A2,ThIPOa;
end;
theorem ThInjectiveIPO:
for G being Group
for I being non empty set
for F being normal Subgroup-Family of I,G
st F is one-to-one
holds G is_internal_product_of F
iff ((the multMagma of G = gr Union (Carrier F))
& (for i being Element of I
for J being Subset of I st J = I \ {i}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G))
proof
let G be Group;
let I be non empty set;
let F be normal Subgroup-Family of I,G;
assume A1: F is one-to-one;
thus G is_internal_product_of F implies
((the multMagma of G = gr Union (Carrier F))
& (for i being Element of I
for J being Subset of I st J = I \ {i}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G))
proof
assume Z2: G is_internal_product_of F;
hence the multMagma of G = gr Union (Carrier F);
let i be Element of I;
A2: {i} c= {j where j is Element of I : F.i = F.j}
proof
for x being object st x in {i}
holds x in {j where j is Element of I : F.i = F.j}
proof
let x be object;
assume x in {i};
then x = i by TARSKI:def 1;
hence x in {j where j is Element of I : F.i = F.j};
end;
hence thesis by TARSKI:def 3;
end;
for x being object st x in {j where j is Element of I : F.i = F.j}
holds x in {i}
proof
let x be object;
assume x in {j where j is Element of I : F.i = F.j};
then consider j being Element of I such that
B2: x = j & F.i = F.j;
dom F = I by PARTFUN1:def 2;
then i = j by A1, B2;
hence x in {i} by B2, TARSKI:def 1;
end;
then A3: {j where j is Element of I : F.i = F.j} c= {i} by TARSKI:def 3;
let J be Subset of I;
assume J = I \ {i};
then Z4: J = I \ {j where j is Element of I : F.i = F.j}
by A2, A3, XBOOLE_0:def 10;
let N be strict normal Subgroup of G;
assume N = gr (Union (Carrier (F|J)));
hence F.i /\ N = (1).G by Z2, Z4, ThIPO;
end;
assume Z6: the multMagma of G = gr Union (Carrier F);
assume Z7: for i being Element of I
for J being Subset of I st J = I \ {i}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G;
for i being Element of I
for J being Subset of I st J = I \ {j where j is Element of I : F.i = F.j}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G
proof
let i be Element of I;
let J be Subset of I;
assume B2: J = I \ {j where j is Element of I : F.i = F.j};
A2: {i} c= {j where j is Element of I : F.i = F.j}
proof
for x being object st x in {i}
holds x in {j where j is Element of I : F.i = F.j}
proof
let x be object;
assume x in {i};
then x = i by TARSKI:def 1;
hence x in {j where j is Element of I : F.i = F.j};
end;
hence thesis by TARSKI:def 3;
end;
for x being object st x in {j where j is Element of I : F.i = F.j}
holds x in {i}
proof
let x be object;
assume x in {j where j is Element of I : F.i = F.j};
then consider j being Element of I such that
B1: x = j & F.i = F.j;
dom F = I by PARTFUN1:def 2;
then i = j by A1, B1;
hence x in {i} by B1, TARSKI:def 1;
end;
then {j where j is Element of I : F.i = F.j} c= {i} by TARSKI:def 3;
then A3: {j where j is Element of I : F.i = F.j} = {i}
by A2, XBOOLE_0:def 10;
let N be strict normal Subgroup of G;
assume B3: N = gr (Union (Carrier (F|J)));
thus F.i /\ N = (1).G by Z7,B2,B3,A3;
end;
hence G is_internal_product_of F by Z6, ThIPO;
end;
:: Aschbacher, Finite Group Theory, Theorem (1.9)
:: Hungerford, Algebra, Ch. 1, section 8, Theorem 8.6
:: Robinson, Theory of Groups, Ch 1, section 4, Theorem 1.4.7 (ii)
theorem :: ThRecognition:
for G being strict Group
for I being non empty set
for F being normal Subgroup-Family of I,G
st F is one-to-one
holds G is_internal_product_of F iff F is internal DirectSumComponents of G,I
proof
let G be strict Group;
let I be non empty set;
let F be normal Subgroup-Family of I,G;
assume A1: F is one-to-one;
A2: for i being Element of I
for J being Subset of I
holds Carrier (F|J) = (Carrier F) | J
proof
let i be Element of I;
let J be Subset of I;
per cases;
suppose J is empty;
hence thesis;
end;
suppose J is non empty;
then reconsider J as non empty Subset of I;
for j being Element of J
holds (Carrier (F|J)).j = ((Carrier F) | J).j
proof
let j be Element of J;
j in J;
then j in dom (F|J) by PARTFUN1:def 2;
then B1: (F|J).j = F.j by FUNCT_1:47;
B2: (Carrier (F|J)).j = the carrier of F.j by B1, Th9
.= (Carrier F).j by Th9;
dom ((Carrier F)|J) = J by PARTFUN1:def 2;
hence (Carrier (F|J)).j = ((Carrier F) | J).j by B2, FUNCT_1:47;
end;
hence thesis by PBOOLE:def 21;
end;
end;
thus G is_internal_product_of F implies
F is internal DirectSumComponents of G,I
proof
assume A3: G is_internal_product_of F;
A4: (for i being Element of I holds F.i is normal Subgroup of G);
A6: for i being Element of I
ex UFi being Subset of G
st (UFi = Union ((Carrier F) | (I \ {i}))
& ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)})
proof
let i be Element of I;
set J = I \ {i};
take UFi = Union (Carrier (F|(I \ {i})));
thus UFi = Union ((Carrier F) | (I \ {i})) by A2;
consider N being strict normal Subgroup of G such that
B3: N = gr (Union (Carrier (F|(I \ {i}))))
by ThJoinNormUnionRes;
B4: ((F.i) /\ N) = (1).G by A1,A3,B3,ThInjectiveIPO;
[#] ((F.i) /\ N) = (carr (F.i)) /\ (carr N) by GROUP_2:def 10
.= ([#] (F.i)) /\ ([#] (gr UFi)) by B3;
hence ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} by B4, GROUP_2:def 7;
end;
thus F is internal DirectSumComponents of G,I by A3,A4,A6,GROUP_20:16;
end;
thus F is internal DirectSumComponents of G,I implies
G is_internal_product_of F
proof
assume A3: F is internal DirectSumComponents of G,I;
A5: ex UF being Subset of G st (UF = Union (Carrier F) & gr UF = G)
by A3, GROUP_20:16;
for i being Element of I
for J being Subset of I st J = I \ {i}
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|J)))
holds F.i /\ N = (1).G
proof
let i be Element of I;
let J be Subset of I;
assume B2: J = I \ {i};
let N be strict normal Subgroup of G;
assume B3: N = gr (Union (Carrier (F|J)));
consider UFi being Subset of G such that
B4: UFi = Union ((Carrier F)|(I \ {i})) and
B5: ([#] (gr UFi)) /\ ([#] (F.i)) = {(1_ G)} by A3, GROUP_20:16;
N = gr UFi by A2, B2, B3, B4;
then B6: ([#] N) /\ ([#] (F.i)) = carr (1).G by B5,GROUP_2:def 7;
reconsider Fi=F.i as Subgroup of G;
carr ((N qua Subgroup of G) /\ (Fi))
= (carr (N qua Subgroup of G)) /\ (carr (Fi)) by GROUP_2:81;
hence thesis by B6, GROUP_2:59;
end;
hence G is_internal_product_of F by A1, A5, ThInjectiveIPO;
end;
end;
definition
let G be Group;
let Fam be Subset of Subgroups G;
pred G is_internal_product_of Fam means
(for H being strict Subgroup of G st H in Fam
holds H is normal Subgroup of G)
& (ex A being Subset of G
st A = union { UH where UH is Subset of G :
ex H being strict Subgroup of G
st H in Fam & UH = the carrier of H }
& the multMagma of G = gr A)
& (for H being strict Subgroup of G st H in Fam
for A being Subset of G
st A = union { UK where UK is Subset of G :
ex K being strict Subgroup of G
st K in Fam & UK = the carrier of K
& K <> H }
holds H /\ gr A = (1).G);
end;
:: We eventually want to prove a proposition along the lines of
:: "FittingSubgroup G is_internal_product_of Sylow_subgroups G"
:: *without* having to construct a family of subgroups.
definition
let G be Group;
let H be strict Subgroup of G;
let Fam be Subset of Subgroups G;
pred H is_internal_product_of Fam means
(for H1 being strict Subgroup of G st H1 in Fam
holds H1 is normal Subgroup of H)
& (ex A being Subset of G
st A = union { UH where UH is Subset of G :
ex H being strict Subgroup of G
st H in Fam & UH = the carrier of H }
& H = gr A)
& (for H1 being strict Subgroup of G st H1 in Fam
for A being Subset of G
st A = union { UK where UK is Subset of G :
ex K being strict Subgroup of G
st K in Fam & UK = the carrier of K
& K <> H1 }
holds H1 /\ gr A = (1).G);
end;
theorem ThGSubOmega:
G is Subgroup of (Omega).G
proof
G is Subgroup of G by GROUP_2:54;
hence thesis by GROUP_2:57;
end;
theorem ThMinorAnnoyance:
for G being Group
for H being Subgroup of G
st H is normal Subgroup of (Omega).G
holds H is normal Subgroup of G
proof
let G be Group;
let H be Subgroup of G;
assume Z1: H is normal Subgroup of (Omega).G;
G is Subgroup of (Omega).G by ThGSubOmega;
hence thesis by Z1, GROUP_6:8;
end;
theorem
for G being Group
for Fam being Subset of Subgroups G
holds G is_internal_product_of Fam
iff (Omega).G is_internal_product_of Fam
proof
let G be Group;
let Fam be Subset of Subgroups G;
hereby
assume A1: G is_internal_product_of Fam;
for H being strict Subgroup of G st H in Fam
holds H is normal Subgroup of (Omega).G
proof
let H be strict Subgroup of G;
assume H in Fam;
then H is normal Subgroup of G by A1;
hence H is normal Subgroup of (Omega).G
by GROUP_6:8, GROUP_2:57, GROUP_2:def 5;
end;
hence (Omega).G is_internal_product_of Fam by A1;
end;
assume A2: (Omega).G is_internal_product_of Fam;
for H being strict Subgroup of G st H in Fam
holds H is normal Subgroup of G
proof
let H be strict Subgroup of G;
assume H in Fam;
then H is normal Subgroup of (Omega).G by A2;
hence H is normal Subgroup of G by ThMinorAnnoyance;
end;
hence G is_internal_product_of Fam by A2;
end;
theorem ThCarrG:
for G being Group
for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of Subgroups G st Fam = rng F
holds union { A where A is Subset of G : ex H being strict Subgroup of G
st H in Fam & A = the carrier of H } = Union (Carrier F)
proof
let G be Group;
let I be non empty set;
let F be componentwise_strict Subgroup-Family of I,G;
let Fam be Subset of Subgroups G;
assume A1: Fam = rng F;
set X = { A where A is Subset of G : ex H being strict Subgroup of G
st H in Fam & A = the carrier of H };
for x being object holds x in X iff x in rng (Carrier F)
proof
let x be object;
hereby
assume x in X;
then consider A being Subset of G such that
A2: x = A &
ex H being strict Subgroup of G st H in Fam & A = the carrier of H;
consider H being strict Subgroup of G such that
A3: H in Fam & x = the carrier of H by A2;
consider i being Element of I such that
A4: H = F.i by A1, A3, MssRng;
x = (Carrier F).i by A3,A4,Th9;
hence x in rng (Carrier F) by MssRng;
end;
assume x in rng (Carrier F);
then consider i being Element of I such that
A5: x = (Carrier F).i by MssRng;
F.i is strict Subgroup of G by Def19;
then consider H being strict Subgroup of G such that
A6: H = F.i;
A8: H in Fam by A1, A6, MssRng;
ex A being Subset of G st x = A & ex H0 being strict Subgroup
of G st A = the carrier of H0 & H0 in Fam
proof
take A = carr H;
thus thesis by A8, A5, A6, Th9;
end;
hence x in X;
end;
then X = rng (Carrier F) by TARSKI:2;
hence union X = Union (Carrier F) by CARD_3:def 4;
end;
theorem ThUnionFam:
for G being Group
for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of Subgroups G st Fam = rng F
for H being strict Subgroup of G
for i being Element of I st H = F.i
for J being Subset of I st J = I \ {j where j is Element of I : F.i = F.j}
holds
union { A where A is Subset of G :
ex K being strict Subgroup of G
st K in Fam & A = the carrier of K & K <> H }
= Union (Carrier (F|J))
proof
let G be Group;
let I be non empty set;
let F be componentwise_strict Subgroup-Family of I,G;
let Fam be Subset of Subgroups G;
assume A1: Fam = rng F;
let H be strict Subgroup of G;
let i be Element of I;
assume A3: H = F.i;
let J be Subset of I;
assume A4: J = I \ {j where j is Element of I : F.i = F.j};
set X = { A where A is Subset of G :
ex K being strict Subgroup of G
st K in Fam & A = the carrier of K & K <> H };
for x being object holds x in X iff x in rng (Carrier (F|J))
proof
let x be object;
thus x in X implies x in rng (Carrier (F|J))
proof
assume x in X;
then consider A being Subset of G such that
B2: A = x & ex K being strict Subgroup of G
st K in Fam & A = the carrier of K & K <> H;
consider K being strict Subgroup of G such that
B3: K in Fam & A = the carrier of K & K <> H by B2;
consider j being Element of I such that
B4: F.j = K by A1, B3, MssRng;
B5: dom (F|J) = J & dom (Carrier (F|J)) = J by PARTFUN1:def 2;
B6: j in J
proof
not j in {j1 where j1 is Element of I : F.i = F.j1}
by A3, B3, B4, ThCoim;
hence thesis by A4, XBOOLE_0:def 5;
end;
then reconsider j as Element of J;
reconsider Fj=(F|J).j as Subgroup of G by B6, GROUP_20:def 1;
B7: (Carrier (F|J)).j = the carrier of Fj by B6, Th9;
A = (Carrier (F|J)).j by B3, B4, B6, B7, FUNCT_1:49;
hence x in rng (Carrier (F|J)) by B2, B5, B6, FUNCT_1:3;
end;
assume x in rng (Carrier (F|J));
then consider j0 being object such that
Z3: j0 in dom (Carrier (F|J)) & x = (Carrier (F|J)).j0
by FUNCT_1:def 3;
reconsider j=j0 as Element of J by Z3;
Z5: j in J by Z3;
reconsider Fj = (F|J).j as Subgroup of G by Z3, GROUP_20:def 1;
reconsider A = the carrier of Fj as Subset of G by GROUP_2:def 5;
Z5b: Fj = F.j by Z3, FUNCT_1:49;
Z6: Fj in Fam
proof
j in I by Z5;
then B2: j in dom F by PARTFUN1:def 2;
(F|J).j = F.j by Z3, FUNCT_1:49;
hence thesis by A1, B2, FUNCT_1:3;
end;
Z7: Fj <> H
proof
not j in {j where j is Element of I : F.i = F.j}
by A4, Z3, XBOOLE_0:def 5;
hence H <> Fj by A3, Z5, Z5b;
end;
Z8: x = the carrier of Fj by Z3, Th9;
ex K being strict Subgroup of G
st K in Fam & A = the carrier of K & K <> H
proof
reconsider K = Fj as strict Subgroup of G by Z3, Def19;
take K;
thus thesis by Z6, Z7;
end;
hence x in X by Z8;
end;
then X = rng (Carrier (F|J)) by TARSKI:2;
hence union X = Union (Carrier (F|J)) by CARD_3:def 4;
end;
theorem :::ThEquivDefs:
for G being Group
for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of Subgroups G st Fam = rng F
holds G is_internal_product_of F
iff G is_internal_product_of Fam
proof
let G be Group;
let I be non empty set;
let F be componentwise_strict Subgroup-Family of I,G;
let Fam be Subset of Subgroups G;
assume A1: Fam = rng F;
thus G is_internal_product_of F implies G is_internal_product_of Fam
proof
assume B1: G is_internal_product_of F;
B2: for H being strict Subgroup of G st H in Fam
holds H is normal Subgroup of G
proof
let H be strict Subgroup of G;
assume H in Fam;
then consider i being Element of I such that
Z1: H = F.i by A1, MssRng;
thus H is normal Subgroup of G by B1, Z1;
end;
B3: ex A being Subset of G
st A = union { UH where UH is Subset of G :
ex H being strict Subgroup of G
st H in Fam & UH = the carrier of H }
& the multMagma of G = gr A
proof
consider A being Subset of G such that
Z1: A = Union (Carrier F);
take A;
thus union { A where A is Subset of G :
ex H being strict Subgroup of G
st H in Fam & A = the carrier of H }
= A by A1,Z1,ThCarrG;
thus the multMagma of G = gr A by Z1, B1;
end;
for H being strict Subgroup of G st H in Fam
for A being Subset of G
st A = union { UK where UK is Subset of G :
ex K being strict Subgroup of G
st K in Fam & UK = the carrier of K
& K <> H }
holds H /\ gr A = (1).G
proof
let H be strict Subgroup of G;
assume Z1: H in Fam;
let A be Subset of G;
assume Z2: A = union { UK where UK is Subset of G :
ex K being strict Subgroup of G
st K in Fam & UK = the carrier of K & K <> H };
consider i being Element of I such that
Z3: H = F.i by A1,Z1,MssRng;
reconsider J=I \ {j where j is Element of I : F.i = F.j} as Subset of I;
for i being Element of I holds F.i is normal Subgroup of G by B1;
then F is normal Subgroup-Family of I,G by ThS1;
then consider N being strict normal Subgroup of G such that
Z5: N = gr Union (Carrier (F|J)) by ThJoinNormUnionRes;
H = F/.i & F/.i /\ N = (1).G by B1, Z3, Z5, Def20;
hence H /\ gr A = (1).G by A1, Z2, Z3, Z5, ThUnionFam;
end;
hence G is_internal_product_of Fam by B2, B3;
end;
assume B1: G is_internal_product_of Fam;
B2: for i being Element of I holds F.i is normal Subgroup of G
proof
let i be Element of I;
F.i is Subgroup of G & F.i is strict Subgroup of G by ThS2;
hence F.i is normal Subgroup of G by A1, B1, MssRng;
end;
for i being Element of I
for N being strict normal Subgroup of G
st N = gr (Union (Carrier (F|(I \ {j where j is Element of I : F.i = F.j}))))
holds F/.i /\ N = (1).G
proof
let i be Element of I;
let N be strict normal Subgroup of G;
assume Z2: N = gr (Union (Carrier (F|(I \ {j where
j is Element of I : F.i = F.j}))));
reconsider H=F.i as strict Subgroup of G by Def19;
reconsider H as strict normal Subgroup of G by A1, B1, MssRng;
reconsider J = I \ {j where j is Element of I : F.i = F.j} as Subset of I;
Z4: union { A0 where A0 is Subset of G :
ex K being strict Subgroup of G
st K in Fam & A0 = the carrier of K & K <> H }
= Union (Carrier (F|J)) by A1, ThUnionFam; then
reconsider A = union { A0 where A0 is Subset of G :
ex K being strict Subgroup of G
st K in Fam & A0 = the carrier of K & K <> H }
as Subset of G;
H /\ N = (1).G by A1, B1, Z2, Z4, MssRng;
hence thesis by Def20;
end;
hence G is_internal_product_of F by A1, B1, B2, ThCarrG;
end;
:: It turns out, the real universal property of product groups are the
:: friends we made along the way.