HomeTheorem List (p. 182 of 500)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 182 of 500) | < 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-30900) |
Hilbert Space Explorer
(30901-32423) |
Users' Mathboxes
(32424-49930) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 1stf2 18101 | 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 18102* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
| ⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐶 2ndF 𝐷) ⇒ ⊢ (𝜑 → 𝑄 = ⟨(2nd ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (2nd ↾ (𝑥𝐻𝑦)))⟩) | ||
| Theorem | 2ndf1 18103 | 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 18104 | 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 18105 | 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 18106 | 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 18107* | Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → 𝑃 = ⟨(𝑥 ∈ 𝐵 ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (ℎ ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))⟩) | ||
| Theorem | prf1 18108 | Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝑃)‘𝑋) = ⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)⟩) | ||
| Theorem | prf2fval 18109* | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝑃)𝑌) = (ℎ ∈ (𝑋𝐻𝑌) ↦ ⟨((𝑋(2nd ‘𝐹)𝑌)‘ℎ), ((𝑋(2nd ‘𝐺)𝑌)‘ℎ)⟩)) | ||
| Theorem | prf2 18110 | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝑃)𝑌)‘𝐾) = ⟨((𝑋(2nd ‘𝐹)𝑌)‘𝐾), ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)⟩) | ||
| Theorem | prfcl 18111 | The pairing of functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐷 is a functor ⟨𝐹, 𝐺⟩:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺) & ⊢ 𝑇 = (𝐷 ×c 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇)) | ||
| Theorem | prf1st 18112 | Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐷 1stF 𝐸) ∘func 𝑃) = 𝐹) | ||
| Theorem | prf2nd 18113 | Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺) | ||
| Theorem | 1st2ndprf 18114 | 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 18115 | 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 | xpcpropd 18116 | 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 18117 | Extend class notation with the evaluation functor. |
| class evalF | ||
| Syntax | ccurf 18118 | Extend class notation with the currying of a functor. |
| class curryF | ||
| Syntax | cuncf 18119 | Extend class notation with the uncurrying of a functor. |
| class uncurryF | ||
| Syntax | cdiag 18120 | Extend class notation to include the diagonal functor. |
| class Δfunc | ||
| Definition | df-evlf 18121* | 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 18122* | 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 18123* | 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 18124* | 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 18125* | 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 18126* | 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 18127 | 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 18128 | Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹(1st ‘𝐸)𝑋) = ((1st ‘𝐹)‘𝑋)) | ||
| Theorem | evlfcllem 18129 | Lemma for evlfcl 18130. (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 18130 | 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 18131* | 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 18132* | 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 18133* | 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 18134 | 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 18135 | 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 18136 | 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 18137* | 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 18138 | 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 18139 | 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 18140 | 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 18141 | 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 18142 | 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 18143 | 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 18144 | 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 18145 | 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 18146 | Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
| ⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) ⇒ ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF 𝐹) = 𝐺) | ||
| Theorem | uncfcurf 18147 | Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
| ⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) ⇒ ⊢ (𝜑 → (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺) = 𝐹) | ||
| Theorem | diagval 18148 | 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 18149 | 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 18150 | 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 18151 | 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 18152 | 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 18153 | Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = (𝐵 × {𝐹})) | ||
| Theorem | diag2cl 18154 | 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 18155 | As shown in diagval 18148, 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 18156 | Extend class notation with the Hom functor. |
| class HomF | ||
| Syntax | cyon 18157 | Extend class notation with the Yoneda embedding. |
| class Yon | ||
| Definition | df-hof 18158* | 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 18159 | 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 18160* | 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 18161 | 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 18162 | 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 18163* | 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 18164* | 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 18165 | 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 18166 | Lemma for hofcl 18167. (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑀 = (HomF‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑊)) & ⊢ (𝜑 → 𝑃 ∈ (𝑆𝐻𝑍)) & ⊢ (𝜑 → 𝑄 ∈ (𝑊𝐻𝑇)) ⇒ ⊢ (𝜑 → ((𝐾(⟨𝑆, 𝑍⟩(comp‘𝐶)𝑋)𝑃)(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑆, 𝑇⟩)(𝑄(⟨𝑌, 𝑊⟩(comp‘𝐶)𝑇)𝐿)) = ((𝑃(⟨𝑍, 𝑊⟩(2nd ‘𝑀)⟨𝑆, 𝑇⟩)𝑄)(⟨(𝑋𝐻𝑌), (𝑍𝐻𝑊)⟩(comp‘𝐷)(𝑆𝐻𝑇))(𝐾(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩)𝐿))) | ||
| Theorem | hofcl 18167 | 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 18168 | Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝐶 ×c 𝑂) Func 𝐷)) | ||
| Theorem | yonval 18169 | Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) ⇒ ⊢ (𝜑 → 𝑌 = (⟨𝐶, 𝑂⟩ curryF 𝑀)) | ||
| Theorem | yoncl 18170 | 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 18171 | 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 18172 | 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 18173 | 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 18174 | Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑍)) & ⊢ (𝜑 → 𝐺 ∈ (𝑊𝐻𝑋)) ⇒ ⊢ (𝜑 → ((((𝑋(2nd ‘𝑌)𝑍)‘𝐹)‘𝑊)‘𝐺) = (𝐹(⟨𝑊, 𝑋⟩ · 𝑍)𝐺)) | ||
| Theorem | hofpropd 18175 | 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 18176 | 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 18177 | Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑌 = (Yon‘𝑂) & ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑌 = (⟨𝑂, 𝐶⟩ curryF 𝑀)) | ||
| Theorem | oyoncl 18178 | 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 18179 | 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 18180 | Lemma for yoneda 18191. (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 18181 | Lemma for yoneda 18191. (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 18182* | Lemma for yoneda 18191. (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 18183* | Lemma for yoneda 18191. (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 18184* | Lemma for yoneda 18191. (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 | yonedalem4c 18185* | Lemma for yoneda 18191. (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 ‘𝐹)‘𝑋)) ⇒ ⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) ∈ (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) | ||
| Theorem | yonedalem22 18186 | Lemma for yoneda 18191. (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 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) ⇒ ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2nd ‘𝑌)𝑋)‘𝐾)(⟨((1st ‘𝑌)‘𝑋), 𝐹⟩(2nd ‘𝐻)⟨((1st ‘𝑌)‘𝑃), 𝐺⟩)𝐴)) | ||
| Theorem | yonedalem3b 18187* | Lemma for yoneda 18191. (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 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) & ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) ⇒ ⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1st ‘𝑍)𝑋), (𝐺(1st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1st ‘𝑍)𝑋), (𝐹(1st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1st ‘𝐸)𝑃))(𝐹𝑀𝑋))) | ||
| Theorem | yonedalem3 18188* | Lemma for yoneda 18191. (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 ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸)) | ||
| Theorem | yonedainv 18189* | The Yoneda Lemma with explicit inverse. (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 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) & ⊢ 𝐼 = (Inv‘𝑅) & ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))))) ⇒ ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁) | ||
| Theorem | yonffthlem 18190* | Lemma for yonffth 18192. (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 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) & ⊢ 𝐼 = (Inv‘𝑅) & ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))))) ⇒ ⊢ (𝜑 → 𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))) | ||
| Theorem | yoneda 18191* | The Yoneda Lemma. There is a natural isomorphism between the functors 𝑍 and 𝐸, where 𝑍(𝐹, 𝑋) is the natural transformations from Yon(𝑋) = Hom ( − , 𝑋) to 𝐹, and 𝐸(𝐹, 𝑋) = 𝐹(𝑋) is the evaluation functor. Here we need two universes to state the claim: the smaller universe 𝑈 is used for forming the functor category 𝑄 = 𝐶 op → SetCat(𝑈), which itself does not (necessarily) live in 𝑈 but instead is an element of the larger universe 𝑉. (If 𝑈 is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set 𝑈 = 𝑉 in this case.) (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 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) & ⊢ 𝐼 = (Iso‘𝑅) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐼𝐸)) | ||
| Theorem | yonffth 18192 | The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category 𝐶 as a full subcategory of the category 𝑄 of presheaves on 𝐶. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))) | ||
| Theorem | yoniso 18193* | If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from 𝐶 into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐷 = (CatCat‘𝑉) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐼 = (Iso‘𝐷) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐸 = (𝑄 ↾s ran (1st ‘𝑌)) & ⊢ (𝜑 → 𝑉 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝐹‘(𝑥(Hom ‘𝐶)𝑦)) = 𝑦) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝐶𝐼𝐸)) | ||
| Syntax | codu 18194 | Class function defining dual orders. |
| class ODual | ||
| Definition | df-odu 18195 |
Define the dual of an ordered structure, which replaces the order
component of the structure with its reverse. See odubas 18199, oduleval 18197,
and oduleg 18198 for its principal properties.
EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 18403. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩)) | ||
| Theorem | oduval 18196 | Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ 𝐷 = (𝑂 sSet ⟨(le‘ndx), ◡ ≤ ⟩) | ||
| Theorem | oduleval 18197 | Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ ◡ ≤ = (le‘𝐷) | ||
| Theorem | oduleg 18198 | Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) & ⊢ 𝐺 = (le‘𝐷) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝐺𝐵 ↔ 𝐵 ≤ 𝐴)) | ||
| Theorem | odubas 18199 | Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Proof shortened by AV, 12-Nov-2024.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ 𝐵 = (Base‘𝑂) ⇒ ⊢ 𝐵 = (Base‘𝐷) | ||
| Syntax | cproset 18200 | Extend class notation with the class of all prosets. |
| class Proset | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |