Add (full) subcategory, explain embedding

trees/tt-000G.tree

@@ -17,6 +17,8 @@
 
 \transclude{tt-000H}
 
+\transclude{tt-002Y}
+
 \transclude{tt-000M}
 
 \transclude{tt-002W}

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
 }
 

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.}
+}

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}}