:: Category Ens
:: by Czes{\l}aw Byli\'nski
::
:: Received August 1, 1991
:: Copyright (c) 1991 Association of Mizar Users

definition

let V be non empty set ;
func Funcs V -> set equals :: ENS_1:def 1
union { (Funcs A,B) where A, B is Element of V : verum } ;
coherence
union { (Funcs A,B) where A, B is Element of V : verum } is set ;

end;

:: deftheorem defines Funcs ENS_1:def 1 :

for V being non empty set holds Funcs V = union { (Funcs A,B) where A, B is Element of V : verum } ;

registration

let V be non empty set ;
cluster Funcs V -> functional non empty ;
coherence
( Funcs V is functional & not Funcs V is empty )

proof end;

end;

theorem Th1: :: ENS_1:1

for V being non empty set
for f being set holds
( f in Funcs V iff ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) )

proof end;

theorem :: ENS_1:2

for V being non empty set
for A, B being Element of V holds Funcs A,B c= Funcs V

proof end;

theorem Th3: :: ENS_1:3

for V being non empty set
for W being non empty Subset of V holds Funcs W c= Funcs V

proof end;

definition

let V be non empty set ;
func Maps V -> set equals :: ENS_1:def 2
{ [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } ;
coherence
{ [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } is set ;

end;

:: deftheorem defines Maps ENS_1:def 2 :

for V being non empty set holds Maps V = { [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } ;

registration

let V be non empty set ;
cluster Maps V -> non empty ;
coherence
not Maps V is empty

proof end;

end;

theorem Th4: :: ENS_1:4

for V being non empty set
for m being Element of Maps V ex f being Element of Funcs V ex A, B being Element of V st
( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B )

proof end;

theorem Th5: :: ENS_1:5

for V being non empty set
for A, B being Element of V
for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps V

proof end;

theorem :: ENS_1:6

for V being non empty set holds Maps V c= [:[:V,V:],(Funcs V):]

proof end;

theorem Th7: :: ENS_1:7

for V being non empty set
for W being non empty Subset of V holds Maps W c= Maps V

proof end;

Lm1: for x1, y1, x2, y2, x3, y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds
( x1 = y1 & x2 = y2 )

proof end;

registration

let V be non empty set ;
let m be Element of Maps V;
cluster m `2 -> Relation-like Function-like ;
coherence
( m `2 is Function-like & m `2 is Relation-like )

proof end;

end;

definition

let V be non empty set ;
let m be Element of Maps V;
canceled;
func dom m -> Element of V equals :: ENS_1:def 4
(m `1 ) `1 ;
coherence
(m `1 ) `1 is Element of V

proof end;

func cod m -> Element of V equals :: ENS_1:def 5
(m `1 ) `2 ;
coherence
(m `1 ) `2 is Element of V

proof end;

end;

:: deftheorem ENS_1:def 3 :

canceled;

:: deftheorem defines dom ENS_1:def 4 :

for V being non empty set
for m being Element of Maps V holds dom m = (m `1 ) `1 ;

:: deftheorem defines cod ENS_1:def 5 :

for V being non empty set
for m being Element of Maps V holds cod m = (m `1 ) `2 ;

theorem Th8: :: ENS_1:8

for V being non empty set
for m being Element of Maps V holds m = [[(dom m),(cod m)],(m `2 )]

proof end;

Lm2: for V being non empty set
for m, m' being Element of Maps V st m `2 = m' `2 & dom m = dom m' & cod m = cod m' holds
m = m'

proof end;

theorem Th9: :: ENS_1:9

for V being non empty set
for m being Element of Maps V holds
( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) )

proof end;

Lm3: for V being non empty set
for m being Element of Maps V holds
( dom (m `2 ) = dom m & rng (m `2 ) c= cod m )

proof end;

theorem Th10: :: ENS_1:10

for V being non empty set
for f being Function
for A, B being set st [[A,B],f] in Maps V holds
( ( B = {} implies A = {} ) & f is Function of A,B )

proof end;

definition

let V be non empty set ;
let A be Element of V;
func id$ A -> Element of Maps V equals :: ENS_1:def 6
[[A,A],(id A)];
coherence
[[A,A],(id A)] is Element of Maps V by Th5;

end;

:: deftheorem defines id$ ENS_1:def 6 :

for V being non empty set
for A being Element of V holds id$ A = [[A,A],(id A)];

theorem Th11: :: ENS_1:11

for V being non empty set
for A being Element of V holds
( (id$ A) `2 = id A & dom (id$ A) = A & cod (id$ A) = A )

proof end;

definition

let V be non empty set ;
let m1, m2 be Element of Maps V;
assume A1: cod m1 = dom m2 ;
func m2 * m1 -> Element of Maps V equals :Def7: :: ENS_1:def 7
[[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))];
coherence
[[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))] is Element of Maps V

proof end;

end;

:: deftheorem Def7 defines * ENS_1:def 7 :

for V being non empty set
for m1, m2 being Element of Maps V st cod m1 = dom m2 holds
m2 * m1 = [[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))];

theorem Th12: :: ENS_1:12

for V being non empty set
for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
( (m2 * m1) `2 = (m2 `2 ) * (m1 `2 ) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )

proof end;

theorem Th13: :: ENS_1:13

for V being non empty set
for m2, m1, m3 being Element of Maps V st dom m2 = cod m1 & dom m3 = cod m2 holds
m3 * (m2 * m1) = (m3 * m2) * m1

proof end;

theorem Th14: :: ENS_1:14

for V being non empty set
for m being Element of Maps V holds
( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )

proof end;

definition

let V be non empty set ;
let A, B be Element of V;
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 } ;
correctness
coherence
{ [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } is set ;
;

end;

:: deftheorem defines Maps ENS_1:def 8 :

for V being non empty set
for A, B being Element of V holds Maps A,B = { [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } ;

theorem Th15: :: ENS_1:15

for V being non empty set
for A, B being Element of V
for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps A,B

proof end;

theorem Th16: :: ENS_1:16

for V being non empty set
for A, B being Element of V
for m being Element of Maps V st m in Maps A,B holds
m = [[A,B],(m `2 )]

proof end;

theorem Th17: :: ENS_1:17

for V being non empty set
for A, B being Element of V holds Maps A,B c= Maps V

proof end;

Lm4: for V being non empty set
for A, B being Element of V
for f being Function st [[A,B],f] in Maps A,B holds
( ( B = {} implies A = {} ) & f is Function of A,B )

proof end;

theorem :: ENS_1:18

for V being non empty set holds Maps V = union { (Maps A,B) where A, B is Element of V : verum }

proof end;

theorem Th19: :: ENS_1:19

for V being non empty set
for A, B being Element of V
for m being Element of Maps V holds
( m in Maps A,B iff ( dom m = A & cod m = B ) )

proof end;

theorem Th20: :: ENS_1:20

for V being non empty set
for A, B being Element of V
for m being Element of Maps V st m in Maps A,B holds
m `2 in Funcs A,B

proof end;

Lm5: for V being non empty set
for W being non empty Subset of V
for A, B being Element of W
for A', B' being Element of V st A = A' & B = B' holds
Maps A,B = Maps A',B'

proof end;

definition

let V be non empty set ;
let m be Element of Maps V;
attr m is surjective means :: ENS_1:def 9
rng (m `2 ) = cod m;

end;

:: deftheorem defines surjective ENS_1:def 9 :

for V being non empty set
for m being Element of Maps V holds
( m is surjective iff rng (m `2 ) = cod m );

definition

let V be non empty set ;
func fDom V -> Function of (Maps V),V means :Def10: :: ENS_1:def 10
for m being Element of Maps V holds it . m = dom m;
existence
ex b₁ being Function of (Maps V),V st
for m being Element of Maps V holds b₁ . m = dom m

proof end;

uniqueness
for b₁, b₂ being Function of (Maps V),V st ( for m being Element of Maps V holds b₁ . m = dom m ) & ( for m being Element of Maps V holds b₂ . m = dom m ) holds
b₁ = b₂

proof end;

func fCod V -> Function of (Maps V),V means :Def11: :: ENS_1:def 11
for m being Element of Maps V holds it . m = cod m;
existence
ex b₁ being Function of (Maps V),V st
for m being Element of Maps V holds b₁ . m = cod m

proof end;

uniqueness
for b₁, b₂ being Function of (Maps V),V st ( for m being Element of Maps V holds b₁ . m = cod m ) & ( for m being Element of Maps V holds b₂ . m = cod m ) holds
b₁ = b₂

proof end;

func fComp V -> PartFunc of [:(Maps V),(Maps V):],(Maps V) means :Def12: :: ENS_1:def 12
( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom it iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
it . [m2,m1] = m2 * m1 ) );
existence
ex b₁ being PartFunc of [:(Maps V),(Maps V):],(Maps V) st
( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b₁ iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b₁ . [m2,m1] = m2 * m1 ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of [:(Maps V),(Maps V):],(Maps V) st ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b₁ iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b₁ . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b₂ iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b₂ . [m2,m1] = m2 * m1 ) holds
b₁ = b₂

proof end;

func fId V -> Function of V,(Maps V) means :Def13: :: ENS_1:def 13
for A being Element of V holds it . A = id$ A;
existence
ex b₁ being Function of V,(Maps V) st
for A being Element of V holds b₁ . A = id$ A

proof end;

uniqueness
for b₁, b₂ being Function of V,(Maps V) st ( for A being Element of V holds b₁ . A = id$ A ) & ( for A being Element of V holds b₂ . A = id$ A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines fDom ENS_1:def 10 :

for V being non empty set
for b₂ being Function of (Maps V),V holds
( b₂ = fDom V iff for m being Element of Maps V holds b₂ . m = dom m );

:: deftheorem Def11 defines fCod ENS_1:def 11 :

for V being non empty set
for b₂ being Function of (Maps V),V holds
( b₂ = fCod V iff for m being Element of Maps V holds b₂ . m = cod m );

:: deftheorem Def12 defines fComp ENS_1:def 12 :

for V being non empty set
for b₂ being PartFunc of [:(Maps V),(Maps V):],(Maps V) holds
( b₂ = fComp V iff ( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b₂ iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b₂ . [m2,m1] = m2 * m1 ) ) );

:: deftheorem Def13 defines fId ENS_1:def 13 :

for V being non empty set
for b₂ being Function of V,(Maps V) holds
( b₂ = fId V iff for A being Element of V holds b₂ . A = id$ A );

definition

let V be non empty set ;
func Ens V -> CatStr equals :: ENS_1:def 14
CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #);
coherence
CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #) is CatStr ;

end;

:: deftheorem defines Ens ENS_1:def 14 :

for V being non empty set holds Ens V = CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #);

theorem Th21: :: ENS_1:21

for V being non empty set holds CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #) is Category

proof end;

registration

let V be non empty set ;
cluster Ens V -> non empty non void strict Category-like ;
coherence
( Ens V is strict & Ens V is Category-like & not Ens V is void & not Ens V is empty ) by Th21;

end;

theorem :: ENS_1:22

for V being non empty set
for A being Element of V holds A is Object of (Ens V) ;

definition

let V be non empty set ;
let A be Element of V;
func @ A -> Object of (Ens V) equals :: ENS_1:def 15
A;
coherence
A is Object of (Ens V) ;

end;

:: deftheorem defines @ ENS_1:def 15 :

for V being non empty set
for A being Element of V holds @ A = A;

theorem :: ENS_1:23

for V being non empty set
for a being Object of (Ens V) holds a is Element of V ;

definition

let V be non empty set ;
let a be Object of (Ens V);
func @ a -> Element of V equals :: ENS_1:def 16
a;
coherence
a is Element of V ;

end;

:: deftheorem defines @ ENS_1:def 16 :

for V being non empty set
for a being Object of (Ens V) holds @ a = a;

theorem :: ENS_1:24

for V being non empty set
for m being Element of Maps V holds m is Morphism of (Ens V) ;

definition

let V be non empty set ;
let m be Element of Maps V;
func @ m -> Morphism of (Ens V) equals :: ENS_1:def 17
m;
coherence
m is Morphism of (Ens V) ;

end;

:: deftheorem defines @ ENS_1:def 17 :

for V being non empty set
for m being Element of Maps V holds @ m = m;

theorem :: ENS_1:25

for V being non empty set
for f being Morphism of (Ens V) holds f is Element of Maps V ;

definition

let V be non empty set ;
let f be Morphism of (Ens V);
func @ f -> Element of Maps V equals :: ENS_1:def 18
f;
coherence
f is Element of Maps V ;

end;

:: deftheorem defines @ ENS_1:def 18 :

for V being non empty set
for f being Morphism of (Ens V) holds @ f = f;

theorem :: ENS_1:26

for V being non empty set
for f being Morphism of (Ens V) holds
( dom f = dom (@ f) & cod f = cod (@ f) ) by Def10, Def11;

theorem Th27: :: ENS_1:27

for V being non empty set
for a, b being Object of (Ens V) holds Hom a,b = Maps (@ a),(@ b)

proof end;

Lm6: for V being non empty set
for a, b being Object of (Ens V) st Hom a,b <> {} holds
Funcs (@ a),(@ b) <> {}

proof end;

theorem Th28: :: ENS_1:28

for V being non empty set
for g, f being Morphism of (Ens V) st dom g = cod f holds
g * f = (@ g) * (@ f)

proof end;

theorem :: ENS_1:29

for V being non empty set
for a being Object of (Ens V) holds id a = id$ (@ a) by Def13;

theorem :: ENS_1:30

for V being non empty set
for a being Object of (Ens V) st a = {} holds
a is initial

proof end;

theorem Th31: :: ENS_1:31

for V being non empty set
for a being Object of (Ens V) st {} in V & a is initial holds
a = {}

proof end;

theorem :: ENS_1:32

for W being Universe
for a being Object of (Ens W) st a is initial holds
a = {} by Th31, CLASSES2:62;

theorem :: ENS_1:33

for V being non empty set
for a being Object of (Ens V) st ex x being set st a = {x} holds
a is terminal

proof end;

theorem Th34: :: ENS_1:34

for V being non empty set
for a being Object of (Ens V) st V <> {{} } & a is terminal holds
ex x being set st a = {x}

proof end;

theorem :: ENS_1:35

for W being Universe
for a being Object of (Ens W) st a is terminal holds
ex x being set st a = {x}

proof end;

theorem :: ENS_1:36

for V being non empty set
for f being Morphism of (Ens V) holds
( f is monic iff (@ f) `2 is one-to-one )

proof end;

theorem Th37: :: ENS_1:37

for V being non empty set
for f being Morphism of (Ens V) st f is epi & ex A being Element of V ex x1, x2 being set st
( x1 in A & x2 in A & x1 <> x2 ) holds
@ f is surjective

proof end;

theorem :: ENS_1:38

for V being non empty set
for f being Morphism of (Ens V) st @ f is surjective holds
f is epi

proof end;

theorem :: ENS_1:39

for W being Universe
for f being Morphism of (Ens W) st f is epi holds
@ f is surjective

proof end;

theorem :: ENS_1:40

for V being non empty set
for W being non empty Subset of V holds Ens W is_full_subcategory_of Ens V

proof end;

definition

let C be Category;
func Hom C -> set equals :: ENS_1:def 19
{ (Hom a,b) where a, b is Object of C : verum } ;
coherence
{ (Hom a,b) where a, b is Object of C : verum } is set ;

end;

:: deftheorem defines Hom ENS_1:def 19 :

for C being Category holds Hom C = { (Hom a,b) where a, b is Object of C : verum } ;

registration

let C be Category;
cluster Hom C -> non empty ;
coherence
not Hom C is empty

proof end;

end;

theorem :: ENS_1:41

for C being Category
for a, b being Object of C holds Hom a,b in Hom C ;

theorem :: ENS_1:42

for C being Category
for a being Object of C
for f being Morphism of C holds
( ( Hom a,(cod f) = {} implies Hom a,(dom f) = {} ) & ( Hom (dom f),a = {} implies Hom (cod f),a = {} ) )

proof end;

definition

let C be Category;
let a be Object of C;
let f be Morphism of C;
func hom a,f -> Function of (Hom a,(dom f)),(Hom a,(cod f)) means :Def20: :: ENS_1:def 20
for g being Morphism of C st g in Hom a,(dom f) holds
it . g = f * g;
existence
ex b₁ being Function of (Hom a,(dom f)),(Hom a,(cod f)) st
for g being Morphism of C st g in Hom a,(dom f) holds
b₁ . g = f * g

proof end;

uniqueness
for b₁, b₂ being Function of (Hom a,(dom f)),(Hom a,(cod f)) st ( for g being Morphism of C st g in Hom a,(dom f) holds
b₁ . g = f * g ) & ( for g being Morphism of C st g in Hom a,(dom f) holds
b₂ . g = f * g ) holds
b₁ = b₂

proof end;

func hom f,a -> Function of (Hom (cod f),a),(Hom (dom f),a) means :Def21: :: ENS_1:def 21
for g being Morphism of C st g in Hom (cod f),a holds
it . g = g * f;
existence
ex b₁ being Function of (Hom (cod f),a),(Hom (dom f),a) st
for g being Morphism of C st g in Hom (cod f),a holds
b₁ . g = g * f

proof end;

uniqueness
for b₁, b₂ being Function of (Hom (cod f),a),(Hom (dom f),a) st ( for g being Morphism of C st g in Hom (cod f),a holds
b₁ . g = g * f ) & ( for g being Morphism of C st g in Hom (cod f),a holds
b₂ . g = g * f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines hom ENS_1:def 20 :

for C being Category
for a being Object of C
for f being Morphism of C
for b₄ being Function of (Hom a,(dom f)),(Hom a,(cod f)) holds
( b₄ = hom a,f iff for g being Morphism of C st g in Hom a,(dom f) holds
b₄ . g = f * g );

:: deftheorem Def21 defines hom ENS_1:def 21 :

for C being Category
for a being Object of C
for f being Morphism of C
for b₄ being Function of (Hom (cod f),a),(Hom (dom f),a) holds
( b₄ = hom f,a iff for g being Morphism of C st g in Hom (cod f),a holds
b₄ . g = g * f );

theorem Th43: :: ENS_1:43

for C being Category
for a, c being Object of C holds hom a,(id c) = id (Hom a,c)

proof end;

theorem Th44: :: ENS_1:44

for C being Category
for c, a being Object of C holds hom (id c),a = id (Hom c,a)

proof end;

theorem Th45: :: ENS_1:45

for C being Category
for a being Object of C
for g, f being Morphism of C st dom g = cod f holds
hom a,(g * f) = (hom a,g) * (hom a,f)

proof end;

theorem Th46: :: ENS_1:46

for C being Category
for a being Object of C
for g, f being Morphism of C st dom g = cod f holds
hom (g * f),a = (hom f,a) * (hom g,a)

proof end;

theorem Th47: :: ENS_1:47

for C being Category
for a being Object of C
for f being Morphism of C holds [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)] is Element of Maps (Hom C)

proof end;

theorem Th48: :: ENS_1:48

for C being Category
for a being Object of C
for f being Morphism of C holds [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] is Element of Maps (Hom C)

proof end;

definition

let C be Category;
let a be Object of C;
func hom?- a -> Function of the carrier' of C,(Maps (Hom C)) means :Def22: :: ENS_1:def 22
for f being Morphism of C holds it . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)];
existence
ex b₁ being Function of the carrier' of C,(Maps (Hom C)) st
for f being Morphism of C holds b₁ . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)]

proof end;

uniqueness
for b₁, b₂ being Function of the carrier' of C,(Maps (Hom C)) st ( for f being Morphism of C holds b₁ . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)] ) & ( for f being Morphism of C holds b₂ . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)] ) holds
b₁ = b₂

proof end;

func hom-? a -> Function of the carrier' of C,(Maps (Hom C)) means :Def23: :: ENS_1:def 23
for f being Morphism of C holds it . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)];
existence
ex b₁ being Function of the carrier' of C,(Maps (Hom C)) st
for f being Morphism of C holds b₁ . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)]

proof end;

uniqueness
for b₁, b₂ being Function of the carrier' of C,(Maps (Hom C)) st ( for f being Morphism of C holds b₁ . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] ) & ( for f being Morphism of C holds b₂ . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines hom?- ENS_1:def 22 :

for C being Category
for a being Object of C
for b₃ being Function of the carrier' of C,(Maps (Hom C)) holds
( b₃ = hom?- a iff for f being Morphism of C holds b₃ . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)] );

:: deftheorem Def23 defines hom-? ENS_1:def 23 :

for C being Category
for a being Object of C
for b₃ being Function of the carrier' of C,(Maps (Hom C)) holds
( b₃ = hom-? a iff for f being Morphism of C holds b₃ . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] );

Lm7: for V being non empty set
for C being Category
for T being Function of the carrier' of C,(Maps (Hom C)) st Hom C c= V holds
T is Function of the carrier' of C,the carrier' of (Ens V)

proof end;

Lm8: for V being non empty set
for C being Category
for a, c being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom a,c holds
(hom?- a) . (id c) = id d

proof end;

Lm9: for V being non empty set
for C being Category
for c, a being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom c,a holds
(hom-? a) . (id c) = id d

proof end;

theorem Th49: :: ENS_1:49

for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom?- a is Functor of C, Ens V

proof end;

theorem Th50: :: ENS_1:50

for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom-? a is Contravariant_Functor of C, Ens V

proof end;

theorem Th51: :: ENS_1:51

for C being Category
for f, f' being Morphism of C st Hom (dom f),(cod f') = {} holds
Hom (cod f),(dom f') = {}

proof end;

definition

let C be Category;
let f, g be Morphism of C;
func hom f,g -> Function of (Hom (cod f),(dom g)),(Hom (dom f),(cod g)) means :Def24: :: ENS_1:def 24
for h being Morphism of C st h in Hom (cod f),(dom g) holds
it . h = (g * h) * f;
existence
ex b₁ being Function of (Hom (cod f),(dom g)),(Hom (dom f),(cod g)) st
for h being Morphism of C st h in Hom (cod f),(dom g) holds
b₁ . h = (g * h) * f

proof end;

uniqueness
for b₁, b₂ being Function of (Hom (cod f),(dom g)),(Hom (dom f),(cod g)) st ( for h being Morphism of C st h in Hom (cod f),(dom g) holds
b₁ . h = (g * h) * f ) & ( for h being Morphism of C st h in Hom (cod f),(dom g) holds
b₂ . h = (g * h) * f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def24 defines hom ENS_1:def 24 :

for C being Category
for f, g being Morphism of C
for b₄ being Function of (Hom (cod f),(dom g)),(Hom (dom f),(cod g)) holds
( b₄ = hom f,g iff for h being Morphism of C st h in Hom (cod f),(dom g) holds
b₄ . h = (g * h) * f );

theorem Th52: :: ENS_1:52

for C being Category
for f, g being Morphism of C holds [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] is Element of Maps (Hom C)

proof end;

theorem Th53: :: ENS_1:53

for C being Category
for a being Object of C
for f being Morphism of C holds
( hom (id a),f = hom a,f & hom f,(id a) = hom f,a )

proof end;

theorem Th54: :: ENS_1:54

for C being Category
for a, b being Object of C holds hom (id a),(id b) = id (Hom a,b)

proof end;

theorem :: ENS_1:55

for C being Category
for f, g being Morphism of C holds hom f,g = (hom (dom f),g) * (hom f,(dom g))

proof end;

theorem Th56: :: ENS_1:56

for C being Category
for g, f, g', f' being Morphism of C st cod g = dom f & dom g' = cod f' holds
hom (f * g),(g' * f') = (hom g,g') * (hom f,f')

proof end;

definition

let C be Category;
func hom?? C -> Function of the carrier' of [:C,C:],(Maps (Hom C)) means :Def25: :: ENS_1:def 25
for f, g being Morphism of C holds it . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)];
existence
ex b₁ being Function of the carrier' of [:C,C:],(Maps (Hom C)) st
for f, g being Morphism of C holds b₁ . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)]

proof end;

uniqueness
for b₁, b₂ being Function of the carrier' of [:C,C:],(Maps (Hom C)) st ( for f, g being Morphism of C holds b₁ . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] ) & ( for f, g being Morphism of C holds b₂ . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def25 defines hom?? ENS_1:def 25 :

for C being Category
for b₂ being Function of the carrier' of [:C,C:],(Maps (Hom C)) holds
( b₂ = hom?? C iff for f, g being Morphism of C holds b₂ . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] );

theorem Th57: :: ENS_1:57

for C being Category
for a being Object of C holds
( hom?- a = (curry (hom?? C)) . (id a) & hom-? a = (curry' (hom?? C)) . (id a) )

proof end;

Lm10: for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom a,b holds
(hom?? C) . [(id a),(id b)] = id d

proof end;

theorem Th58: :: ENS_1:58

for V being non empty set
for C being Category st Hom C c= V holds
hom?? C is Functor of [:(C opp ),C:], Ens V

proof end;

definition

let V be non empty set ;
let C be Category;
let a be Object of C;
assume A1: Hom C c= V ;
func hom?- V,a -> Functor of C, Ens V equals :Def26: :: ENS_1:def 26
hom?- a;
coherence
hom?- a is Functor of C, Ens V by A1, Th49;
func hom-? V,a -> Contravariant_Functor of C, Ens V equals :Def27: :: ENS_1:def 27
hom-? a;
coherence
hom-? a is Contravariant_Functor of C, Ens V by A1, Th50;

end;

:: deftheorem Def26 defines hom?- ENS_1:def 26 :

for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom?- V,a = hom?- a;

:: deftheorem Def27 defines hom-? ENS_1:def 27 :

for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom-? V,a = hom-? a;

definition

let V be non empty set ;
let C be Category;
assume A1: Hom C c= V ;
func hom?? V,C -> Functor of [:(C opp ),C:], Ens V equals :Def28: :: ENS_1:def 28
hom?? C;
coherence
hom?? C is Functor of [:(C opp ),C:], Ens V by A1, Th58;

end;

:: deftheorem Def28 defines hom?? ENS_1:def 28 :

for V being non empty set
for C being Category st Hom C c= V holds
hom?? V,C = hom?? C;

theorem :: ENS_1:59

for V being non empty set
for C being Category
for a being Object of C
for f being Morphism of C st Hom C c= V holds
(hom?- V,a) . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)]

proof end;

theorem :: ENS_1:60

for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom?- V,a)) . b = Hom a,b

proof end;

theorem :: ENS_1:61

for V being non empty set
for C being Category
for a being Object of C
for f being Morphism of C st Hom C c= V holds
(hom-? V,a) . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)]

proof end;

theorem :: ENS_1:62

for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom-? V,a)) . b = Hom b,a

proof end;

theorem :: ENS_1:63

for V being non empty set
for C being Category
for f, g being Morphism of C st Hom C c= V holds
(hom?? V,C) . [(f opp ),g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)]

proof end;

theorem :: ENS_1:64

for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom?? V,C)) . [(a opp ),b] = Hom a,b

proof end;

theorem :: ENS_1:65

for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
(hom?? V,C) ?- (a opp ) = hom?- V,a

proof end;

theorem :: ENS_1:66

for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
(hom?? V,C) -? a = hom-? V,a

proof end;