![]() |
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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fthestrcsetc 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 is faithful. (Contributed by AV, 2-Apr-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ (π β πΉ(πΈ Faith π)πΊ) | ||
Theorem | fullestrcsetc 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 full. (Contributed by AV, 2-Apr-2020.) |
β’ πΈ = (ExtStrCatβπ) & β’ π = (SetCatβπ) & β’ π΅ = (BaseβπΈ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm (Baseβπ₯))))) β β’ (π β πΉ(πΈ Full π)πΊ) | ||
Theorem | equivestrcsetc 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 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 18104 | 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 18105* | Lemma 1 for funcsetcestrc 18115. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) β β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) | ||
Theorem | funcsetcestrclem2 18106* | Lemma 2 for funcsetcestrc 18115. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) β β’ ((π β§ π β πΆ) β (πΉβπ) β π) | ||
Theorem | funcsetcestrclem3 18107* | Lemma 3 for funcsetcestrc 18115. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ πΈ = (ExtStrCatβπ) & β’ π΅ = (BaseβπΈ) β β’ (π β πΉ:πΆβΆπ΅) | ||
Theorem | embedsetcestrclem 18108* | Lemma for embedsetcestrc 18118. (Contributed by AV, 31-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ πΈ = (ExtStrCatβπ) & β’ π΅ = (BaseβπΈ) β β’ (π β πΉ:πΆβ1-1βπ΅) | ||
Theorem | funcsetcestrclem4 18109* | Lemma 4 for funcsetcestrc 18115. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) β β’ (π β πΊ Fn (πΆ Γ πΆ)) | ||
Theorem | funcsetcestrclem5 18110* | Lemma 5 for funcsetcestrc 18115. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) β β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ) = ( I βΎ (π βm π))) | ||
Theorem | funcsetcestrclem6 18111* | Lemma 6 for funcsetcestrc 18115. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) β β’ ((π β§ (π β πΆ β§ π β πΆ) β§ π» β (π βm π)) β ((ππΊπ)βπ») = π») | ||
Theorem | funcsetcestrclem7 18112* | Lemma 7 for funcsetcestrc 18115. (Contributed by AV, 27-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ ((π β§ π β πΆ) β ((ππΊπ)β((Idβπ)βπ)) = ((IdβπΈ)β(πΉβπ))) | ||
Theorem | funcsetcestrclem8 18113* | Lemma 8 for funcsetcestrc 18115. (Contributed by AV, 28-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ):(π(Hom βπ)π)βΆ((πΉβπ)(Hom βπΈ)(πΉβπ))) | ||
Theorem | funcsetcestrclem9 18114* | Lemma 9 for funcsetcestrc 18115. (Contributed by AV, 28-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ) β§ (π» β (π(Hom βπ)π) β§ πΎ β (π(Hom βπ)π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»))) | ||
Theorem | funcsetcestrc 18115* | 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 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 is faithful. (Contributed by AV, 31-Mar-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ (π β πΉ(π Faith πΈ)πΊ) | ||
Theorem | fullsetcestrc 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 full. (Contributed by AV, 1-Apr-2020.) |
β’ π = (SetCatβπ) & β’ πΆ = (Baseβπ) & β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) & β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) & β’ πΈ = (ExtStrCatβπ) β β’ (π β πΉ(π Full πΈ)πΊ) | ||
Theorem | embedsetcestrc 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 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 18119 | Extend class notation with the product of two categories. |
class Γc | ||
Syntax | c1stf 18120 | Extend class notation with the first projection functor. |
class 1stF | ||
Syntax | c2ndf 18121 | Extend class notation with the second projection functor. |
class 2ndF | ||
Syntax | cprf 18122 | Extend class notation with the functor pairing operation. |
class β¨,β©F | ||
Definition | df-xpc 18123* | 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 18124* | 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 18125* | 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 18126* | 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 18127 | The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.) |
β’ Γc Fn (V Γ V) | ||
Theorem | xpcval 18128* | 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 18129 | Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π = (BaseβπΆ) & β’ π = (Baseβπ·) β β’ (π Γ π) = (Baseβπ) | ||
Theorem | xpchomfval 18130* | 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 18131 | 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 18132 | A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ πΎ = (Hom βπ) β β’ Rel (ππΎπ) | ||
Theorem | xpccofval 18133* | 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 18134 | 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 18135 | 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 18136 | 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 18137 | 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 18138 | 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 18139* | 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 18140 | 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 18141 | The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β π β Cat) | ||
Theorem | 1stfval 18142* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ π» = (Hom βπ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ 1stF π·) β β’ (π β π = β¨(1st βΎ π΅), (π₯ β π΅, π¦ β π΅ β¦ (1st βΎ (π₯π»π¦)))β©) | ||
Theorem | 1stf1 18143 | 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 18144 | 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 18145* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π = (πΆ Γc π·) & β’ π΅ = (Baseβπ) & β’ π» = (Hom βπ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π = (πΆ 2ndF π·) β β’ (π β π = β¨(2nd βΎ π΅), (π₯ β π΅, π¦ β π΅ β¦ (2nd βΎ (π₯π»π¦)))β©) | ||
Theorem | 2ndf1 18146 | 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 18147 | 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 18148 | 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 18149 | 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 18150* | Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) β β’ (π β π = β¨(π₯ β π΅ β¦ β¨((1st βπΉ)βπ₯), ((1st βπΊ)βπ₯)β©), (π₯ β π΅, π¦ β π΅ β¦ (β β (π₯π»π¦) β¦ β¨((π₯(2nd βπΉ)π¦)ββ), ((π₯(2nd βπΊ)π¦)ββ)β©))β©) | ||
Theorem | prf1 18151 | Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) & β’ (π β π β π΅) β β’ (π β ((1st βπ)βπ) = β¨((1st βπΉ)βπ), ((1st βπΊ)βπ)β©) | ||
Theorem | prf2fval 18152* | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π(2nd βπ)π) = (β β (ππ»π) β¦ β¨((π(2nd βπΉ)π)ββ), ((π(2nd βπΊ)π)ββ)β©)) | ||
Theorem | prf2 18153 | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΎ β (ππ»π)) β β’ (π β ((π(2nd βπ)π)βπΎ) = β¨((π(2nd βπΉ)π)βπΎ), ((π(2nd βπΊ)π)βπΎ)β©) | ||
Theorem | prfcl 18154 | The pairing of functors πΉ:πΆβΆπ· and πΊ:πΆβΆπ· is a functor β¨πΉ, πΊβ©:πΆβΆ(π· Γ πΈ). (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ π = (π· Γc πΈ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) β β’ (π β π β (πΆ Func π)) | ||
Theorem | prf1st 18155 | Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) β β’ (π β ((π· 1stF πΈ) βfunc π) = πΉ) | ||
Theorem | prf2nd 18156 | Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΉ β¨,β©F πΊ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func πΈ)) β β’ (π β ((π· 2ndF πΈ) βfunc π) = πΊ) | ||
Theorem | 1st2ndprf 18157 | 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 18158 | 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 18159 | Obsolete proof of catcxpccl 18158 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 18160 | 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 18161 | Extend class notation with the evaluation functor. |
class evalF | ||
Syntax | ccurf 18162 | Extend class notation with the currying of a functor. |
class curryF | ||
Syntax | cuncf 18163 | Extend class notation with the uncurrying of a functor. |
class uncurryF | ||
Syntax | cdiag 18164 | Extend class notation to include the diagonal functor. |
class Ξfunc | ||
Definition | df-evlf 18165* | 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 18166* | 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 18167* | 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 18168* | 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 18169* | 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 18170* | 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 18171 | 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 18172 | Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ πΈ = (πΆ evalF π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ π΅ = (BaseβπΆ) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β π β π΅) β β’ (π β (πΉ(1st βπΈ)π) = ((1st βπΉ)βπ)) | ||
Theorem | evlfcllem 18173 | Lemma for evlfcl 18174. (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 18174 | 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 18175* | 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 18176* | 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 18177* | 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 18178 | 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 18179 | 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 18180 | 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 18181* | 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 18182 | 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 18183 | 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 18184 | 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 18185 | 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 18186 | 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 18187 | 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 18188 | 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 18189 | 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 18190 | Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΉ = (β¨βπΆπ·πΈββ© uncurryF πΊ) & β’ (π β π· β Cat) & β’ (π β πΈ β Cat) & β’ (π β πΊ β (πΆ Func (π· FuncCat πΈ))) β β’ (π β (β¨πΆ, π·β© curryF πΉ) = πΊ) | ||
Theorem | uncfcurf 18191 | Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
β’ πΊ = (β¨πΆ, π·β© curryF πΉ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β πΉ β ((πΆ Γc π·) Func πΈ)) β β’ (π β (β¨βπΆπ·πΈββ© uncurryF πΊ) = πΉ) | ||
Theorem | diagval 18192 | 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 18193 | 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 18194 | 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 18195 | 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 18196 | 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 18197 | Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.) |
β’ πΏ = (πΆΞfuncπ·) & β’ π΄ = (BaseβπΆ) & β’ π΅ = (Baseβπ·) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β πΉ β (ππ»π)) β β’ (π β ((π(2nd βπΏ)π)βπΉ) = (π΅ Γ {πΉ})) | ||
Theorem | diag2cl 18198 | 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 18199 | As shown in diagval 18192, 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βπ·))) | ||
Syntax | chof 18200 | Extend class notation with the Hom functor. |
class HomF |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |