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