Home | Metamath
Proof Explorer Theorem List (p. 178 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | idfu1 17701 | Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΌ = (idfuncβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) β β’ (π β ((1st βπΌ)βπ) = π) | ||
Theorem | idfucl 17702 | The identity functor is a functor. Example 3.20(1) of [Adamek] p. 30. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ πΌ = (idfuncβπΆ) β β’ (πΆ β Cat β πΌ β (πΆ Func πΆ)) | ||
Theorem | cofuval 17703* | Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (π· Func πΈ)) β β’ (π β (πΊ βfunc πΉ) = β¨((1st βπΊ) β (1st βπΉ)), (π₯ β π΅, π¦ β π΅ β¦ ((((1st βπΉ)βπ₯)(2nd βπΊ)((1st βπΉ)βπ¦)) β (π₯(2nd βπΉ)π¦)))β©) | ||
Theorem | cofu1st 17704 | Value of the object part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (π· Func πΈ)) β β’ (π β (1st β(πΊ βfunc πΉ)) = ((1st βπΊ) β (1st βπΉ))) | ||
Theorem | cofu1 17705 | Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (π· Func πΈ)) & β’ (π β π β π΅) β β’ (π β ((1st β(πΊ βfunc πΉ))βπ) = ((1st βπΊ)β((1st βπΉ)βπ))) | ||
Theorem | cofu2nd 17706 | Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (π· Func πΈ)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π(2nd β(πΊ βfunc πΉ))π) = ((((1st βπΉ)βπ)(2nd βπΊ)((1st βπΉ)βπ)) β (π(2nd βπΉ)π))) | ||
Theorem | cofu2 17707 | Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (π· Func πΈ)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π» = (Hom βπΆ) & β’ (π β π β (ππ»π)) β β’ (π β ((π(2nd β(πΊ βfunc πΉ))π)βπ ) = ((((1st βπΉ)βπ)(2nd βπΊ)((1st βπΉ)βπ))β((π(2nd βπΉ)π)βπ ))) | ||
Theorem | cofuval2 17708* | Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ (π β πΉ(πΆ Func π·)πΊ) & β’ (π β π»(π· Func πΈ)πΎ) β β’ (π β (β¨π», πΎβ© βfunc β¨πΉ, πΊβ©) = β¨(π» β πΉ), (π₯ β π΅, π¦ β π΅ β¦ (((πΉβπ₯)πΎ(πΉβπ¦)) β (π₯πΊπ¦)))β©) | ||
Theorem | cofucl 17709 | The composition of two functors is a functor. Proposition 3.23 of [Adamek] p. 33. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (π· Func πΈ)) β β’ (π β (πΊ βfunc πΉ) β (πΆ Func πΈ)) | ||
Theorem | cofuass 17710 | Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ (π β πΊ β (πΆ Func π·)) & β’ (π β π» β (π· Func πΈ)) & β’ (π β πΎ β (πΈ Func πΉ)) β β’ (π β ((πΎ βfunc π») βfunc πΊ) = (πΎ βfunc (π» βfunc πΊ))) | ||
Theorem | cofulid 17711 | The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ (π β πΉ β (πΆ Func π·)) & β’ πΌ = (idfuncβπ·) β β’ (π β (πΌ βfunc πΉ) = πΉ) | ||
Theorem | cofurid 17712 | The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ (π β πΉ β (πΆ Func π·)) & β’ πΌ = (idfuncβπΆ) β β’ (π β (πΉ βfunc πΌ) = πΉ) | ||
Theorem | resfval 17713* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β πΉ β π) & β’ (π β π» β π) β β’ (π β (πΉ βΎf π») = β¨((1st βπΉ) βΎ dom dom π»), (π₯ β dom π» β¦ (((2nd βπΉ)βπ₯) βΎ (π»βπ₯)))β©) | ||
Theorem | resfval2 17714* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β πΉ β π) & β’ (π β π» β π) & β’ (π β πΊ β π) & β’ (π β π» Fn (π Γ π)) β β’ (π β (β¨πΉ, πΊβ© βΎf π») = β¨(πΉ βΎ π), (π₯ β π, π¦ β π β¦ ((π₯πΊπ¦) βΎ (π₯π»π¦)))β©) | ||
Theorem | resf1st 17715 | Value of the functor restriction operator on objects. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β πΉ β π) & β’ (π β π» β π) & β’ (π β π» Fn (π Γ π)) β β’ (π β (1st β(πΉ βΎf π»)) = ((1st βπΉ) βΎ π)) | ||
Theorem | resf2nd 17716 | Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β πΉ β π) & β’ (π β π» β π) & β’ (π β π» Fn (π Γ π)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π(2nd β(πΉ βΎf π»))π) = ((π(2nd βπΉ)π) βΎ (ππ»π))) | ||
Theorem | funcres 17717 | A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β πΉ β (πΆ Func π·)) & β’ (π β π» β (SubcatβπΆ)) β β’ (π β (πΉ βΎf π») β ((πΆ βΎcat π») Func π·)) | ||
Theorem | funcres2b 17718* | Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π΄ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β π β (Subcatβπ·)) & β’ (π β π Fn (π Γ π)) & β’ (π β πΉ:π΄βΆπ) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯πΊπ¦):πβΆ((πΉβπ₯)π (πΉβπ¦))) β β’ (π β (πΉ(πΆ Func π·)πΊ β πΉ(πΆ Func (π· βΎcat π ))πΊ)) | ||
Theorem | funcres2 17719 | A functor into a restricted category is also a functor into the whole category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β (Subcatβπ·) β (πΆ Func (π· βΎcat π )) β (πΆ Func π·)) | ||
Theorem | wunfunc 17720 | A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.) |
β’ (π β π β WUni) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (πΆ Func π·) β π) | ||
Theorem | wunfuncOLD 17721 | Obsolete proof of wunfunc 17720 as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π β WUni) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (πΆ Func π·) β π) | ||
Theorem | funcpropd 17722 | If two categories have the same set of objects, morphisms, and compositions, then they have the same functors. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ (π β (Homf βπ΄) = (Homf βπ΅)) & β’ (π β (compfβπ΄) = (compfβπ΅)) & β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (π΄ Func πΆ) = (π΅ Func π·)) | ||
Theorem | funcres2c 17723 | Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
β’ π΄ = (BaseβπΆ) & β’ πΈ = (π· βΎs π) & β’ (π β π· β Cat) & β’ (π β π β π) & β’ (π β πΉ:π΄βΆπ) β β’ (π β (πΉ(πΆ Func π·)πΊ β πΉ(πΆ Func πΈ)πΊ)) | ||
Syntax | cful 17724 | Extend class notation with the class of all full functors. |
class Full | ||
Syntax | cfth 17725 | Extend class notation with the class of all faithful functors. |
class Faith | ||
Definition | df-full 17726* | Function returning all the full functors from a category πΆ to a category π·. A full functor is a functor in which all the morphism maps πΊ(π, π) between objects π, π β πΆ are surjections. Definition 3.27(3) in [Adamek] p. 34. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ Full = (π β Cat, π β Cat β¦ {β¨π, πβ© β£ (π(π Func π)π β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)ran (π₯ππ¦) = ((πβπ₯)(Hom βπ)(πβπ¦)))}) | ||
Definition | df-fth 17727* | Function returning all the faithful functors from a category πΆ to a category π·. A faithful functor is a functor in which all the morphism maps πΊ(π, π) between objects π, π β πΆ are injections. Definition 3.27(2) in [Adamek] p. 34. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ Faith = (π β Cat, π β Cat β¦ {β¨π, πβ© β£ (π(π Func π)π β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)Fun β‘(π₯ππ¦))}) | ||
Theorem | fullfunc 17728 | A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ (πΆ Full π·) β (πΆ Func π·) | ||
Theorem | fthfunc 17729 | A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ (πΆ Faith π·) β (πΆ Func π·) | ||
Theorem | relfull 17730 | The set of full functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ Rel (πΆ Full π·) | ||
Theorem | relfth 17731 | The set of faithful functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ Rel (πΆ Faith π·) | ||
Theorem | isfull 17732* | Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π½ = (Hom βπ·) β β’ (πΉ(πΆ Full π·)πΊ β (πΉ(πΆ Func π·)πΊ β§ βπ₯ β π΅ βπ¦ β π΅ ran (π₯πΊπ¦) = ((πΉβπ₯)π½(πΉβπ¦)))) | ||
Theorem | isfull2 17733* | Equivalent condition for a full functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π½ = (Hom βπ·) & β’ π» = (Hom βπΆ) β β’ (πΉ(πΆ Full π·)πΊ β (πΉ(πΆ Func π·)πΊ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯πΊπ¦):(π₯π»π¦)βontoβ((πΉβπ₯)π½(πΉβπ¦)))) | ||
Theorem | fullfo 17734 | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π½ = (Hom βπ·) & β’ π» = (Hom βπΆ) & β’ (π β πΉ(πΆ Full π·)πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΊπ):(ππ»π)βontoβ((πΉβπ)π½(πΉβπ))) | ||
Theorem | fulli 17735* | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π½ = (Hom βπ·) & β’ π» = (Hom βπΆ) & β’ (π β πΉ(πΆ Full π·)πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β ((πΉβπ)π½(πΉβπ))) β β’ (π β βπ β (ππ»π)π = ((ππΊπ)βπ)) | ||
Theorem | isfth 17736* | Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) β β’ (πΉ(πΆ Faith π·)πΊ β (πΉ(πΆ Func π·)πΊ β§ βπ₯ β π΅ βπ¦ β π΅ Fun β‘(π₯πΊπ¦))) | ||
Theorem | isfth2 17737* | Equivalent condition for a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) β β’ (πΉ(πΆ Faith π·)πΊ β (πΉ(πΆ Func π·)πΊ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯πΊπ¦):(π₯π»π¦)β1-1β((πΉβπ₯)π½(πΉβπ¦)))) | ||
Theorem | isffth2 17738* | A fully faithful functor is a functor which is bijective on hom-sets. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) β β’ (πΉ((πΆ Full π·) β© (πΆ Faith π·))πΊ β (πΉ(πΆ Func π·)πΊ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯πΊπ¦):(π₯π»π¦)β1-1-ontoβ((πΉβπ₯)π½(πΉβπ¦)))) | ||
Theorem | fthf1 17739 | The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ (π β πΉ(πΆ Faith π·)πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΊπ):(ππ»π)β1-1β((πΉβπ)π½(πΉβπ))) | ||
Theorem | fthi 17740 | The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ (π β πΉ(πΆ Faith π·)πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β (ππ»π)) & β’ (π β π β (ππ»π)) β β’ (π β (((ππΊπ)βπ ) = ((ππΊπ)βπ) β π = π)) | ||
Theorem | ffthf1o 17741 | The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ (π β πΉ((πΆ Full π·) β© (πΆ Faith π·))πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΊπ):(ππ»π)β1-1-ontoβ((πΉβπ)π½(πΉβπ))) | ||
Theorem | fullpropd 17742 | If two categories have the same set of objects, morphisms, and compositions, then they have the same full functors. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ (π β (Homf βπ΄) = (Homf βπ΅)) & β’ (π β (compfβπ΄) = (compfβπ΅)) & β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (π΄ Full πΆ) = (π΅ Full π·)) | ||
Theorem | fthpropd 17743 | If two categories have the same set of objects, morphisms, and compositions, then they have the same faithful functors. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ (π β (Homf βπ΄) = (Homf βπ΅)) & β’ (π β (compfβπ΄) = (compfβπ΅)) & β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (π΄ Faith πΆ) = (π΅ Faith π·)) | ||
Theorem | fulloppc 17744 | The opposite functor of a full functor is also full. Proposition 3.43(d) in [Adamek] p. 39. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ π = (oppCatβπ·) & β’ (π β πΉ(πΆ Full π·)πΊ) β β’ (π β πΉ(π Full π)tpos πΊ) | ||
Theorem | fthoppc 17745 | The opposite functor of a faithful functor is also faithful. Proposition 3.43(c) in [Adamek] p. 39. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ π = (oppCatβπ·) & β’ (π β πΉ(πΆ Faith π·)πΊ) β β’ (π β πΉ(π Faith π)tpos πΊ) | ||
Theorem | ffthoppc 17746 | The opposite functor of a fully faithful functor is also full and faithful. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ π = (oppCatβπ·) & β’ (π β πΉ((πΆ Full π·) β© (πΆ Faith π·))πΊ) β β’ (π β πΉ((π Full π) β© (π Faith π))tpos πΊ) | ||
Theorem | fthsect 17747 | A faithful functor reflects sections. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ(πΆ Faith π·)πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β (ππ»π)) & β’ (π β π β (ππ»π)) & β’ π = (SectβπΆ) & β’ π = (Sectβπ·) β β’ (π β (π(πππ)π β ((ππΊπ)βπ)((πΉβπ)π(πΉβπ))((ππΊπ)βπ))) | ||
Theorem | fthinv 17748 | A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ(πΆ Faith π·)πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β (ππ»π)) & β’ (π β π β (ππ»π)) & β’ πΌ = (InvβπΆ) & β’ π½ = (Invβπ·) β β’ (π β (π(ππΌπ)π β ((ππΊπ)βπ)((πΉβπ)π½(πΉβπ))((ππΊπ)βπ))) | ||
Theorem | fthmon 17749 | A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ(πΆ Faith π·)πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β (ππ»π)) & β’ π = (MonoβπΆ) & β’ π = (Monoβπ·) & β’ (π β ((ππΊπ)βπ ) β ((πΉβπ)π(πΉβπ))) β β’ (π β π β (πππ)) | ||
Theorem | fthepi 17750 | A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ(πΆ Faith π·)πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β (ππ»π)) & β’ πΈ = (EpiβπΆ) & β’ π = (Epiβπ·) & β’ (π β ((ππΊπ)βπ ) β ((πΉβπ)π(πΉβπ))) β β’ (π β π β (ππΈπ)) | ||
Theorem | ffthiso 17751 | A fully faithful functor reflects isomorphisms. Corollary 3.32 of [Adamek] p. 35. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ(πΆ Faith π·)πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β (ππ»π)) & β’ (π β πΉ(πΆ Full π·)πΊ) & β’ πΌ = (IsoβπΆ) & β’ π½ = (Isoβπ·) β β’ (π β (π β (ππΌπ) β ((ππΊπ)βπ ) β ((πΉβπ)π½(πΉβπ)))) | ||
Theorem | fthres2b 17752* | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΄ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β π β (Subcatβπ·)) & β’ (π β π Fn (π Γ π)) & β’ (π β πΉ:π΄βΆπ) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯πΊπ¦):πβΆ((πΉβπ₯)π (πΉβπ¦))) β β’ (π β (πΉ(πΆ Faith π·)πΊ β πΉ(πΆ Faith (π· βΎcat π ))πΊ)) | ||
Theorem | fthres2c 17753 | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
β’ π΄ = (BaseβπΆ) & β’ πΈ = (π· βΎs π) & β’ (π β π· β Cat) & β’ (π β π β π) & β’ (π β πΉ:π΄βΆπ) β β’ (π β (πΉ(πΆ Faith π·)πΊ β πΉ(πΆ Faith πΈ)πΊ)) | ||
Theorem | fthres2 17754 | A faithful functor into a restricted category is also a faithful functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ (π β (Subcatβπ·) β (πΆ Faith (π· βΎcat π )) β (πΆ Faith π·)) | ||
Theorem | idffth 17755 | The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ πΌ = (idfuncβπΆ) β β’ (πΆ β Cat β πΌ β ((πΆ Full πΆ) β© (πΆ Faith πΆ))) | ||
Theorem | cofull 17756 | The composition of two full functors is full. Proposition 3.30(d) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ (π β πΉ β (πΆ Full π·)) & β’ (π β πΊ β (π· Full πΈ)) β β’ (π β (πΊ βfunc πΉ) β (πΆ Full πΈ)) | ||
Theorem | cofth 17757 | The composition of two faithful functors is faithful. Proposition 3.30(c) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ (π β πΉ β (πΆ Faith π·)) & β’ (π β πΊ β (π· Faith πΈ)) β β’ (π β (πΊ βfunc πΉ) β (πΆ Faith πΈ)) | ||
Theorem | coffth 17758 | The composition of two fully faithful functors is fully faithful. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ (π β πΉ β ((πΆ Full π·) β© (πΆ Faith π·))) & β’ (π β πΊ β ((π· Full πΈ) β© (π· Faith πΈ))) β β’ (π β (πΊ βfunc πΉ) β ((πΆ Full πΈ) β© (πΆ Faith πΈ))) | ||
Theorem | rescfth 17759 | The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π· = (πΆ βΎcat π½) & β’ πΌ = (idfuncβπ·) β β’ (π½ β (SubcatβπΆ) β πΌ β (π· Faith πΆ)) | ||
Theorem | ressffth 17760 | The inclusion functor from a full subcategory is a full and faithful functor, see also remark 4.4(2) in [Adamek] p. 49. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π· = (πΆ βΎs π) & β’ πΌ = (idfuncβπ·) β β’ ((πΆ β Cat β§ π β π) β πΌ β ((π· Full πΆ) β© (π· Faith πΆ))) | ||
Theorem | fullres2c 17761 | Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
β’ π΄ = (BaseβπΆ) & β’ πΈ = (π· βΎs π) & β’ (π β π· β Cat) & β’ (π β π β π) & β’ (π β πΉ:π΄βΆπ) β β’ (π β (πΉ(πΆ Full π·)πΊ β πΉ(πΆ Full πΈ)πΊ)) | ||
Theorem | ffthres2c 17762 | Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΄ = (BaseβπΆ) & β’ πΈ = (π· βΎs π) & β’ (π β π· β Cat) & β’ (π β π β π) & β’ (π β πΉ:π΄βΆπ) β β’ (π β (πΉ((πΆ Full π·) β© (πΆ Faith π·))πΊ β πΉ((πΆ Full πΈ) β© (πΆ Faith πΈ))πΊ)) | ||
Syntax | cnat 17763 | Extend class notation to include the collection of natural transformations. |
class Nat | ||
Syntax | cfuc 17764 | Extend class notation to include the functor category. |
class FuncCat | ||
Definition | df-nat 17765* | Definition of a natural transformation between two functors. A natural transformation π΄:πΉβΆπΊ is a collection of arrows π΄(π₯):πΉ(π₯)βΆπΊ(π₯), such that π΄(π¦) β πΉ(β) = πΊ(β) β π΄(π₯) for each morphism β:π₯βΆπ¦. Definition 6.1 in [Adamek] p. 83, and definition in [Lang] p. 65. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ Nat = (π‘ β Cat, π’ β Cat β¦ (π β (π‘ Func π’), π β (π‘ Func π’) β¦ β¦(1st βπ) / πβ¦β¦(1st βπ) / π β¦{π β Xπ₯ β (Baseβπ‘)((πβπ₯)(Hom βπ’)(π βπ₯)) β£ βπ₯ β (Baseβπ‘)βπ¦ β (Baseβπ‘)ββ β (π₯(Hom βπ‘)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ’)(π βπ¦))((π₯(2nd βπ)π¦)ββ)) = (((π₯(2nd βπ)π¦)ββ)(β¨(πβπ₯), (π βπ₯)β©(compβπ’)(π βπ¦))(πβπ₯))})) | ||
Definition | df-fuc 17766* | Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ FuncCat = (π‘ β Cat, π’ β Cat β¦ {β¨(Baseβndx), (π‘ Func π’)β©, β¨(Hom βndx), (π‘ Nat π’)β©, β¨(compβndx), (π£ β ((π‘ Func π’) Γ (π‘ Func π’)), β β (π‘ Func π’) β¦ β¦(1st βπ£) / πβ¦β¦(2nd βπ£) / πβ¦(π β (π(π‘ Nat π’)β), π β (π(π‘ Nat π’)π) β¦ (π₯ β (Baseβπ‘) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ’)((1st ββ)βπ₯))(πβπ₯)))))β©}) | ||
Theorem | fnfuc 17767 | The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ FuncCat Fn (Cat Γ Cat) | ||
Theorem | natfval 17768* | Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.) |
β’ π = (πΆ Nat π·) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ Β· = (compβπ·) β β’ π = (π β (πΆ Func π·), π β (πΆ Func π·) β¦ β¦(1st βπ) / πβ¦β¦(1st βπ) / π β¦{π β Xπ₯ β π΅ ((πβπ₯)π½(π βπ₯)) β£ βπ₯ β π΅ βπ¦ β π΅ ββ β (π₯π»π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β© Β· (π βπ¦))((π₯(2nd βπ)π¦)ββ)) = (((π₯(2nd βπ)π¦)ββ)(β¨(πβπ₯), (π βπ₯)β© Β· (π βπ¦))(πβπ₯))}) | ||
Theorem | isnat 17769* | Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ Β· = (compβπ·) & β’ (π β πΉ(πΆ Func π·)πΊ) & β’ (π β πΎ(πΆ Func π·)πΏ) β β’ (π β (π΄ β (β¨πΉ, πΊβ©πβ¨πΎ, πΏβ©) β (π΄ β Xπ₯ β π΅ ((πΉβπ₯)π½(πΎβπ₯)) β§ βπ₯ β π΅ βπ¦ β π΅ ββ β (π₯π»π¦)((π΄βπ¦)(β¨(πΉβπ₯), (πΉβπ¦)β© Β· (πΎβπ¦))((π₯πΊπ¦)ββ)) = (((π₯πΏπ¦)ββ)(β¨(πΉβπ₯), (πΎβπ₯)β© Β· (πΎβπ¦))(π΄βπ₯))))) | ||
Theorem | isnat2 17770* | Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ Β· = (compβπ·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) β β’ (π β (π΄ β (πΉππΊ) β (π΄ β Xπ₯ β π΅ (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)) β§ βπ₯ β π΅ βπ¦ β π΅ ββ β (π₯π»π¦)((π΄βπ¦)(β¨((1st βπΉ)βπ₯), ((1st βπΉ)βπ¦)β© Β· ((1st βπΊ)βπ¦))((π₯(2nd βπΉ)π¦)ββ)) = (((π₯(2nd βπΊ)π¦)ββ)(β¨((1st βπΉ)βπ₯), ((1st βπΊ)βπ₯)β© Β· ((1st βπΊ)βπ¦))(π΄βπ₯))))) | ||
Theorem | natffn 17771 | The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΆ Nat π·) β β’ π Fn ((πΆ Func π·) Γ (πΆ Func π·)) | ||
Theorem | natrcl 17772 | Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) β β’ (π΄ β (πΉππΊ) β (πΉ β (πΆ Func π·) β§ πΊ β (πΆ Func π·))) | ||
Theorem | nat1st2nd 17773 | Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ (π β π΄ β (πΉππΊ)) β β’ (π β π΄ β (β¨(1st βπΉ), (2nd βπΉ)β©πβ¨(1st βπΊ), (2nd βπΊ)β©)) | ||
Theorem | natixp 17774* | A natural transformation is a function from the objects of πΆ to homomorphisms from πΉ(π₯) to πΊ(π₯). (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ (π β π΄ β (β¨πΉ, πΊβ©πβ¨πΎ, πΏβ©)) & β’ π΅ = (BaseβπΆ) & β’ π½ = (Hom βπ·) β β’ (π β π΄ β Xπ₯ β π΅ ((πΉβπ₯)π½(πΎβπ₯))) | ||
Theorem | natcl 17775 | A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ (π β π΄ β (β¨πΉ, πΊβ©πβ¨πΎ, πΏβ©)) & β’ π΅ = (BaseβπΆ) & β’ π½ = (Hom βπ·) & β’ (π β π β π΅) β β’ (π β (π΄βπ) β ((πΉβπ)π½(πΎβπ))) | ||
Theorem | natfn 17776 | A natural transformation is a function on the objects of πΆ. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ (π β π΄ β (β¨πΉ, πΊβ©πβ¨πΎ, πΏβ©)) & β’ π΅ = (BaseβπΆ) β β’ (π β π΄ Fn π΅) | ||
Theorem | nati 17777 | Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ (π β π΄ β (β¨πΉ, πΊβ©πβ¨πΎ, πΏβ©)) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπ·) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β (ππ»π)) β β’ (π β ((π΄βπ)(β¨(πΉβπ), (πΉβπ)β© Β· (πΎβπ))((ππΊπ)βπ )) = (((ππΏπ)βπ )(β¨(πΉβπ), (πΎβπ)β© Β· (πΎβπ))(π΄βπ))) | ||
Theorem | wunnat 17778 | A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.) |
β’ (π β π β WUni) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (πΆ Nat π·) β π) | ||
Theorem | wunnatOLD 17779 | Obsolete proof of wunnat 17778 as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π β WUni) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (πΆ Nat π·) β π) | ||
Theorem | catstr 17780 | A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ {β¨(Baseβndx), πβ©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©} Struct β¨1, ;15β© | ||
Theorem | fucval 17781* | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (πΆ Func π·) & β’ π = (πΆ Nat π·) & β’ π΄ = (BaseβπΆ) & β’ Β· = (compβπ·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β β = (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st βπ£) / πβ¦β¦(2nd βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st ββ)βπ₯))(πβπ₯)))))) β β’ (π β π = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), πβ©, β¨(compβndx), β β©}) | ||
Theorem | fuccofval 17782* | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (πΆ Func π·) & β’ π = (πΆ Nat π·) & β’ π΄ = (BaseβπΆ) & β’ Β· = (compβπ·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ β = (compβπ) β β’ (π β β = (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st βπ£) / πβ¦β¦(2nd βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st ββ)βπ₯))(πβπ₯)))))) | ||
Theorem | fucbas 17783 | The objects of the functor category are functors from πΆ to π·. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΆ FuncCat π·) β β’ (πΆ Func π·) = (Baseβπ) | ||
Theorem | fuchom 17784 | The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) β β’ π = (Hom βπ) | ||
Theorem | fuchomOLD 17785 | Obsolete proof of fuchom 17784 as of 14-Oct-2024. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) β β’ π = (Hom βπ) | ||
Theorem | fucco 17786* | Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ π΄ = (BaseβπΆ) & β’ Β· = (compβπ·) & β’ β = (compβπ) & β’ (π β π β (πΉππΊ)) & β’ (π β π β (πΊππ»)) β β’ (π β (π(β¨πΉ, πΊβ© β π»)π ) = (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπΉ)βπ₯), ((1st βπΊ)βπ₯)β© Β· ((1st βπ»)βπ₯))(π βπ₯)))) | ||
Theorem | fuccoval 17787 | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ π΄ = (BaseβπΆ) & β’ Β· = (compβπ·) & β’ β = (compβπ) & β’ (π β π β (πΉππΊ)) & β’ (π β π β (πΊππ»)) & β’ (π β π β π΄) β β’ (π β ((π(β¨πΉ, πΊβ© β π»)π )βπ) = ((πβπ)(β¨((1st βπΉ)βπ), ((1st βπΊ)βπ)β© Β· ((1st βπ»)βπ))(π βπ))) | ||
Theorem | fuccocl 17788 | The composition of two natural transformations is a natural transformation. Remark 6.14(a) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ β = (compβπ) & β’ (π β π β (πΉππΊ)) & β’ (π β π β (πΊππ»)) β β’ (π β (π(β¨πΉ, πΊβ© β π»)π ) β (πΉππ»)) | ||
Theorem | fucidcl 17789 | The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ 1 = (Idβπ·) & β’ (π β πΉ β (πΆ Func π·)) β β’ (π β ( 1 β (1st βπΉ)) β (πΉππΉ)) | ||
Theorem | fuclid 17790 | Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ β = (compβπ) & β’ 1 = (Idβπ·) & β’ (π β π β (πΉππΊ)) β β’ (π β (( 1 β (1st βπΊ))(β¨πΉ, πΊβ© β πΊ)π ) = π ) | ||
Theorem | fucrid 17791 | Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ β = (compβπ) & β’ 1 = (Idβπ·) & β’ (π β π β (πΉππΊ)) β β’ (π β (π (β¨πΉ, πΉβ© β πΊ)( 1 β (1st βπΉ))) = π ) | ||
Theorem | fucass 17792 | Associativity of natural transformation composition. Remark 6.14(b) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ β = (compβπ) & β’ (π β π β (πΉππΊ)) & β’ (π β π β (πΊππ»)) & β’ (π β π β (π»ππΎ)) β β’ (π β ((π(β¨πΊ, π»β© β πΎ)π)(β¨πΉ, πΊβ© β πΎ)π ) = (π(β¨πΉ, π»β© β πΎ)(π(β¨πΉ, πΊβ© β π»)π ))) | ||
Theorem | fuccatid 17793* | The functor category is a category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ 1 = (Idβπ·) β β’ (π β (π β Cat β§ (Idβπ) = (π β (πΆ Func π·) β¦ ( 1 β (1st βπ))))) | ||
Theorem | fuccat 17794 | The functor category is a category. Remark 6.16 in [Adamek] p. 88. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β π β Cat) | ||
Theorem | fucid 17795 | The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ πΌ = (Idβπ) & β’ 1 = (Idβπ·) & β’ (π β πΉ β (πΆ Func π·)) β β’ (π β (πΌβπΉ) = ( 1 β (1st βπΉ))) | ||
Theorem | fucsect 17796* | Two natural transformations are in a section iff all the components are in a section relation. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (BaseβπΆ) & β’ π = (πΆ Nat π·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) & β’ π = (Sectβπ) & β’ π = (Sectβπ·) β β’ (π β (π(πΉππΊ)π β (π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π((1st βπΊ)βπ₯))(πβπ₯)))) | ||
Theorem | fucinv 17797* | Two natural transformations are inverses of each other iff all the components are inverse. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (BaseβπΆ) & β’ π = (πΆ Nat π·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) & β’ πΌ = (Invβπ) & β’ π½ = (Invβπ·) β β’ (π β (π(πΉπΌπΊ)π β (π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))(πβπ₯)))) | ||
Theorem | invfuc 17798* | If π(π₯) is an inverse to π(π₯) for each π₯, and π is a natural transformation, then π is also a natural transformation, and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (BaseβπΆ) & β’ π = (πΆ Nat π·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) & β’ πΌ = (Invβπ) & β’ π½ = (Invβπ·) & β’ (π β π β (πΉππΊ)) & β’ ((π β§ π₯ β π΅) β (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))π) β β’ (π β π(πΉπΌπΊ)(π₯ β π΅ β¦ π)) | ||
Theorem | fuciso 17799* | A natural transformation is an isomorphism of functors iff all its components are isomorphisms. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (BaseβπΆ) & β’ π = (πΆ Nat π·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) & β’ πΌ = (Isoβπ) & β’ π½ = (Isoβπ·) β β’ (π β (π΄ β (πΉπΌπΊ) β (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))))) | ||
Theorem | natpropd 17800 | If two categories have the same set of objects, morphisms, and compositions, then they have the same natural transformations. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ (π β (Homf βπ΄) = (Homf βπ΅)) & β’ (π β (compfβπ΄) = (compfβπ΅)) & β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β π΄ β Cat) & β’ (π β π΅ β Cat) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β (π΄ Nat πΆ) = (π΅ Nat π·)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |