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

::

:: Received October 25, 1989

:: Copyright (c) 1990-2017 Association of Mizar Users

definition

attr c_{1} is strict ;

struct CatStr -> MultiGraphStruct ;

aggr CatStr(# carrier, carrier', Source, Target, Comp #) -> CatStr ;

sel Comp c_{1} -> PartFunc of [: the carrier' of c_{1}, the carrier' of c_{1}:], the carrier' of c_{1};

end;
struct CatStr -> MultiGraphStruct ;

aggr CatStr(# carrier, carrier', Source, Target, Comp #) -> CatStr ;

sel Comp c

definition

let C be CatStr ;

mode Object of C is Element of C;

mode Morphism of C is Element of the carrier' of C;

end;
mode Object of C is Element of C;

mode Morphism of C is Element of the carrier' of C;

:: Domain and codomain of a Morphism

registration
end;

definition

let C be CatStr ;

let f, g be Morphism of C;

assume A1: [g,f] in dom the Comp of C ;

coherence

the Comp of C . (g,f) is Morphism of C by A1, PARTFUN1:4;

end;
let f, g be Morphism of C;

assume A1: [g,f] in dom the Comp of C ;

coherence

the Comp of C . (g,f) is Morphism of C by A1, PARTFUN1:4;

:: deftheorem Def1 defines (*) CAT_1:def 1 :

for C being CatStr

for f, g being Morphism of C st [g,f] in dom the Comp of C holds

g (*) f = the Comp of C . (g,f);

for C being CatStr

for f, g being Morphism of C st [g,f] in dom the Comp of C holds

g (*) f = the Comp of C . (g,f);

definition

let C be non empty non void CatStr ;

let a, b be Object of C;

coherence

{ f where f is Morphism of C : ( dom f = a & cod f = b ) } is Subset of the carrier' of C;

end;
let a, b be Object of C;

func Hom (a,b) -> Subset of the carrier' of C equals :: CAT_1:def 4

{ f where f is Morphism of C : ( dom f = a & cod f = b ) } ;

correctness { f where f is Morphism of C : ( dom f = a & cod f = b ) } ;

coherence

{ f where f is Morphism of C : ( dom f = a & cod f = b ) } is Subset of the carrier' of C;

proof end;

:: deftheorem defines Hom CAT_1:def 4 :

for C being non empty non void CatStr

for a, b being Object of C holds Hom (a,b) = { f where f is Morphism of C : ( dom f = a & cod f = b ) } ;

for C being non empty non void CatStr

for a, b being Object of C holds Hom (a,b) = { f where f is Morphism of C : ( dom f = a & cod f = b ) } ;

theorem Th1: :: CAT_1:1

for C being non empty non void CatStr

for f being Morphism of C

for a, b being Object of C holds

( f in Hom (a,b) iff ( dom f = a & cod f = b ) )

for f being Morphism of C

for a, b being Object of C holds

( f in Hom (a,b) iff ( dom f = a & cod f = b ) )

proof end;

theorem :: CAT_1:2

definition

let C be non empty non void CatStr ;

let a, b be Object of C;

assume A1: Hom (a,b) <> {} ;

existence

ex b_{1} being Morphism of C st b_{1} in Hom (a,b)
by A1, SUBSET_1:4;

end;
let a, b be Object of C;

assume A1: Hom (a,b) <> {} ;

existence

ex b

:: deftheorem Def3 defines Morphism CAT_1:def 5 :

for C being non empty non void CatStr

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

for b_{4} being Morphism of C holds

( b_{4} is Morphism of a,b iff b_{4} in Hom (a,b) );

for C being non empty non void CatStr

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

for b

( b

::$CT

theorem Th4: :: CAT_1:5

for C being non empty non void CatStr

for a, b being Object of C

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

( dom f = a & cod f = b )

for a, b being Object of C

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

( dom f = a & cod f = b )

proof end;

theorem :: CAT_1:6

for C being non empty non void CatStr

for a, b, c, d being Object of C

for f being Morphism of a,b

for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds

( a = c & b = d )

for a, b, c, d being Object of C

for f being Morphism of a,b

for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds

( a = c & b = d )

proof end;

theorem Th6: :: CAT_1:7

for C being non empty non void CatStr

for a, b being Object of C

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

for g being Morphism of a,b holds f = g

for a, b being Object of C

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

for g being Morphism of a,b holds f = g

proof end;

theorem Th7: :: CAT_1:8

for C being non empty non void CatStr

for a, b being Object of C

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

Hom (a,b) = {f}

for a, b being Object of C

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

Hom (a,b) = {f}

proof end;

theorem :: CAT_1:9

for C being non empty non void CatStr

for a, b, c, d being Object of C

for f being Morphism of a,b st Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} holds

ex h being Morphism of c,d st Hom (c,d) = {h}

for a, b, c, d being Object of C

for f being Morphism of a,b st Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} holds

ex h being Morphism of c,d st Hom (c,d) = {h}

proof end;

:: Category

definition

let C be non empty non void CatStr ;

end;
attr C is Category-like means :Def4: :: CAT_1:def 6

for f, g being Morphism of C holds

( [g,f] in dom the Comp of C iff dom g = cod f );

for f, g being Morphism of C holds

( [g,f] in dom the Comp of C iff dom g = cod f );

attr C is transitive means :Def5: :: CAT_1:def 7

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

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

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

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

:: deftheorem Def4 defines Category-like CAT_1:def 6 :

for C being non empty non void CatStr holds

( C is Category-like iff for f, g being Morphism of C holds

( [g,f] in dom the Comp of C iff dom g = cod f ) );

for C being non empty non void CatStr holds

( C is Category-like iff for f, g being Morphism of C holds

( [g,f] in dom the Comp of C iff dom g = cod f ) );

:: deftheorem Def5 defines transitive CAT_1:def 7 :

for C being non empty non void CatStr holds

( C is transitive iff for f, g being Morphism of C st dom g = cod f holds

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

for C being non empty non void CatStr holds

( C is transitive iff for f, g being Morphism of C st dom g = cod f holds

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

:: deftheorem Def6 defines associative CAT_1:def 8 :

for C being non empty non void CatStr holds

( C is associative iff for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds

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

for C being non empty non void CatStr holds

( C is associative iff for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds

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

:: deftheorem Def7 defines reflexive CAT_1:def 9 :

for C being non empty non void CatStr holds

( C is reflexive iff for b being Element of C holds Hom (b,b) <> {} );

for C being non empty non void CatStr holds

( C is reflexive iff for b being Element of C holds Hom (b,b) <> {} );

:: deftheorem Def8 defines with_identities CAT_1:def 10 :

for C being non empty non void CatStr holds

( C is with_identities iff for a being Element of C ex i being Morphism of a,a st

for b being Element of C 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 ) ) );

for C being non empty non void CatStr holds

( C is with_identities iff for a being Element of C ex i being Morphism of a,a st

for b being Element of C 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 ) ) );

definition

let o, m be object ;

coherence

CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) is strict CatStr ;

;

end;
func 1Cat (o,m) -> strict CatStr equals :: CAT_1:def 11

CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);

correctness CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);

coherence

CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) is strict CatStr ;

;

:: deftheorem defines 1Cat CAT_1:def 11 :

for o, m being object holds 1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);

for o, m being object holds 1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);

registration

let o, m be object ;

coherence

( not 1Cat (o,m) is empty & 1Cat (o,m) is trivial & not 1Cat (o,m) is void & 1Cat (o,m) is trivial' ) ;

end;
coherence

( not 1Cat (o,m) is empty & 1Cat (o,m) is trivial & not 1Cat (o,m) is void & 1Cat (o,m) is trivial' ) ;

registration

coherence

for b_{1} being non empty non void CatStr st not b_{1} is empty & b_{1} is trivial holds

( b_{1} is transitive & b_{1} is reflexive )

end;
for b

( b

proof end;

registration

coherence

for b_{1} being non empty non void CatStr st not b_{1} is void & b_{1} is trivial' holds

( b_{1} is associative & b_{1} is with_identities )

end;
for b

( b

proof end;

registration

ex b_{1} being non empty non void CatStr st

( b_{1} is reflexive & b_{1} is transitive & b_{1} is associative & b_{1} is with_identities & b_{1} is Category-like & not b_{1} is void & not b_{1} is empty & b_{1} is strict )
end;

cluster non empty non void V62() strict Category-like transitive associative reflexive with_identities for CatStr ;

existence ex b

( b

proof end;

definition

mode Category is non empty non void Category-like transitive associative reflexive with_identities CatStr ;

end;
registration

let C be non empty non void reflexive CatStr ;

let a be Object of C;

coherence

not Hom (a,a) is empty by Def7;

end;
let a be Object of C;

coherence

not Hom (a,a) is empty by Def7;

theorem Th9: :: CAT_1:11

for o, m being set

for a, b being Object of (1Cat (o,m))

for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b)

for a, b being Object of (1Cat (o,m))

for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b)

proof end;

theorem :: CAT_1:12

for o, m being set

for a, b being Object of (1Cat (o,m))

for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b

for a, b being Object of (1Cat (o,m))

for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b

proof end;

theorem :: CAT_1:13

theorem :: CAT_1:14

for o, m being set

for a, b, c, d being Object of (1Cat (o,m))

for f being Morphism of a,b

for g being Morphism of c,d holds f = g

for a, b, c, d being Object of (1Cat (o,m))

for f being Morphism of a,b

for g being Morphism of c,d holds f = g

proof end;

theorem :: CAT_1:15

theorem Th14: :: CAT_1:16

for C being Category

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

g (*) f = the Comp of C . (g,f)

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

g (*) f = the Comp of C . (g,f)

proof end;

theorem :: CAT_1:17

theorem :: CAT_1:18

definition

let C be non empty non void reflexive with_identities CatStr ;

let a be Object of C;

ex b_{1} being Morphism of a,a st

for b being Object of C holds

( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b_{1} = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b_{1} (*) f = f ) )
by Def8;

uniqueness

for b_{1}, b_{2} being Morphism of a,a st ( for b being Object of C holds

( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b_{1} = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b_{1} (*) f = f ) ) ) & ( for b being Object of C holds

( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b_{2} = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b_{2} (*) f = f ) ) ) holds

b_{1} = b_{2}

end;
let a be Object of C;

func id a -> Morphism of a,a means :Def10: :: CAT_1:def 12

for b being Object of C holds

( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) it = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds it (*) f = f ) );

existence for b being Object of C holds

( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) it = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds it (*) f = f ) );

ex b

for b being Object of C holds

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

uniqueness

for b

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

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

b

proof end;

:: deftheorem Def10 defines id CAT_1:def 12 :

for C being non empty non void reflexive with_identities CatStr

for a being Object of C

for b_{3} being Morphism of a,a holds

( b_{3} = id a iff for b being Object of C holds

( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b_{3} = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b_{3} (*) f = f ) ) );

for C being non empty non void reflexive with_identities CatStr

for a being Object of C

for b

( b

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

::$CT 2

theorem :: CAT_1:21

for C being Category

for b being Object of C

for f being Morphism of C st cod f = b holds

(id b) (*) f = f

for b being Object of C

for f being Morphism of C st cod f = b holds

(id b) (*) f = f

proof end;

theorem :: CAT_1:22

for C being Category

for b being Object of C

for g being Morphism of C st dom g = b holds

g (*) (id b) = g

for b being Object of C

for g being Morphism of C st dom g = b holds

g (*) (id b) = g

proof end;

theorem Th19: :: CAT_1:23

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

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

g (*) f in Hom (a,c)

for a, b, c being Object of C

for f being Morphism of a,b

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

g (*) f in Hom (a,c)

proof end;

definition

let C be Category;

let a, b, c be Object of C;

let f be Morphism of a,b;

let g be Morphism of b,c;

assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ;

correctness

coherence

g (*) f is Morphism of a,c;

end;
let a, b, c be Object of C;

let f be Morphism of a,b;

let g be Morphism of b,c;

assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ;

correctness

coherence

g (*) f is Morphism of a,c;

proof end;

:: deftheorem Def11 defines * CAT_1:def 13 :

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

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

g * f = g (*) f;

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

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

g * f = g (*) f;

theorem :: CAT_1:24

theorem Th21: :: CAT_1:25

for C being Category

for a, b, c, d being Object of C

for f being Morphism of a,b

for g being Morphism of b,c

for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds

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

for a, b, c, d being Object of C

for f being Morphism of a,b

for g being Morphism of b,c

for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds

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

proof end;

::$CT

theorem Th23: :: CAT_1:28

for C being Category

for a, b being Object of C

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

(id b) * f = f

for a, b being Object of C

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

(id b) * f = f

proof end;

theorem Th24: :: CAT_1:29

for C being Category

for b, c being Object of C

for g being Morphism of b,c st Hom (b,c) <> {} holds

g * (id b) = g

for b, c being Object of C

for g being Morphism of b,c st Hom (b,c) <> {} holds

g * (id b) = g

proof end;

registration

let C be Category;

let a be Object of C;

let f be Morphism of a,a;

A1: Hom (a,a) <> {} ;

reducibility

f * (id a) = f by A1, Th24;

reducibility

(id a) * f = f by A1, Th23;

end;
let a be Object of C;

let f be Morphism of a,a;

A1: Hom (a,a) <> {} ;

reducibility

f * (id a) = f by A1, Th24;

reducibility

(id a) * f = f by A1, Th23;

:: Monics, Epis

:: deftheorem defines monic CAT_1:def 14 :

for C being Category

for b, c being Object of C

for g being Morphism of b,c holds

( g is monic iff ( Hom (b,c) <> {} & ( for a being Object of C st Hom (a,b) <> {} holds

for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds

f1 = f2 ) ) );

for C being Category

for b, c being Object of C

for g being Morphism of b,c holds

( g is monic iff ( Hom (b,c) <> {} & ( for a being Object of C st Hom (a,b) <> {} holds

for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds

f1 = f2 ) ) );

:: deftheorem defines epi CAT_1:def 15 :

for C being Category

for a, b being Object of C

for f being Morphism of a,b holds

( f is epi iff ( Hom (a,b) <> {} & ( for c being Object of C st Hom (b,c) <> {} holds

for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds

g1 = g2 ) ) );

for C being Category

for a, b being Object of C

for f being Morphism of a,b holds

( f is epi iff ( Hom (a,b) <> {} & ( for c being Object of C st Hom (b,c) <> {} holds

for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds

g1 = g2 ) ) );

:: deftheorem defines invertible CAT_1:def 16 :

for C being Category

for a, b being Object of C

for f being Morphism of a,b holds

( f is invertible iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st

( f * g = id b & g * f = id a ) ) );

for C being Category

for a, b being Object of C

for f being Morphism of a,b holds

( f is invertible iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st

( f * g = id b & g * f = id a ) ) );

theorem :: CAT_1:31

theorem :: CAT_1:32

for C being Category

for b, c, d being Object of C

for g being Morphism of b,c

for h being Morphism of c,d st g is monic & h is monic holds

h * g is monic

for b, c, d being Object of C

for g being Morphism of b,c

for h being Morphism of c,d st g is monic & h is monic holds

h * g is monic

proof end;

theorem :: CAT_1:33

for C being Category

for b, c, d being Object of C

for g being Morphism of b,c

for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds

g is monic

for b, c, d being Object of C

for g being Morphism of b,c

for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds

g is monic

proof end;

theorem :: CAT_1:34

for C being Category

for a, b being Object of C

for h being Morphism of a,b

for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds

g is monic

for a, b being Object of C

for h being Morphism of a,b

for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds

g is monic

proof end;

theorem :: CAT_1:36

theorem :: CAT_1:37

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st f is epi & g is epi holds

g * f is epi

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st f is epi & g is epi holds

g * f is epi

proof end;

theorem :: CAT_1:38

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds

g is epi

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds

g is epi

proof end;

theorem :: CAT_1:39

for C being Category

for a, b being Object of C

for h being Morphism of a,b

for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds

h is epi

for a, b being Object of C

for h being Morphism of a,b

for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds

h is epi

proof end;

theorem :: CAT_1:41

theorem Th37: :: CAT_1:42

for C being Category

for a, b being Object of C

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

for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds

g1 = g2

for a, b being Object of C

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

for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds

g1 = g2

proof end;

definition

let C be Category;

let a, b be Object of C;

let f be Morphism of a,b;

assume A1: f is invertible ;

existence

ex b_{1} being Morphism of b,a st

( f * b_{1} = id b & b_{1} * f = id a )
by A1;

uniqueness

for b_{1}, b_{2} being Morphism of b,a st f * b_{1} = id b & b_{1} * f = id a & f * b_{2} = id b & b_{2} * f = id a holds

b_{1} = b_{2}
by A1, Th37;

end;
let a, b be Object of C;

let f be Morphism of a,b;

assume A1: f is invertible ;

existence

ex b

( f * b

uniqueness

for b

b

:: deftheorem Def15 defines " CAT_1:def 17 :

for C being Category

for a, b being Object of C

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

for b_{5} being Morphism of b,a holds

( b_{5} = f " iff ( f * b_{5} = id b & b_{5} * f = id a ) );

for C being Category

for a, b being Object of C

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

for b

( b

theorem :: CAT_1:43

for C being Category

for a, b being Object of C

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

( f is monic & f is epi )

for a, b being Object of C

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

( f is monic & f is epi )

proof end;

theorem Th40: :: CAT_1:45

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st f is invertible & g is invertible holds

g * f is invertible

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st f is invertible & g is invertible holds

g * f is invertible

proof end;

theorem :: CAT_1:46

for C being Category

for a, b being Object of C

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

f " is invertible

for a, b being Object of C

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

f " is invertible

proof end;

theorem :: CAT_1:47

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st f is invertible & g is invertible holds

(g * f) " = (f ") * (g ")

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st f is invertible & g is invertible holds

(g * f) " = (f ") * (g ")

proof end;

definition

let C be Category;

let a be Object of C;

reflexivity

for a being Object of C ex f being Morphism of a,a st f is invertible

for a, b being Object of C st ex f being Morphism of a,b st f is invertible holds

ex f being Morphism of b,a st f is invertible

end;
let a be Object of C;

attr a is terminal means :: CAT_1:def 18

for b being Object of C holds

( Hom (b,a) <> {} & ex f being Morphism of b,a st

for g being Morphism of b,a holds f = g );

for b being Object of C holds

( Hom (b,a) <> {} & ex f being Morphism of b,a st

for g being Morphism of b,a holds f = g );

attr a is initial means :: CAT_1:def 19

for b being Object of C holds

( Hom (a,b) <> {} & ex f being Morphism of a,b st

for g being Morphism of a,b holds f = g );

let b be Object of C;for b being Object of C holds

( Hom (a,b) <> {} & ex f being Morphism of a,b st

for g being Morphism of a,b holds f = g );

reflexivity

for a being Object of C ex f being Morphism of a,a st f is invertible

proof end;

symmetry for a, b being Object of C st ex f being Morphism of a,b st f is invertible holds

ex f being Morphism of b,a st f is invertible

proof end;

:: deftheorem defines terminal CAT_1:def 18 :

for C being Category

for a being Object of C holds

( a is terminal iff for b being Object of C holds

( Hom (b,a) <> {} & ex f being Morphism of b,a st

for g being Morphism of b,a holds f = g ) );

for C being Category

for a being Object of C holds

( a is terminal iff for b being Object of C holds

( Hom (b,a) <> {} & ex f being Morphism of b,a st

for g being Morphism of b,a holds f = g ) );

:: deftheorem defines initial CAT_1:def 19 :

for C being Category

for a being Object of C holds

( a is initial iff for b being Object of C holds

( Hom (a,b) <> {} & ex f being Morphism of a,b st

for g being Morphism of a,b holds f = g ) );

for C being Category

for a being Object of C holds

( a is initial iff for b being Object of C holds

( Hom (a,b) <> {} & ex f being Morphism of a,b st

for g being Morphism of a,b holds f = g ) );

:: deftheorem defines are_isomorphic CAT_1:def 20 :

for C being Category

for a, b being Object of C holds

( a,b are_isomorphic iff ex f being Morphism of a,b st f is invertible );

for C being Category

for a, b being Object of C holds

( a,b are_isomorphic iff ex f being Morphism of a,b st f is invertible );

theorem :: CAT_1:48

for C being Category

for a, b being Object of C holds

( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st

( f * f9 = id b & f9 * f = id a ) ) )

for a, b being Object of C holds

( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st

( f * f9 = id b & f9 * f = id a ) ) )

proof end;

theorem :: CAT_1:49

for C being Category

for a being Object of C holds

( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )

for a being Object of C holds

( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )

proof end;

theorem Th45: :: CAT_1:50

for C being Category

for a being Object of C st a is initial holds

for h being Morphism of a,a holds id a = h

for a being Object of C st a is initial holds

for h being Morphism of a,a holds id a = h

proof end;

theorem :: CAT_1:51

for C being Category

for a, b being Object of C st a is initial & b is initial holds

a,b are_isomorphic

for a, b being Object of C st a is initial & b is initial holds

a,b are_isomorphic

proof end;

theorem :: CAT_1:52

for C being Category

for a, b being Object of C st a is initial & a,b are_isomorphic holds

b is initial

for a, b being Object of C st a is initial & a,b are_isomorphic holds

b is initial

proof end;

theorem :: CAT_1:53

for C being Category

for b being Object of C holds

( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )

for b being Object of C holds

( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )

proof end;

theorem Th49: :: CAT_1:54

for C being Category

for a being Object of C st a is terminal holds

for h being Morphism of a,a holds id a = h

for a being Object of C st a is terminal holds

for h being Morphism of a,a holds id a = h

proof end;

theorem :: CAT_1:55

for C being Category

for a, b being Object of C st a is terminal & b is terminal holds

a,b are_isomorphic

for a, b being Object of C st a is terminal & b is terminal holds

a,b are_isomorphic

proof end;

theorem :: CAT_1:56

for C being Category

for a, b being Object of C st b is terminal & a,b are_isomorphic holds

a is terminal

for a, b being Object of C st b is terminal & a,b are_isomorphic holds

a is terminal

proof end;

theorem :: CAT_1:57

for C being Category

for a, b being Object of C

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

f is monic

for a, b being Object of C

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

f is monic

proof end;

registration

let C be Category;

let a be Object of C;

reducibility

dom (id a) = a

cod (id a) = a

end;
let a be Object of C;

reducibility

dom (id a) = a

proof end;

reducibility cod (id a) = a

proof end;

theorem :: CAT_1:60

for C being Category

for a, b, c being Object of C st a,b are_isomorphic & b,c are_isomorphic holds

a,c are_isomorphic

for a, b, c being Object of C st a,b are_isomorphic & b,c are_isomorphic holds

a,c are_isomorphic

proof end;

:: Functors (Covariant Functors)

definition

let C, D be Category;

ex b_{1} being Function of the carrier' of C, the carrier' of D st

( ( for c being Element of C ex d being Element of D st b_{1} . (id c) = id d ) & ( for f being Element of the carrier' of C holds

( b_{1} . (id (dom f)) = id (dom (b_{1} . f)) & b_{1} . (id (cod f)) = id (cod (b_{1} . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds

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

end;
mode Functor of C,D -> Function of the carrier' of C, the carrier' of D means :Def19: :: CAT_1:def 21

( ( for c being Element of C ex d being Element of D st it . (id c) = id d ) & ( for f being Element of the carrier' of C holds

( it . (id (dom f)) = id (dom (it . f)) & it . (id (cod f)) = id (cod (it . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds

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

existence ( ( for c being Element of C ex d being Element of D st it . (id c) = id d ) & ( for f being Element of the carrier' of C holds

( it . (id (dom f)) = id (dom (it . f)) & it . (id (cod f)) = id (cod (it . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds

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

ex b

( ( for c being Element of C ex d being Element of D st b

( b

b

proof end;

:: deftheorem Def19 defines Functor CAT_1:def 21 :

for C, D being Category

for b_{3} being Function of the carrier' of C, the carrier' of D holds

( b_{3} is Functor of C,D iff ( ( for c being Element of C ex d being Element of D st b_{3} . (id c) = id d ) & ( for f being Element of the carrier' of C holds

( b_{3} . (id (dom f)) = id (dom (b_{3} . f)) & b_{3} . (id (cod f)) = id (cod (b_{3} . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds

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

for C, D being Category

for b

( b

( b

b

theorem Th56: :: CAT_1:61

for C, D being Category

for T being Function of the carrier' of C, the carrier' of D st ( for c being Object of C ex d being Object of D st T . (id c) = id d ) & ( for f being Morphism of C holds

( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

T . (g (*) f) = (T . g) (*) (T . f) ) holds

T is Functor of C,D

for T being Function of the carrier' of C, the carrier' of D st ( for c being Object of C ex d being Object of D st T . (id c) = id d ) & ( for f being Morphism of C holds

( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

T . (g (*) f) = (T . g) (*) (T . f) ) holds

T is Functor of C,D

proof end;

theorem :: CAT_1:62

theorem :: CAT_1:63

theorem Th59: :: CAT_1:64

for C, D being Category

for T being Functor of C,D

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

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

for T being Functor of C,D

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

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

proof end;

theorem Th60: :: CAT_1:65

for C, D being Category

for T being Function of the carrier' of C, the carrier' of D

for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds

( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

T . (g (*) f) = (T . g) (*) (T . f) ) holds

T is Functor of C,D

for T being Function of the carrier' of C, the carrier' of D

for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds

( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

T . (g (*) f) = (T . g) (*) (T . f) ) holds

T is Functor of C,D

proof end;

:: Object Function of a Functor

definition

let C, D be Category;

let F be Function of the carrier' of C, the carrier' of D;

assume A1: for c being Element of C ex d being Element of D st F . (id c) = id d ;

ex b_{1} being Function of the carrier of C, the carrier of D st

for c being Element of C

for d being Element of D st F . (id c) = id d holds

b_{1} . c = d

for b_{1}, b_{2} being Function of the carrier of C, the carrier of D st ( for c being Element of C

for d being Element of D st F . (id c) = id d holds

b_{1} . c = d ) & ( for c being Element of C

for d being Element of D st F . (id c) = id d holds

b_{2} . c = d ) holds

b_{1} = b_{2}

end;
let F be Function of the carrier' of C, the carrier' of D;

assume A1: for c being Element of C ex d being Element of D st F . (id c) = id d ;

func Obj F -> Function of the carrier of C, the carrier of D means :Def20: :: CAT_1:def 22

for c being Element of C

for d being Element of D st F . (id c) = id d holds

it . c = d;

existence for c being Element of C

for d being Element of D st F . (id c) = id d holds

it . c = d;

ex b

for c being Element of C

for d being Element of D st F . (id c) = id d holds

b

proof end;

uniqueness for b

for d being Element of D st F . (id c) = id d holds

b

for d being Element of D st F . (id c) = id d holds

b

b

proof end;

:: deftheorem Def20 defines Obj CAT_1:def 22 :

for C, D being Category

for F being Function of the carrier' of C, the carrier' of D st ( for c being Element of C ex d being Element of D st F . (id c) = id d ) holds

for b_{4} being Function of the carrier of C, the carrier of D holds

( b_{4} = Obj F iff for c being Element of C

for d being Element of D st F . (id c) = id d holds

b_{4} . c = d );

for C, D being Category

for F being Function of the carrier' of C, the carrier' of D st ( for c being Element of C ex d being Element of D st F . (id c) = id d ) holds

for b

( b

for d being Element of D st F . (id c) = id d holds

b

theorem :: CAT_1:66

theorem Th62: :: CAT_1:67

for C, D being Category

for T being Functor of C,D

for c being Object of C

for d being Object of D st T . (id c) = id d holds

(Obj T) . c = d

for T being Functor of C,D

for c being Object of C

for d being Object of D st T . (id c) = id d holds

(Obj T) . c = d

proof end;

theorem Th63: :: CAT_1:68

for C, D being Category

for T being Functor of C,D

for c being Object of C holds T . (id c) = id ((Obj T) . c)

for T being Functor of C,D

for c being Object of C holds T . (id c) = id ((Obj T) . c)

proof end;

theorem Th64: :: CAT_1:69

for C, D being Category

for T being Functor of C,D

for f being Morphism of C holds

( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )

for T being Functor of C,D

for f being Morphism of C holds

( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )

proof end;

definition

let C, D be Category;

let T be Functor of C,D;

let c be Object of C;

correctness

coherence

(Obj T) . c is Object of D;

;

end;
let T be Functor of C,D;

let c be Object of C;

correctness

coherence

(Obj T) . c is Object of D;

;

:: deftheorem defines . CAT_1:def 23 :

for C, D being Category

for T being Functor of C,D

for c being Object of C holds T . c = (Obj T) . c;

for C, D being Category

for T being Functor of C,D

for c being Object of C holds T . c = (Obj T) . c;

theorem :: CAT_1:70

theorem :: CAT_1:71

theorem :: CAT_1:72

theorem Th68: :: CAT_1:73

for B, C, D being Category

for T being Functor of B,C

for S being Functor of C,D holds S * T is Functor of B,D

for T being Functor of B,C

for S being Functor of C,D holds S * T is Functor of B,D

proof end;

:: Composition of Functors

definition

let B, C, D be Category;

let T be Functor of B,C;

let S be Functor of C,D;

:: original: *

redefine func S * T -> Functor of B,D;

coherence

T * S is Functor of B,D by Th68;

end;
let T be Functor of B,C;

let S be Functor of C,D;

:: original: *

redefine func S * T -> Functor of B,D;

coherence

T * S is Functor of B,D by Th68;

theorem Th70: :: CAT_1:75

for B, C, D being Category

for T being Functor of B,C

for S being Functor of C,D

for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)

for T being Functor of B,C

for S being Functor of C,D

for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)

proof end;

theorem :: CAT_1:76

:: Identity Functor

definition

let C, D be Category;

let T be Functor of C,D;

end;
let T be Functor of C,D;

attr T is isomorphic means :: CAT_1:def 25

( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D );

( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D );

:: deftheorem defines isomorphic CAT_1:def 25 :

for C, D being Category

for T being Functor of C,D holds

( T is isomorphic iff ( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D ) );

for C, D being Category

for T being Functor of C,D holds

( T is isomorphic iff ( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D ) );

:: deftheorem defines full CAT_1:def 26 :

for C, D being Category

for T being Functor of C,D holds

( T is full iff for c, c9 being Object of C st Hom ((T . c),(T . c9)) <> {} holds

for g being Morphism of T . c,T . c9 holds

( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) );

for C, D being Category

for T being Functor of C,D holds

( T is full iff for c, c9 being Object of C st Hom ((T . c),(T . c9)) <> {} holds

for g being Morphism of T . c,T . c9 holds

( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) );

:: deftheorem defines faithful CAT_1:def 27 :

for C, D being Category

for T being Functor of C,D holds

( T is faithful iff for c, c9 being Object of C st Hom (c,c9) <> {} holds

for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds

f1 = f2 );

for C, D being Category

for T being Functor of C,D holds

( T is faithful iff for c, c9 being Object of C st Hom (c,c9) <> {} holds

for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds

f1 = f2 );

theorem Th76: :: CAT_1:81

for C, D being Category

for T being Functor of C,D

for c, c9 being Object of C

for f being set st f in Hom (c,c9) holds

T . f in Hom ((T . c),(T . c9))

for T being Functor of C,D

for c, c9 being Object of C

for f being set st f in Hom (c,c9) holds

T . f in Hom ((T . c),(T . c9))

proof end;

theorem Th77: :: CAT_1:82

for C, D being Category

for T being Functor of C,D

for c, c9 being Object of C st Hom (c,c9) <> {} holds

for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9))

for T being Functor of C,D

for c, c9 being Object of C st Hom (c,c9) <> {} holds

for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9))

proof end;

theorem Th78: :: CAT_1:83

for C, D being Category

for T being Functor of C,D

for c, c9 being Object of C st Hom (c,c9) <> {} holds

for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9

for T being Functor of C,D

for c, c9 being Object of C st Hom (c,c9) <> {} holds

for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9

proof end;

theorem Th79: :: CAT_1:84

for C, D being Category

for T being Functor of C,D

for c, c9 being Object of C st Hom (c,c9) <> {} holds

Hom ((T . c),(T . c9)) <> {}

for T being Functor of C,D

for c, c9 being Object of C st Hom (c,c9) <> {} holds

Hom ((T . c),(T . c9)) <> {}

proof end;

theorem :: CAT_1:85

for B, C, D being Category

for T being Functor of B,C

for S being Functor of C,D st T is full & S is full holds

S * T is full

for T being Functor of B,C

for S being Functor of C,D st T is full & S is full holds

S * T is full

proof end;

theorem :: CAT_1:86

for B, C, D being Category

for T being Functor of B,C

for S being Functor of C,D st T is faithful & S is faithful holds

S * T is faithful

for T being Functor of B,C

for S being Functor of C,D st T is faithful & S is faithful holds

S * T is faithful

proof end;

theorem Th82: :: CAT_1:87

for C, D being Category

for T being Functor of C,D

for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9))

for T being Functor of C,D

for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9))

proof end;

definition

let C, D be Category;

let T be Functor of C,D;

let c, c9 be Object of C;

coherence

T | (Hom (c,c9)) is Function of (Hom (c,c9)),(Hom ((T . c),(T . c9)));

end;
let T be Functor of C,D;

let c, c9 be Object of C;

func hom (T,c,c9) -> Function of (Hom (c,c9)),(Hom ((T . c),(T . c9))) equals :: CAT_1:def 28

T | (Hom (c,c9));

correctness T | (Hom (c,c9));

coherence

T | (Hom (c,c9)) is Function of (Hom (c,c9)),(Hom ((T . c),(T . c9)));

proof end;

:: deftheorem defines hom CAT_1:def 28 :

for C, D being Category

for T being Functor of C,D

for c, c9 being Object of C holds hom (T,c,c9) = T | (Hom (c,c9));

for C, D being Category

for T being Functor of C,D

for c, c9 being Object of C holds hom (T,c,c9) = T | (Hom (c,c9));

theorem Th83: :: CAT_1:88

for C, D being Category

for T being Functor of C,D

for c, c9 being Object of C st Hom (c,c9) <> {} holds

for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f

for T being Functor of C,D

for c, c9 being Object of C st Hom (c,c9) <> {} holds

for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f

proof end;

theorem :: CAT_1:89

for C, D being Category

for T being Functor of C,D holds

( T is full iff for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) )

for T being Functor of C,D holds

( T is full iff for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) )

proof end;

theorem :: CAT_1:90

for C, D being Category

for T being Functor of C,D holds

( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one )

for T being Functor of C,D holds

( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one )

proof end;

theorem :: CAT_1:91

for C being Category

for a, b being Element of C st Hom (a,b) <> {} holds

ex m being Morphism of a,b st m in Hom (a,b)

for a, b being Element of C st Hom (a,b) <> {} holds

ex m being Morphism of a,b st m in Hom (a,b)

proof end;

theorem :: CAT_1:92

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

proof end;