:: Miscellaneous Facts about Functors
:: by Grzegorz Bancerek
::
:: Received July 31, 2001
:: Copyright (c) 2001-2021 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 )

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 )

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 )

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 "

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 "

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 "

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 "

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 "

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 "

proof end;

definition

let A, B be AltCatStr ;

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

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

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 )

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 )

proof end;

theorem :: YELLOW20:12

for A, B being semi-functional para-functional category holds A,B have_the_same_composition

proof end;

definition

let f, g be Function;

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
ex b₁ being Function st
( dom b₁ = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds
b₁ . x = (f . x) /\ (g . x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds
b₁ . x = (f . x) /\ (g . x) ) & dom b₂ = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds
b₂ . x = (f . x) /\ (g . x) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, f, g being Function st dom b₁ = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds
b₁ . x = (f . x) /\ (g . x) ) holds
( dom b₁ = (dom g) /\ (dom f) & ( for x being object st x in (dom g) /\ (dom f) holds
b₁ . x = (g . x) /\ (f . x) ) ) ;

end;

:: deftheorem Def2 defines Intersect YELLOW20:def 2 :
for f, g, b₃ being Function holds
( b₃ = Intersect (f,g) iff ( dom b₃ = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds
b₃ . x = (f . x) /\ (g . x) ) ) );

theorem :: YELLOW20:13

for I being set
for A, B being ManySortedSet of I holds Intersect (A,B) = A (/\) B

proof end;

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

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

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

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

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

proof end;

definition

let A, B be AltCatStr ;
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
ex b₁ being strict AltCatStr st
( the carrier of b₁ = the carrier of A /\ the carrier of B & the Arrows of b₁ = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b₁ = Intersect ( the Comp of A, the Comp of B) )

proof end;

uniqueness
for b₁, b₂ being strict AltCatStr st the carrier of b₁ = the carrier of A /\ the carrier of B & the Arrows of b₁ = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b₁ = Intersect ( the Comp of A, the Comp of B) & the carrier of b₂ = the carrier of A /\ the carrier of B & the Arrows of b₂ = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b₂ = Intersect ( the Comp of A, the Comp of B) holds
b₁ = b₂ ;

end;

:: deftheorem Def3 defines Intersect YELLOW20:def 3 :
for A, B being AltCatStr st A,B have_the_same_composition holds
for b₃ being strict AltCatStr holds
( b₃ = Intersect (A,B) iff ( the carrier of b₃ = the carrier of A /\ the carrier of B & the Arrows of b₃ = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b₃ = Intersect ( the Comp of A, the Comp of B) ) );

theorem :: YELLOW20:19

for A, B being AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) = Intersect (B,A)

proof end;

theorem Th20: :: YELLOW20:20

for A, B being AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) is SubCatStr of A

proof end;

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

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

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

proof end;

theorem :: YELLOW20:24

for A, B being non empty with_units AltCatStr st A,B have_the_same_composition holds
for a being Object of A
for b being Object of B
for o being Object of (Intersect (A,B)) st o = a & o = b & idm a = idm b holds
idm a in <^o,o^> by Th23;

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

proof end;

scheme :: YELLOW20:sch 1
SubcategoryUniq{ F₁() -> category, F₂() -> non empty subcategory of F₁(), F₃() -> non empty subcategory of F₁(), P₁[ set ], P₂[ set , set , set ] } :

AltCatStr(# the carrier of F₂(), the Arrows of F₂(), the Comp of F₂() #) = AltCatStr(# the carrier of F₃(), the Arrows of F₃(), the Comp of F₃() #)

provided

A1: for a being Object of F₁() holds
( a is Object of F₂() iff P₁[a] ) and
A2: for a, b being Object of F₁()
for a9, b9 being Object of F₂() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P₂[a,b,f] ) and
A3: for a being Object of F₁() holds
( a is Object of F₃() iff P₁[a] ) and
A4: for a, b being Object of F₁()
for a9, b9 being Object of F₃() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P₂[a,b,f] )

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

proof end;

scheme :: YELLOW20:sch 2
FullSubcategoryEx{ F₁() -> category, P₁[ set ] } :

ex B being non empty strict full subcategory of F₁() st
for a being Object of F₁() holds
( a is Object of B iff P₁[a] )

provided

A1: ex a being Object of F₁() st P₁[a]

proof end;

scheme :: YELLOW20:sch 3
FullSubcategoryUniq{ F₁() -> category, F₂() -> non empty full subcategory of F₁(), F₃() -> non empty full subcategory of F₁(), P₁[ set ] } :

AltCatStr(# the carrier of F₂(), the Arrows of F₂(), the Comp of F₂() #) = AltCatStr(# the carrier of F₃(), the Arrows of F₃(), the Comp of F₃() #)

provided

A1: for a being Object of F₁() holds
( a is Object of F₂() iff P₁[a] ) and
A2: for a being Object of F₁() holds
( a is Object of F₃() iff P₁[a] )

proof end;

registration

let f be Function-yielding Function;
let x, y be set ;

cluster f . (x,y) -> Relation-like Function-like ;

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

end;

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

proof end;

registration

let A be category;
let C be non empty subcategory of A;

cluster incl C -> id-preserving comp-preserving ;

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

proof end;

end;

registration

let A be category;
let C be non empty subcategory of A;

cluster incl C -> Covariant ;

coherence
incl C is Covariant ;

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;

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

proof end;

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

proof end;

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

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

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

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

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

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 )

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

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

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 )

proof end;

definition

let A, B be category;
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 ) ) );

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

end;

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

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

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 ;

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 ;

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

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

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

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

proof end;

theorem :: YELLOW20:43

for A being category
for B being non empty subcategory of A holds B,B are_isomorphic_under id A

proof end;

theorem Th44: :: YELLOW20:44

for f, g being Function st f c= g holds
~ f c= ~ g

proof end;

theorem :: YELLOW20:45

for f, g being Function st dom f is Relation & ~ f c= ~ g holds
f c= g

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

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

proof end;

theorem Th48: :: YELLOW20:48

for A being category
for B being non empty subcategory of A holds B opp is subcategory 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))

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 "

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 "

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

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

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

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

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

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

proof end;