:: Natural Transformations. Discrete Categories
:: by Andrzej Trybulec
::
:: Copyright (c) 1991-2021 Association of Mizar Users

theorem :: NATTRA_1:1
canceled;

theorem :: NATTRA_1:2
canceled;

theorem :: NATTRA_1:3
canceled;

theorem :: NATTRA_1:4
canceled;

::$CT 4 theorem Th1: :: NATTRA_1:5 for A being Category for a being Object of A holds [[(id a),(id a)],(id a)] in the Comp of A proof end; theorem Th2: :: NATTRA_1:6 for m, o being set holds the Comp of (1Cat (o,m)) = {[[m,m],m]} proof end; theorem Th3: :: NATTRA_1:7 for A being Category for a being Object of A holds 1Cat (a,(id a)) is Subcategory of A proof end; theorem Th4: :: NATTRA_1:8 for A being Category 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 ) proof end; theorem Th5: :: NATTRA_1:9 for A being Category for O being non empty Subset of the carrier of A for 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 ) holds for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A proof end; theorem Th6: :: NATTRA_1:10 for C being strict Category for 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 proof end; definition end; :: deftheorem NATTRA_1:def 1 : canceled; theorem :: NATTRA_1:11 for A, B, C being Category for F being Functor of A,B for G being Functor of B,C for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f) proof end; :: 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 A, B being Category for F1, F2 being Functor of A,B st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds F1 . f = F2 . f ) holds F1 = F2 proof end; theorem Th9: :: NATTRA_1:13 for A, B being Category for F being Functor of A,B for a, b, c being Object of A st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f) proof end; theorem :: NATTRA_1:14 for A, B being Category for F being Functor of A,B for c being Object of A for d being Object of B st F /. (id c) = id d holds F . c = d proof end; theorem Th11: :: NATTRA_1:15 for A, B being Category for F being Functor of A,B for a being Object of A holds F /. (id a) = id (F . a) proof end; theorem :: NATTRA_1:16 for A being Category for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (id A) /. f = f proof end; theorem :: NATTRA_1:17 for A being Category for a, b, c, d being Object of A st Hom (a,b) meets Hom (c,d) holds ( a = c & b = d ) proof end; definition let A, B be Category; let F1, F2 be Functor of A,B; pred F1 is_transformable_to F2 means :Def1: :: NATTRA_1:def 2 for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} ; reflexivity for F1 being Functor of A,B for a being Object of A holds Hom ((F1 . a),(F1 . a)) <> {} ; end; :: deftheorem Def1 defines is_transformable_to NATTRA_1:def 2 : for A, B being Category for F1, F2 being Functor of A,B holds ( F1 is_transformable_to F2 iff for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} ); theorem Th14: :: NATTRA_1:18 for A, B being Category for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds F is_transformable_to F2 proof end; definition let A, B be Category; let F1, F2 be Functor of A,B; assume A1: F1 is_transformable_to F2 ; mode transformation of F1,F2 -> Function of the carrier of A, the carrier' of B means :Def2: :: NATTRA_1:def 3 for a being Object of A holds it . a is Morphism of F1 . a,F2 . a; existence ex b1 being Function of the carrier of A, the carrier' of B st for a being Object of A holds b1 . a is Morphism of F1 . a,F2 . a proof end; end; :: deftheorem Def2 defines transformation NATTRA_1:def 3 : for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for b5 being Function of the carrier of A, the carrier' of B holds ( b5 is transformation of F1,F2 iff for a being Object of A holds b5 . a is Morphism of F1 . a,F2 . a ); definition let A, B be Category; let F be Functor of A,B; func id F -> transformation of F,F means :Def3: :: NATTRA_1:def 4 for a being Object of A holds it . a = id (F . a); existence ex b1 being transformation of F,F st for a being Object of A holds b1 . a = id (F . a) proof end; uniqueness for b1, b2 being transformation of F,F st ( for a being Object of A holds b1 . a = id (F . a) ) & ( for a being Object of A holds b2 . a = id (F . a) ) holds b1 = b2 proof end; end; :: deftheorem Def3 defines id NATTRA_1:def 4 : for A, B being Category for F being Functor of A,B for b4 being transformation of F,F holds ( b4 = id F iff for a being Object of A holds b4 . a = id (F . a) ); definition let A, B be Category; let F1, F2 be Functor of A,B; assume A1: 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 :Def4: :: NATTRA_1:def 5 t . a; coherence t . a is Morphism of F1 . a,F2 . a by ; end; :: deftheorem Def4 defines . NATTRA_1:def 5 : for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 for a being Object of A holds t . a = t . a; definition let A, B be Category; let F, F1, F2 be Functor of A,B; assume that A1: F is_transformable_to F1 and A2: 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 :Def5: :: NATTRA_1:def 6 for a being Object of A holds it . a = (t2 . a) * (t1 . a); existence ex b1 being transformation of F,F2 st for a being Object of A holds b1 . a = (t2 . a) * (t1 . a) proof end; uniqueness for b1, b2 being transformation of F,F2 st ( for a being Object of A holds b1 . a = (t2 . a) * (t1 . a) ) & ( for a being Object of A holds b2 . a = (t2 . a) * (t1 . a) ) holds b1 = b2 proof end; end; :: deftheorem Def5 defines * NATTRA_1:def 6 : for A, B being Category for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for b8 being transformation of F,F2 holds ( b8 = t2 * t1 iff for a being Object of A holds b8 . a = (t2 . a) * (t1 . a) ); theorem Th15: :: NATTRA_1:19 for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds t1 = t2 proof end; theorem Th16: :: NATTRA_1:20 for A, B being Category for F being Functor of A,B for a being Object of A holds (id F) . a = id (F . a) proof end; theorem Th17: :: NATTRA_1:21 for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 holds ( (id F2) * t = t & t * (id F1) = t ) proof end; theorem Th18: :: NATTRA_1:22 for A, B being Category for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 * t2) * t1 = t3 * (t2 * t1) proof end; Lm1: for A, B being Category for F being Functor of A,B for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) proof end; definition let A, B be Category; let F1, F2 be Functor of A,B; 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) <> {} holds for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ); reflexivity for F1 being Functor of A,B holds ( F1 is_transformable_to F1 & ex t being transformation of F1,F1 st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F1 /. f) * (t . a) ) proof end; end; :: deftheorem defines is_naturally_transformable_to NATTRA_1:def 7 : for A, B being Category for F1, F2 being Functor of A,B holds ( F1 is_naturally_transformable_to F2 iff ( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ) ); Lm2: for A, B being Category for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 * t1) . b) * (F /. f) = (F2 /. f) * ((t2 * t1) . a) proof end; theorem Th19: :: NATTRA_1:23 for A, B being Category for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds F is_naturally_transformable_to F2 proof end; definition let A, B be Category; let F1, F2 be Functor of A,B; assume A1: F1 is_naturally_transformable_to F2 ; mode natural_transformation of F1,F2 -> transformation of F1,F2 means :Def7: :: NATTRA_1:def 8 for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (it . b) * (F1 /. f) = (F2 /. f) * (it . a); existence ex b1 being transformation of F1,F2 st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (b1 . b) * (F1 /. f) = (F2 /. f) * (b1 . a) by A1; end; :: deftheorem Def7 defines natural_transformation NATTRA_1:def 8 : for A, B being Category for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for b5 being transformation of F1,F2 holds ( b5 is natural_transformation of F1,F2 iff for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (b5 . b) * (F1 /. f) = (F2 /. f) * (b5 . a) ); definition let A, B be Category; let F be Functor of A,B; :: original: id redefine func id F -> natural_transformation of F,F; coherence id F is natural_transformation of F,F proof end; end; definition let A, B be Category; let F, F1, F2 be Functor of A,B; assume that A1: F is_naturally_transformable_to F1 and A2: 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 :Def8: :: NATTRA_1:def 9 t2 * t1; coherence t2 * t1 is natural_transformation of F,F2 proof end; end; :: deftheorem Def8 defines * NATTRA_1:def 9 : for A, B being Category for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 holds t2 * t1 = t2 * t1; theorem Th20: :: NATTRA_1:24 for A, B being Category for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 holds ( (id F2) * t = t & t * (id F1) = t ) proof end; theorem Th21: :: NATTRA_1:25 for A, B being Category for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds 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) proof end; theorem Th22: :: NATTRA_1:26 for A, B being Category for F, F1, F2, F3 being Functor of A,B for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t3 being natural_transformation of F2,F3 holds (t3 * t1) * t = t3 * (t1 * t) proof end; :: Natural equivalences definition let A, B be Category; let F1, F2 be Functor of A,B; 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; :: deftheorem defines invertible NATTRA_1:def 10 : for A, B being Category for F1, F2 being Functor of A,B for IT being transformation of F1,F2 holds ( IT is invertible iff for a being Object of A holds IT . a is invertible ); definition let A, B be Category; let F1, F2 be Functor of A,B; 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 for F1 being Functor of A,B holds ( F1 is_naturally_transformable_to F1 & ex t being natural_transformation of F1,F1 st t is invertible ) proof end; end; :: deftheorem defines are_naturally_equivalent NATTRA_1:def 11 : for A, B being Category for F1, F2 being Functor of A,B holds ( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible ) ); notation let A, B be Category; let F1, F2 be Functor of A,B; synonym F1 ~= F2 for F1,F2 are_naturally_equivalent ; end; Lm3: for A, B being Category for F1, F2 being Functor of A,B for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is invertible holds F2 is_transformable_to F1 proof end; definition let A, B be Category; let F1, F2 be Functor of A,B; assume A1: F1 is_transformable_to F2 ; let t1 be transformation of F1,F2; assume A2: t1 is invertible ; func t1 " -> transformation of F2,F1 means :Def11: :: NATTRA_1:def 12 for a being Object of A holds it . a = (t1 . a) " ; existence ex b1 being transformation of F2,F1 st for a being Object of A holds b1 . a = (t1 . a) " proof end; uniqueness for b1, b2 being transformation of F2,F1 st ( for a being Object of A holds b1 . a = (t1 . a) " ) & ( for a being Object of A holds b2 . a = (t1 . a) " ) holds b1 = b2 proof end; end; :: deftheorem Def11 defines " NATTRA_1:def 12 : for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t1 being transformation of F1,F2 st t1 is invertible holds for b6 being transformation of F2,F1 holds ( b6 = t1 " iff for a being Object of A holds b6 . a = (t1 . a) " ); Lm4: now :: thesis: for A, B being Category for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) let A, B be Category; :: thesis: for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) let F1, F2 be Functor of A,B; :: thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) let t1 be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 & t1 is invertible implies for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) ) assume that A1: F1 is_naturally_transformable_to F2 and A2: t1 is invertible ; :: thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) let a, b be Object of A; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) ) assume A3: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) A4: Hom ((F1 . a),(F1 . b)) <> {} by ; let f be Morphism of a,b; :: thesis: ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) A5: Hom ((F2 . a),(F2 . b)) <> {} by ; A6: F1 is_transformable_to F2 by A1; A7: Hom ((F1 . b),(F2 . b)) <> {} by ; A8: t1 . b is invertible by A2; then A9: Hom ((F2 . b),(F1 . b)) <> {} ; A10: Hom ((F1 . a),(F2 . a)) <> {} by ; (F2 /. f) * (t1 . a) = (t1 . b) * (F1 /. f) by A1, A3, Def7; then A11: (((t1 . b) ") * (F2 /. f)) * (t1 . a) = ((t1 . b) ") * ((t1 . b) * (F1 /. f)) by .= (((t1 . b) ") * (t1 . b)) * (F1 /. f) by .= (id (F1 . b)) * (F1 /. f) by .= F1 /. f by ; A12: t1 . a is invertible by A2; then A13: Hom ((F2 . a),(F1 . a)) <> {} ; then A14: Hom ((F2 . a),(F1 . b)) <> {} by ; then ((t1 . b) ") * (F2 /. f) = (((t1 . b) ") * (F2 /. f)) * (id (F2 . a)) by CAT_1:29 .= (((t1 . b) ") * (F2 /. f)) * ((t1 . a) * ((t1 . a) ")) by .= (F1 /. f) * ((t1 . a) ") by ; hence ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 . a) ") by .= (F1 /. f) * ((t1 ") . a) by ; :: thesis: verum end; Lm5: for A, B being Category for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds F2 is_naturally_transformable_to F1 proof end; definition let A, B be Category; let F1, F2 be Functor of A,B; let t1 be natural_transformation of F1,F2; assume that A1: F1 is_naturally_transformable_to F2 and A2: t1 is invertible ; func t1 " -> natural_transformation of F2,F1 equals :Def12: :: NATTRA_1:def 13 t1 " ; coherence t1 " is natural_transformation of F2,F1 proof end; end; :: deftheorem Def12 defines " NATTRA_1:def 13 : for A, B being Category for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds t1 " = t1 " ; theorem Th23: :: NATTRA_1:27 for A, B being Category for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds for a being Object of A holds (t1 ") . a = (t1 . a) " proof end; theorem :: NATTRA_1:28 for A, B being Category for F1, F2 being Functor of A,B st F1 ~= F2 holds F2 ~= F1 proof end; theorem Th25: :: NATTRA_1:29 for A, B being Category for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds F1 ~= F3 proof end; definition let A, B be Category; let F1, F2 be Functor of A,B; assume A1: F1,F2 are_naturally_equivalent ; mode natural_equivalence of F1,F2 -> natural_transformation of F1,F2 means :Def13: :: NATTRA_1:def 14 it is invertible ; existence ex b1 being natural_transformation of F1,F2 st b1 is invertible by A1; end; :: deftheorem Def13 defines natural_equivalence NATTRA_1:def 14 : for A, B being Category for F1, F2 being Functor of A,B st F1,F2 are_naturally_equivalent holds for b5 being natural_transformation of F1,F2 holds ( b5 is natural_equivalence of F1,F2 iff b5 is invertible ); theorem :: NATTRA_1:30 for A, B being Category for F being Functor of A,B holds id F is natural_equivalence of F,F proof end; theorem :: NATTRA_1:31 for A, B being Category for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds for t being natural_equivalence of F1,F2 for t9 being natural_equivalence of F2,F3 holds t9 * t is natural_equivalence of F1,F3 proof end; definition let A, B be Category; mode NatTrans-DOMAIN of A,B -> non empty set means :Def14: :: NATTRA_1:def 15 for x being set st x in it holds ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ); existence ex b1 being non empty set st for x being set st x in b1 holds ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) proof end; end; :: deftheorem Def14 defines NatTrans-DOMAIN NATTRA_1:def 15 : for A, B being Category for b3 being non empty set holds ( b3 is NatTrans-DOMAIN of A,B iff for x being set st x in b3 holds ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ); definition let A, B be Category; func NatTrans (A,B) -> NatTrans-DOMAIN of A,B means :Def15: :: NATTRA_1:def 16 for x being set holds ( x in it iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ); existence ex b1 being NatTrans-DOMAIN of A,B st for x being set holds ( x in b1 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) proof end; uniqueness for b1, b2 being NatTrans-DOMAIN of A,B st ( for x being set holds ( x in b1 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) & ( for x being set holds ( x in b2 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def15 defines NatTrans NATTRA_1:def 16 : for A, B being Category for b3 being NatTrans-DOMAIN of A,B holds ( b3 = NatTrans (A,B) iff for x being set holds ( x in b3 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ); theorem Th28: :: NATTRA_1:32 for A, B being Category for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 holds ( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B) ) proof end; definition let A, B be Category; func Functors (A,B) -> strict Category means :Def16: :: 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 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 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 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) ); existence ex b1 being strict Category st ( the carrier of b1 = Funct (A,B) & the carrier' of b1 = NatTrans (A,B) & ( for f being Morphism of b1 holds ( dom f = (f 1) 1 & cod f = (f 1) 2 ) ) & ( for f, g being Morphism of b1 st dom g = cod f holds [g,f] in dom the Comp of b1 ) & ( for f, g being Morphism of b1 st [g,f] in dom the Comp of b1 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b1 . [g,f] = [[F,F2],(t1 * t)] ) ) & ( for a being Object of b1 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) ) proof end; uniqueness for b1, b2 being strict Category st the carrier of b1 = Funct (A,B) & the carrier' of b1 = NatTrans (A,B) & ( for f being Morphism of b1 holds ( dom f = (f 1) 1 & cod f = (f 1) 2 ) ) & ( for f, g being Morphism of b1 st dom g = cod f holds [g,f] in dom the Comp of b1 ) & ( for f, g being Morphism of b1 st [g,f] in dom the Comp of b1 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b1 . [g,f] = [[F,F2],(t1 * t)] ) ) & ( for a being Object of b1 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) & the carrier of b2 = Funct (A,B) & the carrier' of b2 = NatTrans (A,B) & ( for f being Morphism of b2 holds ( dom f = (f 1) 1 & cod f = (f 1) 2 ) ) & ( for f, g being Morphism of b2 st dom g = cod f holds [g,f] in dom the Comp of b2 ) & ( for f, g being Morphism of b2 st [g,f] in dom the Comp of b2 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b2 . [g,f] = [[F,F2],(t1 * t)] ) ) & ( for a being Object of b2 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) holds b1 = b2 proof end; end; :: deftheorem Def16 defines Functors NATTRA_1:def 17 : for A, B being Category for b3 being strict Category holds ( b3 = Functors (A,B) iff ( the carrier of b3 = Funct (A,B) & the carrier' of b3 = NatTrans (A,B) & ( for f being Morphism of b3 holds ( dom f = (f 1) 1 & cod f = (f 1) 2 ) ) & ( for f, g being Morphism of b3 st dom g = cod f holds [g,f] in dom the Comp of b3 ) & ( for f, g being Morphism of b3 st [g,f] in dom the Comp of b3 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b3 . [g,f] = [[F,F2],(t1 * t)] ) ) & ( for a being Object of b3 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) ) ); :: As immediate consequences of the definition we get theorem Th29: :: NATTRA_1:33 for A, B being Category for F, F1 being Functor of A,B for t being natural_transformation of F,F1 for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds ( dom f = F & cod f = F1 ) proof end; theorem :: NATTRA_1:34 for A, B being Category for a, b being Object of (Functors (A,B)) for f being Morphism of a,b st Hom (a,b) <> {} holds ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st ( a = F & b = F1 & f = [[F,F1],t] ) proof end; theorem Th31: :: NATTRA_1:35 for A, B being Category for F, F1, F2, F3 being Functor of A,B for t being natural_transformation of F,F1 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 ) proof end; theorem :: NATTRA_1:36 for A, B being Category for F, F1, F2 being Functor of A,B for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 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)] proof end; definition let C be Category; attr C is quasi-discrete means :Def17: :: NATTRA_1:def 18 for a, b being Element of C st Hom (a,b) <> {} holds a = b; attr C is pseudo-discrete means :Def18: :: NATTRA_1:def 19 for a being Element of C holds Hom (a,a) is trivial ; end; :: deftheorem Def17 defines quasi-discrete NATTRA_1:def 18 : for C being Category holds ( C is quasi-discrete iff for a, b being Element of C st Hom (a,b) <> {} holds a = b ); :: deftheorem Def18 defines pseudo-discrete NATTRA_1:def 19 : for C being Category holds ( C is pseudo-discrete iff for a being Element of C holds Hom (a,a) is trivial ); Lm6: for C being Category st C is quasi-discrete holds the carrier' of C = union { (Hom (a,a)) where a is Element of C : verum } proof end; Lm7: for C being Category for a being Element of C st C is pseudo-discrete holds Hom (a,a) = {(id a)} proof end; definition let C be Category; attr C is discrete means :: NATTRA_1:def 20 ( C is quasi-discrete & C is pseudo-discrete ); end; :: deftheorem defines discrete NATTRA_1:def 20 : for C being Category holds ( C is discrete iff ( C is quasi-discrete & C is pseudo-discrete ) ); registration coherence for b1 being Category st b1 is discrete holds ( b1 is quasi-discrete & b1 is pseudo-discrete ) ; coherence for b1 being Category st b1 is quasi-discrete & b1 is pseudo-discrete holds b1 is discrete ; end; Lm8: for C being Category st C is discrete holds the carrier' of C c= { (id a) where a is Element of C : verum } proof end; registration let o, m be set ; cluster 1Cat (o,m) -> discrete ; coherence 1Cat (o,m) is discrete proof end; end; registration existence ex b1 being Category st b1 is discrete proof end; end; registration let C be discrete Category; let a be Element of C; cluster Hom (a,a) -> trivial ; coherence Hom (a,a) is trivial by Def18; end; theorem Th33: :: NATTRA_1:37 for A being discrete Category for a being Object of A holds Hom (a,a) = {(id a)} proof end; registration let A be discrete Category; cluster -> discrete for Subcategory of A; coherence for b1 being Subcategory of A holds b1 is discrete proof end; end; registration let A, B be discrete Category; cluster [:A,B:] -> discrete ; coherence [:A,B:] is discrete proof end; end; theorem :: NATTRA_1:38 canceled; theorem :: NATTRA_1:39 canceled; theorem :: NATTRA_1:40 canceled; ::$CT 3
theorem Th34: :: NATTRA_1:41
for A being discrete Category
for B being Category
for F1, F2 being Functor of B,A st F1 is_transformable_to F2 holds
F1 = F2
proof end;

theorem Th35: :: NATTRA_1:42
for A being discrete Category
for B being Category
for F being Functor of B,A
for t being transformation of F,F holds t = id F
proof end;

registration
let B be Category;
let A be discrete Category;
cluster Functors (B,A) -> strict discrete ;
coherence
Functors (B,A) is discrete
proof end;
end;

registration
let C be Category;
existence
ex b1 being Subcategory of C st
( b1 is strict & b1 is discrete )
proof end;
end;

definition
let C be Category;
func IdCat C -> strict Subcategory of C means :Def20: :: NATTRA_1:def 21
( the carrier of it = the carrier of C & the carrier' of it = { (id a) where a is Object of C : verum } );
existence
ex b1 being strict Subcategory of C st
( the carrier of b1 = the carrier of C & the carrier' of b1 = { (id a) where a is Object of C : verum } )
proof end;
uniqueness
for b1, b2 being strict Subcategory of C st the carrier of b1 = the carrier of C & the carrier' of b1 = { (id a) where a is Object of C : verum } & the carrier of b2 = the carrier of C & the carrier' of b2 = { (id a) where a is Object of C : verum } holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines IdCat NATTRA_1:def 21 :
for C being Category
for b2 being strict Subcategory of C holds
( b2 = IdCat C iff ( the carrier of b2 = the carrier of C & the carrier' of b2 = { (id a) where a is Object of C : verum } ) );

registration
let C be Category;
coherence
proof end;
end;

registration
existence
ex b1 being Category st
( b1 is strict & b1 is discrete )
proof end;
end;

registration
let C be strict discrete Category;
reduce IdCat C to C;
reducibility
IdCat C = C
proof end;
end;

theorem :: NATTRA_1:43
canceled;

theorem :: NATTRA_1:44
canceled;

theorem :: NATTRA_1:45
canceled;

theorem :: NATTRA_1:46
canceled;

::\$CT 4
theorem :: NATTRA_1:47
for A, B being Category holds IdCat [:A,B:] = [:(),():]
proof end;