HomeTheorem List (p. 498 of 503)
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. 498 of 503) | < 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-31007) |
Hilbert Space Explorer
(31008-32530) |
Users' Mathboxes
(32531-50295) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | uptrlem2 49701* | Lemma for uptr 49703. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ ∙ = (comp‘𝐷) & ⊢ ⚬ = (comp‘𝐸) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ 𝐴) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐼((1st ‘𝐹)‘𝑍))) & ⊢ (𝜑 → ((𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) ⇒ ⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽((1st ‘𝐺)‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍(2nd ‘𝐺)𝑊)‘𝑘)(⟨𝑌, ((1st ‘𝐺)‘𝑍)⟩ ⚬ ((1st ‘𝐺)‘𝑊))𝑁) ↔ ∀𝑔 ∈ (𝑋𝐼((1st ‘𝐹)‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍(2nd ‘𝐹)𝑊)‘𝑘)(⟨𝑋, ((1st ‘𝐹)‘𝑍)⟩ ∙ ((1st ‘𝐹)‘𝑊))𝑀))) | ||
| Theorem | uptrlem3 49702 | Lemma for uptr 49703. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽(𝐹‘𝑍))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁)) | ||
| Theorem | uptr 49703 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽(𝐹‘𝑍))) ⇒ ⊢ (𝜑 → (𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁)) | ||
| Theorem | uptri 49704 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀) ⇒ ⊢ (𝜑 → 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁) | ||
| Theorem | uptra 49705 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → ((𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑀) = 𝑁) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽((1st ‘𝐹)‘𝑍))) ⇒ ⊢ (𝜑 → (𝑍(𝐹(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(𝐺(𝐶 UP 𝐸)𝑌)𝑁)) | ||
| Theorem | uptrar 49706 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → (◡(𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑁) = 𝑀) & ⊢ (𝜑 → 𝑍(𝐺(𝐶 UP 𝐸)𝑌)𝑁) ⇒ ⊢ (𝜑 → 𝑍(𝐹(𝐶 UP 𝐷)𝑋)𝑀) | ||
| Theorem | uptrai 49707 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ (𝜑 → ((𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝑍(𝐹(𝐶 UP 𝐷)𝑋)𝑀) ⇒ ⊢ (𝜑 → 𝑍(𝐺(𝐶 UP 𝐸)𝑌)𝑁) | ||
| Theorem | uobffth 49708 | A fully faithful functor generates equal sets of universal objects. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) ⇒ ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌)) | ||
| Theorem | uobeqw 49709 | If a full functor (in fact, a full embedding) is a section of a fully faithful functor (surjective on objects), then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ (𝜑 → 𝐾 ∈ (𝐷 Full 𝐸)) & ⊢ (𝜑 → (𝐿 ∘func 𝐾) = 𝐼) & ⊢ (𝜑 → 𝐿 ∈ ((𝐸 Full 𝐷) ∩ (𝐸 Faith 𝐷))) ⇒ ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌)) | ||
| Theorem | uobeq 49710 | If a full functor (in fact, a full embedding) is a section of a functor (surjective on objects), then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ (𝜑 → 𝐾 ∈ (𝐷 Full 𝐸)) & ⊢ (𝜑 → (𝐿 ∘func 𝐾) = 𝐼) & ⊢ (𝜑 → 𝐿 ∈ (𝐸 Func 𝐷)) ⇒ ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌)) | ||
| Theorem | uptr2 49711 | Universal property and fully faithful functor surjective on objects. (Contributed by Zhi Wang, 25-Nov-2025.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑌 = (𝑅‘𝑋)) & ⊢ (𝜑 → 𝑅:𝐴–onto→𝐵) & ⊢ (𝜑 → 𝑅((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝑆) & ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝑅, 𝑆⟩) = ⟨𝐹, 𝐺⟩) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) ⇒ ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐶 UP 𝐸)𝑍)𝑀 ↔ 𝑌(⟨𝐾, 𝐿⟩(𝐷 UP 𝐸)𝑍)𝑀)) | ||
| Theorem | uptr2a 49712 | Universal property and fully faithful functor surjective on objects. (Contributed by Zhi Wang, 25-Nov-2025.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑌 = ((1st ‘𝐾)‘𝑋)) & ⊢ (𝜑 → (𝐺 ∘func 𝐾) = 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐾 ∈ ((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))) & ⊢ (𝜑 → (1st ‘𝐾):𝐴–onto→𝐵) ⇒ ⊢ (𝜑 → (𝑋(𝐹(𝐶 UP 𝐸)𝑍)𝑀 ↔ 𝑌(𝐺(𝐷 UP 𝐸)𝑍)𝑀)) | ||
| Theorem | isnatd 49713* | Property of being a natural transformation; deduction form. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) & ⊢ (𝜑 → 𝐴 Fn 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐴‘𝑥) ∈ ((𝐹‘𝑥)𝐽(𝐾‘𝑥))) & ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ℎ ∈ (𝑥𝐻𝑦)) → ((𝐴‘𝑦)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(⟨(𝐹‘𝑥), (𝐾‘𝑥)⟩ · (𝐾‘𝑦))(𝐴‘𝑥))) ⇒ ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) | ||
| Theorem | natrcl2 49714 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) | ||
| Theorem | natrcl3 49715 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) | ||
| Theorem | catbas 49716 | The base of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ 𝐵 ∈ V ⇒ ⊢ 𝐵 = (Base‘𝐶) | ||
| Theorem | cathomfval 49717 | The hom-sets of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ 𝐻 ∈ V ⇒ ⊢ 𝐻 = (Hom ‘𝐶) | ||
| Theorem | catcofval 49718 | Composition of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ · ∈ V ⇒ ⊢ · = (comp‘𝐶) | ||
| Theorem | natoppf 49719 | A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝑀 = (𝑂 Nat 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (⟨𝐾, tpos 𝐿⟩𝑀⟨𝐹, tpos 𝐺⟩)) | ||
| Theorem | natoppf2 49720 | A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝑀 = (𝑂 Nat 𝑃) & ⊢ (𝜑 → 𝐾 = ( oppFunc ‘𝐹)) & ⊢ (𝜑 → 𝐿 = ( oppFunc ‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐿𝑀𝐾)) | ||
| Theorem | natoppfb 49721 | A natural transformation is natural between opposite functors, and vice versa. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝑀 = (𝑂 Nat 𝑃) & ⊢ (𝜑 → 𝐾 = ( oppFunc ‘𝐹)) & ⊢ (𝜑 → 𝐿 = ( oppFunc ‘𝐺)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹𝑁𝐺) = (𝐿𝑀𝐾)) | ||
| Theorem | initoo2 49722 | An initial object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ 𝐵) | ||
| Theorem | termoo2 49723 | A terminal object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ 𝐵) | ||
| Theorem | zeroo2 49724 | A zero object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑂 ∈ (ZeroO‘𝐶) → 𝑂 ∈ 𝐵) | ||
| Theorem | oppcinito 49725 | Initial objects are terminal in the opposite category. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ (TermO‘(oppCat‘𝐶))) | ||
| Theorem | oppctermo 49726 | Terminal objects are initial in the opposite category. Comments before Definition 7.4 in [Adamek] p. 102. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝐼 ∈ (TermO‘𝐶) ↔ 𝐼 ∈ (InitO‘(oppCat‘𝐶))) | ||
| Theorem | oppczeroo 49727 | Zero objects are zero in the opposite category. Remark 7.8 of [Adamek] p. 103. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐼 ∈ (ZeroO‘𝐶) ↔ 𝐼 ∈ (ZeroO‘(oppCat‘𝐶))) | ||
| Theorem | termoeu2 49728 | Terminal objects are essentially unique; if 𝐴 is a terminal object, then so is every object that is isomorphic to 𝐴. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶)) & ⊢ (𝜑 → 𝐴( ≃𝑐 ‘𝐶)𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶)) | ||
| Theorem | initopropdlemlem 49729 | Lemma for initopropdlem 49730, termopropdlem 49731, and zeroopropdlem 49732. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝐹 Fn 𝑋 & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝑌) & ⊢ 𝑋 ⊆ 𝑌 & ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑋) → (𝐹‘𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵)) | ||
| Theorem | initopropdlem 49730 | Lemma for initopropd 49733. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → ¬ 𝐶 ∈ V) ⇒ ⊢ (𝜑 → (InitO‘𝐶) = (InitO‘𝐷)) | ||
| Theorem | termopropdlem 49731 | Lemma for termopropd 49734. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → ¬ 𝐶 ∈ V) ⇒ ⊢ (𝜑 → (TermO‘𝐶) = (TermO‘𝐷)) | ||
| Theorem | zeroopropdlem 49732 | Lemma for zeroopropd 49735. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → ¬ 𝐶 ∈ V) ⇒ ⊢ (𝜑 → (ZeroO‘𝐶) = (ZeroO‘𝐷)) | ||
| Theorem | initopropd 49733 | Two structures with the same base, hom-sets and composition operation have the same initial objects. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → (InitO‘𝐶) = (InitO‘𝐷)) | ||
| Theorem | termopropd 49734 | Two structures with the same base, hom-sets and composition operation have the same terminal objects. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → (TermO‘𝐶) = (TermO‘𝐷)) | ||
| Theorem | zeroopropd 49735 | Two structures with the same base, hom-sets and composition operation have the same zero objects. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → (ZeroO‘𝐶) = (ZeroO‘𝐷)) | ||
| Theorem | reldmxpc 49736 | The binary product of categories is a proper operator, so it can be used with ovprc1 7400, elbasov 17180, strov2rcl 17181, and so on. See reldmxpcALT 49737 for an alternate proof with less "essential steps" but more "bytes". (Proposed by SN, 15-Oct-2025.) (Contributed by Zhi Wang, 15-Oct-2025.) |
| ⊢ Rel dom ×c | ||
| Theorem | reldmxpcALT 49737 | Alternate proof of reldmxpc 49736. (Contributed by Zhi Wang, 15-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Rel dom ×c | ||
| Theorem | elxpcbasex1 49738 | A non-empty base set of the product category indicates the existence of the first factor of the product category. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof shortened by SN, 15-Oct-2025.) |
| ⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ V) | ||
| Theorem | elxpcbasex1ALT 49739 | Alternate proof of elxpcbasex1 49738. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ V) | ||
| Theorem | elxpcbasex2 49740 | A non-empty base set of the product category indicates the existence of the second factor of the product category. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof shortened by SN, 15-Oct-2025.) |
| ⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐷 ∈ V) | ||
| Theorem | elxpcbasex2ALT 49741 | Alternate proof of elxpcbasex2 49740. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐷 ∈ V) | ||
| Theorem | xpcfucbas 49742 | The base set of the product of two categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) ⇒ ⊢ ((𝐵 Func 𝐶) × (𝐷 Func 𝐸)) = (Base‘𝑇) | ||
| Theorem | xpcfuchomfval 49743* | Set of morphisms of the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ 𝐴 = (Base‘𝑇) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ 𝐾 = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐴 ↦ (((1st ‘𝑢)(𝐵 Nat 𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(𝐷 Nat 𝐸)(2nd ‘𝑣)))) | ||
| Theorem | xpcfuchom 49744 | Set of morphisms of the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ 𝐴 = (Base‘𝑇) & ⊢ 𝐾 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋𝐾𝑌) = (((1st ‘𝑋)(𝐵 Nat 𝐶)(1st ‘𝑌)) × ((2nd ‘𝑋)(𝐷 Nat 𝐸)(2nd ‘𝑌)))) | ||
| Theorem | xpcfuchom2 49745 | Value of the set of morphisms in the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ (𝜑 → 𝑀 ∈ (𝐵 Func 𝐶)) & ⊢ (𝜑 → 𝑁 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝑃 ∈ (𝐵 Func 𝐶)) & ⊢ (𝜑 → 𝑄 ∈ (𝐷 Func 𝐸)) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ (𝜑 → (⟨𝑀, 𝑁⟩𝐾⟨𝑃, 𝑄⟩) = ((𝑀(𝐵 Nat 𝐶)𝑃) × (𝑁(𝐷 Nat 𝐸)𝑄))) | ||
| Theorem | xpcfucco2 49746 | Value of composition in the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ 𝑂 = (comp‘𝑇) & ⊢ (𝜑 → 𝐹 ∈ (𝑀(𝐵 Nat 𝐶)𝑃)) & ⊢ (𝜑 → 𝐺 ∈ (𝑁(𝐷 Nat 𝐸)𝑄)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃(𝐵 Nat 𝐶)𝑅)) & ⊢ (𝜑 → 𝐿 ∈ (𝑄(𝐷 Nat 𝐸)𝑆)) ⇒ ⊢ (𝜑 → (⟨𝐾, 𝐿⟩(⟨⟨𝑀, 𝑁⟩, ⟨𝑃, 𝑄⟩⟩𝑂⟨𝑅, 𝑆⟩)⟨𝐹, 𝐺⟩) = ⟨(𝐾(⟨𝑀, 𝑃⟩(comp‘(𝐵 FuncCat 𝐶))𝑅)𝐹), (𝐿(⟨𝑁, 𝑄⟩(comp‘(𝐷 FuncCat 𝐸))𝑆)𝐺)⟩) | ||
| Theorem | xpcfuccocl 49747 | The composition of two natural transformations is a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ 𝑂 = (comp‘𝑇) & ⊢ (𝜑 → 𝐹 ∈ (𝑀(𝐵 Nat 𝐶)𝑃)) & ⊢ (𝜑 → 𝐺 ∈ (𝑁(𝐷 Nat 𝐸)𝑄)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃(𝐵 Nat 𝐶)𝑅)) & ⊢ (𝜑 → 𝐿 ∈ (𝑄(𝐷 Nat 𝐸)𝑆)) ⇒ ⊢ (𝜑 → (⟨𝐾, 𝐿⟩(⟨⟨𝑀, 𝑁⟩, ⟨𝑃, 𝑄⟩⟩𝑂⟨𝑅, 𝑆⟩)⟨𝐹, 𝐺⟩) ∈ ((𝑀(𝐵 Nat 𝐶)𝑅) × (𝑁(𝐷 Nat 𝐸)𝑆))) | ||
| Theorem | xpcfucco3 49748* | Value of composition in the binary product of categories of functors; expressed explicitly. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ 𝑂 = (comp‘𝑇) & ⊢ (𝜑 → 𝐹 ∈ (𝑀(𝐵 Nat 𝐶)𝑃)) & ⊢ (𝜑 → 𝐺 ∈ (𝑁(𝐷 Nat 𝐸)𝑄)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃(𝐵 Nat 𝐶)𝑅)) & ⊢ (𝜑 → 𝐿 ∈ (𝑄(𝐷 Nat 𝐸)𝑆)) & ⊢ 𝑋 = (Base‘𝐵) & ⊢ 𝑌 = (Base‘𝐷) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐸) ⇒ ⊢ (𝜑 → (⟨𝐾, 𝐿⟩(⟨⟨𝑀, 𝑁⟩, ⟨𝑃, 𝑄⟩⟩𝑂⟨𝑅, 𝑆⟩)⟨𝐹, 𝐺⟩) = ⟨(𝑥 ∈ 𝑋 ↦ ((𝐾‘𝑥)(⟨((1st ‘𝑀)‘𝑥), ((1st ‘𝑃)‘𝑥)⟩ · ((1st ‘𝑅)‘𝑥))(𝐹‘𝑥))), (𝑦 ∈ 𝑌 ↦ ((𝐿‘𝑦)(⟨((1st ‘𝑁)‘𝑦), ((1st ‘𝑄)‘𝑦)⟩ ∙ ((1st ‘𝑆)‘𝑦))(𝐺‘𝑦)))⟩) | ||
| Syntax | cswapf 49749 | Extend class notation with the class of swap functors. |
| class swapF | ||
| Definition | df-swapf 49750* |
Define the swap functor from (𝐶 ×c 𝐷) to (𝐷
×c 𝐶) by
swapping all objects (swapf1 49762) and morphisms (swapf2 49764) .
Such functor is called a "swap functor" in https://arxiv.org/pdf/2302.07810 49764 or a "twist functor" in https://arxiv.org/pdf/2508.01886 49764, the latter of which finds its counterpart as "twisting map" in https://arxiv.org/pdf/2411.04102 49764 for tensor product of algebras. The "swap functor" or "twisting map" is often denoted as a small tau 𝜏 in literature. However, the term "twist functor" is defined differently in https://arxiv.org/pdf/1208.4046 49764 and thus not adopted here. tpos I depends on more mathbox theorems, and thus are not adopted here. See dfswapf2 49751 for an alternate definition. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩) | ||
| Theorem | dfswapf2 49751* | Alternate definition of swapF (df-swapf 49750). (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(tpos I ↾ 𝑏), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (tpos I ↾ (𝑢ℎ𝑣)))⟩) | ||
| Theorem | swapfval 49752* | Value of the swap functor. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) ⇒ ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨(𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))⟩) | ||
| Theorem | swapfelvv 49753 | A swap functor is an ordered pair. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (V × V)) | ||
| Theorem | swapf2fvala 49754* | The morphism part of the swap functor. See also swapf2fval 49755. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) ⇒ ⊢ (𝜑 → (2nd ‘(𝐶 swapF 𝐷)) = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))) | ||
| Theorem | swapf2fval 49755* | The morphism part of the swap functor. See also swapf2fvala 49754. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑃 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))) | ||
| Theorem | swapf1vala 49756* | The object part of the swap functor. See also swapf1val 49757. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝜑 → (1st ‘(𝐶 swapF 𝐷)) = (𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥})) | ||
| Theorem | swapf1val 49757* | The object part of the swap functor. See also swapf1vala 49756. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑂 = (𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥})) | ||
| Theorem | swapf2fn 49758 | The morphism part of the swap functor is a function on the Cartesian square of the base set. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑃 Fn (𝐵 × 𝐵)) | ||
| Theorem | swapf1a 49759 | The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑂‘𝑋) = ⟨(2nd ‘𝑋), (1st ‘𝑋)⟩) | ||
| Theorem | swapf2vala 49760* | The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) ⇒ ⊢ (𝜑 → (𝑋𝑃𝑌) = (𝑓 ∈ (𝑋𝐻𝑌) ↦ ∪ ◡{𝑓})) | ||
| Theorem | swapf2a 49761 | The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋𝑃𝑌)‘𝐹) = ⟨(2nd ‘𝐹), (1st ‘𝐹)⟩) | ||
| Theorem | swapf1 49762 | The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷)) ⇒ ⊢ (𝜑 → (𝑋𝑂𝑌) = ⟨𝑌, 𝑋⟩) | ||
| Theorem | swapf2val 49763* | The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷)) & ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐷)) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) ⇒ ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑃⟨𝑍, 𝑊⟩) = (𝑓 ∈ (⟨𝑋, 𝑌⟩𝐻⟨𝑍, 𝑊⟩) ↦ ∪ ◡{𝑓})) | ||
| Theorem | swapf2 49764 | The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷)) & ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐷)) & ⊢ (𝜑 → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑍)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌(Hom ‘𝐷)𝑊)) ⇒ ⊢ (𝜑 → (𝐹(⟨𝑋, 𝑌⟩𝑃⟨𝑍, 𝑊⟩)𝐺) = ⟨𝐺, 𝐹⟩) | ||
| Theorem | swapf1f1o 49765 | The object part of the swap functor is a bijection between base sets. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐴 = (Base‘𝑇) ⇒ ⊢ (𝜑 → 𝑂:𝐵–1-1-onto→𝐴) | ||
| Theorem | swapf2f1o 49766 | The morphism part of the swap functor is a bijection between hom-sets. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ 𝐻 = (Hom ‘𝑆) & ⊢ 𝐽 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷)) & ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐷)) ⇒ ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑃⟨𝑍, 𝑊⟩):(⟨𝑋, 𝑌⟩𝐻⟨𝑍, 𝑊⟩)–1-1-onto→(⟨𝑌, 𝑋⟩𝐽⟨𝑊, 𝑍⟩)) | ||
| Theorem | swapf2f1oa 49767 | The morphism part of the swap functor is a bijection between hom-sets. (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ 𝐻 = (Hom ‘𝑆) & ⊢ 𝐽 = (Hom ‘𝑇) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝑃𝑌):(𝑋𝐻𝑌)–1-1-onto→((𝑂‘𝑋)𝐽(𝑂‘𝑌))) | ||
| Theorem | swapf2f1oaALT 49768 | Alternate proof of swapf2f1oa 49767. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ 𝐻 = (Hom ‘𝑆) & ⊢ 𝐽 = (Hom ‘𝑇) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝑃𝑌):(𝑋𝐻𝑌)–1-1-onto→((𝑂‘𝑋)𝐽(𝑂‘𝑌))) | ||
| Theorem | swapfid 49769 | Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfida 49770. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷)) & ⊢ 1 = (Id‘𝑆) & ⊢ 𝐼 = (Id‘𝑇) ⇒ ⊢ (𝜑 → ((⟨𝑋, 𝑌⟩𝑃⟨𝑋, 𝑌⟩)‘( 1 ‘⟨𝑋, 𝑌⟩)) = (𝐼‘(𝑂‘⟨𝑋, 𝑌⟩))) | ||
| Theorem | swapfida 49770 | Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfid 49769. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 1 = (Id‘𝑆) & ⊢ 𝐼 = (Id‘𝑇) ⇒ ⊢ (𝜑 → ((𝑋𝑃𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝑂‘𝑋))) | ||
| Theorem | swapfcoa 49771 | Composition in the source category is mapped to composition in the target. (𝜑 → 𝐶 ∈ Cat) and (𝜑 → 𝐷 ∈ Cat) can be replaced by a weaker hypothesis (𝜑 → 𝑆 ∈ Cat). (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝑆) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑍)) & ⊢ · = (comp‘𝑆) & ⊢ ∙ = (comp‘𝑇) ⇒ ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝑁(⟨𝑋, 𝑌⟩ · 𝑍)𝑀)) = (((𝑌𝑃𝑍)‘𝑁)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝑀))) | ||
| Theorem | swapffunc 49772 | The swap functor is a functor. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑂(𝑆 Func 𝑇)𝑃) | ||
| Theorem | swapfffth 49773 | The swap functor is a fully faithful functor. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑂((𝑆 Full 𝑇) ∩ (𝑆 Faith 𝑇))𝑃) | ||
| Theorem | swapffunca 49774 | The swap functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) ⇒ ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (𝑆 Func 𝑇)) | ||
| Theorem | swapfiso 49775 | The swap functor is an isomorphism between product categories. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝑇 ∈ 𝑈) & ⊢ 𝐼 = (Iso‘𝐸) ⇒ ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (𝑆𝐼𝑇)) | ||
| Theorem | swapciso 49776 | The product category is categorically isomorphic to the swapped product category. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝑇 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝑆( ≃𝑐 ‘𝐸)𝑇) | ||
| Theorem | oppc1stflem 49777* | A utility theorem for proving theorems on projection functors of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) → ( oppFunc ‘(𝐶𝐹𝐷)) = (𝑂𝐹𝑃)) & ⊢ 𝐹 = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ 𝑌) ⇒ ⊢ (𝜑 → ( oppFunc ‘(𝐶𝐹𝐷)) = (𝑂𝐹𝑃)) | ||
| Theorem | oppc1stf 49778 | The opposite functor of the first projection functor is the first projection functor of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( oppFunc ‘(𝐶 1stF 𝐷)) = (𝑂 1stF 𝑃)) | ||
| Theorem | oppc2ndf 49779 | The opposite functor of the second projection functor is the second projection functor of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( oppFunc ‘(𝐶 2ndF 𝐷)) = (𝑂 2ndF 𝑃)) | ||
| Theorem | 1stfpropd 49780 | If two categories have the same set of objects, morphisms, and compositions, then they have same first projection functors. (Contributed by Zhi Wang, 20-Nov-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ Cat) & ⊢ (𝜑 → 𝐵 ∈ Cat) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (𝐴 1stF 𝐶) = (𝐵 1stF 𝐷)) | ||
| Theorem | 2ndfpropd 49781 | If two categories have the same set of objects, morphisms, and compositions, then they have same second projection functors. (Contributed by Zhi Wang, 20-Nov-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ Cat) & ⊢ (𝜑 → 𝐵 ∈ Cat) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (𝐴 2ndF 𝐶) = (𝐵 2ndF 𝐷)) | ||
| Theorem | diagpropd 49782 | If two categories have the same set of objects, morphisms, and compositions, then they have same diagonal functors. (Contributed by Zhi Wang, 20-Nov-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ Cat) & ⊢ (𝜑 → 𝐵 ∈ Cat) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (𝐴Δfunc𝐶) = (𝐵Δfunc𝐷)) | ||
| Theorem | cofuswapfcl 49783 | The bifunctor pre-composed with a swap functor is a bifunctor. (Contributed by Zhi Wang, 10-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) & ⊢ (𝜑 → 𝐺 = (𝐹 ∘func (𝐶 swapF 𝐷))) ⇒ ⊢ (𝜑 → 𝐺 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) | ||
| Theorem | cofuswapf1 49784 | The object part of a bifunctor pre-composed with a swap functor. (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) & ⊢ (𝜑 → 𝐺 = (𝐹 ∘func (𝐶 swapF 𝐷))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(1st ‘𝐺)𝑌) = (𝑌(1st ‘𝐹)𝑋)) | ||
| Theorem | cofuswapf2 49785 | The morphism part of a bifunctor pre-composed with a swap functor. (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) & ⊢ (𝜑 → 𝐺 = (𝐹 ∘func (𝐶 swapF 𝐷))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑍)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐽𝑊)) ⇒ ⊢ (𝜑 → (𝑀(⟨𝑋, 𝑌⟩(2nd ‘𝐺)⟨𝑍, 𝑊⟩)𝑁) = (𝑁(⟨𝑌, 𝑋⟩(2nd ‘𝐹)⟨𝑊, 𝑍⟩)𝑀)) | ||
| Theorem | tposcurf1cl 49786 | The partially evaluated transposed curry functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷)))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 = ((1st ‘𝐺)‘𝑋)) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸)) | ||
| Theorem | tposcurf11 49787 | Value of the double evaluated transposed curry functor. (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷)))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 = ((1st ‘𝐺)‘𝑋)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝐾)‘𝑌) = (𝑌(1st ‘𝐹)𝑋)) | ||
| Theorem | tposcurf12 49788 | The partially evaluated transposed curry functor at a morphism. (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷)))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 = ((1st ‘𝐺)‘𝑋)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 ∈ (𝑌𝐽𝑍)) ⇒ ⊢ (𝜑 → ((𝑌(2nd ‘𝐾)𝑍)‘𝐻) = (𝐻(⟨𝑌, 𝑋⟩(2nd ‘𝐹)⟨𝑍, 𝑋⟩)( 1 ‘𝑋))) | ||
| Theorem | tposcurf1 49789* | Value of the object part of the transposed curry functor. (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷)))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 = ((1st ‘𝐺)‘𝑋)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑦(1st ‘𝐹)𝑋)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (𝑔(⟨𝑦, 𝑋⟩(2nd ‘𝐹)⟨𝑧, 𝑋⟩)( 1 ‘𝑋))))⟩) | ||
| Theorem | tposcurf2 49790* | Value of the transposed curry functor at a morphism. (Contributed by Zhi Wang, 10-Oct-2025.) |
| ⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷)))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)) ⇒ ⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ ((𝐼‘𝑧)(⟨𝑧, 𝑋⟩(2nd ‘𝐹)⟨𝑧, 𝑌⟩)𝐾))) | ||
| Theorem | tposcurf2val 49791 | Value of a component of the transposed curry functor natural transformation. (Contributed by Zhi Wang, 10-Oct-2025.) |
| ⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷)))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐿‘𝑍) = ((𝐼‘𝑍)(⟨𝑍, 𝑋⟩(2nd ‘𝐹)⟨𝑍, 𝑌⟩)𝐾)) | ||
| Theorem | tposcurf2cl 49792 | The transposed curry functor at a morphism is a natural transformation. (Contributed by Zhi Wang, 10-Oct-2025.) |
| ⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷)))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)) & ⊢ 𝑁 = (𝐷 Nat 𝐸) ⇒ ⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌))) | ||
| Theorem | tposcurfcl 49793 | The transposed curry functor of a functor 𝐹:𝐷 × 𝐶⟶𝐸 is a functor tposcurry (𝐹):𝐶⟶(𝐷⟶𝐸). (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷)))) & ⊢ 𝑄 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸)) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝑄)) | ||
| Theorem | diag1 49794* | The constant functor of 𝑋. Example 3.20(2) of [Adamek] p. 30. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ 𝑋), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑓 ∈ (𝑦𝐽𝑧) ↦ ( 1 ‘𝑋)))⟩) | ||
| Theorem | diag1a 49795* | The constant functor of 𝑋. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 𝐾 = ⟨(𝐵 × {𝑋}), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ ((𝑦𝐽𝑧) × {( 1 ‘𝑋)}))⟩) | ||
| Theorem | diag1f1lem 49796 | The object part of the diagonal functor is 1-1 if 𝐵 is non-empty. Note that (𝜑 → (𝑀 = 𝑁 ↔ 𝑋 = 𝑌)) also holds because of diag1f1 49797 and f1fveq 7211. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑀 = ((1st ‘𝐿)‘𝑋) & ⊢ 𝑁 = ((1st ‘𝐿)‘𝑌) ⇒ ⊢ (𝜑 → (𝑀 = 𝑁 → 𝑋 = 𝑌)) | ||
| Theorem | diag1f1 49797 | 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 49798 | Lemma for diag2f1 49799. The converse is trivial (fveq2 6835). (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = ((𝑋(2nd ‘𝐿)𝑌)‘𝐺) → 𝐹 = 𝐺)) | ||
| Theorem | diag2f1 49799 | 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 49800 | Lemma for proving functor theorems. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) & ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜏)) → 𝜂) & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜂) → 𝜃) & ⊢ ((𝜑 ∧ 𝜂) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜂)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |