:: by Grzegorz Bancerek

::

:: Received January 12, 2001

:: Copyright (c) 2001-2018 Association of Mizar Users

:: <section1>Definability of categories and functors</section1>

scheme :: YELLOW18:sch 1

AltCatStrLambda{ F_{1}() -> non empty set , F_{2}( object , object ) -> set , F_{3}( object , object , object , object , object ) -> object } :

AltCatStrLambda{ F

ex C being non empty transitive strict AltCatStr st

( the carrier of C = F_{1}() & ( for a, b being Object of C holds <^a,b^> = F_{2}(a,b) ) & ( for a, b, c being Object of C st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F_{3}(a,b,c,f,g) ) )

provided( the carrier of C = F

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F

A1:
for a, b, c being Element of F_{1}()

for f, g being set st f in F_{2}(a,b) & g in F_{2}(b,c) holds

F_{3}(a,b,c,f,g) in F_{2}(a,c)

for f, g being set st f in F

F

proof end;

scheme :: YELLOW18:sch 2

CatAssocSch{ F_{1}() -> non empty transitive AltCatStr , F_{2}( object , object , object , object , object ) -> object } :

provided

CatAssocSch{ F

provided

A1:
for a, b, c being Object of F_{1}() st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F_{2}(a,b,c,f,g)
and

A2: for a, b, c, d being Object of F_{1}()

for f, g, h being set st f in <^a,b^> & g in <^b,c^> & h in <^c,d^> holds

F_{2}(a,c,d,F_{2}(a,b,c,f,g),h) = F_{2}(a,b,d,f,F_{2}(b,c,d,g,h))

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F

A2: for a, b, c, d being Object of F

for f, g, h being set st f in <^a,b^> & g in <^b,c^> & h in <^c,d^> holds

F

proof end;

scheme :: YELLOW18:sch 3

CatUnitsSch{ F_{1}() -> non empty transitive AltCatStr , F_{2}( object , object , object , object , object ) -> object } :

provided

CatUnitsSch{ F

provided

A1:
for a, b, c being Object of F_{1}() st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F_{2}(a,b,c,f,g)
and

A2: for a being Object of F_{1}() ex f being set st

( f in <^a,a^> & ( for b being Object of F_{1}()

for g being set st g in <^a,b^> holds

F_{2}(a,a,b,f,g) = g ) )
and

A3: for a being Object of F_{1}() ex f being set st

( f in <^a,a^> & ( for b being Object of F_{1}()

for g being set st g in <^b,a^> holds

F_{2}(b,a,a,g,f) = g ) )

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F

A2: for a being Object of F

( f in <^a,a^> & ( for b being Object of F

for g being set st g in <^a,b^> holds

F

A3: for a being Object of F

( f in <^a,a^> & ( for b being Object of F

for g being set st g in <^b,a^> holds

F

proof end;

scheme :: YELLOW18:sch 4

CategoryLambda{ F_{1}() -> non empty set , F_{2}( object , object ) -> set , F_{3}( object , object , object , object , object ) -> object } :

CategoryLambda{ F

ex C being strict category st

( the carrier of C = F_{1}() & ( for a, b being Object of C holds <^a,b^> = F_{2}(a,b) ) & ( for a, b, c being Object of C st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F_{3}(a,b,c,f,g) ) )

provided( the carrier of C = F

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F

A1:
for a, b, c being Element of F_{1}()

for f, g being set st f in F_{2}(a,b) & g in F_{2}(b,c) holds

F_{3}(a,b,c,f,g) in F_{2}(a,c)
and

A2: for a, b, c, d being Element of F_{1}()

for f, g, h being set st f in F_{2}(a,b) & g in F_{2}(b,c) & h in F_{2}(c,d) holds

F_{3}(a,c,d,F_{3}(a,b,c,f,g),h) = F_{3}(a,b,d,f,F_{3}(b,c,d,g,h))
and

A3: for a being Element of F_{1}() ex f being set st

( f in F_{2}(a,a) & ( for b being Element of F_{1}()

for g being set st g in F_{2}(a,b) holds

F_{3}(a,a,b,f,g) = g ) )
and

A4: for a being Element of F_{1}() ex f being set st

( f in F_{2}(a,a) & ( for b being Element of F_{1}()

for g being set st g in F_{2}(b,a) holds

F_{3}(b,a,a,g,f) = g ) )

for f, g being set st f in F

F

A2: for a, b, c, d being Element of F

for f, g, h being set st f in F

F

A3: for a being Element of F

( f in F

for g being set st g in F

F

A4: for a being Element of F

( f in F

for g being set st g in F

F

proof end;

scheme :: YELLOW18:sch 5

CategoryLambdaUniq{ F_{1}() -> non empty set , F_{2}( object , object ) -> object , F_{3}( object , object , object , object , object ) -> object } :

CategoryLambdaUniq{ F

for C1, C2 being non empty transitive AltCatStr st the carrier of C1 = F_{1}() & ( for a, b being Object of C1 holds <^a,b^> = F_{2}(a,b) ) & ( for a, b, c being Object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F_{3}(a,b,c,f,g) ) & the carrier of C2 = F_{1}() & ( for a, b being Object of C2 holds <^a,b^> = F_{2}(a,b) ) & ( for a, b, c being Object of C2 st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F_{3}(a,b,c,f,g) ) holds

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

proof end;

scheme :: YELLOW18:sch 6

CategoryQuasiLambda{ F_{1}() -> non empty set , P_{1}[ object , object , object ], F_{2}( object , object ) -> set , F_{3}( object , object , object , object , object ) -> object } :

CategoryQuasiLambda{ F

ex C being strict category st

( the carrier of C = F_{1}() & ( for a, b being Object of C

for f being set holds

( f in <^a,b^> iff ( f in F_{2}(a,b) & P_{1}[a,b,f] ) ) ) & ( for a, b, c being Object of C st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F_{3}(a,b,c,f,g) ) )

provided( the carrier of C = F

for f being set holds

( f in <^a,b^> iff ( f in F

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = F

A1:
for a, b, c being Element of F_{1}()

for f, g being set st f in F_{2}(a,b) & P_{1}[a,b,f] & g in F_{2}(b,c) & P_{1}[b,c,g] holds

( F_{3}(a,b,c,f,g) in F_{2}(a,c) & P_{1}[a,c,F_{3}(a,b,c,f,g)] )
and

A2: for a, b, c, d being Element of F_{1}()

for f, g, h being set st f in F_{2}(a,b) & P_{1}[a,b,f] & g in F_{2}(b,c) & P_{1}[b,c,g] & h in F_{2}(c,d) & P_{1}[c,d,h] holds

F_{3}(a,c,d,F_{3}(a,b,c,f,g),h) = F_{3}(a,b,d,f,F_{3}(b,c,d,g,h))
and

A3: for a being Element of F_{1}() ex f being set st

( f in F_{2}(a,a) & P_{1}[a,a,f] & ( for b being Element of F_{1}()

for g being set st g in F_{2}(a,b) & P_{1}[a,b,g] holds

F_{3}(a,a,b,f,g) = g ) )
and

A4: for a being Element of F_{1}() ex f being set st

( f in F_{2}(a,a) & P_{1}[a,a,f] & ( for b being Element of F_{1}()

for g being set st g in F_{2}(b,a) & P_{1}[b,a,g] holds

F_{3}(b,a,a,g,f) = g ) )

for f, g being set st f in F

( F

A2: for a, b, c, d being Element of F

for f, g, h being set st f in F

F

A3: for a being Element of F

( f in F

for g being set st g in F

F

A4: for a being Element of F

( f in F

for g being set st g in F

F

proof end;

registration

let f be Function-yielding Function;

let a, b, c be set ;

coherence

( f . (a,b,c) is Relation-like & f . (a,b,c) is Function-like )

end;
let a, b, c be set ;

coherence

( f . (a,b,c) is Relation-like & f . (a,b,c) is Function-like )

proof end;

scheme :: YELLOW18:sch 7

SubcategoryEx{ F_{1}() -> category, P_{1}[ object ], P_{2}[ object , object , object ] } :

SubcategoryEx{ F

ex B being non empty strict subcategory of F_{1}() st

( ( for a being Object of F_{1}() holds

( a is Object of B iff P_{1}[a] ) ) & ( for a, b being Object of F_{1}()

for a9, b9 being Object of B st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff P_{2}[a,b,f] ) ) )

provided( ( for a being Object of F

( a is Object of B iff P

for a9, b9 being Object of B st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff P

A1:
ex a being Object of F_{1}() st P_{1}[a]
and

A2: for a, b, c being Object of F_{1}() st P_{1}[a] & P_{1}[b] & P_{1}[c] & <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c st P_{2}[a,b,f] & P_{2}[b,c,g] holds

P_{2}[a,c,g * f]
and

A3: for a being Object of F_{1}() st P_{1}[a] holds

P_{2}[a,a, idm a]

A2: for a, b, c being Object of F

for f being Morphism of a,b

for g being Morphism of b,c st P

P

A3: for a being Object of F

P

proof end;

scheme :: YELLOW18:sch 8

CovariantFunctorLambda{ F_{1}() -> category, F_{2}() -> category, F_{3}( object ) -> object , F_{4}( object , object , object ) -> object } :

CovariantFunctorLambda{ F

ex F being strict covariant Functor of F_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}(a) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{4}(a,b,f) ) )

provided( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

A1:
for a being Object of F_{1}() holds F_{3}(a) is Object of F_{2}()
and

A2: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{4}(a,b,f) in the Arrows of F_{2}() . (F_{3}(a),F_{3}(b))
and

A3: for a, b, c being Object of F_{1}() st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of F_{2}() st a9 = F_{3}(a) & b9 = F_{3}(b) & c9 = F_{3}(c) holds

for f9 being Morphism of a9,b9

for g9 being Morphism of b9,c9 st f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) holds

F_{4}(a,c,(g * f)) = g9 * f9
and

A4: for a being Object of F_{1}()

for a9 being Object of F_{2}() st a9 = F_{3}(a) holds

F_{4}(a,a,(idm a)) = idm a9

A2: for a, b being Object of F

for f being Morphism of a,b holds F

A3: for a, b, c being Object of F

for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of F

for f9 being Morphism of a9,b9

for g9 being Morphism of b9,c9 st f9 = F

F

A4: for a being Object of F

for a9 being Object of F

F

proof end;

theorem Th1: :: YELLOW18:1

for A, B being category

for F, G being covariant Functor of A,B st ( for a being Object of A holds F . a = G . a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = G . f ) holds

FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)

for F, G being covariant Functor of A,B st ( for a being Object of A holds F . a = G . a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = G . f ) holds

FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)

proof end;

scheme :: YELLOW18:sch 9

ContravariantFunctorLambda{ F_{1}() -> category, F_{2}() -> category, F_{3}( object ) -> object , F_{4}( object , object , object ) -> object } :

ContravariantFunctorLambda{ F

ex F being strict contravariant Functor of F_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}(a) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{4}(a,b,f) ) )

provided( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

A1:
for a being Object of F_{1}() holds F_{3}(a) is Object of F_{2}()
and

A2: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{4}(a,b,f) in the Arrows of F_{2}() . (F_{3}(b),F_{3}(a))
and

A3: for a, b, c being Object of F_{1}() st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of F_{2}() st a9 = F_{3}(a) & b9 = F_{3}(b) & c9 = F_{3}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) holds

F_{4}(a,c,(g * f)) = f9 * g9
and

A4: for a being Object of F_{1}()

for a9 being Object of F_{2}() st a9 = F_{3}(a) holds

F_{4}(a,a,(idm a)) = idm a9

A2: for a, b being Object of F

for f being Morphism of a,b holds F

A3: for a, b, c being Object of F

for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of F

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F

F

A4: for a being Object of F

for a9 being Object of F

F

proof end;

theorem Th2: :: YELLOW18:2

for A, B being category

for F, G being contravariant Functor of A,B st ( for a being Object of A holds F . a = G . a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = G . f ) holds

FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)

for F, G being contravariant Functor of A,B st ( for a being Object of A holds F . a = G . a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = G . f ) holds

FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)

proof end;

:: <section2>Isomorphism and equivalence of categories</section2>

definition

let A, B, C be non empty set ;

let f be Function of [:A,B:],C;

( f is one-to-one iff for a1, a2 being Element of A

for b1, b2 being Element of B st f . (a1,b1) = f . (a2,b2) holds

( a1 = a2 & b1 = b2 ) )

end;
let f be Function of [:A,B:],C;

:: original: one-to-one

redefine attr f is one-to-one means :: YELLOW18:def 1

for a1, a2 being Element of A

for b1, b2 being Element of B st f . (a1,b1) = f . (a2,b2) holds

( a1 = a2 & b1 = b2 );

compatibility redefine attr f is one-to-one means :: YELLOW18:def 1

for a1, a2 being Element of A

for b1, b2 being Element of B st f . (a1,b1) = f . (a2,b2) holds

( a1 = a2 & b1 = b2 );

( f is one-to-one iff for a1, a2 being Element of A

for b1, b2 being Element of B st f . (a1,b1) = f . (a2,b2) holds

( a1 = a2 & b1 = b2 ) )

proof end;

:: deftheorem defines one-to-one YELLOW18:def 1 :

for A, B, C being non empty set

for f being Function of [:A,B:],C holds

( f is one-to-one iff for a1, a2 being Element of A

for b1, b2 being Element of B st f . (a1,b1) = f . (a2,b2) holds

( a1 = a2 & b1 = b2 ) );

for A, B, C being non empty set

for f being Function of [:A,B:],C holds

( f is one-to-one iff for a1, a2 being Element of A

for b1, b2 being Element of B st f . (a1,b1) = f . (a2,b2) holds

( a1 = a2 & b1 = b2 ) );

scheme :: YELLOW18:sch 10

CoBijectiveSch{ F_{1}() -> category, F_{2}() -> category, F_{3}() -> covariant Functor of F_{1}(),F_{2}(), F_{4}( object ) -> object , F_{5}( object , object , object ) -> object } :

provided

CoBijectiveSch{ F

provided

A1:
for a being Object of F_{1}() holds F_{3}() . a = F_{4}(a)
and

A2: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{3}() . f = F_{5}(a,b,f)
and

A3: for a, b being Object of F_{1}() st F_{4}(a) = F_{4}(b) holds

a = b and

A4: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f, g being Morphism of a,b st F_{5}(a,b,f) = F_{5}(a,b,g) holds

f = g and

A5: for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b ex c, d being Object of F_{1}() ex g being Morphism of c,d st

( a = F_{4}(c) & b = F_{4}(d) & <^c,d^> <> {} & f = F_{5}(c,d,g) )

A2: for a, b being Object of F

for f being Morphism of a,b holds F

A3: for a, b being Object of F

a = b and

A4: for a, b being Object of F

for f, g being Morphism of a,b st F

f = g and

A5: for a, b being Object of F

for f being Morphism of a,b ex c, d being Object of F

( a = F

proof end;

scheme :: YELLOW18:sch 11

CatIsomorphism{ F_{1}() -> category, F_{2}() -> category, F_{3}( object ) -> object , F_{4}( object , object , object ) -> object } :

provided

CatIsomorphism{ F

provided

A1:
ex F being covariant Functor of F_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}(a) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{4}(a,b,f) ) )
and

A2: for a, b being Object of F_{1}() st F_{3}(a) = F_{3}(b) holds

a = b and

A3: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f, g being Morphism of a,b st F_{4}(a,b,f) = F_{4}(a,b,g) holds

f = g and

A4: for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b ex c, d being Object of F_{1}() ex g being Morphism of c,d st

( a = F_{3}(c) & b = F_{3}(d) & <^c,d^> <> {} & f = F_{4}(c,d,g) )

( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

A2: for a, b being Object of F

a = b and

A3: for a, b being Object of F

for f, g being Morphism of a,b st F

f = g and

A4: for a, b being Object of F

for f being Morphism of a,b ex c, d being Object of F

( a = F

proof end;

scheme :: YELLOW18:sch 12

ContraBijectiveSch{ F_{1}() -> category, F_{2}() -> category, F_{3}() -> contravariant Functor of F_{1}(),F_{2}(), F_{4}( object ) -> object , F_{5}( object , object , object ) -> object } :

provided

ContraBijectiveSch{ F

provided

A1:
for a being Object of F_{1}() holds F_{3}() . a = F_{4}(a)
and

A2: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{3}() . f = F_{5}(a,b,f)
and

A3: for a, b being Object of F_{1}() st F_{4}(a) = F_{4}(b) holds

a = b and

A4: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f, g being Morphism of a,b st F_{5}(a,b,f) = F_{5}(a,b,g) holds

f = g and

A5: for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b ex c, d being Object of F_{1}() ex g being Morphism of c,d st

( b = F_{4}(c) & a = F_{4}(d) & <^c,d^> <> {} & f = F_{5}(c,d,g) )

A2: for a, b being Object of F

for f being Morphism of a,b holds F

A3: for a, b being Object of F

a = b and

A4: for a, b being Object of F

for f, g being Morphism of a,b st F

f = g and

A5: for a, b being Object of F

for f being Morphism of a,b ex c, d being Object of F

( b = F

proof end;

scheme :: YELLOW18:sch 13

CatAntiIsomorphism{ F_{1}() -> category, F_{2}() -> category, F_{3}( object ) -> object , F_{4}( object , object , object ) -> object } :

provided

CatAntiIsomorphism{ F

provided

A1:
ex F being contravariant Functor of F_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}(a) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{4}(a,b,f) ) )
and

A2: for a, b being Object of F_{1}() st F_{3}(a) = F_{3}(b) holds

a = b and

A3: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f, g being Morphism of a,b st F_{4}(a,b,f) = F_{4}(a,b,g) holds

f = g and

A4: for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b ex c, d being Object of F_{1}() ex g being Morphism of c,d st

( b = F_{3}(c) & a = F_{3}(d) & <^c,d^> <> {} & f = F_{4}(c,d,g) )

( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

A2: for a, b being Object of F

a = b and

A3: for a, b being Object of F

for f, g being Morphism of a,b st F

f = g and

A4: for a, b being Object of F

for f being Morphism of a,b ex c, d being Object of F

( b = F

proof end;

definition

let A, B be category;

for A being category ex F, G being covariant Functor of A,A st

( G * F, id A are_naturally_equivalent & F * G, id A are_naturally_equivalent )

for A, B being category st ex F being covariant Functor of A,B ex G being covariant Functor of B,A st

( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent ) holds

ex F being covariant Functor of B,A ex G being covariant Functor of A,B st

( G * F, id B are_naturally_equivalent & F * G, id A are_naturally_equivalent ) ;

end;
pred A,B are_equivalent means :: YELLOW18:def 2

ex F being covariant Functor of A,B ex G being covariant Functor of B,A st

( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent );

reflexivity ex F being covariant Functor of A,B ex G being covariant Functor of B,A st

( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent );

for A being category ex F, G being covariant Functor of A,A st

( G * F, id A are_naturally_equivalent & F * G, id A are_naturally_equivalent )

proof end;

symmetry for A, B being category st ex F being covariant Functor of A,B ex G being covariant Functor of B,A st

( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent ) holds

ex F being covariant Functor of B,A ex G being covariant Functor of A,B st

( G * F, id B are_naturally_equivalent & F * G, id A are_naturally_equivalent ) ;

:: deftheorem defines are_equivalent YELLOW18:def 2 :

for A, B being category holds

( A,B are_equivalent iff ex F being covariant Functor of A,B ex G being covariant Functor of B,A st

( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent ) );

for A, B being category holds

( A,B are_equivalent iff ex F being covariant Functor of A,B ex G being covariant Functor of B,A st

( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent ) );

theorem Th3: :: YELLOW18:3

for A, B, C being non empty reflexive AltGraph

for F1, F2 being feasible FunctorStr over A,B

for G1, G2 being FunctorStr over B,C st FunctorStr(# the ObjectMap of F1, the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F2, the MorphMap of F2 #) & FunctorStr(# the ObjectMap of G1, the MorphMap of G1 #) = FunctorStr(# the ObjectMap of G2, the MorphMap of G2 #) holds

G1 * F1 = G2 * F2

for F1, F2 being feasible FunctorStr over A,B

for G1, G2 being FunctorStr over B,C st FunctorStr(# the ObjectMap of F1, the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F2, the MorphMap of F2 #) & FunctorStr(# the ObjectMap of G1, the MorphMap of G1 #) = FunctorStr(# the ObjectMap of G2, the MorphMap of G2 #) holds

G1 * F1 = G2 * F2

proof end;

scheme :: YELLOW18:sch 14

NatTransLambda{ F_{1}() -> category, F_{2}() -> category, F_{3}() -> covariant Functor of F_{1}(),F_{2}(), F_{4}() -> covariant Functor of F_{1}(),F_{2}(), F_{5}( object ) -> object } :

NatTransLambda{ F

ex t being natural_transformation of F_{3}(),F_{4}() st

( F_{3}() is_naturally_transformable_to F_{4}() & ( for a being Object of F_{1}() holds t ! a = F_{5}(a) ) )

provided( F

A1:
for a being Object of F_{1}() holds F_{5}(a) in <^(F_{3}() . a),(F_{4}() . a)^>
and

A2: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b

for g1 being Morphism of (F_{3}() . a),(F_{4}() . a) st g1 = F_{5}(a) holds

for g2 being Morphism of (F_{3}() . b),(F_{4}() . b) st g2 = F_{5}(b) holds

g2 * (F_{3}() . f) = (F_{4}() . f) * g1

A2: for a, b being Object of F

for f being Morphism of a,b

for g1 being Morphism of (F

for g2 being Morphism of (F

g2 * (F

proof end;

scheme :: YELLOW18:sch 15

NatEquivalenceLambda{ F_{1}() -> category, F_{2}() -> category, F_{3}() -> covariant Functor of F_{1}(),F_{2}(), F_{4}() -> covariant Functor of F_{1}(),F_{2}(), F_{5}( object ) -> object } :

NatEquivalenceLambda{ F

ex t being natural_equivalence of F_{3}(),F_{4}() st

( F_{3}(),F_{4}() are_naturally_equivalent & ( for a being Object of F_{1}() holds t ! a = F_{5}(a) ) )

provided( F

A1:
for a being Object of F_{1}() holds

( F_{5}(a) in <^(F_{3}() . a),(F_{4}() . a)^> & <^(F_{4}() . a),(F_{3}() . a)^> <> {} & ( for f being Morphism of (F_{3}() . a),(F_{4}() . a) st f = F_{5}(a) holds

f is iso ) ) and

A2: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b

for g1 being Morphism of (F_{3}() . a),(F_{4}() . a) st g1 = F_{5}(a) holds

for g2 being Morphism of (F_{3}() . b),(F_{4}() . b) st g2 = F_{5}(b) holds

g2 * (F_{3}() . f) = (F_{4}() . f) * g1

( F

f is iso ) ) and

A2: for a, b being Object of F

for f being Morphism of a,b

for g1 being Morphism of (F

for g2 being Morphism of (F

g2 * (F

proof end;

:: <section3>Dual categories</section3>

definition

let C1, C2 be non empty AltCatStr ;

for C1, C2 being non empty AltCatStr st the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being Object of C1

for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds

the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ) holds

( the carrier of C1 = the carrier of C2 & the Arrows of C1 = ~ the Arrows of C2 & ( for a, b, c being Object of C2

for a9, b9, c9 being Object of C1 st a9 = a & b9 = b & c9 = c holds

the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a)) ) )

end;
pred C1,C2 are_opposite means :: YELLOW18:def 3

( the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being Object of C1

for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds

the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ) );

symmetry ( the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being Object of C1

for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds

the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ) );

for C1, C2 being non empty AltCatStr st the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being Object of C1

for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds

the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ) holds

( the carrier of C1 = the carrier of C2 & the Arrows of C1 = ~ the Arrows of C2 & ( for a, b, c being Object of C2

for a9, b9, c9 being Object of C1 st a9 = a & b9 = b & c9 = c holds

the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a)) ) )

proof end;

:: deftheorem defines are_opposite YELLOW18:def 3 :

for C1, C2 being non empty AltCatStr holds

( C1,C2 are_opposite iff ( the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being Object of C1

for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds

the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ) ) );

for C1, C2 being non empty AltCatStr holds

( C1,C2 are_opposite iff ( the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being Object of C1

for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds

the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ) ) );

theorem :: YELLOW18:6

for A, B being non empty AltCatStr st A,B are_opposite holds

for a being Object of A holds a is Object of B ;

for a being Object of A holds a is Object of B ;

theorem :: YELLOW18:8

theorem Th9: :: YELLOW18:9

for C1, C2 being non empty transitive AltCatStr holds

( C1,C2 are_opposite iff ( the carrier of C2 = the carrier of C1 & ( for a, b, c being Object of C1

for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds

( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b

for g being Morphism of b,c

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds

f9 * g9 = g * f ) ) ) ) )

( C1,C2 are_opposite iff ( the carrier of C2 = the carrier of C1 & ( for a, b, c being Object of C1

for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds

( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b

for g being Morphism of b,c

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds

f9 * g9 = g * f ) ) ) ) )

proof end;

theorem Th10: :: YELLOW18:10

for A, B being category st A,B are_opposite holds

for a being Object of A

for b being Object of B st a = b holds

idm a = idm b

for a being Object of A

for b being Object of B st a = b holds

idm a = idm b

proof end;

theorem Th11: :: YELLOW18:11

for A, B being non empty transitive AltCatStr st A,B are_opposite & A is associative holds

B is associative

B is associative

proof end;

theorem Th12: :: YELLOW18:12

for A, B being non empty transitive AltCatStr st A,B are_opposite & A is with_units holds

B is with_units

B is with_units

proof end;

theorem Th13: :: YELLOW18:13

for C, C1, C2 being non empty AltCatStr st C,C1 are_opposite holds

( C,C2 are_opposite iff AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) )

( C,C2 are_opposite iff AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) )

proof end;

definition

let C be non empty transitive AltCatStr ;

for b_{1}, b_{2} being non empty transitive strict AltCatStr st C,b_{1} are_opposite & C,b_{2} are_opposite holds

b_{1} = b_{2}
by Th13;

existence

ex b_{1} being non empty transitive strict AltCatStr st C,b_{1} are_opposite

end;
func C opp -> non empty transitive strict AltCatStr means :Def4: :: YELLOW18:def 4

C,it are_opposite ;

uniqueness C,it are_opposite ;

for b

b

existence

ex b

proof end;

:: deftheorem Def4 defines opp YELLOW18:def 4 :

for C being non empty transitive AltCatStr

for b_{2} being non empty transitive strict AltCatStr holds

( b_{2} = C opp iff C,b_{2} are_opposite );

for C being non empty transitive AltCatStr

for b

( b

registration
end;

registration
end;

definition

let A, B be category;

assume A1: A,B are_opposite ;

deffunc H_{1}( set ) -> set = $1;

deffunc H_{2}( set , set , set ) -> set = $3;

A2: for a being Object of A holds H_{1}(a) is Object of B
by A1;

for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of B st a9 = H_{1}(a) & b9 = H_{1}(b) & c9 = H_{1}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H_{2}(a,b,f) & g9 = H_{2}(b,c,g) holds

H_{2}(a,c,g * f) = f9 * g9
by A1, Th9;

A6: for a being Object of A

for a9 being Object of B st a9 = H_{1}(a) holds

H_{2}(a,a, idm a) = idm a9
by A1, Th10;

ex b_{1} being strict contravariant Functor of A,B st

( ( for a being Object of A holds b_{1} . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{1} . f = f ) )

for b_{1}, b_{2} being strict contravariant Functor of A,B st ( for a being Object of A holds b_{1} . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{1} . f = f ) & ( for a being Object of A holds b_{2} . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{2} . f = f ) holds

b_{1} = b_{2}

end;
assume A1: A,B are_opposite ;

deffunc H

deffunc H

A2: for a being Object of A holds H

A3: now :: thesis: for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds H_{2}(a,b,f) in the Arrows of B . (H_{1}(b),H_{1}(a))

A5:
for a, b, c being Object of A st <^a,b^> <> {} & <^b,c^> <> {} holds for f being Morphism of a,b holds H

let a, b be Object of A; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds H_{2}(a,b,f) in the Arrows of B . (H_{1}(b),H_{1}(a)) )

assume A4: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds H_{2}(a,b,f) in the Arrows of B . (H_{1}(b),H_{1}(a))

let f be Morphism of a,b; :: thesis: H_{2}(a,b,f) in the Arrows of B . (H_{1}(b),H_{1}(a))

reconsider a9 = a, b9 = b as Object of B by A2;

<^a,b^> = <^b9,a9^> by A1, Th9

.= the Arrows of B . (b,a) ;

hence H_{2}(a,b,f) in the Arrows of B . (H_{1}(b),H_{1}(a))
by A4; :: thesis: verum

end;
assume A4: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds H

let f be Morphism of a,b; :: thesis: H

reconsider a9 = a, b9 = b as Object of B by A2;

<^a,b^> = <^b9,a9^> by A1, Th9

.= the Arrows of B . (b,a) ;

hence H

for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of B st a9 = H

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H

H

A6: for a being Object of A

for a9 being Object of B st a9 = H

H

func dualizing-func (A,B) -> strict contravariant Functor of A,B means :Def5: :: YELLOW18:def 5

( ( for a being Object of A holds it . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

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

existence ( ( for a being Object of A holds it . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

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

ex b

( ( for a being Object of A holds b

for f being Morphism of a,b holds b

proof end;

uniqueness for b

for f being Morphism of a,b holds b

for f being Morphism of a,b holds b

b

proof end;

:: deftheorem Def5 defines dualizing-func YELLOW18:def 5 :

for A, B being category st A,B are_opposite holds

for b_{3} being strict contravariant Functor of A,B holds

( b_{3} = dualizing-func (A,B) iff ( ( for a being Object of A holds b_{3} . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{3} . f = f ) ) );

for A, B being category st A,B are_opposite holds

for b

( b

for f being Morphism of a,b holds b

theorem Th14: :: YELLOW18:14

for A, B being category st A,B are_opposite holds

(dualizing-func (A,B)) * (dualizing-func (B,A)) = id B

(dualizing-func (A,B)) * (dualizing-func (B,A)) = id B

proof end;

registration

let A be category;

coherence

dualizing-func (A,(A opp)) is bijective by Def4, Th15;

coherence

dualizing-func ((A opp),A) is bijective

end;
coherence

dualizing-func (A,(A opp)) is bijective by Def4, Th15;

coherence

dualizing-func ((A opp),A) is bijective

proof end;

theorem Th17: :: YELLOW18:17

for A, B, C being category st A,B are_opposite holds

( A,C are_isomorphic iff B,C are_anti-isomorphic )

( A,C are_isomorphic iff B,C are_anti-isomorphic )

proof end;

theorem :: YELLOW18:18

for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_isomorphic holds

B,D are_isomorphic

B,D are_isomorphic

proof end;

theorem :: YELLOW18:19

for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_anti-isomorphic holds

B,D are_anti-isomorphic

B,D are_anti-isomorphic

proof end;

Lm1: now :: thesis: for A, B being category st A,B are_opposite holds

for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

let A, B be category; :: thesis: ( A,B are_opposite implies for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )

assume A1: A,B are_opposite ; :: thesis: for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

let a, b be Object of A; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )

assume that

A2: <^a,b^> <> {} and

A3: <^b,a^> <> {} ; :: thesis: for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

let a9, b9 be Object of B; :: thesis: ( a9 = a & b9 = b implies for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )

assume that

A4: a9 = a and

A5: b9 = b ; :: thesis: for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

let f be Morphism of a,b; :: thesis: for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

let f9 be Morphism of b9,a9; :: thesis: ( f9 = f implies ( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )

assume A6: f9 = f ; :: thesis: ( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

thus ( f is retraction implies f9 is coretraction ) :: thesis: ( f is coretraction implies f9 is retraction )

end;
for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )

assume A1: A,B are_opposite ; :: thesis: for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

let a, b be Object of A; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )

assume that

A2: <^a,b^> <> {} and

A3: <^b,a^> <> {} ; :: thesis: for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

let a9, b9 be Object of B; :: thesis: ( a9 = a & b9 = b implies for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )

assume that

A4: a9 = a and

A5: b9 = b ; :: thesis: for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

let f be Morphism of a,b; :: thesis: for f9 being Morphism of b9,a9 st f9 = f holds

( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

let f9 be Morphism of b9,a9; :: thesis: ( f9 = f implies ( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )

assume A6: f9 = f ; :: thesis: ( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )

thus ( f is retraction implies f9 is coretraction ) :: thesis: ( f is coretraction implies f9 is retraction )

proof

thus
( f is coretraction implies f9 is retraction )
:: thesis: verum
given g being Morphism of b,a such that A7:
g is_right_inverse_of f
; :: according to ALTCAT_3:def 2 :: thesis: f9 is coretraction

reconsider g9 = g as Morphism of a9,b9 by A1, A4, A5, Th7;

take g9 ; :: according to ALTCAT_3:def 3 :: thesis: g9 is_left_inverse_of f9

f * g = idm b by A7

.= idm b9 by A1, A5, Th10 ;

hence g9 * f9 = idm b9 by A1, A2, A3, A4, A5, A6, Th9; :: according to ALTCAT_3:def 1 :: thesis: verum

end;
reconsider g9 = g as Morphism of a9,b9 by A1, A4, A5, Th7;

take g9 ; :: according to ALTCAT_3:def 3 :: thesis: g9 is_left_inverse_of f9

f * g = idm b by A7

.= idm b9 by A1, A5, Th10 ;

hence g9 * f9 = idm b9 by A1, A2, A3, A4, A5, A6, Th9; :: according to ALTCAT_3:def 1 :: thesis: verum

proof

given g being Morphism of b,a such that A8:
g is_left_inverse_of f
; :: according to ALTCAT_3:def 3 :: thesis: f9 is retraction

reconsider g9 = g as Morphism of a9,b9 by A1, A4, A5, Th7;

take g9 ; :: according to ALTCAT_3:def 2 :: thesis: f9 is_left_inverse_of g9

g * f = idm a by A8

.= idm a9 by A1, A4, Th10 ;

hence f9 * g9 = idm a9 by A1, A2, A3, A4, A5, A6, Th9; :: according to ALTCAT_3:def 1 :: thesis: verum

end;
reconsider g9 = g as Morphism of a9,b9 by A1, A4, A5, Th7;

take g9 ; :: according to ALTCAT_3:def 2 :: thesis: f9 is_left_inverse_of g9

g * f = idm a by A8

.= idm a9 by A1, A4, Th10 ;

hence f9 * g9 = idm a9 by A1, A2, A3, A4, A5, A6, Th9; :: according to ALTCAT_3:def 1 :: thesis: verum

theorem :: YELLOW18:20

for A, B being category st A,B are_opposite holds

for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( f is retraction iff f9 is coretraction )

for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( f is retraction iff f9 is coretraction )

proof end;

theorem :: YELLOW18:21

for A, B being category st A,B are_opposite holds

for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( f is coretraction iff f9 is retraction )

for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( f is coretraction iff f9 is retraction )

proof end;

theorem Th22: :: YELLOW18:22

for A, B being category st A,B are_opposite holds

for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f & f is retraction & f is coretraction holds

f9 " = f "

for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f & f is retraction & f is coretraction holds

f9 " = f "

proof end;

theorem Th23: :: YELLOW18:23

for A, B being category st A,B are_opposite holds

for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( f is iso iff f9 is iso )

for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds

for a9, b9 being Object of B st a9 = a & b9 = b holds

for f being Morphism of a,b

for f9 being Morphism of b9,a9 st f9 = f holds

( f is iso iff f9 is iso )

proof end;

theorem Th24: :: YELLOW18:24

for A, B, C, D being category st A,B are_opposite & C,D are_opposite holds

for F, G being covariant Functor of B,C st F,G are_naturally_equivalent holds

((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) are_naturally_equivalent

for F, G being covariant Functor of B,C st F,G are_naturally_equivalent holds

((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) are_naturally_equivalent

proof end;

theorem Th25: :: YELLOW18:25

for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_equivalent holds

B,D are_equivalent

B,D are_equivalent

proof end;

definition

let A, B be category;

symmetry

for A, B being category st A,B opp are_equivalent holds

B,A opp are_equivalent

end;
symmetry

for A, B being category st A,B opp are_equivalent holds

B,A opp are_equivalent

proof end;

:: deftheorem Def6 defines are_dual YELLOW18:def 6 :

for A, B being category holds

( A,B are_dual iff A,B opp are_equivalent );

for A, B being category holds

( A,B are_dual iff A,B opp are_equivalent );

:: <section4>Concrete categories</section4>

definition

let C be category;

end;
attr C is para-functional means :: YELLOW18:def 7

ex F being ManySortedSet of C st

for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((F . a1),(F . a2));

ex F being ManySortedSet of C st

for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((F . a1),(F . a2));

:: deftheorem defines para-functional YELLOW18:def 7 :

for C being category holds

( C is para-functional iff ex F being ManySortedSet of C st

for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((F . a1),(F . a2)) );

for C being category holds

( C is para-functional iff ex F being ManySortedSet of C st

for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((F . a1),(F . a2)) );

registration

for b_{1} being category st b_{1} is quasi-functional holds

b_{1} is para-functional
end;

cluster non empty transitive quasi-functional associative with_units -> para-functional for category;

coherence for b

b

proof end;

definition

let C be category;

let a be set ;

for b_{1} being set holds verum
;

existence

( ( a is Object of C implies ex b_{1} being set ex b being Object of C st

( b = a & b_{1} = proj1 (idm b) ) ) & ( a is not Object of C implies ex b_{1} being set st b_{1} = {} ) )

for b_{1}, b_{2} being set holds

( ( a is Object of C & ex b being Object of C st

( b = a & b_{1} = proj1 (idm b) ) & ex b being Object of C st

( b = a & b_{2} = proj1 (idm b) ) implies b_{1} = b_{2} ) & ( a is not Object of C & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )
;

end;
let a be set ;

func C -carrier_of a -> set means :Def8: :: YELLOW18:def 8

ex b being Object of C st

( b = a & it = proj1 (idm b) ) if a is Object of C

otherwise it = {} ;

consistency ex b being Object of C st

( b = a & it = proj1 (idm b) ) if a is Object of C

otherwise it = {} ;

for b

existence

( ( a is Object of C implies ex b

( b = a & b

proof end;

uniqueness for b

( ( a is Object of C & ex b being Object of C st

( b = a & b

( b = a & b

:: deftheorem Def8 defines -carrier_of YELLOW18:def 8 :

for C being category

for a, b_{3} being set holds

( ( a is Object of C implies ( b_{3} = C -carrier_of a iff ex b being Object of C st

( b = a & b_{3} = proj1 (idm b) ) ) ) & ( a is not Object of C implies ( b_{3} = C -carrier_of a iff b_{3} = {} ) ) );

for C being category

for a, b

( ( a is Object of C implies ( b

( b = a & b

definition

let C be category;

let a be Object of C;

compatibility

for b_{1} being set holds

( b_{1} = C -carrier_of a iff b_{1} = proj1 (idm a) )
by Def8;

end;
let a be Object of C;

compatibility

for b

( b

:: deftheorem defines -carrier_of YELLOW18:def 9 :

for C being category

for a being Object of C holds C -carrier_of a = proj1 (idm a);

for C being category

for a being Object of C holds C -carrier_of a = proj1 (idm a);

definition

let C be category;

end;
attr C is set-id-inheriting means :Def10: :: YELLOW18:def 10

for a being Object of C holds idm a = id (the_carrier_of a);

for a being Object of C holds idm a = id (the_carrier_of a);

:: deftheorem Def10 defines set-id-inheriting YELLOW18:def 10 :

for C being category holds

( C is set-id-inheriting iff for a being Object of C holds idm a = id (the_carrier_of a) );

for C being category holds

( C is set-id-inheriting iff for a being Object of C holds idm a = id (the_carrier_of a) );

definition

let C be category;

end;
attr C is concrete means :: YELLOW18:def 11

( C is para-functional & C is semi-functional & C is set-id-inheriting );

( C is para-functional & C is semi-functional & C is set-id-inheriting );

:: deftheorem defines concrete YELLOW18:def 11 :

for C being category holds

( C is concrete iff ( C is para-functional & C is semi-functional & C is set-id-inheriting ) );

for C being category holds

( C is concrete iff ( C is para-functional & C is semi-functional & C is set-id-inheriting ) );

registration

for b_{1} being category st b_{1} is concrete holds

( b_{1} is para-functional & b_{1} is semi-functional & b_{1} is set-id-inheriting )
;

for b_{1} being category st b_{1} is para-functional & b_{1} is semi-functional & b_{1} is set-id-inheriting holds

b_{1} is concrete
;

end;

cluster non empty transitive associative with_units concrete -> semi-functional para-functional set-id-inheriting for category;

coherence for b

( b

cluster non empty transitive semi-functional associative with_units para-functional set-id-inheriting -> concrete for category;

coherence for b

b

registration

ex b_{1} being category st

( b_{1} is concrete & b_{1} is quasi-functional & b_{1} is strict )
end;

cluster non empty transitive strict quasi-functional associative with_units reflexive concrete for category;

existence ex b

( b

proof end;

theorem Th33: :: YELLOW18:33

for C being category holds

( C is para-functional iff for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2)) )

( C is para-functional iff for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2)) )

proof end;

theorem Th34: :: YELLOW18:34

for C being para-functional category

for a, b being Object of C st <^a,b^> <> {} holds

for f being Morphism of a,b holds f is Function of (the_carrier_of a),(the_carrier_of b)

for a, b being Object of C st <^a,b^> <> {} holds

for f being Morphism of a,b holds f is Function of (the_carrier_of a),(the_carrier_of b)

proof end;

registration

let A be para-functional category;

let a, b be Object of A;

coherence

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

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

end;
let a, b be Object of A;

coherence

for b

( b

proof end;

theorem Th35: :: YELLOW18:35

for C being para-functional category

for a, b being Object of C st <^a,b^> <> {} holds

for f being Morphism of a,b holds

( dom f = the_carrier_of a & rng f c= the_carrier_of b )

for a, b being Object of C st <^a,b^> <> {} holds

for f being Morphism of a,b holds

( dom f = the_carrier_of a & rng f c= the_carrier_of b )

proof end;

theorem Th36: :: YELLOW18:36

for C being semi-functional para-functional category

for a, b, c being Object of C st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = g * f

for a, b, c being Object of C st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = g * f

proof end;

theorem Th37: :: YELLOW18:37

for C being semi-functional para-functional category

for a being Object of C st id (the_carrier_of a) in <^a,a^> holds

idm a = id (the_carrier_of a)

for a being Object of C st id (the_carrier_of a) in <^a,a^> holds

idm a = id (the_carrier_of a)

proof end;

scheme :: YELLOW18:sch 16

ConcreteCategoryLambda{ F_{1}() -> non empty set , F_{2}( object , object ) -> set , F_{3}( object ) -> set } :

ConcreteCategoryLambda{ F

ex C being strict concrete category st

( the carrier of C = F_{1}() & ( for a being Object of C holds the_carrier_of a = F_{3}(a) ) & ( for a, b being Object of C holds <^a,b^> = F_{2}(a,b) ) )

provided( the carrier of C = F

A1:
for a, b, c being Element of F_{1}()

for f, g being Function st f in F_{2}(a,b) & g in F_{2}(b,c) holds

g * f in F_{2}(a,c)
and

A2: for a, b being Element of F_{1}() holds F_{2}(a,b) c= Funcs (F_{3}(a),F_{3}(b))
and

A3: for a being Element of F_{1}() holds id F_{3}(a) in F_{2}(a,a)

for f, g being Function st f in F

g * f in F

A2: for a, b being Element of F

A3: for a being Element of F

proof end;

scheme :: YELLOW18:sch 17

ConcreteCategoryQuasiLambda{ F_{1}() -> non empty set , P_{1}[ object , object , object ], F_{2}( object ) -> set } :

ConcreteCategoryQuasiLambda{ F

ex C being strict concrete category st

( the carrier of C = F_{1}() & ( for a being Object of C holds the_carrier_of a = F_{2}(a) ) & ( for a, b being Element of F_{1}()

for f being Function holds

( f in the Arrows of C . (a,b) iff ( f in Funcs (F_{2}(a),F_{2}(b)) & P_{1}[a,b,f] ) ) ) )

provided( the carrier of C = F

for f being Function holds

( f in the Arrows of C . (a,b) iff ( f in Funcs (F

A1:
for a, b, c being Element of F_{1}()

for f, g being Function st P_{1}[a,b,f] & P_{1}[b,c,g] holds

P_{1}[a,c,g * f]
and

A2: for a being Element of F_{1}() holds P_{1}[a,a, id F_{2}(a)]

for f, g being Function st P

P

A2: for a being Element of F

proof end;

scheme :: YELLOW18:sch 18

ConcreteCategoryEx{ F_{1}() -> non empty set , F_{2}( object ) -> set , P_{1}[ object , object ], P_{2}[ object , object , object ] } :

ConcreteCategoryEx{ F

ex C being strict concrete category st

( the carrier of C = F_{1}() & ( for a being Object of C

for x being set holds

( x in the_carrier_of a iff ( x in F_{2}(a) & P_{1}[a,x] ) ) ) & ( for a, b being Element of F_{1}()

for f being Function holds

( f in the Arrows of C . (a,b) iff ( f in Funcs ((C -carrier_of a),(C -carrier_of b)) & P_{2}[a,b,f] ) ) ) )

provided( the carrier of C = F

for x being set holds

( x in the_carrier_of a iff ( x in F

for f being Function holds

( f in the Arrows of C . (a,b) iff ( f in Funcs ((C -carrier_of a),(C -carrier_of b)) & P

A1:
for a, b, c being Element of F_{1}()

for f, g being Function st P_{2}[a,b,f] & P_{2}[b,c,g] holds

P_{2}[a,c,g * f]
and

A2: for a being Element of F_{1}()

for X being set st ( for x being set holds

( x in X iff ( x in F_{2}(a) & P_{1}[a,x] ) ) ) holds

P_{2}[a,a, id X]

for f, g being Function st P

P

A2: for a being Element of F

for X being set st ( for x being set holds

( x in X iff ( x in F

P

proof end;

scheme :: YELLOW18:sch 19

ConcreteCategoryUniq1{ F_{1}() -> non empty set , F_{2}( object , object ) -> object } :

ConcreteCategoryUniq1{ F

for C1, C2 being semi-functional para-functional category st the carrier of C1 = F_{1}() & ( for a, b being Object of C1 holds <^a,b^> = F_{2}(a,b) ) & the carrier of C2 = F_{1}() & ( for a, b being Object of C2 holds <^a,b^> = F_{2}(a,b) ) holds

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

proof end;

scheme :: YELLOW18:sch 20

ConcreteCategoryUniq2{ F_{1}() -> non empty set , P_{1}[ object , object , object ], F_{2}( object ) -> set } :

ConcreteCategoryUniq2{ F

for C1, C2 being semi-functional para-functional category st the carrier of C1 = F_{1}() & ( for a, b being Element of F_{1}()

for f being Function holds

( f in the Arrows of C1 . (a,b) iff ( f in Funcs (F_{2}(a),F_{2}(b)) & P_{1}[a,b,f] ) ) ) & the carrier of C2 = F_{1}() & ( for a, b being Element of F_{1}()

for f being Function holds

( f in the Arrows of C2 . (a,b) iff ( f in Funcs (F_{2}(a),F_{2}(b)) & P_{1}[a,b,f] ) ) ) holds

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

for f being Function holds

( f in the Arrows of C1 . (a,b) iff ( f in Funcs (F

for f being Function holds

( f in the Arrows of C2 . (a,b) iff ( f in Funcs (F

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

proof end;

scheme :: YELLOW18:sch 21

ConcreteCategoryUniq3{ F_{1}() -> non empty set , F_{2}( object ) -> set , P_{1}[ object , object ], P_{2}[ object , object , object ] } :

ConcreteCategoryUniq3{ F

for C1, C2 being semi-functional para-functional category st the carrier of C1 = F_{1}() & ( for a being Object of C1

for x being set holds

( x in the_carrier_of a iff ( x in F_{2}(a) & P_{1}[a,x] ) ) ) & ( for a, b being Element of F_{1}()

for f being Function holds

( f in the Arrows of C1 . (a,b) iff ( f in Funcs ((C1 -carrier_of a),(C1 -carrier_of b)) & P_{2}[a,b,f] ) ) ) & the carrier of C2 = F_{1}() & ( for a being Object of C2

for x being set holds

( x in the_carrier_of a iff ( x in F_{2}(a) & P_{1}[a,x] ) ) ) & ( for a, b being Element of F_{1}()

for f being Function holds

( f in the Arrows of C2 . (a,b) iff ( f in Funcs ((C2 -carrier_of a),(C2 -carrier_of b)) & P_{2}[a,b,f] ) ) ) holds

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

for x being set holds

( x in the_carrier_of a iff ( x in F

for f being Function holds

( f in the Arrows of C1 . (a,b) iff ( f in Funcs ((C1 -carrier_of a),(C1 -carrier_of b)) & P

for x being set holds

( x in the_carrier_of a iff ( x in F

for f being Function holds

( f in the Arrows of C2 . (a,b) iff ( f in Funcs ((C2 -carrier_of a),(C2 -carrier_of b)) & P

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

proof end;

:: <section5>Equivalence between concrete categories</section5>

theorem Th38: :: YELLOW18:38

for C being concrete category

for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds

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

rng f = the_carrier_of b

for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds

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

rng f = the_carrier_of b

proof end;

theorem Th39: :: YELLOW18:39

for C being concrete category

for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds

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

f is one-to-one

for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds

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

f is one-to-one

proof end;

theorem Th41: :: YELLOW18:41

for C being semi-functional para-functional category

for a, b being Object of C st <^a,b^> <> {} holds

for f being Morphism of a,b st f is one-to-one & f " in <^b,a^> holds

f is iso

for a, b being Object of C st <^a,b^> <> {} holds

for f being Morphism of a,b st f is one-to-one & f " in <^b,a^> holds

f is iso

proof end;

theorem :: YELLOW18:42

for C being concrete category

for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds

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

f " = f "

for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds

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

f " = f "

proof end;

scheme :: YELLOW18:sch 22

ConcreteCatEquivalence{ F_{1}() -> semi-functional para-functional category, F_{2}() -> semi-functional para-functional category, F_{3}( object ) -> object , F_{4}( object ) -> object , F_{5}( object , object , object ) -> Function, F_{6}( object , object , object ) -> Function, F_{7}( object ) -> Function, F_{8}( object ) -> Function } :

provided

ConcreteCatEquivalence{ F

provided

A1:
ex F being covariant Functor of F_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}(a) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{5}(a,b,f) ) )
and

A2: ex G being covariant Functor of F_{2}(),F_{1}() st

( ( for a being Object of F_{2}() holds G . a = F_{4}(a) ) & ( for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds G . f = F_{6}(a,b,f) ) )
and

A3: for a, b being Object of F_{1}() st a = F_{4}(F_{3}(b)) holds

( F_{7}(b) in <^a,b^> & F_{7}(b) " in <^b,a^> & F_{7}(b) is one-to-one )
and

A4: for a, b being Object of F_{2}() st b = F_{3}(F_{4}(a)) holds

( F_{8}(a) in <^a,b^> & F_{8}(a) " in <^b,a^> & F_{8}(a) is one-to-one )
and

A5: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{7}(b) * F_{6}(F_{3}(a),F_{3}(b),F_{5}(a,b,f)) = f * F_{7}(a)
and

A6: for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{5}(F_{4}(a),F_{4}(b),F_{6}(a,b,f)) * F_{8}(a) = F_{8}(b) * f

( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

A2: ex G being covariant Functor of F

( ( for a being Object of F

for f being Morphism of a,b holds G . f = F

A3: for a, b being Object of F

( F

A4: for a, b being Object of F

( F

A5: for a, b being Object of F

for f being Morphism of a,b holds F

A6: for a, b being Object of F

for f being Morphism of a,b holds F

proof end;

:: <section6>Concretization of categories</section6>

definition

let C be category;

defpred S_{1}[ set , set ] means $1 = $2 `22 ;

defpred S_{2}[ set , set , Function] means ex fa, fb being Object of C ex g being Morphism of fa,fb st

( fa = $1 & fb = $2 & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds $3 . [h,[o,fa]] = [(g * h),[o,fb]] ) );

deffunc H_{1}( set ) -> set = Union (disjoin the Arrows of C);

A1: for a, b, c being Element of C

for f, g being Function st S_{2}[a,b,f] & S_{2}[b,c,g] holds

S_{2}[a,c,g * f]

for X being set st ( for x being set holds

( x in X iff ( x in H_{1}(a) & S_{1}[a,x] ) ) ) holds

S_{2}[a,a, id X]

for b_{1}, b_{2} being strict concrete category st the carrier of b_{1} = the carrier of C & ( for a being Object of b_{1}

for x being set holds

( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C

for f being Function holds

( f in the Arrows of b_{1} . (a,b) iff ( f in Funcs ((b_{1} -carrier_of a),(b_{1} -carrier_of b)) & ex fa, fb being Object of C ex g being Morphism of fa,fb st

( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) & the carrier of b_{2} = the carrier of C & ( for a being Object of b_{2}

for x being set holds

( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C

for f being Function holds

( f in the Arrows of b_{2} . (a,b) iff ( f in Funcs ((b_{2} -carrier_of a),(b_{2} -carrier_of b)) & ex fa, fb being Object of C ex g being Morphism of fa,fb st

( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) holds

b_{1} = b_{2}

ex b_{1} being strict concrete category st

( the carrier of b_{1} = the carrier of C & ( for a being Object of b_{1}

for x being set holds

( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C

for f being Function holds

( f in the Arrows of b_{1} . (a,b) iff ( f in Funcs ((b_{1} -carrier_of a),(b_{1} -carrier_of b)) & ex fa, fb being Object of C ex g being Morphism of fa,fb st

( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) )

end;
defpred S

defpred S

( fa = $1 & fb = $2 & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds $3 . [h,[o,fa]] = [(g * h),[o,fb]] ) );

deffunc H

A1: for a, b, c being Element of C

for f, g being Function st S

S

proof end;

A13:
for a being Element of Cfor X being set st ( for x being set holds

( x in X iff ( x in H

S

proof end;

func Concretized C -> strict concrete category means :Def12: :: YELLOW18:def 12

( the carrier of it = the carrier of C & ( for a being Object of it

for x being set holds

( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C

for f being Function holds

( f in the Arrows of it . (a,b) iff ( f in Funcs ((it -carrier_of a),(it -carrier_of b)) & ex fa, fb being Object of C ex g being Morphism of fa,fb st

( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) );

uniqueness ( the carrier of it = the carrier of C & ( for a being Object of it

for x being set holds

( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C

for f being Function holds

( f in the Arrows of it . (a,b) iff ( f in Funcs ((it -carrier_of a),(it -carrier_of b)) & ex fa, fb being Object of C ex g being Morphism of fa,fb st

( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) );

for b

for x being set holds

( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C

for f being Function holds

( f in the Arrows of b

( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) & the carrier of b

for x being set holds

( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C

for f being Function holds

( f in the Arrows of b

( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) holds

b

proof end;

existence ex b

( the carrier of b

for x being set holds

( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C

for f being Function holds

( f in the Arrows of b

( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) )

proof end;

:: deftheorem Def12 defines Concretized YELLOW18:def 12 :

for C being category

for b_{2} being strict concrete category holds

( b_{2} = Concretized C iff ( the carrier of b_{2} = the carrier of C & ( for a being Object of b_{2}

for x being set holds

( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C

for f being Function holds

( f in the Arrows of b_{2} . (a,b) iff ( f in Funcs ((b_{2} -carrier_of a),(b_{2} -carrier_of b)) & ex fa, fb being Object of C ex g being Morphism of fa,fb st

( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) ) );

for C being category

for b

( b

for x being set holds

( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C

for f being Function holds

( f in the Arrows of b

( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds

for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) ) );

theorem Th43: :: YELLOW18:43

for A being category

for a being Object of A

for x being set holds

( x in (Concretized A) -carrier_of a iff ex b being Object of A ex f being Morphism of b,a st

( <^b,a^> <> {} & x = [f,[b,a]] ) )

for a being Object of A

for x being set holds

( x in (Concretized A) -carrier_of a iff ex b being Object of A ex f being Morphism of b,a st

( <^b,a^> <> {} & x = [f,[b,a]] ) )

proof end;

registration

let A be category;

let a be Object of A;

coherence

not (Concretized A) -carrier_of a is empty

end;
let a be Object of A;

coherence

not (Concretized A) -carrier_of a is empty

proof end;

theorem Th44: :: YELLOW18:44

for A being category

for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b ex F being Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) st

( F in the Arrows of (Concretized A) . (a,b) & ( for c being Object of A

for g being Morphism of c,a st <^c,a^> <> {} holds

F . [g,[c,a]] = [(f * g),[c,b]] ) )

for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b ex F being Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) st

( F in the Arrows of (Concretized A) . (a,b) & ( for c being Object of A

for g being Morphism of c,a st <^c,a^> <> {} holds

F . [g,[c,a]] = [(f * g),[c,b]] ) )

proof end;

theorem Th45: :: YELLOW18:45

for A being category

for a, b being Object of A

for F1, F2 being Function st F1 in the Arrows of (Concretized A) . (a,b) & F2 in the Arrows of (Concretized A) . (a,b) & F1 . [(idm a),[a,a]] = F2 . [(idm a),[a,a]] holds

F1 = F2

for a, b being Object of A

for F1, F2 being Function st F1 in the Arrows of (Concretized A) . (a,b) & F2 in the Arrows of (Concretized A) . (a,b) & F1 . [(idm a),[a,a]] = F2 . [(idm a),[a,a]] holds

F1 = F2

proof end;

scheme :: YELLOW18:sch 23

NonUniqMSFunctionEx{ F_{1}() -> set , F_{2}() -> ManySortedSet of F_{1}(), F_{3}() -> ManySortedSet of F_{1}(), P_{1}[ object , object , object ] } :

NonUniqMSFunctionEx{ F

ex F being ManySortedFunction of F_{2}(),F_{3}() st

for i, x being object st i in F_{1}() & x in F_{2}() . i holds

( (F . i) . x in F_{3}() . i & P_{1}[i,x,(F . i) . x] )

providedfor i, x being object st i in F

( (F . i) . x in F

A1:
for i, x being object st i in F_{1}() & x in F_{2}() . i holds

ex y being object st

( y in F_{3}() . i & P_{1}[i,x,y] )

ex y being object st

( y in F

proof end;

definition

let A be category;

set B = Concretized A;

for b_{1}, b_{2} being strict covariant Functor of A, Concretized A st ( for a being Object of A holds b_{1} . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds (b_{1} . f) . [(idm a),[a,a]] = [f,[a,b]] ) & ( for a being Object of A holds b_{2} . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds (b_{2} . f) . [(idm a),[a,a]] = [f,[a,b]] ) holds

b_{1} = b_{2}

ex b_{1} being strict covariant Functor of A, Concretized A st

( ( for a being Object of A holds b_{1} . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds (b_{1} . f) . [(idm a),[a,a]] = [f,[a,b]] ) )

end;
set B = Concretized A;

func Concretization A -> strict covariant Functor of A, Concretized A means :Def13: :: YELLOW18:def 13

( ( for a being Object of A holds it . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds (it . f) . [(idm a),[a,a]] = [f,[a,b]] ) );

uniqueness ( ( for a being Object of A holds it . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds (it . f) . [(idm a),[a,a]] = [f,[a,b]] ) );

for b

for f being Morphism of a,b holds (b

for f being Morphism of a,b holds (b

b

proof end;

existence ex b

( ( for a being Object of A holds b

for f being Morphism of a,b holds (b

proof end;

:: deftheorem Def13 defines Concretization YELLOW18:def 13 :

for A being category

for b_{2} being strict covariant Functor of A, Concretized A holds

( b_{2} = Concretization A iff ( ( for a being Object of A holds b_{2} . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds (b_{2} . f) . [(idm a),[a,a]] = [f,[a,b]] ) ) );

for A being category

for b

( b

for f being Morphism of a,b holds (b