:: Categories of Groups
:: by Michal Muzalewski
::
:: Received October 3, 1991
:: Copyright (c) 1991-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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;
begin :: 0a. Auxiliary theorems: sets and universums
reserve x, y for set;
reserve D for non empty set;
reserve UN for Universe;
theorem :: GRCAT_1:1
for u1,u2,u3,u4 being Element of UN holds [u1,u2,u3] in UN & [u1,
u2,u3,u4] in UN;
:: 0c. Auxiliary theorems: Trivial Group
theorem :: GRCAT_1:2
op2.({},{}) = {} & op1.{} = {} & op0 = {};
theorem :: GRCAT_1:3
{{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN;
registration
cluster Trivial-addLoopStr -> midpoint_operator;
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 = {};
:: 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
:: GRCAT_1:def 1
union{Hom(a,b) where a
is Object of C,b is Object of C : a in O & b in O};
end;
registration
let C,O;
cluster Morphs(O) -> non empty;
end;
definition
let C,O;
func dom(O) -> Function of Morphs(O),O equals
:: GRCAT_1:def 2
(the Source of C)|Morphs(O);
func cod(O) -> Function of Morphs(O),O equals
:: GRCAT_1:def 3
(the Target of C)|Morphs(O);
func comp(O) -> PartFunc of [:Morphs(O),(Morphs(O)):],Morphs(O) equals
:: GRCAT_1:def 4
(the Comp of C)||Morphs(O);
::$CD
end;
definition
let C,O;
func cat(O) -> Subcategory of C equals
:: GRCAT_1:def 6
CatStr (# O,Morphs(O),dom(O),cod(O),comp(O)#);
end;
registration
let C,O;
cluster cat(O) -> strict;
end;
theorem :: GRCAT_1:5
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
:: GRCAT_1:def 7
(the carrier of G) --> 0.H;
end;
theorem :: GRCAT_1:6
comp Trivial-addLoopStr = op1;
registration
let G be non empty addMagma, H being right_zeroed non empty addLoopStr;
cluster ZeroMap(G,H) -> additive;
end;
registration
let G be non empty addMagma, H be right_zeroed non empty addLoopStr;
cluster additive for Function of G,H;
end;
theorem :: GRCAT_1:7
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;
registration
let G1 be non empty addMagma,
G2,G3 being right_zeroed non empty addLoopStr,
f being additive Function of G1, G2,
g being additive Function of G2, G3;
cluster g*f -> additive for Function of G1, G3;
end;
:: 1b. carrier of groups
reserve G,H for AddGroup;
definition
struct GroupMorphismStr (# Source,Target -> AddGroup, Fun -> Function of the
Source, the Target #);
end;
definition
::$CD
let f be GroupMorphismStr;
func dom(f) -> AddGroup equals
:: GRCAT_1:def 9
the Source of f;
func cod(f) -> AddGroup equals
:: GRCAT_1:def 10
the Target of f;
end;
definition
let f be GroupMorphismStr;
func fun(f) -> Function of dom(f),cod(f) equals
:: GRCAT_1:def 11
the Fun of f;
end;
theorem :: GRCAT_1:8
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
:: GRCAT_1:def 12
GroupMorphismStr(# G,H,ZeroMap(G,H)#);
end;
registration
let G,H;
cluster ZERO(G,H) -> strict;
end;
definition
let IT be GroupMorphismStr;
attr IT is GroupMorphism-like means
:: GRCAT_1:def 13
fun(IT) is additive;
end;
registration
cluster strict GroupMorphism-like for GroupMorphismStr;
end;
definition
mode GroupMorphism is GroupMorphism-like GroupMorphismStr;
end;
theorem :: GRCAT_1:9
for F being GroupMorphism holds the Fun of F is additive;
registration
let G,H;
cluster ZERO(G,H) -> GroupMorphism-like;
end;
definition
let G,H;
mode Morphism of G,H -> GroupMorphism means
:: GRCAT_1:def 14
dom(it) = G & cod(it) = H;
end;
registration
let G,H;
cluster strict for Morphism of G,H;
end;
theorem :: GRCAT_1:10
for f being strict GroupMorphismStr st dom(f) = G & cod(f) = H &
fun(f) is additive holds f is strict Morphism of G,H;
theorem :: GRCAT_1:11
for f being Function of G,H st f is additive holds
GroupMorphismStr (# G,H,f#) is strict Morphism of G,H;
registration let G be non empty addMagma;
cluster id G -> additive;
end;
definition
let G;
func ID G -> Morphism of G,G equals
:: GRCAT_1:def 15
GroupMorphismStr(# G,G,id G#);
end;
registration
let G;
cluster ID G -> strict;
end;
definition
let G,H;
redefine func ZERO(G,H) -> strict Morphism of G,H;
end;
theorem :: GRCAT_1:12
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;
theorem :: GRCAT_1:13
for F being strict Morphism of G,H ex f being Function of G,H st
F = GroupMorphismStr(# G,H,f#);
theorem :: GRCAT_1:14
for F being GroupMorphism ex G,H st F is Morphism of G,H;
theorem :: GRCAT_1:15
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;
theorem :: GRCAT_1:16
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;
definition
let G,F be GroupMorphism;
assume
dom(G) = cod(F);
func G*F -> strict GroupMorphism means
:: GRCAT_1:def 16
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#);
end;
theorem :: GRCAT_1:17
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;
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;
end;
theorem :: GRCAT_1:18
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#);
theorem :: GRCAT_1:19
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#);
theorem :: 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;
theorem :: GRCAT_1:21
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;
theorem :: 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;
theorem :: GRCAT_1:23
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;
:: 2. Sourceains of groups
definition
let IT be set;
attr IT is Group_DOMAIN-like means
:: GRCAT_1:def 17
for x being object st x in IT holds x is strict AddGroup;
end;
registration
cluster Group_DOMAIN-like non empty for set;
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;
end;
registration
let V;
cluster strict for Element of V;
end;
:: 3. Domains of morphisms
definition
let IT be set;
attr IT is GroupMorphism_DOMAIN-like means
:: GRCAT_1:def 18
for x being object st x in IT holds x is strict GroupMorphism;
end;
registration
cluster GroupMorphism_DOMAIN-like non empty for set;
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;
end;
registration
let M be GroupMorphism_DOMAIN;
cluster strict for Element of M;
end;
theorem :: GRCAT_1:24
for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN;
definition
let G,H;
mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means
:: GRCAT_1:def 19
for x being Element of it holds x is strict Morphism of G,H;
end;
theorem :: GRCAT_1:25
D is GroupMorphism_DOMAIN of G,H iff for x being Element of D
holds x is strict Morphism of G,H;
theorem :: GRCAT_1:26
for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G, H;
definition
let G,H be 1-sorted;
mode MapsSet of G,H -> set means
:: GRCAT_1:def 20
for x being set st x in it holds x is Function of G,H;
end;
definition
let G,H be 1-sorted;
func Maps(G,H) -> MapsSet of G,H equals
:: GRCAT_1:def 21
Funcs(the carrier of G, the carrier
of H);
end;
registration
let G be 1-sorted, H be non empty 1-sorted;
cluster Maps(G,H) -> non empty;
end;
registration
let G be 1-sorted, H be non empty 1-sorted;
cluster non empty for MapsSet of G,H;
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;
end;
definition
let G,H;
func Morphs(G,H) -> GroupMorphism_DOMAIN of G,H means
:: GRCAT_1:def 22
for x being object holds x in it iff x is strict Morphism of G,H;
end;
definition
let G,H;
let M be GroupMorphism_DOMAIN of G,H;
redefine mode Element of M -> Morphism of G,H;
end;
registration
let G,H;
let M be GroupMorphism_DOMAIN of G,H;
cluster strict for Element of M;
end;
:: 4a. Category of groups - objects
definition
let x,y be object;
pred GO x,y means
:: GRCAT_1:def 23
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 :: GRCAT_1:27
for x,y1,y2 being object st GO x,y1 & GO x,y2 holds y1 = y2;
theorem :: GRCAT_1:28
ex x st x in UN & GO x,Trivial-addLoopStr;
definition
let UN;
func GroupObjects(UN) -> set means
:: GRCAT_1:def 24
for y being object holds y in it
iff ex x being object st x in UN & GO x,y;
end;
theorem :: GRCAT_1:29
Trivial-addLoopStr in GroupObjects(UN);
registration
let UN;
cluster GroupObjects(UN) -> non empty;
end;
theorem :: GRCAT_1:30
for x being Element of GroupObjects(UN) holds x is strict AddGroup;
registration
let UN;
cluster GroupObjects(UN) -> Group_DOMAIN-like;
end;
:: 4b. Category of groups - morphisms
definition
let V;
func Morphs(V) -> GroupMorphism_DOMAIN means
:: 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;
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;
redefine func cod(F) -> strict Element of V;
end;
definition
let V;
let G be Element of V;
func ID(G) -> strict Element of Morphs(V) equals
:: GRCAT_1:def 26
ID(G);
end;
definition
let V;
func dom(V) -> Function of Morphs(V),V means
:: GRCAT_1:def 27
for f being Element of Morphs(V) holds it.f = dom(f);
func cod(V) -> Function of Morphs(V),V means
:: GRCAT_1:def 28
for f being Element of Morphs(V) holds it.f = cod(f);
end;
::
:: 4d. Category of groups - superposition
::
theorem :: GRCAT_1:31
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
;
theorem :: GRCAT_1:32
for g,f being Element of Morphs(V) st dom(g) = cod(f) holds g*f in Morphs(V);
definition
let V;
func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means
:: 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;
end;
::
:: 4e. Definition of Category of groups
::
definition
let UN;
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))#);
end;
registration
let UN;
cluster GroupCat(UN) -> strict non void non empty;
end;
theorem :: GRCAT_1:33
for f,g being Morphism of GroupCat(UN) holds [g,f] in dom(the
Comp of GroupCat(UN)) iff dom g = cod f;
theorem :: GRCAT_1:34
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);
::$CT
theorem :: GRCAT_1:36
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);
registration
let UN;
cluster GroupCat UN -> reflexive Category-like;
end;
registration
let UN;
cluster GroupCat UN ->
transitive associative with_identities;
end;
definition
let UN;
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
};
end;
theorem :: GRCAT_1:37
Trivial-addLoopStr in AbGroupObjects(UN);
registration
let UN;
cluster AbGroupObjects(UN) -> non empty;
end;
definition
let UN;
func AbGroupCat UN -> Subcategory of GroupCat(UN) equals
:: GRCAT_1:def 32
cat AbGroupObjects UN;
end;
registration
let UN;
cluster AbGroupCat(UN) -> strict;
end;
theorem :: GRCAT_1:38
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
:: GRCAT_1:def 33
{G where G is Element of AbGroupCat(UN) : ex H being
midpoint_operator AbGroup st G = H};
end;
registration
let UN;
cluster MidOpGroupObjects(UN) -> non empty;
end;
definition
let UN;
func MidOpGroupCat UN -> Subcategory of AbGroupCat(UN) equals
:: GRCAT_1:def 34
cat MidOpGroupObjects UN;
end;
registration
let UN;
cluster MidOpGroupCat(UN) -> strict;
end;
theorem :: GRCAT_1:39
the carrier of MidOpGroupCat(UN) = MidOpGroupObjects(UN);
theorem :: GRCAT_1:40
Trivial-addLoopStr in MidOpGroupObjects(UN);
theorem :: GRCAT_1:41 :: 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;
theorem :: GRCAT_1:42
for a being Object of GroupCat(UN), aa being Element of
GroupObjects(UN) st a = aa holds id a = ID aa;