P. 158 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15701-15800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subccocl 15701	A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> J e. (Subcat ` C ) )   &    |- ( ph -> J Fn ( S X. S ) )   &    |- ( ph -> X e. S )   &    |- .x. = (comp ` C )   &    |- ( ph -> Y e. S )   &    |- ( ph -> Z e. S )   &    |- ( ph -> F e. ( X J Y ) )   &    |- ( ph -> G e. ( Y J Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) )
Theorem	subccatid 15702*	A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat J )   &    |- ( ph -> J e. (Subcat ` C ) )   &    |- ( ph -> J Fn ( S X. S ) )   &    |- .1. = ( Id ` C )   =>    |- ( ph -> ( D e. Cat /\ ( Id ` D ) = ( x e. S |-> ( .1. ` x ) ) ) )
Theorem	subcid 15703	The identity in a subcategory is the same as the original category. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat J )   &    |- ( ph -> J e. (Subcat ` C ) )   &    |- ( ph -> J Fn ( S X. S ) )   &    |- .1. = ( Id ` C )   &    |- ( ph -> X e. S )   =>    |- ( ph -> ( .1. ` X ) = ( ( Id ` D ) ` X ) )
Theorem	subccat 15704	A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat J )   &    |- ( ph -> J e. (Subcat ` C ) )   =>    |- ( ph -> D e. Cat )
Theorem	issubc3 15705*	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 16546, for the same reasons, since categories are a generalization of monoids. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- H = ( Hom f ` C )   &    |- .1. = ( Id ` C )   &    |- D = ( C |`cat J )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> J Fn ( S X. S ) )   =>    |- ( ph -> ( J e. (Subcat ` C ) <-> ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) )
Theorem	fullsubc 15706	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.)
|- B = ( Base ` C )   &    |- H = ( Hom f ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> S C_ B )   =>    |- ( ph -> ( H |` ( S X. S ) ) e. (Subcat ` C ) )
Theorem	fullresc 15707	The category formed by structure restriction is the same as the category restriction. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom f ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> S C_ B )   &    |- D = ( C ↾s S )   &    |- E = ( C |`cat ( H |` ( S X. S ) ) )   =>    |- ( ph -> ( ( Hom f ` D ) = ( Hom f ` E ) /\ (compf ` D ) = (compf ` E ) ) )
Theorem	resscat 15708	A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ( C e. Cat /\ S e. V ) -> ( C ↾s S ) e. Cat )
Theorem	subsubc 15709	A subcategory of a subcategory is a subcategory. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- D = ( C |`cat H )   =>    |- ( H e. (Subcat ` C ) -> ( J e. (Subcat ` D ) <-> ( J e. (Subcat ` C ) /\ J C_cat H ) ) )
8.1.7  Functors
Syntax	cfunc 15710	Extend class notation with the class of all functors.
class Func
Syntax	cidfu 15711	Extend class notation with identity functor.
class idfunc
Syntax	ccofu 15712	Extend class notation with functor composition.
class o.func
Syntax	cresf 15713	Extend class notation to include restriction of a functor to a subcategory.
class |`f
Definition	df-func 15714*	Function returning all the functors from a category t to a category u. Definition 3.17 of [Adamek] p. 29, and definition in [Lang] p. 62 ("covariant functor"). Intuitively a functor associates any morphism of t to a morphism of u, any object of t to an object of u, and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of t to an object of u we write it associates any identity of t to an identity of u 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 = ( t e. Cat , u e. Cat |-> { <. f , g >. | [. ( Base ` t ) / b ]. ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) } )
Definition	df-idfu 15715*	Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- idfunc = ( t e. Cat |-> [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. )
Definition	df-cofu 15716*	Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )
Definition	df-resf 15717*	Define the restriction of a functor to a subcategory (analogue of df-res 4866). (Contributed by Mario Carneiro, 6-Jan-2017.)
|- |`f = ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. )
Theorem	relfunc 15718	The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- Rel ( D Func E )
Theorem	funcrcl 15719	Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( F e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )
Theorem	isfunc 15720*	Value of the set of functors between two categories. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- C = ( Base ` E )   &    |- H = ( Hom ` D )   &    |- J = ( Hom ` E )   &    |- .1. = ( Id ` D )   &    |- I = ( Id ` E )   &    |- .x. = (comp ` D )   &    |- O = (comp ` E )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   =>    |- ( ph -> ( F ( D Func E ) G <-> ( F : B --> C /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. B ( ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) ) )
Theorem	isfuncd 15721*	Deduce that an operation is a functor of categories. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- B = ( Base ` D )   &    |- C = ( Base ` E )   &    |- H = ( Hom ` D )   &    |- J = ( Hom ` E )   &    |- .1. = ( Id ` D )   &    |- I = ( Id ` E )   &    |- .x. = (comp ` D )   &    |- O = (comp ` E )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> F : B --> C )   &    |- ( ph -> G Fn ( B X. B ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )   &    |- ( ( ph /\ x e. B ) -> ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) )   =>    |- ( ph -> F ( D Func E ) G )
Theorem	funcf1 15722	The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- C = ( Base ` E )   &    |- ( ph -> F ( D Func E ) G )   =>    |- ( ph -> F : B --> C )
Theorem	funcixp 15723*	The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- H = ( Hom ` D )   &    |- J = ( Hom ` E )   &    |- ( ph -> F ( D Func E ) G )   =>    |- ( ph -> G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
Theorem	funcf2 15724	The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- H = ( Hom ` D )   &    |- J = ( Hom ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X G Y ) : ( X H Y ) --> ( ( F ` X ) J ( F ` Y ) ) )
Theorem	funcfn2 15725	The morphism part of a functor is a function. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` D )   &    |- ( ph -> F ( D Func E ) G )   =>    |- ( ph -> G Fn ( B X. B ) )
Theorem	funcid 15726	A functor maps each identity to the corresponding identity in the target category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- .1. = ( Id ` D )   &    |- I = ( Id ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( X G X ) ` ( .1. ` X ) ) = ( I ` ( F ` X ) ) )
Theorem	funcco 15727	A functor maps composition in the source category to composition in the target. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- H = ( Hom ` D )   &    |- .x. = (comp ` D )   &    |- O = (comp ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> M e. ( X H Y ) )   &    |- ( ph -> N e. ( Y H Z ) )   =>    |- ( ph -> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) )
Theorem	funcsect 15728	The image of a section under a functor is a section. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- S = (Sect ` D )   &    |- T = (Sect ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> M ( X S Y ) N )   =>    |- ( ph -> ( ( X G Y ) ` M ) ( ( F ` X ) T ( F ` Y ) ) ( ( Y G X ) ` N ) )
Theorem	funcinv 15729	The image of an inverse under a functor is an inverse. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` D )   &    |- I = (Inv ` D )   &    |- J = (Inv ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> M ( X I Y ) N )   =>    |- ( ph -> ( ( X G Y ) ` M ) ( ( F ` X ) J ( F ` Y ) ) ( ( Y G X ) ` N ) )
Theorem	funciso 15730	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.)
|- B = ( Base ` D )   &    |- I = ( Iso ` D )   &    |- J = ( Iso ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> M e. ( X I Y ) )   =>    |- ( ph -> ( ( X G Y ) ` M ) e. ( ( F ` X ) J ( F ` Y ) ) )
Theorem	funcoppc 15731	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.)
|- O = (oppCat ` C )   &    |- P = (oppCat ` D )   &    |- ( ph -> F ( C Func D ) G )   =>    |- ( ph -> F ( O Func P )tpos G )
Theorem	idfuval 15732*	Value of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- H = ( Hom ` C )   =>    |- ( ph -> I = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
Theorem	idfu2nd 15733	Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( 2nd ` I ) Y ) = ( _I |` ( X H Y ) ) )
Theorem	idfu2 15734	Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- I = (idfunc ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( ( X ( 2nd ` I ) Y ) ` F ) = F )
Theorem	idfu1st 15735	Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   =>    |- ( ph -> ( 1st ` I ) = ( _I |` B ) )
Theorem	idfu1 15736	Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( 1st ` I ) ` X ) = X )
Theorem	idfucl 15737	The identity functor is a functor. Example 3.20(1) of [Adamek] p. 30. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   =>    |- ( C e. Cat -> I e. ( C Func C ) )
Theorem	cofuval 15738*	Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   =>    |- ( ph -> ( G o.func F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
Theorem	cofu1st 15739	Value of the object part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   =>    |- ( ph -> ( 1st ` ( G o.func F ) ) = ( ( 1st ` G ) o. ( 1st ` F ) ) )
Theorem	cofu1 15740	Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( 1st ` ( G o.func F ) ) ` X ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) )
Theorem	cofu2nd 15741	Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( 2nd ` ( G o.func F ) ) Y ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) )
Theorem	cofu2 15742	Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- H = ( Hom ` C )   &    |- ( ph -> R e. ( X H Y ) )   =>    |- ( ph -> ( ( X ( 2nd ` ( G o.func F ) ) Y ) ` R ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) )
Theorem	cofuval2 15743*	Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F ( C Func D ) G )   &    |- ( ph -> H ( D Func E ) K )   =>    |- ( ph -> ( <. H , K >. o.func <. F , G >. ) = <. ( H o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) K ( F ` y ) ) o. ( x G y ) ) ) >. )
Theorem	cofucl 15744	The composition of two functors is a functor. Proposition 3.23 of [Adamek] p. 33. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   =>    |- ( ph -> ( G o.func F ) e. ( C Func E ) )
Theorem	cofuass 15745	Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> G e. ( C Func D ) )   &    |- ( ph -> H e. ( D Func E ) )   &    |- ( ph -> K e. ( E Func F ) )   =>    |- ( ph -> ( ( K o.func H ) o.func G ) = ( K o.func ( H o.func G ) ) )
Theorem	cofulid 15746	The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> F e. ( C Func D ) )   &    |- I = (idfunc ` D )   =>    |- ( ph -> ( I o.func F ) = F )
Theorem	cofurid 15747	The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> F e. ( C Func D ) )   &    |- I = (idfunc ` C )   =>    |- ( ph -> ( F o.func I ) = F )
Theorem	resfval 15748*	Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> H e. W )   =>    |- ( ph -> ( F |`f H ) = <. ( ( 1st ` F ) |` dom dom H ) , ( x e. dom H |-> ( ( ( 2nd ` F ) ` x ) |` ( H ` x ) ) ) >. )
Theorem	resfval2 15749*	Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> H e. W )   &    |- ( ph -> G e. X )   &    |- ( ph -> H Fn ( S X. S ) )   =>    |- ( ph -> ( <. F , G >. |`f H ) = <. ( F |` S ) , ( x e. S , y e. S |-> ( ( x G y ) |` ( x H y ) ) ) >. )
Theorem	resf1st 15750	Value of the functor restriction operator on objects. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> H e. W )   &    |- ( ph -> H Fn ( S X. S ) )   =>    |- ( ph -> ( 1st ` ( F |`f H ) ) = ( ( 1st ` F ) |` S ) )
Theorem	resf2nd 15751	Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> H e. W )   &    |- ( ph -> H Fn ( S X. S ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   =>    |- ( ph -> ( X ( 2nd ` ( F |`f H ) ) Y ) = ( ( X ( 2nd ` F ) Y ) |` ( X H Y ) ) )
Theorem	funcres 15752	A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> H e. (Subcat ` C ) )   =>    |- ( ph -> ( F |`f H ) e. ( ( C |`cat H ) Func D ) )
Theorem	funcres2b 15753*	Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- A = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> R e. (Subcat ` D ) )   &    |- ( ph -> R Fn ( S X. S ) )   &    |- ( ph -> F : A --> S )   &    |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x G y ) : Y --> ( ( F ` x ) R ( F ` y ) ) )   =>    |- ( ph -> ( F ( C Func D ) G <-> F ( C Func ( D |`cat R ) ) G ) )
Theorem	funcres2 15754	A functor into a restricted category is also a functor into the whole category. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( R e. (Subcat ` D ) -> ( C Func ( D |`cat R ) ) C_ ( C Func D ) )
Theorem	wunfunc 15755	A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- ( ph -> U e. WUni )   &    |- ( ph -> C e. U )   &    |- ( ph -> D e. U )   =>    |- ( ph -> ( C Func D ) e. U )
Theorem	funcpropd 15756	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.)
|- ( ph -> ( Hom f ` A ) = ( Hom f ` B ) )   &    |- ( ph -> (compf ` A ) = (compf ` B ) )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( A Func C ) = ( B Func D ) )
Theorem	funcres2c 15757	Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
|- A = ( Base ` C )   &    |- E = ( D ↾s S )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> S e. V )   &    |- ( ph -> F : A --> S )   =>    |- ( ph -> ( F ( C Func D ) G <-> F ( C Func E ) G ) )
8.1.8  Full & faithful functors
Syntax	cful 15758	Extend class notation with the class of all full functors.
class Full
Syntax	cfth 15759	Extend class notation with the class of all faithful functors.
class Faith
Definition	df-full 15760*	Function returning all the full functors from a category C to a category D. A full functor is a functor in which all the morphism maps G ( X , Y ) between objects X , Y e. C are surjections. Definition 3.27(3) in [Adamek] p. 34. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- Full = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } )
Definition	df-fth 15761*	Function returning all the faithful functors from a category C to a category D. A full functor is a functor in which all the morphism maps G ( X , Y ) between objects X , Y e. C are injections. Definition 3.27(2) in [Adamek] p. 34. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- Faith = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } )
Theorem	fullfunc 15762	A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( C Full D ) C_ ( C Func D )
Theorem	fthfunc 15763	A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( C Faith D ) C_ ( C Func D )
Theorem	relfull 15764	The set of full functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- Rel ( C Full D )
Theorem	relfth 15765	The set of faithful functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- Rel ( C Faith D )
Theorem	isfull 15766*	Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- J = ( Hom ` D )   =>    |- ( F ( C Full D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
Theorem	isfull2 15767*	Equivalent condition for a full functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- J = ( Hom ` D )   &    |- H = ( Hom ` C )   =>    |- ( F ( C Full D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) )
Theorem	fullfo 15768	The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- J = ( Hom ` D )   &    |- H = ( Hom ` C )   &    |- ( ph -> F ( C Full D ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X G Y ) : ( X H Y ) -onto-> ( ( F ` X ) J ( F ` Y ) ) )
Theorem	fulli 15769*	The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- J = ( Hom ` D )   &    |- H = ( Hom ` C )   &    |- ( ph -> F ( C Full D ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> R e. ( ( F ` X ) J ( F ` Y ) ) )   =>    |- ( ph -> E. f e. ( X H Y ) R = ( ( X G Y ) ` f ) )
Theorem	isfth 15770*	Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   =>    |- ( F ( C Faith D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B Fun `' ( x G y ) ) )
Theorem	isfth2 15771*	Equivalent condition for a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   =>    |- ( F ( C Faith D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) ) )
Theorem	isffth2 15772*	A fully faithful functor is a functor which is bijective on hom-sets. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   =>    |- ( F ( ( C Full D ) i^i ( C Faith D ) ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-onto-> ( ( F ` x ) J ( F ` y ) ) ) )
Theorem	fthf1 15773	The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- ( ph -> F ( C Faith D ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) )
Theorem	fthi 15774	The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- ( ph -> F ( C Faith D ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> R e. ( X H Y ) )   &    |- ( ph -> S e. ( X H Y ) )   =>    |- ( ph -> ( ( ( X G Y ) ` R ) = ( ( X G Y ) ` S ) <-> R = S ) )
Theorem	ffthf1o 15775	The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- ( ph -> F ( ( C Full D ) i^i ( C Faith D ) ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X G Y ) : ( X H Y ) -1-1-onto-> ( ( F ` X ) J ( F ` Y ) ) )
Theorem	fullpropd 15776	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.)
|- ( ph -> ( Hom f ` A ) = ( Hom f ` B ) )   &    |- ( ph -> (compf ` A ) = (compf ` B ) )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( A Full C ) = ( B Full D ) )
Theorem	fthpropd 15777	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.)
|- ( ph -> ( Hom f ` A ) = ( Hom f ` B ) )   &    |- ( ph -> (compf ` A ) = (compf ` B ) )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( A Faith C ) = ( B Faith D ) )
Theorem	fulloppc 15778	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.)
|- O = (oppCat ` C )   &    |- P = (oppCat ` D )   &    |- ( ph -> F ( C Full D ) G )   =>    |- ( ph -> F ( O Full P )tpos G )
Theorem	fthoppc 15779	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.)
|- O = (oppCat ` C )   &    |- P = (oppCat ` D )   &    |- ( ph -> F ( C Faith D ) G )   =>    |- ( ph -> F ( O Faith P )tpos G )
Theorem	ffthoppc 15780	The opposite functor of a fully faithful functor is also full and faithful. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- O = (oppCat ` C )   &    |- P = (oppCat ` D )   &    |- ( ph -> F ( ( C Full D ) i^i ( C Faith D ) ) G )   =>    |- ( ph -> F ( ( O Full P ) i^i ( O Faith P ) )tpos G )
Theorem	fthsect 15781	A faithful functor reflects sections. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> F ( C Faith D ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> M e. ( X H Y ) )   &    |- ( ph -> N e. ( Y H X ) )   &    |- S = (Sect ` C )   &    |- T = (Sect ` D )   =>    |- ( ph -> ( M ( X S Y ) N <-> ( ( X G Y ) ` M ) ( ( F ` X ) T ( F ` Y ) ) ( ( Y G X ) ` N ) ) )
Theorem	fthinv 15782	A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> F ( C Faith D ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> M e. ( X H Y ) )   &    |- ( ph -> N e. ( Y H X ) )   &    |- I = (Inv ` C )   &    |- J = (Inv ` D )   =>    |- ( ph -> ( M ( X I Y ) N <-> ( ( X G Y ) ` M ) ( ( F ` X ) J ( F ` Y ) ) ( ( Y G X ) ` N ) ) )
Theorem	fthmon 15783	A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> F ( C Faith D ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> R e. ( X H Y ) )   &    |- M = (Mono ` C )   &    |- N = (Mono ` D )   &    |- ( ph -> ( ( X G Y ) ` R ) e. ( ( F ` X ) N ( F ` Y ) ) )   =>    |- ( ph -> R e. ( X M Y ) )
Theorem	fthepi 15784	A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> F ( C Faith D ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> R e. ( X H Y ) )   &    |- E = (Epi ` C )   &    |- P = (Epi ` D )   &    |- ( ph -> ( ( X G Y ) ` R ) e. ( ( F ` X ) P ( F ` Y ) ) )   =>    |- ( ph -> R e. ( X E Y ) )
Theorem	ffthiso 15785	A fully faithful functor reflects isomorphisms. Corollary 3.32 of [Adamek] p. 35. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> F ( C Faith D ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> R e. ( X H Y ) )   &    |- ( ph -> F ( C Full D ) G )   &    |- I = ( Iso ` C )   &    |- J = ( Iso ` D )   =>    |- ( ph -> ( R e. ( X I Y ) <-> ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) )
Theorem	fthres2b 15786*	Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- A = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> R e. (Subcat ` D ) )   &    |- ( ph -> R Fn ( S X. S ) )   &    |- ( ph -> F : A --> S )   &    |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x G y ) : Y --> ( ( F ` x ) R ( F ` y ) ) )   =>    |- ( ph -> ( F ( C Faith D ) G <-> F ( C Faith ( D |`cat R ) ) G ) )
Theorem	fthres2c 15787	Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
|- A = ( Base ` C )   &    |- E = ( D ↾s S )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> S e. V )   &    |- ( ph -> F : A --> S )   =>    |- ( ph -> ( F ( C Faith D ) G <-> F ( C Faith E ) G ) )
Theorem	fthres2 15788	A faithful functor into a restricted category is also a faithful functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- ( R e. (Subcat ` D ) -> ( C Faith ( D |`cat R ) ) C_ ( C Faith D ) )
Theorem	idffth 15789	The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- I = (idfunc ` C )   =>    |- ( C e. Cat -> I e. ( ( C Full C ) i^i ( C Faith C ) ) )
Theorem	cofull 15790	The composition of two full functors is full. Proposition 3.30(d) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- ( ph -> F e. ( C Full D ) )   &    |- ( ph -> G e. ( D Full E ) )   =>    |- ( ph -> ( G o.func F ) e. ( C Full E ) )
Theorem	cofth 15791	The composition of two faithful functors is faithful. Proposition 3.30(c) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- ( ph -> F e. ( C Faith D ) )   &    |- ( ph -> G e. ( D Faith E ) )   =>    |- ( ph -> ( G o.func F ) e. ( C Faith E ) )
Theorem	coffth 15792	The composition of two fully faithful functors is fully faithful. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- ( ph -> F e. ( ( C Full D ) i^i ( C Faith D ) ) )   &    |- ( ph -> G e. ( ( D Full E ) i^i ( D Faith E ) ) )   =>    |- ( ph -> ( G o.func F ) e. ( ( C Full E ) i^i ( C Faith E ) ) )
Theorem	rescfth 15793	The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- D = ( C |`cat J )   &    |- I = (idfunc ` D )   =>    |- ( J e. (Subcat ` C ) -> I e. ( D Faith C ) )
Theorem	ressffth 15794	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.)
|- D = ( C ↾s S )   &    |- I = (idfunc ` D )   =>    |- ( ( C e. Cat /\ S e. V ) -> I e. ( ( D Full C ) i^i ( D Faith C ) ) )
Theorem	fullres2c 15795	Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
|- A = ( Base ` C )   &    |- E = ( D ↾s S )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> S e. V )   &    |- ( ph -> F : A --> S )   =>    |- ( ph -> ( F ( C Full D ) G <-> F ( C Full E ) G ) )
Theorem	ffthres2c 15796	Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- A = ( Base ` C )   &    |- E = ( D ↾s S )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> S e. V )   &    |- ( ph -> F : A --> S )   =>    |- ( ph -> ( F ( ( C Full D ) i^i ( C Faith D ) ) G <-> F ( ( C Full E ) i^i ( C Faith E ) ) G ) )
8.1.9  Natural transformations and the functor category
Syntax	cnat 15797	Extend class notation to include the collection of natural transformations.
class Nat
Syntax	cfuc 15798	Extend class notation to include the functor category.
class FuncCat
Definition	df-nat 15799*	Definition of a natural transformation between two functors. A natural transformation A : F --> G is a collection of arrows A ( x ) : F ( x ) --> G ( x ), such that A ( y ) o. F ( h ) = G ( h ) o. A ( x ) for each morphism h : x --> y. Definition 6.1 in [Adamek] p. 83, and definition in [Lang] p. 65. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Nat = ( t e. Cat , u e. Cat |-> ( f e. ( t Func u ) , g e. ( t Func u ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` t ) ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) | A. x e. ( Base ` t ) A. y e. ( Base ` t ) A. h e. ( x ( Hom ` t ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. (comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. (comp ` u ) ( s ` y ) ) ( a ` x ) ) } ) )
Definition	df-fuc 15800*	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 = ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. (comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )