Home | Metamath
Proof Explorer Theorem List (p. 172 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | subcfn 17101 | An element in the set of subcategories is a binary function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝑆 = dom dom 𝐽) ⇒ ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) | ||
Theorem | subcss1 17102 | The objects of a subcategory are a subset of the objects of the original. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝐵) | ||
Theorem | subcss2 17103 | The morphisms of a subcategory are a subset of the morphisms of the original. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐽𝑌) ⊆ (𝑋𝐻𝑌)) | ||
Theorem | subcidcl 17104 | The identity of the original category is contained in each subcategory. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐽𝑋)) | ||
Theorem | subccocl 17105 | A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐽𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐽𝑍)) | ||
Theorem | subccatid 17106* | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑥 ∈ 𝑆 ↦ ( 1 ‘𝑥)))) | ||
Theorem | subcid 17107 | The identity in a subcategory is the same as the original category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) = ((Id‘𝐷)‘𝑋)) | ||
Theorem | subccat 17108 | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → 𝐷 ∈ Cat) | ||
Theorem | issubc3 17109* | Alternate definition of a subcategory, as a subset of the category which is itself a category. The assumption that the identity be closed is necessary just as in the case of a monoid, issubm2 17959, for the same reasons, since categories are a generalization of monoids. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat))) | ||
Theorem | fullsubc 17110 | The full subcategory generated by a subset of objects is the category with these objects and the same morphisms as the original. The result is always a subcategory (and it is full, meaning that all morphisms of the original category between objects in the subcategory is also in the subcategory), see definition 4.1(2) of [Adamek] p. 48. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ↾ (𝑆 × 𝑆)) ∈ (Subcat‘𝐶)) | ||
Theorem | fullresc 17111 | The category formed by structure restriction is the same as the category restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ 𝐷 = (𝐶 ↾s 𝑆) & ⊢ 𝐸 = (𝐶 ↾cat (𝐻 ↾ (𝑆 × 𝑆))) ⇒ ⊢ (𝜑 → ((Homf ‘𝐷) = (Homf ‘𝐸) ∧ (compf‘𝐷) = (compf‘𝐸))) | ||
Theorem | resscat 17112 | A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾s 𝑆) ∈ Cat) | ||
Theorem | subsubc 17113 | A subcategory of a subcategory is a subcategory. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) ⇒ ⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻))) | ||
Syntax | cfunc 17114 | Extend class notation with the class of all functors. |
class Func | ||
Syntax | cidfu 17115 | Extend class notation with identity functor. |
class idfunc | ||
Syntax | ccofu 17116 | Extend class notation with functor composition. |
class ∘func | ||
Syntax | cresf 17117 | Extend class notation to include restriction of a functor to a subcategory. |
class ↾f | ||
Definition | df-func 17118* | Function returning all the functors from a category 𝑡 to a category 𝑢. Definition 3.17 of [Adamek] p. 29, and definition in [Lang] p. 62 ("covariant functor"). Intuitively a functor associates any morphism of 𝑡 to a morphism of 𝑢, any object of 𝑡 to an object of 𝑢, and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of 𝑡 to an object of 𝑢 we write it associates any identity of 𝑡 to an identity of 𝑢 which simplifies the definition. According to remark 3.19 in [Adamek] p. 30, "a functor F : A -> B is technically a family of functions; one from Ob(A) to Ob(B) [here: f, called "the object part" in the following], and for each pair (A,A') of A-objects, one from hom(A,A') to hom(FA, FA') [here: g, called "the morphism part" in the following]". (Contributed by FL, 10-Feb-2008.) (Revised by Mario Carneiro, 2-Jan-2017.) |
⊢ Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {〈𝑓, 𝑔〉 ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}) | ||
Definition | df-idfu 17119* | Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ idfunc = (𝑡 ∈ Cat ↦ ⦋(Base‘𝑡) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉) | ||
Definition | df-cofu 17120* | Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ ∘func = (𝑔 ∈ V, 𝑓 ∈ V ↦ 〈((1st ‘𝑔) ∘ (1st ‘𝑓)), (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))〉) | ||
Definition | df-resf 17121* | Define the restriction of a functor to a subcategory (analogue of df-res 5561). (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ↾f = (𝑓 ∈ V, ℎ ∈ V ↦ 〈((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))〉) | ||
Theorem | relfunc 17122 | The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ Rel (𝐷 Func 𝐸) | ||
Theorem | funcrcl 17123 | Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝐹 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) | ||
Theorem | isfunc 17124* | Value of the set of functors between two categories. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 1 = (Id‘𝐷) & ⊢ 𝐼 = (Id‘𝐸) & ⊢ · = (comp‘𝐷) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) ⇒ ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))) | ||
Theorem | isfuncd 17125* | Deduce that an operation is a functor of categories. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 1 = (Id‘𝐷) & ⊢ 𝐼 = (Id‘𝐸) & ⊢ · = (comp‘𝐷) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧))) → ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) ⇒ ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) | ||
Theorem | funcf1 17126 | The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) | ||
Theorem | funcixp 17127* | The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) | ||
Theorem | funcf2 17128 | The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
Theorem | funcfn2 17129 | The morphism part of a functor is a function. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) | ||
Theorem | funcid 17130 | A functor maps each identity to the corresponding identity in the target category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 1 = (Id‘𝐷) & ⊢ 𝐼 = (Id‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝐹‘𝑋))) | ||
Theorem | funcco 17131 | A functor maps composition in the source category to composition in the target. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑍)‘(𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀))) | ||
Theorem | funcsect 17132 | The image of a section under a functor is a section. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝑆 = (Sect‘𝐷) & ⊢ 𝑇 = (Sect‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀(𝑋𝑆𝑌)𝑁) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝑇(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁)) | ||
Theorem | funcinv 17133 | The image of an inverse under a functor is an inverse. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐼 = (Inv‘𝐷) & ⊢ 𝐽 = (Inv‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀(𝑋𝐼𝑌)𝑁) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝐽(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁)) | ||
Theorem | funciso 17134 | The image of an isomorphism under a functor is an isomorphism. Proposition 3.21 of [Adamek] p. 32. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐼 = (Iso‘𝐷) & ⊢ 𝐽 = (Iso‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
Theorem | funcoppc 17135 | A functor on categories yields a functor on the opposite categories (in the same direction), see definition 3.41 of [Adamek] p. 39. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝑂 Func 𝑃)tpos 𝐺) | ||
Theorem | idfuval 17136* | Value of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐼 = 〈( I ↾ 𝐵), (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))〉) | ||
Theorem | idfu2nd 17137 | Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝐼)𝑌) = ( I ↾ (𝑋𝐻𝑌))) | ||
Theorem | idfu2 17138 | Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝐼)𝑌)‘𝐹) = 𝐹) | ||
Theorem | idfu1st 17139 | Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → (1st ‘𝐼) = ( I ↾ 𝐵)) | ||
Theorem | idfu1 17140 | Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝐼)‘𝑋) = 𝑋) | ||
Theorem | idfucl 17141 | 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 17142* | 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 17143 | 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 17144 | 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 17145 | 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 17146 | 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 17147* | Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐻(𝐷 Func 𝐸)𝐾) ⇒ ⊢ (𝜑 → (〈𝐻, 𝐾〉 ∘func 〈𝐹, 𝐺〉) = 〈(𝐻 ∘ 𝐹), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐾(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))〉) | ||
Theorem | cofucl 17148 | 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 17149 | Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐻 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐾 ∈ (𝐸 Func 𝐹)) ⇒ ⊢ (𝜑 → ((𝐾 ∘func 𝐻) ∘func 𝐺) = (𝐾 ∘func (𝐻 ∘func 𝐺))) | ||
Theorem | cofulid 17150 | The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (idfunc‘𝐷) ⇒ ⊢ (𝜑 → (𝐼 ∘func 𝐹) = 𝐹) | ||
Theorem | cofurid 17151 | The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘func 𝐼) = 𝐹) | ||
Theorem | resfval 17152* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 ↾f 𝐻) = 〈((1st ‘𝐹) ↾ dom dom 𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))〉) | ||
Theorem | resfval2 17153* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (〈𝐹, 𝐺〉 ↾f 𝐻) = 〈(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))〉) | ||
Theorem | resf1st 17154 | Value of the functor restriction operator on objects. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (1st ‘(𝐹 ↾f 𝐻)) = ((1st ‘𝐹) ↾ 𝑆)) | ||
Theorem | resf2nd 17155 | Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘(𝐹 ↾f 𝐻))𝑌) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) | ||
Theorem | funcres 17156 | A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ↾f 𝐻) ∈ ((𝐶 ↾cat 𝐻) Func 𝐷)) | ||
Theorem | funcres2b 17157* | 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 17158 | 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 17159 | A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈) | ||
Theorem | funcpropd 17160 | 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 17161 | 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 17162 | Extend class notation with the class of all full functors. |
class Full | ||
Syntax | cfth 17163 | Extend class notation with the class of all faithful functors. |
class Faith | ||
Definition | df-full 17164* | 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 17165* | 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 17166 | A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷) | ||
Theorem | fthfunc 17167 | A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷) | ||
Theorem | relfull 17168 | The set of full functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ Rel (𝐶 Full 𝐷) | ||
Theorem | relfth 17169 | The set of faithful functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ Rel (𝐶 Faith 𝐷) | ||
Theorem | isfull 17170* | Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) ⇒ ⊢ (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ran (𝑥𝐺𝑦) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
Theorem | isfull2 17171* | Equivalent condition for a full functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–onto→((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
Theorem | fullfo 17172 | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–onto→((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
Theorem | fulli 17173* | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ (𝑋𝐻𝑌)𝑅 = ((𝑋𝐺𝑌)‘𝑓)) | ||
Theorem | isfth 17174* | Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))) | ||
Theorem | isfth2 17175* | Equivalent condition for a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) ⇒ ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–1-1→((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
Theorem | isffth2 17176* | 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 17177 | 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 17178 | The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑆 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (((𝑋𝐺𝑌)‘𝑅) = ((𝑋𝐺𝑌)‘𝑆) ↔ 𝑅 = 𝑆)) | ||
Theorem | ffthf1o 17179 | 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 17180 | 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 17181 | 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 17182 | 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 17183 | 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 17184 | 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 17185 | A faithful functor reflects sections. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑋)) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝐷) ⇒ ⊢ (𝜑 → (𝑀(𝑋𝑆𝑌)𝑁 ↔ ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝑇(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁))) | ||
Theorem | fthinv 17186 | A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑋)) & ⊢ 𝐼 = (Inv‘𝐶) & ⊢ 𝐽 = (Inv‘𝐷) ⇒ ⊢ (𝜑 → (𝑀(𝑋𝐼𝑌)𝑁 ↔ ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝐽(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁))) | ||
Theorem | fthmon 17187 | A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ 𝑁 = (Mono‘𝐷) & ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑁(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → 𝑅 ∈ (𝑋𝑀𝑌)) | ||
Theorem | fthepi 17188 | A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ 𝑃 = (Epi‘𝐷) & ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑃(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐸𝑌)) | ||
Theorem | ffthiso 17189 | 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 17190* | 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 17191 | 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 17192 | 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 17193 | The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → 𝐼 ∈ ((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶))) | ||
Theorem | cofull 17194 | 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 17195 | 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 17196 | 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 17197 | The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ 𝐼 = (idfunc‘𝐷) ⇒ ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 ∈ (𝐷 Faith 𝐶)) | ||
Theorem | ressffth 17198 | 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 17199 | 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 17200 | 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 𝐸))𝐺)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |