:: Category of Functors between Alternative Categories
:: by Robert Nieszczerzewski
::
:: Received June 12, 1997
:: Copyright (c) 1997-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 RELAT_2, ALTCAT_1, XBOOLE_0, MSUALG_6, FUNCTOR0, CAT_1, FUNCT_1,
PZFMISC1, NATTRA_1, PBOOLE, STRUCT_0, SUBSET_1, REALSET1, RELAT_1,
FUNCT_2, CARD_3, CAT_2, ZFMISC_1, TARSKI, FUNCTOR2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCTOR0, XTUPLE_0, MCART_1,
DOMAIN_1, RELAT_1, STRUCT_0, CARD_3, FUNCT_1, PBOOLE, FUNCT_2, BINOP_1,
MULTOP_1, ALTCAT_1;
constructors DOMAIN_1, CARD_3, FUNCTOR0, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, ALTCAT_1, FUNCTOR0,
PBOOLE, FUNCT_1, RELAT_1;
requirements SUBSET, BOOLE;
begin
registration
let A be transitive with_units non empty AltCatStr, B be with_units non
empty AltCatStr;
cluster -> feasible id-preserving for Functor of A, B;
end;
registration
let A be transitive with_units non empty AltCatStr, B be with_units non
empty AltCatStr;
cluster covariant -> Covariant comp-preserving for Functor of A, B;
cluster Covariant comp-preserving -> covariant for Functor of A, B;
cluster contravariant -> Contravariant comp-reversing for Functor of A, B;
cluster Contravariant comp-reversing -> contravariant for Functor of A, B;
end;
theorem :: FUNCTOR2:1
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 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;
theorem :: FUNCTOR2:2
for A,B being transitive with_units non empty AltCatStr, F,F1,
F2 being 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 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 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 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 Functor of A,B;
assume
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
:: FUNCTOR2:def 5
for a being Object of A holds it!a = (t2!a) * (t1!a);
end;
theorem :: FUNCTOR2:3
for A,B being transitive with_units non empty AltCatStr, F1,F2
being 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:4
for A,B being transitive with_units non empty AltCatStr, F
being Functor of A,B holds for a being Object of A holds (idt F)!a =
idm(F.a);
theorem :: FUNCTOR2:5
for A,B being transitive with_units non empty AltCatStr, F1,F2
being 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:6
for A,B being category, F,F1,F2,F3 being 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
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);
reflexivity;
end;
theorem :: FUNCTOR2:7
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:8
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 & 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:9
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:10
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:11
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 object 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;