HomeTheorem List (p. 494 of 498)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 494 of 498) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30862) |
Hilbert Space Explorer
(30863-32385) |
Users' Mathboxes
(32386-49800) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | diag1f1lem 49301 | The object part of the diagonal functor is 1-1 if 𝐵 is non-empty. Note that (𝜑 → (𝑀 = 𝑁 ↔ 𝑋 = 𝑌)) also holds because of diag1f1 49302 and f1fveq 7199. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑀 = ((1st ‘𝐿)‘𝑋) & ⊢ 𝑁 = ((1st ‘𝐿)‘𝑌) ⇒ ⊢ (𝜑 → (𝑀 = 𝑁 → 𝑋 = 𝑌)) | ||
| Theorem | diag1f1 49302 | The object part of the diagonal functor is 1-1 if 𝐵 is non-empty. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → (1st ‘𝐿):𝐴–1-1→(𝐷 Func 𝐶)) | ||
| Theorem | diag2f1lem 49303 | Lemma for diag2f1 49304. The converse is trivial (fveq2 6822). (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = ((𝑋(2nd ‘𝐿)𝑌)‘𝐺) → 𝐹 = 𝐺)) | ||
| Theorem | diag2f1 49304 | If 𝐵 is non-empty, the morphism part of a diagonal functor is injective functions from hom-sets into sets of natural transformations. (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ 𝑁 = (𝐷 Nat 𝐶) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝐿)𝑌):(𝑋𝐻𝑌)–1-1→(((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌))) | ||
| Theorem | fucofulem1 49305 | Lemma for proving functor theorems. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) & ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜏)) → 𝜂) & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜂) → 𝜃) & ⊢ ((𝜑 ∧ 𝜂) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜂)) | ||
| Theorem | fucofulem2 49306* | Lemma for proving functor theorems. Maybe consider eufnfv 7165 to prove the uniqueness of a functor. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐵 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) & ⊢ 𝐻 = (Hom ‘((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))) ⇒ ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(𝐶 Nat 𝐸)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑢𝐺𝑣)) ∧ ∀𝑚 ∈ 𝐵 ∀𝑛 ∈ 𝐵 ((𝑚𝐺𝑛) = (𝑏 ∈ ((1st ‘𝑚)(𝐷 Nat 𝐸)(1st ‘𝑛)), 𝑎 ∈ ((2nd ‘𝑚)(𝐶 Nat 𝐷)(2nd ‘𝑛)) ↦ (𝑏(𝑚𝐺𝑛)𝑎)) ∧ ∀𝑝 ∈ ((1st ‘𝑚)(𝐷 Nat 𝐸)(1st ‘𝑛))∀𝑞 ∈ ((2nd ‘𝑚)(𝐶 Nat 𝐷)(2nd ‘𝑛))(𝑝(𝑚𝐺𝑛)𝑞) ∈ ((𝐹‘𝑚)(𝐶 Nat 𝐸)(𝐹‘𝑛))))) | ||
| Theorem | fuco2el 49307 | Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩ ∈ (𝑆 × 𝑅) ↔ (𝐾𝑆𝐿 ∧ 𝐹𝑅𝐺)) | ||
| Theorem | fuco2eld 49308 | Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅)) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝐾𝑆𝐿) & ⊢ (𝜑 → 𝐹𝑅𝐺) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑊) | ||
| Theorem | fuco2eld2 49309 | Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅)) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ Rel 𝑆 & ⊢ Rel 𝑅 ⇒ ⊢ (𝜑 → 𝑈 = ⟨⟨(1st ‘(1st ‘𝑈)), (2nd ‘(1st ‘𝑈))⟩, ⟨(1st ‘(2nd ‘𝑈)), (2nd ‘(2nd ‘𝑈))⟩⟩) | ||
| Theorem | fuco2eld3 49310 | Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅)) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ Rel 𝑆 & ⊢ Rel 𝑅 ⇒ ⊢ (𝜑 → ((1st ‘(1st ‘𝑈))𝑆(2nd ‘(1st ‘𝑈)) ∧ (1st ‘(2nd ‘𝑈))𝑅(2nd ‘(2nd ‘𝑈)))) | ||
| Syntax | cfuco 49311 | Extend class notation with functor composition bifunctors. |
| class ∘F | ||
| Definition | df-fuco 49312* | Definition of functor composition bifunctors. Given three categories 𝐶, 𝐷, and 𝐸, (⟨𝐶, 𝐷⟩ ∘F 𝐸) is a functor from the product category of two categories of functors to a category of functors (fucofunc 49354). The object part maps two functors to their composition (fuco11 49321 and fuco11b 49332). The morphism part defines the "composition" of two natural transformations (fuco22 49334) into another natural transformation (fuco22nat 49341) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 49347). Note that such "composition" is different from fucco 17872 because they "compose" along different "axes". (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ ∘F = (𝑝 ∈ V, 𝑒 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌⦋((𝑑 Func 𝑒) × (𝑐 Func 𝑑)) / 𝑤⦌⟨( ∘func ↾ 𝑤), (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝑑 Nat 𝑒)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝑐 Nat 𝑑)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩) | ||
| Theorem | fucofvalg 49313* | Value of the function giving the functor composition bifunctor. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝑃 ∈ 𝑈) & ⊢ (𝜑 → (1st ‘𝑃) = 𝐶) & ⊢ (𝜑 → (2nd ‘𝑃) = 𝐷) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → (𝑃 ∘F 𝐸) = ⚬ ) & ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ⇒ ⊢ (𝜑 → ⚬ = ⟨( ∘func ↾ 𝑊), (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩) | ||
| Theorem | fucofval 49314* | Value of the function giving the functor composition bifunctor. Hypotheses fucofval.c and fucofval.d are not redundant (fucofvalne 49320). (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ ) & ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ⇒ ⊢ (𝜑 → ⚬ = ⟨( ∘func ↾ 𝑊), (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩) | ||
| Theorem | fucoelvv 49315 | A functor composition bifunctor is an ordered pair. Enables 1st2ndb 7964. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ ) ⇒ ⊢ (𝜑 → ⚬ ∈ (V × V)) | ||
| Theorem | fuco1 49316 | The object part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ⇒ ⊢ (𝜑 → 𝑂 = ( ∘func ↾ 𝑊)) | ||
| Theorem | fucof1 49317 | The object part of the functor composition bifunctor maps ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) into (𝐶 Func 𝐸). (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ⇒ ⊢ (𝜑 → 𝑂:𝑊⟶(𝐶 Func 𝐸)) | ||
| Theorem | fuco2 49318* | The morphism part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ⇒ ⊢ (𝜑 → 𝑃 = (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))) | ||
| Theorem | fucofn2 49319 | The morphism part of the functor composition bifunctor is a function on the Cartesian square of the base set. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ⇒ ⊢ (𝜑 → 𝑃 Fn (𝑊 × 𝑊)) | ||
| Theorem | fucofvalne 49320* | Value of the function giving the functor composition bifunctor, if 𝐶 or 𝐷 are not sets. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → ¬ (𝐶 ∈ V ∧ 𝐷 ∈ V)) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ ) & ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ⇒ ⊢ (𝜑 → ⚬ ≠ ⟨( ∘func ↾ 𝑊), (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩) | ||
| Theorem | fuco11 49321 | The object part of the functor composition bifunctor maps two functors to their composition. (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) ⇒ ⊢ (𝜑 → (𝑂‘𝑈) = (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩)) | ||
| Theorem | fuco11cl 49322 | The object part of the functor composition bifunctor maps into (𝐶 Func 𝐸). (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) ⇒ ⊢ (𝜑 → (𝑂‘𝑈) ∈ (𝐶 Func 𝐸)) | ||
| Theorem | fuco11a 49323* | The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly. (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑂‘𝑈) = ⟨(𝐾 ∘ 𝐹), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐿(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))⟩) | ||
| Theorem | fuco112 49324* | The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (2nd ‘(𝑂‘𝑈)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐿(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))) | ||
| Theorem | fuco111 49325 | The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the object part of the composed functor. (Contributed by Zhi Wang, 2-Oct-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) ⇒ ⊢ (𝜑 → (1st ‘(𝑂‘𝑈)) = (𝐾 ∘ 𝐹)) | ||
| Theorem | fuco111x 49326 | The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the object part of the composed functor. An object is mapped by two functors in succession. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → ((1st ‘(𝑂‘𝑈))‘𝑋) = (𝐾‘(𝐹‘𝑋))) | ||
| Theorem | fuco112x 49327 | The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘(𝑂‘𝑈))𝑌) = (((𝐹‘𝑋)𝐿(𝐹‘𝑌)) ∘ (𝑋𝐺𝑌))) | ||
| Theorem | fuco112xa 49328 | The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. A morphism is mapped by two functors in succession. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝐴 ∈ (𝑋(Hom ‘𝐶)𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘(𝑂‘𝑈))𝑌)‘𝐴) = (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐴))) | ||
| Theorem | fuco11id 49329 | The identity morphism of the mapped object. (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ 𝑄 = (𝐶 FuncCat 𝐸) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ 1 = (Id‘𝐸) ⇒ ⊢ (𝜑 → (𝐼‘(𝑂‘𝑈)) = ( 1 ∘ (𝐾 ∘ 𝐹))) | ||
| Theorem | fuco11idx 49330 | The identity morphism of the mapped object. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ 𝑄 = (𝐶 FuncCat 𝐸) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ 1 = (Id‘𝐸) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → ((𝐼‘(𝑂‘𝑈))‘𝑋) = ( 1 ‘(𝐾‘(𝐹‘𝑋)))) | ||
| Theorem | fuco21 49331* | The morphism part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝑀(𝐶 Func 𝐷)𝑁) & ⊢ (𝜑 → 𝑅(𝐷 Func 𝐸)𝑆) & ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩) ⇒ ⊢ (𝜑 → (𝑈𝑃𝑉) = (𝑏 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩), 𝑎 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑀‘𝑥))(⟨(𝐾‘(𝐹‘𝑥)), (𝐾‘(𝑀‘𝑥))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑥)))(((𝐹‘𝑥)𝐿(𝑀‘𝑥))‘(𝑎‘𝑥)))))) | ||
| Theorem | fuco11b 49332 | The object part of the functor composition bifunctor maps two functors to their composition. (Contributed by Zhi Wang, 11-Oct-2025.) |
| ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑂) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (𝐺𝑂𝐹) = (𝐺 ∘func 𝐹)) | ||
| Theorem | fuco11bALT 49333 | Alternate proof of fuco11b 49332. (Contributed by Zhi Wang, 11-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑂) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (𝐺𝑂𝐹) = (𝐺 ∘func 𝐹)) | ||
| Theorem | fuco22 49334* | The morphism part of the functor composition bifunctor. See also fuco22a 49345. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩)) & ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩)) ⇒ ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝐵‘(𝑀‘𝑥))(⟨(𝐾‘(𝐹‘𝑥)), (𝐾‘(𝑀‘𝑥))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑥)))(((𝐹‘𝑥)𝐿(𝑀‘𝑥))‘(𝐴‘𝑥))))) | ||
| Theorem | fucofn22 49335 | The morphism part of the functor composition bifunctor maps two natural transformations to a function on a base set. (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩)) & ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩)) ⇒ ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) Fn (Base‘𝐶)) | ||
| Theorem | fuco23 49336 | The morphism part of the functor composition bifunctor. See also fuco23a 49347. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩)) & ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → ∗ = (⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋)))) ⇒ ⊢ (𝜑 → ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) = ((𝐵‘(𝑀‘𝑋)) ∗ (((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋)))) | ||
| Theorem | fuco22natlem1 49337 | Lemma for fuco22nat 49341. The commutative square of natural transformation 𝐴 in category 𝐷, mapped to category 𝐸 by the morphism part 𝐿 of the functor. (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩)) & ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌)) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) ⇒ ⊢ (𝜑 → ((((𝐹‘𝑌)𝐿(𝑀‘𝑌))‘(𝐴‘𝑌))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝐹‘𝑌))⟩(comp‘𝐸)(𝐾‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐻))) = ((((𝑀‘𝑋)𝐿(𝑀‘𝑌))‘((𝑋𝑁𝑌)‘𝐻))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝐾‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋)))) | ||
| Theorem | fuco22natlem2 49338 | Lemma for fuco22nat 49341. The commutative square of natural transformation 𝐵 in category 𝐸, combined with the commutative square of fuco22natlem1 49337. (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩)) & ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩)) ⇒ ⊢ (𝜑 → (((𝐵‘(𝑀‘𝑌))(⟨(𝐾‘(𝐹‘𝑌)), (𝐾‘(𝑀‘𝑌))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))(((𝐹‘𝑌)𝐿(𝑀‘𝑌))‘(𝐴‘𝑌)))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝐹‘𝑌))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐻))) = ((((𝑀‘𝑋)𝑆(𝑀‘𝑌))‘((𝑋𝑁𝑌)‘𝐻))(⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))((𝐵‘(𝑀‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))))) | ||
| Theorem | fuco22natlem3 49339 | Combine fuco22natlem2 49338 with fuco23 49336. (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩)) & ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩)) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩) ⇒ ⊢ (𝜑 → (((𝐵(𝑈𝑃𝑉)𝐴)‘𝑌)(⟨((𝐾 ∘ 𝐹)‘𝑋), ((𝐾 ∘ 𝐹)‘𝑌)⟩(comp‘𝐸)((𝑅 ∘ 𝑀)‘𝑌))((((𝐹‘𝑋)𝐿(𝐹‘𝑌)) ∘ (𝑋𝐺𝑌))‘𝐻)) = (((((𝑀‘𝑋)𝑆(𝑀‘𝑌)) ∘ (𝑋𝑁𝑌))‘𝐻)(⟨((𝐾 ∘ 𝐹)‘𝑋), ((𝑅 ∘ 𝑀)‘𝑋)⟩(comp‘𝐸)((𝑅 ∘ 𝑀)‘𝑌))((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋))) | ||
| Theorem | fuco22natlem 49340 | The composed natural transformation is a natural transformation. Use fuco22nat 49341 instead. (New usage is discouraged.) (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩)) & ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩)) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩) ⇒ ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) ∈ ((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉))) | ||
| Theorem | fuco22nat 49341 | The composed natural transformation is a natural transformation. (Contributed by Zhi Wang, 2-Oct-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝐶 Nat 𝐷)𝑀)) & ⊢ (𝜑 → 𝐵 ∈ (𝐾(𝐷 Nat 𝐸)𝑅)) & ⊢ (𝜑 → 𝑈 = ⟨𝐾, 𝐹⟩) & ⊢ (𝜑 → 𝑉 = ⟨𝑅, 𝑀⟩) ⇒ ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) ∈ ((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉))) | ||
| Theorem | fucof21 49342 | The morphism part of the functor composition bifunctor maps a hom-set of the product category into a set of natural transformations. (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷)) & ⊢ 𝐽 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑈𝑃𝑉):(𝑈𝐽𝑉)⟶((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉))) | ||
| Theorem | fucoid 49343 | Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid2 49344. (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷)) & ⊢ 1 = (Id‘𝑇) & ⊢ 𝑄 = (𝐶 FuncCat 𝐸) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) ⇒ ⊢ (𝜑 → ((𝑈𝑃𝑈)‘( 1 ‘𝑈)) = (𝐼‘(𝑂‘𝑈))) | ||
| Theorem | fucoid2 49344 | Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid 49343. (Contributed by Zhi Wang, 30-Sep-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷)) & ⊢ 1 = (Id‘𝑇) & ⊢ 𝑄 = (𝐶 FuncCat 𝐸) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) ⇒ ⊢ (𝜑 → ((𝑈𝑃𝑈)‘( 1 ‘𝑈)) = (𝐼‘(𝑂‘𝑈))) | ||
| Theorem | fuco22a 49345* | The morphism part of the functor composition bifunctor. See also fuco22 49334. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑈 = ⟨𝐾, 𝐹⟩) & ⊢ (𝜑 → 𝑉 = ⟨𝑅, 𝑀⟩) & ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝐶 Nat 𝐷)𝑀)) & ⊢ (𝜑 → 𝐵 ∈ (𝐾(𝐷 Nat 𝐸)𝑅)) ⇒ ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝐵‘((1st ‘𝑀)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑀)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑅)‘((1st ‘𝑀)‘𝑥)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐾)((1st ‘𝑀)‘𝑥))‘(𝐴‘𝑥))))) | ||
| Theorem | fuco23alem 49346 | The naturality property (nati 17865) in category 𝐸. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩)) & ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ · = (comp‘𝐸) ⇒ ⊢ (𝜑 → ((𝐵‘(𝑀‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩ · (𝑅‘(𝑀‘𝑋)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))) = ((((𝐹‘𝑋)𝑆(𝑀‘𝑋))‘(𝐴‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝐹‘𝑋))⟩ · (𝑅‘(𝑀‘𝑋)))(𝐵‘(𝐹‘𝑋)))) | ||
| Theorem | fuco23a 49347 | The morphism part of the functor composition bifunctor. An alternate definition of ∘F. See also fuco23 49336. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩)) & ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩) & ⊢ (𝜑 → ∗ = (⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝐹‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋)))) ⇒ ⊢ (𝜑 → ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) = ((((𝐹‘𝑋)𝑆(𝑀‘𝑋))‘(𝐴‘𝑋)) ∗ (𝐵‘(𝐹‘𝑋)))) | ||
| Theorem | fucocolem1 49348 | Lemma for fucoco 49352. Associativity for morphisms in category 𝐸. To simply put, ((𝑎 · 𝑏) · (𝑐 · 𝑑)) = (𝑎 · ((𝑏 · 𝑐) · 𝑑)) for morphism compositions. (Contributed by Zhi Wang, 2-Oct-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿)) & ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀)) & ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑃 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝑄 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐴 ∈ (((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))(Hom ‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋)))) & ⊢ (𝜑 → 𝐵 ∈ (((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋))(Hom ‘𝐸)((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋)))) ⇒ ⊢ (𝜑 → (((𝑈‘((1st ‘𝑁)‘𝑋))(⟨((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑋)))𝐴)(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑋)))(𝐵(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋)))((((1st ‘𝐺)‘𝑋)(2nd ‘𝐹)((1st ‘𝐿)‘𝑋))‘(𝑆‘𝑋)))) = ((𝑈‘((1st ‘𝑁)‘𝑋))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑋)))((𝐴(⟨((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋)), ((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋)))𝐵)(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋)))((((1st ‘𝐺)‘𝑋)(2nd ‘𝐹)((1st ‘𝐿)‘𝑋))‘(𝑆‘𝑋))))) | ||
| Theorem | fucocolem2 49349* | Lemma for fucoco 49352. The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 2-Oct-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿)) & ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀)) & ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁)) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩) & ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩) & ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩) & ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩) & ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩) & ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷)) & ⊢ · = (comp‘𝑇) & ⊢ ∗ = (comp‘𝐷) ⇒ ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ (((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝑁)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))(𝑅‘((1st ‘𝑁)‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝑁)‘𝑥))‘((𝑉‘𝑥)(⟨((1st ‘𝐺)‘𝑥), ((1st ‘𝐿)‘𝑥)⟩ ∗ ((1st ‘𝑁)‘𝑥))(𝑆‘𝑥)))))) | ||
| Theorem | fucocolem3 49350* | Lemma for fucoco 49352. The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿)) & ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀)) & ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁)) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩) & ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩) & ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩) & ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩) & ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩) & ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷)) & ⊢ · = (comp‘𝑇) & ⊢ ∗ = (comp‘𝐷) ⇒ ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))(((𝑅‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐹)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥)))))) | ||
| Theorem | fucocolem4 49351* | Lemma for fucoco 49352. The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 2-Oct-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿)) & ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀)) & ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁)) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩) & ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩) & ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩) & ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩) & ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩) & ⊢ 𝑄 = (𝐶 FuncCat 𝐸) & ⊢ ∙ = (comp‘𝑄) ⇒ ⊢ (𝜑 → (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ (((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥)))))) | ||
| Theorem | fucoco 49352 | Composition in the source category is mapped to composition in the target. See also fucoco2 49353. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿)) & ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀)) & ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁)) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩) & ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩) & ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩) & ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩) & ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩) & ⊢ 𝑄 = (𝐶 FuncCat 𝐸) & ⊢ ∙ = (comp‘𝑄) & ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷)) & ⊢ · = (comp‘𝑇) ⇒ ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴))) | ||
| Theorem | fucoco2 49353 | Composition in the source category is mapped to composition in the target. See also fucoco 49352. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷)) & ⊢ 𝑄 = (𝐶 FuncCat 𝐸) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ · = (comp‘𝑇) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ 𝐽 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐽𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑌𝐽𝑍)) ⇒ ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴))) | ||
| Theorem | fucofunc 49354 |
The functor composition bifunctor is a functor. See also fucofunca 49355.
However, it is unlikely the unique functor compatible with the functor composition. As a counterexample, let 𝐶 and 𝐷 be terminal categories (categories of one object and one morphism, df-termc 49468), for example, (SetCat‘1o) (the trivial category, setc1oterm 49486), and 𝐸 be a category with two objects equipped with only two non-identity morphisms 𝑓 and 𝑔, pointing in the same direction. It is possible to map the ordered pair of natural transformations ⟨𝑎, 𝑖⟩, where 𝑎 sends to 𝑓 and 𝑖 is the identity natural transformation, to the other natural transformation 𝑏 sending to 𝑔, i.e., define the morphism part 𝑃 such that (𝑎(𝑈𝑃𝑉)𝑖) = 𝑏 such that (𝑏‘𝑋) = 𝑔 given hypotheses of fuco23 49336. Such construction should be provable as a functor. Given any 𝑃, it is a morphism part of a functor compatible with the object part, i.e., the functor composition, i.e., the restriction of ∘func, iff both of the following hold. 1. It has the same form as df-fuco 49312 up to fuco23 49336, but ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) might be mapped to a different morphism in category 𝐸. See fucofulem2 49306 for some insights. 2. fuco22nat 49341, fucoid 49343, and fucoco 49352 are satisfied. (Contributed by Zhi Wang, 3-Oct-2025.) |
| ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷)) & ⊢ 𝑄 = (𝐶 FuncCat 𝐸) & ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑂(𝑇 Func 𝑄)𝑃) | ||
| Theorem | fucofunca 49355 | The functor composition bifunctor is a functor. See also fucofunc 49354. (Contributed by Zhi Wang, 10-Oct-2025.) |
| ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷)) & ⊢ 𝑄 = (𝐶 FuncCat 𝐸) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) ⇒ ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) ∈ (𝑇 Func 𝑄)) | ||
| Theorem | fucolid 49356* | Post-compose a natural transformation with an identity natural transformation. (Contributed by Zhi Wang, 11-Oct-2025.) |
| ⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑃) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ 𝑄 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐴 ∈ (𝐺(𝐶 Nat 𝐷)𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐼‘𝐹)(⟨𝐹, 𝐺⟩𝑃⟨𝐹, 𝐻⟩)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐻)‘𝑥))‘(𝐴‘𝑥)))) | ||
| Theorem | fucorid 49357* | Pre-composing a natural transformation with the identity natural transformation of a functor is pre-composing it with the object part of the functor, in maps-to notation. (Contributed by Zhi Wang, 11-Oct-2025.) |
| ⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑃) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝐺(𝐷 Nat 𝐸)𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝐴(⟨𝐺, 𝐹⟩𝑃⟨𝐻, 𝐹⟩)(𝐼‘𝐹)) = (𝑥 ∈ (Base‘𝐶) ↦ (𝐴‘((1st ‘𝐹)‘𝑥)))) | ||
| Theorem | fucorid2 49358 | Pre-composing a natural transformation with the identity natural transformation of a functor is pre-composing it with the object part of the functor. (Contributed by Zhi Wang, 11-Oct-2025.) |
| ⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑃) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝐺(𝐷 Nat 𝐸)𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝐴(⟨𝐺, 𝐹⟩𝑃⟨𝐻, 𝐹⟩)(𝐼‘𝐹)) = (𝐴 ∘ (1st ‘𝐹))) | ||
| Theorem | postcofval 49359* | Value of the post-composition functor as a curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ ⚬ = (⟨𝑅, 𝑄⟩ curryF (⟨𝐶, 𝐷⟩ ∘F 𝐸)) & ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐾 = ((1st ‘ ⚬ )‘𝐹) ⇒ ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐶 Func 𝐷) ↦ (𝐹 ∘func 𝑔)), (𝑔 ∈ (𝐶 Func 𝐷), ℎ ∈ (𝐶 Func 𝐷) ↦ (𝑎 ∈ (𝑔(𝐶 Nat 𝐷)ℎ) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((((1st ‘𝑔)‘𝑥)(2nd ‘𝐹)((1st ‘ℎ)‘𝑥))‘(𝑎‘𝑥)))))⟩) | ||
| Theorem | postcofcl 49360 | The post-composition functor as a curry of the functor composition bifunctor is a functor. (Contributed by Zhi Wang, 11-Oct-2025.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ ⚬ = (⟨𝑅, 𝑄⟩ curryF (⟨𝐶, 𝐷⟩ ∘F 𝐸)) & ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐾 = ((1st ‘ ⚬ )‘𝐹) & ⊢ 𝑆 = (𝐶 FuncCat 𝐸) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝑄 Func 𝑆)) | ||
| Theorem | precofvallem 49361 | Lemma for precofval 49362 to enable catlid 17589 or catrid 17590. (Contributed by Zhi Wang, 11-Oct-2025.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 1 = (Id‘𝐷) & ⊢ 𝐼 = (Id‘𝐸) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((((𝐹‘𝑋)𝐿(𝐹‘𝑋))‘(( 1 ∘ 𝐹)‘𝑋)) = (𝐼‘(𝐾‘(𝐹‘𝑋))) ∧ (𝐾‘(𝐹‘𝑋)) ∈ 𝐵)) | ||
| Theorem | precofval 49362* | 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 49363* | Alternate proof of precofval 49362. (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 49364* | 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 49365 | 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 49366* | 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 49367* | 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 49368 | Extend class notation with pre-composition functors. |
| class −∘F | ||
| Definition | df-prcof 49369* |
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 49366). But such definition requires an explicit third category. prcoftposcurfuco 49378 and prcoftposcurfucoa 49379 prove the equivalence. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ −∘F = (𝑝 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑑⦌⦋(2nd ‘𝑝) / 𝑒⦌⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩) | ||
| Theorem | reldmprcof 49370 | The domain of −∘F is a relation. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ Rel dom −∘F | ||
| Theorem | prcofvalg 49371* | Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝐵 = (𝐷 Func 𝐸) & ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐹 ∈ 𝑈) & ⊢ (𝜑 → 𝑃 ∈ 𝑉) & ⊢ (𝜑 → (1st ‘𝑃) = 𝐷) & ⊢ (𝜑 → (2nd ‘𝑃) = 𝐸) ⇒ ⊢ (𝜑 → (𝑃 −∘F 𝐹) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func 𝐹)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩) | ||
| Theorem | prcofvala 49372* | Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝐵 = (𝐷 Func 𝐸) & ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝑈) ⇒ ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func 𝐹)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩) | ||
| Theorem | prcofval 49373* | Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝐵 = (𝐷 Func 𝐸) & ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ Rel 𝑅 & ⊢ (𝜑 → 𝐹𝑅𝐺) ⇒ ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func ⟨𝐹, 𝐺⟩)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ 𝐹)))⟩) | ||
| Theorem | prcofpropd 49374 | 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 49375 | The pre-composition functor is an ordered pair. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑈) & ⊢ (𝜑 → 𝑃 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑃 −∘F 𝐹) ∈ (V × V)) | ||
| Theorem | reldmprcof1 49376 | 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 49377 | 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 49378 | 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 49379 | 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 49380 | The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ 𝑆 = (𝐶 FuncCat 𝐸) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) ∈ (𝑅 Func 𝑆)) | ||
| Theorem | prcoffunca 49381 | The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025.) |
| ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ 𝑆 = (𝐶 FuncCat 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) ∈ (𝑅 Func 𝑆)) | ||
| Theorem | prcoffunca2 49382 | The pre-composition functor is a functor. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ 𝑅 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ 𝑆 = (𝐶 FuncCat 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐾, 𝐿⟩) ⇒ ⊢ (𝜑 → 𝐾(𝑅 Func 𝑆)𝐿) | ||
| Theorem | prcof1 49383 | The object part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → (1st ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑂) ⇒ ⊢ (𝜑 → (𝑂‘𝐾) = (𝐾 ∘func 𝐹)) | ||
| Theorem | prcof2a 49384* | The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.) |
| ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐾𝑃𝐿) = (𝑎 ∈ (𝐾𝑁𝐿) ↦ (𝑎 ∘ (1st ‘𝐹)))) | ||
| Theorem | prcof2 49385* | The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.) |
| ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩)) = 𝑃) & ⊢ Rel 𝑅 & ⊢ (𝜑 → 𝐹𝑅𝐺) ⇒ ⊢ (𝜑 → (𝐾𝑃𝐿) = (𝑎 ∈ (𝐾𝑁𝐿) ↦ (𝑎 ∘ 𝐹))) | ||
| Theorem | prcof21a 49386 | The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.) |
| ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐴 ∈ (𝐾𝑁𝐿)) & ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐾𝑃𝐿)‘𝐴) = (𝐴 ∘ (1st ‘𝐹))) | ||
| Theorem | prcof22a 49387 | The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.) |
| ⊢ 𝑁 = (𝐷 Nat 𝐸) & ⊢ (𝜑 → 𝐴 ∈ (𝐾𝑁𝐿)) & ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (((𝐾𝑃𝐿)‘𝐴)‘𝑋) = (𝐴‘((1st ‘𝐹)‘𝑋))) | ||
| Theorem | prcofdiag1 49388 | 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 49389 | 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 49390 | Reverse closure for the category of categories (in a universe) (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → 𝑈 ∈ V) | ||
| Theorem | catcrcl2 49391 | Reverse closure for the category of categories (in a universe) (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | elcatchom 49392 | A morphism of the category of categories (in a universe) is a functor. See df-catc 18006 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 18010). (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑋 Func 𝑌)) | ||
| Theorem | catcsect 49393 | 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 49394 | 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 49395 | 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 49396 | 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 49397 | 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 49398 | The object part of the op functor on functor categories. Lemma for fucoppc 49405. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (1st ‘(𝐹‘𝑋)) = (1st ‘𝑋)) | ||
| Theorem | opf12 49399 | The object part of the op functor on functor categories. Lemma for oppfdiag 49411. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷))) & ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝑀(2nd ‘(𝐹‘𝑋))𝑁) = (𝑁(2nd ‘𝑋)𝑀)) | ||
| Theorem | opf2fval 49400* | The morphism part of the op functor on functor categories. Lemma for fucoppc 49405. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑦𝑁𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐹𝑌) = ( I ↾ (𝑌𝑁𝑋))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |