Copyright (c) 1991 Association of Mizar Users
environ
vocabulary CLASSES2, PARTFUN1, RELAT_1, FUNCT_1, MIDSP_1, BOOLE, VECTSP_2,
FUNCT_2, VECTSP_1, MIDSP_2, RLVECT_1, ARYTM_1, CAT_1, TARSKI, CAT_2,
PRE_TOPC, ORDINAL4, FUNCOP_1, MOD_1, ENS_1, GRCAT_1, ALGSTR_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MOD_1, RELAT_1, FUNCT_1,
MCART_1, STRUCT_0, BINOP_1, RLVECT_1, VECTSP_1, VECTSP_2, PARTFUN1,
CAT_1, CLASSES2, PRE_TOPC, FUNCT_2, CAT_2, ALGSTR_1, MIDSP_1, MIDSP_2;
constructors BINOP_1, VECTSP_2, CLASSES2, CAT_2, MIDSP_2, TOPS_2, ALGSTR_1,
CLASSES1, MEMBERED, PARTFUN1, RELAT_2, XBOOLE_0;
clusters RELSET_1, GROUP_1, STRUCT_0, SUBSET_1, CLASSES2, ALGSTR_1, MIDSP_2,
MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0;
requirements SUBSET, BOOLE;
theorems BINOP_1, CAT_1, CAT_2, CLASSES2, FUNCOP_1, FUNCT_1, FUNCT_2, MIDSP_2,
MCART_1, PARTFUN1, VECTSP_1, TARSKI, ZFMISC_1, RLVECT_1, RELAT_1,
RELSET_1, ORDINAL1, XBOOLE_0, ALGSTR_1;
schemes FUNCT_2, PARTFUN1, TARSKI, XBOOLE_0;
begin :: 0a. Auxiliary theorems: sets and universums
reserve x, y for set;
reserve D for non empty set;
reserve UN for Universe;
canceled;
theorem
Th2: for X,Y,A being set, z being set st z in A & A c= [:X,Y:]
ex x being Element of X, y being Element of Y st z = [x,y]
proof
let X,Y,A be set, z be set;
assume z in A & A c= [:X,Y:];
then consider x,y such that
A1: x in X & y in Y & z = [x,y] by ZFMISC_1:103;
reconsider x as Element of X by A1;
reconsider y as Element of Y by A1;
take x,y;
thus thesis by A1;
end;
theorem
Th3: for u1,u2,u3,u4 being Element of UN holds
[u1,u2,u3] is Element of UN & [u1,u2,u3,u4] is Element of UN
proof
let u1,u2,u3,u4 be Element of UN;
A1: [u1,u2,u3] = [[u1,u2],u3] by MCART_1:def 3;
[u1,u2,u3,u4] = [[u1,u2,u3],u4] by MCART_1:def 4;
hence thesis by A1,CLASSES2:64;
end;
theorem
Th4: for x,y st x in y & y in UN holds x in UN
proof
let x,y; assume
A1: x in y & y in UN;
then y c= UN by ORDINAL1:def 2;
hence thesis by A1;
end;
:: 0b. Auxiliary schemes: partial functions
scheme PartLambda2{X,Y,Z()->set,F(set,set)->set,P[set,set]}:
ex f being PartFunc of [:X(),Y():],Z()
st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y])
& (for x,y st [x,y] in dom f holds f.[x,y] = F(x,y))
provided
A1: for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z()
proof
defpred R[set,set] means $1 in X() & $2 in Y() & P[$1,$2];
deffunc G(set,set) = F($1,$2);
A2: for x,y st R[x,y] holds G(x,y) in Z() by A1;
consider f being PartFunc of [:X(),Y():],Z() such that
A3: (for x,y holds [x,y] in dom f iff x in X() & y in Y() & R[x,y]) and
A4: (for x,y st [x,y] in dom f holds f.[x,y] = G(x,y)) from LambdaR2(A2);
take f;
thus for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y] by A3;
thus for x,y st [x,y] in dom f holds f.[x,y] = F(x,y) by A4;
end;
scheme PartLambda2D{X,Y()->non empty set,Z()->set,F(set,set)->set,
P[set,set]}: ex f being PartFunc of [:X(),Y():],Z()
st (for x being Element of X(), y being Element of Y() holds
[x,y] in dom f iff P[x,y])
& (for x being Element of X(), y being Element of Y() st [x,y] in
dom f holds f.[x,y] = F(x,y))
provided
A1: for x being Element of X(), y being Element of Y() st P[x,y] holds
F(x,y) in Z()
proof
defpred R[set,set] means P[$1,$2];
deffunc G(set,set) = F($1,$2);
A2: for x,y st x in X() & y in Y() & R[x,y] holds G(x,y) in Z() by A1;
consider f being PartFunc of [:X(),Y():],Z() such that
A3: for x,y holds [x,y] in dom f iff x in X() & y in Y() & R[x,y] and
A4: for x,y st [x,y] in dom f holds f.[x,y] = G(x,y) from PartLambda2(A2);
take f;
thus for x being Element of X(), y being Element of Y() holds
[x,y] in dom f iff P[x,y] by A3;
thus for x being Element of X(), y being Element of Y() st [x,y] in dom f
holds f.[x,y] = F(x,y) by A4;
end;
:: 0c. Auxiliary theorems: Trivial Group
theorem
Th5: op2.({},{}) = {} & op1.{} = {} & op0 = {}
proof
A1: {} in {{}} by TARSKI:def 1;
[{},{}] in [:{{}},{{}}:] by ZFMISC_1:34;
then op2.[{},{}] = {} by FUNCT_2:65;
hence op2.({},{}) = {} by BINOP_1:def 1;
thus op1.{} = {} by A1,FUNCT_2:65;
thus op0 = {} by TARSKI:def 1;
end;
theorem
Th6: {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN &
op2 in UN & op1 in UN
proof
set D = {{}};
{} in UN by CLASSES2:62;
hence A1: D in UN by CLASSES2:63;
hence [D,D] in UN by CLASSES2:64;
thus A2: [:D,D:] in UN by A1,CLASSES2:67;
A3: Funcs(D,D) in UN by A1,CLASSES2:67;
A4: Funcs([:D,D:],D) in UN by A1,A2,CLASSES2:67;
op2 in Funcs([:D,D:],D) by FUNCT_2:11;
hence op2 in UN by A4,Th4;
op1 in Funcs(D,D) by FUNCT_2:11;
hence op1 in UN by A3,Th4;
end;
theorem
Th7: LoopStr (# {{}},op2,Extract {} #) is midpoint_operator
proof
set G = LoopStr (# {{}}, op2, Extract {} #);
A1: for a being Element of G
ex x being Element of G st Double x = a
proof
let a be Element of G;
consider x being Element of G;
take x;
thus Double x = {} by TARSKI:def 1
.= a by TARSKI:def 1;
end;
now
let a be Element of G;
assume Double a = 0.G;
thus a = {} by TARSKI:def 1
.= 0.G by TARSKI:def 1;end;
hence thesis by A1,MIDSP_2:def 5;
end;
definition
cluster L_Trivial -> midpoint_operator;
coherence by Th7,ALGSTR_1:def 4;
end;
theorem
(for x being Element of L_Trivial holds x = {})
& (for x,y being Element of L_Trivial holds x+y = {})
& (for x being Element of L_Trivial holds -x = {})
& 0.L_Trivial = {} by ALGSTR_1:def 4,TARSKI:def 1;
:: 0d. Auxiliary theorems: subcategories
reserve C for Category;
reserve O for non empty Subset of the Objects of C;
definition let C,O;
canceled 4;
func Morphs(O) -> Subset of the Morphisms of C equals :Def5:
union{Hom(a,b) where a is Object of C,b is Object of C : a in O & b in O};
coherence by CAT_2:28;
end;
definition let C,O;
cluster Morphs(O) -> non empty;
coherence
proof
union{Hom(a,b) where a is Object of C,b is Object of C : a in O & b in O}
= Morphs O by Def5;
hence thesis by CAT_2:28;
end;
end;
definition let C,O;
func dom(O) -> Function of Morphs(O),O equals
:Def6: (the Dom of C)|Morphs(O);
coherence
proof
set M = Morphs(O);
M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in
O}
by Def5;
hence (the Dom of C)|M is Function of M,O by CAT_2:29;
end;
func cod(O) -> Function of Morphs(O),O equals
:Def7: (the Cod of C)|Morphs(O);
coherence
proof
set M = Morphs(O);
M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in
O}
by Def5;
hence (the Cod of C)|M is Function of M,O by CAT_2:29;
end;
func comp(O) -> PartFunc of [:Morphs(O),(Morphs(O)):],Morphs(O) equals
:Def8: (the Comp of C)|([:Morphs(O),Morphs(O):] qua set);
coherence
proof
set M = Morphs(O);
M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in
O} by Def5;
hence (the Comp of C)|([:M,M:] qua set)
is PartFunc of [:M,M:],M by CAT_2:29;
end;
func ID(O) -> Function of O,Morphs(O) equals
:Def9: (the Id of C)|O;
coherence
proof
set M = Morphs(O);
M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in
O}
by Def5;
hence (the Id of C)|O is Function of O,M by CAT_2:29;
end;
end;
theorem
Th9: CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#)
is_full_subcategory_of C
proof
set M = Morphs(O);
A1: M = union{Hom(a,b) where a is Object of C,b is Object of C:
a in O & b in O} by Def5;
A2: dom(O) = (the Dom of C)|M by Def6;
A3: cod(O) = (the Cod of C)|M by Def7;
A4: comp(O) = (the Comp of C)|([:M,M:] qua set) by Def8;
ID(O) = (the Id of C)|O by Def9;
hence thesis by A1,A2,A3,A4,CAT_2:30;
end;
definition let C,O;
func cat(O) -> Subcategory of C equals
:Def10: CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#);
coherence
proof
CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#)
is_full_subcategory_of C by Th9;
hence thesis by CAT_2:def 6;
end;
end;
definition let C,O;
cluster cat(O) -> strict;
coherence
proof
CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#) = cat O by Def10;
hence thesis;
end;
end;
theorem
Th10: the Objects of cat(O) = O
proof
cat(O) = CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#) by Def10;
hence thesis;
end;
:: 1a. Maps of the carriers of groups
definition let G be 1-sorted;
func id G -> map of G,G equals
:Def11: id the carrier of G;
coherence;
end;
theorem Th11:
for G being non empty 1-sorted,
x being Element of G holds (id G).x = x
proof
let G be non empty 1-sorted;
let x be Element of G;
id G = id the carrier of G by Def11;
hence thesis by FUNCT_1:35;
end;
theorem Th12:
for G being 1-sorted, H being non empty 1-sorted,
f being map of G, H holds f*(id G) = f & (id H)*f = f
proof
let G be 1-sorted, H be non empty 1-sorted;
let f be map of G,H;
set u = id G, v = id H, X = the carrier of G, Y = the carrier of H;
A1: u = id X & v = id Y by Def11;
A2: dom f = X by FUNCT_2:def 1;
rng f c= Y by RELSET_1:12;
hence f*u = f & v*f = f by A1,A2,RELAT_1:77,79;
end;
definition let G,H be non empty ZeroStr;
func ZeroMap(G,H) -> map of G,H equals
:Def12: (the carrier of G) --> 0.H;
coherence
proof
set i = (the carrier of G) --> 0.H;
dom i = the carrier of G & rng i = {0.H} by FUNCOP_1:14,19;
then i is Function of the carrier of G, the carrier of H by FUNCT_2:4;
hence i is map of G,H;
end;
end;
definition let G,H be non empty LoopStr; let f be map of G,H;
attr f is additive means
:Def13: for x,y being Element of G holds f.(x+y) = f.x+f.y;
end;
theorem Th13:
comp L_Trivial = op1
proof
reconsider f = comp L_Trivial as Function of {{}}, {{}} by ALGSTR_1:def 4;
for x being set st x in {{}} holds op1.x = f.x
proof
let x be set; assume A1: x in {{}};
then reconsider x as Element of L_Trivial by ALGSTR_1:def
4;
x = {} by A1,TARSKI:def 1;
then op1.x = -x by Th5,ALGSTR_1:def 4,TARSKI:def 1 .= f.x by VECTSP_1:def
25;
hence thesis;
end;
hence thesis by FUNCT_2:18;
end;
theorem
Th14: for G1,G2,G3 being non empty LoopStr,
f being map of G1,G2, g being map of G2,G3
st f is additive & g is additive holds g*f is additive
proof
let G1,G2,G3 be non empty LoopStr,
f be map of G1,G2, g be map of G2,G3 such that
A1: f is additive and
A2: g is additive;
set h = g*f;
now let x,y be Element of G1;
A3: g.(f.x) = h.x & g.(f.y) = h.y by FUNCT_2:21;
thus h.(x+y) = g.(f.(x+y)) by FUNCT_2:21
.= g.(f.x+f.y) by A1,Def13
.= h.x+h.y by A2,A3,Def13;end;
hence thesis by Def13;
end;
theorem Th15:
for G being non empty ZeroStr,
H being non empty LoopStr,
x being Element of G holds ZeroMap(G,H).x = 0.H
proof
let G be non empty ZeroStr,
H be non empty LoopStr;
let x be Element of G;
(ZeroMap(G,H)) = (the carrier of G) --> 0.H by Def12;
hence thesis by FUNCOP_1:13;
end;
theorem Th16:
for G being non empty LoopStr,
H being right_zeroed (non empty LoopStr) holds ZeroMap(G,H) is additive
proof
let G be non empty LoopStr, H be right_zeroed (non empty LoopStr);
set f = ZeroMap(G,H);
for x,y being Element of G holds f.(x+y) = f.x+f.y
proof
let x,y be Element of G;
f.(x+y) = 0.H & f.x = 0.H & f.y = 0.H by Th15;
hence f.(x+y) = f.x+f.y by RLVECT_1:def 7;
end;
hence thesis by Def13;
end;
:: 1b. Morphisms of groups
reserve G,H for AddGroup;
definition
struct GroupMorphismStr (# Dom,Cod -> AddGroup,
Fun -> map of the Dom, the Cod #);
end;
definition let f be GroupMorphismStr;
func dom(f) -> AddGroup equals
:Def14: the Dom of f;
coherence;
func cod(f) -> AddGroup equals
:Def15: the Cod of f;
coherence;
end;
definition let f be GroupMorphismStr;
func fun(f) -> map of dom(f),cod(f) equals
:Def16: the Fun of f;
coherence
proof
dom(f) = the Dom of f & cod(f) = the Cod of f by Def14,Def15;
hence the Fun of f is map of dom(f),cod(f);
end;
end;
theorem
for f being GroupMorphismStr,
G1,G2 being AddGroup,
f0 being map of G1,G2 st f = GroupMorphismStr(# G1,G2,f0#)
holds dom f = G1 & cod f = G2 & fun f = f0 by Def14,Def15,Def16;
definition let G,H;
func ZERO(G,H) -> GroupMorphismStr equals
:Def17: GroupMorphismStr(# G,H,ZeroMap(G,H)#);
coherence;
end;
definition let G,H;
cluster ZERO(G,H) -> strict;
coherence
proof
ZERO(G,H) = GroupMorphismStr(# G,H,ZeroMap(G,H)#) by Def17;
hence thesis;
end;
end;
Lm1: dom(ZERO(G,H)) = G & cod(ZERO(G,H)) = H
& fun(ZERO(G,H)) = ZeroMap(G,H)
proof
ZERO(G,H) = GroupMorphismStr(# G,H,ZeroMap(G,H)#) by Def17;
hence thesis by Def14,Def15,Def16;
end;
definition let IT be GroupMorphismStr;
attr IT is GroupMorphism-like means
:Def18: fun(IT) is additive;
end;
definition
cluster strict GroupMorphism-like GroupMorphismStr;
existence
proof
consider G,H;
set z = ZERO(G,H);
dom(z) = G & cod(z) = H & fun(z) = ZeroMap(G,H) by Lm1;
then fun(z) is additive by Th16;
then z is GroupMorphism-like by Def18;
hence thesis;
end;
end;
definition
mode GroupMorphism is GroupMorphism-like GroupMorphismStr;
end;
theorem
Th18: for F being GroupMorphism holds the Fun of F is additive
proof
let F be GroupMorphism;
A1: the Fun of F = fun(F) by Def16;
the Dom of F = dom(F) & the Cod of F = cod(F) by Def14,Def15;
hence thesis by A1,Def18;
end;
definition let G,H;
cluster ZERO(G,H) -> GroupMorphism-like;
coherence
proof
set z = ZERO(G,H);
dom(z) = G & cod(z) = H & fun(z) = ZeroMap(G,H) by Lm1;
then fun(z) is additive by Th16;
hence thesis by Def18;
end;
end;
definition let G,H;
mode Morphism of G,H -> GroupMorphism means
:Def19: dom(it) = G & cod(it) = H;
existence
proof
take ZERO(G,H);
thus thesis by Lm1;
end;
end;
definition let G,H;
cluster strict Morphism of G,H;
existence
proof
dom(ZERO(G,H)) = G & cod(ZERO(G,H)) = H by Lm1;
then ZERO(G,H) is Morphism of G,H by Def19;
hence thesis;
end;
end;
theorem
Th19: for f being strict GroupMorphismStr
st dom(f) = G & cod(f) = H & fun(f) is additive
holds f is strict Morphism of G,H
proof
let f be strict GroupMorphismStr; assume
A1: dom(f) = G & cod(f) = H & fun(f) is additive;
then reconsider f' = f as strict GroupMorphism by Def18;
f' is strict Morphism of G,H by A1,Def19;
hence thesis;
end;
theorem
Th20: for f being map of G,H st f is additive
holds GroupMorphismStr (# G,H,f#) is strict Morphism of G,H
proof
let f be map of G,H such that
A1: f is additive;
set F = GroupMorphismStr (# G,H,f#);
dom(F) = G & cod(F) = H & fun(F) = f by Def14,Def15,Def16;
hence thesis by A1,Th19;
end;
theorem Th21:
for G being non empty LoopStr holds id G is additive
proof
let G be non empty LoopStr;
set f = id G;
for x,y being Element of G holds f.(x+y) = f.x+f.y
proof
let x,y be Element of G;
f.(x+y) = x+y & f.x = x & f.y = y by Th11;
hence f.(x+y) = f.x+f.y;
end;
hence thesis by Def13;
end;
definition let G;
func ID G -> Morphism of G,G equals
:Def20: GroupMorphismStr(# G,G,id G#);
coherence
proof
set i = GroupMorphismStr(# G,G,id G#);
A1: dom(i) = G & cod(i) = G & fun(i) = id G by Def14,Def15,Def16;
id G is additive by Th21;
hence i is Morphism of G,G by A1,Th19;
end;
end;
definition let G;
cluster ID G -> strict;
coherence
proof
ID G = GroupMorphismStr(# G,G,id G#) by Def20;
hence thesis;
end;
end;
definition let G,H;
redefine func ZERO(G,H) -> strict Morphism of G,H;
coherence
proof
set i = ZERO(G,H);
A1: dom(i) = G & cod(i) = H & fun(i) = ZeroMap(G,H) by Lm1;
ZeroMap(G,H) is additive by Th16;
hence thesis by A1,Th19;
end;
end;
theorem
Th22: for F being Morphism of G,H ex f being map of G,H
st the GroupMorphismStr of F = GroupMorphismStr(# G,H,f#) &
f is additive
proof
let F be Morphism of G,H;
A1: the Dom of F = dom(F) by Def14
.= G by Def19;
A2: the Cod of F = cod(F) by Def15
.= H by Def19;
then reconsider f = the Fun of F as map of G,H by A1;
take f;
thus thesis by A1,A2,Th18;
end;
theorem
Th23: for F being strict Morphism of G,H ex f being map of G,H
st F = GroupMorphismStr(# G,H,f#)
proof
let F be strict Morphism of G,H;
consider f being map of G,H such that
A1: F = GroupMorphismStr(# G,H,f#) & f is additive by Th22;
take f;
thus thesis by A1;
end;
theorem
Th24: for F being GroupMorphism ex G,H st F is Morphism of G,H
proof
let F be GroupMorphism;
take G = the Dom of F,H = the Cod of F;
dom(F) = G & cod(F) = H by Def14,Def15;
hence thesis by Def19;
end;
theorem
for F being strict GroupMorphism ex G,H being AddGroup, f being map of G,H
st F is Morphism of G,H
& F = GroupMorphismStr(# G,H,f#)
& f is additive
proof
let F be strict GroupMorphism;
consider G,H such that
A1: F is Morphism of G,H by Th24;
reconsider F' = F as Morphism of G,H by A1;
consider f being map of G,H such that
A2: F' = GroupMorphismStr(# G,H,f#) & f is additive by Th22;
take G,H,f;
thus thesis by A2;
end;
theorem
Th26: for g,f being GroupMorphism st dom(g) = cod(f)
ex G1,G2,G3 being AddGroup st g is Morphism of G2,G3
& f is Morphism of G1,G2
proof
defpred P[GroupMorphism,GroupMorphism] means dom($1) = cod($2);
let g,f be GroupMorphism such that
A1: P[g,f];
consider G2,G3 being AddGroup such that
A2: g is Morphism of G2,G3 by Th24;
A3: G2 = dom(g) by A2,Def19;
consider G1,G2' being AddGroup such that
A4: f is Morphism of G1,G2' by Th24;
G2' = cod(f) by A4,Def19;
hence thesis by A1,A2,A3,A4;
end;
definition let G,F be GroupMorphism;
assume A1: dom(G) = cod(F);
func G*F -> strict GroupMorphism means
:Def21: for G1,G2,G3 being AddGroup,
g being map of G2,G3, f being map of G1,G2
st the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#) &
the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#)
holds it = GroupMorphismStr(# G1,G3,g*f#);
existence
proof
consider G1',G2',G3' being AddGroup such that
A2: G is Morphism of G2',G3' and
A3: F is Morphism of G1',G2' by A1,Th26;
consider g' being map of G2',G3' such that
A4: the GroupMorphismStr of G = GroupMorphismStr(# G2',G3',g'#)and
A5: g' is additive by A2,Th22;
consider f' being map of G1',G2' such that
A6: the GroupMorphismStr of F = GroupMorphismStr(# G1',G2',f'#)and
A7: f' is additive by A3,Th22;
g'*f' is additive by A5,A7,Th14;
then reconsider T' = (GroupMorphismStr(# G1',G3',g'*f'#))
as strict GroupMorphism by Th20;
take T';
thus thesis by A4,A6;
end;
uniqueness
proof
let S1,S2 be strict GroupMorphism such that
A8: for G1,G2,G3 being AddGroup,
g being map of G2,G3, f being map of G1,G2
st the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#) &
the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#)
holds S1 = GroupMorphismStr(# G1,G3,g*f#)and
A9: for G1,G2,G3 being AddGroup,
g being map of G2,G3, f being map of G1,G2
st the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#) &
the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#)
holds S2 = GroupMorphismStr(# G1,G3,g*f#);
consider G2',G3' being AddGroup such that
A10: G is Morphism of G2',G3' by Th24;
reconsider G' = G as Morphism of G2',G3' by A10;
A11: G2' = dom(G) by A10,Def19;
consider G1',G2'' being AddGroup such that
A12: F is Morphism of G1',G2'' by Th24;
reconsider F' = F as Morphism of G1',G2'' by A12;
reconsider F' as Morphism of G1',G2' by A1,A11,Def19;
consider g' being map of G2',G3' such that
A13: the GroupMorphismStr of G' = GroupMorphismStr(# G2',G3',g'#)
and g' is additive by Th22;
consider f' being map of G1',G2' such that
A14: the GroupMorphismStr of F' = GroupMorphismStr(# G1',G2',f'#)
and f' is additive by Th22;
thus S1 = (GroupMorphismStr(# G1',G3',g'*f'#)) by A8,A13,A14
.= S2 by A9,A13,A14;
end;
end;
canceled;
theorem
Th28: for G1,G2,G3 being AddGroup,
G being Morphism of G2,G3,
F being Morphism of G1,G2
holds G*F is Morphism of G1,G3
proof
let G1,G2,G3 be AddGroup,
G be Morphism of G2,G3, F be Morphism of G1,G2;
consider g being map of G2,G3 such that
A1: the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#)
and g is additive by Th22;
consider f being map of G1,G2 such that
A2: the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#)
and f is additive by Th22;
dom(G) = G2 by Def19
.= cod(F) by Def19;
then G*F = GroupMorphismStr(# G1,G3,g*f#) by A1,A2,Def21;
then dom(G*F) = G1 & cod(G*F) = G3 by Def14,Def15;
hence thesis by Def19;
end;
definition let G1,G2,G3 be AddGroup,
G be Morphism of G2,G3,
F be Morphism of G1,G2;
redefine func G*F -> strict Morphism of G1,G3;
coherence by Th28;
end;
theorem
Th29: for G1,G2,G3 being AddGroup,
G being Morphism of G2,G3,
F being Morphism of G1,G2,
g being map of G2,G3, f being map of G1,G2
st G = GroupMorphismStr(# G2,G3,g#) & F = GroupMorphismStr(# G1,G2,f#)
holds G*F = GroupMorphismStr(# G1,G3,g*f#)
proof
let G1,G2,G3 be AddGroup,
G be Morphism of G2,G3, F be Morphism of G1,G2,
g be map of G2,G3, f be map of G1,G2 such that
A1: G = GroupMorphismStr(# G2,G3,g#) & F = GroupMorphismStr(# G1,G2,f#);
dom(G) = G2 by Def19
.= cod(F) by Def19;
hence thesis by A1,Def21;
end;
theorem
Th30: for f,g being strict GroupMorphism st dom g = cod f holds
ex G1,G2,G3 being AddGroup,
f0 being map of G1,G2, g0 being map of G2,G3
st f = GroupMorphismStr(# G1,G2,f0#)
& g = GroupMorphismStr(# G2,G3,g0#)
& g*f = GroupMorphismStr(# G1,G3,g0*f0#)
proof
let f,g be strict GroupMorphism such that
A1: dom g = cod f;
set G1 = dom f,G2 = cod f, G3 = cod g;
reconsider f' = f as strict Morphism of G1,G2 by Def19;
reconsider g' = g as strict Morphism of G2,G3 by A1,Def19;
consider f0 being map of G1,G2 such that
A2: f' = GroupMorphismStr(# G1,G2,f0#) by Th23;
consider g0 being map of G2,G3 such that
A3: g' = GroupMorphismStr(# G2,G3,g0#) by Th23;
take G1,G2,G3,f0,g0;
thus thesis by A2,A3,Th29;
end;
theorem
Th31: for f,g being strict GroupMorphism st dom g = cod f holds
dom(g*f) = dom f & cod (g*f) = cod g
proof
let f,g be strict GroupMorphism; assume
dom g = cod f;
then consider G1,G2,G3 being AddGroup,
f0 being map of G1,G2, g0 being map of G2,G3 such that
A1: f = GroupMorphismStr(# G1,G2,f0#)
& g = GroupMorphismStr(# G2,G3,g0#)
& g*f = GroupMorphismStr(# G1,G3,g0*f0#) by Th30;
thus dom(g*f) = G1 by A1,Def14
.= dom f by A1,Def14;
thus cod(g*f) = G3 by A1,Def15
.= cod g by A1,Def15;
end;
theorem
Th32: for G1,G2,G3,G4 being AddGroup, f being strict Morphism of G1,G2,
g being strict Morphism of G2,G3,
h being strict Morphism of G3,G4
holds h*(g*f) = (h*g)*f
proof
let G1,G2,G3,G4 be AddGroup, f be strict Morphism of G1,G2,
g be strict Morphism of G2,G3, h be strict Morphism of G3,G4;
consider f0 being map of G1,G2 such that
A1: f = GroupMorphismStr(# G1,G2,f0#) by Th23;
consider g0 being map of G2,G3 such that
A2: g = GroupMorphismStr(# G2,G3,g0#) by Th23;
consider h0 being map of G3,G4 such that
A3: h = GroupMorphismStr(# G3,G4,h0#) by Th23;
A4: g*f = GroupMorphismStr(# G1,G3,g0*f0#) by A1,A2,Th29;
A5: h*g = GroupMorphismStr(# G2,G4,h0*g0#) by A2,A3,Th29;
h*(g*f) = GroupMorphismStr(# G1,G4,h0*(g0*f0)#) by A3,A4,Th29
.= GroupMorphismStr(# G1,G4,(h0*g0)*f0#) by RELAT_1:55
.= (h*g)*f by A1,A5,Th29;
hence thesis;
end;
theorem
Th33: for f,g,h being strict GroupMorphism
st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f
proof
let f,g,h be strict GroupMorphism such that
A1: dom h = cod g & dom g = cod f;
set G2 = cod f, G3 = cod g;
reconsider f' = f as Morphism of (dom f),G2 by Def19;
reconsider g' = g as Morphism of G2,G3 by A1,Def19;
reconsider h' = h as Morphism of G3,(cod h) by A1,Def19;
h'*(g'*f') = (h'*g')*f' by Th32;
hence thesis;
end;
theorem
Th34: dom ID(G) = G
& cod ID(G) = G
& (for f being strict GroupMorphism st cod f = G holds (ID G)*f = f)
& (for g being strict GroupMorphism st dom g = G holds g*(ID G) = g)
proof
set i = ID G;
thus dom i = G by Def19;
thus cod i = G by Def19;
thus for f being strict GroupMorphism st cod f = G holds i*f = f
proof
let f be strict GroupMorphism such that
A1: cod f = G;
set H = dom(f);
reconsider f' = f as Morphism of H,G by A1,Def19;
A2: dom(i) = G by Def19;
A3: i = GroupMorphismStr(# G,G,id G#) by Def20;
consider m being map of H,G such that
A4: f' = GroupMorphismStr(# H,G,m#) by Th23;
(id G)*m = m by Th12;
hence i*f = f by A1,A2,A3,A4,Def21;
end;
thus for g being strict GroupMorphism st dom g = G holds g*(ID G) = g
proof
let f be strict GroupMorphism such that
A5: dom f = G;
set H = cod(f);
reconsider f' = f as Morphism of G,H by A5,Def19;
A6: cod(i) = G by Def19;
A7: i = GroupMorphismStr(# G,G,id G#) by Def20;
consider m being map of G,H such that
A8: f' = GroupMorphismStr(# G,H,m#) by Th23;
m*(id G) = m by Th12;
hence f*i = f by A5,A6,A7,A8,Def21;
end;
end;
:: 2. Domains of groups
definition let IT be set;
attr IT is Group_DOMAIN-like means
:Def22: for x being set st x in IT holds x is strict AddGroup;
end;
definition
cluster Group_DOMAIN-like non empty set;
existence
proof
set D = {L_Trivial};
A1: for x be set st x in D holds x is strict AddGroup by TARSKI:def 1;
take D;
thus thesis by A1,Def22;
end;
end;
definition
mode Group_DOMAIN is Group_DOMAIN-like non empty set;
end;
reserve V for Group_DOMAIN;
definition let V;
redefine mode Element of V -> AddGroup;
coherence by Def22;
end;
definition let V;
cluster strict Element of V;
existence
proof consider v being Element of V;
v is strict AddGroup by Def22;
hence thesis;
end;
end;
:: 3. Domains of morphisms
definition let IT be set;
attr IT is GroupMorphism_DOMAIN-like means
:Def23: for x being set st x in IT holds x is strict GroupMorphism;
end;
definition
cluster GroupMorphism_DOMAIN-like non empty set;
existence
proof
consider G;
take {ID G};
for x being set st x in {ID G} holds x is strict GroupMorphism
by TARSKI:def 1;
hence thesis by Def23;
end;
end;
definition
mode GroupMorphism_DOMAIN is GroupMorphism_DOMAIN-like non empty set;
end;
definition let M be GroupMorphism_DOMAIN;
redefine mode Element of M -> GroupMorphism;
coherence by Def23;
end;
definition let M be GroupMorphism_DOMAIN;
cluster strict Element of M;
existence
proof consider m being Element of M;
m is strict GroupMorphism by Def23;
hence thesis;
end;
end;
canceled 2;
theorem
Th37: for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN
proof
let f be strict GroupMorphism;
for x being set st x in {f} holds x is strict GroupMorphism by TARSKI:def
1
;
hence thesis by Def23;
end;
definition let G,H;
mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means
:Def24: for x being Element of it holds x is strict Morphism of G,H;
existence
proof
reconsider D = {ZERO(G,H)} as GroupMorphism_DOMAIN by Th37;
take D;
thus thesis by TARSKI:def 1;
end;
end;
theorem
Th38: D is GroupMorphism_DOMAIN of G,H
iff for x being Element of D holds x is strict Morphism of G,H
proof
thus D is GroupMorphism_DOMAIN of G,H
implies for x being Element of D holds x is strict Morphism of G,H
by Def24;
thus (for x being Element of D holds x is strict Morphism of G,H)
implies D is GroupMorphism_DOMAIN of G,H
proof
assume A1: for x being Element of D holds x is strict Morphism of G,H;
then for x being set st x in D holds x is strict GroupMorphism;
then reconsider D' = D as GroupMorphism_DOMAIN by Def23;
for x being Element of D' holds x is strict Morphism of G,H by A1;
hence thesis by Def24;
end;
end;
theorem
for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H
proof
let f be strict Morphism of G,H;
for x being Element of {f} holds x is strict Morphism of G,H
by TARSKI:def 1;
hence thesis by Th38;
end;
definition let G,H be 1-sorted;
mode MapsSet of G,H means
:Def25: for x being set st x in it holds x is map of G,H;
existence
proof take {};
thus thesis;
end;
end;
definition let G,H be 1-sorted;
func Maps(G,H) -> MapsSet of G,H equals
:Def26: Funcs(the carrier of G, the carrier of H);
coherence
proof let x be set;
assume x in Funcs(the carrier of G, the carrier of H);
then x is Function of the carrier of G, the carrier of H by FUNCT_2:121;
hence thesis;
end;
end;
definition let G be 1-sorted, H be non empty 1-sorted;
cluster Maps(G,H) -> non empty;
coherence
proof Maps(G,H) = Funcs(the carrier of G, the carrier of H) by Def26;
hence thesis;
end;
end;
definition let G be 1-sorted, H be non empty 1-sorted;
cluster non empty MapsSet of G,H;
existence
proof Maps(G,H) is non empty;
hence thesis;
end;
end;
definition let G be 1-sorted, H be non empty 1-sorted;
let M be non empty MapsSet of G,H;
redefine mode Element of M -> map of G,H;
coherence by Def25;
end;
definition let G,H;
func Morphs(G,H) -> GroupMorphism_DOMAIN of G,H means
:Def27: x in it iff x is strict Morphism of G,H;
existence
proof
set D = { GroupMorphismStr(# G,H,f#) where f is Element of
Maps(G,H) : f is additive };
ZeroMap(G,H) is Element of
Funcs(the carrier of G, the carrier of H) by FUNCT_2:11;
then reconsider f0 = ZeroMap(G,H) as Element of Maps(G,H) by Def26;
f0 is additive by Th16;
then GroupMorphismStr(# G,H,f0#) in D;
then reconsider D as non empty set;
A1: x in D implies x is strict Morphism of G,H
proof
assume x in D;
then ex f being Element of
Maps(G,H) st x = GroupMorphismStr (# G,H,f#) & f is additive;
hence thesis by Th20;
end;
then A2: for x being Element of D holds x is strict Morphism of G,H;
A3: x is strict Morphism of G,H implies x in D
proof
assume x is strict Morphism of G,H;
then reconsider x as strict Morphism of G,H;
dom(x) = G & cod(x) = H by Def19;
then A4: the Dom of x = G & the Cod of x = H by Def14,Def15;
A5: (the Fun of x) is additive by Th18;
reconsider f = the Fun of x as map of G,H by A4;
f is Element of Funcs(the carrier of G, the carrier of H)
by FUNCT_2:11;
then reconsider g = f as Element of Maps(G,H) by Def26;
x = GroupMorphismStr(# G,H,g #) by A4;
hence thesis by A5;
end;
reconsider D as GroupMorphism_DOMAIN of G,H by A2,Th38;
take D;
thus thesis by A1,A3;
end;
uniqueness
proof
let D1,D2 be GroupMorphism_DOMAIN of G,H such that
A6: x in D1 iff x is strict Morphism of G,H and
A7: x in D2 iff x is strict Morphism of G,H;
x in D1 iff x in D2
proof
thus x in D1 implies x in D2
proof
assume x in D1;
then x is strict Morphism of G,H by A6;
hence thesis by A7;
end;
thus x in D2 implies x in D1
proof
assume x in D2;
then x is strict Morphism of G,H by A7;
hence thesis by A6;
end;
end;
hence thesis by TARSKI:2;
end;
end;
definition let G,H; let M be GroupMorphism_DOMAIN of G,H;
redefine mode Element of M -> Morphism of G,H;
coherence by Def24;
end;
definition let G,H; let M be GroupMorphism_DOMAIN of G,H;
cluster strict Element of M;
existence
proof consider m being Element of M;
m is strict Morphism of G,H by Def24;
hence thesis;
end;
end;
:: 4a. Category of groups - objects
definition let x,y;
pred GO x,y means
:Def28: ex x1,x2,x3,x4 being set st x = [x1,x2,x3,x4] &
ex G being strict AddGroup
st y = G
& x1 = the carrier of G
& x2 = the add of G
& x3 = comp G
& x4 = the Zero of G;
end;
theorem
Th40: for x,y1,y2 being set st GO x,y1 & GO x,y2 holds y1 = y2
proof
let x,y1,y2 be set such that
A1: GO x,y1 and
A2: GO x,y2;
consider a1,a2,a3,a4 being set such that
A3: x = [a1,a2,a3,a4]and
A4: ex G being strict AddGroup st y1 = G
& a1 = the carrier of G
& a2 = the add of G
& a3 = comp G
& a4 = the Zero of G by A1,Def28;
consider b1,b2,b3,b4 being set such that
A5: x = [b1,b2,b3,b4]and
A6: ex G being strict AddGroup st y2 = G
& b1 = the carrier of G
& b2 = the add of G
& b3 = comp G
& b4 = the Zero of G by A2,Def28;
consider G1 being strict AddGroup such that
A7: y1 = G1
& a1 = the carrier of G1
& a2 = the add of G1
& a3 = comp G1
& a4 = the Zero of G1 by A4;
consider G2 being strict AddGroup such that
A8: y2 = G2
& b1 = the carrier of G2
& b2 = the add of G2
& b3 = comp G2
& b4 = the Zero of G2 by A6;
the carrier of G1 = the carrier of G2
& the add of G1 = the add of G2
& comp G1 = comp G2
& the Zero of G1 = the Zero of G2 by A3,A5,A7,A8,MCART_1:33;
hence thesis by A7,A8;
end;
theorem
Th41: ex x st x in UN & GO x,L_Trivial
proof
reconsider u = {} as Element of UN by CLASSES2:62;
set x1 = {u};
Extract {} = u by ALGSTR_1:def 3;
then reconsider x4 = Extract {} as Element of UN;
reconsider x3 = comp L_Trivial as Element of UN by Th6,Th13;
reconsider x2 = op2 as Element of UN by Th6;
set x = [x1,x2,x3,x4];
A1: x is Element of UN by Th3;
take x;
thus thesis by A1,Def28,ALGSTR_1:def 4;
end;
definition let UN;
func GroupObjects(UN) -> set means
:Def29: for y holds y in it iff ex x st x in UN & GO x,y;
existence
proof
defpred P[set,set] means GO $1,$2;
A1: for x,y1,y2 being set st P[x,y1] & P[x,y2] holds y1 = y2 by Th40;
consider Y being set such that
A2: for y holds y in Y iff ex x st x in UN & P[x,y] from Fraenkel(A1);
take Y;
thus thesis by A2;
end;
uniqueness
proof
defpred P[set] means ex x st x in UN & GO x,$1;
for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
hence thesis;
end;
end;
theorem
Th42: L_Trivial in GroupObjects(UN)
proof
ex x st x in UN & GO x,L_Trivial by Th41;
hence thesis by Def29;
end;
definition let UN;
cluster GroupObjects(UN) -> non empty;
coherence by Th42;
end;
theorem
Th43: for x being Element of GroupObjects(UN) holds x is strict AddGroup
proof
let x be Element of GroupObjects(UN);
consider u being set such that
A1: u in UN & GO u,x by Def29;
ex x1,x2,x3,x4 being set st
u = [x1,x2,x3,x4] & ex G being strict AddGroup
st x = G
& x1 = the carrier of G
& x2 = the add of G
& x3 = comp G
& x4 = the Zero of G by A1,Def28;
hence thesis;
end;
definition let UN;
cluster GroupObjects(UN) -> Group_DOMAIN-like;
coherence
proof
for x being set st x in GroupObjects(UN) holds x is strict AddGroup
by Th43;
hence thesis by Def22;
end;
end;
:: 4b. Category of groups - morphisms
definition let V;
func Morphs(V) -> GroupMorphism_DOMAIN means
:Def30: for x holds x in it iff ex G,H being strict Element of V
st x is strict Morphism of G,H;
existence
proof
consider G0,H0 being strict Element of V;
set M = Morphs(G0,H0), S = { Morphs(G,H) where
G is strict Element of V, H is strict Element of V :
not contradiction };
A1: (ZERO(G0,H0)) is Element of M by Def27;
M in S;
then reconsider T = union S as non empty set by A1,TARSKI:def 4;
A2: for x holds x in T iff ex G,H being strict Element of V
st x is strict Morphism of G,H
proof
let x;
thus x in T implies ex G,H being strict Element of V
st x is strict Morphism of G,H
proof
assume x in T;
then consider Y being set such that
A3: x in Y and
A4: Y in S by TARSKI:def 4;
consider G,H being strict Element of V such that
A5: Y = Morphs(G,H) by A4;
take G,H;
thus thesis by A3,A5,Def27;
end;
thus (ex G,H being strict Element of V
st x is strict Morphism of G,H) implies x in T
proof
given G,H being strict Element of V such that
A6: x is strict Morphism of G,H;
set M = Morphs(G,H);
A7: x in M by A6,Def27;
M in S;
hence thesis by A7,TARSKI:def 4;
end;
end;
now let x be set;
assume x in T;
then ex G,H being strict Element of V st
x is strict Morphism of G,H by A2;
hence x is strict GroupMorphism;end;
then reconsider T' = T as GroupMorphism_DOMAIN by Def23;
take T';
thus thesis by A2;
end;
uniqueness
proof
let D1,D2 be GroupMorphism_DOMAIN such that
A8: for x holds x in D1 iff ex G,H being strict Element of V
st x is strict Morphism of G,H and
A9: for x holds x in D2 iff ex G,H being strict Element of V
st x is strict Morphism of G,H;
now let x;
x in D1 iff
ex G,H being strict Element of V st x is strict Morphism of G,H
by A8;
hence x in D1 iff x in D2 by A9;end;
hence thesis by TARSKI:2;
end;
end;
::
:: 4c. Category of groups - dom,cod,id
::
definition let V; let F be Element of Morphs(V);
redefine func dom(F) -> strict Element of V;
coherence
proof
consider G,H being strict Element of V such that
A1: F is strict Morphism of G,H by Def30;
reconsider F' = F as Morphism of G,H by A1;
dom(F') = G by Def19;
hence thesis;
end;
func cod(F) -> strict Element of V;
coherence
proof
consider G,H being strict Element of V such that
A2: F is strict Morphism of G,H by Def30;
reconsider F' = F as Morphism of G,H by A2;
cod(F') = H by Def19;
hence thesis;
end;
end;
definition let V; let G be Element of V;
func ID(G) -> strict Element of Morphs(V) equals
:Def31: ID(G);
coherence
proof
reconsider G' = G as strict Element of V by Def22;
ID(G') is strict Element of Morphs(V) by Def30;
hence thesis;
end;
end;
definition let V;
func dom(V) -> Function of Morphs(V),V means
:Def32: for f being Element of Morphs(V) holds it.f = dom(f);
existence
proof
deffunc F(Element of Morphs(V)) = dom $1;
consider F being Function of Morphs(V),V such that
A1: for f being Element of Morphs(V) holds F.f = F(f) from LambdaD;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be Function of Morphs(V),V such that
A2: for f being Element of Morphs(V) holds F1.f = dom(f) and
A3: for f being Element of Morphs(V) holds F2.f = dom(f);
now let f be Element of Morphs(V);
F1.f = dom(f) by A2;
hence F1.f = F2.f by A3;end;
hence thesis by FUNCT_2:113;
end;
func cod(V) -> Function of Morphs(V),V means
:Def33: for f being Element of Morphs(V) holds it.f = cod(f);
existence
proof
deffunc F(Element of Morphs(V)) = cod $1;
consider F being Function of Morphs(V),V such that
A4: for f being Element of Morphs(V) holds F.f = F(f) from LambdaD;
take F;
thus thesis by A4;
end;
uniqueness
proof
let F1,F2 be Function of Morphs(V),V such that
A5: for f being Element of Morphs(V) holds F1.f = cod(f) and
A6: for f being Element of Morphs(V) holds F2.f = cod(f);
now let f be Element of Morphs(V);
F1.f = cod(f) by A5;
hence F1.f = F2.f by A6;end;
hence thesis by FUNCT_2:113;
end;
func ID(V) -> Function of V,Morphs(V) means
:Def34: for G being Element of V holds it.G = ID(G);
existence
proof
deffunc F(Element of V) = ID $1;
consider F being Function of V,Morphs(V) such that
A7: for G being Element of V holds F.G = F(G) from LambdaD;
take F;
thus thesis by A7;
end;
uniqueness
proof
let F1,F2 be Function of V,Morphs(V) such that
A8: for G being Element of V holds F1.G = ID(G) and
A9: for G being Element of V holds F2.G = ID(G);
now let G be Element of V;
F1.G = ID(G) by A8;
hence F1.G = F2.G by A9;end;
hence thesis by FUNCT_2:113;
end;
end;
::
:: 4d. Category of groups - superposition
::
theorem
Th44: for g,f being Element of Morphs(V) st dom(g) = cod(f)
ex G1,G2,G3 being strict Element of V st g is Morphism of G2,G3
& f is Morphism of G1,G2
proof
set X = Morphs(V);
defpred P[Element of X,Element of X] means dom($1) = cod($2);
let g,f be Element of X such that
A1: P[g,f];
consider G2,G3 being strict Element of V such that
A2: g is strict Morphism of G2,G3 by Def30;
A3: G2 = dom(g) by A2,Def19;
consider G1,G2' being strict Element of V such that
A4: f is strict Morphism of G1,G2' by Def30;
G2' = cod(f) by A4,Def19;
hence thesis by A1,A2,A3,A4;
end;
theorem
Th45: for g,f being Element of Morphs(V) st dom(g) = cod(f)
holds g*f in Morphs(V)
proof
set X = Morphs(V);
defpred P[Element of X,Element of X] means dom($1) = cod($2);
let g,f be Element of X; assume
P[g,f];
then consider G1,G2,G3 being strict Element of V such that
A1: g is Morphism of G2,G3 & f is Morphism of G1,G2 by Th44;
reconsider g' = g as Morphism of G2,G3 by A1;
reconsider f' = f as Morphism of G1,G2 by A1;
g'*f' is Morphism of G1,G3;
hence thesis by Def30;
end;
definition let V;
func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means
:Def35:
(for g,f being Element of Morphs(V) holds [g,f] in dom it iff dom(g) = cod(f))
& (for g,f being Element of Morphs(V) st [g,f] in dom it
holds it.[g,f] = g*f);
existence
proof
set X = Morphs(V);
defpred P[Element of X,Element of X] means dom($1) = cod($2);
deffunc F(Element of X,Element of X) = $1*$2;
A1: for g,f being Element of X st P[g,f] holds F(g,f) in X by Th45;
consider c being PartFunc of [:X,X:],X such that
A2: for g,f being Element of X holds [g,f] in dom c iff P[g,f] and
A3: for g,f being Element of X st [g,f] in dom c
holds c.[g,f] = F(g,f) from PartLambda2D(A1);
take c;
thus thesis by A2,A3;
end;
uniqueness
proof
set X = Morphs(V);
defpred P[Element of X,Element of X] means dom($1) = cod($2);
let c1,c2 be PartFunc of [:X,X:],X such that
A4: for g,f being Element of X holds [g,f] in dom c1 iff P[g,f] and
A5: for g,f being Element of X st [g,f] in dom c1
holds c1.[g,f] = g*f and
A6: for g,f being Element of X holds [g,f] in dom c2 iff P[g,f] and
A7: for g,f being Element of X st [g,f] in dom c2
holds c2.[g,f] = g*f;
A8: dom c1 c= [:X,X:] & dom c2 c= [:X,X:] by RELSET_1:12;
A9: dom c1 = dom c2
proof
now let x; assume
A10: x in dom c1;
then consider g,f being Element of X such that
A11: x = [g,f] by A8,Th2;
P[g,f] by A4,A10,A11;
hence x in dom c2 by A6,A11;end;
then A12: dom c1 c= dom c2 by TARSKI:def 3;
now let x; assume
A13: x in dom c2;
then consider g,f being Element of X such that
A14: x = [g,f] by A8,Th2;
P[g,f] by A6,A13,A14;
hence x in dom c1 by A4,A14;end;
then dom c2 c= dom c1 by TARSKI:def 3;
hence thesis by A12,XBOOLE_0:def 10;
end;
set V' = dom c1;
for x,y st [x,y] in V' holds c1.[x,y]=c2.[x,y]
proof
let x,y;assume
A15: [x,y] in V';
then reconsider x,y as Element of X by A8,ZFMISC_1:106;
c1.[x,y] = x*y by A5,A15;
hence thesis by A7,A9,A15;
end;
hence thesis by A9,PARTFUN1:35;
end;
end;
::
:: 4e. Definition of Category of groups
::
definition let UN;
func GroupCat(UN) -> CatStr equals
:Def36: CatStr(# GroupObjects(UN),Morphs(GroupObjects(UN)),
dom(GroupObjects(UN)),cod(GroupObjects(UN)),
comp(GroupObjects(UN)),ID(GroupObjects(UN))#);
coherence;
end;
definition let UN;
cluster GroupCat(UN) -> strict;
coherence
proof
GroupCat UN = CatStr(# GroupObjects(UN),Morphs(GroupObjects(UN)),
dom(GroupObjects(UN)),cod(GroupObjects(UN)),
comp(GroupObjects(UN)),ID(GroupObjects(UN))#) by Def36;
hence thesis;
end;
end;
theorem
Th46: for f,g being Morphism of GroupCat(UN) holds
[g,f] in dom(the Comp of GroupCat(UN)) iff dom g = cod f
proof
set C = GroupCat(UN), V = GroupObjects(UN);
A1: C = CatStr(# V,Morphs(V),dom(V),cod(V),comp(V),ID(V)#) by Def36;
let f,g be Morphism of C;
reconsider f' = f as Element of Morphs(V) by A1;
reconsider g' = g as Element of Morphs(V) by A1;
A2: dom g = dom(V).g' by A1,CAT_1:def 2
.= dom(g') by Def32;
cod f = cod(V).f' by A1,CAT_1:def 3
.= cod(f') by Def33;
hence thesis by A1,A2,Def35;
end;
theorem
Th47: for f being (Morphism of GroupCat(UN)),
f' being Element of Morphs(GroupObjects(UN)),
b being Object of GroupCat(UN),
b' being Element of GroupObjects(UN)
holds f is strict Element of Morphs(GroupObjects(UN))
& f' is Morphism of GroupCat(UN)
& b is strict Element of GroupObjects(UN)
& b' is Object of GroupCat(UN)
proof
set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V);
A1: C = CatStr(# V,X,dom(V),cod(V),comp(V),ID(V)#) by Def36;
let f be (Morphism of C),
f' be Element of X,
b be Object of C,
b' be Element of V;
ex G,H being strict Element of V st f is strict Morphism of G,H
by A1,Def30;
hence f is strict Element of X by A1;
thus f' is Morphism of C by A1;
consider x such that
A2: x in UN & GO x,b by A1,Def29;
ex x1,x2,x3,x4 being set st
x = [x1,x2,x3,x4] &
ex G being strict AddGroup
st b = G
& x1 = the carrier of G
& x2 = the add of G
& x3 = comp G
& x4 = the Zero of G by A2,Def28;
hence b is strict Element of V by A1;
thus b' is Object of C by A1;
end;
theorem
Th48: for b being Object of GroupCat(UN),
b' being Element of GroupObjects(UN)
st b = b' holds id b = ID(b')
proof
set C = GroupCat(UN), V = GroupObjects(UN);
A1: C = CatStr(# V,(Morphs(V)),dom(V),cod(V),comp(V),ID(V)#) by Def36;
let b be Object of C, b' be Element of V; assume
b = b';
hence id b = (ID(V)).b' by A1,CAT_1:def 5
.= ID(b') by Def34;
end;
theorem
Th49: for f being Morphism of GroupCat(UN)
for f' being Element of Morphs(GroupObjects(UN))
st f = f'
holds dom f = dom f'
& cod f = cod f'
proof
set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V);
A1: C = CatStr(# V,X,dom(V),cod(V),comp(V),ID(V)#) by Def36;
let f be (Morphism of C), f' be Element of X; assume
A2: f = f';
hence dom f = dom(V).f' by A1,CAT_1:def 2
.= dom f' by Def32;
thus cod f = cod(V).f' by A1,A2,CAT_1:def 3
.= cod f' by Def33;
end;
theorem
Th50: for f,g being (Morphism of GroupCat(UN)),
f',g' being Element of Morphs(GroupObjects(UN))
st f = f' & g = g'
holds (dom g = cod f iff dom g' = cod f')
& (dom g = cod f iff [g',f'] in dom comp(GroupObjects(UN)))
& (dom g = cod f implies g*f = g'*f')
& (dom f = dom g iff dom f' = dom g')
& (cod f = cod g iff cod f' = cod g')
proof
set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V);
A1: C = CatStr(# V,X,dom(V),cod(V),comp(V),ID(V)#) by Def36;
let f,g be Morphism of C;
let f',g' be Element of X; assume
A2: f = f' & g = g';
then A3: dom g = dom g' by Th49;
A4: cod f = cod f' by A2,Th49;
A5: dom f = dom f' by A2,Th49;
A6: cod g = cod g' by A2,Th49;
thus dom g = cod f iff dom g' = cod f' by A2,A4,Th49;
thus A7: dom g = cod f iff [g',f'] in dom comp(V) by A3,A4,Def35;
thus dom g = cod f implies g*f = g'*f'
proof
assume A8: dom g = cod f;
then [g,f] in dom (the Comp of C) by Th46;
hence g*f = (comp(V)).[g',f'] by A1,A2,CAT_1:def 4
.= g'*f' by A7,A8,Def35;
end;
thus dom f = dom g iff dom f' = dom g' by A2,A5,Th49;
thus cod f = cod g iff cod f' = cod g' by A2,A6,Th49;
end;
Lm2: for f,g being Morphism of GroupCat(UN) st dom g = cod f holds
dom(g*f) = dom f
& cod (g*f) = cod g
proof set X = Morphs(GroupObjects(UN));
let f,g be Morphism of GroupCat(UN) such that
A1: dom g = cod f;
reconsider f' = f as strict Element of X by Th47;
reconsider g' = g as strict Element of X by Th47;
A2: dom g' = cod f' by A1,Th50;
then A3: dom(g'*f') = dom f'
& cod (g'*f') = cod g' by Th31;
reconsider gf = g'*f' as Element of X by A2,Th45;
gf = g*f by A1,Th50;
hence thesis by A3,Th50;
end;
Lm3: for f,g,h being Morphism of GroupCat(UN)
st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f
proof set X = Morphs(
(GroupObjects(UN)));
let f,g,h be Morphism of (GroupCat(UN)) such that
A1: dom h = cod g & dom g = cod f;
reconsider f'=f, g'=g, h'=h as strict Element of X by Th47;
A2: dom h' = cod g' & dom g' = cod f' by A1,Th50;
A3: g'*f' = g*f & h'*g' = h*g by A1,Th50;
reconsider gf = g'*f', hg = h'*g' as Element of X by A2,Th45;
A4: dom(h) = cod(g*f) by A1,Lm2;
A5: dom(h*g) = cod(f) by A1,Lm2;
h*(g*f) = h'*gf by A3,A4,Th50
.= hg*f' by A2,Th33
.= (h*g)*f by A3,A5,Th50;
hence thesis;
end;
Lm4: for b being Object of GroupCat(UN) holds
dom id b = b
& cod id b = b
& (for f being Morphism of GroupCat(UN)
st cod f = b holds (id b)*f = f)
& (for g being Morphism of GroupCat(UN)
st dom g = b holds g*(id b) = g)
proof
set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V);
let b be Object of C;
reconsider b' = b as Element of V by Th47;
reconsider b'' = b' as AddGroup;
A1: id b = ID(b') by Th48;
hence A2: dom id b = dom ID(b') by Th49
.= dom ID(b'') by Def31
.= b by Th34;
thus A3: cod id b = cod ID(b') by A1,Th49
.= cod ID(b'') by Def31
.= b by Th34;
thus for f being Morphism of C st cod f = b holds (id b)*f = f
proof
let f be Morphism of C such that
A4: cod f = b;
reconsider f1 = f as strict Element of X by Th47;
reconsider f' = f1 as strict GroupMorphism;
A5: cod f' = b'' by A4,Th49;
thus (id b)*f = ID(b')*f' by A1,A2,A4,Th50
.= ID(b'')*f' by Def31
.= f by A5,Th34;
end;
thus for g being Morphism of C st dom g = b holds g*(id b) = g
proof
let f be Morphism of C such that
A6: dom f = b;
reconsider f1 = f as strict Element of X by Th47;
reconsider f' = f1 as strict GroupMorphism;
A7: dom f' = b'' by A6,Th49;
thus f*(id b) = f'*ID(b') by A1,A3,A6,Th50
.= f'*ID(b'') by Def31
.= f by A7,Th34;
end;
end;
definition let UN;
cluster GroupCat(UN) -> Category-like;
coherence
proof
( for f,g being Morphism of GroupCat(UN)
holds [g,f] in dom(the Comp of GroupCat(UN)) iff dom g = cod f )
& ( for f,g being Morphism of GroupCat(UN) st dom g = cod f
holds dom(g*f) = dom f & cod (g*f) = cod g )
& ( for f,g,h being Morphism of GroupCat(UN)
st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f )
& ( for b being Object of GroupCat(UN)
holds dom id b = b & cod id b = b &
(for f being Morphism of GroupCat(UN)
st cod f = b holds (id b)*f = f) &
(for g being Morphism of GroupCat(UN)
st dom g = b holds g*(id b) = g) ) by Lm2,Lm3,Lm4,Th46;
hence thesis by CAT_1:29;
end;
end;
definition let UN;
func AbGroupObjects(UN) -> Subset of the Objects of GroupCat(UN) equals
:Def37: {G where G is Element of the Objects of GroupCat(UN)
: ex H being AbGroup st G = H};
coherence
proof
set D2 = the Objects of GroupCat(UN);
now
let x be set;
assume x in {G where G is Element of D2 : ex H being AbGroup st G = H};
then ex G being Element of D2 st x = G & ex H being AbGroup st G = H;
hence x in D2;end;
hence thesis by TARSKI:def 3;
end;
end;
theorem
Th51: L_Trivial in AbGroupObjects(UN)
proof
set D2 = the Objects of GroupCat(UN);
set T = L_Trivial;
GroupCat(UN) = CatStr(# GroupObjects(UN),Morphs(GroupObjects(UN)),
dom(GroupObjects(UN)),cod(GroupObjects(UN)),
comp(GroupObjects(UN)),ID(GroupObjects(UN))#) by Def36;
then T in D2 by Th42;
then T in {G where G is Element of D2 : ex H being AbGroup st G = H};
hence thesis by Def37;
end;
definition let UN;
cluster AbGroupObjects(UN) -> non empty;
coherence by Th51;
end;
definition let UN;
func AbGroupCat(UN) -> Subcategory of GroupCat(UN) equals
:Def38: cat(AbGroupObjects(UN));
coherence;
end;
definition let UN;
cluster AbGroupCat(UN) -> strict;
coherence
proof
AbGroupCat(UN) = cat(AbGroupObjects(UN)) by Def38;
hence thesis;
end;
end;
theorem
Th52: the Objects of AbGroupCat(UN) = AbGroupObjects(UN)
proof
AbGroupCat(UN) = cat(AbGroupObjects(UN)) by Def38;
hence thesis by Th10;
end;
:: 6. Subcategory of groups with the operator of 1/2
definition let UN;
func MidOpGroupObjects(UN) -> Subset of the Objects of AbGroupCat(UN) equals
:Def39: {G where G is Element of the Objects of AbGroupCat(UN)
: ex H being midpoint_operator AbGroup st G = H};
coherence
proof
set D2 = the Objects of AbGroupCat(UN);
now
let x be set;
assume x in {G where G is Element of D2
: ex H being midpoint_operator AbGroup st G = H};
then ex G being Element of D2 st
x = G & ex H being midpoint_operator AbGroup st G = H;
hence x in D2;end;
hence thesis by TARSKI:def 3;
end;
end;
definition let UN;
cluster MidOpGroupObjects(UN) -> non empty;
coherence
proof
set D2 = the Objects of AbGroupCat(UN);
set D1 = {G where G is Element of D2
: ex H being midpoint_operator AbGroup st G = H};
set T = L_Trivial;
D2 = AbGroupObjects(UN) by Th52;
then T in D2 by Th51;
then T in D1;
then reconsider D1 as non empty set;
now
let x be set;
assume x in D1;
then ex G being Element of D2 st
x = G & ex H being midpoint_operator AbGroup st G = H;
hence x in D2;end;
hence thesis by Def39;
end;
end;
definition let UN;
func MidOpGroupCat(UN) -> Subcategory of AbGroupCat(UN) equals
:Def40: cat(MidOpGroupObjects(UN));
coherence;
end;
definition let UN;
cluster MidOpGroupCat(UN) -> strict;
coherence
proof
MidOpGroupCat(UN) = cat(MidOpGroupObjects(UN)) by Def40;
hence thesis;
end;
end;
theorem
the Objects of MidOpGroupCat(UN) = MidOpGroupObjects(UN)
proof
MidOpGroupCat(UN) = cat(MidOpGroupObjects(UN)) by Def40;
hence thesis by Th10;
end;
theorem
L_Trivial in MidOpGroupObjects(UN)
proof
set D2 = the Objects of AbGroupCat(UN);
set T = L_Trivial;
D2 = AbGroupObjects(UN) by Th52;
then T in D2 by Th51;
then T in {G where G is Element of D2
: ex H being midpoint_operator AbGroup st G = H};
hence thesis by Def39;
end;