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