Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Functors for Alternative Categories

**by****Andrzej Trybulec**- Received April 24, 1996
- MML identifier: FUNCTOR0

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, MCART_1, BOOLE, RELAT_1, PBOOLE, SGRAPH1, PRALG_1, FUNCOP_1, MSUALG_3, CAT_4, ALTCAT_1, RELAT_2, MSUALG_6, CAT_1, ALTCAT_2, FUNCT_3, ENS_1, WELLORD1, FUNCTOR0; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, MCART_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FUNCT_3, FUNCT_4, PBOOLE, STRUCT_0, PRALG_1, MSUALG_1, MSUALG_3, ALTCAT_1, ALTCAT_2; constructors ALTCAT_2, MCART_1; clusters RELAT_1, FUNCT_1, ALTCAT_1, ALTCAT_2, MSUALG_1, STRUCT_0, PRALG_1, RELSET_1, SUBSET_1, FUNCT_2; requirements SUBSET, BOOLE; begin :: Preliminaries scheme ValOnPair {X()-> non empty set,f()-> Function, x1,x2()-> Element of X(), F(set,set)-> set, P[set,set]}: f().(x1(),x2()) = F(x1(),x2()) provided f() = { [[o,o'],F(o,o')] where o is Element of X(), o' is Element of X(): P[o,o'] } and P[x1(),x2()]; theorem :: FUNCTOR0:1 for A being set holds {} is Function of A,{}; canceled; theorem :: FUNCTOR0:3 for I being set for M being ManySortedSet of I holds M*id I = M; definition let f be empty Function; cluster ~f -> empty; let g be Function; cluster [:f,g:] -> empty; cluster [:g,f:] -> empty; end; theorem :: FUNCTOR0:4 for A being set, f being Function holds f.:id A = (~f).:id A; theorem :: FUNCTOR0:5 for X,Y being set, f being Function of X,Y holds f is onto iff [:f,f:] is onto; definition let f be Function-yielding Function; cluster ~f -> Function-yielding; end; theorem :: FUNCTOR0:6 for A,B being set, a being set holds ~([:A,B:] --> a) = [:B,A:] --> a; theorem :: FUNCTOR0:7 for f,g being Function st f is one-to-one & g is one-to-one holds [:f,g:]" = [:f",g":]; theorem :: FUNCTOR0:8 for f being Function st [:f,f:] is one-to-one holds f is one-to-one; theorem :: FUNCTOR0:9 for f being Function st f is one-to-one holds ~f is one-to-one; theorem :: FUNCTOR0:10 for f,g being Function st ~[:f,g:] is one-to-one holds [:g,f:] is one-to-one; theorem :: FUNCTOR0:11 for f,g being Function st f is one-to-one & g is one-to-one holds ~[:f,g:]" = ~([:g,f:]"); theorem :: FUNCTOR0:12 for A,B be set, f being Function of A,B st f is onto holds id B c= [:f,f:].:id A; theorem :: FUNCTOR0:13 for F,G being Function-yielding Function, f be Function holds (G**F)*f = (G*f)**(F*f); definition let A,B,C be set, f be Function of [:A,B:],C; redefine func ~f -> Function of [:B,A:],C; end; theorem :: FUNCTOR0:14 for A,B,C being set, f being Function of [:A,B:],C st ~f is onto holds f is onto; theorem :: FUNCTOR0:15 for A be set, B being non empty set, f being Function of A,B holds [:f,f:].:id A c= id B; begin :: Functions bewteen Cartesian products definition let A,B be set; mode bifunction of A,B is Function of [:A,A:],[:B,B:]; canceled; end; definition let A,B be set, f be bifunction of A,B; attr f is Covariant means :: FUNCTOR0:def 2 ex g being Function of A,B st f = [:g,g:]; attr f is Contravariant means :: FUNCTOR0:def 3 ex g being Function of A,B st f = ~[:g,g:]; end; theorem :: FUNCTOR0:16 for A be set, B be non empty set, b being Element of B, f being bifunction of A,B st f = [:A,A:] --> [b,b] holds f is Covariant Contravariant; definition let A,B be set; cluster Covariant Contravariant bifunction of A,B; end; theorem :: FUNCTOR0:17 for A,B being non empty set for f being Covariant Contravariant bifunction of A,B ex b being Element of B st f = [:A,A:] --> [b,b]; begin :: Unary transformatiom definition let I1,I2 be set, f be Function of I1,I2; let A be ManySortedSet of I1, B be ManySortedSet of I2; mode MSUnTrans of f,A,B -> ManySortedSet of I1 means :: FUNCTOR0:def 4 ex I2' being non empty set, B' being ManySortedSet of I2', f' being Function of I1,I2' st f = f' & B = B' & it is ManySortedFunction of A,B'*f' if I2 <> {} otherwise it = [0]I1; end; definition let I1 be set, I2 be non empty set, f be Function of I1,I2; let A be ManySortedSet of I1, B be ManySortedSet of I2; redefine mode MSUnTrans of f,A,B means :: FUNCTOR0:def 5 it is ManySortedFunction of A,B*f; end; definition let I1,I2 be set; let f be Function of I1,I2; let A be ManySortedSet of I1, B be ManySortedSet of I2; cluster -> Function-yielding MSUnTrans of f,A,B; end; theorem :: FUNCTOR0:18 for I1 being set, I2,I3 being non empty set, f being Function of I1,I2, g being Function of I2,I3, B being ManySortedSet of I2, C being ManySortedSet of I3, G being MSUnTrans of g,B,C holds G*f is MSUnTrans of g*f,B*f,C; definition let I1 be set, I2 be non empty set, f be Function of I1,I2, A be ManySortedSet of [:I1,I1:], B be ManySortedSet of [:I2,I2:], F be MSUnTrans of [:f,f:],A,B; redefine func ~F -> MSUnTrans of [:f,f:],~A,~B; end; theorem :: FUNCTOR0:19 for I1,I2 being non empty set, A being ManySortedSet of I1, B being ManySortedSet of I2, o being Element of I2 st B.o <> {} for m being Element of B.o, f being Function of I1,I2 st f = I1 --> o holds { [o',A.o' --> m] where o' is Element of I1: not contradiction } is MSUnTrans of f,A,B; theorem :: FUNCTOR0:20 for I1 being set, I2,I3 being non empty set, f being Function of I1,I2, g being Function of I2,I3, A being ManySortedSet of I1, B being ManySortedSet of I2, C being ManySortedSet of I3, F being MSUnTrans of f,A,B, G being MSUnTrans of g*f,B*f,C st for ii being set st ii in I1 & (B*f).ii = {} holds A.ii = {} or (C*(g*f)).ii = {} holds G**(F qua Function-yielding Function) is MSUnTrans of g*f,A,C; begin :: Functors definition let C1,C2 be 1-sorted; struct BimapStr over C1,C2 (#ObjectMap -> bifunction of the carrier of C1, the carrier of C2 #); end; definition let C1,C2 be non empty AltGraph; let F be BimapStr over C1,C2; let o be object of C1; func F.o -> object of C2 equals :: FUNCTOR0:def 6 ((the ObjectMap of F).(o,o))`1; end; definition let A,B be 1-sorted, F be BimapStr over A,B; attr F is one-to-one means :: FUNCTOR0:def 7 the ObjectMap of F is one-to-one; attr F is onto means :: FUNCTOR0:def 8 the ObjectMap of F is onto; attr F is reflexive means :: FUNCTOR0:def 9 (the ObjectMap of F).:id the carrier of A c= id the carrier of B; attr F is coreflexive means :: FUNCTOR0:def 10 id the carrier of B c= (the ObjectMap of F).:id the carrier of A; end; definition let A,B be non empty AltGraph, F be BimapStr over A,B; redefine attr F is reflexive means :: FUNCTOR0:def 11 for o being object of A holds (the ObjectMap of F).(o,o) = [F.o,F.o]; end; theorem :: FUNCTOR0:21 for A,B being reflexive non empty AltGraph, F being BimapStr over A,B st F is coreflexive for o being object of B ex o' being object of A st F.o' = o; definition let C1, C2 be non empty AltGraph; let F be BimapStr over C1,C2; attr F is feasible means :: FUNCTOR0:def 12 for o1,o2 being object of C1 st <^o1,o2^> <> {} holds (the Arrows of C2).((the ObjectMap of F).(o1,o2)) <> {}; end; definition let C1,C2 be AltGraph; struct(BimapStr over C1,C2) FunctorStr over C1,C2 (#ObjectMap -> bifunction of the carrier of C1,the carrier of C2, MorphMap -> MSUnTrans of the ObjectMap, the Arrows of C1, the Arrows of C2 #); end; definition let C1,C2 be 1-sorted; let IT be BimapStr over C1,C2; attr IT is Covariant means :: FUNCTOR0:def 13 the ObjectMap of IT is Covariant; attr IT is Contravariant means :: FUNCTOR0:def 14 the ObjectMap of IT is Contravariant; end; definition let C1,C2 be AltGraph; cluster Covariant FunctorStr over C1,C2; cluster Contravariant FunctorStr over C1,C2; end; definition let C1,C2 be AltGraph; let F be FunctorStr over C1,C2; let o1,o2 be object of C1; func Morph-Map(F,o1,o2) equals :: FUNCTOR0:def 15 (the MorphMap of F).(o1,o2); end; definition let C1,C2 be AltGraph; let F be FunctorStr over C1,C2; let o1,o2 be object of C1; cluster Morph-Map(F,o1,o2) -> Relation-like Function-like; end; definition let C1,C2 be non empty AltGraph; let F be Covariant FunctorStr over C1,C2; let o1,o2 be object of C1; redefine func Morph-Map(F,o1,o2) -> Function of <^o1,o2^>, <^F.o1,F.o2^>; end; definition let C1,C2 be non empty AltGraph; let F be Covariant FunctorStr over C1,C2; let o1,o2 be object of C1 such that <^o1,o2^> <> {} & <^F.o1,F.o2^> <> {}; let m be Morphism of o1,o2; func F.m -> Morphism of F.o1, F.o2 equals :: FUNCTOR0:def 16 Morph-Map(F,o1,o2).m; end; definition let C1,C2 be non empty AltGraph; let F be Contravariant FunctorStr over C1,C2; let o1,o2 be object of C1; redefine func Morph-Map(F,o1,o2) -> Function of <^o1,o2^>, <^F.o2,F.o1^>; end; definition let C1,C2 be non empty AltGraph; let F be Contravariant FunctorStr over C1,C2; let o1,o2 be object of C1 such that <^o1,o2^> <> {} & <^F.o2,F.o1^> <> {}; let m be Morphism of o1,o2; func F.m -> Morphism of F.o2, F.o1 equals :: FUNCTOR0:def 17 Morph-Map(F,o1,o2).m; end; definition let C1,C2 be non empty AltGraph; let o be object of C2 such that <^o,o^> <> {}; let m be Morphism of o,o; func C1 --> m -> strict FunctorStr over C1,C2 means :: FUNCTOR0:def 18 the ObjectMap of it = [:the carrier of C1,the carrier of C1:] --> [o,o] & the MorphMap of it = { [[o1,o2],<^o1,o2^> --> m] where o1 is object of C1, o2 is object of C1: not contradiction }; end; theorem :: FUNCTOR0:22 for C1,C2 being non empty AltGraph, o2 being object of C2 st <^o2,o2^> <> {} for m be Morphism of o2,o2, o1 being object of C1 holds (C1 --> m).o1 = o2; definition let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph; let o be object of C2, m be Morphism of o,o; cluster C1 --> m -> Covariant Contravariant feasible; end; definition let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph; cluster feasible Covariant Contravariant FunctorStr over C1,C2; end; theorem :: FUNCTOR0:23 for C1, C2 being non empty AltGraph, F being Covariant FunctorStr over C1,C2, o1,o2 being object of C1 holds (the ObjectMap of F).(o1,o2) = [F.o1,F.o2]; definition let C1, C2 be non empty AltGraph; let F be Covariant FunctorStr over C1,C2; redefine attr F is feasible means :: FUNCTOR0:def 19 for o1,o2 being object of C1 st <^o1,o2^> <> {} holds <^F.o1,F.o2^> <> {}; end; theorem :: FUNCTOR0:24 for C1, C2 being non empty AltGraph, F being Contravariant FunctorStr over C1,C2, o1,o2 being object of C1 holds (the ObjectMap of F).(o1,o2) = [F.o2,F.o1]; definition let C1, C2 be non empty AltGraph; let F be Contravariant FunctorStr over C1,C2; redefine attr F is feasible means :: FUNCTOR0:def 20 for o1,o2 being object of C1 st <^o1,o2^> <> {} holds <^F.o2,F.o1^> <> {}; end; definition let C1,C2 be AltGraph; let F be FunctorStr over C1,C2; cluster the MorphMap of F -> Function-yielding; end; definition cluster non empty reflexive AltCatStr; end; :: Wlasnosci funktorow, Semadeni-Wiweger str. 32 definition let C1,C2 be with_units (non empty AltCatStr); let F be FunctorStr over C1,C2; attr F is id-preserving means :: FUNCTOR0:def 21 for o being object of C1 holds Morph-Map(F,o,o).idm o = idm F.o; end; theorem :: FUNCTOR0:25 for C1,C2 being non empty AltGraph, o2 being object of C2 st <^o2,o2^> <> {} for m be Morphism of o2,o2, o,o' being object of C1, f being Morphism of o,o' st <^o,o'^> <> {} holds Morph-Map(C1 --> m,o,o').f = m; definition cluster with_units -> reflexive (non empty AltCatStr); end; definition let C1,C2 be with_units (non empty AltCatStr); let o2 be object of C2; cluster C1 --> idm o2 -> id-preserving; end; definition let C1 be non empty AltGraph; let C2 be non empty reflexive AltGraph; let o2 be object of C2; let m be Morphism of o2,o2; cluster C1 --> m -> reflexive; end; definition let C1 be non empty AltGraph; let C2 be non empty reflexive AltGraph; cluster feasible reflexive FunctorStr over C1,C2; end; definition let C1,C2 be with_units (non empty AltCatStr); cluster id-preserving feasible reflexive strict FunctorStr over C1,C2; end; definition let C1,C2 be non empty AltCatStr; let F be FunctorStr over C1,C2; attr F is comp-preserving means :: FUNCTOR0:def 22 for o1,o2,o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} for f being Morphism of o1,o2, g being Morphism of o2,o3 ex f' being Morphism of F.o1,F.o2, g' being Morphism of F.o2,F.o3 st f' = Morph-Map(F,o1,o2).f & g' = Morph-Map(F,o2,o3).g & Morph-Map(F,o1,o3).(g*f) = g'*f'; end; definition let C1,C2 be non empty AltCatStr; let F be FunctorStr over C1,C2; attr F is comp-reversing means :: FUNCTOR0:def 23 for o1,o2,o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} for f being Morphism of o1,o2, g being Morphism of o2,o3 ex f' being Morphism of F.o2,F.o1, g' being Morphism of F.o3,F.o2 st f' = Morph-Map(F,o1,o2).f & g' = Morph-Map(F,o2,o3).g & Morph-Map(F,o1,o3).(g*f) = f'*g'; end; definition let C1 be non empty transitive AltCatStr; let C2 be non empty reflexive AltCatStr; let F be Covariant feasible FunctorStr over C1,C2; redefine attr F is comp-preserving means :: FUNCTOR0:def 24 for o1,o2,o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} for f being Morphism of o1,o2, g being Morphism of o2,o3 holds F.(g*f) = (F.g)*(F.f); end; definition let C1 be non empty transitive AltCatStr; let C2 be non empty reflexive AltCatStr; let F be Contravariant feasible FunctorStr over C1,C2; redefine attr F is comp-reversing means :: FUNCTOR0:def 25 for o1,o2,o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} for f being Morphism of o1,o2, g being Morphism of o2,o3 holds F.(g*f) = (F.f)*(F.g); end; theorem :: FUNCTOR0:26 for C1 being non empty AltGraph, C2 being non empty reflexive AltGraph, o2 being object of C2, m be Morphism of o2,o2, F being Covariant feasible FunctorStr over C1,C2 st F = C1 --> m for o,o' being object of C1, f being Morphism of o,o' st <^o,o'^> <> {} holds F.f = m; theorem :: FUNCTOR0:27 for C1 being non empty AltGraph, C2 being non empty reflexive AltGraph, o2 being object of C2, m be Morphism of o2,o2, o,o' being object of C1, f being Morphism of o,o' st <^o,o'^> <> {} holds (C1 --> m).f = m; definition let C1 be non empty transitive AltCatStr, C2 be with_units (non empty AltCatStr); let o be object of C2; cluster C1 --> idm o -> comp-preserving comp-reversing; end; definition let C1 be transitive with_units (non empty AltCatStr), C2 be with_units (non empty AltCatStr); mode Functor of C1,C2 -> FunctorStr over C1,C2 means :: FUNCTOR0:def 26 it is feasible id-preserving & (it is Covariant comp-preserving or it is Contravariant comp-reversing); end; definition let C1 be transitive with_units (non empty AltCatStr), C2 be with_units (non empty AltCatStr), F be Functor of C1,C2; attr F is covariant means :: FUNCTOR0:def 27 F is Covariant comp-preserving; attr F is contravariant means :: FUNCTOR0:def 28 F is Contravariant comp-reversing; end; definition let A be AltCatStr, B be SubCatStr of A; func incl B -> strict FunctorStr over B,A means :: FUNCTOR0:def 29 the ObjectMap of it = id [:the carrier of B, the carrier of B:] & the MorphMap of it = id the Arrows of B; end; definition let A be AltGraph; func id A -> strict FunctorStr over A,A means :: FUNCTOR0:def 30 the ObjectMap of it = id [:the carrier of A, the carrier of A:] & the MorphMap of it = id the Arrows of A; end; definition let A be AltCatStr, B be SubCatStr of A; cluster incl B -> Covariant; end; theorem :: FUNCTOR0:28 for A being non empty AltCatStr, B being non empty SubCatStr of A, o being object of B holds (incl B).o = o; theorem :: FUNCTOR0:29 for A being non empty AltCatStr, B being non empty SubCatStr of A, o1,o2 being object of B holds <^o1,o2^> c= <^(incl B).o1,(incl B).o2^>; definition let A be non empty AltCatStr, B be non empty SubCatStr of A; cluster incl B -> feasible; end; definition let A,B be AltGraph, F be FunctorStr over A,B; attr F is faithful means :: FUNCTOR0:def 31 the MorphMap of F is "1-1"; end; definition let A,B be AltGraph, F be FunctorStr over A,B; attr F is full means :: FUNCTOR0:def 32 ex B' being ManySortedSet of [:the carrier of A, the carrier of A:], f being ManySortedFunction of (the Arrows of A),B' st B' = (the Arrows of B)*the ObjectMap of F & f = the MorphMap of F & f is "onto"; end; definition let A be AltGraph, B be non empty AltGraph, F be FunctorStr over A,B; redefine attr F is full means :: FUNCTOR0:def 33 ex f being ManySortedFunction of (the Arrows of A), (the Arrows of B)*the ObjectMap of F st f = the MorphMap of F & f is "onto"; end; definition let A,B be AltGraph, F be FunctorStr over A,B; attr F is injective means :: FUNCTOR0:def 34 F is one-to-one faithful; attr F is surjective means :: FUNCTOR0:def 35 F is full onto; end; definition let A,B be AltGraph, F be FunctorStr over A,B; attr F is bijective means :: FUNCTOR0:def 36 F is injective surjective; end; definition let A,B be transitive with_units (non empty AltCatStr); cluster strict covariant contravariant feasible Functor of A,B; end; theorem :: FUNCTOR0:30 for A being non empty AltGraph, o being object of A holds (id A).o = o; theorem :: FUNCTOR0:31 for A being non empty AltGraph, o1,o2 being object of A st <^o1,o2^> <> {} for m being Morphism of o1,o2 holds Morph-Map(id A,o1,o2).m = m; definition let A be non empty AltGraph; cluster id A -> feasible Covariant; end; definition let A be non empty AltGraph; cluster Covariant feasible FunctorStr over A,A; end; theorem :: FUNCTOR0:32 for A being non empty AltGraph, o1,o2 being object of A st <^o1,o2^> <> {} for F being Covariant feasible FunctorStr over A,A st F = id A for m being Morphism of o1,o2 holds F.m = m; definition let A be transitive with_units (non empty AltCatStr); cluster id A -> id-preserving comp-preserving; end; definition let A be transitive with_units (non empty AltCatStr); redefine func id A -> strict covariant Functor of A,A; end; definition let A be AltGraph; cluster id A -> bijective; end; begin :: The composition of functors definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph; let F be feasible FunctorStr over C1,C2, G be FunctorStr over C2,C3; func G*F -> strict FunctorStr over C1,C3 means :: FUNCTOR0:def 37 the ObjectMap of it = (the ObjectMap of G)*the ObjectMap of F & the MorphMap of it = ((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F; end; definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph; let F be Covariant feasible FunctorStr over C1,C2, G be Covariant FunctorStr over C2,C3; cluster G*F -> Covariant; end; definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph; let F be Contravariant feasible FunctorStr over C1,C2, G be Covariant FunctorStr over C2,C3; cluster G*F -> Contravariant; end; definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph; let F be Covariant feasible FunctorStr over C1,C2, G be Contravariant FunctorStr over C2,C3; cluster G*F -> Contravariant; end; definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph; let F be Contravariant feasible FunctorStr over C1,C2, G be Contravariant FunctorStr over C2,C3; cluster G*F -> Covariant; end; definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph; let F be feasible FunctorStr over C1,C2, G be feasible FunctorStr over C2,C3; cluster G*F -> feasible; end; theorem :: FUNCTOR0:33 for C1 being non empty AltGraph, C2,C3,C4 being non empty reflexive AltGraph, F being feasible FunctorStr over C1,C2, G being feasible FunctorStr over C2,C3, H being FunctorStr over C3,C4 holds H*G*F = H*(G*F); theorem :: FUNCTOR0:34 for C1 being non empty AltCatStr, C2,C3 being non empty reflexive AltCatStr, F be feasible reflexive FunctorStr over C1,C2, G be FunctorStr over C2,C3, o be object of C1 holds (G*F).o = G.(F.o); theorem :: FUNCTOR0:35 for C1 being non empty AltGraph, C2,C3 being non empty reflexive AltGraph, F be feasible reflexive FunctorStr over C1,C2, G be FunctorStr over C2,C3, o be object of C1 holds Morph-Map(G*F,o,o) = Morph-Map(G,F.o,F.o)*Morph-Map(F,o,o); definition let C1,C2,C3 be with_units (non empty AltCatStr); let F be id-preserving feasible reflexive FunctorStr over C1,C2; let G be id-preserving FunctorStr over C2,C3; cluster G*F -> id-preserving; end; definition let A,C be non empty reflexive AltCatStr; let B be non empty SubCatStr of A; let F be FunctorStr over A,C; func F|B -> FunctorStr over B,C equals :: FUNCTOR0:def 38 F*incl B; end; begin :: The inverse functor definition let A,B be non empty AltGraph, F be FunctorStr over A,B; assume F is bijective; func F" -> strict FunctorStr over B,A means :: FUNCTOR0:def 39 the ObjectMap of it = (the ObjectMap of F)" & ex f being ManySortedFunction of (the Arrows of A), (the Arrows of B)*the ObjectMap of F st f = the MorphMap of F & the MorphMap of it = f""*(the ObjectMap of F)"; end; theorem :: FUNCTOR0:36 for A,B being transitive with_units (non empty AltCatStr), F being feasible FunctorStr over A,B st F is bijective holds F" is bijective feasible; theorem :: FUNCTOR0:37 for A,B being transitive with_units (non empty AltCatStr), F being feasible reflexive FunctorStr over A,B st F is bijective coreflexive holds F" is reflexive; theorem :: FUNCTOR0:38 for A,B being transitive with_units (non empty AltCatStr), F being feasible reflexive id-preserving FunctorStr over A,B st F is bijective coreflexive holds F" is id-preserving; theorem :: FUNCTOR0:39 for A,B being transitive with_units (non empty AltCatStr), F being feasible FunctorStr over A,B st F is bijective Covariant holds F" is Covariant; theorem :: FUNCTOR0:40 for A,B being transitive with_units (non empty AltCatStr), F being feasible FunctorStr over A,B st F is bijective Contravariant holds F" is Contravariant; theorem :: FUNCTOR0:41 for A,B being transitive with_units (non empty AltCatStr), F being feasible reflexive FunctorStr over A,B st F is bijective coreflexive Covariant for o1,o2 being object of B, m being Morphism of o1,o2 st <^o1,o2^> <> {} holds Morph-Map(F,F".o1,F".o2).(Morph-Map(F",o1,o2).m) = m; theorem :: FUNCTOR0:42 for A,B being transitive with_units (non empty AltCatStr), F being feasible reflexive FunctorStr over A,B st F is bijective coreflexive Contravariant for o1,o2 being object of B, m being Morphism of o1,o2 st <^o1,o2^> <> {} holds Morph-Map(F,F".o2,F".o1).(Morph-Map(F",o1,o2).m) = m; theorem :: FUNCTOR0:43 for A,B being transitive with_units (non empty AltCatStr), F being feasible reflexive FunctorStr over A,B st F is bijective comp-preserving Covariant coreflexive holds F" is comp-preserving; theorem :: FUNCTOR0:44 for A,B being transitive with_units (non empty AltCatStr), F being feasible reflexive FunctorStr over A,B st F is bijective comp-reversing Contravariant coreflexive holds F" is comp-reversing; definition let C1 be 1-sorted, C2 be non empty 1-sorted; cluster Covariant -> reflexive BimapStr over C1,C2; end; definition let C1 be 1-sorted, C2 be non empty 1-sorted; cluster Contravariant -> reflexive BimapStr over C1,C2; end; theorem :: FUNCTOR0:45 for C1,C2 being 1-sorted, M being BimapStr over C1,C2 st M is Covariant onto holds M is coreflexive; theorem :: FUNCTOR0:46 for C1,C2 being 1-sorted, M being BimapStr over C1,C2 st M is Contravariant onto holds M is coreflexive; definition let C1 be transitive with_units (non empty AltCatStr), C2 be with_units (non empty AltCatStr); cluster covariant -> reflexive Functor of C1,C2; end; definition let C1 be transitive with_units (non empty AltCatStr), C2 be with_units (non empty AltCatStr); cluster contravariant -> reflexive Functor of C1,C2; end; theorem :: FUNCTOR0:47 for C1 being transitive with_units (non empty AltCatStr), C2 being with_units (non empty AltCatStr), F being Functor of C1,C2 st F is covariant onto holds F is coreflexive; theorem :: FUNCTOR0:48 for C1 being transitive with_units (non empty AltCatStr), C2 being with_units (non empty AltCatStr), F being Functor of C1,C2 st F is contravariant onto holds F is coreflexive; theorem :: FUNCTOR0:49 for A,B being transitive with_units (non empty AltCatStr), F being covariant Functor of A,B st F is bijective ex G being Functor of B,A st G = F" & G is bijective covariant; theorem :: FUNCTOR0:50 for A,B being transitive with_units (non empty AltCatStr), F being contravariant Functor of A,B st F is bijective ex G being Functor of B,A st G = F" & G is bijective contravariant; definition let A,B be transitive with_units (non empty AltCatStr); pred A,B are_isomorphic means :: FUNCTOR0:def 40 ex F being Functor of A,B st F is bijective covariant; reflexivity; symmetry; pred A,B are_anti-isomorphic means :: FUNCTOR0:def 41 ex F being Functor of A,B st F is bijective contravariant; symmetry; end;

Back to top