Home | Metamath
Proof Explorer Theorem List (p. 168 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | curfuncf 16701 | Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) ⇒ ⊢ (𝜑 → (〈𝐶, 𝐷〉 curryF 𝐹) = 𝐺) | ||
Theorem | uncfcurf 16702 | Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) ⇒ ⊢ (𝜑 → (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) = 𝐹) | ||
Theorem | diagval 16703 | 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 16704 | 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 16705 | 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 16706 | 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 16707 | 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 16708 | Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = (𝐵 × {𝐹})) | ||
Theorem | diag2cl 16709 | 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 16710 | As shown in diagval 16703, 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 16711 | Extend class notation with the Hom functor. |
class HomF | ||
Syntax | cyon 16712 | Extend class notation with the Yoneda embedding. |
class Yon | ||
Definition | df-hof 16713* | 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 16714 | 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 16715* | 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 16716 | 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 16717 | 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 16718* | 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 16719* | 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 16720 | 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 16721 | Lemma for hofcl 16722. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑊)) & ⊢ (𝜑 → 𝑃 ∈ (𝑆𝐻𝑍)) & ⊢ (𝜑 → 𝑄 ∈ (𝑊𝐻𝑇)) ⇒ ⊢ (𝜑 → ((𝐾(〈𝑆, 𝑍〉(comp‘𝐶)𝑋)𝑃)(〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑆, 𝑇〉)(𝑄(〈𝑌, 𝑊〉(comp‘𝐶)𝑇)𝐿)) = ((𝑃(〈𝑍, 𝑊〉(2nd ‘𝑀)〈𝑆, 𝑇〉)𝑄)(〈(𝑋𝐻𝑌), (𝑍𝐻𝑊)〉(comp‘𝐷)(𝑆𝐻𝑇))(𝐾(〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑍, 𝑊〉)𝐿))) | ||
Theorem | hofcl 16722 | 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 16723 | Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝐶 ×c 𝑂) Func 𝐷)) | ||
Theorem | yonval 16724 | Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ 𝑌 = (Yon‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) ⇒ ⊢ (𝜑 → 𝑌 = (〈𝐶, 𝑂〉 curryF 𝑀)) | ||
Theorem | yoncl 16725 | 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 16726 | 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 16727 | 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 16728 | 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 16729 | Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑍)) & ⊢ (𝜑 → 𝐺 ∈ (𝑊𝐻𝑋)) ⇒ ⊢ (𝜑 → ((((𝑋(2nd ‘𝑌)𝑍)‘𝐹)‘𝑊)‘𝐺) = (𝐹(〈𝑊, 𝑋〉 · 𝑍)𝐺)) | ||
Theorem | hofpropd 16730 | 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 16731 | 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 16732 | Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑌 = (Yon‘𝑂) & ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑌 = (〈𝑂, 𝐶〉 curryF 𝑀)) | ||
Theorem | oyoncl 16733 | 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 16734 | 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 16735 | Lemma for yoneda 16746. (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 16736 | Lemma for yoneda 16746. (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 16737* | Lemma for yoneda 16746. (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 16738* | Lemma for yoneda 16746. (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 16739* | Lemma for yoneda 16746. (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 16740* | Lemma for yoneda 16746. (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 16741 | Lemma for yoneda 16746. (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 16742* | Lemma for yoneda 16746. (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 16743* | Lemma for yoneda 16746. (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 16744* | 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 16745* | Lemma for yonffth 16747. (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 16746* | 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 16747 | 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 16748* | 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 | cpreset 16749 | Extend class notation with the class of all presets. |
class Preset | ||
Syntax | cdrs 16750 | Extend class notation with the class of all directed sets. |
class Dirset | ||
Definition | df-preset 16751* |
Define the class of preordered sets (presets). A preset is a set
equipped with a transitive and reflexive relation.
Preorders are a natural generalization of order for sets where there is a well-defined ordering, but it in some sense "fails to capture the whole story", in that there may be pairs of elements which are indistinguishable under the order. Two elements which are not equal but are less-or-equal to each other behave the same under all order operations and may be thought of as "tied". A preorder can naturally be strengthened by requiring that there are no ties, resulting in a partial order, or by stating that all comparable pairs of elements are tied, resulting in an equivalence relation. Every preorder naturally factors into these two types; the tied relation on a preorder is an equivalence relation and the quotient under that relation is a partial order. (Contributed by FL, 17-Nov-2014.) (Revised by Stefan O'Rear, 31-Jan-2015.) |
⊢ Preset = {𝑓 ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))} | ||
Definition | df-drs 16752* |
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 = {𝑓 ∈ Preset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))} | ||
Theorem | isprs 16753* | Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Preset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
Theorem | prslem 16754 | Lemma for prsref 16755 and prstr 16756. (Contributed by Mario Carneiro, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Preset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
Theorem | prsref 16755 | Less-or-equal is reflexive in a preset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Preset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) | ||
Theorem | prstr 16756 | Less-or-equal is transitive in a preset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Preset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ≤ 𝑍) | ||
Theorem | isdrs 16757* | Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Preset ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) | ||
Theorem | drsdir 16758* | Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑧 ∈ 𝐵 (𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧)) | ||
Theorem | drsprs 16759 | A directed set is a preset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Preset ) | ||
Theorem | drsbn0 16760 | The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset → 𝐵 ≠ ∅) | ||
Theorem | drsdirfi 16761* | Any finite number of elements in a directed set have a common upper bound. Here is where the non-emptiness constraint in df-drs 16752 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 16762* | 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 ↔ (𝐾 ∈ Preset ∧ ∀𝑥 ∈ (𝒫 𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦)) | ||
Syntax | cpo 16763 | Extend class notation with the class of posets. |
class Poset | ||
Syntax | cplt 16764 | Extend class notation with less-than for posets. |
class lt | ||
Syntax | club 16765 | Extend class notation with poset least upper bound. |
class lub | ||
Syntax | cglb 16766 | Extend class notation with poset greatest lower bound. |
class glb | ||
Syntax | cjn 16767 | Extend class notation with poset join. |
class join | ||
Syntax | cmee 16768 | Extend class notation with poset meet. |
class meet | ||
Definition | df-poset 16769* |
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 us 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 3218 and related theorems. (Contributed by NM, 18-Oct-2012.) |
⊢ Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))} | ||
Theorem | ispos 16770* | The predicate "is a poset." (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
Theorem | ispos2 16771* |
A poset is an antisymmetric preset.
EDITORIAL: could become the definition of poset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ Preset ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))) | ||
Theorem | posprs 16772 | A poset is a preset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐾 ∈ Poset → 𝐾 ∈ Preset ) | ||
Theorem | posi 16773 | Lemma for poset properties. (Contributed by NM, 11-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
Theorem | posref 16774 | A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) | ||
Theorem | posasymb 16775 | A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
Theorem | postr 16776 | A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) | ||
Theorem | 0pos 16777 | Technical lemma to simplify the statement of ipopos 16983. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 15739) and any relation partially orders an empty set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ ∅ ∈ Poset | ||
Theorem | isposd 16778* | Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014.) |
⊢ (𝜑 → 𝐾 ∈ V) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → ≤ = (le‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ (𝜑 → 𝐾 ∈ Poset) | ||
Theorem | isposi 16779* | Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.) |
⊢ 𝐾 ∈ V & ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ 𝐾 ∈ Poset | ||
Theorem | isposix 16780* | Properties that determine a poset (explicit structure version). Note that the numeric indices of the structure components are not mentioned explicitly in either the theorem or its proof. (Contributed by NM, 9-Nov-2012.) |
⊢ 𝐵 ∈ V & ⊢ ≤ ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(le‘ndx), ≤ 〉} & ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ 𝐾 ∈ Poset | ||
Definition | df-plt 16781 | Define less-than ordering for posets and related structures. Unlike df-base 15700 and df-ple 15788, this is a derived component extractor and not an extensible structure component extractor that defines the poset. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ lt = (𝑝 ∈ V ↦ ((le‘𝑝) ∖ I )) | ||
Theorem | pltfval 16782 | Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I )) | ||
Theorem | pltval 16783 | Less-than relation. (df-pss 3556 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) | ||
Theorem | pltle 16784 | Less-than implies less-than-or-equal. (pssss 3664 analog.) (Contributed by NM, 4-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌)) | ||
Theorem | pltne 16785 | Less-than relation. (df-pss 3556 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌)) | ||
Theorem | pltirr 16786 | The less-than relation is not reflexive. (pssirr 3669 analog.) (Contributed by NM, 7-Feb-2012.) |
⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋 < 𝑋) | ||
Theorem | pleval2i 16787 | One direction of pleval2 16788. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌))) | ||
Theorem | pleval2 16788 | Less-than-or-equal in terms of less-than. (sspss 3668 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 < 𝑌 ∨ 𝑋 = 𝑌))) | ||
Theorem | pltnle 16789 | Less-than implies not inverse less-than-or-equal. (Contributed by NM, 18-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋) | ||
Theorem | pltval3 16790 | Alternate expression for less-than relation. (dfpss3 3655 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋))) | ||
Theorem | pltnlt 16791 | The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 < 𝑋) | ||
Theorem | pltn2lp 16792 | The less-than relation has no 2-cycle loops. (pssn2lp 3670 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ¬ (𝑋 < 𝑌 ∧ 𝑌 < 𝑋)) | ||
Theorem | plttr 16793 | The less-than relation is transitive. (psstr 3673 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍)) | ||
Theorem | pltletr 16794 | Transitive law for chained less-than and less-than-or-equal. (psssstr 3675 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍)) | ||
Theorem | plelttr 16795 | Transitive law for chained less-than-or-equal and less-than. (sspsstr 3674 analog.) (Contributed by NM, 2-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍)) | ||
Theorem | pospo 16796 | Write a poset structure in terms of the proper-class poset predicate (strict less than version). (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ Poset ↔ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ ))) | ||
Definition | df-lub 16797* | Define the least upper bound (LUB) of a set of (poset) elements. The domain is restricted to exclude sets 𝑠 for which the LUB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.) |
⊢ lub = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))})) | ||
Definition | df-glb 16798* | Define the greatest lower bound (GLB) of a set of (poset) elements. The domain is restricted to exclude sets 𝑠 for which the GLB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.) |
⊢ glb = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑧(le‘𝑝)𝑦 → 𝑧(le‘𝑝)𝑥)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑧(le‘𝑝)𝑦 → 𝑧(le‘𝑝)𝑥))})) | ||
Definition | df-join 16799* | Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by Mario Carneiro, 3-Nov-2015.) |
⊢ join = (𝑝 ∈ V ↦ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧}) | ||
Definition | df-meet 16800* | Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.) |
⊢ meet = (𝑝 ∈ V ↦ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |