:: Natural Transformations. Discrete Categories
:: by Andrzej Trybulec
::
:: Received May 15, 1991
:: Copyright (c) 1991-2016 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, RELAT_1, ZFMISC_1, PARTFUN1,
FUNCT_4, REALSET1, TARSKI, CAT_1, GRAPH_1, STRUCT_0, CAT_2, MCART_1,
PZFMISC1, ALGSTR_0, FUNCT_2, NATTRA_1, MONOID_0, RELAT_2, BINOP_1,
ALTCAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, REALSET1,
PARTFUN1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_4, STRUCT_0,
GRAPH_1, CAT_1, CAT_2, CAT_3;
constructors PARTFUN1, REALSET1, CAT_2, FUNCOP_1, RELSET_1, CAT_3, XTUPLE_0,
FUNCT_4;
registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, CAT_1, CAT_2, STRUCT_0,
ZFMISC_1, RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
begin
:: Preliminaries
reserve A,B,C for Category,
F,F1,F2,F3 for Functor of A,B,
G for Functor of B, C;
reserve m,o for set;
::$CT 4
theorem :: NATTRA_1:5
for a being Object of A holds [[id a,id a],id a] in the Comp of A;
theorem :: NATTRA_1:6
the Comp of 1Cat(o,m) = {[[m,m],m]};
theorem :: NATTRA_1:7
for a being Object of A holds 1Cat(a,id a) is Subcategory of A;
theorem :: NATTRA_1:8
for C being Subcategory of A holds the Source of C = (the Source
of A)|the carrier' of C & the Target of C = (the Target of A)|the carrier' of C
& the Comp of C = (the Comp of A)||the carrier' of C;
theorem :: NATTRA_1:9
for O being non empty Subset of the carrier of A,
M being non empty Subset of the carrier' of A st
for o being Element of A st o in O holds id o in M
for DOM,COD being Function of M,O st DOM = (the Source of A) |M &
COD = (the Target of A)|M
for COMP being PartFunc of [:M,M qua non empty set:], M
st COMP = (the Comp of A)||M
holds CatStr(#O,M,DOM,COD,COMP#) is Subcategory of A;
theorem :: NATTRA_1:10
for C being strict Category, A being strict Subcategory of C st
the carrier of A = the carrier of C & the carrier' of A = the carrier' of C
holds A = C;
begin :: Application of a functor to a morphism
definition
::$CD
end;
theorem :: NATTRA_1:11
for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,
b holds (G*F)/.f = G/.(F/.f);
:: The following theorems are analogues of theorems from CAT_1, with
:: the new concept of the application of a functor to a morphism
theorem :: NATTRA_1:12
for F1,F2 being Functor of A,B
st for a,b being Object of A st Hom(a,b) <> {}
for f being Morphism of a,b holds F1.f = F2.f
holds F1 = F2;
theorem :: NATTRA_1:13
for a,b,c being Object of A st Hom(a,b) <> {} & Hom(b,c) <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds F/.(g*f) = (F/.g)*(F/.f);
theorem :: NATTRA_1:14
for c being Object of A, d being Object of B st F/.(id c) = id d
holds F.c = d;
theorem :: NATTRA_1:15
for a being Object of A holds F/.id a = id (F.a);
theorem :: NATTRA_1:16
for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,
b holds (id A)/.f = f;
theorem :: NATTRA_1:17
for a,b,c,d being Object of A st Hom(a,b) meets Hom(c,d) holds a = c & b = d;
begin :: Transformations
definition
let A,B,F1,F2;
pred F1 is_transformable_to F2 means
:: NATTRA_1:def 2
for a being Object of A holds Hom(F1.a,F2.a) <> {};
reflexivity;
end;
theorem :: NATTRA_1:18
F is_transformable_to F1 & F1 is_transformable_to F2 implies F
is_transformable_to F2;
definition
let A,B,F1,F2;
assume
F1 is_transformable_to F2;
mode transformation of F1,F2 -> Function of the carrier of A, the carrier'
of B means
:: NATTRA_1:def 3
for a being Object of A holds it.a is Morphism of F1.a,F2.a;
end;
definition
let A,B;
let F be Functor of A,B;
func id F ->transformation of F,F means
:: NATTRA_1:def 4
for a being Object of A holds it.a = id (F.a);
end;
definition
let A,B,F1,F2;
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 equals
:: NATTRA_1:def 5
t.a;
end;
definition
let A,B,F,F1,F2;
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
:: NATTRA_1:def 6
for a being Object of A holds it.a = (t2.a)*(t1.a);
end;
theorem :: NATTRA_1:19
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 :: NATTRA_1:20
for a being Object of A holds id F.a = id(F.a);
theorem :: NATTRA_1:21
F1 is_transformable_to F2 implies for t being transformation of
F1,F2 holds (id F2)`*`t = t & t`*`(id F1) = t;
theorem :: NATTRA_1:22
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,F1,F2;
pred F1 is_naturally_transformable_to F2 means
:: NATTRA_1:def 7
F1 is_transformable_to
F2 & ex t being transformation of F1,F2 st for a,b being Object of A st Hom(a,b
) <> {} for f being Morphism of a,b holds t.b*F1/.f = F2/.f*t.a;
reflexivity;
end;
theorem :: NATTRA_1:23
F is_naturally_transformable_to F1 & F1
is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2;
definition
let A,B,F1,F2;
assume
F1 is_naturally_transformable_to F2;
mode natural_transformation of F1,F2 -> transformation of F1,F2 means
:: NATTRA_1:def 8
for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,b holds
it.b*F1/.f = F2/.f*it.a;
end;
definition
let A,B,F;
redefine func id F -> natural_transformation of F,F;
end;
definition
let A,B,F,F1,F2 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 equals
:: NATTRA_1:def 9
t2`*`t1;
end;
theorem :: NATTRA_1:24
F1 is_naturally_transformable_to F2 implies for t being
natural_transformation of F1,F2 holds (id F2)`*`t = t & t`*`(id F1) = t;
reserve t for natural_transformation of F,F1,
t1 for natural_transformation of F1,F2;
theorem :: NATTRA_1:25
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 :: NATTRA_1:26
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);
:: Natural equivalences
definition
let A,B,F1,F2;
let IT be transformation of F1,F2;
attr IT is invertible means
:: NATTRA_1:def 10
for a being Object of A holds IT.a is invertible;
end;
definition
let A,B,F1,F2;
pred F1,F2 are_naturally_equivalent means
:: NATTRA_1:def 11
F1
is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2
st t is invertible;
reflexivity;
end;
notation
let A,B,F1,F2;
synonym F1 ~= F2 for F1,F2 are_naturally_equivalent;
end;
definition
let A,B,F1,F2 such that
F1 is_transformable_to F2;
let t1 be transformation of F1,F2 such that
t1 is invertible;
func t1" -> transformation of F2,F1 means
:: NATTRA_1:def 12
for a being Object of A holds it.a = (t1.a)";
end;
definition
let A,B,F1,F2,t1 such that
F1 is_naturally_transformable_to F2 and
t1 is invertible;
func t1" -> natural_transformation of F2,F1 equals
:: NATTRA_1:def 13
(t1 qua
transformation of F1,F2)";
end;
theorem :: NATTRA_1:27
for A,B,F1,F2,t1 st F1 is_naturally_transformable_to F2 & t1 is
invertible for a being Object of A holds t1".a = (t1.a)";
theorem :: NATTRA_1:28
F1 ~= F2 implies F2 ~= F1;
theorem :: NATTRA_1:29
F1 ~= F2 & F2 ~= F3 implies F1 ~= F3;
definition
let A,B,F1,F2;
assume
F1,F2 are_naturally_equivalent;
mode natural_equivalence of F1,F2 -> natural_transformation of F1,F2 means
:: NATTRA_1:def 14
it is invertible;
end;
theorem :: NATTRA_1:30
id F is natural_equivalence of F,F;
theorem :: NATTRA_1:31
F1 ~= F2 & F2 ~= F3 implies for t being natural_equivalence of F1,F2,
t9 being natural_equivalence of F2,F3 holds t9`*`t is natural_equivalence of F1
,F3;
begin :: Functor category
definition
let A,B;
mode NatTrans-DOMAIN of A,B -> non empty set means
:: NATTRA_1:def 15
for x being set
holds x in it implies ex F1,F2 being Functor of A,B, t being
natural_transformation of F1,F2 st x = [[F1,F2],t] & F1
is_naturally_transformable_to F2;
end;
definition
let A,B;
func NatTrans(A,B) -> NatTrans-DOMAIN of A,B means
:: NATTRA_1:def 16
for x being set
holds x in it iff ex F1,F2 being Functor of A,B, t being natural_transformation
of F1,F2 st x = [[F1,F2],t] & F1 is_naturally_transformable_to F2;
end;
theorem :: NATTRA_1:32
F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B);
definition
let A,B;
func Functors(A,B) -> strict Category means
:: NATTRA_1:def 17
the carrier of it =
Funct(A,B) & the carrier' of it = NatTrans(A,B) & (for f being Morphism of it
holds dom f = f`1`1 & cod f = f`1`2) & (for f,g being Morphism of it st dom g =
cod f holds [g,f] in dom the Comp of it) & (for f,g being Morphism of it st [g,
f] in dom (the Comp of it) ex F,F1,F2,t,t1 st f = [[F,F1],t] & g = [[F1,F2],t1]
& (the Comp of it).[g,f] = [[F,F2],t1`*`t])
& for a being Object of it, F st F
= a holds id a = [[F,F],id F];
end;
:: As immediate consequences of the definition we get
theorem :: NATTRA_1:33
for f being Morphism of Functors(A,B) st f = [[F,F1],t] holds
dom f = F & cod f = F1;
theorem :: NATTRA_1:34
for a,b being Object of Functors(A,B), f being Morphism of a,b st Hom(
a,b) <> {} ex F,F1,t st a = F & b = F1 & f = [[F,F1],t];
theorem :: NATTRA_1:35
for t9 being natural_transformation of F2,F3 for f,g being
Morphism of Functors(A,B) st f = [[F,F1],t] & g = [[F2,F3],t9] holds [g,f] in
dom the Comp of Functors(A,B) iff F1 = F2;
theorem :: NATTRA_1:36
for f,g being Morphism of Functors(A,B) st f = [[F,F1],t] & g = [[F1,
F2],t1] holds g(*)f = [[F,F2],t1`*`t];
begin :: Discrete categories
definition
let C be Category;
attr C is quasi-discrete means
:: NATTRA_1:def 18
for a,b being Element of C st Hom(a,b)<>{} holds a=b;
attr C is pseudo-discrete means
:: NATTRA_1:def 19
for a being Element of C holds Hom(a,a) is trivial;
end;
reserve a,b for Element of C;
definition
let C be Category;
attr C is discrete means
:: NATTRA_1:def 20
C is quasi-discrete pseudo-discrete;
end;
registration
cluster discrete -> quasi-discrete pseudo-discrete for Category;
cluster quasi-discrete pseudo-discrete -> discrete for Category;
end;
registration let o,m be set;
cluster 1Cat(o,m) -> discrete;
end;
registration
cluster discrete for Category;
end;
registration let C be discrete Category;
let a be Element of C;
cluster Hom(a,a) -> trivial;
end;
theorem :: NATTRA_1:37
for A being discrete Category, a being Object of A holds Hom(a,a ) = { id a};
registration let A be discrete Category;
cluster -> discrete for Subcategory of A;
end;
registration let A,B be discrete Category;
cluster [:A,B:] -> discrete;
end;
::$CT 3
theorem :: NATTRA_1:41
for A being discrete Category, B being Category, F1,F2 being
Functor of B,A st F1 is_transformable_to F2 holds F1 = F2;
theorem :: NATTRA_1:42
for A being discrete Category, B being Category, F being Functor
of B,A, t being transformation of F,F holds t = id F;
registration let B be Category, A be discrete Category;
cluster Functors(B,A) -> discrete;
end;
registration
let C be Category;
cluster strict discrete for Subcategory of C;
end;
definition
let C;
func IdCat(C) -> strict Subcategory of C means
:: NATTRA_1:def 21
the carrier of it = the carrier of C &
the carrier' of it = the set of all id a where a is Object of C;
end;
registration
let C;
cluster IdCat C -> discrete;
end;
registration
cluster strict discrete for Category;
end;
registration let C be strict discrete Category;
reduce IdCat C to C;
end;
::$CT 4
theorem :: NATTRA_1:47
IdCat([:A,B:]) = [:IdCat(A), IdCat(B):];