FUNCTOR2: Category of Functors between Alternative Categories

:: Category of Functors between Alternative Categories
:: by Robert Nieszczerzewski
::
:: Received June 12, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users

registration

let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;

cluster -> feasible id-preserving for Functor of A,B;

coherence by FUNCTOR0:def 25;

end;

registration

let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;

cluster covariant -> Covariant comp-preserving for Functor of A,B;

coherence by FUNCTOR0:def 26;

cluster Covariant comp-preserving -> covariant for Functor of A,B;

coherence by FUNCTOR0:def 26;

cluster contravariant -> Contravariant comp-reversing for Functor of A,B;

coherence by FUNCTOR0:def 27;

cluster Contravariant comp-reversing -> contravariant for Functor of A,B;

coherence by FUNCTOR0:def 27;

end;

theorem Th1: :: FUNCTOR2:1

for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B
for a being Object of A holds F . (idm a) = idm (F . a)

proof end;

definition

let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be Functor of A,B;

pred F1 is_transformable_to F2 means :: FUNCTOR2:def 1
for a being Object of A holds <^(F1 . a),(F2 . a)^> <> {} ;

reflexivity by ALTCAT_2:def 7;

end;

:: deftheorem defines is_transformable_to FUNCTOR2:def 1 :

theorem Th2: :: FUNCTOR2:2

for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
F is_transformable_to F2

proof end;

definition

let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;

mode transformation of F1,F2 -> ManySortedSet of the carrier of A means :Def2: :: FUNCTOR2:def 2
for a being Object of A holds it . a is Morphism of (F1 . a),(F2 . a);

existence

proof end;

end;

:: deftheorem Def2 defines transformation FUNCTOR2:def 2 :

definition

let A, B be non empty transitive with_units AltCatStr ;
let F be Functor of A,B;

func idt F -> transformation of F,F means :Def3: :: FUNCTOR2:def 3
for a being Object of A holds it . a = idm (F . a);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines idt FUNCTOR2:def 3 :

definition

let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;
let t be transformation of F1,F2;
let a be Object of A;

func t ! a -> Morphism of (F1 . a),(F2 . a) means :Def4: :: FUNCTOR2:def 4
it = t . a;

existence

proof end;

correctness ;

end;

:: deftheorem Def4 defines ! FUNCTOR2:def 4 :

definition

let A, B be non empty transitive with_units AltCatStr ;
let F, F1, F2 be Functor of A,B;
assume A1: ( F is_transformable_to F1 & F1 is_transformable_to F2 ) ;
let t1 be transformation of F,F1;
let t2 be transformation of F1,F2;

func t2 `*` t1 -> transformation of F,F2 means :Def5: :: FUNCTOR2:def 5
for a being Object of A holds it ! a = (t2 ! a) * (t1 ! a);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines `*` FUNCTOR2:def 5 :

theorem Th3: :: FUNCTOR2:3

for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 ! a = t2 ! a ) holds
t1 = t2

proof end;

theorem Th4: :: FUNCTOR2:4

for A, B being non empty transitive with_units AltCatStr
for F being Functor of A,B
for a being Object of A holds (idt F) ! a = idm (F . a)

proof end;

theorem Th5: :: FUNCTOR2:5

for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t )

proof end;

theorem Th6: :: FUNCTOR2:6

for A, B being category
for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)

proof end;

Lm1: for A, B being non empty transitive with_units AltCatStr
for F, G being covariant Functor of A,B
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)

proof end;

definition

let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be covariant Functor of A,B;

pred F1 is_naturally_transformable_to F2 means :: FUNCTOR2:def 6
( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F2 . f) * (t ! a) );

reflexivity

proof end;

end;

:: deftheorem defines is_naturally_transformable_to FUNCTOR2:def 6 :

theorem :: FUNCTOR2:7

for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B holds F is_naturally_transformable_to F ;

Lm2: for A, B being category
for F, F1, F2 being covariant Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
for t1 being transformation of F,F1 st ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)

proof end;

theorem Th8: :: FUNCTOR2:8

for A, B being category
for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
F is_naturally_transformable_to F2

proof end;

definition

let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be covariant Functor of A,B;
assume A1: F1 is_naturally_transformable_to F2 ;

mode natural_transformation of F1,F2 -> transformation of F1,F2 means :Def7: :: FUNCTOR2:def 7
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (it ! b) * (F1 . f) = (F2 . f) * (it ! a);

existence by A1;

end;

:: deftheorem Def7 defines natural_transformation FUNCTOR2:def 7 :

definition

let A, B be non empty transitive with_units AltCatStr ;
let F be covariant Functor of A,B;
:: original: idt
redefine func idt F -> natural_transformation of F,F;
coherence

proof end;

end;

definition

let A, B be category;
let F, F1, F2 be covariant Functor of A,B;
assume A1: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 ) ;
let t1 be natural_transformation of F,F1;
let t2 be natural_transformation of F1,F2;

func t2 `*` t1 -> natural_transformation of F,F2 means :Def8: :: FUNCTOR2:def 8
it = t2 `*` t1;

existence

proof end;

correctness ;

end;

:: deftheorem Def8 defines `*` FUNCTOR2:def 8 :

theorem :: FUNCTOR2:9

for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t ) by Th5;

theorem :: FUNCTOR2:10

for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being Object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) by Def5;

theorem :: FUNCTOR2:11

for A, B being category
for F, F1, F2, F3 being covariant Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

proof end;

definition

let I be set ;
let A, B be ManySortedSet of I;

func Funcs (A,B) -> set means :Def9: :: FUNCTOR2:def 9
for x being set holds
( x in it iff x is ManySortedFunction of A,B ) if for i being set st i in I & B . i = {} holds
A . i = {}
otherwise it = {} ;