:: Functors for Alternative Categories :: by Andrzej Trybulec :: :: Received April 24, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, FUNCT_1, SUBSET_1, MCART_1, ZFMISC_1, TARSKI, PBOOLE, RELAT_1, FUNCT_2, FUNCOP_1, MEMBER_1, STRUCT_0, ALTCAT_1, RELAT_2, MSUALG_6, CAT_1, ALTCAT_2, FUNCT_3, MSUALG_3, ENS_1, WELLORD1, FUNCTOR0; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, MCART_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FUNCT_3, FUNCT_4, STRUCT_0, MSUALG_3, ALTCAT_1, ALTCAT_2; constructors FUNCT_3, MSUALG_3, ALTCAT_2, RELSET_1, XTUPLE_0; registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE, STRUCT_0, ALTCAT_1, ALTCAT_2, RELSET_1, FUNCT_3, XTUPLE_0, FUNCT_4; requirements SUBSET, BOOLE; begin :: Preliminaries scheme :: FUNCTOR0:sch 1 ValOnPair {X()-> non empty set,f()-> Function, x1,x2()-> Element of X(), F(object,object)-> set, P[object,object]}: f().(x1(),x2()) = F(x1(),x2()) provided f() = { [[o,o9],F(o,o9)] where o is Element of X(), o9 is Element of X(): P[o,o9] } and P[x1(),x2()]; theorem :: FUNCTOR0:1 for A being set holds {} is Function of A,{}; theorem :: FUNCTOR0:2 for I being set for M being ManySortedSet of I holds M*id I = M; registration let f be empty Function; cluster ~f -> empty; let g be Function; cluster [:f,g:] -> empty; cluster [:g,f:] -> empty; end; theorem :: FUNCTOR0:3 for A being set, f being Function holds f.:id A = (~f).:id A; theorem :: FUNCTOR0:4 for X,Y being set, f being Function of X,Y holds f is onto iff [:f,f:] is onto; registration let f be Function-yielding Function; cluster ~f -> Function-yielding; end; theorem :: FUNCTOR0:5 for A,B being set, a being object holds ~([:A,B:] --> a) = [:B,A:] --> a; theorem :: FUNCTOR0:6 for f,g being Function st f is one-to-one & g is one-to-one holds [:f,g:]" = [:f",g":]; theorem :: FUNCTOR0:7 for f being Function st [:f,f:] is one-to-one holds f is one-to-one; theorem :: FUNCTOR0:8 for f being Function st f is one-to-one holds ~f is one-to-one; theorem :: FUNCTOR0:9 for f,g being Function st ~[:f,g:] is one-to-one holds [:g,f:] is one-to-one; theorem :: FUNCTOR0:10 for f,g being Function st f is one-to-one & g is one-to-one holds ~[:f,g:]" = ~([:g,f:]"); theorem :: FUNCTOR0:11 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:12 for F,G being Function-yielding Function, f be Function holds (G**F)*f = (G*f)**(F*f); theorem :: FUNCTOR0:13 for A,B,C being set, f being Function of [:A,B:],C st ~f is onto holds f is onto; theorem :: FUNCTOR0:14 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:]; end; definition let A,B be set, f be bifunction of A,B; attr f is Covariant means :: FUNCTOR0:def 1 ex g being Function of A,B st f = [:g,g:]; attr f is Contravariant means :: FUNCTOR0:def 2 ex g being Function of A,B st f = ~[:g,g:]; end; theorem :: FUNCTOR0:15 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; registration let A,B be set; cluster Covariant Contravariant for bifunction of A,B; end; theorem :: FUNCTOR0:16 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 3 ex I29 being non empty set, B9 being ManySortedSet of I29, f9 being Function of I1,I29 st f = f9 & B = B9 & it is ManySortedFunction of A,B9*f9 if I2 <> {} otherwise it = EmptyMS 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 4 it is ManySortedFunction of A,B*f; end; registration 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 for MSUnTrans of f,A,B; end; theorem :: FUNCTOR0:17 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:18 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 the set of all [o9,A.o9 --> m] where o9 is Element of I1 is MSUnTrans of f,A,B; theorem :: FUNCTOR0:19 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 5 ((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 6 the ObjectMap of F is one-to-one; attr F is onto means :: FUNCTOR0:def 7 the ObjectMap of F is onto; attr F is reflexive means :: FUNCTOR0:def 8 (the ObjectMap of F).:id the carrier of A c= id the carrier of B; attr F is coreflexive means :: FUNCTOR0:def 9 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 10 for o being Object of A holds (the ObjectMap of F).(o,o) = [F.o,F.o]; end; theorem :: FUNCTOR0:20 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 o9 being Object of A st F.o9 = o; definition let C1, C2 be non empty AltGraph; let F be BimapStr over C1,C2; attr F is feasible means :: FUNCTOR0:def 11 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 12 the ObjectMap of IT is Covariant; attr IT is Contravariant means :: FUNCTOR0:def 13 the ObjectMap of IT is Contravariant; end; registration let C1,C2 be AltGraph; cluster Covariant for FunctorStr over C1,C2; cluster Contravariant for 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) -> set equals :: FUNCTOR0:def 14 (the MorphMap of F).(o1,o2); end; registration 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^> <> {} and <^F.o1,F.o2^> <> {}; let m be Morphism of o1,o2; func F.m -> Morphism of F.o1, F.o2 equals :: FUNCTOR0:def 15 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^> <> {} and <^F.o2,F.o1^> <> {}; let m be Morphism of o1,o2; func F.m -> Morphism of F.o2, F.o1 equals :: FUNCTOR0:def 16 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 17 the ObjectMap of it = [:the carrier of C1,the carrier of C1:] --> [o,o] & the MorphMap of it = the set of all [[o1,o2],<^o1,o2^> --> m] where o1 is Object of C1, o2 is Object of C1; end; theorem :: FUNCTOR0:21 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; registration 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; registration let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph; cluster feasible Covariant Contravariant for FunctorStr over C1,C2; end; theorem :: FUNCTOR0:22 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 18 for o1,o2 being Object of C1 st <^o1,o2^> <> {} holds <^F.o1,F.o2^> <> {}; end; theorem :: FUNCTOR0:23 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 19 for o1,o2 being Object of C1 st <^o1,o2^> <> {} holds <^F.o2,F.o1^> <> {}; end; registration let C1,C2 be AltGraph; let F be FunctorStr over C1,C2; cluster the MorphMap of F -> Function-yielding; end; registration cluster non empty reflexive for 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 20 for o being Object of C1 holds Morph-Map(F,o,o).idm o = idm F.o; end; theorem :: FUNCTOR0:24 for C1,C2 being non empty AltGraph, o2 being Object of C2 st <^o2,o2^> <> {} for m be Morphism of o2,o2, o,o9 being Object of C1, f being Morphism of o,o9 st <^o,o9^> <> {} holds Morph-Map(C1 --> m,o,o9).f = m; registration cluster with_units -> reflexive for non empty AltCatStr; end; registration let C1,C2 be with_units non empty AltCatStr; let o2 be Object of C2; cluster C1 --> idm o2 -> id-preserving; end; registration 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; registration let C1 be non empty AltGraph; let C2 be non empty reflexive AltGraph; cluster feasible reflexive for FunctorStr over C1,C2; end; registration let C1,C2 be with_units non empty AltCatStr; cluster id-preserving feasible reflexive strict for 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 21 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 f9 being Morphism of F.o1,F.o2, g9 being Morphism of F.o2,F.o3 st f9 = Morph-Map(F,o1,o2).f & g9 = Morph-Map(F,o2,o3).g & Morph-Map(F,o1,o3).(g*f) = g9*f9; end; definition let C1,C2 be non empty AltCatStr; let F be FunctorStr over C1,C2; attr F is comp-reversing 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 f9 being Morphism of F.o2,F.o1, g9 being Morphism of F.o3,F.o2 st f9 = Morph-Map(F,o1,o2).f & g9 = Morph-Map(F,o2,o3).g & Morph-Map(F,o1,o3).(g*f) = f9*g9; 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 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 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 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.f)*(F.g); end; theorem :: FUNCTOR0:25 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,o9 being Object of C1, f being Morphism of o,o9 st <^o,o9^> <> {} holds F.f = m; 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, o,o9 being Object of C1, f being Morphism of o,o9 st <^o,o9^> <> {} holds (C1 --> m).f = m; registration 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 25 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 26 F is Covariant comp-preserving; attr F is contravariant means :: FUNCTOR0:def 27 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 28 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 29 the ObjectMap of it = id [:the carrier of A, the carrier of A:] & the MorphMap of it = id the Arrows of A; end; registration let A be AltCatStr, B be SubCatStr of A; cluster incl B -> Covariant; end; theorem :: FUNCTOR0:27 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:28 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^>; registration 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 30 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 31 ex B9 being ManySortedSet of [:the carrier of A, the carrier of A:], f being ManySortedFunction of (the Arrows of A),B9 st B9 = (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 32 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 33 F is one-to-one faithful; attr F is surjective means :: FUNCTOR0:def 34 F is full onto; end; definition let A,B be AltGraph, F be FunctorStr over A,B; attr F is bijective means :: FUNCTOR0:def 35 F is injective surjective; end; registration let A,B be transitive with_units non empty AltCatStr; cluster strict covariant contravariant feasible for Functor of A,B; end; theorem :: FUNCTOR0:29 for A being non empty AltGraph, o being Object of A holds (id A).o = o; theorem :: FUNCTOR0:30 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; registration let A be non empty AltGraph; cluster id A -> feasible Covariant; end; registration let A be non empty AltGraph; cluster Covariant feasible for FunctorStr over A,A; end; theorem :: FUNCTOR0:31 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; registration 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; registration 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 36 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; registration 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; registration 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; registration 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; registration 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; registration 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:32 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:33 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:34 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); registration 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 37 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 38 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:35 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:36 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:37 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:38 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:39 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:40 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:41 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:42 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:43 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; registration let C1 be 1-sorted, C2 be non empty 1-sorted; cluster Covariant -> reflexive for BimapStr over C1,C2; end; registration let C1 be 1-sorted, C2 be non empty 1-sorted; cluster Contravariant -> reflexive for BimapStr over C1,C2; end; theorem :: FUNCTOR0:44 for C1,C2 being 1-sorted, M being BimapStr over C1,C2 st M is Covariant onto holds M is coreflexive; theorem :: FUNCTOR0:45 for C1,C2 being 1-sorted, M being BimapStr over C1,C2 st M is Contravariant onto holds M is coreflexive; registration let C1 be transitive with_units non empty AltCatStr, C2 be with_units non empty AltCatStr; cluster covariant -> reflexive for Functor of C1,C2; end; registration let C1 be transitive with_units non empty AltCatStr, C2 be with_units non empty AltCatStr; cluster contravariant -> reflexive for Functor of C1,C2; end; theorem :: FUNCTOR0:46 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: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 contravariant onto holds F is coreflexive; theorem :: FUNCTOR0:48 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:49 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 39 ex F being Functor of A,B st F is bijective covariant; reflexivity; symmetry; pred A,B are_anti-isomorphic means :: FUNCTOR0:def 40 ex F being Functor of A,B st F is bijective contravariant; symmetry; end;