Home | Metamath
Proof Explorer Theorem List (p. 181 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xpcbas 18001 | Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.) |
โข ๐ = (๐ถ รc ๐ท) & โข ๐ = (Baseโ๐ถ) & โข ๐ = (Baseโ๐ท) โ โข (๐ ร ๐) = (Baseโ๐) | ||
Theorem | xpchomfval 18002* | 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 18003 | 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 18004 | A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
โข ๐ = (๐ถ รc ๐ท) & โข ๐พ = (Hom โ๐) โ โข Rel (๐๐พ๐) | ||
Theorem | xpccofval 18005* | 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 18006 | 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 18007 | 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 18008 | 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 18009 | 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 18010 | 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 18011* | 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 18012 | 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 18013 | The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.) |
โข ๐ = (๐ถ รc ๐ท) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ท โ Cat) โ โข (๐ โ ๐ โ Cat) | ||
Theorem | 1stfval 18014* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
โข ๐ = (๐ถ รc ๐ท) & โข ๐ต = (Baseโ๐) & โข ๐ป = (Hom โ๐) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ท โ Cat) & โข ๐ = (๐ถ 1stF ๐ท) โ โข (๐ โ ๐ = โจ(1st โพ ๐ต), (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ (1st โพ (๐ฅ๐ป๐ฆ)))โฉ) | ||
Theorem | 1stf1 18015 | 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 18016 | 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 18017* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
โข ๐ = (๐ถ รc ๐ท) & โข ๐ต = (Baseโ๐) & โข ๐ป = (Hom โ๐) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ท โ Cat) & โข ๐ = (๐ถ 2ndF ๐ท) โ โข (๐ โ ๐ = โจ(2nd โพ ๐ต), (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ (2nd โพ (๐ฅ๐ป๐ฆ)))โฉ) | ||
Theorem | 2ndf1 18018 | 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 18019 | 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 18020 | 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 18021 | 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 18022* | Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
โข ๐ = (๐น โจ,โฉF ๐บ) & โข ๐ต = (Baseโ๐ถ) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐น โ (๐ถ Func ๐ท)) & โข (๐ โ ๐บ โ (๐ถ Func ๐ธ)) โ โข (๐ โ ๐ = โจ(๐ฅ โ ๐ต โฆ โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ), (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ (โ โ (๐ฅ๐ป๐ฆ) โฆ โจ((๐ฅ(2nd โ๐น)๐ฆ)โโ), ((๐ฅ(2nd โ๐บ)๐ฆ)โโ)โฉ))โฉ) | ||
Theorem | prf1 18023 | Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.) |
โข ๐ = (๐น โจ,โฉF ๐บ) & โข ๐ต = (Baseโ๐ถ) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐น โ (๐ถ Func ๐ท)) & โข (๐ โ ๐บ โ (๐ถ Func ๐ธ)) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((1st โ๐)โ๐) = โจ((1st โ๐น)โ๐), ((1st โ๐บ)โ๐)โฉ) | ||
Theorem | prf2fval 18024* | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
โข ๐ = (๐น โจ,โฉF ๐บ) & โข ๐ต = (Baseโ๐ถ) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐น โ (๐ถ Func ๐ท)) & โข (๐ โ ๐บ โ (๐ถ Func ๐ธ)) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐(2nd โ๐)๐) = (โ โ (๐๐ป๐) โฆ โจ((๐(2nd โ๐น)๐)โโ), ((๐(2nd โ๐บ)๐)โโ)โฉ)) | ||
Theorem | prf2 18025 | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
โข ๐ = (๐น โจ,โฉF ๐บ) & โข ๐ต = (Baseโ๐ถ) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐น โ (๐ถ Func ๐ท)) & โข (๐ โ ๐บ โ (๐ถ Func ๐ธ)) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐พ โ (๐๐ป๐)) โ โข (๐ โ ((๐(2nd โ๐)๐)โ๐พ) = โจ((๐(2nd โ๐น)๐)โ๐พ), ((๐(2nd โ๐บ)๐)โ๐พ)โฉ) | ||
Theorem | prfcl 18026 | The pairing of functors ๐น:๐ถโถ๐ท and ๐บ:๐ถโถ๐ท is a functor โจ๐น, ๐บโฉ:๐ถโถ(๐ท ร ๐ธ). (Contributed by Mario Carneiro, 12-Jan-2017.) |
โข ๐ = (๐น โจ,โฉF ๐บ) & โข ๐ = (๐ท รc ๐ธ) & โข (๐ โ ๐น โ (๐ถ Func ๐ท)) & โข (๐ โ ๐บ โ (๐ถ Func ๐ธ)) โ โข (๐ โ ๐ โ (๐ถ Func ๐)) | ||
Theorem | prf1st 18027 | Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
โข ๐ = (๐น โจ,โฉF ๐บ) & โข (๐ โ ๐น โ (๐ถ Func ๐ท)) & โข (๐ โ ๐บ โ (๐ถ Func ๐ธ)) โ โข (๐ โ ((๐ท 1stF ๐ธ) โfunc ๐) = ๐น) | ||
Theorem | prf2nd 18028 | Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
โข ๐ = (๐น โจ,โฉF ๐บ) & โข (๐ โ ๐น โ (๐ถ Func ๐ท)) & โข (๐ โ ๐บ โ (๐ถ Func ๐ธ)) โ โข (๐ โ ((๐ท 2ndF ๐ธ) โfunc ๐) = ๐บ) | ||
Theorem | 1st2ndprf 18029 | 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 18030 | 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 18031 | Obsolete proof of catcxpccl 18030 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 18032 | 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 18033 | Extend class notation with the evaluation functor. |
class evalF | ||
Syntax | ccurf 18034 | Extend class notation with the currying of a functor. |
class curryF | ||
Syntax | cuncf 18035 | Extend class notation with the uncurrying of a functor. |
class uncurryF | ||
Syntax | cdiag 18036 | Extend class notation to include the diagonal functor. |
class ฮfunc | ||
Definition | df-evlf 18037* | 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 18038* | 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 18039* | 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 18040* | 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 18041* | 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 18042* | 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 18043 | 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 18044 | Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.) |
โข ๐ธ = (๐ถ evalF ๐ท) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ท โ Cat) & โข ๐ต = (Baseโ๐ถ) & โข (๐ โ ๐น โ (๐ถ Func ๐ท)) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐น(1st โ๐ธ)๐) = ((1st โ๐น)โ๐)) | ||
Theorem | evlfcllem 18045 | Lemma for evlfcl 18046. (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 18046 | 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 18047* | 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 18048* | 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 18049* | 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 18050 | 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 18051 | 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 18052 | 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 18053* | 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 18054 | 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 18055 | 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 18056 | 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 18057 | 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 18058 | 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 18059 | 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 18060 | 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 18061 | 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 18062 | Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
โข ๐น = (โจโ๐ถ๐ท๐ธโโฉ uncurryF ๐บ) & โข (๐ โ ๐ท โ Cat) & โข (๐ โ ๐ธ โ Cat) & โข (๐ โ ๐บ โ (๐ถ Func (๐ท FuncCat ๐ธ))) โ โข (๐ โ (โจ๐ถ, ๐ทโฉ curryF ๐น) = ๐บ) | ||
Theorem | uncfcurf 18063 | Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
โข ๐บ = (โจ๐ถ, ๐ทโฉ curryF ๐น) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ท โ Cat) & โข (๐ โ ๐น โ ((๐ถ รc ๐ท) Func ๐ธ)) โ โข (๐ โ (โจโ๐ถ๐ท๐ธโโฉ uncurryF ๐บ) = ๐น) | ||
Theorem | diagval 18064 | 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 18065 | 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 18066 | 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 18067 | 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 18068 | 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 18069 | Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.) |
โข ๐ฟ = (๐ถฮfunc๐ท) & โข ๐ด = (Baseโ๐ถ) & โข ๐ต = (Baseโ๐ท) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ท โ Cat) & โข (๐ โ ๐ โ ๐ด) & โข (๐ โ ๐ โ ๐ด) & โข (๐ โ ๐น โ (๐๐ป๐)) โ โข (๐ โ ((๐(2nd โ๐ฟ)๐)โ๐น) = (๐ต ร {๐น})) | ||
Theorem | diag2cl 18070 | 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 18071 | As shown in diagval 18064, 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 18072 | Extend class notation with the Hom functor. |
class HomF | ||
Syntax | cyon 18073 | Extend class notation with the Yoneda embedding. |
class Yon | ||
Definition | df-hof 18074* | Define the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCatโ๐ถ) ร ๐ถ to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017.) |
โข HomF = (๐ โ Cat โฆ โจ(Homf โ๐), โฆ(Baseโ๐) / ๐โฆ(๐ฅ โ (๐ ร ๐), ๐ฆ โ (๐ ร ๐) โฆ (๐ โ ((1st โ๐ฆ)(Hom โ๐)(1st โ๐ฅ)), ๐ โ ((2nd โ๐ฅ)(Hom โ๐)(2nd โ๐ฆ)) โฆ (โ โ ((Hom โ๐)โ๐ฅ) โฆ ((๐(๐ฅ(compโ๐)(2nd โ๐ฆ))โ)(โจ(1st โ๐ฆ), (1st โ๐ฅ)โฉ(compโ๐)(2nd โ๐ฆ))๐))))โฉ) | ||
Definition | df-yon 18075 | Define the Yoneda embedding, which is the currying of the (opposite) Hom functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
โข Yon = (๐ โ Cat โฆ (โจ๐, (oppCatโ๐)โฉ curryF (HomFโ(oppCatโ๐)))) | ||
Theorem | hofval 18076* | Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCatโ๐ถ) ร ๐ถ to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017.) |
โข ๐ = (HomFโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข ๐ต = (Baseโ๐ถ) & โข ๐ป = (Hom โ๐ถ) & โข ยท = (compโ๐ถ) โ โข (๐ โ ๐ = โจ(Homf โ๐ถ), (๐ฅ โ (๐ต ร ๐ต), ๐ฆ โ (๐ต ร ๐ต) โฆ (๐ โ ((1st โ๐ฆ)๐ป(1st โ๐ฅ)), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ (โ โ (๐ปโ๐ฅ) โฆ ((๐(๐ฅ ยท (2nd โ๐ฆ))โ)(โจ(1st โ๐ฆ), (1st โ๐ฅ)โฉ ยท (2nd โ๐ฆ))๐))))โฉ) | ||
Theorem | hof1fval 18077 | The object part of the Hom functor is the Homf operation, which is just a functionalized version of Hom. That is, it is a two argument function, which maps ๐, ๐ to the set of morphisms from ๐ to ๐. (Contributed by Mario Carneiro, 15-Jan-2017.) |
โข ๐ = (HomFโ๐ถ) & โข (๐ โ ๐ถ โ Cat) โ โข (๐ โ (1st โ๐) = (Homf โ๐ถ)) | ||
Theorem | hof1 18078 | The object part of the Hom functor maps ๐, ๐ to the set of morphisms from ๐ to ๐. (Contributed by Mario Carneiro, 15-Jan-2017.) |
โข ๐ = (HomFโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข ๐ต = (Baseโ๐ถ) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐(1st โ๐)๐) = (๐๐ป๐)) | ||
Theorem | hof2fval 18079* | The morphism part of the Hom functor, for morphisms โจ๐, ๐โฉ:โจ๐, ๐โฉโถโจ๐, ๐โฉ (which since the first argument is contravariant means morphisms ๐:๐โถ๐ and ๐:๐โถ๐), yields a function (a morphism of SetCat) mapping โ:๐โถ๐ to ๐ โ โ โ ๐:๐โถ๐. (Contributed by Mario Carneiro, 15-Jan-2017.) |
โข ๐ = (HomFโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข ๐ต = (Baseโ๐ถ) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข ยท = (compโ๐ถ) โ โข (๐ โ (โจ๐, ๐โฉ(2nd โ๐)โจ๐, ๐โฉ) = (๐ โ (๐๐ป๐), ๐ โ (๐๐ป๐) โฆ (โ โ (๐๐ป๐) โฆ ((๐(โจ๐, ๐โฉ ยท ๐)โ)(โจ๐, ๐โฉ ยท ๐)๐)))) | ||
Theorem | hof2val 18080* | The morphism part of the Hom functor, for morphisms โจ๐, ๐โฉ:โจ๐, ๐โฉโถโจ๐, ๐โฉ (which since the first argument is contravariant means morphisms ๐:๐โถ๐ and ๐:๐โถ๐), yields a function (a morphism of SetCat) mapping โ:๐โถ๐ to ๐ โ โ โ ๐:๐โถ๐. (Contributed by Mario Carneiro, 15-Jan-2017.) |
โข ๐ = (HomFโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข ๐ต = (Baseโ๐ถ) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข ยท = (compโ๐ถ) & โข (๐ โ ๐น โ (๐๐ป๐)) & โข (๐ โ ๐บ โ (๐๐ป๐)) โ โข (๐ โ (๐น(โจ๐, ๐โฉ(2nd โ๐)โจ๐, ๐โฉ)๐บ) = (โ โ (๐๐ป๐) โฆ ((๐บ(โจ๐, ๐โฉ ยท ๐)โ)(โจ๐, ๐โฉ ยท ๐)๐น))) | ||
Theorem | hof2 18081 | The morphism part of the Hom functor, for morphisms โจ๐, ๐โฉ:โจ๐, ๐โฉโถโจ๐, ๐โฉ (which since the first argument is contravariant means morphisms ๐:๐โถ๐ and ๐:๐โถ๐), yields a function (a morphism of SetCat) mapping โ:๐โถ๐ to ๐ โ โ โ ๐:๐โถ๐. (Contributed by Mario Carneiro, 15-Jan-2017.) |
โข ๐ = (HomFโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข ๐ต = (Baseโ๐ถ) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข ยท = (compโ๐ถ) & โข (๐ โ ๐น โ (๐๐ป๐)) & โข (๐ โ ๐บ โ (๐๐ป๐)) & โข (๐ โ ๐พ โ (๐๐ป๐)) โ โข (๐ โ ((๐น(โจ๐, ๐โฉ(2nd โ๐)โจ๐, ๐โฉ)๐บ)โ๐พ) = ((๐บ(โจ๐, ๐โฉ ยท ๐)๐พ)(โจ๐, ๐โฉ ยท ๐)๐น)) | ||
Theorem | hofcllem 18082 | Lemma for hofcl 18083. (Contributed by Mario Carneiro, 15-Jan-2017.) |
โข ๐ = (HomFโ๐ถ) & โข ๐ = (oppCatโ๐ถ) & โข ๐ท = (SetCatโ๐) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) & โข ๐ต = (Baseโ๐ถ) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐พ โ (๐๐ป๐)) & โข (๐ โ ๐ฟ โ (๐๐ป๐)) & โข (๐ โ ๐ โ (๐๐ป๐)) & โข (๐ โ ๐ โ (๐๐ป๐)) โ โข (๐ โ ((๐พ(โจ๐, ๐โฉ(compโ๐ถ)๐)๐)(โจ๐, ๐โฉ(2nd โ๐)โจ๐, ๐โฉ)(๐(โจ๐, ๐โฉ(compโ๐ถ)๐)๐ฟ)) = ((๐(โจ๐, ๐โฉ(2nd โ๐)โจ๐, ๐โฉ)๐)(โจ(๐๐ป๐), (๐๐ป๐)โฉ(compโ๐ท)(๐๐ป๐))(๐พ(โจ๐, ๐โฉ(2nd โ๐)โจ๐, ๐โฉ)๐ฟ))) | ||
Theorem | hofcl 18083 | Closure of the Hom functor. Note that the codomain is the category SetCatโ๐ for any universe ๐ which contains each Hom-set. This corresponds to the assertion that ๐ถ be locally small (with respect to ๐). (Contributed by Mario Carneiro, 15-Jan-2017.) |
โข ๐ = (HomFโ๐ถ) & โข ๐ = (oppCatโ๐ถ) & โข ๐ท = (SetCatโ๐) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) โ โข (๐ โ ๐ โ ((๐ รc ๐ถ) Func ๐ท)) | ||
Theorem | oppchofcl 18084 | Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
โข ๐ = (oppCatโ๐ถ) & โข ๐ = (HomFโ๐) & โข ๐ท = (SetCatโ๐) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) โ โข (๐ โ ๐ โ ((๐ถ รc ๐) Func ๐ท)) | ||
Theorem | yonval 18085 | Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข ๐ = (oppCatโ๐ถ) & โข ๐ = (HomFโ๐) โ โข (๐ โ ๐ = (โจ๐ถ, ๐โฉ curryF ๐)) | ||
Theorem | yoncl 18086 | The Yoneda embedding is a functor from the category to the category ๐ of presheaves on ๐ถ. (Contributed by Mario Carneiro, 17-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข ๐ = (oppCatโ๐ถ) & โข ๐ = (SetCatโ๐) & โข ๐ = (๐ FuncCat ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) โ โข (๐ โ ๐ โ (๐ถ Func ๐)) | ||
Theorem | yon1cl 18087 | The Yoneda embedding at an object of ๐ถ is a presheaf on ๐ถ, also known as the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข ๐ต = (Baseโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐ต) & โข ๐ = (oppCatโ๐ถ) & โข ๐ = (SetCatโ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) โ โข (๐ โ ((1st โ๐)โ๐) โ (๐ Func ๐)) | ||
Theorem | yon11 18088 | Value of the Yoneda embedding at an object. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข ๐ต = (Baseโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐ต) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((1st โ((1st โ๐)โ๐))โ๐) = (๐๐ป๐)) | ||
Theorem | yon12 18089 | Value of the Yoneda embedding at a morphism. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข ๐ต = (Baseโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐ต) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐ โ ๐ต) & โข ยท = (compโ๐ถ) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐น โ (๐๐ป๐)) & โข (๐ โ ๐บ โ (๐๐ป๐)) โ โข (๐ โ (((๐(2nd โ((1st โ๐)โ๐))๐)โ๐น)โ๐บ) = (๐บ(โจ๐, ๐โฉ ยท ๐)๐น)) | ||
Theorem | yon2 18090 | Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข ๐ต = (Baseโ๐ถ) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐ต) & โข ๐ป = (Hom โ๐ถ) & โข (๐ โ ๐ โ ๐ต) & โข ยท = (compโ๐ถ) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐น โ (๐๐ป๐)) & โข (๐ โ ๐บ โ (๐๐ป๐)) โ โข (๐ โ ((((๐(2nd โ๐)๐)โ๐น)โ๐)โ๐บ) = (๐น(โจ๐, ๐โฉ ยท ๐)๐บ)) | ||
Theorem | hofpropd 18091 | If two categories have the same set of objects, morphisms, and compositions, then they have the same Hom functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
โข (๐ โ (Homf โ๐ถ) = (Homf โ๐ท)) & โข (๐ โ (compfโ๐ถ) = (compfโ๐ท)) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ท โ Cat) โ โข (๐ โ (HomFโ๐ถ) = (HomFโ๐ท)) | ||
Theorem | yonpropd 18092 | If two categories have the same set of objects, morphisms, and compositions, then they have the same Yoneda functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
โข (๐ โ (Homf โ๐ถ) = (Homf โ๐ท)) & โข (๐ โ (compfโ๐ถ) = (compfโ๐ท)) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ท โ Cat) โ โข (๐ โ (Yonโ๐ถ) = (Yonโ๐ท)) | ||
Theorem | oppcyon 18093 | Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.) |
โข ๐ = (oppCatโ๐ถ) & โข ๐ = (Yonโ๐) & โข ๐ = (HomFโ๐ถ) & โข (๐ โ ๐ถ โ Cat) โ โข (๐ โ ๐ = (โจ๐, ๐ถโฉ curryF ๐)) | ||
Theorem | oyoncl 18094 | The opposite Yoneda embedding is a functor from oppCatโ๐ถ to the functor category ๐ถ โ SetCat. (Contributed by Mario Carneiro, 26-Jan-2017.) |
โข ๐ = (oppCatโ๐ถ) & โข ๐ = (Yonโ๐) & โข (๐ โ ๐ถ โ Cat) & โข ๐ = (SetCatโ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) & โข ๐ = (๐ถ FuncCat ๐) โ โข (๐ โ ๐ โ (๐ Func ๐)) | ||
Theorem | oyon1cl 18095 | The opposite Yoneda embedding at an object of ๐ถ is a functor from ๐ถ to Set, also known as the covariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
โข ๐ = (oppCatโ๐ถ) & โข ๐ = (Yonโ๐) & โข (๐ โ ๐ถ โ Cat) & โข ๐ = (SetCatโ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) & โข ๐ต = (Baseโ๐ถ) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((1st โ๐)โ๐) โ (๐ถ Func ๐)) | ||
Theorem | yonedalem1 18096 | Lemma for yoneda 18107. (Contributed by Mario Carneiro, 28-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข ๐ต = (Baseโ๐ถ) & โข 1 = (Idโ๐ถ) & โข ๐ = (oppCatโ๐ถ) & โข ๐ = (SetCatโ๐) & โข ๐ = (SetCatโ๐) & โข ๐ = (๐ FuncCat ๐) & โข ๐ป = (HomFโ๐) & โข ๐ = ((๐ รc ๐) FuncCat ๐) & โข ๐ธ = (๐ evalF ๐) & โข ๐ = (๐ป โfunc ((โจ(1st โ๐), tpos (2nd โ๐)โฉ โfunc (๐ 2ndF ๐)) โจ,โฉF (๐ 1stF ๐))) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) & โข (๐ โ (ran (Homf โ๐) โช ๐) โ ๐) โ โข (๐ โ (๐ โ ((๐ รc ๐) Func ๐) โง ๐ธ โ ((๐ รc ๐) Func ๐))) | ||
Theorem | yonedalem21 18097 | Lemma for yoneda 18107. (Contributed by Mario Carneiro, 28-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข ๐ต = (Baseโ๐ถ) & โข 1 = (Idโ๐ถ) & โข ๐ = (oppCatโ๐ถ) & โข ๐ = (SetCatโ๐) & โข ๐ = (SetCatโ๐) & โข ๐ = (๐ FuncCat ๐) & โข ๐ป = (HomFโ๐) & โข ๐ = ((๐ รc ๐) FuncCat ๐) & โข ๐ธ = (๐ evalF ๐) & โข ๐ = (๐ป โfunc ((โจ(1st โ๐), tpos (2nd โ๐)โฉ โfunc (๐ 2ndF ๐)) โจ,โฉF (๐ 1stF ๐))) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) & โข (๐ โ (ran (Homf โ๐) โช ๐) โ ๐) & โข (๐ โ ๐น โ (๐ Func ๐)) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐น(1st โ๐)๐) = (((1st โ๐)โ๐)(๐ Nat ๐)๐น)) | ||
Theorem | yonedalem3a 18098* | Lemma for yoneda 18107. (Contributed by Mario Carneiro, 29-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข ๐ต = (Baseโ๐ถ) & โข 1 = (Idโ๐ถ) & โข ๐ = (oppCatโ๐ถ) & โข ๐ = (SetCatโ๐) & โข ๐ = (SetCatโ๐) & โข ๐ = (๐ FuncCat ๐) & โข ๐ป = (HomFโ๐) & โข ๐ = ((๐ รc ๐) FuncCat ๐) & โข ๐ธ = (๐ evalF ๐) & โข ๐ = (๐ป โfunc ((โจ(1st โ๐), tpos (2nd โ๐)โฉ โfunc (๐ 2ndF ๐)) โจ,โฉF (๐ 1stF ๐))) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) & โข (๐ โ (ran (Homf โ๐) โช ๐) โ ๐) & โข (๐ โ ๐น โ (๐ Func ๐)) & โข (๐ โ ๐ โ ๐ต) & โข ๐ = (๐ โ (๐ Func ๐), ๐ฅ โ ๐ต โฆ (๐ โ (((1st โ๐)โ๐ฅ)(๐ Nat ๐)๐) โฆ ((๐โ๐ฅ)โ( 1 โ๐ฅ)))) โ โข (๐ โ ((๐น๐๐) = (๐ โ (((1st โ๐)โ๐)(๐ Nat ๐)๐น) โฆ ((๐โ๐)โ( 1 โ๐))) โง (๐น๐๐):(๐น(1st โ๐)๐)โถ(๐น(1st โ๐ธ)๐))) | ||
Theorem | yonedalem4a 18099* | Lemma for yoneda 18107. (Contributed by Mario Carneiro, 29-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข ๐ต = (Baseโ๐ถ) & โข 1 = (Idโ๐ถ) & โข ๐ = (oppCatโ๐ถ) & โข ๐ = (SetCatโ๐) & โข ๐ = (SetCatโ๐) & โข ๐ = (๐ FuncCat ๐) & โข ๐ป = (HomFโ๐) & โข ๐ = ((๐ รc ๐) FuncCat ๐) & โข ๐ธ = (๐ evalF ๐) & โข ๐ = (๐ป โfunc ((โจ(1st โ๐), tpos (2nd โ๐)โฉ โfunc (๐ 2ndF ๐)) โจ,โฉF (๐ 1stF ๐))) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) & โข (๐ โ (ran (Homf โ๐) โช ๐) โ ๐) & โข (๐ โ ๐น โ (๐ Func ๐)) & โข (๐ โ ๐ โ ๐ต) & โข ๐ = (๐ โ (๐ Func ๐), ๐ฅ โ ๐ต โฆ (๐ข โ ((1st โ๐)โ๐ฅ) โฆ (๐ฆ โ ๐ต โฆ (๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ) โฆ (((๐ฅ(2nd โ๐)๐ฆ)โ๐)โ๐ข))))) & โข (๐ โ ๐ด โ ((1st โ๐น)โ๐)) โ โข (๐ โ ((๐น๐๐)โ๐ด) = (๐ฆ โ ๐ต โฆ (๐ โ (๐ฆ(Hom โ๐ถ)๐) โฆ (((๐(2nd โ๐น)๐ฆ)โ๐)โ๐ด)))) | ||
Theorem | yonedalem4b 18100* | Lemma for yoneda 18107. (Contributed by Mario Carneiro, 29-Jan-2017.) |
โข ๐ = (Yonโ๐ถ) & โข ๐ต = (Baseโ๐ถ) & โข 1 = (Idโ๐ถ) & โข ๐ = (oppCatโ๐ถ) & โข ๐ = (SetCatโ๐) & โข ๐ = (SetCatโ๐) & โข ๐ = (๐ FuncCat ๐) & โข ๐ป = (HomFโ๐) & โข ๐ = ((๐ รc ๐) FuncCat ๐) & โข ๐ธ = (๐ evalF ๐) & โข ๐ = (๐ป โfunc ((โจ(1st โ๐), tpos (2nd โ๐)โฉ โfunc (๐ 2ndF ๐)) โจ,โฉF (๐ 1stF ๐))) & โข (๐ โ ๐ถ โ Cat) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ran (Homf โ๐ถ) โ ๐) & โข (๐ โ (ran (Homf โ๐) โช ๐) โ ๐) & โข (๐ โ ๐น โ (๐ Func ๐)) & โข (๐ โ ๐ โ ๐ต) & โข ๐ = (๐ โ (๐ Func ๐), ๐ฅ โ ๐ต โฆ (๐ข โ ((1st โ๐)โ๐ฅ) โฆ (๐ฆ โ ๐ต โฆ (๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ) โฆ (((๐ฅ(2nd โ๐)๐ฆ)โ๐)โ๐ข))))) & โข (๐ โ ๐ด โ ((1st โ๐น)โ๐)) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐บ โ (๐(Hom โ๐ถ)๐)) โ โข (๐ โ ((((๐น๐๐)โ๐ด)โ๐)โ๐บ) = (((๐(2nd โ๐น)๐)โ๐บ)โ๐ด)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |