YELLOW20: Miscellaneous Facts about Functors

:: Miscellaneous Facts about Functors
:: by Grzegorz Bancerek
::
:: Received July 31, 2001
:: Copyright (c) 2001-2011 Association of Mizar Users

begin

theorem Th1: :: YELLOW20:1

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of 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 of A,B
for G being feasible Covariant FunctorStr of 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 of A,B
for G being feasible Contravariant FunctorStr of 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;

begin

definition

let A, B be AltCatStr ;
pred A,B have_the_same_composition means :Def1: :: YELLOW20:def 1
for a1, a2, a3 being set holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3];
symmetry ;

end;

:: deftheorem Def1 defines have_the_same_composition YELLOW20:def 1 :

theorem Th10: :: YELLOW20:10

for A, B being AltCatStr holds
( A,B have_the_same_composition iff for a1, a2, a3, x being set 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 set st x in (dom f) /\ (dom g) holds
it . x = (f . x) /\ (g . x) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def2 defines Intersect YELLOW20:def 2 :

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 :: YELLOW20:16

canceled;

theorem Th17: :: YELLOW20:17

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 Th18: :: YELLOW20:18

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 Th19: :: YELLOW20:19

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

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines Intersect YELLOW20:def 3 :

theorem :: YELLOW20:20

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

proof end;

theorem Th21: :: YELLOW20:21

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

proof end;

theorem Th22: :: YELLOW20:22

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 Th23: :: YELLOW20:23

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

proof end;

theorem Th24: :: YELLOW20:24

proof end;

theorem :: YELLOW20:25

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

theorem :: YELLOW20:26

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;

begin

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 Th27: :: YELLOW20:27

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;

begin

registration

let f be Function-yielding Function;
let x, y be set ;
cluster f . (x,y) -> Relation-like Function-like ;
coherence ;

end;

theorem Th28: :: YELLOW20:28

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

proof end;

end;

registration

let A be category;
let C be non empty subcategory of A;
cluster incl C -> Covariant ;
coherence ;

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 by FUNCTOR0:def 26;

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

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

proof end;

end;

theorem Th29: :: YELLOW20:29

for A, B being category
for C being non empty subcategory of A
for F being FunctorStr of 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 Th30: :: YELLOW20:30

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 Th31: :: YELLOW20:31

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 Th32: :: YELLOW20:32

for A, B being non empty AltGraph
for F being BimapStr of 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 Th33: :: YELLOW20:33

for A, B being non empty reflexive AltGraph
for F being feasible Covariant FunctorStr of 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 Th34: :: YELLOW20:34

for A, B being non empty AltGraph
for F being Covariant FunctorStr of 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 Th35: :: YELLOW20:35

for A, B being non empty AltGraph
for F being BimapStr of 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 Th36: :: YELLOW20:36

for A, B being non empty reflexive AltGraph
for F being feasible Contravariant FunctorStr of 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 Th37: :: YELLOW20:37

for A, B being non empty AltGraph
for F being Contravariant FunctorStr of 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;

begin

definition

let A, B be category;
let F be FunctorStr of 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 :

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

theorem :: YELLOW20:38

for A, B, A1, B1 being category
for F being FunctorStr of A,B st A1,B1 are_isomorphic_under F holds
A1,B1 are_isomorphic

proof end;

theorem :: YELLOW20:39

for A, B, A1, B1 being category
for F being FunctorStr of A,B st A1,B1 are_anti-isomorphic_under F holds
A1,B1 are_anti-isomorphic

proof end;

theorem :: YELLOW20:40

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

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

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

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

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

proof end;

theorem Th45: :: YELLOW20:45

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

proof end;

theorem :: YELLOW20:46

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

proof end;

theorem Th47: :: YELLOW20:47

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 Th48: :: YELLOW20:48

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

for A being category
for B being non empty subcategory of A holds B opp is subcategory of A opp

proof end;

theorem :: YELLOW20:50

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

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

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

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

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

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

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

for A1, A2 being non empty 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:58

for A1, A2 being non empty 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;