Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Category Ens

by
Czeslaw Bylinski

MML identifier: ENS_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_2, TARSKI, FRAENKEL, FUNCT_1, BOOLE, MCART_1, RELAT_1, CAT_1,
PARTFUN1, QC_LANG1, CLASSES2, FUNCOP_1, FUNCT_4, CAT_2, OPPCAT_1,
FUNCT_5, ENS_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, DOMAIN_1, RELAT_1,
FUNCT_1, FUNCT_2, PARTFUN1, FUNCT_4, FUNCT_5, FRAENKEL, CLASSES2,
FUNCOP_1, CAT_1, CAT_2, OPPCAT_1;
constructors DOMAIN_1, CLASSES2, CAT_2, OPPCAT_1, PARTFUN1, MEMBERED,
XBOOLE_0;
clusters RELAT_1, FUNCT_1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, FUNCT_2,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: Mappings

reserve V for non empty set, A,B,A',B' for Element of V;

definition let V;
func Funcs(V) -> set equals
:: ENS_1:def 1
union { Funcs(A,B): not contradiction };
end;

definition let V;
cluster Funcs(V) -> functional non empty;
end;

theorem :: ENS_1:1
for f being set holds f in Funcs(V) iff
ex A,B st (B={} implies A={}) & f is Function of A,B;

theorem :: ENS_1:2
Funcs(A,B) c= Funcs(V);

theorem :: ENS_1:3
for W be non empty Subset of V holds Funcs W c= Funcs V;

reserve f,f' for Element of Funcs(V);

definition let V;
func Maps(V) -> set equals
:: ENS_1:def 2
{ [[A,B],f]: (B={} implies A={}) & f is Function of A,B};
end;

definition let V;
cluster Maps(V) -> non empty;
end;

reserve m,m1,m2,m3,m' for Element of Maps V;

theorem :: ENS_1:4
ex f,A,B st m = [[A,B],f] & (B = {} implies A = {}) & f is Function of A,B;

theorem :: ENS_1:5
for f being Function of A,B st B={} implies A={} holds [[A,B],f] in Maps V;

theorem :: ENS_1:6
Maps V c= [:[:V,V:],Funcs V:];

theorem :: ENS_1:7
for W be non empty Subset of V holds Maps W c= Maps V;

definition let V be non empty set, m be Element of Maps V;
cluster m`2 -> Function-like Relation-like;
end;

definition let V,m;
canceled;

func dom m -> Element of V equals
:: ENS_1:def 4
m`1`1;
func cod m -> Element of V equals
:: ENS_1:def 5
m`1`2;
end;

theorem :: ENS_1:8
m = [[dom m,cod m],m`2];

theorem :: ENS_1:9
(cod m <> {} or dom m = {}) & m`2 is Function of dom m,cod m;

theorem :: ENS_1:10
for f being Function, A,B being set st [[A,B],f] in Maps(V) holds
(B = {} implies A = {}) & f is Function of A,B;

definition let V,A;
func id\$ A -> Element of Maps V equals
:: ENS_1:def 6
[[A,A],id A];
end;

theorem :: ENS_1:11
(id\$ A)`2 = id A & dom id\$ A = A & cod id\$ A = A;

definition let V,m1,m2;
assume  cod m1 = dom m2;
func m2*m1 -> Element of Maps V equals
:: ENS_1:def 7
[[dom m1,cod m2],m2`2*m1`2];
end;

theorem :: ENS_1:12
dom m2 = cod m1 implies
(m2*m1)`2 = m2`2*m1`2 & dom(m2*m1) = dom m1 & cod(m2*m1) = cod m2;

theorem :: ENS_1:13
dom m2 = cod m1 & dom m3 = cod m2 implies m3*(m2*m1) = (m3*m2)*m1;

theorem :: ENS_1:14
m*(id\$ dom m) = m & (id\$ cod m)*m = m;

definition let V,A,B;
func Maps(A,B) -> set equals
:: ENS_1:def 8
{ [[A,B],f] where f is Element of Funcs V: [[A,B],f] in Maps V };
end;

theorem :: ENS_1:15
for f being Function of A,B st B = {} implies A = {}
holds [[A,B],f] in Maps(A,B);

theorem :: ENS_1:16
m in Maps(A,B) implies m = [[A,B],m`2];

theorem :: ENS_1:17
Maps(A,B) c= Maps V;

theorem :: ENS_1:18
Maps V = union { Maps(A,B): not contradiction };

theorem :: ENS_1:19
m in Maps(A,B) iff dom m = A & cod m = B;

theorem :: ENS_1:20
m in Maps(A,B) implies m`2 in Funcs(A,B);

definition let V,m;
attr m is surjective means
:: ENS_1:def 9
rng m`2 = cod(m);
synonym m is_a_surjection;
end;

begin  :: Category Ens

definition let V;
func fDom V -> Function of Maps V,V means
:: ENS_1:def 10
for m holds it.m = dom m;

func fCod V -> Function of Maps V,V means
:: ENS_1:def 11
for m holds it.m = cod m;

func fComp V -> PartFunc of [:Maps V,Maps V:],Maps V means
:: ENS_1:def 12

(for m2,m1 holds [m2,m1] in dom it iff dom m2 = cod m1) &
(for m2,m1 st dom m2 = cod m1 holds it.[m2,m1] = m2*m1);

func fId V -> Function of V,Maps V means
:: ENS_1:def 13
for A holds it.A = id\$ A;
end;

definition let V;
func Ens(V) -> CatStr equals
:: ENS_1:def 14
CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #);
end;

theorem :: ENS_1:21
CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) is Category;

definition let V;
cluster Ens(V) -> strict Category-like;
end;

reserve a,b for Object of Ens(V);

theorem :: ENS_1:22
A is Object of Ens(V);

definition let V,A;
func @A -> Object of Ens(V) equals
:: ENS_1:def 15
A;
end;

theorem :: ENS_1:23
a is Element of V;

definition let V,a;
func @a -> Element of V equals
:: ENS_1:def 16
a;
end;

reserve f,g,f1,f2 for Morphism of Ens(V);

theorem :: ENS_1:24
m is Morphism of Ens(V);

definition let V,m;
func @m -> Morphism of Ens(V) equals
:: ENS_1:def 17
m;
end;

theorem :: ENS_1:25
f is Element of Maps(V);

definition let V,f;
func @f -> Element of Maps(V) equals
:: ENS_1:def 18
f;
end;

theorem :: ENS_1:26
dom f = dom(@f) & cod f = cod(@f);

theorem :: ENS_1:27
Hom(a,b) = Maps(@a,@b);

theorem :: ENS_1:28
dom g = cod f implies g*f = (@g)*(@f);

theorem :: ENS_1:29
id a = id\$(@a);

theorem :: ENS_1:30
a = {} implies a is initial;

theorem :: ENS_1:31
{} in V & a is initial implies a = {};

theorem :: ENS_1:32
for W being Universe, a being Object of Ens(W) st a is initial
holds a = {};

theorem :: ENS_1:33
(ex x being set st a = {x}) implies a is terminal;

theorem :: ENS_1:34
V <> {{}} & a is terminal implies ex x being set st a = {x};

theorem :: ENS_1:35
for W being Universe, a being Object of Ens(W) st a is terminal
ex x being set st a = {x};

theorem :: ENS_1:36
f is monic iff (@f)`2 is one-to-one;

theorem :: ENS_1:37
f is epi & (ex A st ex x1,x2 being set st x1 in A & x2 in A & x1 <> x2)
implies @f is_a_surjection;

theorem :: ENS_1:38
@f is_a_surjection implies f is epi;

theorem :: ENS_1:39
for W being Universe, f being Morphism of Ens(W) st f is epi
holds @f is_a_surjection;

theorem :: ENS_1:40
for W being non empty Subset of V holds Ens(W) is_full_subcategory_of Ens(
V
);

begin :: Representable Functors

reserve C for Category, a,b,a',b',c for Object of C,
f,g,h,f',g' for Morphism of C;

definition let C;
func Hom(C) -> set equals
:: ENS_1:def 19
end;

definition let C;
cluster Hom(C) -> non empty;
end;

theorem :: ENS_1:41
Hom(a,b) in Hom(C)
;

:: hom-functors

theorem :: ENS_1:42
(Hom(a,cod f) = {} implies Hom(a,dom f) = {}) &
(Hom(dom f,a) = {} implies Hom(cod f,a) = {});

definition let C,a,f;
func hom(a,f) -> Function of Hom(a,dom f),Hom(a,cod f) means
:: ENS_1:def 20
for g st g in Hom(a,dom f) holds it.g = f*g;

func hom(f,a) -> Function of Hom(cod f,a),Hom(dom f,a) means
:: ENS_1:def 21
for g st g in Hom(cod f,a) holds it.g = g*f;
end;

theorem :: ENS_1:43
hom(a,id c) = id Hom(a,c);

theorem :: ENS_1:44
hom(id c,a) = id Hom(c,a);

theorem :: ENS_1:45
dom g = cod f implies hom(a,g*f) = hom(a,g)*hom(a,f);

theorem :: ENS_1:46
dom g = cod f implies hom(g*f,a) = hom(f,a)*hom(g,a);

theorem :: ENS_1:47
[[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] is Element of Maps(Hom(C));

theorem :: ENS_1:48
[[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] is Element of Maps(Hom(C));

definition let C,a;
func hom?-(a) -> Function of the Morphisms of C, Maps(Hom(C)) means
:: ENS_1:def 22
for f holds it.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)];

func hom-?(a) -> Function of the Morphisms of C, Maps(Hom(C)) means
:: ENS_1:def 23
for f holds it.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
end;

theorem :: ENS_1:49
Hom(C) c= V implies hom?-(a) is Functor of C,Ens(V);

theorem :: ENS_1:50
Hom(C) c= V implies hom-?(a) is Contravariant_Functor of C,Ens(V);

:: hom-bifunctor

theorem :: ENS_1:51
Hom(dom f,cod f') = {} implies Hom(cod f,dom f') = {};

definition let C,f,g;
func hom(f,g) -> Function of Hom(cod f,dom g),Hom(dom f,cod g) means
:: ENS_1:def 24
for h st h in Hom(cod f,dom g) holds it.h = g*h*f;
end;

theorem :: ENS_1:52
[[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] is Element of Maps(Hom(C));

theorem :: ENS_1:53
hom(id a,f) = hom(a,f) & hom(f,id a) = hom(f,a);

theorem :: ENS_1:54
hom(id a,id b) = id Hom(a,b);

theorem :: ENS_1:55
hom(f,g) = hom(dom f,g)*hom(f,dom g);

theorem :: ENS_1:56
cod g = dom f & dom g' = cod f' implies hom(f*g,g'*f') = hom(g,g')*hom(f,f');

definition let C;
func hom??(C) -> Function of the Morphisms of [:C,C:], Maps(Hom(C)) means
:: ENS_1:def 25
for f,g holds it.[f,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)]
;
end;

theorem :: ENS_1:57
hom?-(a) = (curry (hom??(C))).(id a) & hom-?(a) = (curry' (hom??(C))).(id a)
;

theorem :: ENS_1:58
Hom(C) c= V implies hom??(C) is Functor of [:C opp,C:],Ens(V);

definition let V,C,a;
assume  Hom(C) c= V;
func hom?-(V,a) -> Functor of C,Ens(V) equals
:: ENS_1:def 26
hom?-(a);
func hom-?(V,a) -> Contravariant_Functor of C,Ens(V) equals
:: ENS_1:def 27
hom-?(a);
end;

definition let V,C;
assume  Hom(C) c= V;
func hom??(V,C) -> Functor of [:C opp,C:],Ens(V) equals
:: ENS_1:def 28
hom??(C);
end;

theorem :: ENS_1:59
Hom(C) c= V implies (hom?-(V,a)).f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)]
;

theorem :: ENS_1:60
Hom(C) c= V implies (Obj (hom?-(V,a))).b = Hom(a,b);

theorem :: ENS_1:61
Hom(C) c= V implies (hom-?(V,a)).f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)]
;

theorem :: ENS_1:62
Hom(C) c= V implies (Obj (hom-?(V,a))).b = Hom(b,a);

theorem :: ENS_1:63
Hom(C) c= V
implies hom??(V,C).[f opp,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)]
;

theorem :: ENS_1:64
Hom(C) c= V implies (Obj (hom??(V,C))).[a opp,b] = Hom(a,b);

theorem :: ENS_1:65
Hom(C) c= V implies hom??(V,C)?-(a opp) = hom?-(V,a);

theorem :: ENS_1:66
Hom(C) c= V implies hom??(V,C)-?a = hom-?(V,a);
```