HomeTheorem List (p. 504 of 507)
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. 504 of 507) | < 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-31307) |
Hilbert Space Explorer
(31308-32830) |
Users' Mathboxes
(32831-50693) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | termcbasmo 50301 | Two objects in a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
| Theorem | termchomn0 50302 | All hom-sets of a terminal category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → ¬ (𝑋𝐻𝑌) = ∅) | ||
| Theorem | termchommo 50303 | All morphisms of a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑊)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
| Theorem | termcid 50304 | 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 50305 | 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 50306 | 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 50307 | 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 50308 | 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 50309 | The category (SetCat‘1o), i.e., the trivial category, is terminal. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ (SetCat‘1o) ∈ TermCat | ||
| Theorem | setc1obas 50310 | The base of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.) |
| ⊢ 1 = (SetCat‘1o) ⇒ ⊢ 1o = (Base‘ 1 ) | ||
| Theorem | setc1ohomfval 50311 | Set of morphisms of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.) |
| ⊢ 1 = (SetCat‘1o) ⇒ ⊢ {⟨∅, ∅, 1o⟩} = (Hom ‘ 1 ) | ||
| Theorem | setc1ocofval 50312 | Composition in the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.) |
| ⊢ 1 = (SetCat‘1o) ⇒ ⊢ {⟨⟨∅, ∅⟩, ∅, {⟨∅, ∅, ∅⟩}⟩} = (comp‘ 1 ) | ||
| Theorem | setc1oid 50313 | The identity morphism of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.) |
| ⊢ 1 = (SetCat‘1o) & ⊢ 𝐼 = (Id‘ 1 ) ⇒ ⊢ (𝐼‘∅) = ∅ | ||
| Theorem | funcsetc1ocl 50314 | The functor to the trivial category. The converse is also true due to reverse closure. (Contributed by Zhi Wang, 22-Oct-2025.) |
| ⊢ 1 = (SetCat‘1o) & ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘∅) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 1 )) | ||
| Theorem | funcsetc1o 50315* | Value of the functor to the trivial category. The converse is also true because 𝐹 would be the empty set if 𝐶 were not a category; and the empty set cannot equal an ordered pair of two sets. (Contributed by Zhi Wang, 22-Oct-2025.) |
| ⊢ 1 = (SetCat‘1o) & ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘∅) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐹 = ⟨(𝐵 × 1o), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × 1o))⟩) | ||
| Theorem | isinito2lem 50316 | The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 1 = (SetCat‘1o) & ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘∅) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼(𝐹(𝐶 UP 1 )∅)∅)) | ||
| Theorem | isinito2 50317 | The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 1 = (SetCat‘1o) & ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘∅) ⇒ ⊢ (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼(𝐹(𝐶 UP 1 )∅)∅) | ||
| Theorem | isinito3 50318 | The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 1 = (SetCat‘1o) & ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘∅) ⇒ ⊢ (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ dom (𝐹(𝐶 UP 1 )∅)) | ||
| Theorem | dfinito4 50319* | An alternate definition of df-inito 18066 using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects 18066. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ InitO = (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅)) | ||
| Theorem | dftermo4 50320* | An alternate definition of df-termo 18067 using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects 18067. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ TermO = (𝑐 ∈ Cat ↦ ⦋(oppCat‘𝑐) / 𝑜⦌⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑜))‘∅) / 𝑓⦌dom (𝑓(𝑜 UP 𝑑)∅)) | ||
| Theorem | termcpropd 50321 | 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 50322 | 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 50323 | 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 17793 and df-sets 17249. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ TermCat) ⇒ ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂)) | ||
| Theorem | oppcterm 50324 | The opposite category of a terminal category is a terminal category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ TermCat) ⇒ ⊢ (𝜑 → 𝑂 ∈ TermCat) | ||
| Theorem | functermclem 50325 | Lemma for functermc 50326. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ ((𝜑 ∧ 𝐾𝑅𝐿) → 𝐾 = 𝐹) & ⊢ (𝜑 → (𝐹𝑅𝐿 ↔ 𝐿 = 𝐺)) ⇒ ⊢ (𝜑 → (𝐾𝑅𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺))) | ||
| Theorem | functermc 50326* | Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝐹 = (𝐵 × 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) ⇒ ⊢ (𝜑 → (𝐾(𝐷 Func 𝐸)𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺))) | ||
| Theorem | functermc2 50327* | Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ TermCat) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝐹 = (𝐵 × 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) ⇒ ⊢ (𝜑 → (𝐷 Func 𝐸) = {⟨𝐹, 𝐺⟩}) | ||
| Theorem | functermceu 50328* | There exists a unique functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ TermCat) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷)) | ||
| Theorem | fulltermc 50329* | 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 50330 | 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 50331 | 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 50332 | 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 50333 | 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 50334 | 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 50335* | The isomorphism between terminal categories is unique. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ TermCat) & ⊢ (𝜑 → 𝑌 ∈ TermCat) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝑋(Iso‘𝐶)𝑌)) | ||
| Theorem | termc2 50336* | 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 50337 for hints. See also eufunc 50340 and euendfunc2 50345 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 50337* | Alternate definition of TermCat. See also df-termc 50291. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ (𝐶 ∈ TermCat ↔ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝐶)) | ||
| Theorem | dftermc2 50338* | Alternate definition of TermCat. See also df-termc 50291 and dftermc3 50349. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ TermCat = {𝑐 ∣ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝑐)} | ||
| Theorem | eufunclem 50339* | 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 50340* | 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 50341 | Lemma for idfudiag1bas 50342 and idfudiag1 50343. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ (𝜑 → ( I ↾ 𝐴) = (𝐴 × {𝐵})) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → 𝐴 = {𝐵}) | ||
| Theorem | idfudiag1bas 50342 | 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 50343 | 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 50344* | 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 50336. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐶)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → 𝐶 ∈ TermCat) | ||
| Theorem | euendfunc2 50345 | 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 50346* | There exists a unique disjointified arrow in a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝐶 ∈ TermCat → ∃!𝑎 𝑎 ∈ (Arrow‘𝐶)) | ||
| Theorem | arweuthinc 50347* | 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 50348* | 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 50349 | Alternate definition of TermCat. See also df-termc 50291, dftermc2 50338. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ TermCat = {𝑐 ∣ (Arrow‘𝑐) ≈ 1o} | ||
| Theorem | termcfuncval 50350 | 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 50351 | 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 50352 | 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 50353 | Value of natural transformations for a terminal category. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ TermCat) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑅 = (𝐴‘𝑋) ⇒ ⊢ (𝜑 → 𝐴 = {⟨𝑋, 𝑅⟩}) | ||
| Theorem | diag2f1olem 50354 | Lemma for diag2f1o 50355. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑁 = (𝐷 Nat 𝐶) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝑀 ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌))) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ 𝐹 = (𝑀‘𝑍) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑀 = ((𝑋(2nd ‘𝐿)𝑌)‘𝐹))) | ||
| Theorem | diag2f1o 50355 | 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 50356 | 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 50357 |
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 50358 | 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 7766) that these isomorphic categories form a proper class. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ 𝑄 = (𝐷 FuncCat 𝐶) & ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝑄 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐶( ≃𝑐 ‘𝐸)𝑄) | ||
| Theorem | funcsn 50359 | The category of one functor to a thin category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → (𝐶 Func 𝐷) = {𝐹}) & ⊢ (𝜑 → 𝐷 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝑄 ∈ TermCat) | ||
| Theorem | fucterm 50360 | The category of functors to a terminal category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ TermCat) ⇒ ⊢ (𝜑 → 𝑄 ∈ TermCat) | ||
| Theorem | 0fucterm 50361 | The category of functors from an initial category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ∅ = (Base‘𝐶)) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) ⇒ ⊢ (𝜑 → 𝑄 ∈ TermCat) | ||
| Theorem | termfucterm 50362 | All functors between two terminal categories are isomorphisms. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ TermCat) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ TermCat) ⇒ ⊢ (𝜑 → (𝑋 Func 𝑌) = (𝑋𝐼𝑌)) | ||
| Theorem | cofuterm 50363 | Post-compose with a functor to a terminal category. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐾 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝐸 ∈ TermCat) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐾) | ||
| Theorem | uobeqterm 50364 | Universal objects and terminal categories. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐴 = (Base‘𝐷) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝐷 ∈ TermCat) & ⊢ (𝜑 → 𝐸 ∈ TermCat) ⇒ ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌)) | ||
| Theorem | isinito4 50365 | 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 50366 | 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 50367 | Class function defining preordered sets as categories. |
| class ProsetToCat | ||
| Definition | df-prstc 50368 |
Definition of the function converting a preordered set to a category.
Justified by prsthinc 50282.
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 50271), by prstcnid 50371, prstchom 50380, and prstcthin 50379. Other important properties include prstcbas 50372, prstcleval 50373, prstcle 50374, prstcocval 50375, prstcoc 50376, prstchom2 50381, and prstcprs 50378. Use those instead. Note that the defining property prstchom 50380 is equivalent to prstchom2 50381 given prstcthin 50379. See thincn0eu 50249 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 50369 | Lemma for prstcnidlem 50370 and prstcthin 50379. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 = ((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)) | ||
| Theorem | prstcnidlem 50370 | Lemma for prstcnid 50371 and prstchomval 50377. (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 50371 | 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 50372 | The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) | ||
| Theorem | prstcleval 50373 | 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 50374 | Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐾)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌)) | ||
| Theorem | prstcocval 50375 | Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ⊥ = (oc‘𝐶)) | ||
| Theorem | prstcoc 50376 | Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋)) | ||
| Theorem | prstchomval 50377 | 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 50378 | The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
| Theorem | prstcthin 50379 | The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
| Theorem | prstchom 50380 |
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 50381* |
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 50382). 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 50382* | Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 50368. See prstchom2 50381 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 50383 | 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 50384 | 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 50385 | 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 50386 | Alternate proof of postcpos 50385. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset)) | ||
| Theorem | postc 50387* | 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 50388* | A singlegon is an element of the class of singlegons. The converse (basrestermcfolem 50389) also holds. This is trivial if 𝐵 is 𝑏 (abid 2748). (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (∃𝑥 𝐵 = {𝑥} → 𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}}) | ||
| Theorem | basrestermcfolem 50389* | An element of the class of singlegons is a singlegon. The converse (discsntermlem 50388) also holds. This is trivial if 𝐵 is 𝑏 (abid 2748). (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}} → ∃𝑥 𝐵 = {𝑥}) | ||
| Theorem | discbas 50390 | 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 50391 | 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 50392* | 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 50393* | 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 50394 | 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 7766 is equivalent to sngl V ∉ V. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ TermCat ∉ V | ||
| Syntax | cmndtc 50395 | Class function defining monoids as categories. |
| class MndToCat | ||
| Definition | df-mndtc 50396 |
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 50398), 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 50399, mndtchom 50402, mndtcco 50403. 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 50397 | 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 50398 | 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 50399* | The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) ⇒ ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵) | ||
| Theorem | mndtcob 50400 | Lemma for mndtchom 50402 and mndtcco 50403. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑀) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |