HomeTheorem List (p. 495 of 500)
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. 495 of 500) | < 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-30942) |
Hilbert Space Explorer
(30943-32465) |
Users' Mathboxes
(32466-49992) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | uptri 49401 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀) ⇒ ⊢ (𝜑 → 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁) | ||
| Theorem | uptra 49402 | 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 49403 | 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 49404 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ (𝜑 → ((𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝑍(𝐹(𝐶 UP 𝐷)𝑋)𝑀) ⇒ ⊢ (𝜑 → 𝑍(𝐺(𝐶 UP 𝐸)𝑌)𝑁) | ||
| Theorem | uobffth 49405 | 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 49406 | 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 49407 | 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 49408 | 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 49409 | 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 49410* | 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 49411 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) | ||
| Theorem | natrcl3 49412 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) | ||
| Theorem | catbas 49413 | The base of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ 𝐵 ∈ V ⇒ ⊢ 𝐵 = (Base‘𝐶) | ||
| Theorem | cathomfval 49414 | The hom-sets of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ 𝐻 ∈ V ⇒ ⊢ 𝐻 = (Hom ‘𝐶) | ||
| Theorem | catcofval 49415 | Composition of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ · ∈ V ⇒ ⊢ · = (comp‘𝐶) | ||
| Theorem | natoppf 49416 | A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝑀 = (𝑂 Nat 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (⟨𝐾, tpos 𝐿⟩𝑀⟨𝐹, tpos 𝐺⟩)) | ||
| Theorem | natoppf2 49417 | A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝑀 = (𝑂 Nat 𝑃) & ⊢ (𝜑 → 𝐾 = ( oppFunc ‘𝐹)) & ⊢ (𝜑 → 𝐿 = ( oppFunc ‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐿𝑀𝐾)) | ||
| Theorem | natoppfb 49418 | 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 49419 | An initial object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ 𝐵) | ||
| Theorem | termoo2 49420 | A terminal object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ 𝐵) | ||
| Theorem | zeroo2 49421 | A zero object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑂 ∈ (ZeroO‘𝐶) → 𝑂 ∈ 𝐵) | ||
| Theorem | oppcinito 49422 | Initial objects are terminal in the opposite category. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ (TermO‘(oppCat‘𝐶))) | ||
| Theorem | oppctermo 49423 | 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 49424 | 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 49425 | 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 49426 | Lemma for initopropdlem 49427, termopropdlem 49428, and zeroopropdlem 49429. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝐹 Fn 𝑋 & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝑌) & ⊢ 𝑋 ⊆ 𝑌 & ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑋) → (𝐹‘𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵)) | ||
| Theorem | initopropdlem 49427 | Lemma for initopropd 49430. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → ¬ 𝐶 ∈ V) ⇒ ⊢ (𝜑 → (InitO‘𝐶) = (InitO‘𝐷)) | ||
| Theorem | termopropdlem 49428 | Lemma for termopropd 49431. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → ¬ 𝐶 ∈ V) ⇒ ⊢ (𝜑 → (TermO‘𝐶) = (TermO‘𝐷)) | ||
| Theorem | zeroopropdlem 49429 | Lemma for zeroopropd 49432. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → ¬ 𝐶 ∈ V) ⇒ ⊢ (𝜑 → (ZeroO‘𝐶) = (ZeroO‘𝐷)) | ||
| Theorem | initopropd 49430 | 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 49431 | 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 49432 | 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 49433 | The binary product of categories is a proper operator, so it can be used with ovprc1 7395, elbasov 17141, strov2rcl 17142, and so on. See reldmxpcALT 49434 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 49434 | Alternate proof of reldmxpc 49433. (Contributed by Zhi Wang, 15-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Rel dom ×c | ||
| Theorem | elxpcbasex1 49435 | 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 49436 | Alternate proof of elxpcbasex1 49435. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ V) | ||
| Theorem | elxpcbasex2 49437 | 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 49438 | Alternate proof of elxpcbasex2 49437. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐷 ∈ V) | ||
| Theorem | xpcfucbas 49439 | 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 49440* | 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 49441 | 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 49442 | 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 49443 | 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 49444 | 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 49445* | 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 49446 | Extend class notation with the class of swap functors. |
| class swapF | ||
| Definition | df-swapf 49447* |
Define the swap functor from (𝐶 ×c 𝐷) to (𝐷
×c 𝐶) by
swapping all objects (swapf1 49459) and morphisms (swapf2 49461) .
Such functor is called a "swap functor" in https://arxiv.org/pdf/2302.07810 49461 or a "twist functor" in https://arxiv.org/pdf/2508.01886 49461, the latter of which finds its counterpart as "twisting map" in https://arxiv.org/pdf/2411.04102 49461 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 49461 and thus not adopted here. tpos I depends on more mathbox theorems, and thus are not adopted here. See dfswapf2 49448 for an alternate definition. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩) | ||
| Theorem | dfswapf2 49448* | Alternate definition of swapF (df-swapf 49447). (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(tpos I ↾ 𝑏), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (tpos I ↾ (𝑢ℎ𝑣)))⟩) | ||
| Theorem | swapfval 49449* | Value of the swap functor. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) ⇒ ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨(𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))⟩) | ||
| Theorem | swapfelvv 49450 | A swap functor is an ordered pair. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (V × V)) | ||
| Theorem | swapf2fvala 49451* | The morphism part of the swap functor. See also swapf2fval 49452. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) ⇒ ⊢ (𝜑 → (2nd ‘(𝐶 swapF 𝐷)) = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))) | ||
| Theorem | swapf2fval 49452* | The morphism part of the swap functor. See also swapf2fvala 49451. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑃 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))) | ||
| Theorem | swapf1vala 49453* | The object part of the swap functor. See also swapf1val 49454. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝜑 → (1st ‘(𝐶 swapF 𝐷)) = (𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥})) | ||
| Theorem | swapf1val 49454* | The object part of the swap functor. See also swapf1vala 49453. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑂 = (𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥})) | ||
| Theorem | swapf2fn 49455 | 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 49456 | The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑂‘𝑋) = ⟨(2nd ‘𝑋), (1st ‘𝑋)⟩) | ||
| Theorem | swapf2vala 49457* | The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) ⇒ ⊢ (𝜑 → (𝑋𝑃𝑌) = (𝑓 ∈ (𝑋𝐻𝑌) ↦ ∪ ◡{𝑓})) | ||
| Theorem | swapf2a 49458 | 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 49459 | The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷)) ⇒ ⊢ (𝜑 → (𝑋𝑂𝑌) = ⟨𝑌, 𝑋⟩) | ||
| Theorem | swapf2val 49460* | 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 49461 | 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 49462 | 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 49463 | 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 49464 | 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 49465 | Alternate proof of swapf2f1oa 49464. (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 49466 | Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfida 49467. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷)) & ⊢ 1 = (Id‘𝑆) & ⊢ 𝐼 = (Id‘𝑇) ⇒ ⊢ (𝜑 → ((⟨𝑋, 𝑌⟩𝑃⟨𝑋, 𝑌⟩)‘( 1 ‘⟨𝑋, 𝑌⟩)) = (𝐼‘(𝑂‘⟨𝑋, 𝑌⟩))) | ||
| Theorem | swapfida 49467 | Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfid 49466. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 1 = (Id‘𝑆) & ⊢ 𝐼 = (Id‘𝑇) ⇒ ⊢ (𝜑 → ((𝑋𝑃𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝑂‘𝑋))) | ||
| Theorem | swapfcoa 49468 | 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 49469 | The swap functor is a functor. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑂(𝑆 Func 𝑇)𝑃) | ||
| Theorem | swapfffth 49470 | The swap functor is a fully faithful functor. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑂((𝑆 Full 𝑇) ∩ (𝑆 Faith 𝑇))𝑃) | ||
| Theorem | swapffunca 49471 | The swap functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) ⇒ ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (𝑆 Func 𝑇)) | ||
| Theorem | swapfiso 49472 | 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 49473 | 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 49474* | 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 49475 | 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 49476 | 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 49477 | 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 49478 | 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 49479 | 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 49480 | 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 49481 | 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 49482 | 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 49483 | 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 49484 | 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 49485 | 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 49486* | 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 49487* | 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 49488 | 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 49489 | 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 49490 | 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 49491* | 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 49492* | The constant functor of 𝑋. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 𝐾 = ⟨(𝐵 × {𝑋}), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ ((𝑦𝐽𝑧) × {( 1 ‘𝑋)}))⟩) | ||
| Theorem | diag1f1lem 49493 | The object part of the diagonal functor is 1-1 if 𝐵 is non-empty. Note that (𝜑 → (𝑀 = 𝑁 ↔ 𝑋 = 𝑌)) also holds because of diag1f1 49494 and f1fveq 7206. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑀 = ((1st ‘𝐿)‘𝑋) & ⊢ 𝑁 = ((1st ‘𝐿)‘𝑌) ⇒ ⊢ (𝜑 → (𝑀 = 𝑁 → 𝑋 = 𝑌)) | ||
| Theorem | diag1f1 49494 | 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 49495 | Lemma for diag2f1 49496. The converse is trivial (fveq2 6832). (Contributed by Zhi Wang, 21-Oct-2025.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = ((𝑋(2nd ‘𝐿)𝑌)‘𝐺) → 𝐹 = 𝐺)) | ||
| Theorem | diag2f1 49496 | 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 49497 | Lemma for proving functor theorems. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) & ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜏)) → 𝜂) & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜂) → 𝜃) & ⊢ ((𝜑 ∧ 𝜂) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜂)) | ||
| Theorem | fucofulem2 49498* | Lemma for proving functor theorems. Maybe consider eufnfv 7173 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 49499 | Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩ ∈ (𝑆 × 𝑅) ↔ (𝐾𝑆𝐿 ∧ 𝐹𝑅𝐺)) | ||
| Theorem | fuco2eld 49500 | Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅)) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝐾𝑆𝐿) & ⊢ (𝜑 → 𝐹𝑅𝐺) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑊) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |