Home | Metamath
Proof Explorer Theorem List (p. 164 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sscfn2 16301 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑇 = dom dom 𝐽) ⇒ ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) | ||
Theorem | ssclem 16302 | Lemma for ssc1 16304 and similar theorems. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (𝐻 ∈ V ↔ 𝑆 ∈ V)) | ||
Theorem | isssc 16303* | Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) | ||
Theorem | ssc1 16304 | Infer subset relation on objects from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝐻 ⊆cat 𝐽) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝑇) | ||
Theorem | ssc2 16305 | Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) ⊆ (𝑋𝐽𝑌)) | ||
Theorem | sscres 16306 | Any function restricted to a square domain is a subcategory subset of the original. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → (𝐻 ↾ (𝑇 × 𝑇)) ⊆cat 𝐻) | ||
Theorem | sscid 16307 | The subcategory subset relation is reflexive. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → 𝐻 ⊆cat 𝐻) | ||
Theorem | ssctr 16308 | The subcategory subset relation is transitive. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶) → 𝐴 ⊆cat 𝐶) | ||
Theorem | ssceq 16309 | The subcategory subset relation is antisymmetric. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴) → 𝐴 = 𝐵) | ||
Theorem | rescval 16310 | Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) ⇒ ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → 𝐷 = ((𝐶 ↾s dom dom 𝐻) sSet 〈(Hom ‘ndx), 𝐻〉)) | ||
Theorem | rescval2 16311 | Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → 𝐷 = ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉)) | ||
Theorem | rescbas 16312 | Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 = (Base‘𝐷)) | ||
Theorem | reschom 16313 | Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐻 = (Hom ‘𝐷)) | ||
Theorem | reschomf 16314 | Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐻 = (Homf ‘𝐷)) | ||
Theorem | rescco 16315 | Composition in the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → · = (comp‘𝐷)) | ||
Theorem | rescabs 16316 | Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) | ||
Theorem | rescabs2 16317 | Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 ↾s 𝑆) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) | ||
Theorem | issubc 16318* | Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑆 = dom dom 𝐽) ⇒ ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) | ||
Theorem | issubc2 16319* | Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) | ||
Theorem | 0ssc 16320 | For any category 𝐶, the empty set is a subcategory subset of 𝐶. (Contributed by AV, 23-Apr-2020.) |
⊢ (𝐶 ∈ Cat → ∅ ⊆cat (Homf ‘𝐶)) | ||
Theorem | 0subcat 16321 | For any category 𝐶, the empty set is a (full) subcategory of 𝐶, see example 4.3(1.a) in [Adamek] p. 48. (Contributed by AV, 23-Apr-2020.) |
⊢ (𝐶 ∈ Cat → ∅ ∈ (Subcat‘𝐶)) | ||
Theorem | catsubcat 16322 | For any category 𝐶, 𝐶 itself is a (full) subcategory of 𝐶, see example 4.3(1.b) in [Adamek] p. 48. (Contributed by AV, 23-Apr-2020.) |
⊢ (𝐶 ∈ Cat → (Homf ‘𝐶) ∈ (Subcat‘𝐶)) | ||
Theorem | subcssc 16323 | An element in the set of subcategories is a subset of the category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ 𝐻 = (Homf ‘𝐶) ⇒ ⊢ (𝜑 → 𝐽 ⊆cat 𝐻) | ||
Theorem | subcfn 16324 | An element in the set of subcategories is a binary function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝑆 = dom dom 𝐽) ⇒ ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) | ||
Theorem | subcss1 16325 | 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 16326 | 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 16327 | 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 16328 | A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐽𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐽𝑍)) | ||
Theorem | subccatid 16329* | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑥 ∈ 𝑆 ↦ ( 1 ‘𝑥)))) | ||
Theorem | subcid 16330 | 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 16331 | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → 𝐷 ∈ Cat) | ||
Theorem | issubc3 16332* | 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 17171, 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 16333 | 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 16334 | 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 16335 | A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾s 𝑆) ∈ Cat) | ||
Theorem | subsubc 16336 | A subcategory of a subcategory is a subcategory. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) ⇒ ⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻))) | ||
Syntax | cfunc 16337 | Extend class notation with the class of all functors. |
class Func | ||
Syntax | cidfu 16338 | Extend class notation with identity functor. |
class idfunc | ||
Syntax | ccofu 16339 | Extend class notation with functor composition. |
class ∘func | ||
Syntax | cresf 16340 | Extend class notation to include restriction of a functor to a subcategory. |
class ↾f | ||
Definition | df-func 16341* | 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 ‘𝑧))) ↑𝑚 ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}) | ||
Definition | df-idfu 16342* | Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ idfunc = (𝑡 ∈ Cat ↦ ⦋(Base‘𝑡) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉) | ||
Definition | df-cofu 16343* | 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 16344* | Define the restriction of a functor to a subcategory (analogue of df-res 5050). (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ↾f = (𝑓 ∈ V, ℎ ∈ V ↦ 〈((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))〉) | ||
Theorem | relfunc 16345 | The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ Rel (𝐷 Func 𝐸) | ||
Theorem | funcrcl 16346 | Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝐹 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) | ||
Theorem | isfunc 16347* | 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 ‘𝑧))) ↑𝑚 (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))) | ||
Theorem | isfuncd 16348* | 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 16349 | The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) | ||
Theorem | funcixp 16350* | 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 ‘𝑧))) ↑𝑚 (𝐻‘𝑧))) | ||
Theorem | funcf2 16351 | The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
Theorem | funcfn2 16352 | The morphism part of a functor is a function. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) | ||
Theorem | funcid 16353 | 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 16354 | 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 16355 | The image of a section under a functor is a section. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝑆 = (Sect‘𝐷) & ⊢ 𝑇 = (Sect‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀(𝑋𝑆𝑌)𝑁) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝑇(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁)) | ||
Theorem | funcinv 16356 | The image of an inverse under a functor is an inverse. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐼 = (Inv‘𝐷) & ⊢ 𝐽 = (Inv‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀(𝑋𝐼𝑌)𝑁) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝐽(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁)) | ||
Theorem | funciso 16357 | 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 16358 | 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 16359* | Value of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐼 = 〈( I ↾ 𝐵), (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))〉) | ||
Theorem | idfu2nd 16360 | Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝐼)𝑌) = ( I ↾ (𝑋𝐻𝑌))) | ||
Theorem | idfu2 16361 | Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝐼)𝑌)‘𝐹) = 𝐹) | ||
Theorem | idfu1st 16362 | Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → (1st ‘𝐼) = ( I ↾ 𝐵)) | ||
Theorem | idfu1 16363 | Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝐼)‘𝑋) = 𝑋) | ||
Theorem | idfucl 16364 | 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 16365* | 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 16366 | 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 16367 | 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 16368 | 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 16369 | 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 16370* | Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐻(𝐷 Func 𝐸)𝐾) ⇒ ⊢ (𝜑 → (〈𝐻, 𝐾〉 ∘func 〈𝐹, 𝐺〉) = 〈(𝐻 ∘ 𝐹), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐾(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))〉) | ||
Theorem | cofucl 16371 | 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 16372 | Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐻 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐾 ∈ (𝐸 Func 𝐹)) ⇒ ⊢ (𝜑 → ((𝐾 ∘func 𝐻) ∘func 𝐺) = (𝐾 ∘func (𝐻 ∘func 𝐺))) | ||
Theorem | cofulid 16373 | The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (idfunc‘𝐷) ⇒ ⊢ (𝜑 → (𝐼 ∘func 𝐹) = 𝐹) | ||
Theorem | cofurid 16374 | The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘func 𝐼) = 𝐹) | ||
Theorem | resfval 16375* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 ↾f 𝐻) = 〈((1st ‘𝐹) ↾ dom dom 𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))〉) | ||
Theorem | resfval2 16376* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (〈𝐹, 𝐺〉 ↾f 𝐻) = 〈(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))〉) | ||
Theorem | resf1st 16377 | Value of the functor restriction operator on objects. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (1st ‘(𝐹 ↾f 𝐻)) = ((1st ‘𝐹) ↾ 𝑆)) | ||
Theorem | resf2nd 16378 | Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘(𝐹 ↾f 𝐻))𝑌) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) | ||
Theorem | funcres 16379 | A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ↾f 𝐻) ∈ ((𝐶 ↾cat 𝐻) Func 𝐷)) | ||
Theorem | funcres2b 16380* | 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 16381 | 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 16382 | A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈) | ||
Theorem | funcpropd 16383 | 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 16384 | 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 16385 | Extend class notation with the class of all full functors. |
class Full | ||
Syntax | cfth 16386 | Extend class notation with the class of all faithful functors. |
class Faith | ||
Definition | df-full 16387* | 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 16388* | Function returning all the faithful functors from a category 𝐶 to a category 𝐷. A full 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 16389 | A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷) | ||
Theorem | fthfunc 16390 | A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷) | ||
Theorem | relfull 16391 | The set of full functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ Rel (𝐶 Full 𝐷) | ||
Theorem | relfth 16392 | The set of faithful functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ Rel (𝐶 Faith 𝐷) | ||
Theorem | isfull 16393* | Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) ⇒ ⊢ (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ran (𝑥𝐺𝑦) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
Theorem | isfull2 16394* | Equivalent condition for a full functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–onto→((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
Theorem | fullfo 16395 | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–onto→((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
Theorem | fulli 16396* | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ (𝑋𝐻𝑌)𝑅 = ((𝑋𝐺𝑌)‘𝑓)) | ||
Theorem | isfth 16397* | Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))) | ||
Theorem | isfth2 16398* | Equivalent condition for a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) ⇒ ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–1-1→((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
Theorem | isffth2 16399* | 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 16400 | The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–1-1→((𝐹‘𝑋)𝐽(𝐹‘𝑌))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |