![]() |
Metamath
Proof Explorer Theorem List (p. 182 of 479) | < 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: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | funcestrcsetc 18101* | The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 23-Mar-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ (π β πΉ(πΈ Func π)πΊ) | ||
Theorem | fthestrcsetc 18102* | The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is faithful. (Contributed by AV, 2-Apr-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ (π β πΉ(πΈ Faith π)πΊ) | ||
Theorem | fullestrcsetc 18103* | The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is full. (Contributed by AV, 2-Apr-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ (π β πΉ(πΈ Full π)πΊ) | ||
Theorem | equivestrcsetc 18104* | The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is an equivalence. According to definition 3.33 (1) of [Adamek] p. 36, "A functor F : A -> B is called an equivalence provided that it is full, faithful, and isomorphism-dense in the sense that for any B-object B' there exists some A-object A' such that F(A') is isomorphic to B'.". Therefore, the category of sets and the category of extensible structures are equivalent, according to definition 3.33 (2) of [Adamek] p. 36, "Categories A and B are called equivalent provided that there is an equivalence from A to B.". (Contributed by AV, 2-Apr-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) & β’ (π β (Baseβndx) β π) β β’ (π β (πΉ(πΈ Faith π)πΊ β§ πΉ(πΈ Full π)πΊ β§ βπ β πΆ βπ β π΅ βπ π:πβ1-1-ontoβ(πΉβπ))) | ||
Theorem | setc1strwun 18105 | A constructed one-slot structure with the objects of the category of sets as base set in a weak universe. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β Ο β π) β β’ ((π β§ π β πΆ) β {β¨(Baseβndx), πβ©} β π) | ||
Theorem | funcsetcestrclem1 18106* | Lemma 1 for funcsetcestrc 18116. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) β β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) | ||
Theorem | funcsetcestrclem2 18107* | Lemma 2 for funcsetcestrc 18116. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) β β’ ((π β§ π β πΆ) β (πΉβπ) β π) | ||
Theorem | funcsetcestrclem3 18108* | Lemma 3 for funcsetcestrc 18116. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ πΈ = (ExtStrCatβπ) & β’ π΅ = (BaseβπΈ) β β’ (π β πΉ:πΆβΆπ΅) | ||
Theorem | embedsetcestrclem 18109* | Lemma for embedsetcestrc 18119. (Contributed by AV, 31-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ πΈ = (ExtStrCatβπ) & β’ π΅ = (BaseβπΈ) β β’ (π β πΉ:πΆβ1-1βπ΅) | ||
Theorem | funcsetcestrclem4 18110* | Lemma 4 for funcsetcestrc 18116. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) β β’ (π β πΊ Fn (πΆ Γ πΆ)) | ||
Theorem | funcsetcestrclem5 18111* | Lemma 5 for funcsetcestrc 18116. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) β β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ) = ( I βΎ (π βm π))) | ||
Theorem | funcsetcestrclem6 18112* | Lemma 6 for funcsetcestrc 18116. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) β β’ ((π β§ (π β πΆ β§ π β πΆ) β§ π» β (π βm π)) β ((ππΊπ)βπ») = π») | ||
Theorem | funcsetcestrclem7 18113* | Lemma 7 for funcsetcestrc 18116. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ ((π β§ π β πΆ) β ((ππΊπ)β((Idβπ)βπ)) = ((IdβπΈ)β(πΉβπ))) | ||
Theorem | funcsetcestrclem8 18114* | Lemma 8 for funcsetcestrc 18116. (Contributed by AV, 28-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ):(π(Hom βπ)π)βΆ((πΉβπ)(Hom βπΈ)(πΉβπ))) | ||
Theorem | funcsetcestrclem9 18115* | Lemma 9 for funcsetcestrc 18116. (Contributed by AV, 28-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ) β§ (π» β (π(Hom βπ)π) β§ πΎ β (π(Hom βπ)π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»))) | ||
Theorem | funcsetcestrc 18116* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 28-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ (π β πΉ(π Func πΈ)πΊ) | ||
Theorem | fthsetcestrc 18117* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is faithful. (Contributed by AV, 31-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ (π β πΉ(π Faith πΈ)πΊ) | ||
Theorem | fullsetcestrc 18118* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is full. (Contributed by AV, 1-Apr-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ (π β πΉ(π Full πΈ)πΊ) | ||
Theorem | embedsetcestrc 18119* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is an embedding. According to definition 3.27 (1) of [Adamek] p. 34, a functor "F is called an embedding provided that F is injective on morphisms", or according to remark 3.28 (1) in [Adamek] p. 34, "a functor is an embedding if and only if it is faithful and injective on objects". (Contributed by AV, 31-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) & β’ π΅ = (BaseβπΈ) β β’ (π β (πΉ(π Faith πΈ)πΊ β§ πΉ:πΆβ1-1βπ΅)) | ||
Syntax | cxpc 18120 | Extend class notation with the product of two categories. |
class Γc | ||
Syntax | c1stf 18121 | Extend class notation with the first projection functor. |
class 1stF | ||
Syntax | c2ndf 18122 | Extend class notation with the second projection functor. |
class 2ndF | ||
Syntax | cprf 18123 | Extend class notation with the functor pairing operation. |
class β¨,β©F | ||
Definition | df-xpc 18124* | Define the binary product of categories, which has objects for each pair of objects of the factors, and morphisms for each pair of morphisms of the factors. Composition is componentwise. (Contributed by Mario Carneiro, 10-Jan-2017.) |
β’ Γc = (π β V, π β V β¦ β¦((Baseβπ) Γ (Baseβπ )) / πβ¦β¦(π’ β π, π£ β π β¦ (((1st βπ’)(Hom βπ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ )(2nd βπ£)))) / ββ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx), ββ©, β¨(compβndx), (π₯ β (π Γ π), π¦ β π β¦ (π β ((2nd βπ₯)βπ¦), π β (ββπ₯) β¦ β¨((1st βπ)(β¨(1st β(1st βπ₯)), (1st β(2nd βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd β(1st βπ₯)), (2nd β(2nd βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β©))β©}) | ||
Definition | df-1stf 18125* | Define the first projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ 1stF = (π β Cat, π β Cat β¦ β¦((Baseβπ) Γ (Baseβπ )) / πβ¦β¨(1st βΎ π), (π₯ β π, π¦ β π β¦ (1st βΎ (π₯(Hom β(π Γc π ))π¦)))β©) | ||
Definition | df-2ndf 18126* | Define the second projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ 2ndF = (π β Cat, π β Cat β¦ β¦((Baseβπ) Γ (Baseβπ )) / πβ¦β¨(2nd βΎ π), (π₯ β π, π¦ β π β¦ (2nd βΎ (π₯(Hom β(π Γc π ))π¦)))β©) | ||
Definition | df-prf 18127* | Define the pairing operation for functors (which takes two functors πΉ:πΆβΆπ· and πΊ:πΆβΆπΈ and produces (πΉ β¨,β©F πΊ):πΆβΆ(π· Γc πΈ)). (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ β¨,β©F = (π β V, π β V β¦ β¦dom (1st βπ) / πβ¦β¨(π₯ β π β¦ β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©), (π₯ β π, π¦ β π β¦ (β β dom (π₯(2nd βπ)π¦) β¦ β¨((π₯(2nd βπ)π¦)ββ), ((π₯(2nd βπ)π¦)ββ)β©))β©) | ||
Theorem | fnxpc 18128 | The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.) |
β’ Γc Fn (V Γ V) | ||
Theorem | xpcval 18129* | Value of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π = (BaseβπΆ) & β’ π = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ Β· = (compβπΆ) & β’ β = (compβπ·) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΅ = (π Γ π)) & β’ (π β πΎ = (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))) & β’ (π β π = (π₯ β (π΅ Γ π΅), π¦ β π΅ β¦ (π β ((2nd βπ₯)πΎπ¦), π β (πΎβπ₯) β¦ β¨((1st βπ)(β¨(1st β(1st βπ₯)), (1st β(2nd βπ₯))β© Β· (1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd β(1st βπ₯)), (2nd β(2nd βπ₯))β© β (2nd βπ¦))(2nd βπ))β©))) β β’ (π β π = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), πΎβ©, β¨(compβndx), πβ©}) | ||
Theorem | xpcbas 18130 | Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π = (BaseβπΆ) & β’ π = (Baseβπ·) β β’ (π Γ π) = (Baseβπ) | ||
Theorem | xpchomfval 18131* | Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ πΎ = (Hom βπ) β β’ πΎ = (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£)))) | ||
Theorem | xpchom 18132 | Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ πΎ = (Hom βπ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΎπ) = (((1st βπ)π»(1st βπ)) Γ ((2nd βπ)π½(2nd βπ)))) | ||
Theorem | relxpchom 18133 | A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ πΎ = (Hom βπ) β β’ Rel (ππΎπ) | ||
Theorem | xpccofval 18134* | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) (Proof shortened by AV, 2-Mar-2024.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ πΎ = (Hom βπ) & β’ Β· = (compβπΆ) & β’ β = (compβπ·) & β’ π = (compβπ) β β’ π = (π₯ β (π΅ Γ π΅), π¦ β π΅ β¦ (π β ((2nd βπ₯)πΎπ¦), π β (πΎβπ₯) β¦ β¨((1st βπ)(β¨(1st β(1st βπ₯)), (1st β(2nd βπ₯))β© Β· (1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd β(1st βπ₯)), (2nd β(2nd βπ₯))β© β (2nd βπ¦))(2nd βπ))β©)) | ||
Theorem | xpcco 18135 | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ πΎ = (Hom βπ) & β’ Β· = (compβπΆ) & β’ β = (compβπ·) & β’ π = (compβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΎπ)) & β’ (π β πΊ β (ππΎπ)) β β’ (π β (πΊ(β¨π, πβ©ππ)πΉ) = β¨((1st βπΊ)(β¨(1st βπ), (1st βπ)β© Β· (1st βπ))(1st βπΉ)), ((2nd βπΊ)(β¨(2nd βπ), (2nd βπ)β© β (2nd βπ))(2nd βπΉ))β©) | ||
Theorem | xpcco1st 18136 | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ πΎ = (Hom βπ) & β’ π = (compβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΎπ)) & β’ (π β πΊ β (ππΎπ)) & β’ Β· = (compβπΆ) β β’ (π β (1st β(πΊ(β¨π, πβ©ππ)πΉ)) = ((1st βπΊ)(β¨(1st βπ), (1st βπ)β© Β· (1st βπ))(1st βπΉ))) | ||
Theorem | xpcco2nd 18137 | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ πΎ = (Hom βπ) & β’ π = (compβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΎπ)) & β’ (π β πΊ β (ππΎπ)) & β’ Β· = (compβπ·) β β’ (π β (2nd β(πΊ(β¨π, πβ©ππ)πΉ)) = ((2nd βπΊ)(β¨(2nd βπ), (2nd βπ)β© Β· (2nd βπ))(2nd βπΉ))) | ||
Theorem | xpchom2 18138 | Value of the set of morphisms in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π = (BaseβπΆ) & β’ π = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ πΎ = (Hom βπ) β β’ (π β (β¨π, πβ©πΎβ¨π, πβ©) = ((ππ»π) Γ (ππ½π))) | ||
Theorem | xpcco2 18139 | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π = (BaseβπΆ) & β’ π = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ Β· = (compβπΆ) & β’ β = (compβπ·) & β’ π = (compβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΉ β (ππ»π)) & β’ (π β πΊ β (ππ½π)) & β’ (π β πΎ β (ππ»π )) & β’ (π β πΏ β (ππ½π)) β β’ (π β (β¨πΎ, πΏβ©(β¨β¨π, πβ©, β¨π, πβ©β©πβ¨π , πβ©)β¨πΉ, πΊβ©) = β¨(πΎ(β¨π, πβ© Β· π )πΉ), (πΏ(β¨π, πβ© β π)πΊ)β©) | ||
Theorem | xpccatid 18140* | The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (BaseβπΆ) & β’ π = (Baseβπ·) & β’ πΌ = (IdβπΆ) & β’ π½ = (Idβπ·) β β’ (π β (π β Cat β§ (Idβπ) = (π₯ β π, π¦ β π β¦ β¨(πΌβπ₯), (π½βπ¦)β©))) | ||
Theorem | xpcid 18141 | The identity morphism in the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (BaseβπΆ) & β’ π = (Baseβπ·) & β’ πΌ = (IdβπΆ) & β’ π½ = (Idβπ·) & β’ 1 = (Idβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ( 1 ββ¨π , πβ©) = β¨(πΌβπ ), (π½βπ)β©) | ||
Theorem | xpccat 18142 | The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β π β Cat) | ||
Theorem | 1stfval 18143* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ π» = (Hom βπ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ 1stF π·) β β’ (π β π = β¨(1st βΎ π΅), (π₯ β π΅, π¦ β π΅ β¦ (1st βΎ (π₯π»π¦)))β©) | ||
Theorem | 1stf1 18144 | Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ π» = (Hom βπ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ 1stF π·) & β’ (π β π β π΅) β β’ (π β ((1st βπ)βπ ) = (1st βπ )) | ||
Theorem | 1stf2 18145 | Value of the first projection on a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ π» = (Hom βπ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ 1stF π·) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π (2nd βπ)π) = (1st βΎ (π π»π))) | ||
Theorem | 2ndfval 18146* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ π» = (Hom βπ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ 2ndF π·) β β’ (π β π = β¨(2nd βΎ π΅), (π₯ β π΅, π¦ β π΅ β¦ (2nd βΎ (π₯π»π¦)))β©) | ||
Theorem | 2ndf1 18147 | Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ π» = (Hom βπ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ 2ndF π·) & β’ (π β π β π΅) β β’ (π β ((1st βπ)βπ ) = (2nd βπ )) | ||
Theorem | 2ndf2 18148 | Value of the first projection on a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ π» = (Hom βπ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ 2ndF π·) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π (2nd βπ)π) = (2nd βΎ (π π»π))) | ||
Theorem | 1stfcl 18149 | The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ 1stF π·) β β’ (π β π β (π Func πΆ)) | ||
Theorem | 2ndfcl 18150 | The second projection functor is a functor onto the right argument. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ 2ndF π·) β β’ (π β π β (π Func π·)) | ||
Theorem | prfval 18151* | Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) β β’ (π β π = β¨(π₯ β π΅ β¦ β¨((1st βπΉ)βπ₯), ((1st βπΊ)βπ₯)β©), (π₯ β π΅, π¦ β π΅ β¦ (β β (π₯π»π¦) β¦ β¨((π₯(2nd βπΉ)π¦)ββ), ((π₯(2nd βπΊ)π¦)ββ)β©))β©) | ||
Theorem | prf1 18152 | Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) & β’ (π β π β π΅) β β’ (π β ((1st βπ)βπ) = β¨((1st βπΉ)βπ), ((1st βπΊ)βπ)β©) | ||
Theorem | prf2fval 18153* | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π(2nd βπ)π) = (β β (ππ»π) β¦ β¨((π(2nd βπΉ)π)ββ), ((π(2nd βπΊ)π)ββ)β©)) | ||
Theorem | prf2 18154 | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΎ β (ππ»π)) β β’ (π β ((π(2nd βπ)π)βπΎ) = β¨((π(2nd βπΉ)π)βπΎ), ((π(2nd βπΊ)π)βπΎ)β©) | ||
Theorem | prfcl 18155 | The pairing of functors πΉ:πΆβΆπ· and πΊ:πΆβΆπ· is a functor β¨πΉ, πΊβ©:πΆβΆ(π· Γ πΈ). (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ π = (π· Γc πΈ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) β β’ (π β π β (πΆ Func π)) | ||
Theorem | prf1st 18156 | Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) β β’ (π β ((π· 1stF πΈ) βfunc π) = πΉ) | ||
Theorem | prf2nd 18157 | Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) β β’ (π β ((π· 2ndF πΈ) βfunc π) = πΊ) | ||
Theorem | 1st2ndprf 18158 | Break a functor into a product category into first and second projections. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (π· Γc πΈ) & β’ (π β πΉ β (πΆ Func π)) & β’ (π β π· β Cat) & β’ (π β πΈ β Cat) β β’ (π β πΉ = (((π· 1stF πΈ) βfunc πΉ) β¨,β©F ((π· 2ndF πΈ) βfunc πΉ))) | ||
Theorem | catcxpccl 18159 | The category of categories for a weak universe is closed under the product category operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ π = (π Γc π) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β π β π΅) | ||
Theorem | catcxpcclOLD 18160 | Obsolete proof of catcxpccl 18159 as of 14-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΆ = (CatCatβπ) & β’ π΅ = (BaseβπΆ) & β’ π = (π Γc π) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β π β π΅) | ||
Theorem | xpcpropd 18161 | If two categories have the same set of objects, morphisms, and compositions, then they have the same product category. (Contributed by Mario Carneiro, 17-Jan-2017.) |
β’ (π β (Homf βπ΄) = (Homf βπ΅)) & β’ (π β (compfβπ΄) = (compfβπ΅)) & β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (π΄ Γc πΆ) = (π΅ Γc π·)) | ||
Syntax | cevlf 18162 | Extend class notation with the evaluation functor. |
class evalF | ||
Syntax | ccurf 18163 | Extend class notation with the currying of a functor. |
class curryF | ||
Syntax | cuncf 18164 | Extend class notation with the uncurrying of a functor. |
class uncurryF | ||
Syntax | cdiag 18165 | Extend class notation to include the diagonal functor. |
class Ξfunc | ||
Definition | df-evlf 18166* | Define the evaluation functor, which is the extension of the evaluation map π, π₯ β¦ (πβπ₯) of functors, to a functor (πΆβΆπ·) Γ πΆβΆπ·. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ evalF = (π β Cat, π β Cat β¦ β¨(π β (π Func π), π₯ β (Baseβπ) β¦ ((1st βπ)βπ₯)), (π₯ β ((π Func π) Γ (Baseβπ)), π¦ β ((π Func π) Γ (Baseβπ)) β¦ β¦(1st βπ₯) / πβ¦β¦(1st βπ¦) / πβ¦(π β (π(π Nat π)π), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st βπ)β(2nd βπ₯)), ((1st βπ)β(2nd βπ¦))β©(compβπ)((1st βπ)β(2nd βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))))β©) | ||
Definition | df-curf 18167* | Define the curry functor, which maps a functor πΉ:πΆ Γ π·βΆπΈ to curryF (πΉ):πΆβΆ(π·βΆπΈ). (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ curryF = (π β V, π β V β¦ β¦(1st βπ) / πβ¦β¦(2nd βπ) / πβ¦β¨(π₯ β (Baseβπ) β¦ β¨(π¦ β (Baseβπ) β¦ (π₯(1st βπ)π¦)), (π¦ β (Baseβπ), π§ β (Baseβπ) β¦ (π β (π¦(Hom βπ)π§) β¦ (((Idβπ)βπ₯)(β¨π₯, π¦β©(2nd βπ)β¨π₯, π§β©)π)))β©), (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π β (π₯(Hom βπ)π¦) β¦ (π§ β (Baseβπ) β¦ (π(β¨π₯, π§β©(2nd βπ)β¨π¦, π§β©)((Idβπ)βπ§)))))β©) | ||
Definition | df-uncf 18168* | Define the uncurry functor, which can be defined equationally using evalF. Strictly speaking, the third category argument is not needed, since the resulting functor is extensionally equal regardless, but it is used in the equational definition and is too much work to remove. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ uncurryF = (π β V, π β V β¦ (((πβ1) evalF (πβ2)) βfunc ((π βfunc ((πβ0) 1stF (πβ1))) β¨,β©F ((πβ0) 2ndF (πβ1))))) | ||
Definition | df-diag 18169* | Define the diagonal functor, which is the functor πΆβΆ(π· Func πΆ) whose object part is π₯ β πΆ β¦ (π¦ β π· β¦ π₯). The value of the functor at an object π₯ is the constant functor which maps all objects in π· to π₯ and all morphisms to 1(π₯). The morphism part is a natural transformation between these functors, which takes π:π₯βΆπ¦ to the natural transformation with every component equal to π. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ Ξfunc = (π β Cat, π β Cat β¦ (β¨π, πβ© curryF (π 1stF π))) | ||
Theorem | evlfval 18170* | Value of the evaluation functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΈ = (πΆ evalF π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπ·) & β’ π = (πΆ Nat π·) β β’ (π β πΈ = β¨(π β (πΆ Func π·), π₯ β π΅ β¦ ((1st βπ)βπ₯)), (π₯ β ((πΆ Func π·) Γ π΅), π¦ β ((πΆ Func π·) Γ π΅) β¦ β¦(1st βπ₯) / πβ¦β¦(1st βπ¦) / πβ¦(π β (πππ), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st βπ)β(2nd βπ₯)), ((1st βπ)β(2nd βπ¦))β© Β· ((1st βπ)β(2nd βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))))β©) | ||
Theorem | evlf2 18171* | Value of the evaluation functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΈ = (πΆ evalF π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπ·) & β’ π = (πΆ Nat π·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΏ = (β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©) β β’ (π β πΏ = (π β (πΉππΊ), π β (ππ»π) β¦ ((πβπ)(β¨((1st βπΉ)βπ), ((1st βπΉ)βπ)β© Β· ((1st βπΊ)βπ))((π(2nd βπΉ)π)βπ)))) | ||
Theorem | evlf2val 18172 | Value of the evaluation natural transformation at an object. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΈ = (πΆ evalF π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπ·) & β’ π = (πΆ Nat π·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΏ = (β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©) & β’ (π β π΄ β (πΉππΊ)) & β’ (π β πΎ β (ππ»π)) β β’ (π β (π΄πΏπΎ) = ((π΄βπ)(β¨((1st βπΉ)βπ), ((1st βπΉ)βπ)β© Β· ((1st βπΊ)βπ))((π(2nd βπΉ)π)βπΎ))) | ||
Theorem | evlf1 18173 | Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΈ = (πΆ evalF π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π΅ = (BaseβπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β π β π΅) β β’ (π β (πΉ(1st βπΈ)π) = ((1st βπΉ)βπ)) | ||
Theorem | evlfcllem 18174 | Lemma for evlfcl 18175. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΈ = (πΆ evalF π·) & β’ π = (πΆ FuncCat π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ Nat π·) & β’ (π β (πΉ β (πΆ Func π·) β§ π β (BaseβπΆ))) & β’ (π β (πΊ β (πΆ Func π·) β§ π β (BaseβπΆ))) & β’ (π β (π» β (πΆ Func π·) β§ π β (BaseβπΆ))) & β’ (π β (π΄ β (πΉππΊ) β§ πΎ β (π(Hom βπΆ)π))) & β’ (π β (π΅ β (πΊππ») β§ πΏ β (π(Hom βπΆ)π))) β β’ (π β ((β¨πΉ, πβ©(2nd βπΈ)β¨π», πβ©)β(β¨π΅, πΏβ©(β¨β¨πΉ, πβ©, β¨πΊ, πβ©β©(compβ(π Γc πΆ))β¨π», πβ©)β¨π΄, πΎβ©)) = (((β¨πΊ, πβ©(2nd βπΈ)β¨π», πβ©)ββ¨π΅, πΏβ©)(β¨((1st βπΈ)ββ¨πΉ, πβ©), ((1st βπΈ)ββ¨πΊ, πβ©)β©(compβπ·)((1st βπΈ)ββ¨π», πβ©))((β¨πΉ, πβ©(2nd βπΈ)β¨πΊ, πβ©)ββ¨π΄, πΎβ©))) | ||
Theorem | evlfcl 18175 | The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors πΆβΆπ·, and the second parameter in π·. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΈ = (πΆ evalF π·) & β’ π = (πΆ FuncCat π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β πΈ β ((π Γc πΆ) Func π·)) | ||
Theorem | curfval 18176* | Value of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ π΄ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) & β’ π΅ = (Baseβπ·) & β’ π½ = (Hom βπ·) & β’ 1 = (IdβπΆ) & β’ π» = (Hom βπΆ) & β’ πΌ = (Idβπ·) β β’ (π β πΊ = β¨(π₯ β π΄ β¦ β¨(π¦ β π΅ β¦ (π₯(1st βπΉ)π¦)), (π¦ β π΅, π§ β π΅ β¦ (π β (π¦π½π§) β¦ (( 1 βπ₯)(β¨π₯, π¦β©(2nd βπΉ)β¨π₯, π§β©)π)))β©), (π₯ β π΄, π¦ β π΄ β¦ (π β (π₯π»π¦) β¦ (π§ β π΅ β¦ (π(β¨π₯, π§β©(2nd βπΉ)β¨π¦, π§β©)(πΌβπ§)))))β©) | ||
Theorem | curf1fval 18177* | Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ π΄ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) & β’ π΅ = (Baseβπ·) & β’ π½ = (Hom βπ·) & β’ 1 = (IdβπΆ) β β’ (π β (1st βπΊ) = (π₯ β π΄ β¦ β¨(π¦ β π΅ β¦ (π₯(1st βπΉ)π¦)), (π¦ β π΅, π§ β π΅ β¦ (π β (π¦π½π§) β¦ (( 1 βπ₯)(β¨π₯, π¦β©(2nd βπΉ)β¨π₯, π§β©)π)))β©)) | ||
Theorem | curf1 18178* | Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ π΄ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) & β’ π΅ = (Baseβπ·) & β’ (π β π β π΄) & β’ πΎ = ((1st βπΊ)βπ) & β’ π½ = (Hom βπ·) & β’ 1 = (IdβπΆ) β β’ (π β πΎ = β¨(π¦ β π΅ β¦ (π(1st βπΉ)π¦)), (π¦ β π΅, π§ β π΅ β¦ (π β (π¦π½π§) β¦ (( 1 βπ)(β¨π, π¦β©(2nd βπΉ)β¨π, π§β©)π)))β©) | ||
Theorem | curf11 18179 | Value of the double evaluated curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ π΄ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) & β’ π΅ = (Baseβπ·) & β’ (π β π β π΄) & β’ πΎ = ((1st βπΊ)βπ) & β’ (π β π β π΅) β β’ (π β ((1st βπΎ)βπ) = (π(1st βπΉ)π)) | ||
Theorem | curf12 18180 | The partially evaluated curry functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ π΄ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) & β’ π΅ = (Baseβπ·) & β’ (π β π β π΄) & β’ πΎ = ((1st βπΊ)βπ) & β’ (π β π β π΅) & β’ π½ = (Hom βπ·) & β’ 1 = (IdβπΆ) & β’ (π β π β π΅) & β’ (π β π» β (ππ½π)) β β’ (π β ((π(2nd βπΎ)π)βπ») = (( 1 βπ)(β¨π, πβ©(2nd βπΉ)β¨π, πβ©)π»)) | ||
Theorem | curf1cl 18181 | The partially evaluated curry functor is a functor. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ π΄ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) & β’ π΅ = (Baseβπ·) & β’ (π β π β π΄) & β’ πΎ = ((1st βπΊ)βπ) β β’ (π β πΎ β (π· Func πΈ)) | ||
Theorem | curf2 18182* | Value of the curry functor at a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ π΄ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) & β’ π΅ = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ πΌ = (Idβπ·) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β πΎ β (ππ»π)) & β’ πΏ = ((π(2nd βπΊ)π)βπΎ) β β’ (π β πΏ = (π§ β π΅ β¦ (πΎ(β¨π, π§β©(2nd βπΉ)β¨π, π§β©)(πΌβπ§)))) | ||
Theorem | curf2val 18183 | Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ π΄ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) & β’ π΅ = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ πΌ = (Idβπ·) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β πΎ β (ππ»π)) & β’ πΏ = ((π(2nd βπΊ)π)βπΎ) & β’ (π β π β π΅) β β’ (π β (πΏβπ) = (πΎ(β¨π, πβ©(2nd βπΉ)β¨π, πβ©)(πΌβπ))) | ||
Theorem | curf2cl 18184 | The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ π΄ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) & β’ π΅ = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ πΌ = (Idβπ·) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β πΎ β (ππ»π)) & β’ πΏ = ((π(2nd βπΊ)π)βπΎ) & β’ π = (π· Nat πΈ) β β’ (π β πΏ β (((1st βπΊ)βπ)π((1st βπΊ)βπ))) | ||
Theorem | curfcl 18185 | The curry functor of a functor πΉ:πΆ Γ π·βΆπΈ is a functor curryF (πΉ):πΆβΆ(π·βΆπΈ). (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ π = (π· FuncCat πΈ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) β β’ (π β πΊ β (πΆ Func π)) | ||
Theorem | curfpropd 18186 | If two categories have the same set of objects, morphisms, and compositions, then they curry the same functor to the same result. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ (π β (Homf βπ΄) = (Homf βπ΅)) & β’ (π β (compfβπ΄) = (compfβπ΅)) & β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β π΄ β Cat) & β’ (π β π΅ β Cat) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((π΄ Γc πΆ) Func πΈ)) β β’ (π β (β¨π΄, πΆβ© curryF πΉ) = (β¨π΅, π·β© curryF πΉ)) | ||
Theorem | uncfval 18187 | Value of the uncurry functor, which is the reverse of the curry functor, taking πΊ:πΆβΆ(π·βΆπΈ) to uncurryF (πΊ):πΆ Γ π·βΆπΈ. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΉ = (β¨βπΆπ·πΈββ© uncurryF πΊ) & β’ (π β π· β Cat) & β’ (π β πΈ β Cat) & β’ (π β πΊ β (πΆ Func (π· FuncCat πΈ))) β β’ (π β πΉ = ((π· evalF πΈ) βfunc ((πΊ βfunc (πΆ 1stF π·)) β¨,β©F (πΆ 2ndF π·)))) | ||
Theorem | uncfcl 18188 | The uncurry operation takes a functor πΉ:πΆβΆ(π·βΆπΈ) to a functor uncurryF (πΉ):πΆ Γ π·βΆπΈ. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΉ = (β¨βπΆπ·πΈββ© uncurryF πΊ) & β’ (π β π· β Cat) & β’ (π β πΈ β Cat) & β’ (π β πΊ β (πΆ Func (π· FuncCat πΈ))) β β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) | ||
Theorem | uncf1 18189 | Value of the uncurry functor on an object. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΉ = (β¨βπΆπ·πΈββ© uncurryF πΊ) & β’ (π β π· β Cat) & β’ (π β πΈ β Cat) & β’ (π β πΊ β (πΆ Func (π· FuncCat πΈ))) & β’ π΄ = (BaseβπΆ) & β’ π΅ = (Baseβπ·) & β’ (π β π β π΄) & β’ (π β π β π΅) β β’ (π β (π(1st βπΉ)π) = ((1st β((1st βπΊ)βπ))βπ)) | ||
Theorem | uncf2 18190 | Value of the uncurry functor on a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΉ = (β¨βπΆπ·πΈββ© uncurryF πΊ) & β’ (π β π· β Cat) & β’ (π β πΈ β Cat) & β’ (π β πΊ β (πΆ Func (π· FuncCat πΈ))) & β’ π΄ = (BaseβπΆ) & β’ π΅ = (Baseβπ·) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ (π β π β (ππ»π)) & β’ (π β π β (ππ½π)) β β’ (π β (π (β¨π, πβ©(2nd βπΉ)β¨π, πβ©)π) = ((((π(2nd βπΊ)π)βπ )βπ)(β¨((1st β((1st βπΊ)βπ))βπ), ((1st β((1st βπΊ)βπ))βπ)β©(compβπΈ)((1st β((1st βπΊ)βπ))βπ))((π(2nd β((1st βπΊ)βπ))π)βπ))) | ||
Theorem | curfuncf 18191 | Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΉ = (β¨βπΆπ·πΈββ© uncurryF πΊ) & β’ (π β π· β Cat) & β’ (π β πΈ β Cat) & β’ (π β πΊ β (πΆ Func (π· FuncCat πΈ))) β β’ (π β (β¨πΆ, π·β© curryF πΉ) = πΊ) | ||
Theorem | uncfcurf 18192 | Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) β β’ (π β (β¨βπΆπ·πΈββ© uncurryF πΊ) = πΉ) | ||
Theorem | diagval 18193 | Define the diagonal functor, which is the functor πΆβΆ(π· Func πΆ) whose object part is π₯ β πΆ β¦ (π¦ β π· β¦ π₯). We can define this equationally as the currying of the first projection functor, and by expressing it this way we get a quick proof of functoriality. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β πΏ = (β¨πΆ, π·β© curryF (πΆ 1stF π·))) | ||
Theorem | diagcl 18194 | The diagonal functor is a functor from the base category to the functor category. Another way of saying this is that the constant functor (π¦ β π· β¦ π) is a construction that is natural in π (and covariant). (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (π· FuncCat πΆ) β β’ (π β πΏ β (πΆ Func π)) | ||
Theorem | diag1cl 18195 | The constant functor of π is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π΄ = (BaseβπΆ) & β’ (π β π β π΄) & β’ πΎ = ((1st βπΏ)βπ) β β’ (π β πΎ β (π· Func πΆ)) | ||
Theorem | diag11 18196 | Value of the constant functor at an object. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π΄ = (BaseβπΆ) & β’ (π β π β π΄) & β’ πΎ = ((1st βπΏ)βπ) & β’ π΅ = (Baseβπ·) & β’ (π β π β π΅) β β’ (π β ((1st βπΎ)βπ) = π) | ||
Theorem | diag12 18197 | Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π΄ = (BaseβπΆ) & β’ (π β π β π΄) & β’ πΎ = ((1st βπΏ)βπ) & β’ π΅ = (Baseβπ·) & β’ (π β π β π΅) & β’ π½ = (Hom βπ·) & β’ 1 = (IdβπΆ) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ½π)) β β’ (π β ((π(2nd βπΎ)π)βπΉ) = ( 1 βπ)) | ||
Theorem | diag2 18198 | Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ π΄ = (BaseβπΆ) & β’ π΅ = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β πΉ β (ππ»π)) β β’ (π β ((π(2nd βπΏ)π)βπΉ) = (π΅ Γ {πΉ})) | ||
Theorem | diag2cl 18199 | The diagonal functor at a morphism is a natural transformation between constant functors. (Contributed by Mario Carneiro, 7-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ π΄ = (BaseβπΆ) & β’ π΅ = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β πΉ β (ππ»π)) & β’ π = (π· Nat πΆ) β β’ (π β (π΅ Γ {πΉ}) β (((1st βπΏ)βπ)π((1st βπΏ)βπ))) | ||
Theorem | curf2ndf 18200 | As shown in diagval 18193, the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is π₯ β πΆ β¦ (π¦ β π· β¦ π¦), which is a constant functor of the identity functor at π·. (Contributed by Mario Carneiro, 15-Jan-2017.) |
β’ π = (π· FuncCat π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β (β¨πΆ, π·β© curryF (πΆ 2ndF π·)) = ((1st β(πΞfuncπΆ))β(idfuncβπ·))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |