HomeTheorem List (p. 179 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. 179 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-30880) |
Hilbert Space Explorer
(30881-32403) |
Users' Mathboxes
(32404-49791) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | idfuval 17801* | Value of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐼 = ⟨( I ↾ 𝐵), (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))⟩) | ||
| Theorem | idfu2nd 17802 | Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝐼)𝑌) = ( I ↾ (𝑋𝐻𝑌))) | ||
| Theorem | idfu2 17803 | Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝐼)𝑌)‘𝐹) = 𝐹) | ||
| Theorem | idfu1st 17804 | Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → (1st ‘𝐼) = ( I ↾ 𝐵)) | ||
| Theorem | idfu1 17805 | Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝐼)‘𝑋) = 𝑋) | ||
| Theorem | idfucl 17806 | The identity functor is a functor. Example 3.20(1) of [Adamek] p. 30. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → 𝐼 ∈ (𝐶 Func 𝐶)) | ||
| Theorem | cofuval 17807* | Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) = ⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩) | ||
| Theorem | cofu1st 17808 | Value of the object part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹)) = ((1st ‘𝐺) ∘ (1st ‘𝐹))) | ||
| Theorem | cofu1 17809 | Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘(𝐺 ∘func 𝐹))‘𝑋) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑋))) | ||
| Theorem | cofu2nd 17810 | Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘(𝐺 ∘func 𝐹))𝑌) = ((((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌)) ∘ (𝑋(2nd ‘𝐹)𝑌))) | ||
| Theorem | cofu2 17811 | Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘(𝐺 ∘func 𝐹))𝑌)‘𝑅) = ((((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌))‘((𝑋(2nd ‘𝐹)𝑌)‘𝑅))) | ||
| Theorem | cofuval2 17812* | Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐻(𝐷 Func 𝐸)𝐾) ⇒ ⊢ (𝜑 → (⟨𝐻, 𝐾⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨(𝐻 ∘ 𝐹), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐾(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))⟩) | ||
| Theorem | cofucl 17813 | The composition of two functors is a functor. Proposition 3.23 of [Adamek] p. 33. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸)) | ||
| Theorem | cofuass 17814 | Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐻 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐾 ∈ (𝐸 Func 𝐹)) ⇒ ⊢ (𝜑 → ((𝐾 ∘func 𝐻) ∘func 𝐺) = (𝐾 ∘func (𝐻 ∘func 𝐺))) | ||
| Theorem | cofulid 17815 | The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (idfunc‘𝐷) ⇒ ⊢ (𝜑 → (𝐼 ∘func 𝐹) = 𝐹) | ||
| Theorem | cofurid 17816 | The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘func 𝐼) = 𝐹) | ||
| Theorem | resfval 17817* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 ↾f 𝐻) = ⟨((1st ‘𝐹) ↾ dom dom 𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))⟩) | ||
| Theorem | resfval2 17818* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ↾f 𝐻) = ⟨(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))⟩) | ||
| Theorem | resf1st 17819 | Value of the functor restriction operator on objects. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (1st ‘(𝐹 ↾f 𝐻)) = ((1st ‘𝐹) ↾ 𝑆)) | ||
| Theorem | resf2nd 17820 | Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘(𝐹 ↾f 𝐻))𝑌) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) | ||
| Theorem | funcres 17821 | A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ↾f 𝐻) ∈ ((𝐶 ↾cat 𝐻) Func 𝐷)) | ||
| Theorem | funcres2b 17822* | Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑅 ∈ (Subcat‘𝐷)) & ⊢ (𝜑 → 𝑅 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦))) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺)) | ||
| Theorem | funcres2 17823 | A functor into a restricted category is also a functor into the whole category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝑅 ∈ (Subcat‘𝐷) → (𝐶 Func (𝐷 ↾cat 𝑅)) ⊆ (𝐶 Func 𝐷)) | ||
| Theorem | idfusubc0 17824* | The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020.) |
| ⊢ 𝑆 = (𝐶 ↾cat 𝐽) & ⊢ 𝐼 = (idfunc‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 = ⟨( I ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥(Hom ‘𝑆)𝑦)))⟩) | ||
| Theorem | idfusubc 17825* | The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020.) |
| ⊢ 𝑆 = (𝐶 ↾cat 𝐽) & ⊢ 𝐼 = (idfunc‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 = ⟨( I ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥𝐽𝑦)))⟩) | ||
| Theorem | wunfunc 17826 | A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈) | ||
| Theorem | funcpropd 17827 | If two categories have the same set of objects, morphisms, and compositions, then they have the same functors. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷)) | ||
| Theorem | funcres2c 17828 | Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐸 = (𝐷 ↾s 𝑆) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func 𝐸)𝐺)) | ||
| Syntax | cful 17829 | Extend class notation with the class of all full functors. |
| class Full | ||
| Syntax | cfth 17830 | Extend class notation with the class of all faithful functors. |
| class Faith | ||
| Definition | df-full 17831* | Function returning all the full functors from a category 𝐶 to a category 𝐷. A full functor is a functor in which all the morphism maps 𝐺(𝑋, 𝑌) between objects 𝑋, 𝑌 ∈ 𝐶 are surjections. Definition 3.27(3) in [Adamek] p. 34. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ Full = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))}) | ||
| Definition | df-fth 17832* | Function returning all the faithful functors from a category 𝐶 to a category 𝐷. A faithful functor is a functor in which all the morphism maps 𝐺(𝑋, 𝑌) between objects 𝑋, 𝑌 ∈ 𝐶 are injections. Definition 3.27(2) in [Adamek] p. 34. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ Faith = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦))}) | ||
| Theorem | fullfunc 17833 | A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷) | ||
| Theorem | fthfunc 17834 | A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷) | ||
| Theorem | relfull 17835 | The set of full functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ Rel (𝐶 Full 𝐷) | ||
| Theorem | relfth 17836 | The set of faithful functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ Rel (𝐶 Faith 𝐷) | ||
| Theorem | isfull 17837* | Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) ⇒ ⊢ (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ran (𝑥𝐺𝑦) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | isfull2 17838* | Equivalent condition for a full functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–onto→((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | fullfo 17839 | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–onto→((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
| Theorem | fulli 17840* | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ (𝑋𝐻𝑌)𝑅 = ((𝑋𝐺𝑌)‘𝑓)) | ||
| Theorem | isfth 17841* | Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))) | ||
| Theorem | isfth2 17842* | Equivalent condition for a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) ⇒ ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–1-1→((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | isffth2 17843* | A fully faithful functor is a functor which is bijective on hom-sets. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) ⇒ ⊢ (𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–1-1-onto→((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | fthf1 17844 | The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–1-1→((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
| Theorem | fthi 17845 | The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑆 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (((𝑋𝐺𝑌)‘𝑅) = ((𝑋𝐺𝑌)‘𝑆) ↔ 𝑅 = 𝑆)) | ||
| Theorem | ffthf1o 17846 | The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–1-1-onto→((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
| Theorem | fullpropd 17847 | If two categories have the same set of objects, morphisms, and compositions, then they have the same full functors. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 Full 𝐶) = (𝐵 Full 𝐷)) | ||
| Theorem | fthpropd 17848 | If two categories have the same set of objects, morphisms, and compositions, then they have the same faithful functors. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 Faith 𝐶) = (𝐵 Faith 𝐷)) | ||
| Theorem | fulloppc 17849 | The opposite functor of a full functor is also full. Proposition 3.43(d) in [Adamek] p. 39. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝑂 Full 𝑃)tpos 𝐺) | ||
| Theorem | fthoppc 17850 | The opposite functor of a faithful functor is also faithful. Proposition 3.43(c) in [Adamek] p. 39. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝑂 Faith 𝑃)tpos 𝐺) | ||
| Theorem | ffthoppc 17851 | The opposite functor of a fully faithful functor is also full and faithful. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺) ⇒ ⊢ (𝜑 → 𝐹((𝑂 Full 𝑃) ∩ (𝑂 Faith 𝑃))tpos 𝐺) | ||
| Theorem | fthsect 17852 | A faithful functor reflects sections. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑋)) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝐷) ⇒ ⊢ (𝜑 → (𝑀(𝑋𝑆𝑌)𝑁 ↔ ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝑇(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁))) | ||
| Theorem | fthinv 17853 | A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑋)) & ⊢ 𝐼 = (Inv‘𝐶) & ⊢ 𝐽 = (Inv‘𝐷) ⇒ ⊢ (𝜑 → (𝑀(𝑋𝐼𝑌)𝑁 ↔ ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝐽(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁))) | ||
| Theorem | fthmon 17854 | A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ 𝑁 = (Mono‘𝐷) & ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑁(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → 𝑅 ∈ (𝑋𝑀𝑌)) | ||
| Theorem | fthepi 17855 | A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ 𝑃 = (Epi‘𝐷) & ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑃(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐸𝑌)) | ||
| Theorem | ffthiso 17856 | A fully faithful functor reflects isomorphisms. Corollary 3.32 of [Adamek] p. 35. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐽 = (Iso‘𝐷) ⇒ ⊢ (𝜑 → (𝑅 ∈ (𝑋𝐼𝑌) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))) | ||
| Theorem | fthres2b 17857* | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑅 ∈ (Subcat‘𝐷)) & ⊢ (𝜑 → 𝑅 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦))) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ 𝐹(𝐶 Faith (𝐷 ↾cat 𝑅))𝐺)) | ||
| Theorem | fthres2c 17858 | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐸 = (𝐷 ↾s 𝑆) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ 𝐹(𝐶 Faith 𝐸)𝐺)) | ||
| Theorem | fthres2 17859 | A faithful functor into a restricted category is also a faithful functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ (𝑅 ∈ (Subcat‘𝐷) → (𝐶 Faith (𝐷 ↾cat 𝑅)) ⊆ (𝐶 Faith 𝐷)) | ||
| Theorem | idffth 17860 | The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → 𝐼 ∈ ((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶))) | ||
| Theorem | cofull 17861 | The composition of two full functors is full. Proposition 3.30(d) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Full 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Full 𝐸)) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Full 𝐸)) | ||
| Theorem | cofth 17862 | The composition of two faithful functors is faithful. Proposition 3.30(c) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Faith 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Faith 𝐸)) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Faith 𝐸)) | ||
| Theorem | coffth 17863 | The composition of two fully faithful functors is fully faithful. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ ((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))) & ⊢ (𝜑 → 𝐺 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ ((𝐶 Full 𝐸) ∩ (𝐶 Faith 𝐸))) | ||
| Theorem | rescfth 17864 | The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ 𝐼 = (idfunc‘𝐷) ⇒ ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 ∈ (𝐷 Faith 𝐶)) | ||
| Theorem | ressffth 17865 | The inclusion functor from a full subcategory is a full and faithful functor, see also remark 4.4(2) in [Adamek] p. 49. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾s 𝑆) & ⊢ 𝐼 = (idfunc‘𝐷) ⇒ ⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))) | ||
| Theorem | fullres2c 17866 | Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐸 = (𝐷 ↾s 𝑆) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ 𝐹(𝐶 Full 𝐸)𝐺)) | ||
| Theorem | ffthres2c 17867 | Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐸 = (𝐷 ↾s 𝑆) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) ⇒ ⊢ (𝜑 → (𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺 ↔ 𝐹((𝐶 Full 𝐸) ∩ (𝐶 Faith 𝐸))𝐺)) | ||
| Theorem | inclfusubc 17868* | The "inclusion functor" from a subcategory of a category into the category itself. (Contributed by AV, 30-Mar-2020.) |
| ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ 𝑆 = (𝐶 ↾cat 𝐽) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = ( I ↾ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥𝐽𝑦)))) ⇒ ⊢ (𝜑 → 𝐹(𝑆 Func 𝐶)𝐺) | ||
| Syntax | cnat 17869 | Extend class notation to include the collection of natural transformations. |
| class Nat | ||
| Syntax | cfuc 17870 | Extend class notation to include the functor category. |
| class FuncCat | ||
| Definition | df-nat 17871* | Definition of a natural transformation between two functors. A natural transformation 𝐴:𝐹⟶𝐺 is a collection of arrows 𝐴(𝑥):𝐹(𝑥)⟶𝐺(𝑥), such that 𝐴(𝑦) ∘ 𝐹(ℎ) = 𝐺(ℎ) ∘ 𝐴(𝑥) for each morphism ℎ:𝑥⟶𝑦. Definition 6.1 in [Adamek] p. 83, and definition in [Lang] p. 65. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ Nat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))})) | ||
| Definition | df-fuc 17872* | Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ FuncCat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩}) | ||
| Theorem | fnfuc 17873 | The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ FuncCat Fn (Cat × Cat) | ||
| Theorem | natfval 17874* | Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) ⇒ ⊢ 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩ · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩ · (𝑠‘𝑦))(𝑎‘𝑥))}) | ||
| Theorem | isnat 17875* | Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) ⇒ ⊢ (𝜑 → (𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(⟨(𝐹‘𝑥), (𝐾‘𝑥)⟩ · (𝐾‘𝑦))(𝐴‘𝑥))))) | ||
| Theorem | isnat2 17876* | Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐹𝑁𝐺) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩ · ((1st ‘𝐺)‘𝑦))((𝑥(2nd ‘𝐹)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝐺)𝑦)‘ℎ)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ · ((1st ‘𝐺)‘𝑦))(𝐴‘𝑥))))) | ||
| Theorem | natffn 17877 | The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) | ||
| Theorem | natrcl 17878 | Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ (𝐴 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) | ||
| Theorem | nat1st2nd 17879 | Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (⟨(1st ‘𝐹), (2nd ‘𝐹)⟩𝑁⟨(1st ‘𝐺), (2nd ‘𝐺)⟩)) | ||
| Theorem | natixp 17880* | A natural transformation is a function from the objects of 𝐶 to homomorphisms from 𝐹(𝑥) to 𝐺(𝑥). (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) ⇒ ⊢ (𝜑 → 𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥))) | ||
| Theorem | natcl 17881 | A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) ∈ ((𝐹‘𝑋)𝐽(𝐾‘𝑋))) | ||
| Theorem | natfn 17882 | A natural transformation is a function on the objects of 𝐶. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → 𝐴 Fn 𝐵) | ||
| Theorem | nati 17883 | Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝐴‘𝑌)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩ · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹‘𝑋), (𝐾‘𝑋)⟩ · (𝐾‘𝑌))(𝐴‘𝑋))) | ||
| Theorem | wunnat 17884 | A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈) | ||
| Theorem | catstr 17885 | A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ {⟨(Base‘ndx), 𝑈⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} Struct ⟨1, ;15⟩ | ||
| Theorem | fucval 17886* | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐵 = (𝐶 Func 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩ · ((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))) ⇒ ⊢ (𝜑 → 𝑄 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), ∙ ⟩}) | ||
| Theorem | fuccofval 17887* | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐵 = (𝐶 Func 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ ∙ = (comp‘𝑄) ⇒ ⊢ (𝜑 → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩ · ((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))) | ||
| Theorem | fucbas 17888 | The objects of the functor category are functors from 𝐶 to 𝐷. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) ⇒ ⊢ (𝐶 Func 𝐷) = (Base‘𝑄) | ||
| Theorem | fuchom 17889 | The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ 𝑁 = (Hom ‘𝑄) | ||
| Theorem | fucco 17890* | Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) ⇒ ⊢ (𝜑 → (𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅) = (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ · ((1st ‘𝐻)‘𝑥))(𝑅‘𝑥)))) | ||
| Theorem | fuccoval 17891 | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅)‘𝑋) = ((𝑆‘𝑋)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)⟩ · ((1st ‘𝐻)‘𝑋))(𝑅‘𝑋))) | ||
| Theorem | fuccocl 17892 | The composition of two natural transformations is a natural transformation. Remark 6.14(a) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) ⇒ ⊢ (𝜑 → (𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅) ∈ (𝐹𝑁𝐻)) | ||
| Theorem | fucidcl 17893 | The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ( 1 ∘ (1st ‘𝐹)) ∈ (𝐹𝑁𝐹)) | ||
| Theorem | fuclid 17894 | Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → (( 1 ∘ (1st ‘𝐺))(⟨𝐹, 𝐺⟩ ∙ 𝐺)𝑅) = 𝑅) | ||
| Theorem | fucrid 17895 | Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → (𝑅(⟨𝐹, 𝐹⟩ ∙ 𝐺)( 1 ∘ (1st ‘𝐹))) = 𝑅) | ||
| Theorem | fucass 17896 | Associativity of natural transformation composition. Remark 6.14(b) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) & ⊢ (𝜑 → 𝑇 ∈ (𝐻𝑁𝐾)) ⇒ ⊢ (𝜑 → ((𝑇(⟨𝐺, 𝐻⟩ ∙ 𝐾)𝑆)(⟨𝐹, 𝐺⟩ ∙ 𝐾)𝑅) = (𝑇(⟨𝐹, 𝐻⟩ ∙ 𝐾)(𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅))) | ||
| Theorem | fuccatid 17897* | The functor category is a category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 1 = (Id‘𝐷) ⇒ ⊢ (𝜑 → (𝑄 ∈ Cat ∧ (Id‘𝑄) = (𝑓 ∈ (𝐶 Func 𝐷) ↦ ( 1 ∘ (1st ‘𝑓))))) | ||
| Theorem | fuccat 17898 | The functor category is a category. Remark 6.16 in [Adamek] p. 88. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑄 ∈ Cat) | ||
| Theorem | fucid 17899 | The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝐼‘𝐹) = ( 1 ∘ (1st ‘𝐹))) | ||
| Theorem | fucsect 17900* | Two natural transformations are in a section iff all the components are in a section relation. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ 𝑆 = (Sect‘𝑄) & ⊢ 𝑇 = (Sect‘𝐷) ⇒ ⊢ (𝜑 → (𝑈(𝐹𝑆𝐺)𝑉 ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ 𝑉 ∈ (𝐺𝑁𝐹) ∧ ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝑇((1st ‘𝐺)‘𝑥))(𝑉‘𝑥)))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |