:: by Grzegorz Bancerek

::

:: Received July 31, 2001

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

theorem Th1: :: YELLOW20:1

for A, B being non empty transitive with_units AltCatStr

for F being reflexive feasible FunctorStr over A,B st F is coreflexive & F is bijective holds

for a being Object of A

for b being Object of B holds

( F . a = b iff (F ") . b = a )

for F being reflexive feasible FunctorStr over A,B st F is coreflexive & F is bijective holds

for a being Object of A

for b being Object of B holds

( F . a = b iff (F ") . b = a )

proof end;

theorem Th2: :: YELLOW20:2

for A, B being non empty transitive with_units AltCatStr

for F being feasible Covariant FunctorStr over A,B

for G being feasible Covariant FunctorStr over B,A st F is bijective & G = F " holds

for a1, a2 being Object of A st <^a1,a2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of (F . a1),(F . a2) holds

( F . f = g iff G . g = f )

for F being feasible Covariant FunctorStr over A,B

for G being feasible Covariant FunctorStr over B,A st F is bijective & G = F " holds

for a1, a2 being Object of A st <^a1,a2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of (F . a1),(F . a2) holds

( F . f = g iff G . g = f )

proof end;

theorem Th3: :: YELLOW20:3

for A, B being non empty transitive with_units AltCatStr

for F being feasible Contravariant FunctorStr over A,B

for G being feasible Contravariant FunctorStr over B,A st F is bijective & G = F " holds

for a1, a2 being Object of A st <^a1,a2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of (F . a2),(F . a1) holds

( F . f = g iff G . g = f )

for F being feasible Contravariant FunctorStr over A,B

for G being feasible Contravariant FunctorStr over B,A st F is bijective & G = F " holds

for a1, a2 being Object of A st <^a1,a2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of (F . a2),(F . a1) holds

( F . f = g iff G . g = f )

proof end;

theorem Th4: :: YELLOW20:4

for A, B being category

for F being Functor of A,B st F is bijective holds

for G being Functor of B,A st F * G = id B holds

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

for F being Functor of A,B st F is bijective holds

for G being Functor of B,A st F * G = id B holds

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

proof end;

theorem Th5: :: YELLOW20:5

for A, B being category

for F being Functor of A,B st F is bijective holds

for G being Functor of B,A st G * F = id A holds

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

for F being Functor of A,B st F is bijective holds

for G being Functor of B,A st G * F = id A holds

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

proof end;

theorem :: YELLOW20:6

for A, B being category

for F being covariant Functor of A,B st F is bijective holds

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

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

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

for F being covariant Functor of A,B st F is bijective holds

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

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

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

proof end;

theorem :: YELLOW20:7

for A, B being category

for F being contravariant Functor of A,B st F is bijective holds

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

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

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

for F being contravariant Functor of A,B st F is bijective holds

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

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

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

proof end;

theorem :: YELLOW20:8

for A, B being category

for F being covariant Functor of A,B st F is bijective holds

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

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

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

for F being covariant Functor of A,B st F is bijective holds

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

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

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

proof end;

theorem :: YELLOW20:9

for A, B being category

for F being contravariant Functor of A,B st F is bijective holds

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

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

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

for F being contravariant Functor of A,B st F is bijective holds

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

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

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

proof end;

definition

let A, B be AltCatStr ;

for A, B being AltCatStr st ( for a1, a2, a3 being object holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] ) holds

for a1, a2, a3 being object holds the Comp of B . [a1,a2,a3] tolerates the Comp of A . [a1,a2,a3] ;

end;
pred A,B have_the_same_composition means :: YELLOW20:def 1

for a1, a2, a3 being object holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3];

symmetry for a1, a2, a3 being object holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3];

for A, B being AltCatStr st ( for a1, a2, a3 being object holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] ) holds

for a1, a2, a3 being object holds the Comp of B . [a1,a2,a3] tolerates the Comp of A . [a1,a2,a3] ;

:: deftheorem defines have_the_same_composition YELLOW20:def 1 :

for A, B being AltCatStr holds

( A,B have_the_same_composition iff for a1, a2, a3 being object holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] );

for A, B being AltCatStr holds

( A,B have_the_same_composition iff for a1, a2, a3 being object holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] );

theorem Th10: :: YELLOW20:10

for A, B being AltCatStr holds

( A,B have_the_same_composition iff for a1, a2, a3, x being object st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds

( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )

( A,B have_the_same_composition iff for a1, a2, a3, x being object st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds

( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )

proof end;

theorem Th11: :: YELLOW20:11

for A, B being non empty transitive AltCatStr holds

( A,B have_the_same_composition iff for a1, a2, a3 being Object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds

for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 )

( A,B have_the_same_composition iff for a1, a2, a3 being Object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds

for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 )

proof end;

definition

let f, g be Function;

ex b_{1} being Function st

( dom b_{1} = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds

b_{1} . x = (f . x) /\ (g . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds

b_{1} . x = (f . x) /\ (g . x) ) & dom b_{2} = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds

b_{2} . x = (f . x) /\ (g . x) ) holds

b_{1} = b_{2}

for b_{1}, f, g being Function st dom b_{1} = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds

b_{1} . x = (f . x) /\ (g . x) ) holds

( dom b_{1} = (dom g) /\ (dom f) & ( for x being object st x in (dom g) /\ (dom f) holds

b_{1} . x = (g . x) /\ (f . x) ) )
;

end;
func Intersect (f,g) -> Function means :Def2: :: YELLOW20:def 2

( dom it = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds

it . x = (f . x) /\ (g . x) ) );

existence ( dom it = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds

it . x = (f . x) /\ (g . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

b

( dom b

b

:: deftheorem Def2 defines Intersect YELLOW20:def 2 :

for f, g, b_{3} being Function holds

( b_{3} = Intersect (f,g) iff ( dom b_{3} = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds

b_{3} . x = (f . x) /\ (g . x) ) ) );

for f, g, b

( b

b

theorem Th14: :: YELLOW20:14

for I, J being set

for A being ManySortedSet of I

for B being ManySortedSet of J holds Intersect (A,B) is ManySortedSet of I /\ J

for A being ManySortedSet of I

for B being ManySortedSet of J holds Intersect (A,B) is ManySortedSet of I /\ J

proof end;

theorem Th15: :: YELLOW20:15

for I, J being set

for A being ManySortedSet of I

for B being Function

for C being ManySortedSet of J st C = Intersect (A,B) holds

C cc= A

for A being ManySortedSet of I

for B being Function

for C being ManySortedSet of J st C = Intersect (A,B) holds

C cc= A

proof end;

theorem Th16: :: YELLOW20:16

for I1, I2 being set

for A1, B1 being ManySortedSet of I1

for A2, B2 being ManySortedSet of I2

for A, B being ManySortedSet of I1 /\ I2 st A = Intersect (A1,A2) & B = Intersect (B1,B2) holds

for F being ManySortedFunction of A1,B1

for G being ManySortedFunction of A2,B2 st ( for x being set st x in dom F & x in dom G holds

F . x tolerates G . x ) holds

Intersect (F,G) is ManySortedFunction of A,B

for A1, B1 being ManySortedSet of I1

for A2, B2 being ManySortedSet of I2

for A, B being ManySortedSet of I1 /\ I2 st A = Intersect (A1,A2) & B = Intersect (B1,B2) holds

for F being ManySortedFunction of A1,B1

for G being ManySortedFunction of A2,B2 st ( for x being set st x in dom F & x in dom G holds

F . x tolerates G . x ) holds

Intersect (F,G) is ManySortedFunction of A,B

proof end;

theorem Th17: :: YELLOW20:17

for I, J being set

for F being ManySortedSet of [:I,I:]

for G being ManySortedSet of [:J,J:] ex H being ManySortedSet of [:(I /\ J),(I /\ J):] st

( H = Intersect (F,G) & Intersect ({|F|},{|G|}) = {|H|} )

for F being ManySortedSet of [:I,I:]

for G being ManySortedSet of [:J,J:] ex H being ManySortedSet of [:(I /\ J),(I /\ J):] st

( H = Intersect (F,G) & Intersect ({|F|},{|G|}) = {|H|} )

proof end;

theorem Th18: :: YELLOW20:18

for I, J being set

for F1, F2 being ManySortedSet of [:I,I:]

for G1, G2 being ManySortedSet of [:J,J:] ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st

( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )

for F1, F2 being ManySortedSet of [:I,I:]

for G1, G2 being ManySortedSet of [:J,J:] ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st

( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )

proof end;

definition

let A, B be AltCatStr ;

assume A1: A,B have_the_same_composition ;

ex b_{1} being strict AltCatStr st

( the carrier of b_{1} = the carrier of A /\ the carrier of B & the Arrows of b_{1} = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b_{1} = Intersect ( the Comp of A, the Comp of B) )

for b_{1}, b_{2} being strict AltCatStr st the carrier of b_{1} = the carrier of A /\ the carrier of B & the Arrows of b_{1} = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b_{1} = Intersect ( the Comp of A, the Comp of B) & the carrier of b_{2} = the carrier of A /\ the carrier of B & the Arrows of b_{2} = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b_{2} = Intersect ( the Comp of A, the Comp of B) holds

b_{1} = b_{2}
;

end;
assume A1: A,B have_the_same_composition ;

func Intersect (A,B) -> strict AltCatStr means :Def3: :: YELLOW20:def 3

( the carrier of it = the carrier of A /\ the carrier of B & the Arrows of it = Intersect ( the Arrows of A, the Arrows of B) & the Comp of it = Intersect ( the Comp of A, the Comp of B) );

existence ( the carrier of it = the carrier of A /\ the carrier of B & the Arrows of it = Intersect ( the Arrows of A, the Arrows of B) & the Comp of it = Intersect ( the Comp of A, the Comp of B) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines Intersect YELLOW20:def 3 :

for A, B being AltCatStr st A,B have_the_same_composition holds

for b_{3} being strict AltCatStr holds

( b_{3} = Intersect (A,B) iff ( the carrier of b_{3} = the carrier of A /\ the carrier of B & the Arrows of b_{3} = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b_{3} = Intersect ( the Comp of A, the Comp of B) ) );

for A, B being AltCatStr st A,B have_the_same_composition holds

for b

( b

theorem Th21: :: YELLOW20:21

for A, B being AltCatStr st A,B have_the_same_composition holds

for a1, a2 being Object of A

for b1, b2 being Object of B

for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds

<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>

for a1, a2 being Object of A

for b1, b2 being Object of B

for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds

<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>

proof end;

theorem Th22: :: YELLOW20:22

for A, B being transitive AltCatStr st A,B have_the_same_composition holds

Intersect (A,B) is transitive

Intersect (A,B) is transitive

proof end;

theorem Th23: :: YELLOW20:23

for A, B being AltCatStr st A,B have_the_same_composition holds

for a1, a2 being Object of A

for b1, b2 being Object of B

for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^>

for a1, a2 being Object of A

for b1, b2 being Object of B

for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^>

proof end;

theorem :: YELLOW20:24

theorem :: YELLOW20:25

for A, B being category st A,B have_the_same_composition & not Intersect (A,B) is empty & ( for a being Object of A

for b being Object of B st a = b holds

idm a = idm b ) holds

Intersect (A,B) is subcategory of A

for b being Object of B st a = b holds

idm a = idm b ) holds

Intersect (A,B) is subcategory of A

proof end;

scheme :: YELLOW20:sch 1

SubcategoryUniq{ F_{1}() -> category, F_{2}() -> non empty subcategory of F_{1}(), F_{3}() -> non empty subcategory of F_{1}(), P_{1}[ set ], P_{2}[ set , set , set ] } :

SubcategoryUniq{ F

AltCatStr(# the carrier of F_{2}(), the Arrows of F_{2}(), the Comp of F_{2}() #) = AltCatStr(# the carrier of F_{3}(), the Arrows of F_{3}(), the Comp of F_{3}() #)

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

( a is Object of F_{2}() iff P_{1}[a] )
and

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

for a9, b9 being Object of F_{2}() 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] )
and

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

( a is Object of F_{3}() iff P_{1}[a] )
and

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

for a9, b9 being Object of F_{3}() 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] )

( a is Object of F

A2: for a, b being Object of F

for a9, b9 being Object of F

for f being Morphism of a,b holds

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

A3: for a being Object of F

( a is Object of F

A4: for a, b being Object of F

for a9, b9 being Object of F

for f being Morphism of a,b holds

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

proof end;

theorem Th26: :: YELLOW20:26

for A being non empty AltCatStr

for B being non empty SubCatStr of A holds

( B is full iff for a1, a2 being Object of A

for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds

<^b1,b2^> = <^a1,a2^> )

for B being non empty SubCatStr of A holds

( B is full iff for a1, a2 being Object of A

for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds

<^b1,b2^> = <^a1,a2^> )

proof end;

scheme :: YELLOW20:sch 3

FullSubcategoryUniq{ F_{1}() -> category, F_{2}() -> non empty full subcategory of F_{1}(), F_{3}() -> non empty full subcategory of F_{1}(), P_{1}[ set ] } :

FullSubcategoryUniq{ F

AltCatStr(# the carrier of F_{2}(), the Arrows of F_{2}(), the Comp of F_{2}() #) = AltCatStr(# the carrier of F_{3}(), the Arrows of F_{3}(), the Comp of F_{3}() #)

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

( a is Object of F_{2}() iff P_{1}[a] )
and

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

( a is Object of F_{3}() iff P_{1}[a] )

( a is Object of F

A2: for a being Object of F

( a is Object of F

proof end;

registration

let f be Function-yielding Function;

let x, y be set ;

coherence

( f . (x,y) is Relation-like & f . (x,y) is Function-like ) ;

end;
let x, y be set ;

coherence

( f . (x,y) is Relation-like & f . (x,y) is Function-like ) ;

theorem Th27: :: YELLOW20:27

for A being category

for C being non empty subcategory of A

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

for f being Morphism of a,b holds (incl C) . f = f

for C being non empty subcategory of A

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

for f being Morphism of a,b holds (incl C) . f = f

proof end;

registration

let A be category;

let C be non empty subcategory of A;

coherence

( incl C is id-preserving & incl C is comp-preserving )

end;
let C be non empty subcategory of A;

coherence

( incl C is id-preserving & incl C is comp-preserving )

proof end;

registration
end;

definition

let A be category;

let C be non empty subcategory of A;

:: original: incl

redefine func incl C -> strict covariant Functor of C,A;

coherence

incl C is strict covariant Functor of C,A by FUNCTOR0:def 25;

end;
let C be non empty subcategory of A;

:: original: incl

redefine func incl C -> strict covariant Functor of C,A;

coherence

incl C is strict covariant Functor of C,A by FUNCTOR0:def 25;

definition

let A, B be category;

let C be non empty subcategory of A;

let F be covariant Functor of A,B;

:: original: |

redefine func F | C -> strict covariant Functor of C,B;

coherence

F | C is strict covariant Functor of C,B

end;
let C be non empty subcategory of A;

let F be covariant Functor of A,B;

:: original: |

redefine func F | C -> strict covariant Functor of C,B;

coherence

F | C is strict covariant Functor of C,B

proof end;

definition

let A, B be category;

let C be non empty subcategory of A;

let F be contravariant Functor of A,B;

:: original: |

redefine func F | C -> strict contravariant Functor of C,B;

coherence

F | C is strict contravariant Functor of C,B

end;
let C be non empty subcategory of A;

let F be contravariant Functor of A,B;

:: original: |

redefine func F | C -> strict contravariant Functor of C,B;

coherence

F | C is strict contravariant Functor of C,B

proof end;

theorem Th28: :: YELLOW20:28

for A, B being category

for C being non empty subcategory of A

for F being FunctorStr over A,B

for a being Object of A

for c being Object of C st c = a holds

(F | C) . c = F . a

for C being non empty subcategory of A

for F being FunctorStr over A,B

for a being Object of A

for c being Object of C st c = a holds

(F | C) . c = F . a

proof end;

theorem Th29: :: YELLOW20:29

for A, B being category

for C being non empty subcategory of A

for F being covariant Functor of A,B

for a, b being Object of A

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

for f being Morphism of a,b

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

(F | C) . g = F . f

for C being non empty subcategory of A

for F being covariant Functor of A,B

for a, b being Object of A

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

for f being Morphism of a,b

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

(F | C) . g = F . f

proof end;

theorem Th30: :: YELLOW20:30

for A, B being category

for C being non empty subcategory of A

for F being contravariant Functor of A,B

for a, b being Object of A

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

for f being Morphism of a,b

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

(F | C) . g = F . f

for C being non empty subcategory of A

for F being contravariant Functor of A,B

for a, b being Object of A

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

for f being Morphism of a,b

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

(F | C) . g = F . f

proof end;

theorem Th31: :: YELLOW20:31

for A, B being non empty AltGraph

for F being BimapStr over A,B st F is Covariant & F is one-to-one holds

for a, b being Object of A st F . a = F . b holds

a = b

for F being BimapStr over A,B st F is Covariant & F is one-to-one holds

for a, b being Object of A st F . a = F . b holds

a = b

proof end;

theorem Th32: :: YELLOW20:32

for A, B being non empty reflexive AltGraph

for F being feasible Covariant FunctorStr over A,B st F is faithful holds

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

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

f = g

for F being feasible Covariant FunctorStr over A,B st F is faithful holds

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

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

f = g

proof end;

theorem Th33: :: YELLOW20:33

for A, B being non empty AltGraph

for F being Covariant FunctorStr over A,B st F is surjective holds

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

for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st

( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )

for F being Covariant FunctorStr over A,B st F is surjective holds

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

for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st

( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )

proof end;

theorem Th34: :: YELLOW20:34

for A, B being non empty AltGraph

for F being BimapStr over A,B st F is Contravariant & F is one-to-one holds

for a, b being Object of A st F . a = F . b holds

a = b

for F being BimapStr over A,B st F is Contravariant & F is one-to-one holds

for a, b being Object of A st F . a = F . b holds

a = b

proof end;

theorem Th35: :: YELLOW20:35

for A, B being non empty reflexive AltGraph

for F being feasible Contravariant FunctorStr over A,B st F is faithful holds

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

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

f = g

for F being feasible Contravariant FunctorStr over A,B st F is faithful holds

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

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

f = g

proof end;

theorem Th36: :: YELLOW20:36

for A, B being non empty AltGraph

for F being Contravariant FunctorStr over A,B st F is surjective holds

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

for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st

( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )

for F being Contravariant FunctorStr over A,B st F is surjective holds

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

for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st

( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )

proof end;

definition

let A, B be category;

let F be FunctorStr over A,B;

let A9, B9 be category;

end;
let F be FunctorStr over A,B;

let A9, B9 be category;

pred A9,B9 are_isomorphic_under F means :: YELLOW20:def 4

( A9 is subcategory of A & B9 is subcategory of B & ex G being covariant Functor of A9,B9 st

( G is bijective & ( for a9 being Object of A9

for a being Object of A st a9 = a holds

G . a9 = F . a ) & ( for b9, c9 being Object of A9

for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds

for f9 being Morphism of b9,c9

for f being Morphism of b,c st f9 = f holds

G . f9 = (Morph-Map (F,b,c)) . f ) ) );

( A9 is subcategory of A & B9 is subcategory of B & ex G being covariant Functor of A9,B9 st

( G is bijective & ( for a9 being Object of A9

for a being Object of A st a9 = a holds

G . a9 = F . a ) & ( for b9, c9 being Object of A9

for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds

for f9 being Morphism of b9,c9

for f being Morphism of b,c st f9 = f holds

G . f9 = (Morph-Map (F,b,c)) . f ) ) );

pred A9,B9 are_anti-isomorphic_under F means :: YELLOW20:def 5

( A9 is subcategory of A & B9 is subcategory of B & ex G being contravariant Functor of A9,B9 st

( G is bijective & ( for a9 being Object of A9

for a being Object of A st a9 = a holds

G . a9 = F . a ) & ( for b9, c9 being Object of A9

for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds

for f9 being Morphism of b9,c9

for f being Morphism of b,c st f9 = f holds

G . f9 = (Morph-Map (F,b,c)) . f ) ) );

( A9 is subcategory of A & B9 is subcategory of B & ex G being contravariant Functor of A9,B9 st

( G is bijective & ( for a9 being Object of A9

for a being Object of A st a9 = a holds

G . a9 = F . a ) & ( for b9, c9 being Object of A9

for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds

for f9 being Morphism of b9,c9

for f being Morphism of b,c st f9 = f holds

G . f9 = (Morph-Map (F,b,c)) . f ) ) );

:: deftheorem defines are_isomorphic_under YELLOW20:def 4 :

for A, B being category

for F being FunctorStr over A,B

for A9, B9 being category holds

( A9,B9 are_isomorphic_under F iff ( A9 is subcategory of A & B9 is subcategory of B & ex G being covariant Functor of A9,B9 st

( G is bijective & ( for a9 being Object of A9

for a being Object of A st a9 = a holds

G . a9 = F . a ) & ( for b9, c9 being Object of A9

for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds

for f9 being Morphism of b9,c9

for f being Morphism of b,c st f9 = f holds

G . f9 = (Morph-Map (F,b,c)) . f ) ) ) );

for A, B being category

for F being FunctorStr over A,B

for A9, B9 being category holds

( A9,B9 are_isomorphic_under F iff ( A9 is subcategory of A & B9 is subcategory of B & ex G being covariant Functor of A9,B9 st

( G is bijective & ( for a9 being Object of A9

for a being Object of A st a9 = a holds

G . a9 = F . a ) & ( for b9, c9 being Object of A9

for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds

for f9 being Morphism of b9,c9

for f being Morphism of b,c st f9 = f holds

G . f9 = (Morph-Map (F,b,c)) . f ) ) ) );

:: deftheorem defines are_anti-isomorphic_under YELLOW20:def 5 :

for A, B being category

for F being FunctorStr over A,B

for A9, B9 being category holds

( A9,B9 are_anti-isomorphic_under F iff ( A9 is subcategory of A & B9 is subcategory of B & ex G being contravariant Functor of A9,B9 st

( G is bijective & ( for a9 being Object of A9

for a being Object of A st a9 = a holds

G . a9 = F . a ) & ( for b9, c9 being Object of A9

for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds

for f9 being Morphism of b9,c9

for f being Morphism of b,c st f9 = f holds

G . f9 = (Morph-Map (F,b,c)) . f ) ) ) );

for A, B being category

for F being FunctorStr over A,B

for A9, B9 being category holds

( A9,B9 are_anti-isomorphic_under F iff ( A9 is subcategory of A & B9 is subcategory of B & ex G being contravariant Functor of A9,B9 st

( G is bijective & ( for a9 being Object of A9

for a being Object of A st a9 = a holds

G . a9 = F . a ) & ( for b9, c9 being Object of A9

for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds

for f9 being Morphism of b9,c9

for f being Morphism of b,c st f9 = f holds

G . f9 = (Morph-Map (F,b,c)) . f ) ) ) );

theorem :: YELLOW20:37

for A, B, A1, B1 being category

for F being FunctorStr over A,B st A1,B1 are_isomorphic_under F holds

A1,B1 are_isomorphic ;

for F being FunctorStr over A,B st A1,B1 are_isomorphic_under F holds

A1,B1 are_isomorphic ;

theorem :: YELLOW20:38

for A, B, A1, B1 being category

for F being FunctorStr over A,B st A1,B1 are_anti-isomorphic_under F holds

A1,B1 are_anti-isomorphic ;

for F being FunctorStr over A,B st A1,B1 are_anti-isomorphic_under F holds

A1,B1 are_anti-isomorphic ;

theorem :: YELLOW20:39

for A, B being category

for F being covariant Functor of A,B st A,B are_isomorphic_under F holds

F is bijective

for F being covariant Functor of A,B st A,B are_isomorphic_under F holds

F is bijective

proof end;

theorem :: YELLOW20:40

for A, B being category

for F being contravariant Functor of A,B st A,B are_anti-isomorphic_under F holds

F is bijective

for F being contravariant Functor of A,B st A,B are_anti-isomorphic_under F holds

F is bijective

proof end;

theorem :: YELLOW20:41

for A, B being category

for F being covariant Functor of A,B st F is bijective holds

A,B are_isomorphic_under F

for F being covariant Functor of A,B st F is bijective holds

A,B are_isomorphic_under F

proof end;

theorem :: YELLOW20:42

for A, B being category

for F being contravariant Functor of A,B st F is bijective holds

A,B are_anti-isomorphic_under F

for F being contravariant Functor of A,B st F is bijective holds

A,B are_anti-isomorphic_under F

proof end;

theorem Th46: :: YELLOW20:46

for I, J being set

for A being ManySortedSet of [:I,I:]

for B being ManySortedSet of [:J,J:] st A cc= B holds

~ A cc= ~ B

for A being ManySortedSet of [:I,I:]

for B being ManySortedSet of [:J,J:] st A cc= B holds

~ A cc= ~ B

proof end;

theorem Th47: :: YELLOW20:47

for A being non empty transitive AltCatStr

for B being non empty transitive SubCatStr of A holds B opp is SubCatStr of A opp

for B being non empty transitive SubCatStr of A holds B opp is SubCatStr of A opp

proof end;

theorem :: YELLOW20:49

for A being category

for B being non empty subcategory of A holds B,B opp are_anti-isomorphic_under dualizing-func (A,(A opp))

for B being non empty subcategory of A holds B,B opp are_anti-isomorphic_under dualizing-func (A,(A opp))

proof end;

theorem :: YELLOW20:50

for A1, A2 being category

for F being covariant Functor of A1,A2 st F is bijective holds

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds

B2,B1 are_isomorphic_under F "

for F being covariant Functor of A1,A2 st F is bijective holds

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds

B2,B1 are_isomorphic_under F "

proof end;

theorem :: YELLOW20:51

for A1, A2 being category

for F being contravariant Functor of A1,A2 st F is bijective holds

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds

B2,B1 are_anti-isomorphic_under F "

for F being contravariant Functor of A1,A2 st F is bijective holds

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds

B2,B1 are_anti-isomorphic_under F "

proof end;

theorem :: YELLOW20:52

for A1, A2, A3 being category

for F being covariant Functor of A1,A2

for G being covariant Functor of A2,A3

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2

for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G holds

B1,B3 are_isomorphic_under G * F

for F being covariant Functor of A1,A2

for G being covariant Functor of A2,A3

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2

for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G holds

B1,B3 are_isomorphic_under G * F

proof end;

theorem :: YELLOW20:53

for A1, A2, A3 being category

for F being contravariant Functor of A1,A2

for G being covariant Functor of A2,A3

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2

for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G holds

B1,B3 are_anti-isomorphic_under G * F

for F being contravariant Functor of A1,A2

for G being covariant Functor of A2,A3

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2

for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G holds

B1,B3 are_anti-isomorphic_under G * F

proof end;

theorem :: YELLOW20:54

for A1, A2, A3 being category

for F being covariant Functor of A1,A2

for G being contravariant Functor of A2,A3

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2

for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds

B1,B3 are_anti-isomorphic_under G * F

for F being covariant Functor of A1,A2

for G being contravariant Functor of A2,A3

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2

for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds

B1,B3 are_anti-isomorphic_under G * F

proof end;

theorem :: YELLOW20:55

for A1, A2, A3 being category

for F being contravariant Functor of A1,A2

for G being contravariant Functor of A2,A3

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2

for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds

B1,B3 are_isomorphic_under G * F

for F being contravariant Functor of A1,A2

for G being contravariant Functor of A2,A3

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2

for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds

B1,B3 are_isomorphic_under G * F

proof end;

theorem :: YELLOW20:56

for A1, A2 being category

for F being covariant Functor of A1,A2

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st F is bijective & ( for a being Object of A1 holds

( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds

for a1, b1 being Object of B1 st a1 = a & b1 = b holds

for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds

for f being Morphism of a,b holds

( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) holds

B1,B2 are_isomorphic_under F

for F being covariant Functor of A1,A2

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st F is bijective & ( for a being Object of A1 holds

( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds

for a1, b1 being Object of B1 st a1 = a & b1 = b holds

for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds

for f being Morphism of a,b holds

( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) holds

B1,B2 are_isomorphic_under F

proof end;

theorem :: YELLOW20:57

for A1, A2 being category

for F being contravariant Functor of A1,A2

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st F is bijective & ( for a being Object of A1 holds

( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds

for a1, b1 being Object of B1 st a1 = a & b1 = b holds

for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds

for f being Morphism of a,b holds

( f in <^a1,b1^> iff F . f in <^b2,a2^> ) ) holds

B1,B2 are_anti-isomorphic_under F

for F being contravariant Functor of A1,A2

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st F is bijective & ( for a being Object of A1 holds

( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds

for a1, b1 being Object of B1 st a1 = a & b1 = b holds

for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds

for f being Morphism of a,b holds

( f in <^a1,b1^> iff F . f in <^b2,a2^> ) ) holds

B1,B2 are_anti-isomorphic_under F

proof end;