HomeTheorem List (p. 492 of 494)
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. 492 of 494) | < 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-30865) |
Hilbert Space Explorer
(30866-32388) |
Users' Mathboxes
(32389-49332) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | istermc3 49101 | The predicate "is a terminal category". A terminal category is a thin category whose base set is equinumerous to 1o. Consider en1b 9047, map1 9062, and euen1b 9050. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐶 ∈ TermCat ↔ (𝐶 ∈ ThinCat ∧ 𝐵 ≈ 1o)) | ||
| Theorem | termcthin 49102 | A terminal category is a thin category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝐶 ∈ TermCat → 𝐶 ∈ ThinCat) | ||
| Theorem | termcthind 49103 | A terminal category is a thin category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
| Theorem | termccd 49104 | A terminal category is a category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | termcbas 49105* | The base of a terminal category is a singleton. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → ∃𝑥 𝐵 = {𝑥}) | ||
| Theorem | termcbas2 49106 | The base of a terminal category is given by its object. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 = {𝑋}) | ||
| Theorem | termcbasmo 49107 | Two objects in a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
| Theorem | termchomn0 49108 | All hom-sets of a terminal category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → ¬ (𝑋𝐻𝑌) = ∅) | ||
| Theorem | termchommo 49109 | All morphisms of a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑊)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
| Theorem | termcid 49110 | The morphism of a terminal category is an identity morphism. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 𝐹 = ( 1 ‘𝑋)) | ||
| Theorem | termcid2 49111 | The morphism of a terminal category is an identity morphism. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 𝐹 = ( 1 ‘𝑌)) | ||
| Theorem | termchom 49112 | The hom-set of a terminal category is a singleton of the identity morphism. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = {( 1 ‘𝑋)}) | ||
| Theorem | termchom2 49113 | The hom-set of a terminal category is a singleton of the identity morphism. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = {( 1 ‘𝑍)}) | ||
| Theorem | setcsnterm 49114 | The category of one set, either a singleton set or an empty set, is terminal. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ (SetCat‘{{𝐴}}) ∈ TermCat | ||
| Theorem | setc1oterm 49115 | The category (SetCat‘1o), i.e., the trivial category, is terminal. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ (SetCat‘1o) ∈ TermCat | ||
| Theorem | termcpropd 49116 | Two structures with the same base, hom-sets and composition operation are either both terminal categories or neither. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐶 ∈ TermCat ↔ 𝐷 ∈ TermCat)) | ||
| Theorem | oppctermhom 49117 | The opposite category of a terminal category has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ TermCat) ⇒ ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂)) | ||
| Theorem | oppctermco 49118 | The opposite category of a terminal category has the same base, hom-sets and composition operation as the original category. Note that 𝐶 = 𝑂 cannot be proved because 𝐶 might not even be a function. For example, let 𝐶 be ({⟨(Base‘ndx), {∅}⟩, ⟨(Hom ‘ndx), ((V × V) × {{∅}})⟩} ∪ {⟨(comp‘ndx), {∅}⟩, ⟨(comp‘ndx), 2o⟩}); it should be a terminal category, but the opposite category is not itself. See the definitions df-oppc 17726 and df-sets 17183. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ TermCat) ⇒ ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂)) | ||
| Theorem | oppcterm 49119 | The opposite category of a terminal category is a terminal category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ TermCat) ⇒ ⊢ (𝜑 → 𝑂 ∈ TermCat) | ||
| Theorem | functermclem 49120 | Lemma for functermc 49121. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ ((𝜑 ∧ 𝐾𝑅𝐿) → 𝐾 = 𝐹) & ⊢ (𝜑 → (𝐹𝑅𝐿 ↔ 𝐿 = 𝐺)) ⇒ ⊢ (𝜑 → (𝐾𝑅𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺))) | ||
| Theorem | functermc 49121* | Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝐹 = (𝐵 × 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) ⇒ ⊢ (𝜑 → (𝐾(𝐷 Func 𝐸)𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺))) | ||
| Theorem | functermc2 49122* | Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝐹 = (𝐵 × 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) ⇒ ⊢ (𝜑 → (𝐷 Func 𝐸) = {⟨𝐹, 𝐺⟩}) | ||
| Theorem | functermceu 49123* | There exists a unique functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ TermCat) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷)) | ||
| Theorem | fulltermc 49124* | 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 49125 | Given a full functor to a terminal category, the source category must not have empty hom-sets. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ¬ (𝑋𝐻𝑌) = ∅) | ||
| Theorem | termcterm 49126 | 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 49127 | A terminal object of the category of small categories is a terminal category. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → (𝑈 ∩ TermCat) ≠ ∅) & ⊢ (𝜑 → 𝐶 ∈ (TermO‘𝐸)) ⇒ ⊢ (𝜑 → 𝐶 ∈ TermCat) | ||
| Theorem | termcterm3 49128 | 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 | termc2 49129* | 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 49130 for hints. See also eufunc 49133 and euendfunc2 49138 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 49130* | Alternate definition of TermCat. See also df-termc 49098. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ (𝐶 ∈ TermCat ↔ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝐶)) | ||
| Theorem | dftermc2 49131* | Alternate definition of TermCat. See also df-termc 49098 and dftermc3 49142. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ TermCat = {𝑐 ∣ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝑐)} | ||
| Theorem | eufunclem 49132* | 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 49133* | 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 49134 | Lemma for idfudiag1bas 49135 and idfudiag1 49136. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ (𝜑 → ( I ↾ 𝐴) = (𝐴 × {𝐵})) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → 𝐴 = {𝐵}) | ||
| Theorem | idfudiag1bas 49135 | 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 49136 | 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 49137* | 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 49129. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐶)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → 𝐶 ∈ TermCat) | ||
| Theorem | euendfunc2 49138 | 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 49139* | There exists a unique disjointified arrow in a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝐶 ∈ TermCat → ∃!𝑎 𝑎 ∈ (Arrow‘𝐶)) | ||
| Theorem | arweuthinc 49140* | 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 49141* | 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 49142 | Alternate definition of TermCat. See also df-termc 49098, dftermc2 49131. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ TermCat = {𝑐 ∣ (Arrow‘𝑐) ≈ 1o} | ||
| Theorem | termcfuncval 49143 | 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 49144 | 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 49145 | 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 49146 | Value of natural transformations for a terminal category. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑅 = (𝐴‘𝑋) ⇒ ⊢ (𝜑 → 𝐴 = {⟨𝑋, 𝑅⟩}) | ||
| Theorem | diag2f1olem 49147 | Lemma for diag2f1o 49148. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑁 = (𝐷 Nat 𝐶) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝑀 ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌))) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ 𝐹 = (𝑀‘𝑍) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑀 = ((𝑋(2nd ‘𝐿)𝑌)‘𝐹))) | ||
| Theorem | diag2f1o 49148 | 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 49149 | 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 49150 |
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 49151 | Any category 𝐶 is isomorphic to the category of functors from a terminal category to 𝐶. Therefore the number of categories isomorphic to a non-empty category is at least the number of singletons, so large (snnex 7760) that these isomorphic categories form a proper class. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ 𝑄 = (𝐷 FuncCat 𝐶) & ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝑄 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐶( ≃𝑐 ‘𝐸)𝑄) | ||
| Syntax | cprstc 49152 | Class function defining preordered sets as categories. |
| class ProsetToCat | ||
| Definition | df-prstc 49153 |
Definition of the function converting a preordered set to a category.
Justified by prsthinc 49089.
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 49080), by prstcnid 49156, prstchom 49167, and prstcthin 49166. Other important properties include prstcbas 49157, prstcleval 49158, prstcle 49160, prstcocval 49161, prstcoc 49163, prstchom2 49168, and prstcprs 49165. Use those instead. Note that the defining property prstchom 49167 is equivalent to prstchom2 49168 given prstcthin 49166. See thincn0eu 49058 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 49154 | Lemma for prstcnidlem 49155 and prstcthin 49166. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 = ((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)) | ||
| Theorem | prstcnidlem 49155 | Lemma for prstcnid 49156 and prstchomval 49164. (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 49156 | 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 49157 | The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) | ||
| Theorem | prstcleval 49158 | 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 | prstclevalOLD 49159 | Obsolete proof of prstcleval 49158 as of 12-Nov-2024. Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐾)) ⇒ ⊢ (𝜑 → ≤ = (le‘𝐶)) | ||
| Theorem | prstcle 49160 | Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐾)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌)) | ||
| Theorem | prstcocval 49161 | Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ⊥ = (oc‘𝐶)) | ||
| Theorem | prstcocvalOLD 49162 | Obsolete proof of prstcocval 49161 as of 12-Nov-2024. Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ⊥ = (oc‘𝐶)) | ||
| Theorem | prstcoc 49163 | Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋)) | ||
| Theorem | prstchomval 49164 | 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 49165 | The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
| Theorem | prstcthin 49166 | The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
| Theorem | prstchom 49167 |
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 49168* |
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 49169). 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 49169* | Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 49153. See prstchom2 49168 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 49170 | 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 49171 | 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 49172 | 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 49173 | Alternate proof of postcpos 49172. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset)) | ||
| Theorem | postc 49174* | 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 49175* | A singlegon is an element of the class of singlegons. The converse (basrestermcfolem 49176) also holds. This is trivial if 𝐵 is 𝑏 (abid 2716). (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (∃𝑥 𝐵 = {𝑥} → 𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}}) | ||
| Theorem | basrestermcfolem 49176* | An element of the class of singlegons is a singlegon. The converse (discsntermlem 49175) also holds. This is trivial if 𝐵 is 𝑏 (abid 2716). (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}} → ∃𝑥 𝐵 = {𝑥}) | ||
| Theorem | discbas 49177 | 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 49178 | 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 49179* | A discrete category (a category whose only morphisms are the identity morphisms) with a singlegon base is terminal. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩} & ⊢ 𝐶 = (ProsetToCat‘𝐾) ⇒ ⊢ (∃𝑥 𝐵 = {𝑥} → 𝐶 ∈ TermCat) | ||
| Theorem | basrestermcfo 49180* | 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 49181 | 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 7760 is equivalent to sngl V ∉ V. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ TermCat ∉ V | ||
| Syntax | cmndtc 49182 | Class function defining monoids as categories. |
| class MndToCat | ||
| Definition | df-mndtc 49183 |
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 49185), 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 49186, mndtchom 49189, mndtcco 49190. 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 49184 | 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 49185 | 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 49186* | The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) ⇒ ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵) | ||
| Theorem | mndtcob 49187 | Lemma for mndtchom 49189 and mndtcco 49190. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑀) | ||
| Theorem | mndtcbas2 49188 | Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
| Theorem | mndtchom 49189 | 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.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (Base‘𝑀)) | ||
| Theorem | mndtcco 49190 | 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 49191 | 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 49192* | Lemma for mndtccat 49193 and mndtcid 49194. (Contributed by Zhi Wang, 22-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ (0g‘𝑀)))) | ||
| Theorem | mndtccat 49193 | The function value is a category. (Contributed by Zhi Wang, 22-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | mndtcid 49194 | 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 49195 | 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 49196 | 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 49197 | 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 49198 | 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 49199 | All morphisms in a category converted from a group are epimorphisms. (Contributed by Zhi Wang, 23-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐸 = (Epi‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌)) | ||
Some of these theorems are used in the series of lemmas and theorems proving the defining properties of setrecs. | ||
| Theorem | nfintd 49200 | Bound-variable hypothesis builder for intersection. (Contributed by Emmett Weisz, 16-Jan-2020.) |
| ⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∩ 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |