HomeTheorem List (p. 170 of 435)
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. 170 of 435) | < 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-28319) |
Hilbert Space Explorer
(28320-29844) |
Users' Mathboxes
(29845-43440) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cofuass 16901 | Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐻 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐾 ∈ (𝐸 Func 𝐹)) ⇒ ⊢ (𝜑 → ((𝐾 ∘func 𝐻) ∘func 𝐺) = (𝐾 ∘func (𝐻 ∘func 𝐺))) | ||
| Theorem | cofulid 16902 | The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (idfunc‘𝐷) ⇒ ⊢ (𝜑 → (𝐼 ∘func 𝐹) = 𝐹) | ||
| Theorem | cofurid 16903 | The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘func 𝐼) = 𝐹) | ||
| Theorem | resfval 16904* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 ↾f 𝐻) = ⟨((1st ‘𝐹) ↾ dom dom 𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))⟩) | ||
| Theorem | resfval2 16905* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ↾f 𝐻) = ⟨(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))⟩) | ||
| Theorem | resf1st 16906 | Value of the functor restriction operator on objects. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (1st ‘(𝐹 ↾f 𝐻)) = ((1st ‘𝐹) ↾ 𝑆)) | ||
| Theorem | resf2nd 16907 | Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘(𝐹 ↾f 𝐻))𝑌) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) | ||
| Theorem | funcres 16908 | A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ↾f 𝐻) ∈ ((𝐶 ↾cat 𝐻) Func 𝐷)) | ||
| Theorem | funcres2b 16909* | 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 16910 | 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 | wunfunc 16911 | A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈) | ||
| Theorem | funcpropd 16912 | 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 16913 | 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 16914 | Extend class notation with the class of all full functors. |
| class Full | ||
| Syntax | cfth 16915 | Extend class notation with the class of all faithful functors. |
| class Faith | ||
| Definition | df-full 16916* | 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 16917* | 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 16918 | A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷) | ||
| Theorem | fthfunc 16919 | A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷) | ||
| Theorem | relfull 16920 | The set of full functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ Rel (𝐶 Full 𝐷) | ||
| Theorem | relfth 16921 | The set of faithful functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ Rel (𝐶 Faith 𝐷) | ||
| Theorem | isfull 16922* | Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) ⇒ ⊢ (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ran (𝑥𝐺𝑦) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | isfull2 16923* | Equivalent condition for a full functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–onto→((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | fullfo 16924 | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–onto→((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
| Theorem | fulli 16925* | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ (𝑋𝐻𝑌)𝑅 = ((𝑋𝐺𝑌)‘𝑓)) | ||
| Theorem | isfth 16926* | Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))) | ||
| Theorem | isfth2 16927* | Equivalent condition for a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) ⇒ ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–1-1→((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | isffth2 16928* | 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 16929 | 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 16930 | The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑆 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (((𝑋𝐺𝑌)‘𝑅) = ((𝑋𝐺𝑌)‘𝑆) ↔ 𝑅 = 𝑆)) | ||
| Theorem | ffthf1o 16931 | 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 16932 | 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 16933 | 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 16934 | 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 16935 | 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 16936 | 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 16937 | A faithful functor reflects sections. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑋)) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝐷) ⇒ ⊢ (𝜑 → (𝑀(𝑋𝑆𝑌)𝑁 ↔ ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝑇(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁))) | ||
| Theorem | fthinv 16938 | A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑋)) & ⊢ 𝐼 = (Inv‘𝐶) & ⊢ 𝐽 = (Inv‘𝐷) ⇒ ⊢ (𝜑 → (𝑀(𝑋𝐼𝑌)𝑁 ↔ ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝐽(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁))) | ||
| Theorem | fthmon 16939 | A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ 𝑁 = (Mono‘𝐷) & ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑁(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → 𝑅 ∈ (𝑋𝑀𝑌)) | ||
| Theorem | fthepi 16940 | A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ 𝑃 = (Epi‘𝐷) & ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑃(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐸𝑌)) | ||
| Theorem | ffthiso 16941 | 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 16942* | 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 16943 | 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 16944 | 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 16945 | The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → 𝐼 ∈ ((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶))) | ||
| Theorem | cofull 16946 | 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 16947 | 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 16948 | 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 16949 | The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ 𝐼 = (idfunc‘𝐷) ⇒ ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 ∈ (𝐷 Faith 𝐶)) | ||
| Theorem | ressffth 16950 | 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 16951 | 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 16952 | 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 𝐸))𝐺)) | ||
| Syntax | cnat 16953 | Extend class notation to include the collection of natural transformations. |
| class Nat | ||
| Syntax | cfuc 16954 | Extend class notation to include the functor category. |
| class FuncCat | ||
| Definition | df-nat 16955* | 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 16956* | 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 16957 | The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ FuncCat Fn (Cat × Cat) | ||
| Theorem | natfval 16958* | Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) ⇒ ⊢ 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩ · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩ · (𝑠‘𝑦))(𝑎‘𝑥))}) | ||
| Theorem | isnat 16959* | Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) ⇒ ⊢ (𝜑 → (𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(⟨(𝐹‘𝑥), (𝐾‘𝑥)⟩ · (𝐾‘𝑦))(𝐴‘𝑥))))) | ||
| Theorem | isnat2 16960* | 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 16961 | The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) | ||
| Theorem | natrcl 16962 | Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ (𝐴 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) | ||
| Theorem | nat1st2nd 16963 | Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (⟨(1st ‘𝐹), (2nd ‘𝐹)⟩𝑁⟨(1st ‘𝐺), (2nd ‘𝐺)⟩)) | ||
| Theorem | natixp 16964* | 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 16965 | A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) ∈ ((𝐹‘𝑋)𝐽(𝐾‘𝑋))) | ||
| Theorem | natfn 16966 | A natural transformation is a function on the objects of 𝐶. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → 𝐴 Fn 𝐵) | ||
| Theorem | nati 16967 | Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝐴‘𝑌)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩ · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹‘𝑋), (𝐾‘𝑋)⟩ · (𝐾‘𝑌))(𝐴‘𝑋))) | ||
| Theorem | wunnat 16968 | A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈) | ||
| Theorem | catstr 16969 | A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ {⟨(Base‘ndx), 𝑈⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} Struct ⟨1, ;15⟩ | ||
| Theorem | fucval 16970* | 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 16971* | 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 16972 | 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 16973 | The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ 𝑁 = (Hom ‘𝑄) | ||
| Theorem | fucco 16974* | Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) ⇒ ⊢ (𝜑 → (𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅) = (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ · ((1st ‘𝐻)‘𝑥))(𝑅‘𝑥)))) | ||
| Theorem | fuccoval 16975 | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅)‘𝑋) = ((𝑆‘𝑋)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)⟩ · ((1st ‘𝐻)‘𝑋))(𝑅‘𝑋))) | ||
| Theorem | fuccocl 16976 | 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 16977 | The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ( 1 ∘ (1st ‘𝐹)) ∈ (𝐹𝑁𝐹)) | ||
| Theorem | fuclid 16978 | Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → (( 1 ∘ (1st ‘𝐺))(⟨𝐹, 𝐺⟩ ∙ 𝐺)𝑅) = 𝑅) | ||
| Theorem | fucrid 16979 | Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → (𝑅(⟨𝐹, 𝐹⟩ ∙ 𝐺)( 1 ∘ (1st ‘𝐹))) = 𝑅) | ||
| Theorem | fucass 16980 | 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 16981* | 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 16982 | 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 16983 | The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝐼‘𝐹) = ( 1 ∘ (1st ‘𝐹))) | ||
| Theorem | fucsect 16984* | 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 ‘𝐺)‘𝑥))(𝑉‘𝑥)))) | ||
| Theorem | fucinv 16985* | Two natural transformations are inverses of each other iff all the components are inverse. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (Inv‘𝑄) & ⊢ 𝐽 = (Inv‘𝐷) ⇒ ⊢ (𝜑 → (𝑈(𝐹𝐼𝐺)𝑉 ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ 𝑉 ∈ (𝐺𝑁𝐹) ∧ ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))(𝑉‘𝑥)))) | ||
| Theorem | invfuc 16986* | If 𝑉(𝑥) is an inverse to 𝑈(𝑥) for each 𝑥, and 𝑈 is a natural transformation, then 𝑉 is also a natural transformation, and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (Inv‘𝑄) & ⊢ 𝐽 = (Inv‘𝐷) & ⊢ (𝜑 → 𝑈 ∈ (𝐹𝑁𝐺)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))𝑋) ⇒ ⊢ (𝜑 → 𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋)) | ||
| Theorem | fuciso 16987* | A natural transformation is an isomorphism of functors iff all its components are isomorphisms. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (Iso‘𝑄) & ⊢ 𝐽 = (Iso‘𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐹𝐼𝐺) ↔ (𝐴 ∈ (𝐹𝑁𝐺) ∧ ∀𝑥 ∈ 𝐵 (𝐴‘𝑥) ∈ (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))))) | ||
| Theorem | natpropd 16988 | If two categories have the same set of objects, morphisms, and compositions, then they have the same natural transformations. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ Cat) & ⊢ (𝜑 → 𝐵 ∈ Cat) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (𝐴 Nat 𝐶) = (𝐵 Nat 𝐷)) | ||
| Theorem | fucpropd 16989 | If two categories have the same set of objects, morphisms, and compositions, then they have the same functor categories. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ Cat) & ⊢ (𝜑 → 𝐵 ∈ Cat) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (𝐴 FuncCat 𝐶) = (𝐵 FuncCat 𝐷)) | ||
| Syntax | cinito 16990 | Extend class notation with the class of initial objects of a category. |
| class InitO | ||
| Syntax | ctermo 16991 | Extend class notation with the class of terminal objects of a category. |
| class TermO | ||
| Syntax | czeroo 16992 | Extend class notation with the class of zero objects of a category. |
| class ZeroO | ||
| Definition | df-inito 16993* | An object A is said to be an initial object provided that for each object B there is exactly one morphism from A to B. Definition 7.1 in [Adamek] p. 101, or definition in [Lang] p. 57 (called "a universally repelling object" there). (Contributed by AV, 3-Apr-2020.) |
| ⊢ InitO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)}) | ||
| Definition | df-termo 16994* | An object A is called a terminal object provided that for each object B there is exactly one morphism from B to A. Definition 7.4 in [Adamek] p. 102, or definition in [Lang] p. 57 (called "a universally attracting object" there). (Contributed by AV, 3-Apr-2020.) |
| ⊢ TermO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎)}) | ||
| Definition | df-zeroo 16995 | An object A is called a zero object provided that it is both an initial object and a terminal object. Definition 7.7 of [Adamek] p. 103. (Contributed by AV, 3-Apr-2020.) |
| ⊢ ZeroO = (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐))) | ||
| Theorem | initorcl 16996 | Reverse closure for an initial object: If a class has an initial object, the class is a category. (Contributed by AV, 4-Apr-2020.) |
| ⊢ (𝐼 ∈ (InitO‘𝐶) → 𝐶 ∈ Cat) | ||
| Theorem | termorcl 16997 | Reverse closure for a terminal object: If a class has a terminal object, the class is a category. (Contributed by AV, 4-Apr-2020.) |
| ⊢ (𝑇 ∈ (TermO‘𝐶) → 𝐶 ∈ Cat) | ||
| Theorem | zeroorcl 16998 | Reverse closure for a zero object: If a class has a zero object, the class is a category. (Contributed by AV, 4-Apr-2020.) |
| ⊢ (𝑍 ∈ (ZeroO‘𝐶) → 𝐶 ∈ Cat) | ||
| Theorem | initoval 16999* | The value of the initial object function, i.e. the set of all initial objects of a category. (Contributed by AV, 3-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → (InitO‘𝐶) = {𝑎 ∈ 𝐵 ∣ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑎𝐻𝑏)}) | ||
| Theorem | termoval 17000* | The value of the terminal object function, i.e. the set of all terminal objects of a category. (Contributed by AV, 3-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → (TermO‘𝐶) = {𝑎 ∈ 𝐵 ∣ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑎)}) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |