Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Category of Functors between Alternative Categories

**by****Robert Nieszczerzewski**- Received June 12, 1997
- MML identifier: FUNCTOR2

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_2, ALTCAT_1, MSUALG_6, FUNCTOR0, CAT_1, FUNCT_1, BOOLE, NATTRA_1, PBOOLE, QC_LANG1, FUNCT_2, PRALG_1, CARD_3, RELAT_1, CAT_2, TARSKI, FUNCTOR2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCTOR0, MCART_1, DOMAIN_1, RELAT_1, STRUCT_0, CARD_3, FUNCT_1, FUNCT_2, BINOP_1, MULTOP_1, FRAENKEL, PBOOLE, MSUALG_1, ALTCAT_1; constructors FUNCTOR0, DOMAIN_1; clusters STRUCT_0, ALTCAT_1, FUNCTOR0, RELSET_1, SUBSET_1, XBOOLE_0; requirements SUBSET, BOOLE; begin definition let A be transitive with_units (non empty AltCatStr), B be with_units (non empty AltCatStr); cluster -> feasible id-preserving Functor of A, B; end; definition let A be transitive with_units (non empty AltCatStr), B be with_units (non empty AltCatStr); cluster covariant -> Covariant comp-preserving Functor of A, B; cluster Covariant comp-preserving -> covariant Functor of A, B; cluster contravariant -> Contravariant comp-reversing Functor of A, B; cluster Contravariant comp-reversing -> contravariant Functor of A, B; end; canceled; theorem :: FUNCTOR2:2 for A,B being transitive with_units (non empty AltCatStr), F being covariant Functor of A,B for a being object of A holds F.idm a = idm (F.a); begin :: Transformations definition let A,B be transitive with_units (non empty AltCatStr), F1,F2 be covariant 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; end; canceled; theorem :: FUNCTOR2:4 for A,B being transitive with_units (non empty AltCatStr), F,F1,F2 being covariant Functor of A,B holds F is_transformable_to F1 & F1 is_transformable_to F2 implies F is_transformable_to F2; definition let A,B be transitive with_units (non empty AltCatStr), F1,F2 be covariant Functor of A,B; assume F1 is_transformable_to F2; mode transformation of F1,F2 -> ManySortedSet of the carrier of A means :: FUNCTOR2:def 2 for a being object of A holds it.a is Morphism of F1.a,F2.a; end; definition let A,B be transitive with_units (non empty AltCatStr); let F be covariant Functor of A,B; func idt F -> transformation of F,F means :: FUNCTOR2:def 3 for a being object of A holds it.a = idm (F.a); end; definition let A,B be transitive with_units (non empty AltCatStr), F1,F2 be covariant Functor of A,B; assume 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 :: FUNCTOR2:def 4 it = t.a; end; definition let A,B be transitive with_units (non empty AltCatStr), F,F1,F2 be covariant Functor of A,B; assume that F is_transformable_to F1 and 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 :: FUNCTOR2:def 5 for a being object of A holds it!a = (t2!a) * (t1!a); end; theorem :: FUNCTOR2:5 for A,B being transitive with_units (non empty AltCatStr), F1,F2 being covariant Functor of A,B holds F1 is_transformable_to F2 implies for t1,t2 being transformation of F1,F2 st for a being object of A holds t1!a = t2!a holds t1 = t2; theorem :: FUNCTOR2:6 for A,B being transitive with_units (non empty AltCatStr), F being covariant Functor of A,B holds for a being object of A holds (idt F)!a = idm(F.a); theorem :: FUNCTOR2:7 for A,B being transitive with_units (non empty AltCatStr), F1,F2 being covariant Functor of A,B holds F1 is_transformable_to F2 implies for t being transformation of F1,F2 holds (idt F2)`*`t = t & t`*`(idt F1) = t; theorem :: FUNCTOR2:8 for A,B being category, F,F1,F2,F3 being covariant Functor of A,B holds F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 implies for t1 being transformation of F,F1, t2 being transformation of F1,F2, t3 being transformation of F2,F3 holds t3`*`t2`*`t1 = t3`*`(t2`*`t1); begin :: Natural transformations definition let A,B be transitive with_units (non empty AltCatStr), 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^> <> {} for f being Morphism of a,b holds t!b*F1.f = F2.f*(t!a); end; theorem :: FUNCTOR2:9 for A,B be transitive with_units (non empty AltCatStr), F be covariant Functor of A,B holds F is_naturally_transformable_to F; theorem :: FUNCTOR2:10 for A,B be category, F,F1,F2 be covariant Functor of A,B holds F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2; definition let A,B be transitive with_units (non empty AltCatStr), F1,F2 be covariant Functor of A,B; assume F1 is_naturally_transformable_to F2; mode natural_transformation of F1,F2 -> transformation of F1,F2 means :: FUNCTOR2:def 7 for a,b being object of A st <^a,b^> <> {} for f being Morphism of a,b holds it!b*F1.f = F2.f*(it!a); end; definition let A,B be transitive with_units (non empty AltCatStr), F be covariant Functor of A,B; redefine func idt F -> natural_transformation of F,F; end; definition let A,B be category, F,F1,F2 be covariant Functor of A,B such that F is_naturally_transformable_to F1 and 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 :: FUNCTOR2:def 8 it = t2`*`t1; end; theorem :: FUNCTOR2:11 for A,B be transitive with_units (non empty AltCatStr), F1,F2 be covariant Functor of A,B holds F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds (idt F2)`*`t = t & t`*`(idt F1) = t; theorem :: FUNCTOR2:12 for A,B be transitive with_units (non empty AltCatStr), F,F1,F2 be covariant Functor of A,B holds F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies 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); theorem :: FUNCTOR2:13 for A,B be category, F,F1,F2,F3 be covariant Functor of A,B for t be natural_transformation of F,F1, t1 be natural_transformation of F1,F2 holds F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 being natural_transformation of F2,F3 holds t3`*`t1`*`t = t3`*`(t1`*`t) ; begin :: Category of Functors definition let I be set; let A,B be ManySortedSet of I; func Funcs(A,B) -> set means :: FUNCTOR2:def 9 for x be set holds x in it iff x is ManySortedFunction of A,B if for i being set st i in I holds B.i = {} implies A.i = {} otherwise it = {}; end; definition let A,B be transitive with_units (non empty AltCatStr); func Funct(A,B) -> set means :: FUNCTOR2:def 10 for x being set holds x in it iff x is covariant strict Functor of A,B; end; definition let A,B be category; func Functors(A,B) -> strict non empty transitive AltCatStr means :: FUNCTOR2:def 11 the carrier of it = Funct(A,B) & (for F,G being strict covariant Functor of A,B, x being set holds x in (the Arrows of it).(F,G) iff F is_naturally_transformable_to G & x is natural_transformation of F,G) & for F,G,H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H for t1 being natural_transformation of F,G, t2 being natural_transformation of G,H ex f being Function st f = (the Comp of it).(F,G,H) & f.(t2,t1) = t2`*`t1; end;

Back to top