:: Categories of Groups
:: by Michal Muzalewski
::
:: Received October 3, 1991
:: Copyright (c) 1991-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 XBOOLE_0, CLASSES2, TARSKI, ZFMISC_1, SUBSET_1, FUNCT_5, FUNCT_1,
FUNCT_2, ALGSTR_0, MIDSP_2, ROBBINS1, SUPINF_2, ARYTM_3, ARYTM_1, CAT_1,
STRUCT_0, RELAT_1, GRAPH_1, VECTSP_1, PARTFUN1, REALSET1, MIDSP_1, CAT_2,
FUNCOP_1, MSSUBFAM, RLVECT_1, ENS_1, ALGSTR_1, GRCAT_1, MONOID_0,
RELAT_2, BINOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1,
MCART_1, REALSET1, PARTFUN1, FUNCT_2, ORDINAL1, CLASSES2, BINOP_1,
FUNCOP_1, FUNCT_5, STRUCT_0, ALGSTR_0, GRAPH_1, CAT_1, TOPS_2, RLVECT_1,
VECTSP_1, CAT_2, ALGSTR_1, MIDSP_2;
constructors PARTFUN1, CLASSES1, CLASSES2, REALSET1, TOPS_2, VECTSP_2, CAT_2,
ALGSTR_1, MIDSP_2, FUNCOP_1, RELSET_1, FUNCT_5, XTUPLE_0;
registrations XBOOLE_0, RELSET_1, FUNCT_2, CLASSES2, STRUCT_0, ALGSTR_1,
MIDSP_2, ALGSTR_0, CAT_1;
requirements SUBSET, BOOLE;
definitions VECTSP_1, CAT_1;
equalities BINOP_1, STRUCT_0, ALGSTR_1, ALGSTR_0, GRAPH_1, CAT_1, XTUPLE_0,
ORDINAL1;
expansions VECTSP_1;
theorems CAT_1, CAT_2, CLASSES2, FUNCOP_1, FUNCT_1, FUNCT_2, MIDSP_2,
VECTSP_1, TARSKI, ZFMISC_1, RLVECT_1, RELAT_1, ORDINAL1, XBOOLE_0,
TOPS_2, BINOP_1, SUBSET_1, XTUPLE_0;
schemes FUNCT_2, BINOP_1, 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;
theorem Th1:
for u1,u2,u3,u4 being Element of UN holds
[u1,u2,u3] in UN & [u1,u2,u3,u4] in UN
proof
let u1,u2,u3,u4 be Element of UN;
[u1,u2,u3] = [[u1,u2],u3] & [u1,u2,u3,u4] = [[u1,u2,u3],u4];
hence thesis by CLASSES2:58;
end;
:: 0c. Auxiliary theorems: Trivial Group
theorem Th2:
op2.({},{}) = {} & op1.{} = {} & op0 = {}
proof
[{},{}] in [:{{}},{{}}:] by ZFMISC_1:28;
hence op2.({},{}) = {} by FUNCT_2:50;
{} in {{}} by TARSKI:def 1;
hence op1.{} = {} by FUNCT_2:50;
thus thesis;
end;
theorem Th3:
{{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN
proof
set D = {{}};
thus
A1: D in UN by CLASSES2:56,57;
hence [D,D] in UN by CLASSES2:58;
A2: op2 in Funcs([:D,D:],D) by FUNCT_2:8;
thus [:D,D:] in UN by A1,CLASSES2:61;
then Funcs([:D,D:],D) in UN by A1,CLASSES2:61;
hence op2 in UN by A2,ORDINAL1:10;
A3: op1 in Funcs(D,D) by FUNCT_2:8;
Funcs(D,D) in UN by A1,CLASSES2:61;
hence thesis by A3,ORDINAL1:10;
end;
registration
cluster Trivial-addLoopStr -> midpoint_operator;
coherence
proof
set G = Trivial-addLoopStr;
A1: for a being Element of G ex x being Element of G st Double x = a
proof
set x = the Element of G;
let a be Element of G;
take x;
thus Double x = {} by TARSKI:def 1
.= a by TARSKI:def 1;
end;
for a being Element of G st Double a = 0.G holds a = 0.G by TARSKI:def 1;
hence thesis by A1,MIDSP_2:def 5;
end;
end;
theorem
(for x being Element of Trivial-addLoopStr holds x = {}) & (for x,y
being Element of Trivial-addLoopStr holds x+y = {}) & (for x being Element of
Trivial-addLoopStr holds -x = {}) & 0.Trivial-addLoopStr = {}
by TARSKI:def 1;
:: 0d. Auxiliary theorems: subcategories
reserve C for Category;
reserve O for non empty Subset of the carrier of C;
definition
let C,O;
func Morphs(O) -> Subset of the carrier' of C equals
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:19;
end;
registration
let C,O;
cluster Morphs(O) -> non empty;
coherence by CAT_2:19;
end;
definition
let C,O;
func dom(O) -> Function of Morphs(O),O equals
(the Source of C)|Morphs(O);
coherence by CAT_2:20;
func cod(O) -> Function of Morphs(O),O equals
(the Target of C)|Morphs(O);
coherence by CAT_2:20;
func comp(O) -> PartFunc of [:Morphs(O),(Morphs(O)):],Morphs(O) equals
(the Comp of C)||Morphs(O);
coherence by CAT_2:20;
::$CD
end;
definition
let C,O;
func cat(O) -> Subcategory of C equals
CatStr (# O,Morphs(O),dom(O),cod(O),comp(O)#);
coherence by CAT_2:21;
end;
registration
let C,O;
cluster cat(O) -> strict;
coherence;
end;
theorem
the carrier of cat(O) = O;
:: 1a. Maps of the carriers of groups
definition
let G be non empty 1-sorted, H be non empty ZeroStr;
func ZeroMap(G,H) -> Function of G,H equals
(the carrier of G) --> 0.H;
coherence;
end;
theorem Th6:
comp Trivial-addLoopStr = op1
proof
reconsider f = comp Trivial-addLoopStr as Function of {{}}, {{}};
for x being object st x in {{}} holds op1.x = f.x
proof
let x be object;
assume x in {{}};
then reconsider x as Element of Trivial-addLoopStr;
x = {} by TARSKI:def 1;
then op1.x = -x by Th2,TARSKI:def 1
.= f.x by VECTSP_1:def 13;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
registration
let G be non empty addMagma, H being right_zeroed non empty addLoopStr;
cluster ZeroMap(G,H) -> additive;
coherence
proof
set f = ZeroMap(G,H);
let x,y be Element of G;
A1: f.y = 0.H by FUNCOP_1:7;
f.(x+y) = 0.H & f.x = 0.H by FUNCOP_1:7;
hence thesis by A1,RLVECT_1:def 4;
end;
end;
registration
let G be non empty addMagma, H be right_zeroed non empty addLoopStr;
cluster additive for Function of G,H;
existence
proof
take ZeroMap(G,H);
thus thesis;
end;
end;
theorem Th7:
for G1,G2,G3 being non empty addMagma, f being Function of G1,
G2, g being Function of G2,G3 st f is additive & g is additive holds g*f is
additive
proof
let G1,G2,G3 be non empty addMagma, f be Function of G1,G2, g be Function
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:15;
thus h.(x+y) = g.(f.(x+y)) by FUNCT_2:15
.= g.(f.x+f.y) by A1
.= h.x+h.y by A2,A3;
end;
hence thesis;
end;
registration
let G1 be non empty addMagma,
G2,G3 be right_zeroed non empty addLoopStr,
f be additive Function of G1, G2,
g be additive Function of G2, G3;
cluster g*f -> additive for Function of G1, G3;
coherence by Th7;
end;
:: 1b. carrier of groups
reserve G,H for AddGroup;
definition
struct GroupMorphismStr (#
DomG, CodG -> AddGroup,
Fun -> Function of the DomG, the CodG #);
end;
definition
::$CD
let f be GroupMorphismStr;
func dom(f) -> AddGroup equals
the DomG of f;
coherence;
func cod(f) -> AddGroup equals
the CodG of f;
coherence;
end;
definition
let f be GroupMorphismStr;
func fun(f) -> Function of dom(f),cod(f) equals
the Fun of f;
coherence;
end;
theorem
for f being GroupMorphismStr, G1,G2 being AddGroup, f0 being Function
of G1,G2 st f = GroupMorphismStr(# G1,G2,f0#) holds dom f = G1 & cod f = G2 &
fun f = f0;
definition
let G,H;
func ZERO(G,H) -> GroupMorphismStr equals
GroupMorphismStr(# G,H,ZeroMap(G,H)#);
coherence;
end;
registration
let G,H;
cluster ZERO(G,H) -> strict;
coherence;
end;
definition
let IT be GroupMorphismStr;
attr IT is GroupMorphism-like means :Def11:
fun(IT) is additive;
end;
registration
cluster strict GroupMorphism-like for GroupMorphismStr;
existence
proof
set G = the AddGroup;
set z = ZERO(G,G);
z is GroupMorphism-like;
hence thesis;
end;
end;
definition
mode GroupMorphism is GroupMorphism-like GroupMorphismStr;
end;
theorem Th9:
for F being GroupMorphism holds the Fun of F is additive
proof
let F be GroupMorphism;
the Fun of F = fun(F);
hence thesis by Def11;
end;
registration
let G,H;
cluster ZERO(G,H) -> GroupMorphism-like;
coherence;
end;
definition
let G,H;
mode Morphism of G,H -> GroupMorphism means
:Def12:
dom(it) = G & cod(it) = H;
existence
proof
take ZERO(G,H);
thus thesis;
end;
end;
registration
let G,H;
cluster strict for Morphism of G,H;
existence
proof
dom(ZERO(G,H)) = G & cod(ZERO(G,H)) = H;
then ZERO(G,H) is Morphism of G,H by Def12;
hence thesis;
end;
end;
theorem Th10:
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 that
A1: dom(f) = G & cod(f) = H and
A2: fun(f) is additive;
reconsider f9 = f as strict GroupMorphism by A2,Def11;
f9 is strict Morphism of G,H by A1,Def12;
hence thesis;
end;
theorem Th11:
for f being Function of G,H st f is additive holds
GroupMorphismStr (# G,H,f#) is strict Morphism of G,H
proof
let f be Function of G,H such that
A1: f is additive;
set F = GroupMorphismStr (# G,H,f#);
fun(F) = f;
hence thesis by A1,Th10;
end;
registration let G be non empty addMagma;
cluster id G -> additive;
coherence
proof
set f = id G;
let x,y be Element of G;
f.(x+y) = x+y & f.x = x by FUNCT_1:18;
hence thesis by FUNCT_1:18;
end;
end;
definition
let G;
func ID G -> Morphism of G,G equals
GroupMorphismStr(# G,G,id G#);
coherence
proof
set i = GroupMorphismStr(# G,G,id G#);
fun(i) = id G;
hence thesis by Th10;
end;
end;
registration
let G;
cluster ID G -> strict;
coherence;
end;
definition
let G,H;
redefine func ZERO(G,H) -> strict Morphism of G,H; :: redefines ZERO (GRCAT_1, definition)
coherence
proof
set i = ZERO(G,H);
fun(i) = ZeroMap(G,H);
hence thesis by Th10;
end;
end;
theorem Th12:
for F being Morphism of G,H ex f being Function 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 CodG of F = cod(F) .= H by Def12;
A2: the DomG of F = dom(F) .= G by Def12;
then reconsider f = the Fun of F as Function of G,H by A1;
take f;
thus thesis by A2,A1,Th9;
end;
theorem Th13:
for F being strict Morphism of G,H ex f being Function of G,H st
F = GroupMorphismStr(# G,H,f#)
proof
let F be strict Morphism of G,H;
consider f being Function of G,H such that
A1: F = GroupMorphismStr(# G,H,f#) and
f is additive by Th12;
take f;
thus thesis by A1;
end;
theorem Th14:
for F being GroupMorphism ex G,H st F is Morphism of G,H
proof
let F be GroupMorphism;
take G = the DomG of F,H = the CodG of F;
dom(F) = G & cod(F) = H;
hence thesis by Def12;
end;
theorem
for F being strict GroupMorphism
ex G,H being AddGroup, f being Function 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 Th14;
reconsider F9 = F as Morphism of G,H by A1;
consider f being Function of G,H such that
A2: F9 = GroupMorphismStr(# G,H,f#) & f is additive by Th12;
take G,H,f;
thus thesis by A2;
end;
theorem Th16:
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 Th14;
consider G1,G29 being AddGroup such that
A3: f is Morphism of G1,G29 by Th14;
A4: G29 = cod(f) by A3,Def12;
G2 = dom(g) by A2,Def12;
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
:Def14:
for G1,G2,G3 being AddGroup,
g being Function of G2,G3, f being Function 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 G19,G29,G39 being AddGroup such that
A2: G is Morphism of G29,G39 and
A3: F is Morphism of G19,G29 by A1,Th16;
consider f9 being Function of G19,G29 such that
A4: the GroupMorphismStr of F = GroupMorphismStr(# G19,G29,f9#) and
A5: f9 is additive by A3,Th12;
consider g9 being Function of G29,G39 such that
A6: the GroupMorphismStr of G = GroupMorphismStr(# G29,G39,g9#) and
A7: g9 is additive by A2,Th12;
g9*f9 is additive by A7,A5;
then reconsider T9 = (GroupMorphismStr(# G19,G39,g9*f9#)) as strict
GroupMorphism by Th11;
take T9;
thus thesis by A6,A4;
end;
uniqueness
proof
consider G19,G299 being AddGroup such that
A8: F is Morphism of G19,G299 by Th14;
reconsider F9 = F as Morphism of G19,G299 by A8;
consider G29,G39 being AddGroup such that
A9: G is Morphism of G29,G39 by Th14;
G29 = dom(G) by A9,Def12;
then reconsider F9 as Morphism of G19,G29 by A1,Def12;
consider f9 being Function of G19,G29 such that
A10: the GroupMorphismStr of F9 = GroupMorphismStr(# G19,G29,f9#) and
f9 is additive by Th12;
reconsider G9 = G as Morphism of G29,G39 by A9;
let S1,S2 be strict GroupMorphism such that
A11: for G1,G2,G3 being AddGroup, g being Function of G2,G3, f being
Function 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
A12: for G1,G2,G3 being AddGroup, g being Function of G2,G3, f being
Function 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 g9 being Function of G29,G39 such that
A13: the GroupMorphismStr of G9 = GroupMorphismStr(# G29,G39,g9#) and
g9 is additive by Th12;
thus S1 = (GroupMorphismStr(# G19,G39,g9*f9#)) by A11,A13,A10
.= S2 by A12,A13,A10;
end;
end;
theorem Th17:
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 Function of G2,G3 such that
A1: the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#) and
g is additive by Th12;
consider f being Function of G1,G2 such that
A2: the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#) and
f is additive by Th12;
dom(G) = G2 by Def12
.= cod(F) by Def12;
then G*F = GroupMorphismStr(# G1,G3,g*f#) by A1,A2,Def14;
then dom(G*F) = G1 & cod(G*F) = G3;
hence thesis by Def12;
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; :: redefines * (GRCAT_1, definition)
coherence by Th17;
end;
theorem Th18:
for G1,G2,G3 being AddGroup,
G being Morphism of G2,G3, F being Morphism of G1,G2,
g being Function of G2,G3, f being Function 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 Function of G2,G3, f be Function of G1,G2 such that
A1: G = GroupMorphismStr(# G2,G3,g#) & F = GroupMorphismStr(# G1,G2,f#);
dom(G) = G2 by Def12
.= cod(F) by Def12;
hence thesis by A1,Def14;
end;
theorem Th19:
for f,g being strict GroupMorphism st dom g = cod f holds ex G1,
G2,G3 being AddGroup, f0 being Function of G1,G2, g0 being Function 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 f9 = f as strict Morphism of G1,G2 by Def12;
reconsider g9 = g as strict Morphism of G2,G3 by A1,Def12;
consider f0 being Function of G1,G2 such that
A2: f9 = GroupMorphismStr(# G1,G2,f0#);
consider g0 being Function of G2,G3 such that
A3: g9 = GroupMorphismStr(# G2,G3,g0#) by Th13;
take G1,G2,G3,f0,g0;
thus thesis by A2,A3,Th18;
end;
theorem Th20:
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
A1: ex G1,G2,G3 being AddGroup, f0 being Function of G1,G2, g0 being Function
of G2,G3 st f = GroupMorphismStr(# G1,G2,f0#) & g = GroupMorphismStr(# G2,G3,g0
#) & g*f = GroupMorphismStr(# G1,G3,g0*f0#) by Th19;
hence dom(g*f) = dom f;
thus thesis by A1;
end;
theorem Th21:
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 Function of G1,G2 such that
A1: f = GroupMorphismStr(# G1,G2,f0#) by Th13;
consider g0 being Function of G2,G3 such that
A2: g = GroupMorphismStr(# G2,G3,g0#) by Th13;
consider h0 being Function of G3,G4 such that
A3: h = GroupMorphismStr(# G3,G4,h0#) by Th13;
A4: h*g = GroupMorphismStr(# G2,G4,h0*g0#) by A2,A3,Th18;
g*f = GroupMorphismStr(# G1,G3,g0*f0#) by A1,A2,Th18;
then h*(g*f) = GroupMorphismStr(# G1,G4,h0*(g0*f0)#) by A3,Th18
.= GroupMorphismStr(# G1,G4,(h0*g0)*f0#) by RELAT_1:36
.= (h*g)*f by A1,A4,Th18;
hence thesis;
end;
theorem Th22:
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 and
A2: dom g = cod f;
set G2 = cod f, G3 = cod g;
reconsider h9 = h as Morphism of G3,(cod h) by A1,Def12;
reconsider g9 = g as Morphism of G2,G3 by A2,Def12;
reconsider f9 = f as Morphism of (dom f),G2 by Def12;
h9*(g9*f9) = (h9*g9)*f9 by Th21;
hence thesis;
end;
theorem
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;
thus cod i = G;
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 f9 = f as Morphism of H,G by A1,Def12;
consider m being Function of H,G such that
A2: f9 = GroupMorphismStr(# H,G,m#) by Th13;
dom(i) = G & (id G)*m = m by FUNCT_2:17;
hence thesis by A1,A2,Def14;
end;
thus for g being strict GroupMorphism st dom g = G holds g*(ID G) = g
proof
let f be strict GroupMorphism such that
A3: dom f = G;
set H = cod(f);
reconsider f9 = f as Morphism of G,H by A3,Def12;
consider m being Function of G,H such that
A4: f9 = GroupMorphismStr(# G,H,m#) by Th13;
cod(i) = G & m*(id G) = m by FUNCT_2:17;
hence thesis by A3,A4,Def14;
end;
end;
:: 2. Domains of groups
definition
let IT be set;
attr IT is Group_DOMAIN-like means
:Def15:
for x being object st x in IT holds x is strict AddGroup;
end;
registration
cluster Group_DOMAIN-like non empty for set;
existence
proof
set D = {Trivial-addLoopStr};
take D;
for x be object st x in D holds x is strict AddGroup by TARSKI:def 1;
hence thesis;
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; :: redefines Element (SUBSET_1, definition)
coherence by Def15;
end;
registration
let V;
cluster strict for Element of V;
existence
proof
set v = the Element of V;
v is strict AddGroup by Def15;
hence thesis;
end;
end;
:: 3. Domains of morphisms
definition
let IT be set;
attr IT is GroupMorphism_DOMAIN-like means
:Def16:
for x being object st x in IT holds x is strict GroupMorphism;
end;
registration
cluster GroupMorphism_DOMAIN-like non empty for set;
existence
proof
set G = the AddGroup;
take {ID G};
for x being object st x in {ID G} holds x is strict GroupMorphism by
TARSKI:def 1;
hence thesis;
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; :: redefines Element (SUBSET_1, definition)
coherence by Def16;
end;
registration
let M be GroupMorphism_DOMAIN;
cluster strict for Element of M;
existence
proof
set m = the Element of M;
m is strict GroupMorphism by Def16;
hence thesis;
end;
end;
theorem Th24:
for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN
proof
let f be strict GroupMorphism;
for x being object st x in {f} holds x is strict GroupMorphism
by TARSKI:def 1;
hence thesis by Def16;
end;
definition
let G,H;
mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means
:Def17:
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 Th24;
take D;
thus thesis by TARSKI:def 1;
end;
end;
theorem Th25:
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 Def17;
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 object st x in D holds x is strict GroupMorphism;
then reconsider D9 = D as GroupMorphism_DOMAIN by Def16;
for x being Element of D9 holds x is strict Morphism of G,H by A1;
hence thesis by Def17;
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 Th25;
end;
definition
let G,H be 1-sorted;
mode MapsSet of G,H -> set means
:Def18:
for x being set st x in it holds x is Function 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
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);
hence thesis by FUNCT_2:66;
end;
end;
registration
let G be 1-sorted, H be non empty 1-sorted;
cluster Maps(G,H) -> non empty;
coherence;
end;
registration
let G be 1-sorted, H be non empty 1-sorted;
cluster non empty for 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 -> Function of G,H; :: redefines Element (SUBSET_1, definition)
coherence by Def18;
end;
definition
let G,H;
func Morphs(G,H) -> GroupMorphism_DOMAIN of G,H means
:Def20:
for x being object holds x in it iff x is strict Morphism of G,H;
existence
proof
reconsider f0 = ZeroMap(G,H) as Element of Maps(G,H) by FUNCT_2:8;
set D = { GroupMorphismStr(# G,H,f#) where f is Element of Maps(G,H) : f
is additive };
GroupMorphismStr(# G,H,f0#) in D;
then reconsider D as non empty set;
A1: for x being object holds x in D implies x is strict Morphism of G,H
proof let x be object;
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 Th11;
end;
then
A2: for x being Element of D holds x is strict Morphism of G,H;
A3: for x being object holds x is strict Morphism of G,H implies x in D
proof let x be object;
assume x is strict Morphism of G,H;
then reconsider x as strict Morphism of G,H;
A4: dom(x) = G & cod(x) = H by Def12;
then reconsider f = the Fun of x as Function of G,H;
reconsider g = f as Element of Maps(G,H) by FUNCT_2:8;
A5: x = GroupMorphismStr(# G,H,g #) by A4;
(the Fun of x) is additive by Th9;
hence thesis by A5;
end;
reconsider D as GroupMorphism_DOMAIN of G,H by A2,Th25;
take D;
thus thesis by A1,A3;
end;
uniqueness
proof
let D1,D2 be GroupMorphism_DOMAIN of G,H such that
A6: for x being object holds x in D1 iff x is strict Morphism of G,H and
A7: for x being object holds x in D2 iff x is strict Morphism of G,H;
for x being object holds x in D1 iff x in D2
proof let x be object;
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; :: redefines Element (SUBSET_1, definition)
coherence by Def17;
end;
registration
let G,H;
let M be GroupMorphism_DOMAIN of G,H;
cluster strict for Element of M;
existence
proof
set m = the Element of M;
m is strict Morphism of G,H by Def17;
hence thesis;
end;
end;
:: 4a. Category of groups - objects
definition
let x,y be object;
pred GO x,y means
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 addF of G &
x3 = comp G & x4 = 0.G;
end;
theorem Th27:
for x,y1,y2 being object st GO x,y1 & GO x,y2 holds y1 = y2
proof
let x,y1,y2 be object 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 addF of G & a3 = comp G & a4 = 0.G by A1;
consider G1 being strict AddGroup such that
A5: y1 = G1 and
A6: a1 = the carrier of G1 & a2 = the addF of G1 and
a3 = comp G1 and
A7: a4 = 0.G1 by A4;
consider b1,b2,b3,b4 being set such that
A8: x = [b1,b2,b3,b4] and
A9: ex G being strict AddGroup st y2 = G & b1 = the carrier of G & b2 =
the addF of G & b3 = comp G & b4 = 0.G by A2;
consider G2 being strict AddGroup such that
A10: y2 = G2 and
A11: b1 = the carrier of G2 & b2 = the addF of G2 and
b3 = comp G2 and
A12: b4 = 0.G2 by A9;
the carrier of G1 = the carrier of G2 & the addF of G1 = the addF of G2
by A3,A8,A6,A11,XTUPLE_0:5;
hence thesis by A3,A8,A5,A7,A10,A12,XTUPLE_0:5;
end;
theorem Th28:
ex x st x in UN & GO x,Trivial-addLoopStr
proof
reconsider x2 = op2 as Element of UN by Th3;
reconsider x3 = comp Trivial-addLoopStr as Element of UN by Th3,Th6;
reconsider u = {} as Element of UN by CLASSES2:56;
set x1 = {u};
Extract {} = u;
then reconsider x4 = Extract {} as Element of UN;
reconsider x = [x1,x2,x3,x4] as set by TARSKI:1;
take x;
thus x in UN by Th1;
take x1,x2,x3,x4;
thus x = [x1,x2,x3,x4];
take Trivial-addLoopStr;
thus thesis;
end;
definition
let UN;
func GroupObjects(UN) -> set means
:Def22:
for y being object holds y in it
iff ex x being object st x in UN & GO x,y;
existence
proof
defpred P[object,object] means GO $1,$2;
A1: for x,y1,y2 being object st P[x,y1] & P[x,y2] holds y1 = y2 by Th27;
consider Y being set such that
A2: for y being object holds y in Y iff
ex x being object st x in UN & P[x,y] from TARSKI:sch 1(A1);
take Y;
let y be object;
thus y in Y implies ex x being object st x in UN & GO x,y
by A2;
thus thesis by A2;
end;
uniqueness
proof
defpred P[object] means ex x being object st x in UN & GO x,$1;
for X1,X2 being set st
(for x being object holds x in X1 iff P[x]) & (for
x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
hence thesis;
end;
end;
theorem Th29:
Trivial-addLoopStr in GroupObjects(UN)
proof
ex x st x in UN & GO x,Trivial-addLoopStr by Th28;
hence thesis by Def22;
end;
registration
let UN;
cluster GroupObjects(UN) -> non empty;
coherence by Th29;
end;
theorem Th30:
for x being Element of GroupObjects(UN) holds x is strict AddGroup
proof
let x be Element of GroupObjects(UN);
consider u being object such that
u in UN and
A1: GO u,x by Def22;
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 addF of G & x3 = comp G &
x4 = 0.G by A1;
hence thesis;
end;
registration
let UN;
cluster GroupObjects(UN) -> Group_DOMAIN-like;
coherence
by Th30;
end;
:: 4b. Category of groups - morphisms
definition
let V;
func Morphs(V) -> GroupMorphism_DOMAIN means
:Def23:
for x being object holds x in it iff
ex G,H being strict Element of V st x is strict Morphism of G,H;
existence
proof
set G0 = the strict Element of V;
set M = Morphs(G0,G0), S = the set of all
Morphs(G,H) where G is strict Element of V, H
is strict Element of V ;
(ZERO(G0,G0)) is Element of M & M in S by Def20;
then reconsider T = union S as non empty set by TARSKI:def 4;
A1: for x being object
holds x in T iff ex G,H being strict Element of V st x is strict
Morphism of G,H
proof
let x be object;
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
A2: x in Y and
A3: Y in S by TARSKI:def 4;
consider G,H being strict Element of V such that
A4: Y = Morphs(G,H) by A3;
take G,H;
thus thesis by A2,A4,Def20;
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
A5: x is strict Morphism of G,H;
set M = Morphs(G,H);
A6: M in S;
x in M by A5,Def20;
hence thesis by A6,TARSKI:def 4;
end;
end;
now
let x be object;
assume x in T;
then ex G,H being strict Element of V st x is strict Morphism of G,H by
A1;
hence x is strict GroupMorphism;
end;
then reconsider T9 = T as GroupMorphism_DOMAIN by Def16;
take T9;
thus thesis by A1;
end;
uniqueness
proof
let D1,D2 be GroupMorphism_DOMAIN such that
A7: for x being object
holds x in D1 iff ex G,H being strict Element of V st x is
strict Morphism of G,H and
A8: for x being object
holds x in D2 iff ex G,H being strict Element of V st x is
strict Morphism of G,H;
now
let x be object;
x in D1 iff ex G,H being strict Element of V st x is strict
Morphism of G,H by A7;
hence x in D1 iff x in D2 by A8;
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; :: redefines dom (GRCAT_1, definition)
coherence
proof
consider G,H being strict Element of V such that
A1: F is strict Morphism of G,H by Def23;
reconsider F9 = F as Morphism of G,H by A1;
dom(F9) = G by Def12;
hence thesis;
end;
redefine func cod(F) -> strict Element of V; :: redefines cod (GRCAT_1, definition)
coherence
proof
consider G,H being strict Element of V such that
A2: F is strict Morphism of G,H by Def23;
reconsider F9 = F as Morphism of G,H by A2;
cod(F9) = H by Def12;
hence thesis;
end;
end;
definition
let V;
let G be Element of V;
func ID(G) -> strict Element of Morphs(V) equals
ID(G);
coherence
proof
reconsider G9 = G as strict Element of V by Def15;
ID(G9) is strict Element of Morphs(V) by Def23;
hence thesis;
end;
end;
definition
let V;
func dom(V) -> Function of Morphs(V),V means
:Def25:
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 FUNCT_2:sch
4;
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:63;
end;
func cod(V) -> Function of Morphs(V),V means
:Def26:
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 FUNCT_2:sch
4;
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:63;
end;
end;
::
:: 4d. Category of groups - superposition
::
theorem Th31:
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 Def23;
consider G1,G29 being strict Element of V such that
A3: f is strict Morphism of G1,G29 by Def23;
A4: G29 = cod(f) by A3,Def12;
G2 = dom(g) by A2,Def12;
hence thesis by A1,A2,A3,A4;
end;
theorem Th32:
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 and
A2: f is Morphism of G1,G2 by Th31;
reconsider f9 = f as Morphism of G1,G2 by A2;
reconsider g9 = g as Morphism of G2,G3 by A1;
g9*f9 is Morphism of G1,G3;
hence thesis by Def23;
end;
definition
let V;
func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means
:Def27:
(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 Th32;
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])& for
g,f being Element of X st [g,f] in dom c holds c.(g,f) = F(g,f) from BINOP_1:
sch 8(A1);
take c;
thus thesis by A2;
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
A3: for g,f being Element of X holds [g,f] in dom c1 iff P[g,f] and
A4: for g,f being Element of X st [g,f] in dom c1 holds c1.(g,f) = g*f and
A5: for g,f being Element of X holds [g,f] in dom c2 iff P[g,f] and
A6: for g,f being Element of X st [g,f] in dom c2 holds c2.(g,f) = g*f;
set V9 = dom c1;
A7: dom c1 c= [:X,X:] by RELAT_1:def 18;
now
let x be object;
assume
A8: x in dom c1;
then consider g,f being Element of X such that
A9: x = [g,f] by A7,SUBSET_1:43;
P[g,f] by A3,A8,A9;
hence x in dom c2 by A5,A9;
end;
then
A10: dom c1 c= dom c2 by TARSKI:def 3;
A11: for x,y being object st [x,y] in V9 holds c1.(x,y)=c2.(x,y)
proof
let x,y be object;
assume
A12: [x,y] in V9;
then reconsider x,y as Element of X by A7,ZFMISC_1:87;
c1.(x,y) = x*y by A4,A12;
hence thesis by A6,A10,A12;
end;
now
let x be object;
assume
A13: x in dom c2;
dom c2 c= [:X,X:] by RELAT_1:def 18;
then consider g,f being Element of X such that
A14: x = [g,f] by A13,SUBSET_1:43;
P[g,f] by A5,A13,A14;
hence x in dom c1 by A3,A14;
end;
then dom c2 c= dom c1 by TARSKI:def 3;
then dom c1 = dom c2 by A10,XBOOLE_0:def 10;
hence thesis by A11,BINOP_1:20;
end;
end;
::
:: 4e. Definition of Category of groups
::
definition
let UN;
func GroupCat(UN) -> non empty non void strict CatStr equals
CatStr(# GroupObjects(UN),Morphs(
GroupObjects(UN)), dom(GroupObjects(UN)),cod(GroupObjects(UN)), comp(
GroupObjects(UN))#);
coherence;
end;
registration
let UN;
cluster GroupCat(UN) -> strict non void non empty;
coherence;
end;
theorem Th33:
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);
let f,g be Morphism of C;
reconsider f9 = f as Element of Morphs(V);
reconsider g9 = g as Element of Morphs(V);
dom g = dom(g9) & cod f = cod(f9) by Def25,Def26;
hence thesis by Def27;
end;
theorem Th34:
for f being (Morphism of GroupCat(UN)), f9 being Element of
Morphs(GroupObjects(UN)), b being Object of GroupCat(UN), b9 being Element of
GroupObjects(UN) holds f is strict Element of Morphs(GroupObjects(UN)) & f9 is
Morphism of GroupCat(UN) & b is strict Element of GroupObjects(UN) & b9 is
Object of GroupCat(UN)
proof
set C = GroupCat(UN), V = GroupObjects(UN);
set X = Morphs(V);
let f be (Morphism of C), f9 be Element of X, b be Object of C, b9 be
Element of V;
consider x being object such that
x in UN and
A1: GO x,b by Def22;
ex G,H being strict Element of V st f is strict Morphism of G,H by Def23;
hence f is strict Element of X;
thus f9 is Morphism of C;
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 addF of G & x3 = comp G &
x4 = 0.G by A1;
hence b is strict Element of V;
thus thesis;
end;
::$CT
theorem Th35:
for f,g being (Morphism of GroupCat(UN)),
f9,g9 being Element of Morphs(GroupObjects(UN)) st f = f9 & g = g9
holds
(dom g = cod f iff dom g9 = cod f9) &
(dom g = cod f iff [g9,f9] in dom comp(GroupObjects(UN))) &
(dom g = cod f implies g(*)f = g9*f9) &
(dom f = dom g iff dom f9 = dom g9) &
(cod f = cod g iff cod f9 = cod g9)
proof
set C = GroupCat(UN), V = GroupObjects(UN);
set X = Morphs(V);
let f,g be Morphism of C;
let f9,g9 be Element of X;
assume that
A1: f = f9 and
A2: g = g9;
A3: cod f = cod f9 by A1,Def26;
hence dom g = cod f iff dom g9 = cod f9 by A2,Def25;
dom g = dom g9 by A2,Def25;
hence
A4: dom g = cod f iff [g9,f9] in dom comp(V) by A3,Def27;
thus dom g = cod f implies g(*)f = g9*f9
proof
assume
A5: dom g = cod f;
then [g,f] in dom (the Comp of C) by Th33;
hence g(*)f = (comp(V)).(g9,f9) by A1,A2,CAT_1:def 1
.= g9*f9 by A4,A5,Def27;
end;
dom f = dom f9 by A1,Def25;
hence dom f = dom g iff dom f9 = dom g9 by A2,Def25;
cod g = cod g9 by A2,Def26;
hence thesis by A1,Def26;
end;
Lm1: 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 g9 = g as strict Element of X by Th34;
reconsider f9 = f as strict Element of X by Th34;
A2: dom g9 = cod f9 by A1,Th35;
then reconsider gf = g9*f9 as Element of X by Th32;
A3: gf = g(*)f by A1,Th35;
dom(g9*f9) = dom f9 & cod (g9*f9) = cod g9 by A2,Th20;
hence thesis by A3,Th35;
end;
registration
let UN;
cluster GroupCat UN -> reflexive Category-like;
coherence
proof set C = GroupCat UN;
thus C is reflexive
proof let a be Element of C;
reconsider G = a as Element of GroupObjects UN;
consider x being object such that
x in UN and
A1: GO x,G by Def22;
set ii = ID G;
consider x1,x2,x3,x4 being set such that x = [x1,x2,x3,x4] and
A2: ex H being strict AddGroup st G = H & x1 = the carrier of H &
x2 = the addF of H & x3 = comp H & x4 = 0.H by A1;
reconsider G as strict Element of GroupObjects UN by A2;
reconsider ii as Morphism of C;
reconsider ia = ii as GroupMorphismStr;
A3: dom ii = dom ia by Def25
.= a;
cod ii = cod ia by Def26
.= a;
then ii in Hom(a,a) by A3;
hence Hom(a,a)<>{};
end;
let f,g be Morphism of C;
reconsider ff=f, gg=g as Element of Morphs GroupObjects UN;
thus [g,f] in dom(the Comp of C) iff dom g = cod f by Th35;
end;
end;
Lm2:
for a being Element of GroupCat UN,
aa being Element of GroupObjects UN st a = aa
for i being Morphism of a,a st i = ID aa
for b being Element of GroupCat UN holds
(Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g) &
(Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f)
proof
let a be Element of GroupCat UN,
aa be Element of GroupObjects UN such that
a = aa;
let i be Morphism of a,a such that
A1: i = ID aa;
let b be Element of GroupCat UN;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g
proof assume
A2: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider gg=g, ii=i as Element of Morphs GroupObjects UN;
consider G1,H1 being strict Element of GroupObjects UN such that
A3: gg is strict Morphism of G1,H1 by Def23;
consider f being Function of G1,H1 such that
A4: gg = GroupMorphismStr(#G1,H1,f#) by A3,Th13;
A5: ii = GroupMorphismStr(# aa,aa,id aa#) by A1;
A6: cod ii = aa by A1;
A7: dom gg = G1 by A4;
A8: Hom(a,a) <> {};
dom g = a by A2,CAT_1:5 .= cod i by A8,CAT_1:5;
then
A9: dom gg = cod ii by Th35;
then aa = dom gg by A6;
then
A10: aa = G1 by A7;
then reconsider f as Function of aa,H1;
A11: the GroupMorphismStr of gg = GroupMorphismStr(#aa,H1,f#) by A4,A10;
A12: [gg,ii] in dom comp GroupObjects UN by Def27,A9;
then [g,i] in dom the Comp of GroupCat UN;
hence g(*)i = (the Comp of GroupCat UN).(g,i) by CAT_1:def 1
.= (comp GroupObjects UN).(g,i)
.= gg*ii by A12,Def27
.= GroupMorphismStr(# aa,H1,f*id aa#) by A5,Def14,A11,A9
.= GroupMorphismStr(# aa,H1,f#) by FUNCT_2:17
.= g by A10,A4;
end;
thus Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f
proof assume
A13: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider gg=g, ii=i as Element of Morphs GroupObjects UN;
consider G1,H1 being strict Element of GroupObjects UN such that
A14: gg is strict Morphism of G1,H1 by Def23;
consider f being Function of G1,H1 such that
A15: gg = GroupMorphismStr(#G1,H1,f#) by A14,Th13;
A16: ii = GroupMorphismStr(# aa,aa,id aa#) by A1;
A17: dom ii = aa by A1;
A18: cod gg = H1 by A15;
A19: Hom(a,a) <> {};
cod g = a by A13,CAT_1:5 .= dom i by A19,CAT_1:5;
then
A20: cod gg = dom ii by Th35;
then aa = cod gg by A17;
then
A21: aa = H1 by A18;
then reconsider f as Function of G1,aa;
A22: the GroupMorphismStr of gg = GroupMorphismStr(#G1,aa,f#) by A15,A21;
A23: [ii,gg] in dom comp GroupObjects UN by Def27,A20;
then [i,g] in dom the Comp of GroupCat UN;
hence i(*)g = (the Comp of GroupCat UN).(i,g) by CAT_1:def 1
.= (comp GroupObjects UN).(i,g)
.= ii*gg by A23,Def27
.= GroupMorphismStr(# G1,aa,(id aa)*f#) by A16,Def14,A22,A20
.= GroupMorphismStr(# G1,aa,f#) by FUNCT_2:17
.= g by A21,A15;
end;
end;
registration
let UN;
cluster GroupCat UN ->
transitive associative with_identities;
coherence
proof set C = GroupCat UN;
set X = Morphs(GroupObjects(UN));
thus C is transitive
proof
let f,g be Morphism of GroupCat(UN) such that
A1: dom g = cod f;
reconsider g9 = g as strict Element of X by Th34;
reconsider f9 = f as strict Element of X by Th34;
A2: dom g9 = cod f9 by A1,Th35;
then reconsider gf = g9*f9 as Element of X by Th32;
A3: gf = g(*)f by A1,Th35;
dom(g9*f9) = dom f9 & cod (g9*f9) = cod g9 by A2,Th20;
hence thesis by A3,Th35;
end;
thus C is associative
proof
let f,g,h be Morphism of (GroupCat(UN)) such that
A4: dom h = cod g & dom g = cod f;
reconsider f9=f, g9=g, h9=h as strict Element of X by Th34;
A5: h9*g9 = h(*)g & dom(h(*)g) = cod(f) by A4,Lm1,Th35;
A6: dom h9 = cod g9 & dom g9 = cod f9 by A4,Th35;
then reconsider gf = g9*f9, hg = h9*g9 as Element of X by Th32;
g9*f9 = g(*)f & dom(h) = cod(g(*)f) by A4,Lm1,Th35;
then h(*)(g(*)f) = h9*gf by Th35
.= hg*f9 by A6,Th22
.= (h(*)g)(*)f by A5,Th35;
hence thesis;
end;
thus C is with_identities
proof let a be Element of C;
reconsider aa = a as Element of GroupObjects(UN);
reconsider ii = ID aa as Morphism of C;
reconsider ia = ii as GroupMorphismStr;
A7: dom ii = dom ia by Def25
.= a;
cod ii = cod ia by Def26
.= a;
then reconsider ii as Morphism of a,a by A7,CAT_1:4;
take ii;
thus thesis by Lm2;
end;
end;
end;
definition
let UN;
func AbGroupObjects(UN) -> Subset of the carrier of GroupCat(UN) equals
{G
where G is Element of GroupCat(UN) : ex H being AbGroup st G = H
};
coherence
proof
set D2 = the carrier of GroupCat(UN);
now
let x be object;
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 Th36:
Trivial-addLoopStr in AbGroupObjects(UN)
proof
Trivial-addLoopStr in the carrier of GroupCat(UN) by Th29;
hence thesis;
end;
registration
let UN;
cluster AbGroupObjects(UN) -> non empty;
coherence by Th36;
end;
definition
let UN;
func AbGroupCat UN -> Subcategory of GroupCat(UN) equals
cat AbGroupObjects UN;
coherence;
end;
registration
let UN;
cluster AbGroupCat(UN) -> strict;
coherence;
end;
theorem
the carrier of AbGroupCat(UN) = AbGroupObjects(UN);
:: 6. Subcategory of groups with the operator of 1/2
definition
let UN;
func MidOpGroupObjects(UN) -> Subset of the carrier of AbGroupCat(UN) equals
{G where G is Element of AbGroupCat(UN) : ex H being
midpoint_operator AbGroup st G = H};
coherence
proof
set D2 = the carrier of AbGroupCat(UN);
now
let x be object;
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;
registration
let UN;
cluster MidOpGroupObjects(UN) -> non empty;
coherence
proof
set T = Trivial-addLoopStr;
set D2 = the carrier of AbGroupCat(UN);
set D1 = {G where G is Element of D2 : ex H being midpoint_operator
AbGroup st G = H};
T in D2 by Th36;
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;
end;
end;
definition
let UN;
func MidOpGroupCat UN -> Subcategory of AbGroupCat(UN) equals
cat MidOpGroupObjects UN;
coherence;
end;
registration
let UN;
cluster MidOpGroupCat(UN) -> strict;
coherence;
end;
theorem
the carrier of MidOpGroupCat(UN) = MidOpGroupObjects(UN);
theorem
Trivial-addLoopStr in MidOpGroupObjects(UN)
proof
Trivial-addLoopStr in the carrier of AbGroupCat(UN) by Th36;
hence thesis;
end;
theorem :: WAYBEL29:1
for S, T being non empty 1-sorted for f being Function of S, T st f is
one-to-one onto holds f*f" = id T & f"*f = id S & f" is one-to-one onto
proof
let S, T be non empty 1-sorted;
let f be Function of S, T;
A1: [#]T = the carrier of T;
assume
A2: f is one-to-one onto;
then
A3: rng f = the carrier of T by FUNCT_2:def 3;
then dom f = the carrier of S & rng (f") = [#]S by A2,A1,FUNCT_2:def 1
,TOPS_2:49;
hence thesis by A2,A3,A1,FUNCT_2:def 3,TOPS_2:50,52;
end;
theorem
for a being Object of GroupCat(UN), aa being Element of
GroupObjects(UN) st a = aa holds id a = ID aa
proof let a be Object of GroupCat UN, aa be Element of GroupObjects UN;
set C = GroupCat UN;
assume
A1: a = aa;
reconsider ii = ID aa as Morphism of C;
reconsider ia = ii as GroupMorphismStr;
A2: dom ii = dom ia by Def25
.= a by A1;
cod ii = cod ia by Def26
.= a by A1;
then reconsider ii as Morphism of a,a by A2,CAT_1:4;
for b being Object of C holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)ii = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds ii(*)f = f) by A1,Lm2;
hence id a = ID aa by CAT_1:def 12;
end;