:: by Michal Muzalewski

::

:: Received October 3, 1991

:: Copyright (c) 1991-2019 Association of Mizar Users

theorem Th1: :: GRCAT_1:1

for UN being Universe

for u1, u2, u3, u4 being Element of UN holds

( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN )

for u1, u2, u3, u4 being Element of UN holds

( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN )

proof end;

:: 0c. Auxiliary theorems: Trivial Group

theorem Th3: :: GRCAT_1:3

for UN being Universe holds

( {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )

( {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )

proof end;

theorem :: GRCAT_1:4

( ( 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;

definition

let C be Category;

let O be non empty Subset of the carrier of C;

union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is Subset of the carrier' of C by CAT_2:19;

end;
let O be non empty Subset of the carrier of C;

func Morphs O -> Subset of the carrier' of C equals :: GRCAT_1:def 1

union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

coherence union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is Subset of the carrier' of C by CAT_2:19;

:: deftheorem defines Morphs GRCAT_1:def 1 :

for C being Category

for O being non empty Subset of the carrier of C holds Morphs O = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

for C being Category

for O being non empty Subset of the carrier of C holds Morphs O = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

registration

let C be Category;

let O be non empty Subset of the carrier of C;

coherence

not Morphs O is empty by CAT_2:19;

end;
let O be non empty Subset of the carrier of C;

coherence

not Morphs O is empty by CAT_2:19;

definition

let C be Category;

let O be non empty Subset of the carrier of C;

coherence

the Source of C | (Morphs O) is Function of (Morphs O),O by CAT_2:20;

coherence

the Target of C | (Morphs O) is Function of (Morphs O),O by CAT_2:20;

the Comp of C || (Morphs O) is PartFunc of [:(Morphs O),(Morphs O):],(Morphs O) by CAT_2:20;

end;
let O be non empty Subset of the carrier of C;

coherence

the Source of C | (Morphs O) is Function of (Morphs O),O by CAT_2:20;

coherence

the Target of C | (Morphs O) is Function of (Morphs O),O by CAT_2:20;

func comp O -> PartFunc of [:(Morphs O),(Morphs O):],(Morphs O) equals :: GRCAT_1:def 4

the Comp of C || (Morphs O);

coherence the Comp of C || (Morphs O);

the Comp of C || (Morphs O) is PartFunc of [:(Morphs O),(Morphs O):],(Morphs O) by CAT_2:20;

:: deftheorem defines dom GRCAT_1:def 2 :

for C being Category

for O being non empty Subset of the carrier of C holds dom O = the Source of C | (Morphs O);

for C being Category

for O being non empty Subset of the carrier of C holds dom O = the Source of C | (Morphs O);

:: deftheorem defines cod GRCAT_1:def 3 :

for C being Category

for O being non empty Subset of the carrier of C holds cod O = the Target of C | (Morphs O);

for C being Category

for O being non empty Subset of the carrier of C holds cod O = the Target of C | (Morphs O);

:: deftheorem defines comp GRCAT_1:def 4 :

for C being Category

for O being non empty Subset of the carrier of C holds comp O = the Comp of C || (Morphs O);

for C being Category

for O being non empty Subset of the carrier of C holds comp O = the Comp of C || (Morphs O);

definition

let C be Category;

let O be non empty Subset of the carrier of C;

CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #) is Subcategory of C by CAT_2:21;

end;
let O be non empty Subset of the carrier of C;

func cat O -> Subcategory of C equals :: GRCAT_1:def 6

CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #);

coherence CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #);

CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #) is Subcategory of C by CAT_2:21;

:: deftheorem defines cat GRCAT_1:def 6 :

for C being Category

for O being non empty Subset of the carrier of C holds cat O = CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #);

for C being Category

for O being non empty Subset of the carrier of C holds cat O = CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #);

registration
end;

theorem :: GRCAT_1:5

:: 1a. Maps of the carriers of groups

definition

let G be non empty 1-sorted ;

let H be non empty ZeroStr ;

coherence

the carrier of G --> (0. H) is Function of G,H ;

end;
let H be non empty ZeroStr ;

coherence

the carrier of G --> (0. H) is Function of G,H ;

:: deftheorem defines ZeroMap GRCAT_1:def 7 :

for G being non empty 1-sorted

for H being non empty ZeroStr holds ZeroMap (G,H) = the carrier of G --> (0. H);

for G being non empty 1-sorted

for H being non empty ZeroStr holds ZeroMap (G,H) = the carrier of G --> (0. H);

registration

let G be non empty addMagma ;

let H be non empty right_zeroed addLoopStr ;

coherence

ZeroMap (G,H) is additive

end;
let H be non empty right_zeroed addLoopStr ;

coherence

ZeroMap (G,H) is additive

proof end;

registration

let G be non empty addMagma ;

let H be non empty right_zeroed addLoopStr ;

ex b_{1} being Function of G,H st b_{1} is additive

end;
let H be non empty right_zeroed addLoopStr ;

cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty total quasi_total additive for Element of bool [: the carrier of G, the carrier of H:];

existence ex b

proof end;

theorem Th7: :: GRCAT_1:7

for G1, G2, G3 being non empty addMagma

for f being Function of G1,G2

for g being Function of G2,G3 st f is additive & g is additive holds

g * f is additive

for f being Function of G1,G2

for g being Function of G2,G3 st f is additive & g is additive holds

g * f is additive

proof end;

registration

let G1 be non empty addMagma ;

let G2, G3 be non empty right_zeroed addLoopStr ;

let f be additive Function of G1,G2;

let g be additive Function of G2,G3;

coherence

for b_{1} being Function of G1,G3 st b_{1} = g * f holds

b_{1} is additive
by Th7;

end;
let G2, G3 be non empty right_zeroed addLoopStr ;

let f be additive Function of G1,G2;

let g be additive Function of G2,G3;

coherence

for b

b

definition

attr c_{1} is strict ;

struct GroupMorphismStr -> ;

aggr GroupMorphismStr(# Source, Target, Fun #) -> GroupMorphismStr ;

sel Source c_{1} -> AddGroup;

sel Target c_{1} -> AddGroup;

sel Fun c_{1} -> Function of the Source of c_{1}, the Target of c_{1};

end;
struct GroupMorphismStr -> ;

aggr GroupMorphismStr(# Source, Target, Fun #) -> GroupMorphismStr ;

sel Source c

sel Target c

sel Fun c

definition

let f be GroupMorphismStr ;

coherence

the Source of f is AddGroup ;

coherence

the Target of f is AddGroup ;

end;
coherence

the Source of f is AddGroup ;

coherence

the Target of f is AddGroup ;

:: deftheorem defines dom GRCAT_1:def 9 :

for f being GroupMorphismStr holds dom f = the Source of f;

for f being GroupMorphismStr holds dom f = the Source of f;

:: deftheorem defines cod GRCAT_1:def 10 :

for f being GroupMorphismStr holds cod f = the Target of f;

for f being GroupMorphismStr holds cod f = the Target of f;

theorem :: GRCAT_1:8

definition

let G, H be AddGroup;

GroupMorphismStr(# G,H,(ZeroMap (G,H)) #) is GroupMorphismStr ;

end;
func ZERO (G,H) -> GroupMorphismStr equals :: GRCAT_1:def 12

GroupMorphismStr(# G,H,(ZeroMap (G,H)) #);

coherence GroupMorphismStr(# G,H,(ZeroMap (G,H)) #);

GroupMorphismStr(# G,H,(ZeroMap (G,H)) #) is GroupMorphismStr ;

:: deftheorem defines ZERO GRCAT_1:def 12 :

for G, H being AddGroup holds ZERO (G,H) = GroupMorphismStr(# G,H,(ZeroMap (G,H)) #);

for G, H being AddGroup holds ZERO (G,H) = GroupMorphismStr(# G,H,(ZeroMap (G,H)) #);

registration
end;

:: deftheorem Def11 defines GroupMorphism-like GRCAT_1:def 13 :

for IT being GroupMorphismStr holds

( IT is GroupMorphism-like iff fun IT is additive );

for IT being GroupMorphismStr holds

( IT is GroupMorphism-like iff fun IT is additive );

registration

existence

ex b_{1} being GroupMorphismStr st

( b_{1} is strict & b_{1} is GroupMorphism-like )

end;
ex b

( b

proof end;

definition

let G, H be AddGroup;

existence

ex b_{1} being GroupMorphism st

( dom b_{1} = G & cod b_{1} = H )

end;
existence

ex b

( dom b

proof end;

:: deftheorem Def12 defines Morphism GRCAT_1:def 14 :

for G, H being AddGroup

for b_{3} being GroupMorphism holds

( b_{3} is Morphism of G,H iff ( dom b_{3} = G & cod b_{3} = H ) );

for G, H being AddGroup

for b

( b

registration
end;

theorem Th10: :: GRCAT_1:10

for G, H being AddGroup

for f being strict GroupMorphismStr st dom f = G & cod f = H & fun f is additive holds

f is strict Morphism of G,H

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 end;

theorem Th11: :: GRCAT_1:11

for G, H being AddGroup

for f being Function of G,H st f is additive holds

GroupMorphismStr(# G,H,f #) is strict Morphism of G,H

for f being Function of G,H st f is additive holds

GroupMorphismStr(# G,H,f #) is strict Morphism of G,H

proof end;

registration
end;

definition
end;

:: deftheorem defines ID GRCAT_1:def 15 :

for G being AddGroup holds ID G = GroupMorphismStr(# G,G,(id G) #);

for G being AddGroup holds ID G = GroupMorphismStr(# G,G,(id G) #);

definition

let G, H be AddGroup;

:: original: ZERO

redefine func ZERO (G,H) -> strict Morphism of G,H;

coherence

ZERO (G,H) is strict Morphism of G,H

end;
:: original: ZERO

redefine func ZERO (G,H) -> strict Morphism of G,H;

coherence

ZERO (G,H) is strict Morphism of G,H

proof end;

theorem Th12: :: GRCAT_1:12

for G, H being AddGroup

for F being Morphism of G,H ex f being Function of G,H st

( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive )

for F being Morphism of G,H ex f being Function of G,H st

( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive )

proof end;

theorem Th13: :: GRCAT_1:13

for G, H being AddGroup

for F being strict Morphism of G,H ex f being Function of G,H st F = GroupMorphismStr(# G,H,f #)

for F being strict Morphism of G,H ex f being Function of G,H st F = GroupMorphismStr(# G,H,f #)

proof end;

theorem :: GRCAT_1:15

for F being strict GroupMorphism ex G, H being AddGroup ex f being Function of G,H st

( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )

( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )

proof end;

theorem Th16: :: GRCAT_1:16

for g, f being GroupMorphism st dom g = cod f holds

ex G1, G2, G3 being AddGroup st

( g is Morphism of G2,G3 & f is Morphism of G1,G2 )

ex G1, G2, G3 being AddGroup st

( g is Morphism of G2,G3 & f is Morphism of G1,G2 )

proof end;

definition

let G, F be GroupMorphism;

assume A1: dom G = cod F ;

ex b_{1} being strict GroupMorphism st

for G1, G2, G3 being AddGroup

for g being Function of G2,G3

for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds

b_{1} = GroupMorphismStr(# G1,G3,(g * f) #)

for b_{1}, b_{2} being strict GroupMorphism st ( for G1, G2, G3 being AddGroup

for g being Function of G2,G3

for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds

b_{1} = GroupMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being AddGroup

for g being Function of G2,G3

for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds

b_{2} = GroupMorphismStr(# G1,G3,(g * f) #) ) holds

b_{1} = b_{2}

end;
assume A1: dom G = cod F ;

func G * F -> strict GroupMorphism means :Def14: :: GRCAT_1:def 16

for G1, G2, G3 being AddGroup

for g being Function of G2,G3

for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds

it = GroupMorphismStr(# G1,G3,(g * f) #);

existence for G1, G2, G3 being AddGroup

for g being Function of G2,G3

for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds

it = GroupMorphismStr(# G1,G3,(g * f) #);

ex b

for G1, G2, G3 being AddGroup

for g being Function of G2,G3

for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds

b

proof end;

uniqueness for b

for g being Function of G2,G3

for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds

b

for g being Function of G2,G3

for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds

b

b

proof end;

:: deftheorem Def14 defines * GRCAT_1:def 16 :

for G, F being GroupMorphism st dom G = cod F holds

for b_{3} being strict GroupMorphism holds

( b_{3} = G * F iff for G1, G2, G3 being AddGroup

for g being Function of G2,G3

for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds

b_{3} = GroupMorphismStr(# G1,G3,(g * f) #) );

for G, F being GroupMorphism st dom G = cod F holds

for b

( b

for g being Function of G2,G3

for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds

b

theorem Th17: :: GRCAT_1:17

for G1, G2, G3 being AddGroup

for G being Morphism of G2,G3

for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3

for G being Morphism of G2,G3

for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3

proof end;

definition

let G1, G2, G3 be AddGroup;

let G be Morphism of G2,G3;

let F be Morphism of G1,G2;

:: original: *

redefine func G * F -> strict Morphism of G1,G3;

coherence

G * F is strict Morphism of G1,G3 by Th17;

end;
let G be Morphism of G2,G3;

let F be Morphism of G1,G2;

:: original: *

redefine func G * F -> strict Morphism of G1,G3;

coherence

G * F is strict Morphism of G1,G3 by Th17;

theorem Th18: :: GRCAT_1:18

for G1, G2, G3 being AddGroup

for G being Morphism of G2,G3

for F being Morphism of G1,G2

for g being Function of G2,G3

for 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) #)

for G being Morphism of G2,G3

for F being Morphism of G1,G2

for g being Function of G2,G3

for 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 end;

theorem Th19: :: GRCAT_1:19

for f, g being strict GroupMorphism st dom g = cod f holds

ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st

( f = GroupMorphismStr(# G1,G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #) )

ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex 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 end;

theorem Th20: :: GRCAT_1:20

for f, g being strict GroupMorphism st dom g = cod f holds

( dom (g * f) = dom f & cod (g * f) = cod g )

( dom (g * f) = dom f & cod (g * f) = cod g )

proof end;

theorem Th21: :: GRCAT_1:21

for G1, G2, G3, G4 being AddGroup

for f being strict Morphism of G1,G2

for g being strict Morphism of G2,G3

for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f

for f being strict Morphism of G1,G2

for g being strict Morphism of G2,G3

for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f

proof end;

theorem Th22: :: GRCAT_1:22

for f, g, h being strict GroupMorphism st dom h = cod g & dom g = cod f holds

h * (g * f) = (h * g) * f

h * (g * f) = (h * g) * f

proof end;

theorem :: GRCAT_1:23

for G being AddGroup holds

( 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 ) )

( 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 end;

:: 2. Sourceains of groups

definition

let IT be set ;

end;
attr IT is Group_DOMAIN-like means :Def15: :: GRCAT_1:def 17

for x being object st x in IT holds

x is strict AddGroup;

for x being object st x in IT holds

x is strict AddGroup;

:: deftheorem Def15 defines Group_DOMAIN-like GRCAT_1:def 17 :

for IT being set holds

( IT is Group_DOMAIN-like iff for x being object st x in IT holds

x is strict AddGroup );

for IT being set holds

( IT is Group_DOMAIN-like iff for x being object st x in IT holds

x is strict AddGroup );

registration
end;

definition

let V be Group_DOMAIN;

:: original: Element

redefine mode Element of V -> AddGroup;

coherence

for b_{1} being Element of V holds b_{1} is AddGroup
by Def15;

end;
:: original: Element

redefine mode Element of V -> AddGroup;

coherence

for b

registration

let V be Group_DOMAIN;

ex b_{1} being Element of V st b_{1} is strict

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for Element of V;

existence ex b

proof end;

:: 3. Domains of morphisms

definition

let IT be set ;

end;
attr IT is GroupMorphism_DOMAIN-like means :Def16: :: GRCAT_1:def 18

for x being object st x in IT holds

x is strict GroupMorphism;

for x being object st x in IT holds

x is strict GroupMorphism;

:: deftheorem Def16 defines GroupMorphism_DOMAIN-like GRCAT_1:def 18 :

for IT being set holds

( IT is GroupMorphism_DOMAIN-like iff for x being object st x in IT holds

x is strict GroupMorphism );

for IT being set holds

( IT is GroupMorphism_DOMAIN-like iff for x being object st x in IT holds

x is strict GroupMorphism );

registration

existence

ex b_{1} being set st

( b_{1} is GroupMorphism_DOMAIN-like & not b_{1} is empty )

end;
ex b

( b

proof end;

definition

let M be GroupMorphism_DOMAIN;

:: original: Element

redefine mode Element of M -> GroupMorphism;

coherence

for b_{1} being Element of M holds b_{1} is GroupMorphism
by Def16;

end;
:: original: Element

redefine mode Element of M -> GroupMorphism;

coherence

for b

registration
end;

definition

let G, H be AddGroup;

ex b_{1} being GroupMorphism_DOMAIN st

for x being Element of b_{1} holds x is strict Morphism of G,H

end;
mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means :Def17: :: GRCAT_1:def 19

for x being Element of it holds x is strict Morphism of G,H;

existence for x being Element of it holds x is strict Morphism of G,H;

ex b

for x being Element of b

proof end;

:: deftheorem Def17 defines GroupMorphism_DOMAIN GRCAT_1:def 19 :

for G, H being AddGroup

for b_{3} being GroupMorphism_DOMAIN holds

( b_{3} is GroupMorphism_DOMAIN of G,H iff for x being Element of b_{3} holds x is strict Morphism of G,H );

for G, H being AddGroup

for b

( b

theorem Th25: :: GRCAT_1:25

for D being non empty set

for G, H being AddGroup holds

( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )

for G, H being AddGroup holds

( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )

proof end;

definition

let G, H be 1-sorted ;

ex b_{1} being set st

for x being set st x in b_{1} holds

x is Function of G,H

end;
mode MapsSet of G,H -> set means :Def18: :: GRCAT_1:def 20

for x being set st x in it holds

x is Function of G,H;

existence for x being set st x in it holds

x is Function of G,H;

ex b

for x being set st x in b

x is Function of G,H

proof end;

:: deftheorem Def18 defines MapsSet GRCAT_1:def 20 :

for G, H being 1-sorted

for b_{3} being set holds

( b_{3} is MapsSet of G,H iff for x being set st x in b_{3} holds

x is Function of G,H );

for G, H being 1-sorted

for b

( b

x is Function of G,H );

definition

let G, H be 1-sorted ;

Funcs ( the carrier of G, the carrier of H) is MapsSet of G,H

end;
func Maps (G,H) -> MapsSet of G,H equals :: GRCAT_1:def 21

Funcs ( the carrier of G, the carrier of H);

coherence Funcs ( the carrier of G, the carrier of H);

Funcs ( the carrier of G, the carrier of H) is MapsSet of G,H

proof end;

:: deftheorem defines Maps GRCAT_1:def 21 :

for G, H being 1-sorted holds Maps (G,H) = Funcs ( the carrier of G, the carrier of H);

for G, H being 1-sorted holds Maps (G,H) = Funcs ( the carrier of G, the carrier of H);

registration
end;

registration

let G be 1-sorted ;

let H be non empty 1-sorted ;

existence

not for b_{1} being MapsSet of G,H holds b_{1} is empty

end;
let H be non empty 1-sorted ;

existence

not for b

proof end;

definition

let G be 1-sorted ;

let H be non empty 1-sorted ;

let M be non empty MapsSet of G,H;

:: original: Element

redefine mode Element of M -> Function of G,H;

coherence

for b_{1} being Element of M holds b_{1} is Function of G,H
by Def18;

end;
let H be non empty 1-sorted ;

let M be non empty MapsSet of G,H;

:: original: Element

redefine mode Element of M -> Function of G,H;

coherence

for b

definition

let G, H be AddGroup;

ex b_{1} being GroupMorphism_DOMAIN of G,H st

for x being object holds

( x in b_{1} iff x is strict Morphism of G,H )

for b_{1}, b_{2} being GroupMorphism_DOMAIN of G,H st ( for x being object holds

( x in b_{1} iff x is strict Morphism of G,H ) ) & ( for x being object holds

( x in b_{2} iff x is strict Morphism of G,H ) ) holds

b_{1} = b_{2}

end;
func Morphs (G,H) -> GroupMorphism_DOMAIN of G,H means :Def20: :: GRCAT_1:def 22

for x being object holds

( x in it iff x is strict Morphism of G,H );

existence for x being object holds

( x in it iff x is strict Morphism of G,H );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def20 defines Morphs GRCAT_1:def 22 :

for G, H being AddGroup

for b_{3} being GroupMorphism_DOMAIN of G,H holds

( b_{3} = Morphs (G,H) iff for x being object holds

( x in b_{3} iff x is strict Morphism of G,H ) );

for G, H being AddGroup

for b

( b

( x in b

definition

let G, H be AddGroup;

let M be GroupMorphism_DOMAIN of G,H;

:: original: Element

redefine mode Element of M -> Morphism of G,H;

coherence

for b_{1} being Element of M holds b_{1} is Morphism of G,H
by Def17;

end;
let M be GroupMorphism_DOMAIN of G,H;

:: original: Element

redefine mode Element of M -> Morphism of G,H;

coherence

for b

registration

let G, H be AddGroup;

let M be GroupMorphism_DOMAIN of G,H;

existence

ex b_{1} being Element of M st b_{1} is strict

end;
let M be GroupMorphism_DOMAIN of G,H;

existence

ex b

proof end;

:: 4a. Category of groups - objects

:: deftheorem defines GO GRCAT_1:def 23 :

for x, y being object holds

( GO x,y iff 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 ) ) );

for x, y being object holds

( GO x,y iff 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 ) ) );

definition

let UN be Universe;

ex b_{1} being set st

for y being object holds

( y in b_{1} iff ex x being object st

( x in UN & GO x,y ) )

for b_{1}, b_{2} being set st ( for y being object holds

( y in b_{1} iff ex x being object st

( x in UN & GO x,y ) ) ) & ( for y being object holds

( y in b_{2} iff ex x being object st

( x in UN & GO x,y ) ) ) holds

b_{1} = b_{2}

end;
func GroupObjects UN -> set means :Def22: :: GRCAT_1:def 24

for y being object holds

( y in it iff ex x being object st

( x in UN & GO x,y ) );

existence for y being object holds

( y in it iff ex x being object st

( x in UN & GO x,y ) );

ex b

for y being object holds

( y in b

( x in UN & GO x,y ) )

proof end;

uniqueness for b

( y in b

( x in UN & GO x,y ) ) ) & ( for y being object holds

( y in b

( x in UN & GO x,y ) ) ) holds

b

proof end;

:: deftheorem Def22 defines GroupObjects GRCAT_1:def 24 :

for UN being Universe

for b_{2} being set holds

( b_{2} = GroupObjects UN iff for y being object holds

( y in b_{2} iff ex x being object st

( x in UN & GO x,y ) ) );

for UN being Universe

for b

( b

( y in b

( x in UN & GO x,y ) ) );

:: 4b. Category of groups - morphisms

definition

let V be Group_DOMAIN;

ex b_{1} being GroupMorphism_DOMAIN st

for x being object holds

( x in b_{1} iff ex G, H being strict Element of V st x is strict Morphism of G,H )

for b_{1}, b_{2} being GroupMorphism_DOMAIN st ( for x being object holds

( x in b_{1} iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being object holds

( x in b_{2} iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) holds

b_{1} = b_{2}

end;
func Morphs V -> GroupMorphism_DOMAIN means :Def23: :: GRCAT_1:def 25

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 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 );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def23 defines Morphs GRCAT_1:def 25 :

for V being Group_DOMAIN

for b_{2} being GroupMorphism_DOMAIN holds

( b_{2} = Morphs V iff for x being object holds

( x in b_{2} iff ex G, H being strict Element of V st x is strict Morphism of G,H ) );

for V being Group_DOMAIN

for b

( b

( x in b

::

:: 4c. Category of groups - dom,cod,id

::

:: 4c. Category of groups - dom,cod,id

::

definition

let V be Group_DOMAIN;

let F be Element of Morphs V;

:: original: dom

redefine func dom F -> strict Element of V;

coherence

dom F is strict Element of V

redefine func cod F -> strict Element of V;

coherence

cod F is strict Element of V

end;
let F be Element of Morphs V;

:: original: dom

redefine func dom F -> strict Element of V;

coherence

dom F is strict Element of V

proof end;

:: original: codredefine func cod F -> strict Element of V;

coherence

cod F is strict Element of V

proof end;

definition

let V be Group_DOMAIN;

let G be Element of V;

coherence

ID G is strict Element of Morphs V

end;
let G be Element of V;

coherence

ID G is strict Element of Morphs V

proof end;

:: deftheorem defines ID GRCAT_1:def 26 :

for V being Group_DOMAIN

for G being Element of V holds ID G = ID G;

for V being Group_DOMAIN

for G being Element of V holds ID G = ID G;

definition

let V be Group_DOMAIN;

ex b_{1} being Function of (Morphs V),V st

for f being Element of Morphs V holds b_{1} . f = dom f

for b_{1}, b_{2} being Function of (Morphs V),V st ( for f being Element of Morphs V holds b_{1} . f = dom f ) & ( for f being Element of Morphs V holds b_{2} . f = dom f ) holds

b_{1} = b_{2}

ex b_{1} being Function of (Morphs V),V st

for f being Element of Morphs V holds b_{1} . f = cod f

for b_{1}, b_{2} being Function of (Morphs V),V st ( for f being Element of Morphs V holds b_{1} . f = cod f ) & ( for f being Element of Morphs V holds b_{2} . f = cod f ) holds

b_{1} = b_{2}

end;
func dom V -> Function of (Morphs V),V means :Def25: :: GRCAT_1:def 27

for f being Element of Morphs V holds it . f = dom f;

existence for f being Element of Morphs V holds it . f = dom f;

ex b

for f being Element of Morphs V holds b

proof end;

uniqueness for b

b

proof end;

func cod V -> Function of (Morphs V),V means :Def26: :: GRCAT_1:def 28

for f being Element of Morphs V holds it . f = cod f;

existence for f being Element of Morphs V holds it . f = cod f;

ex b

for f being Element of Morphs V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def25 defines dom GRCAT_1:def 27 :

for V being Group_DOMAIN

for b_{2} being Function of (Morphs V),V holds

( b_{2} = dom V iff for f being Element of Morphs V holds b_{2} . f = dom f );

for V being Group_DOMAIN

for b

( b

:: deftheorem Def26 defines cod GRCAT_1:def 28 :

for V being Group_DOMAIN

for b_{2} being Function of (Morphs V),V holds

( b_{2} = cod V iff for f being Element of Morphs V holds b_{2} . f = cod f );

for V being Group_DOMAIN

for b

( b

::

:: 4d. Category of groups - superposition

::

:: 4d. Category of groups - superposition

::

theorem Th31: :: GRCAT_1:31

for V being Group_DOMAIN

for g, f being Element of Morphs V st dom g = cod f holds

ex G1, G2, G3 being strict Element of V st

( g is Morphism of G2,G3 & f is Morphism of G1,G2 )

for g, f being Element of Morphs V st dom g = cod f holds

ex G1, G2, G3 being strict Element of V st

( g is Morphism of G2,G3 & f is Morphism of G1,G2 )

proof end;

theorem Th32: :: GRCAT_1:32

for V being Group_DOMAIN

for g, f being Element of Morphs V st dom g = cod f holds

g * f in Morphs V

for g, f being Element of Morphs V st dom g = cod f holds

g * f in Morphs V

proof end;

definition

let V be Group_DOMAIN;

ex b_{1} being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st

( ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{1} iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{1} holds

b_{1} . (g,f) = g * f ) )

for b_{1}, b_{2} being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{1} iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{1} holds

b_{1} . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{2} iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{2} holds

b_{2} . (g,f) = g * f ) holds

b_{1} = b_{2}

end;
func comp V -> PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) means :Def27: :: GRCAT_1:def 29

( ( 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 ( ( 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 ) );

ex b

( ( for g, f being Element of Morphs V holds

( [g,f] in dom b

b

proof end;

uniqueness for b

( [g,f] in dom b

b

( [g,f] in dom b

b

b

proof end;

:: deftheorem Def27 defines comp GRCAT_1:def 29 :

for V being Group_DOMAIN

for b_{2} being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds

( b_{2} = comp V iff ( ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{2} iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{2} holds

b_{2} . (g,f) = g * f ) ) );

for V being Group_DOMAIN

for b

( b

( [g,f] in dom b

b

::

:: 4e. Definition of Category of groups

::

:: 4e. Definition of Category of groups

::

definition

let UN be Universe;

CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #) is non empty non void strict CatStr ;

end;
func GroupCat UN -> non empty non void strict CatStr equals :: GRCAT_1:def 30

CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #);

coherence CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #);

CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #) is non empty non void strict CatStr ;

:: deftheorem defines GroupCat GRCAT_1:def 30 :

for UN being Universe holds GroupCat UN = CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #);

for UN being Universe holds GroupCat UN = CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #);

registration

let UN be Universe;

coherence

( GroupCat UN is strict & not GroupCat UN is void & not GroupCat UN is empty ) ;

end;
coherence

( GroupCat UN is strict & not GroupCat UN is void & not GroupCat UN is empty ) ;

theorem Th33: :: GRCAT_1:33

for UN being Universe

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) holds

( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f )

proof end;

theorem Th34: :: GRCAT_1:34

for UN being Universe

for f being Morphism of (GroupCat UN)

for f9 being Element of Morphs (GroupObjects UN)

for b being Object of (GroupCat UN)

for 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) )

for f being Morphism of (GroupCat UN)

for f9 being Element of Morphs (GroupObjects UN)

for b being Object of (GroupCat UN)

for 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 end;

::$CT

theorem Th35: :: GRCAT_1:36

for UN being Universe

for f, g being Morphism of (GroupCat UN)

for f9, g9 being Element of Morphs (GroupObjects UN) st f = f9 & g = g9 holds

( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )

for f, g being Morphism of (GroupCat UN)

for f9, g9 being Element of Morphs (GroupObjects UN) st f = f9 & g = g9 holds

( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )

proof end;

Lm1: for UN being Universe

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 end;

registration

let UN be Universe;

coherence

( GroupCat UN is reflexive & GroupCat UN is Category-like )

end;
coherence

( GroupCat UN is reflexive & GroupCat UN is Category-like )

proof end;

Lm2: for UN being Universe

for a being Element of (GroupCat UN)

for aa being Element of GroupObjects UN st a = aa holds

for i being Morphism of a,a st i = ID aa holds

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 end;

registration

let UN be Universe;

coherence

( GroupCat UN is transitive & GroupCat UN is associative & GroupCat UN is with_identities )

end;
coherence

( GroupCat UN is transitive & GroupCat UN is associative & GroupCat UN is with_identities )

proof end;

definition

let UN be Universe;

{ G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } is Subset of the carrier of (GroupCat UN)

end;
func AbGroupObjects UN -> Subset of the carrier of (GroupCat UN) equals :: GRCAT_1:def 31

{ G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } ;

coherence { G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } ;

{ G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } is Subset of the carrier of (GroupCat UN)

proof end;

:: deftheorem defines AbGroupObjects GRCAT_1:def 31 :

for UN being Universe holds AbGroupObjects UN = { G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } ;

for UN being Universe holds AbGroupObjects UN = { G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } ;

definition
end;

:: deftheorem defines AbGroupCat GRCAT_1:def 32 :

for UN being Universe holds AbGroupCat UN = cat (AbGroupObjects UN);

for UN being Universe holds AbGroupCat UN = cat (AbGroupObjects UN);

registration
end;

theorem :: GRCAT_1:38

:: 6. Subcategory of groups with the operator of 1/2

definition

let UN be Universe;

{ G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } is Subset of the carrier of (AbGroupCat UN)

end;
func MidOpGroupObjects UN -> Subset of the carrier of (AbGroupCat UN) equals :: GRCAT_1:def 33

{ G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ;

coherence { G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ;

{ G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } is Subset of the carrier of (AbGroupCat UN)

proof end;

:: deftheorem defines MidOpGroupObjects GRCAT_1:def 33 :

for UN being Universe holds MidOpGroupObjects UN = { G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ;

for UN being Universe holds MidOpGroupObjects UN = { G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ;

definition

let UN be Universe;

cat (MidOpGroupObjects UN) is Subcategory of AbGroupCat UN ;

end;
func MidOpGroupCat UN -> Subcategory of AbGroupCat UN equals :: GRCAT_1:def 34

cat (MidOpGroupObjects UN);

coherence cat (MidOpGroupObjects UN);

cat (MidOpGroupObjects UN) is Subcategory of AbGroupCat UN ;

:: deftheorem defines MidOpGroupCat GRCAT_1:def 34 :

for UN being Universe holds MidOpGroupCat UN = cat (MidOpGroupObjects UN);

for UN being Universe holds MidOpGroupCat UN = cat (MidOpGroupObjects UN);

registration
end;

theorem :: GRCAT_1:39

theorem :: GRCAT_1:41

for S, T being non empty 1-sorted

for f being Function of S,T st f is one-to-one & f is onto holds

( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto )

for f being Function of S,T st f is one-to-one & f is onto holds

( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto )

proof end;

theorem :: GRCAT_1:42

for UN being Universe

for a being Object of (GroupCat UN)

for aa being Element of GroupObjects UN st a = aa holds

id a = ID aa

for a being Object of (GroupCat UN)

for aa being Element of GroupObjects UN st a = aa holds

id a = ID aa

proof end;