Home | Metamath
Proof Explorer Theorem List (p. 166 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | subcfn 16501 | An element in the set of subcategories is a binary function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Subcat | ||
Theorem | subcss1 16502 | The objects of a subcategory are a subset of the objects of the original. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Subcat | ||
Theorem | subcss2 16503 | The morphisms of a subcategory are a subset of the morphisms of the original. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Subcat | ||
Theorem | subcidcl 16504 | The identity of the original category is contained in each subcategory. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Subcat | ||
Theorem | subccocl 16505 | A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Subcat comp | ||
Theorem | subccatid 16506* | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
cat Subcat | ||
Theorem | subcid 16507 | The identity in a subcategory is the same as the original category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
cat Subcat | ||
Theorem | subccat 16508 | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
cat Subcat | ||
Theorem | issubc3 16509* | 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 17348, for the same reasons, since categories are a generalization of monoids. (Contributed by Mario Carneiro, 6-Jan-2017.) |
f cat Subcat cat | ||
Theorem | fullsubc 16510 | 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.) |
f Subcat | ||
Theorem | fullresc 16511 | The category formed by structure restriction is the same as the category restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
f ↾s cat f f compf compf | ||
Theorem | resscat 16512 | A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
↾s | ||
Theorem | subsubc 16513 | A subcategory of a subcategory is a subcategory. (Contributed by Mario Carneiro, 6-Jan-2017.) |
cat Subcat Subcat Subcat cat | ||
Syntax | cfunc 16514 | Extend class notation with the class of all functors. |
Syntax | cidfu 16515 | Extend class notation with identity functor. |
idfunc | ||
Syntax | ccofu 16516 | Extend class notation with functor composition. |
func | ||
Syntax | cresf 16517 | Extend class notation to include restriction of a functor to a subcategory. |
f | ||
Definition | df-func 16518* | 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.) |
comp comp | ||
Definition | df-idfu 16519* | Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
idfunc | ||
Definition | df-cofu 16520* | Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
func | ||
Definition | df-resf 16521* | Define the restriction of a functor to a subcategory (analogue of df-res 5126). (Contributed by Mario Carneiro, 6-Jan-2017.) |
f | ||
Theorem | relfunc 16522 | The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | funcrcl 16523 | Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Theorem | isfunc 16524* | Value of the set of functors between two categories. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp comp | ||
Theorem | isfuncd 16525* | Deduce that an operation is a functor of categories. (Contributed by Mario Carneiro, 4-Jan-2017.) |
comp comp | ||
Theorem | funcf1 16526 | The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | funcixp 16527* | The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | funcf2 16528 | The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | funcfn2 16529 | The morphism part of a functor is a function. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | funcid 16530 | A functor maps each identity to the corresponding identity in the target category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | funcco 16531 | A functor maps composition in the source category to composition in the target. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp comp | ||
Theorem | funcsect 16532 | The image of a section under a functor is a section. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Sect Sect | ||
Theorem | funcinv 16533 | The image of an inverse under a functor is an inverse. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Inv Inv | ||
Theorem | funciso 16534 | 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.) |
Theorem | funcoppc 16535 | 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 tpos | ||
Theorem | idfuval 16536* | Value of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
idfunc | ||
Theorem | idfu2nd 16537 | Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
idfunc | ||
Theorem | idfu2 16538 | Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-Jan-2017.) |
idfunc | ||
Theorem | idfu1st 16539 | Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
idfunc | ||
Theorem | idfu1 16540 | Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
idfunc | ||
Theorem | idfucl 16541 | The identity functor is a functor. Example 3.20(1) of [Adamek] p. 30. (Contributed by Mario Carneiro, 3-Jan-2017.) |
idfunc | ||
Theorem | cofuval 16542* | Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
func | ||
Theorem | cofu1st 16543 | Value of the object part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
func | ||
Theorem | cofu1 16544 | Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.) |
func | ||
Theorem | cofu2nd 16545 | Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
func | ||
Theorem | cofu2 16546 | Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.) |
func | ||
Theorem | cofuval2 16547* | Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
func | ||
Theorem | cofucl 16548 | The composition of two functors is a functor. Proposition 3.23 of [Adamek] p. 33. (Contributed by Mario Carneiro, 3-Jan-2017.) |
func | ||
Theorem | cofuass 16549 | Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017.) |
func func func func | ||
Theorem | cofulid 16550 | The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
idfunc func | ||
Theorem | cofurid 16551 | The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.) |
idfunc func | ||
Theorem | resfval 16552* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
f | ||
Theorem | resfval2 16553* | Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.) |
f | ||
Theorem | resf1st 16554 | Value of the functor restriction operator on objects. (Contributed by Mario Carneiro, 6-Jan-2017.) |
f | ||
Theorem | resf2nd 16555 | Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017.) |
f | ||
Theorem | funcres 16556 | A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Subcat f cat | ||
Theorem | funcres2b 16557* | Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Subcat cat | ||
Theorem | funcres2 16558 | A functor into a restricted category is also a functor into the whole category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Subcat cat | ||
Theorem | wunfunc 16559 | A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017.) |
WUni | ||
Theorem | funcpropd 16560 | 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.) |
f f compf compf f f compf compf | ||
Theorem | funcres2c 16561 | Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
↾s | ||
Syntax | cful 16562 | Extend class notation with the class of all full functors. |
Full | ||
Syntax | cfth 16563 | Extend class notation with the class of all faithful functors. |
Faith | ||
Definition | df-full 16564* | 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 | ||
Definition | df-fth 16565* | 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 | ||
Theorem | fullfunc 16566 | A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Full | ||
Theorem | fthfunc 16567 | A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Faith | ||
Theorem | relfull 16568 | The set of full functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Full | ||
Theorem | relfth 16569 | The set of faithful functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Faith | ||
Theorem | isfull 16570* | Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Full | ||
Theorem | isfull2 16571* | Equivalent condition for a full functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Full | ||
Theorem | fullfo 16572 | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Full | ||
Theorem | fulli 16573* | The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Full | ||
Theorem | isfth 16574* | Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Faith | ||
Theorem | isfth2 16575* | Equivalent condition for a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Faith | ||
Theorem | isffth2 16576* | A fully faithful functor is a functor which is bijective on hom-sets. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Full Faith | ||
Theorem | fthf1 16577 | The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Faith | ||
Theorem | fthi 16578 | The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Faith | ||
Theorem | ffthf1o 16579 | The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017.) |
Full Faith | ||
Theorem | fullpropd 16580 | 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.) |
f f compf compf f f compf compf Full Full | ||
Theorem | fthpropd 16581 | 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.) |
f f compf compf f f compf compf Faith Faith | ||
Theorem | fulloppc 16582 | 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 16583 | 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 16584 | 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 16585 | A faithful functor reflects sections. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Faith Sect Sect | ||
Theorem | fthinv 16586 | A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Faith Inv Inv | ||
Theorem | fthmon 16587 | A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Faith Mono Mono | ||
Theorem | fthepi 16588 | A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Faith Epi Epi | ||
Theorem | ffthiso 16589 | A fully faithful functor reflects isomorphisms. Corollary 3.32 of [Adamek] p. 35. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Faith Full | ||
Theorem | fthres2b 16590* | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Subcat Faith Faith cat | ||
Theorem | fthres2c 16591 | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
↾s Faith Faith | ||
Theorem | fthres2 16592 | 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 16593 | The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
idfunc Full Faith | ||
Theorem | cofull 16594 | 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 16595 | 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 16596 | 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 16597 | The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
cat idfunc Subcat Faith | ||
Theorem | ressffth 16598 | 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 Full Faith | ||
Theorem | fullres2c 16599 | Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
↾s Full Full | ||
Theorem | ffthres2c 16600 | Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.) |
↾s Full Faith Full Faith |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |