HomeTheorem List (p. 496 of 498)
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. 496 of 498) | < 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-30862) |
Hilbert Space Explorer
(30863-32385) |
Users' Mathboxes
(32386-49800) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | oppcterm 49501 | The opposite category of a terminal category is a terminal category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ TermCat) ⇒ ⊢ (𝜑 → 𝑂 ∈ TermCat) | ||
| Theorem | functermclem 49502 | Lemma for functermc 49503. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ ((𝜑 ∧ 𝐾𝑅𝐿) → 𝐾 = 𝐹) & ⊢ (𝜑 → (𝐹𝑅𝐿 ↔ 𝐿 = 𝐺)) ⇒ ⊢ (𝜑 → (𝐾𝑅𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺))) | ||
| Theorem | functermc 49503* | Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝐹 = (𝐵 × 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) ⇒ ⊢ (𝜑 → (𝐾(𝐷 Func 𝐸)𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺))) | ||
| Theorem | functermc2 49504* | Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝐹 = (𝐵 × 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) ⇒ ⊢ (𝜑 → (𝐷 Func 𝐸) = {⟨𝐹, 𝐺⟩}) | ||
| Theorem | functermceu 49505* | There exists a unique functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ TermCat) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷)) | ||
| Theorem | fulltermc 49506* | A functor to a terminal category is full iff all hom-sets of the source category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ (𝑥𝐻𝑦) = ∅)) | ||
| Theorem | fulltermc2 49507 | Given a full functor to a terminal category, the source category must not have empty hom-sets. (Contributed by Zhi Wang, 17-Oct-2025.) (Proof shortened by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ¬ (𝑋𝐻𝑌) = ∅) | ||
| Theorem | termcterm 49508 | A terminal category is a terminal object of the category of small categories. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ TermCat) ⇒ ⊢ (𝜑 → 𝐶 ∈ (TermO‘𝐸)) | ||
| Theorem | termcterm2 49509 | A terminal object of the category of small categories is a terminal category. (Contributed by Zhi Wang, 18-Oct-2025.) (Proof shortened by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → (𝑈 ∩ TermCat) ≠ ∅) & ⊢ (𝜑 → 𝐶 ∈ (TermO‘𝐸)) ⇒ ⊢ (𝜑 → 𝐶 ∈ TermCat) | ||
| Theorem | termcterm3 49510 | In the category of small categories, a terminal object is equivalent to a terminal category. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → (SetCat‘1o) ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐶 ∈ TermCat ↔ 𝐶 ∈ (TermO‘𝐸))) | ||
| Theorem | termcciso 49511 | A category is isomorphic to a terminal category iff it itself is terminal. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ TermCat) ⇒ ⊢ (𝜑 → (𝑌 ∈ TermCat ↔ 𝑋( ≃𝑐 ‘𝐶)𝑌)) | ||
| Theorem | termccisoeu 49512* | The isomorphism between terminal categories is unique. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ TermCat) & ⊢ (𝜑 → 𝑌 ∈ TermCat) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝑋(Iso‘𝐶)𝑌)) | ||
| Theorem | termc2 49513* | If there exists a unique functor from both the category itself and the trivial category, then the category is terminal. Note that the converse also holds, so that it is a biconditional. See the proof of termc 49514 for hints. See also eufunc 49517 and euendfunc2 49522 for some insights on why two categories are sufficient. (Contributed by Zhi Wang, 18-Oct-2025.) (Proof shortened by Zhi Wang, 20-Oct-2025.) |
| ⊢ (∀𝑑 ∈ ({𝐶, (SetCat‘1o)} ∩ Cat)∃!𝑓 𝑓 ∈ (𝑑 Func 𝐶) → 𝐶 ∈ TermCat) | ||
| Theorem | termc 49514* | Alternate definition of TermCat. See also df-termc 49468. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ (𝐶 ∈ TermCat ↔ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝐶)) | ||
| Theorem | dftermc2 49515* | Alternate definition of TermCat. See also df-termc 49468 and dftermc3 49526. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ TermCat = {𝑐 ∣ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝑐)} | ||
| Theorem | eufunclem 49516* | If there exists a unique functor from a non-empty category, then the base of the target category is at most a singleton. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ 𝐵 = (Base‘𝐷) ⇒ ⊢ (𝜑 → 𝐵 ≼ 1o) | ||
| Theorem | eufunc 49517* | If there exists a unique functor from a non-empty category, then the base of the target category is a singleton. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ 𝐵 = (Base‘𝐷) ⇒ ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵) | ||
| Theorem | idfudiag1lem 49518 | Lemma for idfudiag1bas 49519 and idfudiag1 49520. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ (𝜑 → ( I ↾ 𝐴) = (𝐴 × {𝐵})) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → 𝐴 = {𝐵}) | ||
| Theorem | idfudiag1bas 49519 | If the identity functor of a category is the same as a constant functor to the category, then the base is a singleton. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐿 = (𝐶Δfunc𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋) & ⊢ (𝜑 → 𝐼 = 𝐾) ⇒ ⊢ (𝜑 → 𝐵 = {𝑋}) | ||
| Theorem | idfudiag1 49520 | If the identity functor of a category is the same as a constant functor to the category, then the category is terminal. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐿 = (𝐶Δfunc𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋) & ⊢ (𝜑 → 𝐼 = 𝐾) ⇒ ⊢ (𝜑 → 𝐶 ∈ TermCat) | ||
| Theorem | euendfunc 49521* | If there exists a unique endofunctor (a functor from a category to itself) for a non-empty category, then the category is terminal. This partially explains why two categories are sufficient in termc2 49513. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐶)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → 𝐶 ∈ TermCat) | ||
| Theorem | euendfunc2 49522 | If there exists a unique endofunctor (a functor from a category to itself) for a category, then it is either initial (empty) or terminal. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ ((𝐶 Func 𝐶) ≈ 1o → ((Base‘𝐶) = ∅ ∨ 𝐶 ∈ TermCat)) | ||
| Theorem | termcarweu 49523* | There exists a unique disjointified arrow in a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝐶 ∈ TermCat → ∃!𝑎 𝑎 ∈ (Arrow‘𝐶)) | ||
| Theorem | arweuthinc 49524* | If a structure has a unique disjointified arrow, then the structure is a thin category. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (∃!𝑎 𝑎 ∈ (Arrow‘𝐶) → 𝐶 ∈ ThinCat) | ||
| Theorem | arweutermc 49525* | If a structure has a unique disjointified arrow, then the structure is a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (∃!𝑎 𝑎 ∈ (Arrow‘𝐶) → 𝐶 ∈ TermCat) | ||
| Theorem | dftermc3 49526 | Alternate definition of TermCat. See also df-termc 49468, dftermc2 49515. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ TermCat = {𝑐 ∣ (Arrow‘𝑐) ≈ 1o} | ||
| Theorem | termcfuncval 49527 | The value of a functor from a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐶)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑋 = ((1st ‘𝐾)‘𝑌) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐴 ∧ 𝐾 = ⟨{⟨𝑌, 𝑋⟩}, {⟨⟨𝑌, 𝑌⟩, {⟨(𝐼‘𝑌), ( 1 ‘𝑋)⟩}⟩}⟩)) | ||
| Theorem | diag1f1olem 49528 | To any functor from a terminal category can an object in the target base be assigned. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐶)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑋 = ((1st ‘𝐾)‘𝑌) & ⊢ 𝐿 = (𝐶Δfunc𝐷) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐴 ∧ 𝐾 = ((1st ‘𝐿)‘𝑋))) | ||
| Theorem | diag1f1o 49529 | The object part of the diagonal functor is a bijection if 𝐷 is terminal. So any functor from a terminal category is one-to-one correspondent to an object of the target base. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐿 = (𝐶Δfunc𝐷) ⇒ ⊢ (𝜑 → (1st ‘𝐿):𝐴–1-1-onto→(𝐷 Func 𝐶)) | ||
| Theorem | termcnatval 49530 | Value of natural transformations for a terminal category. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑅 = (𝐴‘𝑋) ⇒ ⊢ (𝜑 → 𝐴 = {⟨𝑋, 𝑅⟩}) | ||
| Theorem | diag2f1olem 49531 | Lemma for diag2f1o 49532. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑁 = (𝐷 Nat 𝐶) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝑀 ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌))) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ 𝐹 = (𝑀‘𝑍) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑀 = ((𝑋(2nd ‘𝐿)𝑌)‘𝐹))) | ||
| Theorem | diag2f1o 49532 | If 𝐷 is terminal, the morphism part of a diagonal functor is bijective functions from hom-sets into sets of natural transformations. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑁 = (𝐷 Nat 𝐶) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝐿)𝑌):(𝑋𝐻𝑌)–1-1-onto→(((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌))) | ||
| Theorem | diagffth 49533 | The diagonal functor is a fully faithful functor from a category 𝐶 to the category of functors from a terminal category to 𝐶. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ 𝑄 = (𝐷 FuncCat 𝐶) & ⊢ 𝐿 = (𝐶Δfunc𝐷) ⇒ ⊢ (𝜑 → 𝐿 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))) | ||
| Theorem | diagciso 49534 |
The diagonal functor is an isomorphism from a category 𝐶 to the
category of functors from a terminal category to 𝐶.
It is provable that the inverse of the diagonal functor is the mapped object by the transposed curry of (𝐷 evalF 𝐶), i.e., ∪ ran (1st ‘(⟨𝐷, 𝑄⟩ curryF ((𝐷 evalF 𝐶) ∘func (𝐷 swapF 𝑄)))). (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ 𝑄 = (𝐷 FuncCat 𝐶) & ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝑄 ∈ 𝑈) & ⊢ 𝐼 = (Iso‘𝐸) & ⊢ 𝐿 = (𝐶Δfunc𝐷) ⇒ ⊢ (𝜑 → 𝐿 ∈ (𝐶𝐼𝑄)) | ||
| Theorem | diagcic 49535 | Any category 𝐶 is isomorphic to the category of functors from a terminal category to 𝐶. See also the "Properties" section of https://ncatlab.org/nlab/show/terminal+category. Therefore the number of categories isomorphic to a non-empty category is at least the number of singletons, so large (snnex 7694) that these isomorphic categories form a proper class. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ 𝑄 = (𝐷 FuncCat 𝐶) & ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝑄 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐶( ≃𝑐 ‘𝐸)𝑄) | ||
| Theorem | funcsn 49536 | The category of one functor to a thin category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → (𝐶 Func 𝐷) = {𝐹}) & ⊢ (𝜑 → 𝐷 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝑄 ∈ TermCat) | ||
| Theorem | fucterm 49537 | The category of functors to a terminal category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ TermCat) ⇒ ⊢ (𝜑 → 𝑄 ∈ TermCat) | ||
| Theorem | 0fucterm 49538 | The category of functors from an initial category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ∅ = (Base‘𝐶)) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) ⇒ ⊢ (𝜑 → 𝑄 ∈ TermCat) | ||
| Theorem | termfucterm 49539 | All functors between two terminal categories are isomorphisms. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ TermCat) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ TermCat) ⇒ ⊢ (𝜑 → (𝑋 Func 𝑌) = (𝑋𝐼𝑌)) | ||
| Theorem | cofuterm 49540 | Post-compose with a functor to a terminal category. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐾 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝐸 ∈ TermCat) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐾) | ||
| Theorem | uobeqterm 49541 | Universal objects and terminal categories. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐴 = (Base‘𝐷) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝐸 ∈ TermCat) ⇒ ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌)) | ||
| Theorem | isinito4 49542 | The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ (𝜑 → 1 ∈ TermCat) & ⊢ (𝜑 → 𝑋 ∈ (Base‘ 1 )) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 1 )) ⇒ ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ dom (𝐹(𝐶 UP 1 )𝑋))) | ||
| Theorem | isinito4a 49543 | The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ (𝜑 → 1 ∈ TermCat) & ⊢ (𝜑 → 𝑋 ∈ (Base‘ 1 )) & ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘𝑋) ⇒ ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ dom (𝐹(𝐶 UP 1 )𝑋))) | ||
| Syntax | cprstc 49544 | Class function defining preordered sets as categories. |
| class ProsetToCat | ||
| Definition | df-prstc 49545 |
Definition of the function converting a preordered set to a category.
Justified by prsthinc 49459.
This definition is somewhat arbitrary. Example 3.3(4.d) of [Adamek] p. 24 demonstrates an alternate definition with pairwise disjoint hom-sets. The behavior of the function is defined entirely, up to isomorphism (thincciso 49448), by prstcnid 49548, prstchom 49557, and prstcthin 49556. Other important properties include prstcbas 49549, prstcleval 49550, prstcle 49551, prstcocval 49552, prstcoc 49553, prstchom2 49558, and prstcprs 49555. Use those instead. Note that the defining property prstchom 49557 is equivalent to prstchom2 49558 given prstcthin 49556. See thincn0eu 49426 for justification. "ProsetToCat" was taken instead of "ProsetCat" because the latter might mean the category of preordered sets (classes). However, "ProsetToCat" seems too long. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
| ⊢ ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)) | ||
| Theorem | prstcval 49546 | Lemma for prstcnidlem 49547 and prstcthin 49556. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 = ((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)) | ||
| Theorem | prstcnidlem 49547 | Lemma for prstcnid 49548 and prstchomval 49554. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (comp‘ndx) ⇒ ⊢ (𝜑 → (𝐸‘𝐶) = (𝐸‘(𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩))) | ||
| Theorem | prstcnid 49548 | Components other than Hom and comp are unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (comp‘ndx) & ⊢ (𝐸‘ndx) ≠ (Hom ‘ndx) ⇒ ⊢ (𝜑 → (𝐸‘𝐾) = (𝐸‘𝐶)) | ||
| Theorem | prstcbas 49549 | The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) | ||
| Theorem | prstcleval 49550 | Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐾)) ⇒ ⊢ (𝜑 → ≤ = (le‘𝐶)) | ||
| Theorem | prstcle 49551 | Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐾)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌)) | ||
| Theorem | prstcocval 49552 | Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ⊥ = (oc‘𝐶)) | ||
| Theorem | prstcoc 49553 | Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋)) | ||
| Theorem | prstchomval 49554 | Hom-sets of the constructed category which depend on an arbitrary definition. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐶)) ⇒ ⊢ (𝜑 → ( ≤ × {1o}) = (Hom ‘𝐶)) | ||
| Theorem | prstcprs 49555 | The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
| Theorem | prstcthin 49556 | The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
| Theorem | prstchom 49557 |
Hom-sets of the constructed category are dependent on the preorder.
Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat. However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) | ||
| Theorem | prstchom2 49558* |
Hom-sets of the constructed category are dependent on the preorder.
Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat ( see prstchom2ALT 49559). However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 21-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌))) | ||
| Theorem | prstchom2ALT 49559* | Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 49545. See prstchom2 49558 for a version that does not depend on the definition. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌))) | ||
| Theorem | oduoppcbas 49560 | The dual of a preordered set and the opposite category have the same set of objects. (Contributed by Zhi Wang, 22-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → 𝐷 = (ProsetToCat‘(ODual‘𝐾))) & ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝜑 → (Base‘𝐷) = (Base‘𝑂)) | ||
| Theorem | oduoppcciso 49561 | The dual of a preordered set and the opposite category are category-isomorphic. Example 3.6(1) of [Adamek] p. 25. (Contributed by Zhi Wang, 22-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → 𝐷 = (ProsetToCat‘(ODual‘𝐾))) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → 𝑂 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐷( ≃𝑐 ‘(CatCat‘𝑈))𝑂) | ||
| Theorem | postcpos 49562 | The converted category is a poset iff the original proset is a poset. (Contributed by Zhi Wang, 26-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset)) | ||
| Theorem | postcposALT 49563 | Alternate proof of postcpos 49562. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset)) | ||
| Theorem | postc 49564* | The converted category is a poset iff no distinct objects are isomorphic. (Contributed by Zhi Wang, 25-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝐶 ∈ Poset ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥( ≃𝑐 ‘𝐶)𝑦 → 𝑥 = 𝑦))) | ||
| Theorem | discsntermlem 49565* | A singlegon is an element of the class of singlegons. The converse (basrestermcfolem 49566) also holds. This is trivial if 𝐵 is 𝑏 (abid 2711). (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (∃𝑥 𝐵 = {𝑥} → 𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}}) | ||
| Theorem | basrestermcfolem 49566* | An element of the class of singlegons is a singlegon. The converse (discsntermlem 49565) also holds. This is trivial if 𝐵 is 𝑏 (abid 2711). (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}} → ∃𝑥 𝐵 = {𝑥}) | ||
| Theorem | discbas 49567 | A discrete category (a category whose only morphisms are the identity morphisms) can be constructed for any base set. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩} & ⊢ 𝐶 = (ProsetToCat‘𝐾) ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐶)) | ||
| Theorem | discthin 49568 | A discrete category (a category whose only morphisms are the identity morphisms) is thin. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩} & ⊢ 𝐶 = (ProsetToCat‘𝐾) ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐶 ∈ ThinCat) | ||
| Theorem | discsnterm 49569* | A discrete category (a category whose only morphisms are the identity morphisms) with a singlegon base is terminal. Corollary of example 3.3(4)(c) of [Adamek] p. 24 and example 3.26(1) of [Adamek] p. 33. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩} & ⊢ 𝐶 = (ProsetToCat‘𝐾) ⇒ ⊢ (∃𝑥 𝐵 = {𝑥} → 𝐶 ∈ TermCat) | ||
| Theorem | basrestermcfo 49570* | The base function restricted to the class of terminal categories maps the class of terminal categories onto the class of singletons. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (Base ↾ TermCat):TermCat–onto→{𝑏 ∣ ∃𝑥 𝑏 = {𝑥}} | ||
| Theorem | termcnex 49571 | The class of all terminal categories is a proper class. Therefore both the class of all thin categories and the class of all categories are proper classes. Note that snnex 7694 is equivalent to sngl V ∉ V. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ TermCat ∉ V | ||
| Syntax | cmndtc 49572 | Class function defining monoids as categories. |
| class MndToCat | ||
| Definition | df-mndtc 49573 |
Definition of the function converting a monoid to a category. Example
3.3(4.e) of [Adamek] p. 24.
The definition of the base set is arbitrary. The whole extensible structure becomes the object here (see mndtcbasval 49575), instead of just the base set, as is the case in Example 3.3(4.e) of [Adamek] p. 24. The resulting category is defined entirely, up to isomorphism, by mndtcbas 49576, mndtchom 49579, mndtcco 49580. Use those instead. See example 3.26(3) of [Adamek] p. 33 for more on isomorphism. "MndToCat" was taken instead of "MndCat" because the latter might mean the category of monoids. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
| ⊢ MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩}) | ||
| Theorem | mndtcval 49574 | Value of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) ⇒ ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), {𝑀}⟩, ⟨(Hom ‘ndx), {⟨𝑀, 𝑀, (Base‘𝑀)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑀, 𝑀, 𝑀⟩, (+g‘𝑀)⟩}⟩}) | ||
| Theorem | mndtcbasval 49575 | The base set of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = {𝑀}) | ||
| Theorem | mndtcbas 49576* | The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) ⇒ ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵) | ||
| Theorem | mndtcob 49577 | Lemma for mndtchom 49579 and mndtcco 49580. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑀) | ||
| Theorem | mndtcbas2 49578 | Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
| Theorem | mndtchom 49579 | The only hom-set of the category built from a monoid is the base set of the monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (Proof shortened by Zhi Wang, 22-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (Base‘𝑀)) | ||
| Theorem | mndtcco 49580 | The composition of the category built from a monoid is the monoid operation. (Contributed by Zhi Wang, 22-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → · = (comp‘𝐶)) ⇒ ⊢ (𝜑 → (⟨𝑋, 𝑌⟩ · 𝑍) = (+g‘𝑀)) | ||
| Theorem | mndtcco2 49581 | The composition of the category built from a monoid is the monoid operation. (Contributed by Zhi Wang, 22-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝜑 → ⚬ = (⟨𝑋, 𝑌⟩ · 𝑍)) ⇒ ⊢ (𝜑 → (𝐺 ⚬ 𝐹) = (𝐺(+g‘𝑀)𝐹)) | ||
| Theorem | mndtccatid 49582* | Lemma for mndtccat 49583 and mndtcid 49584. (Contributed by Zhi Wang, 22-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ (0g‘𝑀)))) | ||
| Theorem | mndtccat 49583 | The function value is a category. (Contributed by Zhi Wang, 22-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | mndtcid 49584 | The identity morphism, or identity arrow, of the category built from a monoid is the identity element of the monoid. (Contributed by Zhi Wang, 22-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 1 = (Id‘𝐶)) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) = (0g‘𝑀)) | ||
| Theorem | oppgoppchom 49585 | The converted opposite monoid has the same hom-set as that of the opposite category. Example 3.6(2) of [Adamek] p. 25. (Contributed by Zhi Wang, 21-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐷 = (MndToCat‘(oppg‘𝑀))) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑂)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐷)) & ⊢ (𝜑 → 𝐽 = (Hom ‘𝑂)) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑋) = (𝑌𝐽𝑌)) | ||
| Theorem | oppgoppcco 49586 | The converted opposite monoid has the same composition as that of the opposite category. Example 3.6(2) of [Adamek] p. 25. (Contributed by Zhi Wang, 22-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐷 = (MndToCat‘(oppg‘𝑀))) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑂)) & ⊢ (𝜑 → · = (comp‘𝐷)) & ⊢ (𝜑 → ∙ = (comp‘𝑂)) ⇒ ⊢ (𝜑 → (⟨𝑋, 𝑋⟩ · 𝑋) = (⟨𝑌, 𝑌⟩ ∙ 𝑌)) | ||
| Theorem | oppgoppcid 49587 | The converted opposite monoid has the same identity morphism as that of the opposite category. Example 3.6(2) of [Adamek] p. 25. (Contributed by Zhi Wang, 22-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐷 = (MndToCat‘(oppg‘𝑀))) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑂)) ⇒ ⊢ (𝜑 → ((Id‘𝐷)‘𝑋) = ((Id‘𝑂)‘𝑌)) | ||
| Theorem | grptcmon 49588 | All morphisms in a category converted from a group are monomorphisms. (Contributed by Zhi Wang, 23-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝑀 = (Mono‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋𝐻𝑌)) | ||
| Theorem | grptcepi 49589 | All morphisms in a category converted from a group are epimorphisms. (Contributed by Zhi Wang, 23-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐸 = (Epi‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌)) | ||
| Theorem | 2arwcatlem1 49590 | Lemma for 2arwcat 49595. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ (𝑋𝐻𝑋) = { 0 , 1 } ⇒ ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))) ↔ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) | ||
| Theorem | 2arwcatlem2 49591 | Lemma for 2arwcat 49595. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝑋) & ⊢ (𝜑 → 𝐵 = 𝑌) & ⊢ (𝜑 → 𝐶 = 𝑍) & ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 )) & ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 ) & ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 0 ) = 0 ) ⇒ ⊢ (𝜑 → ( 1 (⟨𝐴, 𝐵⟩ · 𝐶)𝐹) = 𝐹) | ||
| Theorem | 2arwcatlem3 49592 | Lemma for 2arwcat 49595. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝑋) & ⊢ (𝜑 → 𝐵 = 𝑌) & ⊢ (𝜑 → 𝐶 = 𝑍) & ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 )) & ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 ) & ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 0 ) ⇒ ⊢ (𝜑 → (𝐹(⟨𝐴, 𝐵⟩ · 𝐶) 1 ) = 𝐹) | ||
| Theorem | 2arwcatlem4 49593 | Lemma for 2arwcat 49595. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝑋) & ⊢ (𝜑 → 𝐵 = 𝑌) & ⊢ (𝜑 → 𝐶 = 𝑍) & ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 )) & ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 ) & ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 0 ) & ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 0 ) = 0 ) & ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑌⟩ · 𝑍) 0 ) ∈ { 0 , 1 }) & ⊢ (𝜑 → (𝐺 = 0 ∨ 𝐺 = 1 )) ⇒ ⊢ (𝜑 → (𝐺(⟨𝐴, 𝐵⟩ · 𝐶)𝐹) ∈ { 0 , 1 }) | ||
| Theorem | 2arwcatlem5 49594 | Lemma for 2arwcat 49595. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ (𝜑 → ( 1 · 0 ) = 0 ) & ⊢ (𝜑 → ( 0 · 1 ) = 0 ) & ⊢ (𝜑 → ( 0 · 0 ) ∈ { 0 , 1 }) ⇒ ⊢ (𝜑 → (( 0 · 0 ) · 0 ) = ( 0 · ( 0 · 0 ))) | ||
| Theorem | 2arwcat 49595* | The condition for a structure with at most one object and at most two morphisms being a category. "2arwcat.2" to "2arwcat.5" are also necessary conditions if 𝑋, 0, and 1 are all sets, due to catlid 17589, catrid 17590, and catcocl 17591. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ (𝜑 → {𝑋} = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝑋𝐻𝑋) = { 0 , 1 } & ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑋⟩ · 𝑋) 1 ) = 1 ) & ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑋⟩ · 𝑋) 0 ) = 0 ) & ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑋⟩ · 𝑋) 1 ) = 0 ) & ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑋⟩ · 𝑋) 0 ) ∈ { 0 , 1 }) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ {𝑋} ↦ 1 ))) | ||
| Theorem | incat 49596* | Constructing a category with at most one object and at most two morphisms. If 𝑋 is a set then 𝐶 is the category 𝐴 in Exercise 3G of [Adamek] p. 45. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), {𝑋}⟩, ⟨(Hom ‘ndx), {⟨𝑋, 𝑋, 𝐻⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑋, 𝑋⟩, 𝑋, · ⟩}⟩} & ⊢ 𝐻 = {𝐹, 𝐺} & ⊢ · = (𝑓 ∈ 𝐻, 𝑔 ∈ 𝐻 ↦ (𝑓 ∩ 𝑔)) ⇒ ⊢ ((𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ {𝑋} ↦ 𝐺))) | ||
| Theorem | setc1onsubc 49597* | Construct a category with one object and two morphisms and prove that category (SetCat‘1o) satisfies all conditions for a subcategory but the compatibility of identity morphisms, showing the necessity of the latter condition in defining a subcategory. Exercise 4A of [Adamek] p. 58. (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), {∅}⟩, ⟨(Hom ‘ndx), {⟨∅, ∅, 2o⟩}⟩, ⟨(comp‘ndx), {⟨⟨∅, ∅⟩, ∅, · ⟩}⟩} & ⊢ · = (𝑓 ∈ 2o, 𝑔 ∈ 2o ↦ (𝑓 ∩ 𝑔)) & ⊢ 𝐸 = (SetCat‘1o) & ⊢ 𝐽 = (Homf ‘𝐸) & ⊢ 𝑆 = 1o & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝐷 = (𝐶 ↾cat 𝐽) ⇒ ⊢ (𝐶 ∈ Cat ∧ 𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat 𝐻 ∧ ¬ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)) | ||
| Theorem | cnelsubclem 49598* | Lemma for cnelsubc 49599. (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐽 ∈ V & ⊢ 𝑆 ∈ V & ⊢ (𝐶 ∈ Cat ∧ 𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)) ⇒ ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat)) | ||
| Theorem | cnelsubc 49599* | Remark 4.2(2) of [Adamek] p. 48. There exists a category satisfying all conditions for a subcategory but the compatibility of identity morphisms. Therefore such condition in df-subc 17719 is necessary. A stronger statement than nelsubc3 49066. (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat)) | ||
| Syntax | clan 49600 | Class function defining the (local) left Kan extension. |
| class Lan | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |