:: by Czes{\l}aw Byli\'nski

::

:: Received August 1, 1991

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

definition

let V be non empty set ;

union { (Funcs (A,B)) where A, B is Element of V : verum } is set ;

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

union { (Funcs (A,B)) where A, B is Element of V : verum } is set ;

:: 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 } ;

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

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

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;

definition

let V be non empty set ;

{ [[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;
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 ) } ;

{ [[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 ;

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

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

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

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;

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;

coherence

for b_{1} being set st b_{1} = m `2 holds

( b_{1} is Function-like & b_{1} is Relation-like )

end;
let m be Element of Maps V;

coherence

for b

( b

proof end;

definition

let V be non empty set ;

let m be Element of Maps V;

coherence

(m `1) `1 is Element of V

(m `1) `2 is Element of V

end;
let m be Element of Maps V;

coherence

(m `1) `1 is Element of V

proof end;

coherence (m `1) `2 is Element of V

proof end;

:: deftheorem defines dom ENS_1:def 3 :

for V being non empty set

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

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 4 :

for V being non empty set

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

for V being non empty set

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

Lm2: for V being non empty set

for m, m9 being Element of Maps V st m `2 = m9 `2 & dom m = dom m9 & cod m = cod m9 holds

m = m9

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

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 )

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;

coherence

[[A,A],(id A)] is Element of Maps V by Th5;

end;
let A be Element of V;

coherence

[[A,A],(id A)] is Element of Maps V by Th5;

:: deftheorem defines id$ ENS_1:def 5 :

for V being non empty set

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

for V being non empty set

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

theorem :: ENS_1:11

definition

let V be non empty set ;

let m1, m2 be Element of Maps V;

assume A1: cod m1 = dom m2 ;

[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of Maps V

end;
let m1, m2 be Element of Maps V;

assume A1: cod m1 = dom m2 ;

func m2 * m1 -> Element of Maps V equals :Def6: :: ENS_1:def 6

[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];

coherence [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];

[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of Maps V

proof end;

:: deftheorem Def6 defines * ENS_1:def 6 :

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

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 m1, m2 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 )

for m1, m2 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 m1, m2, m3 being Element of Maps V st dom m2 = cod m1 & dom m3 = cod m2 holds

m3 * (m2 * m1) = (m3 * m2) * m1

for m1, m2, 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 )

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;

coherence

{ [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } is set ;

;

end;
let A, B be Element of V;

func Maps (A,B) -> set equals :: ENS_1:def 7

{ [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } ;

correctness { [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } ;

coherence

{ [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } is set ;

;

:: deftheorem defines Maps ENS_1:def 7 :

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

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)

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

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;

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

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)

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 A9, B9 being Element of V st A = A9 & B = B9 holds

Maps (A,B) = Maps (A9,B9)

proof end;

:: deftheorem defines surjective ENS_1:def 8 :

for V being non empty set

for m being Element of Maps V holds

( m is surjective iff rng (m `2) = cod m );

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 ;

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

for m being Element of Maps V holds b_{1} . m = dom m

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

b_{1} = b_{2}

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

for m being Element of Maps V holds b_{1} . m = cod m

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

b_{1} = b_{2}

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

( ( for m2, m1 being Element of Maps V holds

( [m2,m1] in dom b_{1} iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds

b_{1} . [m2,m1] = m2 * m1 ) )

for b_{1}, b_{2} being PartFunc of [:(Maps V),(Maps V):],(Maps V) st ( for m2, m1 being Element of Maps V holds

( [m2,m1] in dom b_{1} iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds

b_{1} . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of Maps V holds

( [m2,m1] in dom b_{2} iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds

b_{2} . [m2,m1] = m2 * m1 ) holds

b_{1} = b_{2}

end;
func fDom V -> Function of (Maps V),V means :Def9: :: ENS_1:def 9

for m being Element of Maps V holds it . m = dom m;

existence for m being Element of Maps V holds it . m = dom m;

ex b

for m being Element of Maps V holds b

proof end;

uniqueness for b

b

proof end;

func fCod V -> Function of (Maps V),V means :Def10: :: ENS_1:def 10

for m being Element of Maps V holds it . m = cod m;

existence for m being Element of Maps V holds it . m = cod m;

ex b

for m being Element of Maps V holds b

proof end;

uniqueness for b

b

proof end;

func fComp V -> PartFunc of [:(Maps V),(Maps V):],(Maps V) means :Def11: :: ENS_1:def 11

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

ex b

( ( for m2, m1 being Element of Maps V holds

( [m2,m1] in dom b

b

proof end;

uniqueness for b

( [m2,m1] in dom b

b

( [m2,m1] in dom b

b

b

proof end;

:: deftheorem Def9 defines fDom ENS_1:def 9 :

for V being non empty set

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

( b_{2} = fDom V iff for m being Element of Maps V holds b_{2} . m = dom m );

for V being non empty set

for b

( b

:: deftheorem Def10 defines fCod ENS_1:def 10 :

for V being non empty set

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

( b_{2} = fCod V iff for m being Element of Maps V holds b_{2} . m = cod m );

for V being non empty set

for b

( b

:: deftheorem Def11 defines fComp ENS_1:def 11 :

for V being non empty set

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

( b_{2} = fComp V iff ( ( for m2, m1 being Element of Maps V holds

( [m2,m1] in dom b_{2} iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds

b_{2} . [m2,m1] = m2 * m1 ) ) );

for V being non empty set

for b

( b

( [m2,m1] in dom b

b

definition

let V be non empty set ;

CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #) is non empty non void strict CatStr ;

end;
func Ens V -> non empty non void strict CatStr equals :: ENS_1:def 13

CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #);

coherence CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #);

CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #) is non empty non void strict CatStr ;

:: deftheorem defines Ens ENS_1:def 13 :

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

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

registration

let V be non empty set ;

( Ens V is Category-like & Ens V is reflexive & Ens V is transitive & Ens V is associative & Ens V is with_identities )

end;
cluster Ens V -> non empty non void strict Category-like transitive associative reflexive with_identities ;

coherence ( Ens V is Category-like & Ens V is reflexive & Ens V is transitive & Ens V is associative & Ens V is with_identities )

proof end;

::$CT

theorem :: ENS_1:22

:: deftheorem defines @ ENS_1:def 14 :

for V being non empty set

for A being Element of V holds @ A = A;

for V being non empty set

for A being Element of V holds @ A = A;

theorem :: ENS_1:23

:: deftheorem defines @ ENS_1:def 15 :

for V being non empty set

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

for V being non empty set

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

theorem :: ENS_1:24

definition
end;

:: deftheorem defines @ ENS_1:def 16 :

for V being non empty set

for m being Element of Maps V holds @ m = m;

for V being non empty set

for m being Element of Maps V holds @ m = m;

theorem :: ENS_1:25

definition
end;

:: deftheorem defines @ ENS_1:def 17 :

for V being non empty set

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

for V being non empty set

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

theorem :: ENS_1:26

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 Th27: :: ENS_1:28

for V being non empty set

for f, g being Morphism of (Ens V) st dom g = cod f holds

g (*) f = (@ g) * (@ f)

for f, g being Morphism of (Ens V) st dom g = cod f holds

g (*) f = (@ g) * (@ f)

proof end;

theorem :: ENS_1:32

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

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

a is terminal

proof end;

theorem Th33: :: 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}

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:36

for V being non empty set

for a, b being Object of (Ens V)

for f being Morphism of a,b st Hom (a,b) <> {} holds

( f is monic iff (@ f) `2 is one-to-one )

for a, b being Object of (Ens V)

for f being Morphism of a,b st Hom (a,b) <> {} holds

( f is monic iff (@ f) `2 is one-to-one )

proof end;

theorem Th36: :: ENS_1:37

for V being non empty set

for a, b being Object of (Ens V)

for f being Morphism of a,b st Hom (a,b) <> {} & 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

for a, b being Object of (Ens V)

for f being Morphism of a,b st Hom (a,b) <> {} & 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 a, b being Object of (Ens V) st Hom (a,b) <> {} holds

for f being Morphism of a,b st @ f is surjective holds

f is epi

for a, b being Object of (Ens V) st Hom (a,b) <> {} holds

for f being Morphism of a,b st @ f is surjective holds

f is epi

proof end;

theorem :: ENS_1:39

for W being Universe

for a, b being Object of (Ens W) st Hom (a,b) <> {} holds

for f being Morphism of a,b st f is epi holds

@ f is surjective

for a, b being Object of (Ens W) st Hom (a,b) <> {} holds

for f being Morphism of a,b st f is epi holds

@ f is surjective

proof end;

Lm7: for V being non empty set

for W being non empty Subset of V holds Ens W is Subcategory of Ens V

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

for W being non empty Subset of V holds Ens W is full Subcategory of Ens V

proof end;

definition
end;

:: deftheorem defines Hom ENS_1:def 18 :

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

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

registration
end;

:: hom-functors

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) = {} ) )

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;

ex b_{1} 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_{1} . g = f (*) g

for b_{1}, b_{2} 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_{1} . g = f (*) g ) & ( for g being Morphism of C st g in Hom (a,(dom f)) holds

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

b_{1} = b_{2}

ex b_{1} 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_{1} . g = g (*) f

for b_{1}, b_{2} 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_{1} . g = g (*) f ) & ( for g being Morphism of C st g in Hom ((cod f),a) holds

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

b_{1} = b_{2}

end;
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 :Def18: :: ENS_1:def 19

for g being Morphism of C st g in Hom (a,(dom f)) holds

it . g = f (*) g;

existence for g being Morphism of C st g in Hom (a,(dom f)) holds

it . g = f (*) g;

ex b

for g being Morphism of C st g in Hom (a,(dom f)) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func hom (f,a) -> Function of (Hom ((cod f),a)),(Hom ((dom f),a)) means :Def19: :: ENS_1:def 20

for g being Morphism of C st g in Hom ((cod f),a) holds

it . g = g (*) f;

existence for g being Morphism of C st g in Hom ((cod f),a) holds

it . g = g (*) f;

ex b

for g being Morphism of C st g in Hom ((cod f),a) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def18 defines hom ENS_1:def 19 :

for C being Category

for a being Object of C

for f being Morphism of C

for b_{4} being Function of (Hom (a,(dom f))),(Hom (a,(cod f))) holds

( b_{4} = hom (a,f) iff for g being Morphism of C st g in Hom (a,(dom f)) holds

b_{4} . g = f (*) g );

for C being Category

for a being Object of C

for f being Morphism of C

for b

( b

b

:: deftheorem Def19 defines hom ENS_1:def 20 :

for C being Category

for a being Object of C

for f being Morphism of C

for b_{4} being Function of (Hom ((cod f),a)),(Hom ((dom f),a)) holds

( b_{4} = hom (f,a) iff for g being Morphism of C st g in Hom ((cod f),a) holds

b_{4} . g = g (*) f );

for C being Category

for a being Object of C

for f being Morphism of C

for b

( b

b

theorem Th44: :: ENS_1:45

for C being Category

for a being Object of C

for f, g being Morphism of C st dom g = cod f holds

hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))

for a being Object of C

for f, g being Morphism of C st dom g = cod f holds

hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))

proof end;

theorem Th45: :: ENS_1:46

for C being Category

for a being Object of C

for f, g being Morphism of C st dom g = cod f holds

hom ((g (*) f),a) = (hom (f,a)) * (hom (g,a))

for a being Object of C

for f, g being Morphism of C st dom g = cod f holds

hom ((g (*) f),a) = (hom (f,a)) * (hom (g,a))

proof end;

theorem Th46: :: 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)

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 Th47: :: 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)

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;

ex b_{1} being Function of the carrier' of C,(Maps (Hom C)) st

for f being Morphism of C holds b_{1} . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]

for b_{1}, b_{2} being Function of the carrier' of C,(Maps (Hom C)) st ( for f being Morphism of C holds b_{1} . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ) & ( for f being Morphism of C holds b_{2} . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ) holds

b_{1} = b_{2}

ex b_{1} being Function of the carrier' of C,(Maps (Hom C)) st

for f being Morphism of C holds b_{1} . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]

for b_{1}, b_{2} being Function of the carrier' of C,(Maps (Hom C)) st ( for f being Morphism of C holds b_{1} . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ) & ( for f being Morphism of C holds b_{2} . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ) holds

b_{1} = b_{2}

end;
let a be Object of C;

func hom?- a -> Function of the carrier' of C,(Maps (Hom C)) means :Def20: :: ENS_1:def 21

for f being Morphism of C holds it . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))];

existence for f being Morphism of C holds it . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))];

ex b

for f being Morphism of C holds b

proof end;

uniqueness for b

b

proof end;

func hom-? a -> Function of the carrier' of C,(Maps (Hom C)) means :Def21: :: ENS_1:def 22

for f being Morphism of C holds it . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))];

existence for f being Morphism of C holds it . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))];

ex b

for f being Morphism of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def20 defines hom?- ENS_1:def 21 :

for C being Category

for a being Object of C

for b_{3} being Function of the carrier' of C,(Maps (Hom C)) holds

( b_{3} = hom?- a iff for f being Morphism of C holds b_{3} . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] );

for C being Category

for a being Object of C

for b

( b

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

for C being Category

for a being Object of C

for b_{3} being Function of the carrier' of C,(Maps (Hom C)) holds

( b_{3} = hom-? a iff for f being Morphism of C holds b_{3} . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] );

for C being Category

for a being Object of C

for b

( b

Lm8: 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;

Lm9: 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;

Lm10: 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 (c,a) holds

(hom-? a) . (id c) = id d

proof end;

theorem Th48: :: 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

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 Th49: :: 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

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;

:: hom-bifunctor

theorem Th50: :: ENS_1:51

for C being Category

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

Hom ((cod f),(dom f9)) = {}

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

Hom ((cod f),(dom f9)) = {}

proof end;

definition

let C be Category;

let f, g be Morphism of C;

ex b_{1} 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_{1} . h = (g (*) h) (*) f

for b_{1}, b_{2} 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_{1} . h = (g (*) h) (*) f ) & ( for h being Morphism of C st h in Hom ((cod f),(dom g)) holds

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

b_{1} = b_{2}

end;
let f, g be Morphism of C;

func hom (f,g) -> Function of (Hom ((cod f),(dom g))),(Hom ((dom f),(cod g))) means :Def22: :: ENS_1:def 23

for h being Morphism of C st h in Hom ((cod f),(dom g)) holds

it . h = (g (*) h) (*) f;

existence for h being Morphism of C st h in Hom ((cod f),(dom g)) holds

it . h = (g (*) h) (*) f;

ex b

for h being Morphism of C st h in Hom ((cod f),(dom g)) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def22 defines hom ENS_1:def 23 :

for C being Category

for f, g being Morphism of C

for b_{4} being Function of (Hom ((cod f),(dom g))),(Hom ((dom f),(cod g))) holds

( b_{4} = hom (f,g) iff for h being Morphism of C st h in Hom ((cod f),(dom g)) holds

b_{4} . h = (g (*) h) (*) f );

for C being Category

for f, g being Morphism of C

for b

( b

b

theorem Th51: :: 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)

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 Th52: :: 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) )

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

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

proof end;

theorem Th55: :: ENS_1:56

for C being Category

for f, g, f9, g9 being Morphism of C st cod g = dom f & dom g9 = cod f9 holds

hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))

for f, g, f9, g9 being Morphism of C st cod g = dom f & dom g9 = cod f9 holds

hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))

proof end;

definition

let C be Category;

ex b_{1} being Function of the carrier' of [:C,C:],(Maps (Hom C)) st

for f, g being Morphism of C holds b_{1} . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]

for b_{1}, b_{2} being Function of the carrier' of [:C,C:],(Maps (Hom C)) st ( for f, g being Morphism of C holds b_{1} . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ) & ( for f, g being Morphism of C holds b_{2} . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ) holds

b_{1} = b_{2}

end;
func hom?? C -> Function of the carrier' of [:C,C:],(Maps (Hom C)) means :Def23: :: ENS_1:def 24

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 for f, g being Morphism of C holds it . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))];

ex b

for f, g being Morphism of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def23 defines hom?? ENS_1:def 24 :

for C being Category

for b_{2} being Function of the carrier' of [:C,C:],(Maps (Hom C)) holds

( b_{2} = hom?? C iff for f, g being Morphism of C holds b_{2} . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] );

for C being Category

for b

( b

theorem Th56: :: 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) )

for a being Object of C holds

( hom?- a = (curry (hom?? C)) . (id a) & hom-? a = (curry' (hom?? C)) . (id a) )

proof end;

Lm11: 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 Th57: :: 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

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 ;

coherence

hom?- a is Functor of C, Ens V by A1, Th48;

coherence

hom-? a is Contravariant_Functor of C, Ens V by A1, Th49;

end;
let C be Category;

let a be Object of C;

assume A1: Hom C c= V ;

coherence

hom?- a is Functor of C, Ens V by A1, Th48;

coherence

hom-? a is Contravariant_Functor of C, Ens V by A1, Th49;

:: deftheorem Def24 defines hom?- ENS_1:def 25 :

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;

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

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 ;

coherence

hom?? C is Functor of [:(C opp),C:], Ens V by A1, Th57;

end;
let C be Category;

assume A1: Hom C c= V ;

coherence

hom?? C is Functor of [:(C opp),C:], Ens V by A1, Th57;

:: deftheorem Def26 defines hom?? ENS_1:def 27 :

for V being non empty set

for C being Category st Hom C c= V holds

hom?? (V,C) = hom?? C;

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

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)

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

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)

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

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)

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)

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)

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;