diff --git a/trees/tt-000G.tree b/trees/tt-000G.tree index 6c5a2f2..fb0ce9e 100644 --- a/trees/tt-000G.tree +++ b/trees/tt-000G.tree @@ -17,6 +17,8 @@ \transclude{tt-000H} +\transclude{tt-002Y} + \transclude{tt-000M} \transclude{tt-002W} diff --git a/trees/tt-002V.tree b/trees/tt-002V.tree index 1614021..68ac4a0 100644 --- a/trees/tt-002V.tree +++ b/trees/tt-002V.tree @@ -21,9 +21,12 @@ a natural transformation #{H_X \to F} is an \vocabk{element}{tt-000M} of #{F(X)} What kind of presheaves are already "built in" to the category #{\C}? } } -\p{The answer by the Yoneda lemma is, the Yoneda embedding #{H_{\bullet}: \C \to [\C^{op}, \Set]} embeds #{\C} into its own presheaf category. So, #{\C} is equivalent to the full subcategory of the presheaf category #{[\C^{op}, \Set]} whose objects are the \vocabk{representables}{tt-002M}. +\p{The answer by the Yoneda lemma is, the Yoneda embedding #{H_{\bullet}: \C \to [\C^{op}, \Set]} embeds #{\C} into its own presheaf category.} + +\p{In mathematics at large, the word "embedding" is used (sometimes informally) to mean a map #{i: X \to Y} that makes #{X} isomorphic to its image in #{Y}, i.e. #{X \iso i(X)}. \citet{1.3.19}{leinster2016basic} tells us that in category theory, a full and faithful functor #{I: X \to Y} can reasonably be called an embedding, as it makes #{X} equivalent to a full subcategory of #{Y}.} + +\p{So, #{\C} is equivalent to the \vocabk{full subcategory}{tt-002Y} of the presheaf category #{[\C^{op}, \Set]} whose objects are the \vocabk{representables}{tt-002M}. } -% TODO: full subcategory % TODO: Every presheaf is a colimit of representables } diff --git a/trees/tt-002Y.tree b/trees/tt-002Y.tree new file mode 100644 index 0000000..046f146 --- /dev/null +++ b/trees/tt-002Y.tree @@ -0,0 +1,20 @@ +\import{tt-macros} +% clifford hopf spin tt math draft +\tag{tt} + +% definition theorem lemma construction observation +% convention corollary axiom example exercise proof +% discussion remark notation +% \taxon{} + +\refdeft{(full) subcategory}{1.2.18}{leinster2016basic}{} + +% kostecki2011introduction leinster2016basic + +\refdef{(full) subcategory}{leinster2016basic}{ +\p{ +Let #{\C} be a category. A \newvocab{subcategory} #{\S} of #{\C} consists of a subclass #{\Ob(\S)} of #{\Ob(\C)} together with, for each #{S, S' \in \Ob(\S)}, a subclass #{\S\left(S, S'\right)} of #{\C\left(S, S'\right)}, such that #{\S} is closed under composition and identities. +} +\p{It is a \newvocab{full subcategory} if #{\S\left(S, S'\right)=\C\left(S, S'\right)} for all #{S, S' \in \Ob(\S)}.} +\p{Whenever #{\S} is a subcategory of a category #{\C} , there is an \newvocab{inclusion functor} #{I : S → A} defined by #{I(S) = S} and #{I( f ) = f} . It is automatically \vocab{faithful}, and it is \vocab{full} iff S is a full subcategory.} +} diff --git a/trees/tt-macros.tree b/trees/tt-macros.tree index 4321ee8..4678fb1 100644 --- a/trees/tt-macros.tree +++ b/trees/tt-macros.tree @@ -16,6 +16,7 @@ \def\D{{\cal D}} \def\E{{\cal E}} \def\J{{\cal J}} +\def\S{{\cal S}} \def\emptycat{\mathrm{0}} \def\termobj{\mathrm{1}}