Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Natural transformations. Discrete categories

by
Andrzej Trybulec

MML identifier: NATTRA_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, PARTFUN1, FUNCT_4, BOOLE, CAT_1, CAT_2, MCART_1,
FUNCT_2, FINSET_1, CARD_1, NATTRA_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, FINSET_1, PARTFUN1,
RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, CARD_1, CAT_1, CAT_2;
constructors MCART_1, CARD_1, CAT_2, PARTFUN1, MEMBERED, XBOOLE_0;
clusters FUNCT_1, FINSET_1, CAT_1, CAT_2, RELSET_1, SUBSET_1, MEMBERED,
ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

:: Preliminaries

reserve A1,A2,B1,B2 for non empty set,
f for Function of A1,B1,
g for Function of A2,B2,
Y1 for non empty Subset of A1,
Y2 for non empty Subset of A2;

definition let A1 be set, B1 be non empty set,
f be Function of A1, B1,
Y1 be Subset of A1;
redefine func f|Y1 -> Function of Y1,B1;
end;

theorem :: NATTRA_1:1
[:f,g:]|[:Y1,Y2:] = [:f|Y1,g|Y2:];

definition let A,B be non empty set;
let A1 be non empty Subset of A, B1 be non empty Subset of B;
let f be PartFunc of [:A1,A1:],A1; let g be PartFunc of [:B1,B1:],B1;
redefine func |:f,g:| -> PartFunc of [:[:A1,B1:],[:A1,B1:]:],[:A1,B1:];
end;

theorem :: NATTRA_1:2
for f being PartFunc of [:A1,A1:],A1, g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f|([:Y1,Y1:] qua set)
for G being PartFunc of [:Y2,Y2:],Y2 st G = g|([:Y2,Y2:] qua set)
holds |:F,G:| = |:f,g:| |([:[:Y1,Y2:],[:Y1,Y2:]:] qua set);

reserve A,B,C for Category,
F,F1,F2,F3 for Functor of A,B,
G for Functor of B,C;

scheme M_Choice{A()-> non empty set, B()-> non empty set,
F(set) -> set}:
ex t being Function of A(),B() st
for a being Element of A() holds t.a in F(a)
provided
for a being Element of A() holds B() meets F(a);

theorem :: NATTRA_1:3
for a being Object of A, m being Morphism of a,a holds m in Hom(a,a);

reserve m,o for set;

theorem :: NATTRA_1:4
for f,g being Morphism of 1Cat(o,m) holds f = g;

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 Dom of C = (the Dom of A)|the Morphisms of C &
the Cod of C = (the Cod of A)|the Morphisms of C &
the Comp of C = (the Comp of A)|[:the Morphisms of C, the Morphisms of C:] &
the Id of C = (the Id of A)|the Objects of C;

theorem :: NATTRA_1:9
for O being non empty Subset of the Objects of A,
M being non empty Subset of the Morphisms of A
for DOM,COD being Function of M,O st
DOM = (the Dom of A) |M & COD = (the Cod of A)|M
for COMP being PartFunc of [:M,M qua non empty set:], M st
COMP = (the Comp of A)|([:M,M:] qua set)
for ID being Function of O,M st ID = (the Id of A)|O
holds CatStr(#O,M,DOM,COD,COMP,ID#) is Subcategory of A;

theorem :: NATTRA_1:10
for C being strict Category, A being strict Subcategory of C st
the Objects of A = the Objects of C & the Morphisms of A = the Morphisms of C
holds A = C;

begin :: Application of a functor to a morphism

definition let A,B,F; let a,b be Object of A such that
Hom(a,b) <> {};
let f be Morphism of a,b;
func F.f -> Morphism of F.a, F.b equals
:: NATTRA_1:def 1
F.f;
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.MIZ, with
:: the new concept of the application of a functor to a morphism

theorem :: NATTRA_1:12 :: CAT_1:95
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  :: CAT_1:99
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 :: CAT_1:107
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  :: CAT_1:108
for a being Object of A holds F.id a = id (F.a);

theorem :: NATTRA_1:16 :: CAT_1:115
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;

canceled;

theorem :: NATTRA_1:19
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 Objects of A, the Morphisms 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:20
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:21
for a being Object of A holds id F.a = id(F.a);

theorem :: NATTRA_1:22
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:23
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;

canceled;

theorem :: NATTRA_1:25
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:26
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:27
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:28
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;
synonym F1 ~= F2;
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;

canceled;

theorem :: NATTRA_1:30
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:31
F1 ~= F2 implies F2 ~= F1;

theorem :: NATTRA_1:32
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:33
id F is natural_equivalence of F,F;

theorem :: NATTRA_1:34
F1 ~= F2 & F2 ~= F3 implies
for t being natural_equivalence of F1,F2,
t' being natural_equivalence of F2,F3 holds
t'`*`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;

definition let A1,B1,A2,B2 be non empty set,
f1 be Function of A1,B1,
f2 be Function of A2,B2;
redefine pred f1 = f2 means
:: NATTRA_1:def 17
A1 = A2 & for a being Element of A1 holds f1.a = f2.a;
end;

theorem :: NATTRA_1:35
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 18
the Objects of it = Funct(A,B) &
the Morphisms 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

canceled 3;

theorem :: NATTRA_1:39
for f being Morphism of Functors(A,B) st f = [[F,F1],t] holds
dom f = F & cod f = F1;

theorem :: NATTRA_1:40
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:41
for t' being natural_transformation of F2,F3
for f,g being Morphism of Functors(A,B) st
f = [[F,F1],t] & g = [[F2,F3],t'] holds
[g,f] in dom the Comp of Functors(A,B) iff F1 = F2;

theorem :: NATTRA_1:42
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 discrete means
:: NATTRA_1:def 19
for f being Morphism of C ex a being Object of C st f = id a;
end;

definition
cluster discrete Category;
end;

canceled;

theorem :: NATTRA_1:44
for A being discrete Category, a being Object of A holds Hom(a,a) = { id a};

theorem :: NATTRA_1:45
A is discrete iff
(for a being Object of A
ex B being finite set st B = Hom(a,a) & card B = 1) &
for a,b being Object of A st a <> b holds Hom(a,b) = {};

theorem :: NATTRA_1:46
1Cat(o,m) is discrete;

theorem :: NATTRA_1:47
for A being discrete Category, C being Subcategory of A holds C is discrete;

theorem :: NATTRA_1:48
A is discrete & B is discrete implies [:A,B:] is discrete;

theorem :: NATTRA_1:49
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:50
for A being discrete Category, B being Category, F being Functor of B,A,
t being transformation of F,F holds t = id F;

theorem :: NATTRA_1:51
A is discrete implies Functors(B,A) is discrete;

definition let C be Category;
cluster strict discrete Subcategory of C;
end;

definition let C;
func IdCat(C) -> strict discrete Subcategory of C means
:: NATTRA_1:def 20
the Objects of it = the Objects of C &
the Morphisms of it = { id a where a is Object of C: not contradiction};
end;

theorem :: NATTRA_1:52
for C being strict Category holds C is discrete implies IdCat(C) = C;

theorem :: NATTRA_1:53
IdCat(IdCat(C)) = IdCat(C);

theorem :: NATTRA_1:54
IdCat(1Cat(o,m)) = 1Cat(o,m);

theorem :: NATTRA_1:55
IdCat([:A,B:]) = [:IdCat(A), IdCat(B):];
```