HomeTheorem List (p. 504 of 509)
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 509) | < 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-31407) |
Hilbert Space Explorer
(31408-32930) |
Users' Mathboxes
(32931-50831) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | precofval 50301* | Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅)))) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹)) ⇒ ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐷 Func 𝐸) ↦ (𝑔 ∘func 𝐹)), (𝑔 ∈ (𝐷 Func 𝐸), ℎ ∈ (𝐷 Func 𝐸) ↦ (𝑎 ∈ (𝑔(𝐷 Nat 𝐸)ℎ) ↦ (𝑥 ∈ (Base‘𝐶) ↦ (𝑎‘((1st ‘𝐹)‘𝑥)))))⟩) | ||
| Theorem | precofvalALT 50302* | Alternate proof of precofval 50301. (Contributed by Zhi Wang, 11-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅)))) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹)) ⇒ ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐷 Func 𝐸) ↦ (𝑔 ∘func 𝐹)), (𝑔 ∈ (𝐷 Func 𝐸), ℎ ∈ (𝐷 Func 𝐸) ↦ (𝑎 ∈ (𝑔(𝐷 Nat 𝐸)ℎ) ↦ (𝑥 ∈ (Base‘𝐶) ↦ (𝑎‘((1st ‘𝐹)‘𝑥)))))⟩) | ||
| Theorem | precofval2 50303* | Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅)))) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹)) ⇒ ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐷 Func 𝐸) ↦ (𝑔 ∘func 𝐹)), (𝑔 ∈ (𝐷 Func 𝐸), ℎ ∈ (𝐷 Func 𝐸) ↦ (𝑎 ∈ (𝑔(𝐷 Nat 𝐸)ℎ) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩) | ||
| Theorem | precofcl 50304 | The pre-composition functor as a transposed curry of the functor composition bifunctor is a functor. (Contributed by Zhi Wang, 11-Oct-2025.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅)))) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹)) & ⊢ 𝑆 = (𝐶 FuncCat 𝐸) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝑅 Func 𝑆)) | ||
| Theorem | precofval3 50305* | Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ 𝐵 = (𝐷 Func 𝐸) & ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐾 = (𝑔 ∈ 𝐵 ↦ (𝑔 ∘func ⟨𝐹, 𝐺⟩))) & ⊢ (𝜑 → 𝐿 = (𝑔 ∈ 𝐵, ℎ ∈ 𝐵 ↦ (𝑎 ∈ (𝑔𝑁ℎ) ↦ (𝑎 ∘ 𝐹)))) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅)))) & ⊢ (𝜑 → 𝑀 = ((1st ‘ ⚬ )‘⟨𝐹, 𝐺⟩)) ⇒ ⊢ (𝜑 → ⟨𝐾, 𝐿⟩ = 𝑀) | ||
| Theorem | precoffunc 50306* | The pre-composition functor, expressed explicitly, is a functor. (Contributed by Zhi Wang, 11-Oct-2025.) (Proof shortened by Zhi Wang, 20-Oct-2025.) |
| ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ 𝐵 = (𝐷 Func 𝐸) & ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐾 = (𝑔 ∈ 𝐵 ↦ (𝑔 ∘func ⟨𝐹, 𝐺⟩))) & ⊢ (𝜑 → 𝐿 = (𝑔 ∈ 𝐵, ℎ ∈ 𝐵 ↦ (𝑎 ∈ (𝑔𝑁ℎ) ↦ (𝑎 ∘ 𝐹)))) & ⊢ 𝑆 = (𝐶 FuncCat 𝐸) ⇒ ⊢ (𝜑 → 𝐾(𝑅 Func 𝑆)𝐿) | ||
| Syntax | cprcof 50307 | Extend class notation with pre-composition functors. |
| class −∘F | ||
| Definition | df-prcof 50308* |
Definition of pre-composition functors. The object part of the
pre-composition functor given by 𝐹 pre-composes a functor with
𝐹; the morphism part pre-composes a natural transformation with the
object part of 𝐹, in terms of function composition. Comments
before the definition in
§
3 of Chapter X in p. 236 of
Mac Lane, Saunders, Categories for the Working Mathematician, 2nd
Edition, Springer Science+Business Media, New York, (1998)
[QA169.M33 1998]; available at
https://math.mit.edu/~hrm/palestine/maclane-categories.pdf
(retrieved
3 Nov 2025). The notation −∘F is inspired by this page:
https://1lab.dev/Cat.Functor.Compose.html.
The pre-composition functor can also be defined as a transposed curry of the functor composition bifunctor (precofval3 50305). But such definition requires an explicit third category. prcoftposcurfuco 50317 and prcoftposcurfucoa 50318 prove the equivalence. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ −∘F = (𝑝 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑑⦌⦋(2nd ‘𝑝) / 𝑒⦌⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩) | ||
| Theorem | reldmprcof 50309 | The domain of −∘F is a relation. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ Rel dom −∘F | ||
| Theorem | prcofvalg 50310* | Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝐵 = (𝐷 Func 𝐸) & ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐹 ∈ 𝑈) & ⊢ (𝜑 → 𝑃 ∈ 𝑉) & ⊢ (𝜑 → (1st ‘𝑃) = 𝐷) & ⊢ (𝜑 → (2nd ‘𝑃) = 𝐸) ⇒ ⊢ (𝜑 → (𝑃 −∘F 𝐹) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func 𝐹)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩) | ||
| Theorem | prcofvala 50311* | Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝐵 = (𝐷 Func 𝐸) & ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝑈) ⇒ ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func 𝐹)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩) | ||
| Theorem | prcofval 50312* | Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝐵 = (𝐷 Func 𝐸) & ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ Rel 𝑅 & ⊢ (𝜑 → 𝐹𝑅𝐺) ⇒ ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func ⟨𝐹, 𝐺⟩)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ 𝐹)))⟩) | ||
| Theorem | prcofpropd 50313 | If the categories have the same set of objects, morphisms, and compositions, then they have the same pre-composition functors. (Contributed by Zhi Wang, 21-Nov-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) ⇒ ⊢ (𝜑 → (⟨𝐴, 𝐶⟩ −∘F 𝐹) = (⟨𝐵, 𝐷⟩ −∘F 𝐹)) | ||
| Theorem | prcofelvv 50314 | The pre-composition functor is an ordered pair. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑈) & ⊢ (𝜑 → 𝑃 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑃 −∘F 𝐹) ∈ (V × V)) | ||
| Theorem | reldmprcof1 50315 | The domain of the object part of the pre-composition functor is a relation. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ Rel dom (1st ‘(𝑃 −∘F 𝐹)) | ||
| Theorem | reldmprcof2 50316 | The domain of the morphism part of the pre-composition functor is a relation. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ Rel dom (2nd ‘(𝑃 −∘F 𝐹)) | ||
| Theorem | prcoftposcurfuco 50317 | The pre-composition functor is the transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅)))) & ⊢ (𝜑 → 𝑀 = ((1st ‘ ⚬ )‘⟨𝐹, 𝐺⟩)) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) = 𝑀) | ||
| Theorem | prcoftposcurfucoa 50318 | The pre-composition functor is the transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅)))) & ⊢ (𝜑 → 𝑀 = ((1st ‘ ⚬ )‘𝐹)) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = 𝑀) | ||
| Theorem | prcoffunc 50319 | The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ 𝑆 = (𝐶 FuncCat 𝐸) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) ∈ (𝑅 Func 𝑆)) | ||
| Theorem | prcoffunca 50320 | The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ 𝑆 = (𝐶 FuncCat 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) ∈ (𝑅 Func 𝑆)) | ||
| Theorem | prcoffunca2 50321 | The pre-composition functor is a functor. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ 𝑆 = (𝐶 FuncCat 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐾, 𝐿⟩) ⇒ ⊢ (𝜑 → 𝐾(𝑅 Func 𝑆)𝐿) | ||
| Theorem | prcof1 50322 | The object part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → (1st ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑂) ⇒ ⊢ (𝜑 → (𝑂‘𝐾) = (𝐾 ∘func 𝐹)) | ||
| Theorem | prcof2a 50323* | The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.) |
| ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐾𝑃𝐿) = (𝑎 ∈ (𝐾𝑁𝐿) ↦ (𝑎 ∘ (1st ‘𝐹)))) | ||
| Theorem | prcof2 50324* | The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.) |
| ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩)) = 𝑃) & ⊢ Rel 𝑅 & ⊢ (𝜑 → 𝐹𝑅𝐺) ⇒ ⊢ (𝜑 → (𝐾𝑃𝐿) = (𝑎 ∈ (𝐾𝑁𝐿) ↦ (𝑎 ∘ 𝐹))) | ||
| Theorem | prcof21a 50325 | The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.) |
| ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐴 ∈ (𝐾𝑁𝐿)) & ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐾𝑃𝐿)‘𝐴) = (𝐴 ∘ (1st ‘𝐹))) | ||
| Theorem | prcof22a 50326 | The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.) |
| ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐴 ∈ (𝐾𝑁𝐿)) & ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (((𝐾𝑃𝐿)‘𝐴)‘𝑋) = (𝐴‘((1st ‘𝐹)‘𝑋))) | ||
| Theorem | prcofdiag1 50327 | A constant functor pre-composed by a functor is another constant functor. (Contributed by Zhi Wang, 25-Nov-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝑀 = (𝐶Δfunc𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐸 Func 𝐷)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((1st ‘𝐿)‘𝑋) ∘func 𝐹) = ((1st ‘𝑀)‘𝑋)) | ||
| Theorem | prcofdiag 50328 | A diagonal functor post-composed by a pre-composition functor is another diagonal functor. (Contributed by Zhi Wang, 25-Nov-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝑀 = (𝐶Δfunc𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐸 Func 𝐷)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → (⟨𝐷, 𝐶⟩ −∘F 𝐹) = 𝐺) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐿) = 𝑀) | ||
| Theorem | catcrcl 50329 | Reverse closure for the category of categories (in a universe) (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → 𝑈 ∈ V) | ||
| Theorem | catcrcl2 50330 | Reverse closure for the category of categories (in a universe) (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | elcatchom 50331 | A morphism of the category of categories (in a universe) is a functor. See df-catc 18194 for the definition of the category Cat, which consists of all categories in the universe 𝑢 (i.e., "𝑢-small categories", see Definition 3.44. of [Adamek] p. 39), with functors as the morphisms (catchom 18198). (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑋 Func 𝑌)) | ||
| Theorem | catcsect 50332 | The property "𝐹 is a section of 𝐺 " in a category of small categories (in a universe). (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (idfunc‘𝑋) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝐹(𝑋𝑆𝑌)𝐺 ↔ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑋)) ∧ (𝐺 ∘func 𝐹) = 𝐼)) | ||
| Theorem | catcinv 50333 | The property "𝐹 is an inverse of 𝐺 " in a category of small categories (in a universe). (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (idfunc‘𝑋) & ⊢ 𝐽 = (idfunc‘𝑌) ⇒ ⊢ (𝐹(𝑋𝑁𝑌)𝐺 ↔ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑋)) ∧ ((𝐺 ∘func 𝐹) = 𝐼 ∧ (𝐹 ∘func 𝐺) = 𝐽))) | ||
| Theorem | catcisoi 50334 | A functor is an isomorphism of categories only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in [Adamek] p. 34. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝑅 = (Base‘𝑋) & ⊢ 𝑆 = (Base‘𝑌) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) | ||
| Theorem | uobeq2 50335 | If a full functor (in fact, a full embedding) is a section, then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ 𝑄 = (CatCat‘𝑈) & ⊢ 𝑆 = (Sect‘𝑄) & ⊢ (𝜑 → 𝐾 ∈ (𝐷 Full 𝐸)) & ⊢ (𝜑 → 𝐾 ∈ dom (𝐷𝑆𝐸)) ⇒ ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌)) | ||
| Theorem | uobeq3 50336 | An isomorphism between categories generates equal sets of universal objects. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ 𝑄 = (CatCat‘𝑈) & ⊢ 𝐼 = (Iso‘𝑄) & ⊢ (𝜑 → 𝐾 ∈ (𝐷𝐼𝐸)) ⇒ ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌)) | ||
| Theorem | opf11 50337 | The object part of the op functor on functor categories. Lemma for fucoppc 50344. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (1st ‘(𝐹‘𝑋)) = (1st ‘𝑋)) | ||
| Theorem | opf12 50338 | The object part of the op functor on functor categories. Lemma for oppfdiag 50350. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝑀(2nd ‘(𝐹‘𝑋))𝑁) = (𝑁(2nd ‘𝑋)𝑀)) | ||
| Theorem | opf2fval 50339* | The morphism part of the op functor on functor categories. Lemma for fucoppc 50344. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑦𝑁𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐹𝑌) = ( I ↾ (𝑌𝑁𝑋))) | ||
| Theorem | opf2 50340* | The morphism part of the op functor on functor categories. Lemma for fucoppc 50344. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑦𝑁𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐷 ∈ (𝑌𝑁𝑋)) ⇒ ⊢ (𝜑 → ((𝑋𝐹𝑌)‘𝐶) = 𝐷) | ||
| Theorem | fucoppclem 50341 | Lemma for fucoppc 50344. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝑌𝑁𝑋) = ((𝐹‘𝑋)(𝑂 Nat 𝑃)(𝐹‘𝑌))) | ||
| Theorem | fucoppcid 50342* | The opposite category of functors is compatible with the category of opposite functors in terms of identity morphism. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (oppCat‘𝑄) & ⊢ 𝑆 = (𝑂 FuncCat 𝑃) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐶 Func 𝐷), 𝑦 ∈ (𝐶 Func 𝐷) ↦ ( I ↾ (𝑦𝑁𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑋)‘((Id‘𝑅)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋))) | ||
| Theorem | fucoppcco 50343* | The opposite category of functors is compatible with the category of opposite functors in terms of composition. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (oppCat‘𝑄) & ⊢ 𝑆 = (𝑂 FuncCat 𝑃) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐶 Func 𝐷), 𝑦 ∈ (𝐶 Func 𝐷) ↦ ( I ↾ (𝑦𝑁𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ (𝑋(Hom ‘𝑅)𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑌(Hom ‘𝑅)𝑍)) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑍)‘(𝐵(⟨𝑋, 𝑌⟩(comp‘𝑅)𝑍)𝐴)) = (((𝑌𝐺𝑍)‘𝐵)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐴))) | ||
| Theorem | fucoppc 50344* | The isomorphism from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (oppCat‘𝑄) & ⊢ 𝑆 = (𝑂 FuncCat 𝑃) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐶 Func 𝐷), 𝑦 ∈ (𝐶 Func 𝐷) ↦ ( I ↾ (𝑦𝑁𝑥)))) & ⊢ 𝑇 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐼 = (Iso‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐹(𝑅𝐼𝑆)𝐺) | ||
| Theorem | fucoppcffth 50345* | A fully faithful functor from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (oppCat‘𝑄) & ⊢ 𝑆 = (𝑂 FuncCat 𝑃) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐶 Func 𝐷), 𝑦 ∈ (𝐶 Func 𝐷) ↦ ( I ↾ (𝑦𝑁𝑥)))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐹((𝑅 Full 𝑆) ∩ (𝑅 Faith 𝑆))𝐺) | ||
| Theorem | fucoppcfunc 50346* | A functor from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (oppCat‘𝑄) & ⊢ 𝑆 = (𝑂 FuncCat 𝑃) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐶 Func 𝐷), 𝑦 ∈ (𝐶 Func 𝐷) ↦ ( I ↾ (𝑦𝑁𝑥)))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) | ||
| Theorem | fucoppccic 50347 | The opposite category of functors is isomorphic to the category of opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑋 = (oppCat‘(𝐷 FuncCat 𝐸)) & ⊢ 𝑌 = ((oppCat‘𝐷) FuncCat (oppCat‘𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌) | ||
| Theorem | oppfdiag1 50348 | A constant functor for opposite categories is the opposite functor of the constant functor for original categories. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐷 Func 𝐶))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘((1st ‘𝐿)‘𝑋)) = ((1st ‘(𝑂Δfunc𝑃))‘𝑋)) | ||
| Theorem | oppfdiag1a 50349 | A constant functor for opposite categories is the opposite functor of the constant functor for original categories. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ( oppFunc ‘((1st ‘𝐿)‘𝑋)) = ((1st ‘(𝑂Δfunc𝑃))‘𝑋)) | ||
| Theorem | oppfdiag 50350* | A diagonal functor for opposite categories is the opposite functor of the diagonal functor for original categories post-composed by an isomorphism (fucoppc 50344). (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐷 Func 𝐶))) & ⊢ 𝑁 = (𝐷 Nat 𝐶) & ⊢ (𝜑 → 𝐺 = (𝑚 ∈ (𝐷 Func 𝐶), 𝑛 ∈ (𝐷 Func 𝐶) ↦ ( I ↾ (𝑛𝑁𝑚)))) ⇒ ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘func ( oppFunc ‘𝐿)) = (𝑂Δfunc𝑃)) | ||
| Syntax | cthinc 50351 | Extend class notation with the class of thin categories. |
| class ThinCat | ||
| Definition | df-thinc 50352* | Definition of the class of thin categories, or posetal categories, whose hom-sets each contain at most one morphism. Example 3.26(2) of [Adamek] p. 33. "ThinCat" was taken instead of "PosCat" because the latter might mean the category of posets. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ ThinCat = {𝑐 ∈ Cat ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)} | ||
| Theorem | isthinc 50353* | The predicate "is a thin category". (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))) | ||
| Theorem | isthinc2 50354* | A thin category is a category in which all hom-sets have cardinality less than or equal to the cardinality of 1o. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ≼ 1o)) | ||
| Theorem | isthinc3 50355* | A thin category is a category in which, given a pair of objects 𝑥 and 𝑦 and any two morphisms 𝑓, 𝑔 from 𝑥 to 𝑦, the morphisms are equal. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑥𝐻𝑦)𝑓 = 𝑔)) | ||
| Theorem | thincc 50356 | A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ (𝐶 ∈ ThinCat → 𝐶 ∈ Cat) | ||
| Theorem | thinccd 50357 | A thin category is a category (deduction form). (Contributed by Zhi Wang, 24-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | thincssc 50358 | A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ ThinCat ⊆ Cat | ||
| Theorem | isthincd2lem1 50359* | Lemma for isthincd2 50371 and thincmo2 50360. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
| Theorem | thincmo2 50360 | Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
| Theorem | thinchom 50361 | A non-empty hom-set of a thin category is given by its element. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ ThinCat) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = {𝐹}) | ||
| Theorem | thincmo 50362* | There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌)) | ||
| Theorem | thincmoALT 50363* | Alternate proof of thincmo 50362. (Contributed by Zhi Wang, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌)) | ||
| Theorem | thincmod 50364* | At most one morphism in each hom-set (deduction form). (Contributed by Zhi Wang, 21-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) ⇒ ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌)) | ||
| Theorem | thincn0eu 50365* | In a thin category, a hom-set being non-empty is equivalent to having a unique element. (Contributed by Zhi Wang, 21-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) ⇒ ⊢ (𝜑 → ((𝑋𝐻𝑌) ≠ ∅ ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌))) | ||
| Theorem | thincid 50366 | In a thin category, a morphism from an object to itself is an identity morphism. (Contributed by Zhi Wang, 24-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑋)) ⇒ ⊢ (𝜑 → 𝐹 = ( 1 ‘𝑋)) | ||
| Theorem | thincmon 50367 | In a thin category, all morphisms are monomorphisms. Example 7.33(9) of [Adamek] p. 110. The converse does not hold. See grptcmon 50527. (Contributed by Zhi Wang, 24-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑀 = (Mono‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋𝐻𝑌)) | ||
| Theorem | thincepi 50368 | In a thin category, all morphisms are epimorphisms. The converse does not hold. See grptcepi 50528. (Contributed by Zhi Wang, 24-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐸 = (Epi‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌)) | ||
| Theorem | isthincd2lem2 50369* | Lemma for isthincd2 50371. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ⇒ ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)) | ||
| Theorem | isthincd 50370* | The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
| Theorem | isthincd2 50371* | The predicate "𝐶 is a thin category" without knowing 𝐶 is a category (deduction form). The identity arrow operator is also provided as a byproduct. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)))) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1 ∈ (𝑦𝐻𝑦)) & ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ⇒ ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))) | ||
| Theorem | oppcthin 50372 | The opposite category of a thin category is thin. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat) | ||
| Theorem | oppcthinco 50373 | If the opposite category of a thin category has the same base and hom-sets as the original category, then it has the same composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂)) ⇒ ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂)) | ||
| Theorem | oppcthinendc 50374* | The opposite category of a thin category whose morphisms are all endomorphisms has the same base, hom-sets (oppcendc 49952) and composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅)) ⇒ ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂)) | ||
| Theorem | oppcthinendcALT 50375* | Alternate proof of oppcthinendc 50374. (Contributed by Zhi Wang, 16-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅)) ⇒ ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂)) | ||
| Theorem | thincpropd 50376 | Two structures with the same base, hom-sets and composition operation are either both thin categories or neither. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐶 ∈ ThinCat ↔ 𝐷 ∈ ThinCat)) | ||
| Theorem | subthinc 50377 | A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝐷 ∈ ThinCat) | ||
| Theorem | functhinclem1 50378* | Lemma for functhinc 50382. Given the object part, there is only one possible morphism part such that the mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ ThinCat) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) & ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅)) ⇒ ⊢ (𝜑 → ((𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝐺𝑤):(𝑧𝐻𝑤)⟶((𝐹‘𝑧)𝐽(𝐹‘𝑤))) ↔ 𝐺 = 𝐾)) | ||
| Theorem | functhinclem2 50379* | Lemma for functhinc 50382. (Contributed by Zhi Wang, 1-Oct-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅ → (𝑥𝐻𝑦) = ∅)) ⇒ ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅)) | ||
| Theorem | functhinclem3 50380* | Lemma for functhinc 50382. The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))) & ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅)) & ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
| Theorem | functhinclem4 50381* | Lemma for functhinc 50382. Other requirements on the morphism part are automatically satisfied. (Contributed by Zhi Wang, 1-Oct-2024.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ ThinCat) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅)) & ⊢ 1 = (Id‘𝐷) & ⊢ 𝐼 = (Id‘𝐸) & ⊢ · = (comp‘𝐷) & ⊢ 𝑂 = (comp‘𝐸) ⇒ ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → ∀𝑎 ∈ 𝐵 (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))) | ||
| Theorem | functhinc 50382* | A functor to a thin category is determined entirely by the object part. The hypothesis "functhinc.1" is related to a monotone function if preorders induced by the categories are considered (catprs2 49946), and can be obtained from funcf2 17963, f002 49790, and ralrimivva 3207. (Contributed by Zhi Wang, 1-Oct-2024.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ ThinCat) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅)) ⇒ ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐺 = 𝐾)) | ||
| Theorem | functhincfun 50383 | A functor to a thin category is determined entirely by the object part. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ ThinCat) ⇒ ⊢ (𝜑 → Fun (𝐶 Func 𝐷)) | ||
| Theorem | fullthinc 50384* | A functor to a thin category is full iff empty hom-sets are mapped to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ ThinCat) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥𝐻𝑦) = ∅ → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅))) | ||
| Theorem | fullthinc2 50385 | A full functor to a thin category maps empty hom-sets to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ ThinCat) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋𝐻𝑌) = ∅ ↔ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅)) | ||
| Theorem | thincfth 50386 | A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024.) |
| ⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) | ||
| Theorem | thincciso 50387* | Two thin categories are isomorphic iff the induced preorders are order-isomorphic. Example 3.26(2) of [Adamek] p. 33. Note that "thincciso.u" is redundant thanks to elbasfv 17313. (Contributed by Zhi Wang, 16-Oct-2024.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑅 = (Base‘𝑋) & ⊢ 𝑆 = (Base‘𝑌) & ⊢ 𝐻 = (Hom ‘𝑋) & ⊢ 𝐽 = (Hom ‘𝑌) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ThinCat) & ⊢ (𝜑 → 𝑌 ∈ ThinCat) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓(∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 ((𝑥𝐻𝑦) = ∅ ↔ ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) = ∅) ∧ 𝑓:𝑅–1-1-onto→𝑆))) | ||
| Theorem | thinccisod 50388* | Two thin categories are isomorphic if the induced preorders are order-isomorphic (deduction form). Example 3.26(2) of [Adamek] p. 33. (Contributed by Zhi Wang, 22-Sep-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝑅 = (Base‘𝑋) & ⊢ 𝑆 = (Base‘𝑌) & ⊢ 𝐻 = (Hom ‘𝑋) & ⊢ 𝐽 = (Hom ‘𝑌) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ ThinCat) & ⊢ (𝜑 → 𝑌 ∈ ThinCat) & ⊢ (𝜑 → 𝐹:𝑅–1-1-onto→𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝑥𝐻𝑦) = ∅ ↔ ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅)) ⇒ ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌) | ||
| Theorem | thincciso2 50389 | Categories isomorphic to a thin category are thin. Example 3.26(2) of [Adamek] p. 33. Note that "thincciso2.u" is redundant thanks to elbasfv 17313. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ (𝜑 → 𝑌 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝑋 ∈ ThinCat) | ||
| Theorem | thincciso3 50390 | Categories isomorphic to a thin category are thin. Example 3.26(2) of [Adamek] p. 33. Note that "thincciso2.u" is redundant thanks to elbasfv 17313. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ (𝜑 → 𝑋 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝑌 ∈ ThinCat) | ||
| Theorem | thincciso4 50391 | Two isomorphic categories are either both thin or neither. Note that "thincciso2.u" is redundant thanks to elbasfv 17313. (Contributed by Zhi Wang, 18-Oct-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌) ⇒ ⊢ (𝜑 → (𝑋 ∈ ThinCat ↔ 𝑌 ∈ ThinCat)) | ||
| Theorem | 0thincg 50392 | Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ ThinCat) | ||
| Theorem | 0thinc 50393 | The empty category (see 0cat 17783) is thin. (Contributed by Zhi Wang, 17-Sep-2024.) |
| ⊢ ∅ ∈ ThinCat | ||
| Theorem | indcthing 50394* | An indiscrete category, i.e., a category where all hom-sets have exactly one morphism, is thin. (Contributed by Zhi Wang, 11-Nov-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐻𝑦) = {𝐹}) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
| Theorem | discthing 50395* | A discrete category, i.e., a category where all morphisms are identity morphisms, is thin. Example 3.26(1) of [Adamek] p. 33. (Contributed by Zhi Wang, 11-Nov-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐻𝑦) = if(𝑥 = 𝑦, {𝐼}, ∅)) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
| Theorem | indthinc 50396* | An indiscrete category in which all hom-sets have exactly one morphism is a thin category. Constructed here is an indiscrete category where all morphisms are ∅. This is a special case of prsthinc 50398, where ≤ = (𝐵 × 𝐵). This theorem also implies a functor from the category of sets to the category of small categories. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof shortened by Zhi Wang, 19-Sep-2024.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶)) & ⊢ (𝜑 → ∅ = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅))) | ||
| Theorem | indthincALT 50397* | An alternate proof of indthinc 50396 assuming more axioms including ax-pow 5334 and ax-un 7740. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶)) & ⊢ (𝜑 → ∅ = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅))) | ||
| Theorem | prsthinc 50398* | Preordered sets as categories. Similar to example 3.3(4.d) of [Adamek] p. 24, but the hom-sets are not pairwise disjoint. One can define a functor from the category of prosets to the category of small thin categories. See catprs 49945 and catprs2 49946 for inducing a preorder from a category. Example 3.26(2) of [Adamek] p. 33 indicates that it induces a bijection from the equivalence class of isomorphic small thin categories to the equivalence class of order-isomorphic preordered sets. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → ( ≤ × {1o}) = (Hom ‘𝐶)) & ⊢ (𝜑 → ∅ = (comp‘𝐶)) & ⊢ (𝜑 → ≤ = (le‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅))) | ||
| Theorem | setcthin 50399* | A category of sets all of whose objects contain at most one element is thin. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (𝜑 → 𝐶 = (SetCat‘𝑈)) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 ∃*𝑝 𝑝 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
| Theorem | setc2othin 50400 | The category (SetCat‘2o) is thin. A special case of setcthin 50399. (Contributed by Zhi Wang, 20-Sep-2024.) |
| ⊢ (SetCat‘2o) ∈ ThinCat | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |