HomeTheorem List (p. 185 of 512)
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. 185 of 512) | < 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-31526) |
Hilbert Space Explorer
(31527-33049) |
Users' Mathboxes
(33050-51159) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | evlfcllem 18401 | Lemma for evlfcl 18402. (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 18402 | 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 18403* | 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 18404* | 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 18405* | 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 18406 | 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 18407 | 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 18408 | 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 18409* | 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 18410 | 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 18411 | 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 18412 | 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 18413 | 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 18414 | 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 18415 | 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 18416 | 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 18417 | 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 18418 | Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
| ⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) ⇒ ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF 𝐹) = 𝐺) | ||
| Theorem | uncfcurf 18419 | Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
| ⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) ⇒ ⊢ (𝜑 → (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺) = 𝐹) | ||
| Theorem | diagval 18420 | 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 18421 | 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 18422 | 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 18423 | 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 18424 | 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 18425 | Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = (𝐵 × {𝐹})) | ||
| Theorem | diag2cl 18426 | 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 18427 | As shown in diagval 18420, 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 18428 | Extend class notation with the Hom functor. |
| class HomF | ||
| Syntax | cyon 18429 | Extend class notation with the Yoneda embedding. |
| class Yon | ||
| Definition | df-hof 18430* | 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 18431 | 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 18432* | 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 18433 | 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 18434 | 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 18435* | 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 18436* | 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 18437 | 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 18438 | Lemma for hofcl 18439. (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑀 = (HomF‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑊)) & ⊢ (𝜑 → 𝑃 ∈ (𝑆𝐻𝑍)) & ⊢ (𝜑 → 𝑄 ∈ (𝑊𝐻𝑇)) ⇒ ⊢ (𝜑 → ((𝐾(⟨𝑆, 𝑍⟩(comp‘𝐶)𝑋)𝑃)(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑆, 𝑇⟩)(𝑄(⟨𝑌, 𝑊⟩(comp‘𝐶)𝑇)𝐿)) = ((𝑃(⟨𝑍, 𝑊⟩(2nd ‘𝑀)⟨𝑆, 𝑇⟩)𝑄)(⟨(𝑋𝐻𝑌), (𝑍𝐻𝑊)⟩(comp‘𝐷)(𝑆𝐻𝑇))(𝐾(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩)𝐿))) | ||
| Theorem | hofcl 18439 | 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 18440 | Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝐶 ×c 𝑂) Func 𝐷)) | ||
| Theorem | yonval 18441 | Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) ⇒ ⊢ (𝜑 → 𝑌 = (⟨𝐶, 𝑂⟩ curryF 𝑀)) | ||
| Theorem | yoncl 18442 | 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 18443 | 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 18444 | 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 18445 | 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 18446 | Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑍)) & ⊢ (𝜑 → 𝐺 ∈ (𝑊𝐻𝑋)) ⇒ ⊢ (𝜑 → ((((𝑋(2nd ‘𝑌)𝑍)‘𝐹)‘𝑊)‘𝐺) = (𝐹(⟨𝑊, 𝑋⟩ · 𝑍)𝐺)) | ||
| Theorem | hofpropd 18447 | 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 18448 | 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 18449 | Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑌 = (Yon‘𝑂) & ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑌 = (⟨𝑂, 𝐶⟩ curryF 𝑀)) | ||
| Theorem | oyoncl 18450 | 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 18451 | 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 18452 | Lemma for yoneda 18463. (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 18453 | Lemma for yoneda 18463. (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 18454* | Lemma for yoneda 18463. (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 18455* | Lemma for yoneda 18463. (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 18456* | Lemma for yoneda 18463. (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 18457* | Lemma for yoneda 18463. (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 18458 | Lemma for yoneda 18463. (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 18459* | Lemma for yoneda 18463. (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 18460* | Lemma for yoneda 18463. (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 18461* | 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 18462* | Lemma for yonffth 18464. (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 18463* | 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 18464 | 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 18465* | 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 18466 | Class function defining dual orders. |
| class ODual | ||
| Definition | df-odu 18467 |
Define the dual of an ordered structure, which replaces the order
component of the structure with its reverse. See odubas 18471, oduleval 18469,
and oduleg 18470 for its principal properties.
EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 18675. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩)) | ||
| Theorem | oduval 18468 | Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ 𝐷 = (𝑂 sSet ⟨(le‘ndx), ◡ ≤ ⟩) | ||
| Theorem | oduleval 18469 | Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ ◡ ≤ = (le‘𝐷) | ||
| Theorem | oduleg 18470 | Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) & ⊢ 𝐺 = (le‘𝐷) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝐺𝐵 ↔ 𝐵 ≤ 𝐴)) | ||
| Theorem | odubas 18471 | 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 18472 | Extend class notation with the class of all prosets. |
| class Proset | ||
| Syntax | cdrs 18473 | Extend class notation with the class of all directed sets. |
| class Dirset | ||
| Definition | df-proset 18474* |
Define the class of preordered sets, or prosets. A proset is a set
equipped with a preorder, that is, a transitive and reflexive relation.
Preorders are a natural generalization of partial orders which need not be antisymmetric: there may be pairs of elements such that each is "less than or equal to" the other, so that both elements have the same order-theoretic properties (in some sense, there is a "tie" among them). If a preorder is required to be antisymmetric, that is, there is no such "tie", then one obtains a partial order. If a preorder is required to be symmetric, that is, all comparable elements are tied, then one obtains an equivalence relation. Every preorder naturally factors into these two notions: the "tie" relation on a proset is an equivalence relation, and the quotient under that equivalence relation is a partial order. (Contributed by FL, 17-Nov-2014.) (Revised by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ Proset = {𝑓 ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))} | ||
| Definition | df-drs 18475* |
Define the class of directed sets. A directed set is a nonempty
preordered set where every pair of elements have some upper bound. Note
that it is not required that there exist a least upper bound.
There is no consensus in the literature over whether directed sets are allowed to be empty. It is slightly more convenient for us if they are not. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ Dirset = {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))} | ||
| Theorem | isprs 18476* | Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Proset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
| Theorem | prslem 18477 | Lemma for prsref 18478 and prstr 18479. (Contributed by Mario Carneiro, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
| Theorem | prsref 18478 | "Less than or equal to" is reflexive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) | ||
| Theorem | prstr 18479 | "Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ≤ 𝑍) | ||
| Theorem | oduprs 18480 | Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ Proset → 𝐷 ∈ Proset ) | ||
| Theorem | isdrs 18481* | Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) | ||
| Theorem | drsdir 18482* | Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑧 ∈ 𝐵 (𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧)) | ||
| Theorem | drsprs 18483 | A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Proset ) | ||
| Theorem | drsbn0 18484 | The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset → 𝐵 ≠ ∅) | ||
| Theorem | drsdirfi 18485* | Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 18475 first comes into play; without it we would need an additional constraint that 𝑋 not be empty. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ⊆ 𝐵 ∧ 𝑋 ∈ Fin) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑦) | ||
| Theorem | isdrs2 18486* | Directed sets may be defined in terms of finite subsets. Again, without nonemptiness we would need to restrict to nonempty subsets here. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ ∀𝑥 ∈ (𝒫 𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦)) | ||
| Syntax | cpo 18487 | Extend class notation with the class of posets. |
| class Poset | ||
| Syntax | cplt 18488 | Extend class notation with less-than for posets. |
| class lt | ||
| Syntax | club 18489 | Extend class notation with poset least upper bound. |
| class lub | ||
| Syntax | cglb 18490 | Extend class notation with poset greatest lower bound. |
| class glb | ||
| Syntax | cjn 18491 | Extend class notation with poset join. |
| class join | ||
| Syntax | cmee 18492 | Extend class notation with poset meet. |
| class meet | ||
| Definition | df-poset 18493* |
Define the class of partially ordered sets (posets). A poset is a set
equipped with a partial order, that is, a binary relation which is
reflexive, antisymmetric, and transitive. Unlike a total order, in a
partial order there may be pairs of elements where neither precedes the
other. Definition of poset in [Crawley] p. 1. Note that
Crawley-Dilworth require that a poset base set be nonempty, but we
follow the convention of most authors who don't make this a requirement.
In our formalism of extensible structures, the base set of a poset 𝑓 is denoted by (Base‘𝑓) and its partial order by (le‘𝑓) (for "less than or equal to"). The quantifiers ∃𝑏∃𝑟 provide a notational shorthand to allow to refer to the base and ordering relation as 𝑏 and 𝑟 in the definition rather than having to repeat (Base‘𝑓) and (le‘𝑓) throughout. These quantifiers can be eliminated with ceqsex2v 3501 and related theorems. (Contributed by NM, 18-Oct-2012.) |
| ⊢ Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))} | ||
| Theorem | ispos 18494* | The predicate "is a poset". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
| Theorem | ispos2 18495* |
A poset is an antisymmetric proset.
EDITORIAL: could become the definition of poset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ Proset ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))) | ||
| Theorem | posprs 18496 | A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset ) | ||
| Theorem | posi 18497 | Lemma for poset properties. (Contributed by NM, 11-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
| Theorem | posref 18498 | A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) | ||
| Theorem | posasymb 18499 | A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
| Theorem | postr 18500 | A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |