CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberMapCoconedefMathlib.CategoryTheory.Sites.Point.Map, function or constantEnglish
Let $x_{2}$ be a point of $J$. Let $F$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Let $P$ be a functor of the set of opposites of $D$ and $A$. Then $\operatorname{isColimitPresheafFiberMapCocone}$ applied to $x_{2}$, $F$, $K$ and $P$ is an element of $\operatorname{IsColimit}$ applied to the presheaf fiber map cocone of $K$ and $P$ defined as $\operatorname{isColimitPresheafFiberOfIsCofilteredCocone}$ applied to the composition of the projection of the fiber of $x_{2}$ and $F$, $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Point\_\_map\_aux}$ applied to $x_{2}$, $F$ and $K$ and $P$.
CategoryTheory.GrothendieckTopology.Point.mapdefMathlib.CategoryTheory.Sites.Point.Map, function or constantWording
the map of F and K (from the name)
English
Let $x_{2}$ be a point of $J$. Let $F$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Then the map of $F$ and $K$ is a point of $K$ defined as the point of the composition of the projection of the fiber of $x_{2}$ and $F$ and $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Point\_\_map\_aux}$ applied to $x_{2}$, $F$ and $K$.
CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCoconedefMathlib.CategoryTheory.Sites.Point.Map, function or constantWording
the presheaf fiber map cocone of K and P (from the name)
English
Let $x_{2}$ be a point of $J$. Let $F$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Let $P$ be a functor of the set of opposites of $D$ and $A$. Then the presheaf fiber map cocone of $K$ and $P$ is a cocone of the composition of the opposite of the projection of the fiber of $x_{2}$ and the composition of the opposite of $F$ and $P$.
CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIsodefMathlib.CategoryTheory.Sites.Point.Map, function or constantWording
the presheaf fiber map isomorphism of F and K (from the name)
English
Let $x_{2}$ be a point of $J$. Let $F$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Let $A$ be a set. Then the presheaf fiber map isomorphism of $F$ and $K$ is an isomorphism of the presheaf fiber of the map of $F$ and $K$ and the composition of the action of the left whiskering of the set of opposites of $D$ and $A$ and the opposite of $F$ and the presheaf fiber of $x_{2}$.
CategoryTheory.GrothendieckTopology.Point.presheafFiberMapObjIsodefMathlib.CategoryTheory.Sites.Point.Map, function or constantWording
the presheaf fiber map object isomorphism of K and P (from the name)
English
Let $x_{2}$ be a point of $J$. Let $F$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Let $P$ be a functor of the set of opposites of $D$ and $A$. Then the presheaf fiber map object isomorphism of $K$ and $P$ is an isomorphism of the action of the presheaf fiber of the map of $F$ and $K$ and $P$ and the action of the presheaf fiber of $x_{2}$ and the composition of the opposite of $F$ and $P$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimitPresheafFiberMapCocone}$ applied to $x_{2}$, $F$, $K$ and $P$ and the cocone of $x_{2}$ and the composition of the opposite of $F$ and $P$.
CategoryTheory.GrothendieckTopology.Point.sheafFiberMapIsodefMathlib.CategoryTheory.Sites.Point.Map, function or constantWording
the sheaf fiber map isomorphism of F and K (from the name)
English
Let $x_{2}$ be a point of $J$. Let $F$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Let $A$ be a set. Then the sheaf fiber map isomorphism of $F$ and $K$ is an isomorphism of the sheaf fiber of the map of $F$ and $K$ and the composition of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$ and the sheaf fiber of $x_{2}$ defined as the composition of the left isomorphism whisker of the sheaf to presheaf of $K$ and $A$ and the presheaf fiber map isomorphism of $F$ and $K$ and the composition of the inverse of the associator of the action of the left whiskering of the set of opposites of $D$ and $A$ and the opposite of $F$ and the presheaf fiber of $x_{2}$ and the composition of the right isomorphism whisker of the inverse of the sheaf pushforward continuous composition sheaf to presheaf isomorphism of $J$ and $K$ and the presheaf fiber of $x_{2}$ and the associator of the sheaf to presheaf of $J$ and $A$ and the presheaf fiber of $x_{2}$.
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMapdefMathlib.CategoryTheory.Sites.Point.Map, function or constantWording
the presheaf fiber map of X and x4 (from the name)
English
Let $x_{2}$ be a point of $J$. Let $F$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Let $P$ be a functor of the set of opposites of $D$ and $A$. Let $X$ be an element of $C$. Let $x_{4}$ be an element of the action of the fiber of $x_{2}$ and $X$. Then the presheaf fiber map of $X$ and $x_{4}$ is a homomorphism of the action of $P$ and $\operatorname{op}$ applied to the action of $F$ and $X$ and the action of the presheaf fiber of the map of $F$ and $K$ and $P$ defined as the presheaf fiber of the element of $X$ and $x_{4}$ and $P$.
CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberOfIsCofilteredCoconedefMathlib.CategoryTheory.Sites.Point.OfIsCofiltered, function or constantEnglish
Let $p$ be a functor of $N$ and $C$ such that for all elements $X$ of $C$, for all sieves $R$ of $X$, if $\MembershipmemMACRoT {J (X)}{R}$, then for all elements $U$ of $N$, for all homomorphisms $f$ of the action of $p$ and $U$ and $X$, there exists an element $Y$ of $C$, such that there exists a homomorphism $g$ of $Y$ and $X$, such that there exists an element $h_{5}$ of the arrow of $R$, such that there exists an element $V$ of $N$, such that there exists a homomorphism $q$ of $V$ and $U$, such that there exists a homomorphism $a$ of the action of $p$ and $V$ and $Y$, such that the composition of $a$ and $g$ is equal to the composition of the map of $p$ and $q$ and $f$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{isColimitPresheafFiberOfIsCofilteredCocone}$ applied to $p$, $\mathrm{hp}$ and $P$ is an element of $\operatorname{IsColimit}$ applied to the presheaf fiber of $p$ and $P$ defined as the inverse function of $\operatorname{isColimitWhiskerEquiv}$ applied to the opposite of the functor of $p$ and the cocone of the action of the action of the left whiskering of the set of opposites of $C$ and $A$ and the opposite of the projection of the fiber of the point of $p$ and $\mathrm{hp}$ and $P$ and the cocone of the point of $p$ and $\mathrm{hp}$ and $P$.
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltereddefMathlib.CategoryTheory.Sites.Point.OfIsCofiltered, function or constantWording
the point of p and hp (from the name)
English
Let $p$ be a functor of $N$ and $C$ such that for all elements $X$ of $C$, for all sieves $R$ of $X$, if $\MembershipmemMACRoT {J (X)}{R}$, then for all elements $U$ of $N$, for all homomorphisms $f$ of the action of $p$ and $U$ and $X$, there exists an element $Y$ of $C$, such that there exists a homomorphism $g$ of $Y$ and $X$, such that there exists an element $h_{4}$ of the arrow of $R$, such that there exists an element $V$ of $N$, such that there exists a homomorphism $q$ of $V$ and $U$, such that there exists a homomorphism $a$ of the action of $p$ and $V$ and $Y$, such that the composition of $a$ and $g$ is equal to the composition of the map of $p$ and $q$ and $f$. Then the point of $p$ and $\mathrm{hp}$ is a point of $J$.
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberdefMathlib.CategoryTheory.Sites.Point.OfIsCofiltered, function or constantWording
the fiber of p (from the name)
English
Let $p$ be a functor of $N$ and $C$. Then the fiber of $p$ is a functor of $C$ and the set of sets defined as the composition of the Yoneda embedding and the composition of the action of the left whiskering of the set of opposites of $C$ and the set of sets and the opposite of $p$ and the colimit.
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMkdefMathlib.CategoryTheory.Sites.Point.OfIsCofiltered, function or constantWording
the fiber of f (from the name)
English
Let $f$ be a homomorphism of the action of $p$ and $U$ and $X$. Then the fiber of $f$ is an element of the action of the fiber of $p$ and $X$ defined as $\operatorname{hom}$ applied to the inclusion of the composition of the opposite of $p$ and the action of the Yoneda embedding and $X$ and $\operatorname{op}$ applied to $U$ and $\operatorname{symm}$ applied to the shrink Yoneda object object equivalence and $f$.
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functordefMathlib.CategoryTheory.Sites.Point.OfIsCofiltered, function or constantWording
the functor of p (from the name)
English
Let $p$ be a functor of $N$ and $C$. Then the functor of $p$ is a functor of $N$ and the set of elements of the fiber of $p$.
CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCoconedefMathlib.CategoryTheory.Sites.Point.OfIsCofiltered, function or constantWording
the presheaf fiber of p and P (from the name)
English
Let $p$ be a functor of $N$ and $C$ such that for all elements $X$ of $C$, for all sieves $R$ of $X$, if $\MembershipmemMACRoT {J (X)}{R}$, then for all elements $U$ of $N$, for all homomorphisms $f$ of the action of $p$ and $U$ and $X$, there exists an element $Y$ of $C$, such that there exists a homomorphism $g$ of $Y$ and $X$, such that there exists an element $h_{5}$ of the arrow of $R$, such that there exists an element $V$ of $N$, such that there exists a homomorphism $q$ of $V$ and $U$, such that there exists a homomorphism $a$ of the action of $p$ and $V$ and $Y$, such that the composition of $a$ and $g$ is equal to the composition of the map of $p$ and $q$ and $f$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the presheaf fiber of $p$ and $P$ is a cocone of the composition of the opposite of $p$ and $P$.
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltereddefMathlib.CategoryTheory.Sites.Point.OfIsCofiltered, function or constantWording
the presheaf fiber of U and P (from the name)
English
Let $p$ be a functor of $N$ and $C$ such that for all elements $X$ of $C$, for all sieves $R$ of $X$, if $\MembershipmemMACRoT {J (X)}{R}$, then for all elements $U_{1}$ of $N$, for all homomorphisms $f$ of the action of $p$ and $U_{1}$ and $X$, there exists an element $Y$ of $C$, such that there exists a homomorphism $g$ of $Y$ and $X$, such that there exists an element $h_{5}$ of the arrow of $R$, such that there exists an element $V$ of $N$, such that there exists a homomorphism $q$ of $V$ and $U_{1}$, such that there exists a homomorphism $a$ of the action of $p$ and $V$ and $Y$, such that the composition of $a$ and $g$ is equal to the composition of the map of $p$ and $q$ and $f$. Let $U$ be an element of $N$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the presheaf fiber of $U$ and $P$ is a homomorphism of the action of $P$ and $\operatorname{op}$ applied to the action of $p$ and $U$ and the action of the presheaf fiber of the point of $p$ and $\mathrm{hp}$ and $P$ defined as the presheaf fiber of the fiber of the identity morphism of the action of $p$ and $U$ and $P$.
CategoryTheory.GrothendieckTopology.Point.overdefMathlib.CategoryTheory.Sites.Point.Over, function or constantEnglish
Let $x_{1}$ be a point of $J$. Let $x_{2}$ be an element of the action of the fiber of $x_{1}$ and $X$. Then $\operatorname{over}$ applied to $x_{1}$ and $x_{2}$ is a point of $\operatorname{over}$ applied to $J$ and $X$.
CategoryTheory.GrothendieckTopology.pointBotdefMathlib.CategoryTheory.Sites.Point.Presheaf, function or constantWording
the point bottom of X (from the name)
English
Let $X$ be an element of $C$. Then the point bottom of $X$ is a point of the bottom.
CategoryTheory.GrothendieckTopology.pointBotFunctordefMathlib.CategoryTheory.Sites.Point.Presheaf, function or constantWording
the functor (from the docstring)
English
The functor is a functor of $C$ and the set of points of the bottom.
CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIsodefMathlib.CategoryTheory.Sites.Point.Presheaf, function or constantWording
the fiber functor of X and A (from the docstring)
English
Let $X$ be an element of $C$. Let $A$ be a set. Then the fiber functor of $X$ and $A$ is an isomorphism of the presheaf fiber of the point bottom of $X$ and the action of the evaluation of the set of opposites of $C$ and $A$ and $\operatorname{op}$ applied to $X$ defined as the inverse of $\operatorname{asIso}$ applied to the presheaf fiber natural transformation of $X$ and $\operatorname{symm}$ applied to the shrink Yoneda object object equivalence and the identity morphism of $X$.
CategoryTheory.GrothendieckTopology.pointsBotdefMathlib.CategoryTheory.Sites.Point.Presheaf, function or constantWording
the point bottom of C (from the name)
English
Let $C$ be a set. Then the point bottom of $C$ is an object property of the set of points of the bottom defined as the object property of $\operatorname{pointBot}$.
CategoryTheory.GrothendieckTopology.Point.presheafToSheafCompSheafFiberIsodefMathlib.CategoryTheory.Sites.Point.Skyscraper, function or constantWording
the presheaf to sheaf composition sheaf fiber isomorphism of x1 and A (from the name)
English
Let $x_{1}$ be a point of $J$. Let $A$ be a set. Then the presheaf to sheaf composition sheaf fiber isomorphism of $x_{1}$ and $A$ is an isomorphism of the composition of the presheaf to sheaf of $J$ and $A$ and the sheaf fiber of $x_{1}$ and the presheaf fiber of $x_{1}$.
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafdefMathlib.CategoryTheory.Sites.Point.Skyscraper, function or constantWording
the skyscraper presheaf of x1 and M (from the name)
English
Let $x_{1}$ be a point of $J$. Let $M$ be an element of $A$. Then the skyscraper presheaf of $x_{1}$ and $M$ is a functor of the set of opposites of $C$ and $A$ defined as the action of the skyscraper presheaf functor of $x_{1}$ and $M$.
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunctiondefMathlib.CategoryTheory.Sites.Point.Skyscraper, function or constantWording
the skyscraper presheaf adjunction of x1 (from the name)
English
Let $x_{1}$ be a point of $J$. Then the skyscraper presheaf adjunction of $x_{1}$ is an adjunction of the presheaf fiber of $x_{1}$ and the skyscraper presheaf functor of $x_{1}$ defined as $\operatorname{mkOfHomEquiv}$ applied to $\operatorname{mk}$ applied to the function that maps $x_{3}$ and $x_{4}$ to the skyscraper presheaf homomorphism equivalence of $x_{1}$, the function that maps $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ to $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Point\_\_skyscraperPresheafHomEquiv\_naturality\_left\_symm}$ applied to $x_{1}$, $x_{8}$ and $x_{9}$ and the function that maps $x_{10}$, $x_{11}$, $x_{12}$, $x_{13}$ and $x_{14}$ to $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Point\_\_skyscraperPresheafHomEquiv\_naturality\_right}$ applied to $x_{1}$, $x_{13}$ and $x_{14}$.
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctordefMathlib.CategoryTheory.Sites.Point.Skyscraper, function or constantWording
the skyscraper presheaf functor of x1 (from the name)
English
Let $x_{1}$ be a point of $J$. Then the skyscraper presheaf functor of $x_{1}$ is a functor of $A$ and the set of functors of the set of opposites of $C$ and $A$ defined as the flip of the composition of the opposite of the fiber of $x_{1}$ and the flip of the product constant.
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquivdefMathlib.CategoryTheory.Sites.Point.Skyscraper, function or constantWording
the skyscraper presheaf homomorphism equivalence of x1 (from the name)
English
Let $x_{1}$ be a point of $J$. Then the skyscraper presheaf homomorphism equivalence of $x_{1}$ is an equivalence from the set of homomorphisms of the action of the presheaf fiber of $x_{1}$ and $P$ and $M$ to the set of homomorphisms of $P$ and the skyscraper presheaf of $x_{1}$ and $M$.
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafdefMathlib.CategoryTheory.Sites.Point.Skyscraper, function or constantWording
the skyscraper sheaf of x1 and M (from the name)
English
Let $x_{1}$ be a point of $J$. Let $M$ be an element of $A$. Then the skyscraper sheaf of $x_{1}$ and $M$ is a sheaf of $J$ and $A$ defined as the action of the skyscraper sheaf functor of $x_{1}$ and $M$.
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunctiondefMathlib.CategoryTheory.Sites.Point.Skyscraper, function or constantWording
the skyscraper sheaf adjunction of x1 (from the name)
English
Let $x_{1}$ be a point of $J$. Then the skyscraper sheaf adjunction of $x_{1}$ is an adjunction of the sheaf fiber of $x_{1}$ and the skyscraper sheaf functor of $x_{1}$.
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctordefMathlib.CategoryTheory.Sites.Point.Skyscraper, function or constantWording
the skyscraper sheaf functor of x1 (from the name)
English
Let $x_{1}$ be a point of $J$. Then the skyscraper sheaf functor of $x_{1}$ is a functor of $A$ and the set of sheaves of $J$ and $A$.
CategoryTheory.Functor.PreservesPairwisePullbacksclassMathlib.CategoryTheory.Sites.Precoverage, predicateEnglish
Let $F$ be a functor of $C$ and $D$. Let $R$ be a presieve of $X$. Then we can say that $\operatorname{PreservesPairwisePullbacks}$ holds for $F$ and $R$.
CategoryTheory.PrecoveragestructureMathlib.CategoryTheory.Sites.Precoverage, typeWording
precoverage of C (from the name)
English
Let $C$ be a set. Then the precoverages of $C$ are a basic type.
CategoryTheory.Precoverage.HasIsosclassMathlib.CategoryTheory.Sites.Precoverage, predicateEnglish
Let $J$ be a precoverage of $C$. Then we can say that $\operatorname{HasIsos}$ holds for $J$.
CategoryTheory.Precoverage.HasPullbacksclassMathlib.CategoryTheory.Sites.Precoverage, predicateWording
J has pullbacks (from the name)
English
Let $J$ be a precoverage of $C$. Then we can say that $J$ has pullbacks.
CategoryTheory.Precoverage.IsStableUnderBaseChangeclassMathlib.CategoryTheory.Sites.Precoverage, predicateWording
J is stable under base change (from the docstring)
English
Let $J$ be a precoverage of $C$. Then we can say that $J$ is stable under base change.
CategoryTheory.Precoverage.IsStableUnderCompositionclassMathlib.CategoryTheory.Sites.Precoverage, predicateWording
J is stable under composition (from the docstring)
English
Let $J$ be a precoverage of $C$. Then we can say that $J$ is stable under composition.
CategoryTheory.Precoverage.IsStableUnderSupclassMathlib.CategoryTheory.Sites.Precoverage, predicateWording
J is a stable under supremum (from the name)
English
Let $J$ be a precoverage of $C$. Then we can say that $J$ is a stable under supremum.
CategoryTheory.Precoverage.PullbacksPreservedByclassMathlib.CategoryTheory.Sites.Precoverage, predicateEnglish
Let $J$ be a precoverage of $C$. Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{PullbacksPreservedBy}$ holds for $J$ and $F$.
CategoryTheory.Precoverage.comapdefMathlib.CategoryTheory.Sites.Precoverage, function or constantWording
the preimage of F and J (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $J$ be a precoverage of $D$. Then the preimage of $F$ and $J$ is a precoverage of $C$ defined as $\operatorname{mk}$ applied to the function that maps $Y$ to $\operatorname{ofPred}$ applied to the function that maps $R$ to the proposition that the map of $F$ and $R$ is an element of the covering of $J$ and the action of $F$ and $Y$.
CategoryTheory.Precoverage.coveringsdefMathlib.CategoryTheory.Sites.Precoverage, function or constantWording
the covering of self and X (from the name)
English
Let $\mathrm{self}$ be a precoverage of $C$. Let $X$ be an element of $C$. Then the covering of $\mathrm{self}$ and $X$ is an element of the power set of the set of presieves of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $X$.
CategoryTheory.Precoverage.GeneratesstructureMathlib.CategoryTheory.Sites.Precoverage.Generates, predicateEnglish
Let $K$ be a precoverage of $C$. Let $J$ be a Grothendieck topology of $C$. Then we can say that $\operatorname{Generates}$ holds for $K$ and $J$.
CategoryTheory.Precoverage.SubsheafClosureinductiveMathlib.CategoryTheory.Sites.Precoverage.Subsheaf, predicateEnglish
Let $K$ be a precoverage of $C$. Let $x_{1}$ be a function from elements $Z_{1}$ of $C$ to elements of the power set of the action of $F$ and $\operatorname{op}$ applied to $Z_{1}$. Let $Z$ be an element of $C$. Let $x_{2}$ be an element of the action of $F$ and $\operatorname{op}$ applied to $Z$. Then we can say that $\operatorname{SubsheafClosure}$ holds for $K$, $Z_{1}$, $x_{1}$, $Z$ and $x_{2}$.
CategoryTheory.Precoverage.SubsheafClosure.belowinductiveMathlib.CategoryTheory.Sites.Precoverage.Subsheaf, predicateEnglish
Assume that $\operatorname{SubsheafClosure}$ holds for $K$, $x_{1}$, $Z$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.
CategoryTheory.Precoverage.subsheafifydefMathlib.CategoryTheory.Sites.Precoverage.Subsheaf, function or constantEnglish
Let $K$ be a precoverage of $C$. Let $x_{1}$ be a function from elements $Z$ of $C$ to elements of the power set of the action of $F$ and $\operatorname{op}$ applied to $Z$. Then $\operatorname{subsheafify}$ applied to $K$, $Z$ and $x_{1}$ is a subfunctor of $F$.
CategoryTheory.GrothendieckTopology.toPrecoveragedefMathlib.CategoryTheory.Sites.PrecoverageToGrothendieck, function or constantWording
the induced coverage by a Grothendieck topology as a precoverage of J (from the docstring)
English
Let $J$ be a Grothendieck topology of $C$. Then the induced coverage by a Grothendieck topology as a precoverage of $J$ is a precoverage of $C$ defined as $\operatorname{mk}$ applied to the function that maps $S$ to $\operatorname{ofPred}$ applied to the function that maps $R$ to $\MembershipmemMACRoT {J (S)}{\operatorname{generate} (R)}$.
CategoryTheory.Precoverage.Saturate.belowinductiveMathlib.CategoryTheory.Sites.PrecoverageToGrothendieck, predicateEnglish
Assume that $\operatorname{Saturate}$ holds for $J$, $X$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.
CategoryTheory.Precoverage.toGrothendieckdefMathlib.CategoryTheory.Sites.PrecoverageToGrothendieck, function or constantEnglish
Let $J$ be a precoverage of $C$. Then $\operatorname{toGrothendieck}$ applied to $J$ is a Grothendieck topology of $C$ defined as $\operatorname{mk}$ applied to the function that maps $X$ to $\operatorname{ofPred}$ applied to $\operatorname{Saturate}$ applied to $J$ and $X$, $\operatorname{top}$, the function that maps $x_{1}$, $x_{2}$, $x_{3}$, $x_{4}$ and $\mathrm{hS}$ to $\operatorname{pullback}$ applied to $x_{1}$, $x_{3}$, $\mathrm{hS}$, $x_{2}$ and $x_{4}$ and the function that maps $x_{5}$, $x_{6}$, $\mathrm{hS1}$, $x_{7}$ and $\mathrm{hR}$ to $\operatorname{transitive}$ applied to $x_{5}$, $x_{6}$, $x_{7}$, $\mathrm{hS1}$ and $\mathrm{hR}$.
CategoryTheory.Presieve.isTerminal_of_isSheafFor_empty_presievedefMathlib.CategoryTheory.Sites.Preserves, function or constantEnglish
Let $I$ be an element of $C$. Let $F$ be a functor of the set of opposites of $C$ and the set of sets such that $\operatorname{IsSheafFor}$ holds for $F$ and the presieve of $\operatorname{elim}$ and the function that maps $a$ to the eliminator of $\operatorname{instIsEmpty}$ and $a$. Then $\mathrm{CategoryTheory\_\_Presieve\_\_isTerminal\_of\_isSheafFor\_empty\_presieve}$ applied to $I$, $F$ and $\mathrm{hF}$ is an element of $\operatorname{IsTerminal}$ applied to the action of $F$ and $\operatorname{op}$ applied to $I$ defined as $\operatorname{ofUnique}$ applied to the action of $F$ and $\operatorname{op}$ applied to $I$.
CategoryTheory.GrothendieckTopology.PreservesSheafificationclassMathlib.CategoryTheory.Sites.PreservesSheafification, predicateEnglish
Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $A$ and $B$. Then we can say that $\operatorname{PreservesSheafification}$ holds for $J$ and $F$.
CategoryTheory.Sheaf.composeAndSheafifydefMathlib.CategoryTheory.Sites.PreservesSheafification, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $A$ and $B$. Then $\operatorname{composeAndSheafify}$ applied to $J$ and $F$ is a functor of the set of sheaves of $J$ and $A$ and the set of sheaves of $J$ and $B$ defined as the composition of the sheaf to presheaf of $J$ and $A$ and the composition of the action of the right whiskering of $A$ and $B$ and $F$ and the presheaf to sheaf of $J$ and $B$.
CategoryTheory.presheafToSheafCompComposeAndSheafifyIsodefMathlib.CategoryTheory.Sites.PreservesSheafification, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $A$ and $B$. Then $\operatorname{presheafToSheafCompComposeAndSheafifyIso}$ applied to $J$ and $F$ is an isomorphism of the composition of the presheaf to sheaf of $J$ and $A$ and $\operatorname{composeAndSheafify}$ applied to $J$ and $F$ and the composition of the action of the right whiskering of $A$ and $B$ and $F$ and the presheaf to sheaf of $J$ and $B$ defined as the inverse of $\operatorname{asIso}$ applied to $\operatorname{toPresheafToSheafCompComposeAndSheafify}$ applied to $J$ and $F$.
CategoryTheory.sheafComposeNatIsodefMathlib.CategoryTheory.Sites.PreservesSheafification, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $A$ and $B$. Let $x_{4}$ be an adjunction of $x_{3}$ and the sheaf to presheaf of $J$ and $A$. Let $x_{6}$ be an adjunction of $x_{5}$ and the sheaf to presheaf of $J$ and $B$. Then $\operatorname{sheafComposeNatIso}$ applied to $J$, $F$, $x_{4}$ and $x_{6}$ is an isomorphism of the composition of the action of the right whiskering of $A$ and $B$ and $F$ and $x_{5}$ and the composition of $x_{3}$ and $\operatorname{sheafCompose}$ applied to $J$ and $F$ defined as $\operatorname{asIso}$ applied to $\operatorname{sheafComposeNatTrans}$ applied to $J$, $F$, $x_{4}$ and $x_{6}$.
CategoryTheory.sheafComposeNatTransdefMathlib.CategoryTheory.Sites.PreservesSheafification, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $A$ and $B$. Let $x_{4}$ be an adjunction of $x_{3}$ and the sheaf to presheaf of $J$ and $A$. Let $x_{6}$ be an adjunction of $x_{5}$ and the sheaf to presheaf of $J$ and $B$. Then $\operatorname{sheafComposeNatTrans}$ applied to $J$, $F$, $x_{4}$ and $x_{6}$ is a homomorphism of the composition of the action of the right whiskering of $A$ and $B$ and $F$ and $x_{5}$ and the composition of $x_{3}$ and $\operatorname{sheafCompose}$ applied to $J$ and $F$.
CategoryTheory.sheafifyComposeIsodefMathlib.CategoryTheory.Sites.PreservesSheafification, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $A$ and $B$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{sheafifyComposeIso}$ applied to $J$, $F$ and $P$ is an isomorphism of the sheafification of $J$ and the composition of $P$ and $F$ and the composition of the sheafification of $J$ and $P$ and $F$ defined as the map isomorphism of the sheaf to presheaf of $J$ and $B$ and the application of $\operatorname{sheafComposeNatIso}$ applied to $J$, $F$, the sheafification adjunction of $J$ and $A$ and the sheafification adjunction of $J$ and $B$ and $P$.
CategoryTheory.toPresheafToSheafCompComposeAndSheafifydefMathlib.CategoryTheory.Sites.PreservesSheafification, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $A$ and $B$. Then $\operatorname{toPresheafToSheafCompComposeAndSheafify}$ applied to $J$ and $F$ is a homomorphism of the composition of the action of the right whiskering of $A$ and $B$ and $F$ and the presheaf to sheaf of $J$ and $B$ and the composition of the presheaf to sheaf of $J$ and $A$ and $\operatorname{composeAndSheafify}$ applied to $J$ and $F$ defined as the right whisker of the unit of the sheafification adjunction of $J$ and $A$ and the composition of the action of the right whiskering of $A$ and $B$ and $F$ and the presheaf to sheaf of $J$ and $B$.
CategoryTheory.GrothendieckTopology.toPretopologydefMathlib.CategoryTheory.Sites.Pretopology, function or constantWording
the pretopology of J (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Then the pretopology of $J$ is a pretopology of $C$.
CategoryTheory.Precoverage.toPretopologydefMathlib.CategoryTheory.Sites.Pretopology, function or constantWording
the pretopology of C and J (from the name)
English
Let $C$ be a set. Let $J$ be a precoverage of $C$. Then the pretopology of $C$ and $J$ is a pretopology of $C$.
CategoryTheory.PretopologystructureMathlib.CategoryTheory.Sites.Pretopology, typeWording
pretopology of C (from the name)
English
Let $C$ be a set. Then the pretopologies of $C$ are a basic type.
CategoryTheory.Pretopology.gidefMathlib.CategoryTheory.Sites.Pretopology, function or constantEnglish
Let $C$ be a set. Then $\operatorname{gi}$ applied to $C$ is a Galois insertion of $\operatorname{toGrothendieck}$ and $\operatorname{toPretopology}$.
CategoryTheory.Pretopology.toGrothendieckdefMathlib.CategoryTheory.Sites.Pretopology, function or constantEnglish
Let $K$ be a pretopology of $C$. Then $\operatorname{toGrothendieck}$ applied to $K$ is a Grothendieck topology of $C$.
CategoryTheory.Pretopology.trivialdefMathlib.CategoryTheory.Sites.Pretopology, function or constantEnglish
Let $C$ be a set. Then $\operatorname{trivial}$ applied to $C$ is a pretopology of $C$.
CategoryTheory.GrothendieckTopology.pseudofunctorOverdefMathlib.CategoryTheory.Sites.PseudofunctorSheafOver, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then $\operatorname{pseudofunctorOver}$ applied to $J$ and $A$ is a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories.
CategoryTheory.Functor.sheafAdjunctionContinuousdefMathlib.CategoryTheory.Sites.Pullback, function or constantEnglish
Let $G$ be a functor of $C$ and $D$. Let $A$ be a set. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Then $\operatorname{sheafAdjunctionContinuous}$ applied to $G$, $A$, $J$ and $K$ is an adjunction of the sheaf pullback of $J$ and $K$ and $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$ defined as the adjunction of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$.
CategoryTheory.Functor.sheafPullbackdefMathlib.CategoryTheory.Sites.Pullback, function or constantWording
the sheaf pullback of J and K (from the name)
English
Let $G$ be a functor of $C$ and $D$. Let $A$ be a set. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Then the sheaf pullback of $J$ and $K$ is a functor of the set of sheaves of $J$ and $A$ and the set of sheaves of $K$ and $A$ defined as the left adjoint of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$.
CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuousdefMathlib.CategoryTheory.Sites.Pullback, function or constantEnglish
generation took over the time limit
CategoryTheory.Functor.sheafPullbackConstruction.sheafPullbackdefMathlib.CategoryTheory.Sites.Pullback, function or constantWording
the sheaf pullback of J and K (from the name)
English
Let $G$ be a functor of $C$ and $D$. Let $A$ be a set. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Then the sheaf pullback of $J$ and $K$ is a functor of the set of sheaves of $J$ and $A$ and the set of sheaves of $K$ and $A$ defined as the composition of the sheaf to presheaf of $J$ and $A$ and the composition of $\operatorname{lan}$ applied to the opposite of $G$ and the presheaf to sheaf of $K$ and $A$.
CategoryTheory.Functor.sheafPullbackConstruction.sheafPullbackIsodefMathlib.CategoryTheory.Sites.Pullback, function or constantWording
the sheaf pullback isomorphism of J and K (from the name)
English
Let $G$ be a functor of $C$ and $D$. Let $A$ be a set. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Then the sheaf pullback isomorphism of $J$ and $K$ is an isomorphism of the sheaf pullback of $J$ and $K$ and the sheaf pullback of $J$ and $K$ defined as $\operatorname{leftAdjointUniq}$ applied to $\operatorname{sheafAdjunctionContinuous}$ applied to $G$, $A$, $J$ and $K$ and $\operatorname{sheafAdjunctionContinuous}$ applied to $G$, $A$, $J$ and $K$.
CategoryTheory.Presheaf.IsSeparateddefMathlib.CategoryTheory.Sites.Sheaf, predicateWording
P is separated with respect to J (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then $P$ is separated with respect to $J$, if for all elements $X$ of $C$, for all sieves $S$ of $X$, if $\MembershipmemMACRoT {J (X)}{S}$, then for all types $x_{4}$ and $y$ of the action of $P$ and $\operatorname{op}$ applied to $X$, if for all elements $Y$ of $C$, for all homomorphisms $f$ of $Y$ and $X$, if $\operatorname{arrows}$ holds for $S$, then $\operatorname{hom}$ applied to the map of $P$ and the opposite in $f$ and $x_{4}$ is equal to $\operatorname{hom}$ applied to the map of $P$ and the opposite in $f$ and $y$, then $\EqtMACRoH {x_{4}}{y}$.
CategoryTheory.Presheaf.IsSheafdefMathlib.CategoryTheory.Sites.Sheaf, predicateEnglish
Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{IsSheaf}$ holds for $J$ and $P$, if for all elements $E$ of $A$, $J$ is a sheaf.
CategoryTheory.Presheaf.IsSheaf'defMathlib.CategoryTheory.Sites.Sheaf, predicateEnglish
Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{IsSheaf'}$ holds for $J$ and $P$, if for all elements $U$ of $C$, for all presieves $R$ of $U$, if $\MembershipmemMACRoT {J (U)}{\operatorname{generate} (R)}$, then $\mathrm{Nonempty}$ holds for $\operatorname{IsLimit}$ applied to the inclusion of the fork map of $R$ and $P$ and $\operatorname{w}$ applied to $R$ and $P$.
CategoryTheory.Presheaf.IsSheaf.amalgamatedefMathlib.CategoryTheory.Sites.Sheaf, function or constantEnglish
Assume that $\operatorname{IsSheaf}$ holds for $J$ and $P$. Let $S$ be a cover of $J$ and $X$. Let $x_{2}$ be a function from elements $I$ of $\operatorname{Arrow}$ applied to $S$ to homomorphisms of $E$ and the action of $P$ and $\operatorname{op}$ applied to $\operatorname{Y}$ applied to $I$ such that for all elements $x_{3}$ and $x_{4}$ of $\operatorname{Arrow}$ applied to $S$, for all relations $r$ of $x_{3}$ and $x_{4}$, the composition of $x_{2}$ applied to $x_{3}$ and the map of $P$ and the opposite in $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2081\_}$ applied to $r$ is equal to the composition of $x_{2}$ applied to $x_{4}$ and the map of $P$ and the opposite in $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2082\_}$ applied to $r$. Then $\operatorname{amalgamate}$ applied to $\mathrm{hP}$, $S$, $I$, $x_{2}$ and $\mathrm{hx}$ is a homomorphism of $E$ and the action of $P$ and $\operatorname{op}$ applied to $X$.
CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrowsdefMathlib.CategoryTheory.Sites.Sheaf, function or constantEnglish
Assume that $\operatorname{IsSheaf}$ holds for $J$ and $P$. Let $f$ be a function from elements $i_{2}$ of $I$ to homomorphisms of $X$ applied to $i_{2}$ and $S$ such that the sieve of $X$ and $f$ is an element of $J$ applied to $S$. Let $x_{2}$ be a function from elements $i_{1}$ of $I$ to homomorphisms of $E$ and the action of $P$ and $\operatorname{op}$ applied to $X$ applied to $i_{1}$ such that for all elements $W$ of $C$, for all elements $i$ and $j$ of $I$, for all homomorphisms $a$ of $W$ and $X$ applied to $i$, for all homomorphisms $b$ of $W$ and $X$ applied to $j$, if the composition of $a$ and $f$ applied to $i$ is equal to the composition of $b$ and $f$ applied to $j$, then the composition of $x_{2}$ applied to $i$ and the map of $P$ and the opposite in $a$ is equal to the composition of $x_{2}$ applied to $j$ and the map of $P$ and the opposite in $b$. Then $\operatorname{amalgamateOfArrows}$ applied to $\mathrm{hP}$, $i_{2}$, $f$, $\mathrm{hf}$, $i_{1}$, $x_{2}$ and $\mathrm{hx}$ is a homomorphism of $E$ and the action of $P$ and $\operatorname{op}$ applied to $S$ defined as the function that maps $x_{2}$ and $\mathrm{hx}$ to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Presheaf\_\_IsSheaf\_\_existsUnique\_amalgamation\_ofArrows}$ applied to $\mathrm{hP}$, $i_{2}$, $f$, $\mathrm{hf}$ and $i_{1}$, $x_{2}$ and $\mathrm{hx}$.
CategoryTheory.Presheaf.IsSheaf.isLimitMultiforkdefMathlib.CategoryTheory.Sites.Sheaf, function or constantEnglish
Assume that $\operatorname{IsSheaf}$ holds for $J$ and $P$. Let $S$ be a cover of $J$ and $X$. Then $\operatorname{isLimitMultifork}$ applied to $\mathrm{hP}$ and $S$ is an element of $\operatorname{IsLimit}$ applied to the multifork of $S$ and $P$.
CategoryTheory.Presheaf.conesEquivSieveCompatibleFamilydefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the cone equivalence sieve compatible family of S and E (from the name)
English
Let $P$ be a functor of the set of opposites of $C$ and $A$. Let $S$ be a sieve of $X$. Let $E$ be an opposite of $A$. Then the cone equivalence sieve compatible family of $S$ and $E$ is an equivalence from the action of the cone of the composition of the opposite of the diagram of the arrow of $S$ and $P$ and $E$ to $\SubtypeSet {x_{2}}{\operatorname{SieveCompatible} (x_{2})}$.
CategoryTheory.Presheaf.firstMapdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the map of R and P (from the docstring)
English
Let $R$ be a presieve of $U$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the map of $R$ and $P$ is a homomorphism of the first object of $R$ and $P$ and the second object of $R$ and $P$ defined as the lift of the function that maps $x_{2}$ to the composition of the projection of the function that maps $f$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{fst}$ applied to $f$ and $\ProdfstMACRoZ {x_{2}}$ and the map of $P$ and the opposite in the first projection of the pullback of $\operatorname{snd}$ applied to $\ProdfstMACRoZ {x_{2}}$ and $\operatorname{snd}$ applied to $\ProdsndMACRoAA {x_{2}}$.
CategoryTheory.Presheaf.firstObjdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the first object of R and P (from the name)
English
Let $R$ be a presieve of $U$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the first object of $R$ and $P$ is an element of $A$ defined as the product object of the function that maps $f$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{fst}$ applied to $f$.
CategoryTheory.Presheaf.forkMapdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the fork map of R and P (from the name)
English
Let $R$ be a presieve of $U$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the fork map of $R$ and $P$ is a homomorphism of the action of $P$ and $\operatorname{op}$ applied to $U$ and the first object of $R$ and $P$ defined as the lift of the function that maps $f$ to the map of $P$ and the opposite in $\operatorname{snd}$ applied to $f$.
CategoryTheory.Presheaf.homEquivAmalgamationdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the homomorphism equivalence amalgamation of hx (from the name)
English
Assume that $\operatorname{SieveCompatible}$ holds for $x_{2}$. Then the homomorphism equivalence amalgamation of $\mathrm{hx}$ is an equivalence from the set of homomorphisms of the cone of $\mathrm{hx}$ and the map cone of $P$ and the opposite of the cocone of the arrow of $S$ to $\SubtypeSet {t}{\operatorname{IsAmalgamation} (x_{2} , t)}$.
CategoryTheory.Presheaf.isLimitOfIsSheafdefMathlib.CategoryTheory.Sites.Sheaf, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Let $S$ be a cover of $J$ and $X$. Assume that $\operatorname{IsSheaf}$ holds for $J$ and $P$. Then $\operatorname{isLimitOfIsSheaf}$ applied to $J$, $P$, $S$ and $\mathrm{hP}$ is an element of $\operatorname{IsLimit}$ applied to the multifork of $S$ and $P$.
CategoryTheory.Presheaf.isSheafForIsSheafFor'defMathlib.CategoryTheory.Sites.Sheaf, function or constantEnglish
Let $P$ be a functor of the set of opposites of $C$ and $A$. Let $s$ be a functor of $A$ and the set of sets. Let $U$ be an element of $C$. Let $R$ be a presieve of $U$. Then $\operatorname{isSheafForIsSheafFor'}$ applied to $P$, $s$, $U$ and $R$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $s$ and the inclusion of the fork map of $R$ and $P$ and $\operatorname{w}$ applied to $R$ and $P$ to $\operatorname{IsLimit}$ applied to the inclusion of the fork map of the composition of $P$ and $s$ and $R$ and $\operatorname{w}$ applied to the composition of $P$ and $s$ and $R$.
CategoryTheory.Presheaf.secondMapdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the map of R and P (from the docstring)
English
Let $R$ be a presieve of $U$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the map of $R$ and $P$ is a homomorphism of the first object of $R$ and $P$ and the second object of $R$ and $P$ defined as the lift of the function that maps $x_{2}$ to the composition of the projection of the function that maps $f$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{fst}$ applied to $f$ and $\ProdsndMACRoAA {x_{2}}$ and the map of $P$ and the opposite in the second projection of the pullback of $\operatorname{snd}$ applied to $\ProdfstMACRoZ {x_{2}}$ and $\operatorname{snd}$ applied to $\ProdsndMACRoAA {x_{2}}$.
CategoryTheory.Presheaf.secondObjdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the second object of R and P (from the name)
English
Let $R$ be a presieve of $U$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the second object of $R$ and $P$ is an element of $A$ defined as the product object of the function that maps $\mathrm{fg}$ to the action of $P$ and $\operatorname{op}$ applied to the pullback of $\operatorname{snd}$ applied to $\ProdfstMACRoZ {\mathrm{fg}}$ and $\operatorname{snd}$ applied to $\ProdsndMACRoAA {\mathrm{fg}}$.
CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.conedefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the cone of hx (from the name)
English
Assume that $\operatorname{SieveCompatible}$ holds for $x_{2}$. Then the cone of $\mathrm{hx}$ is a cone of the composition of the opposite of the diagram of the arrow of $S$ and $P$ defined as $\operatorname{mk}$ applied to the opposite of $E$ and the inverse function of the cone equivalence sieve compatible family of $S$ and $E$ and $x_{2}$.
CategoryTheory.SheafdefMathlib.CategoryTheory.Sites.Sheaf, typeWording
sheaf of J and A (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then a sheaf of $J$ and $A$ is an element of the function that maps $J$ and $A$ to the set of full subcategories of $\operatorname{IsSheaf}$ applied to $J$.
CategoryTheory.Sheaf.homEquivdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the homomorphism equivalence (from the name)
English
generation took over the time limit
CategoryTheory.Sheaf.isTerminalOfBotCoverdefMathlib.CategoryTheory.Sites.Sheaf, function or constantEnglish
Let $F$ be a sheaf of $J$ and $A$. Let $X$ be an element of $C$ such that the bottom is an element of $J$ applied to $X$. Then $\operatorname{isTerminalOfBotCover}$ applied to $F$, $X$ and $H$ is an element of $\operatorname{IsTerminal}$ applied to the action of the object of $F$ and $\operatorname{op}$ applied to $X$ defined as $\operatorname{ofUnique}$ applied to the action of the object of $F$ and $\operatorname{op}$ applied to $X$.
CategoryTheory.Sheaf.isTerminalOfEqTopdefMathlib.CategoryTheory.Sites.Sheaf, function or constantEnglish
Assume that $J$ is equal to the top. Let $F$ be a sheaf of $J$ and $A$. Then $\operatorname{isTerminalOfEqTop}$ applied to $H$ and $F$ is an element of $\operatorname{IsTerminal}$ applied to $F$.
CategoryTheory.Sheaf.isTerminalTerminaldefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the constant sheaf of J and hX (from the docstring)
English
Let $J$ be a Grothendieck topology of $C$. Let $\mathrm{hX}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then the constant sheaf of $J$ and $\mathrm{hX}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{terminal}$ applied to $J$ and $\mathrm{hX}$.
CategoryTheory.fullyFaithfulSheafToPresheafdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the fully faithful sheaf to presheaf of J and A (from the name)
English
generation took over the time limit
CategoryTheory.sheafBotEquivalencedefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the sheaf bottom equivalence of A (from the name)
English
Let $A$ be a set. Then the sheaf bottom equivalence of $A$ is an equivalence of the set of sheaves of the bottom and $A$ and the set of functors of the set of opposites of $C$ and $A$.
CategoryTheory.sheafOverdefMathlib.CategoryTheory.Sites.Sheaf, function or constantEnglish
Let $x_{2}$ be a sheaf of $J$ and $A$. Let $E$ be an element of $A$. Then $\operatorname{sheafOver}$ applied to $x_{2}$ and $E$ is a sheaf of $J$ and the set of sets.
CategoryTheory.sheafSectionsdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the sheaf section of J and A (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the sheaf section of $J$ and $A$ is a functor of the set of opposites of $C$ and the set of functors of the set of sheaves of $J$ and $A$ and $A$ defined as the flip of the sheaf to presheaf of $J$ and $A$.
CategoryTheory.sheafSectionsNatIsoEvaluationdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the sheaf section natural isomorphism evaluation of J and A (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the sheaf section natural isomorphism evaluation of $J$ and $A$ is an isomorphism of the action of the sheaf section of $J$ and $A$ and $\operatorname{op}$ applied to $X$ and the composition of the sheaf to presheaf of $J$ and $A$ and the action of the evaluation of the set of opposites of $C$ and $A$ and $\operatorname{op}$ applied to $X$ defined as the identity of the action of the sheaf section of $J$ and $A$ and $\operatorname{op}$ applied to $X$.
CategoryTheory.sheafToPresheafdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the sheaf to presheaf of J and A (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the sheaf to presheaf of $J$ and $A$ is a functor of the set of sheaves of $J$ and $A$ and the set of functors of the set of opposites of $C$ and $A$ defined as the inclusion of $\operatorname{IsSheaf}$ applied to $J$.
CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheafdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the sheaf to presheaf composition Coyoneda composition whiskering left sheaf to presheaf (from the name)
English
generation took over the time limit
CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheafdefMathlib.CategoryTheory.Sites.Sheaf, function or constantWording
the sheaf to presheaf composition Yoneda composition whiskering left sheaf to presheaf (from the name)
English
generation took over the time limit
CategoryTheory.Sheaf.HdefMathlib.CategoryTheory.Sites.SheafCohomology.Basic, typeEnglish
Let $F$ be a sheaf of $J$ and the set of additive commutative group categories. Let $n$ be a natural number. Then an element of $\operatorname{H}$ applied to $F$ and $n$ is an element of the function that maps $F$ and $n$ to the set of extensions of $F$ and $n$.
CategoryTheory.Sheaf.H'defMathlib.CategoryTheory.Sites.SheafCohomology.Basic, function or constantEnglish
Let $F$ be a sheaf of $J$ and the set of additive commutative group categories. Let $n$ be a natural number. Let $X$ be an element of $C$. Then $\operatorname{H'}$ applied to $F$, $n$ and $X$ is an additive commutative group category defined as the action of the cohomology presheaf of $F$ and $n$ and $\operatorname{op}$ applied to $X$.
CategoryTheory.Sheaf.H.equiv₀defMathlib.CategoryTheory.Sites.SheafCohomology.Basic, function or constantWording
the equivalence of F and hT (from the name)
English
Let $F$ be a sheaf of $J$ and the set of additive commutative group categories. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then the equivalence of $F$ and $\mathrm{hT}$ is an additive equivalence of $\operatorname{H}$ applied to $F$ and $0$ and the set of carriers of the action of the object of $F$ and $\operatorname{op}$ applied to $T$ defined as the composition of the additive bijection and the composition of the homomorphism additive equivalence of $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Integer$ and $F$ and the additive equivalence of the action of the action of the sheaf section of $J$ and the set of additive commutative group categories and $\operatorname{op}$ applied to $T$ and $F$.
CategoryTheory.Sheaf.H.mapdefMathlib.CategoryTheory.Sites.SheafCohomology.Basic, function or constantWording
the map of f and n (from the name)
English
Let $f$ be a homomorphism of $F$ and $G$. Let $n$ be a natural number. Then the map of $f$ and $n$ is an additive monoid homomorphism of $\operatorname{H}$ applied to $F$ and $n$ and $\operatorname{H}$ applied to $G$ and $n$.
CategoryTheory.Sheaf.cohomologyPresheafdefMathlib.CategoryTheory.Sites.SheafCohomology.Basic, function or constantWording
the cohomology presheaf of F and n (from the name)
English
Let $F$ be a sheaf of $J$ and the set of additive commutative group categories. Let $n$ be a natural number. Then the cohomology presheaf of $F$ and $n$ is a functor of the set of opposites of $C$ and the set of additive commutative group categories defined as the action of the cohomology presheaf functor of $J$ and $n$ and $F$.
CategoryTheory.Sheaf.cohomologyPresheafFunctordefMathlib.CategoryTheory.Sites.SheafCohomology.Basic, function or constantWording
the cohomology presheaf functor of J and n (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $n$ be a natural number. Then the cohomology presheaf functor of $J$ and $n$ is a functor of the set of sheaves of $J$ and the set of additive commutative group categories and the set of functors of the set of opposites of $C$ and the set of additive commutative group categories defined as the flip of the composition of the opposite of the composition of the Yoneda and the composition of the action of the right whiskering of the set of sets and the set of additive commutative group categories and the free functor and the presheaf to sheaf of $J$ and the set of additive commutative group categories and the functor of $n$.
CategoryTheory.Sheaf.functorHdefMathlib.CategoryTheory.Sites.SheafCohomology.Basic, function or constantWording
the functor of J and n (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $n$ be a natural number. Then the functor of $J$ and $n$ is a functor of the set of sheaves of $J$ and the set of additive commutative group categories and the set of additive commutative group categories.
CategoryTheory.cechComplexFunctordefMathlib.CategoryTheory.Sites.SheafCohomology.Cech, function or constantWording
the Cech complex functor of U (from the name)
English
Let $U$ be a function from elements of $x_{3}$ to elements of $C$. Then the Cech complex functor of $U$ is a functor of the set of functors of the set of opposites of $C$ and $A$ and the set of cochain complexes of $A$ and $\Natural$ defined as the cochain complex functor of the Cech of $\operatorname{mk}$ applied to $x_{3}$ and $U$.
CategoryTheory.Sheaf.H.longSequencedefMathlib.CategoryTheory.Sites.SheafCohomology.ExactSequences, function or constantWording
the long sequence of x1 and x2 (from the name)
English
Assume that $\operatorname{ShortExact}$ holds for $S$. Let $x_{1}$ and $x_{2}$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{1} + 1 , x_{2})$ and $\mathrm{CategoryTheory\_\_Sheaf\_\_H\_\_longSequence\_\_\_auto\_1}$. Then the long sequence of $x_{1}$ and $x_{2}$ is a composable arrow of the set of additive commutative group categories and $5$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2085\_}$ applied to the additive commutative group category of the map of $\operatorname{f}$ applied to $S$ and $x_{1}$, the additive commutative group category of the map of $\operatorname{g}$ applied to $S$ and $x_{1}$, the additive commutative group category of $\mathrm{CategoryTheory\_\_Sheaf\_\_H\_\_\_u3b4\_}$ applied to $\mathrm{hS}$, $x_{1}$, $x_{2}$ and $h_{2}$, the additive commutative group category of the map of $\operatorname{f}$ applied to $S$ and $x_{2}$ and the additive commutative group category of the map of $\operatorname{g}$ applied to $S$ and $x_{2}$.
CategoryTheory.Sheaf.H.longSequenceFunctordefMathlib.CategoryTheory.Sites.SheafCohomology.ExactSequences, function or constantWording
the long sequence functor of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be natural numbers such that $x_{1} + 1 = x_{2}$. Then the long sequence functor of $x_{1}$ and $x_{2}$ is a functor of the set of short exact sequences of the set of sheaves of $J$ and the set of additive commutative group categories and the set of composable arrows of the set of additive commutative group categories and $5$.
CategoryTheory.Sheaf.H.longSequenceHomdefMathlib.CategoryTheory.Sites.SheafCohomology.ExactSequences, function or constantWording
the long sequence homomorphism of x2 and f (from the name)
English
Let $x_{1}$ and $x_{2}$ be natural numbers. Assume that $\operatorname{ShortExact}$ holds for $x_{3}$. Assume that $\operatorname{ShortExact}$ holds for $x_{4}$. Let $f$ be a homomorphism of $x_{3}$ and $x_{4}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{1} + 1 , x_{2})$ and $\mathrm{CategoryTheory\_\_Sheaf\_\_H\_\_longSequenceHom\_\_\_auto\_1}$. Then the long sequence homomorphism of $x_{2}$ and $f$ is a homomorphism of the long sequence of $x_{1}$ and $x_{2}$ and the long sequence of $x_{1}$ and $x_{2}$.
CategoryTheory.Sheaf.H.δdefMathlib.CategoryTheory.Sites.SheafCohomology.ExactSequences, function or constantEnglish
Assume that $\operatorname{ShortExact}$ holds for $S$. Let $x_{1}$ and $x_{2}$ be natural numbers such that $x_{1} + 1 = x_{2}$. Then $\mathrm{CategoryTheory\_\_Sheaf\_\_H\_\_\_u3b4\_}$ applied to $\mathrm{hS}$, $x_{1}$, $x_{2}$ and $h_{2}$ is an additive monoid homomorphism of $\operatorname{H}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and $x_{1}$ and $\operatorname{H}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $x_{2}$ defined as the postcomposition of the class in $\mathrm{hS}$ and the action of the constant sheaf of $J$ and the set of additive commutative group categories and $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Integer$.
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiproddefMathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris, function or constantEnglish
Let $S$ be an element of $\operatorname{MayerVietorisSquare}$ applied to $J$. Let $F$ be a sheaf of $J$ and the set of additive commutative group categories. Let $n$ be a natural number. Then $\operatorname{fromBiprod}$ applied to $S$, $F$ and $n$ is a homomorphism of the biproduct of $\operatorname{H'}$ applied to $F$, $n$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_}$ applied to $\operatorname{toSquare}$ applied to $S$ and $\operatorname{H'}$ applied to $F$, $n$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_}$ applied to $\operatorname{toSquare}$ applied to $S$ and $\operatorname{H'}$ applied to $F$, $n$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2081\_}$ applied to $\operatorname{toSquare}$ applied to $S$ defined as $\operatorname{desc}$ applied to the map of the cohomology presheaf of $F$ and $n$ and the opposite in $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $\operatorname{toSquare}$ applied to $S$ and $\operatorname{neg}$ applied to the map of the cohomology presheaf of $F$ and $n$ and the opposite in $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $\operatorname{toSquare}$ applied to $S$.
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequencedefMathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris, function or constantWording
the sequence of x1 and x2 (from the name)
English
Let $S$ be an element of $\operatorname{MayerVietorisSquare}$ applied to $J$. Let $F$ be a sheaf of $J$ and the set of additive commutative group categories. Let $x_{1}$ and $x_{2}$ be natural numbers such that $x_{1} + 1 = x_{2}$. Then the sequence of $x_{1}$ and $x_{2}$ is a composable arrow of the set of additive commutative group categories and $5$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2085\_}$ applied to the biproduct of $F$ and $x_{1}$, $\operatorname{fromBiprod}$ applied to $S$, $F$ and $x_{1}$, $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_MayerVietorisSquare\_\_\_u3b4\_}$ applied to $S$, $F$, $x_{1}$, $x_{2}$ and $h_{3}$, the biproduct of $F$ and $x_{2}$ and $\operatorname{fromBiprod}$ applied to $S$, $F$ and $x_{2}$.
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequenceIsodefMathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris, function or constantWording
the sequence isomorphism of x1 and x2 (from the name)
English
Let $S$ be an element of $\operatorname{MayerVietorisSquare}$ applied to $J$. Let $F$ be a sheaf of $J$ and the set of additive commutative group categories. Let $x_{1}$ and $x_{2}$ be natural numbers such that $x_{1} + 1 = x_{2}$. Then the sequence isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of the sequence of $x_{1}$ and $x_{2}$ and the contravariant sequence of $x_{1}$ and $x_{2}$.
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiproddefMathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris, function or constantWording
the biproduct of F and n (from the name)
English
Let $S$ be an element of $\operatorname{MayerVietorisSquare}$ applied to $J$. Let $F$ be a sheaf of $J$ and the set of additive commutative group categories. Let $n$ be a natural number. Then the biproduct of $F$ and $n$ is a homomorphism of $\operatorname{H'}$ applied to $F$, $n$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $\operatorname{toSquare}$ applied to $S$ and the biproduct of $\operatorname{H'}$ applied to $F$, $n$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_}$ applied to $\operatorname{toSquare}$ applied to $S$ and $\operatorname{H'}$ applied to $F$, $n$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_}$ applied to $\operatorname{toSquare}$ applied to $S$ defined as the lift of the map of the cohomology presheaf of $F$ and $n$ and the opposite in $\mathrm{CategoryTheory\_\_Square\_\_f\_u2082\_\_u2084\_}$ applied to $\operatorname{toSquare}$ applied to $S$ and the map of the cohomology presheaf of $F$ and $n$ and the opposite in $\mathrm{CategoryTheory\_\_Square\_\_f\_u2083\_\_u2084\_}$ applied to $\operatorname{toSquare}$ applied to $S$.
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δdefMathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris, function or constantEnglish
Let $S$ be an element of $\operatorname{MayerVietorisSquare}$ applied to $J$. Let $F$ be a sheaf of $J$ and the set of additive commutative group categories. Let $x_{1}$ and $x_{2}$ be natural numbers such that $x_{1} + 1 = x_{2}$. Then $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_MayerVietorisSquare\_\_\_u3b4\_}$ applied to $S$, $F$, $x_{1}$, $x_{2}$ and $h_{3}$ is a homomorphism of $\operatorname{H'}$ applied to $F$, $x_{1}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2081\_}$ applied to $\operatorname{toSquare}$ applied to $S$ and $\operatorname{H'}$ applied to $F$, $x_{2}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $\operatorname{toSquare}$ applied to $S$.
CategoryTheory.presheafHomdefMathlib.CategoryTheory.Sites.SheafHom, function or constantWording
the presheaf homomorphism of F and G (from the name)
English
Let $F$ and $G$ be functors of the set of opposites of $C$ and $A$. Then the presheaf homomorphism of $F$ and $G$ is a functor of the set of opposites of $C$ and the set of sets.
CategoryTheory.presheafHomSectionsEquivdefMathlib.CategoryTheory.Sites.SheafHom, function or constantWording
the presheaf homomorphism section equivalence of F and G (from the name)
English
Let $F$ and $G$ be functors of the set of opposites of $C$ and $A$. Then the presheaf homomorphism section equivalence of $F$ and $G$ is an equivalence from the set of elements of the section of the presheaf homomorphism of $F$ and $G$ to the set of homomorphisms of $F$ and $G$.
CategoryTheory.sheafHomdefMathlib.CategoryTheory.Sites.SheafHom, function or constantWording
the sheaf homomorphism of F and G (from the name)
English
Let $F$ and $G$ be sheaves of $J$ and $A$. Then the sheaf homomorphism of $F$ and $G$ is a sheaf of $J$ and the set of sets.
CategoryTheory.sheafHom'defMathlib.CategoryTheory.Sites.SheafHom, function or constantWording
the sheaf homomorphism of F and G (from the name)
English
Let $F$ and $G$ be sheaves of $J$ and $A$. Then the sheaf homomorphism of $F$ and $G$ is a functor of the set of opposites of $C$ and the set of sets.
CategoryTheory.sheafHom'IsodefMathlib.CategoryTheory.Sites.SheafHom, function or constantWording
the canonical isomorphism of F and G (from the docstring)
English
Let $F$ and $G$ be sheaves of $J$ and $A$. Then the canonical isomorphism of $F$ and $G$ is an isomorphism of the sheaf homomorphism of $F$ and $G$ and the presheaf homomorphism of the object of $F$ and the object of $G$.
CategoryTheory.sheafHomSectionsEquivdefMathlib.CategoryTheory.Sites.SheafHom, function or constantWording
the sheaf homomorphism section equivalence of F and G (from the name)
English
Let $F$ and $G$ be sheaves of $J$ and $A$. Then the sheaf homomorphism section equivalence of $F$ and $G$ is an equivalence from the set of elements of the section of the object of the sheaf homomorphism of $F$ and $G$ to the set of homomorphisms of $F$ and $G$ defined as the composition of the equivalence of the map isomorphism of the section functor of the set of opposites of $C$ and the canonical isomorphism of $F$ and $G$ and the composition of the presheaf homomorphism section equivalence of the object of $F$ and the object of $G$ and the inverse of the homomorphism equivalence.
CategoryTheory.Presieve.IsSeparateddefMathlib.CategoryTheory.Sites.SheafOfTypes, predicateWording
J is separated (from the docstring)
English
Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then $J$ is separated, if for all elements $X$ of $C$, for all sieves $S$ of $X$, if $\MembershipmemMACRoT {J (X)}{S}$, then $P$ is separated.
CategoryTheory.Presieve.IsSheafdefMathlib.CategoryTheory.Sites.SheafOfTypes, predicateWording
J is a sheaf (from the docstring)
English
Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then $J$ is a sheaf, if for all elements $X$ of $C$, for all sieves $S$ of $X$, if $\MembershipmemMACRoT {J (X)}{S}$, then $\operatorname{IsSheafFor}$ holds for $P$ and the arrow of $S$.
CategoryTheory.Presieve.compatibleYonedaFamily_toCoconedefMathlib.CategoryTheory.Sites.SheafOfTypes, function or constantWording
the compatible Yoneda family to cocone of W and x1 (from the name)
English
Let $R$ be a presieve of $X$. Let $W$ be an element of $C$. Let $x_{1}$ be a compatible family of element of the action of the Yoneda and $W$ and $R$. Then the compatible Yoneda family to cocone of $W$ and $x_{1}$ is a cocone of the diagram of $R$.
CategoryTheory.Presieve.yonedaFamilyOfElements_fromCoconedefMathlib.CategoryTheory.Sites.SheafOfTypes, function or constantWording
the Yoneda family of R and s (from the name)
English
Let $R$ be a presieve of $X$. Let $s$ be a cocone of the diagram of $R$. Then the Yoneda family of $R$ and $s$ is a family of element of the action of the Yoneda and $\operatorname{pt}$ applied to $s$ and $R$ defined as the function that maps $x_{1}$, $f$ and $\mathrm{hf}$ to the component of the inclusion of $s$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $f$ and $\mathrm{hf}$.
CategoryTheory.HasSheafifyclassMathlib.CategoryTheory.Sites.Sheafification, predicateWording
J has sheafifications (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then we can say that $J$ has sheafifications.
CategoryTheory.HasWeakSheafifydefMathlib.CategoryTheory.Sites.Sheafification, predicateWording
J has weak sheafifications (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then $J$ has weak sheafifications, if the sheaf to presheaf of $J$ and $A$ is a right adjoint.
CategoryTheory.isoSheafifydefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the isomorphism sheafification of J and hP (from the name)
English
Let $J$ be a Grothendieck topology of $C$ such that $\operatorname{IsSheaf}$ holds for $J$ and $P$. Then the isomorphism sheafification of $J$ and $\mathrm{hP}$ is an isomorphism of $P$ and the sheafification of $J$ and $P$ defined as $\operatorname{asIso}$ applied to the sheafification of $J$ and $P$.
CategoryTheory.presheafToSheafdefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the presheaf to sheaf of J and A (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the presheaf to sheaf of $J$ and $A$ is a functor of the set of functors of the set of opposites of $C$ and $A$ and the set of sheaves of $J$ and $A$ defined as the left adjoint of the sheaf to presheaf of $J$ and $A$.
CategoryTheory.sheafificationdefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the sheafification of J and D (from the docstring)
English
Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Then the sheafification of $J$ and $D$ is a functor of the set of functors of the set of opposites of $C$ and $D$ and the set of functors of the set of opposites of $C$ and $D$ defined as the composition of the presheaf to sheaf of $J$ and $D$ and the sheaf to presheaf of $J$ and $D$.
CategoryTheory.sheafificationAdjunctiondefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the sheafification adjunction of J and A (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the sheafification adjunction of $J$ and $A$ is an adjunction of the presheaf to sheaf of $J$ and $A$ and the sheaf to presheaf of $J$ and $A$ defined as the adjunction of the sheaf to presheaf of $J$ and $A$.
CategoryTheory.sheafificationIsodefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the sheafification isomorphism of P (from the name)
English
Let $P$ be a sheaf of $J$ and $D$. Then the sheafification isomorphism of $P$ is an isomorphism of $P$ and the action of the presheaf to sheaf of $J$ and $D$ and the object of $P$.
CategoryTheory.sheafificationNatIsodefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the natural isomorphism of J and D (from the docstring)
English
Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Then the natural isomorphism of $J$ and $D$ is an isomorphism of the identity of the set of sheaves of $J$ and $D$ and the composition of the sheaf to presheaf of $J$ and $D$ and the presheaf to sheaf of $J$ and $D$.
CategoryTheory.sheafifydefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the sheafification of J and P (from the docstring)
English
Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Then the sheafification of $J$ and $P$ is a functor of the set of opposites of $C$ and $D$ defined as the object of the action of the presheaf to sheaf of $J$ and $D$ and $P$.
CategoryTheory.sheafifyLiftdefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the sheafification lift of J and x2 (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $x_{2}$ be a homomorphism of $P$ and $Q$. Assume that $\operatorname{IsSheaf}$ holds for $J$ and $Q$. Then the sheafification lift of $J$ and $x_{2}$ is a homomorphism of the sheafification of $J$ and $P$ and $Q$ defined as the homomorphism of $\operatorname{symm}$ applied to the homomorphism equivalence of $P$ and $\operatorname{mk}$ applied to $Q$ and $\mathrm{hQ}$ and $x_{2}$.
CategoryTheory.sheafifyMapdefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the sheafification map of J and x2 (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $x_{2}$ be a homomorphism of $P$ and $Q$. Then the sheafification map of $J$ and $x_{2}$ is a homomorphism of the sheafification of $J$ and $P$ and the sheafification of $J$ and $Q$ defined as the homomorphism of the map of the presheaf to sheaf of $J$ and $D$ and $x_{2}$.
CategoryTheory.toSheafificationdefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the sheafification of J and D (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Then the sheafification of $J$ and $D$ is a homomorphism of the identity of the set of functors of the set of opposites of $C$ and $D$ and the sheafification of $J$ and $D$ defined as the unit of the sheafification adjunction of $J$ and $D$.
CategoryTheory.toSheafifydefMathlib.CategoryTheory.Sites.Sheafification, function or constantWording
the sheafification of J and P (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Then the sheafification of $J$ and $P$ is a homomorphism of $P$ and the sheafification of $J$ and $P$ defined as the component of the unit of the sheafification adjunction of $J$ and $D$ and $P$.
CategoryTheory.SievestructureMathlib.CategoryTheory.Sites.Sieves.Basic, typeWording
sieve of X (from the name)
English
Let $X$ be an element of $C$. Then the sieves of $X$ are a basic type.
CategoryTheory.Sieve.BindStructdefMathlib.CategoryTheory.Sites.Sieves.Basic, typeEnglish
Let $S$ be a presieve of $X$. Let $R$ be a function from elements $Y$ of $C$ and homomorphisms $f$ of $Y$ and $X$ and elements of $\mathrm{Proof}$ applied to $S$ applied to $Y$ and $f$ to sieves of $Y$. Let $h$ be a homomorphism of $Z$ and $X$. Then an element of $\operatorname{BindStruct}$ applied to $S$, $Y$, $f$, $R$ and $h$ is an element of the function that maps $S$, $R$, $h$, $R$ and $h$ to $\operatorname{BindStruct}$ applied to $S$, the function that maps $x_{1}$, $x_{2}$ and $\mathrm{hf}$ to the arrow of $Y$ applied to $x_{1}$, $x_{2}$ and $\mathrm{hf}$, $f$, $R$ and $h$.
CategoryTheory.Sieve.arrowsdefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the arrow of self (from the name)
English
Let $\mathrm{self}$ be a sieve of $X$. Then the arrow of $\mathrm{self}$ is a presieve of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Sieve.binddefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantEnglish
Let $S$ be a presieve of $X$. Let $R$ be a function from elements $Y$ of $C$ and homomorphisms $f$ of $Y$ and $X$ and elements of $\mathrm{Proof}$ applied to $S$ applied to $Y$ and $f$ to sieves of $Y$. Then $\operatorname{bind}$ applied to $S$, $Y$, $f$ and $R$ is a sieve of $X$.
CategoryTheory.Sieve.galoisCoinsertionOfMonodefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the Galois coinsertion of f (from the name)
English
Let $f$ be a homomorphism of $Y$ and $X$. Then the Galois coinsertion of $f$ is a Galois coinsertion of $\operatorname{pushforward}$ applied to $f$ and $\operatorname{pullback}$ applied to $f$.
CategoryTheory.Sieve.galoisInsertionOfIsSplitEpidefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the Galois insertion of f (from the name)
English
Let $f$ be a homomorphism of $Y$ and $X$. Then the Galois insertion of $f$ is a Galois insertion of $\operatorname{pushforward}$ applied to $f$ and $\operatorname{pullback}$ applied to $f$.
CategoryTheory.Sieve.generatedefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantEnglish
Let $R$ be a presieve of $X$. Then $\operatorname{generate}$ applied to $R$ is a sieve of $X$.
CategoryTheory.Sieve.giGeneratedefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantEnglish
$\operatorname{giGenerate}$ is a Galois insertion of $\operatorname{generate}$ and $\operatorname{arrows}$.
CategoryTheory.Sieve.infdefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the infimum of x1 (from the docstring)
English
Let $x_{1}$ be an element of the power set of the set of sieves of $X$. Then the infimum of $x_{1}$ is a sieve of $X$.
CategoryTheory.Sieve.interdefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the intersection of S and R (from the name)
English
Let $S$ and $R$ be sieves of $X$. Then the intersection of $S$ and $R$ is a sieve of $X$.
CategoryTheory.Sieve.ofArrowsdefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the sieve of Y and f (from the name)
English
Let $Y$ be a function from elements of $I$ to elements of $C$. Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $Y$ applied to $i$ and $X$. Then the sieve of $Y$ and $i$ is a sieve of $X$ defined as the function that maps $f$ to $\operatorname{generate}$ applied to the presieve of $Y$ and $i$ and $f$.
CategoryTheory.Sieve.ofArrows.hdefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantEnglish
Assume that $\operatorname{arrows}$ holds for the sieve of $Y$ and $f$. Then $\operatorname{h}$ applied to $\mathrm{hg}$ is a homomorphism of $W$ and $Y$ applied to $\operatorname{i}$ applied to $\mathrm{hg}$.
CategoryTheory.Sieve.ofArrows.idefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantEnglish
Assume that $\operatorname{arrows}$ holds for the sieve of $Y$ and $f$. Then $\operatorname{i}$ applied to $\mathrm{hg}$ is an element of $I$ defined as $\operatorname{choose}$ applied to $\operatorname{exists}$ applied to $\mathrm{hg}$.
CategoryTheory.Sieve.ofObjectsdefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the sieve of Y and X (from the name)
English
Let $Y$ be a function from elements of $I$ to elements of $C$. Let $X$ be an element of $C$. Then the sieve of $Y$ and $X$ is a sieve of $X$.
CategoryTheory.Sieve.ofTwoArrowsdefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the sieve of i and j (from the name)
English
Let $i$ be a homomorphism of $U$ and $X$. Let $j$ be a homomorphism of $V$ and $X$. Then the sieve of $i$ and $j$ is a sieve of $X$.
CategoryTheory.Sieve.pullbackdefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the pullback of h and S (from the name)
English
Let $h$ be a homomorphism of $Y$ and $X$. Let $S$ be a sieve of $X$. Then the pullback of $h$ and $S$ is a sieve of $Y$.
CategoryTheory.Sieve.pushforwarddefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantEnglish
Let $f$ be a homomorphism of $Y$ and $X$. Let $R$ be a sieve of $Y$. Then $\operatorname{pushforward}$ applied to $f$ and $R$ is a sieve of $X$.
CategoryTheory.Sieve.supdefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the supremum of x1 (from the docstring)
English
Let $x_{1}$ be an element of the power set of the set of sieves of $X$. Then the supremum of $x_{1}$ is a sieve of $X$.
CategoryTheory.Sieve.uniondefMathlib.CategoryTheory.Sites.Sieves.Basic, function or constantWording
the union of S and R (from the name)
English
Let $S$ and $R$ be sieves of $X$. Then the union of $S$ and $R$ is a sieve of $X$.
CategoryTheory.Presieve.FunctorPushforwardStructure.liftdefMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantWording
the lift of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{FunctorPushforwardStructure}$ applied to $F$, $S$ and $f$. Then the lift of $\mathrm{self}$ is a homomorphism of $Y$ and the action of $F$ and $\operatorname{preobj}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
CategoryTheory.Presieve.FunctorPushforwardStructure.premapdefMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{FunctorPushforwardStructure}$ applied to $F$, $S$ and $f$. Then $\operatorname{premap}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{preobj}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
CategoryTheory.Presieve.FunctorPushforwardStructure.preobjdefMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{FunctorPushforwardStructure}$ applied to $F$, $S$ and $f$. Then $\operatorname{preobj}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Presieve.functorPullbackdefMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantWording
the functor pullback of F and R (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $R$ be a presieve of the action of $F$ and $X$. Then the functor pullback of $F$ and $R$ is a presieve of $X$ defined as the function that maps $x_{2}$ and $f$ to $R$ applied to the action of $F$ and $x_{2}$ and the map of $F$ and $f$.
CategoryTheory.Presieve.functorPushforwarddefMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantEnglish
Let $F$ be a functor of $C$ and $D$. Let $S$ be a presieve of $X$. Then there is a presieve of the action of $F$ and $X$. Proof. Let $F$ be arbitrary. Let $S$ be arbitrary. Let $Y$ be arbitrary. Let $f$ be arbitrary. By C. Let $Z$ be arbitrary. By Z. By X. By Quiver__Hom. Let $g$ be arbitrary. By Y. By F. By Z. By CategoryTheory__Functor__obj. By Quiver__Hom. Let $h$ be arbitrary. By Z. By g. By S. By f. By h. By F. By g. By CategoryTheory__Functor__map. By CategoryTheory__CategoryStruct__comp. By Eqt. By and. By exists. By exists. By exists.
CategoryTheory.Presieve.getFunctorPushforwardStructuredefMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantEnglish
Assume that $\operatorname{functorPushforward}$ holds for $F$, $S$, $Y$ and $f$. Then $\operatorname{getFunctorPushforwardStructure}$ applied to $h$ is an element of $\operatorname{FunctorPushforwardStructure}$ applied to $F$, $S$ and $f$.
CategoryTheory.Presieve.mapinductiveMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantWording
the map of F and s (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $s$ be a presieve of $X$. Then the map of $F$ and $s$ is a presieve of the action of $F$ and $X$.
CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertiondefMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantWording
the essential surjection full functor Galois insertion of F and X (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the essential surjection full functor Galois insertion of $F$ and $X$ is a Galois insertion of $\operatorname{functorPushforward}$ applied to $F$ and $\operatorname{functorPullback}$ applied to $F$.
CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertiondefMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantWording
the fully faithful functor Galois coinsertion of F and X (from the name)
English
generation took over the time limit
CategoryTheory.Sieve.functorPullbackdefMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantWording
the functor pullback of F and R (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $R$ be a sieve of the action of $F$ and $X$. Then the functor pullback of $F$ and $R$ is a sieve of $X$.
CategoryTheory.Sieve.functorPushforwarddefMathlib.CategoryTheory.Sites.Sieves.Functoriality, function or constantEnglish
Let $F$ be a functor of $C$ and $D$. Let $R$ be a sieve of $X$. Then $\operatorname{functorPushforward}$ applied to $F$ and $R$ is a sieve of the action of $F$ and $X$.
CategoryTheory.Sieve.functordefMathlib.CategoryTheory.Sites.Sieves.Presheaf, function or constantWording
the functor of S (from the name)
English
Let $S$ be a sieve of $X$. Then the functor of $S$ is a functor of the set of opposites of $C$ and the set of sets.
CategoryTheory.Sieve.functorInclusiondefMathlib.CategoryTheory.Sites.Sieves.Presheaf, function or constantWording
the functor inclusion of S (from the name)
English
Let $S$ be a sieve of $X$. Then the functor inclusion of $S$ is a homomorphism of the functor of $S$ and the action of the Yoneda and $X$.
CategoryTheory.Sieve.natTransOfLedefMathlib.CategoryTheory.Sites.Sieves.Presheaf, function or constantWording
the natural transformation of h (from the name)
English
Assume that $S \leq T$. Then the natural transformation of $h$ is a homomorphism of the functor of $S$ and the functor of $T$.
CategoryTheory.Sieve.sieveOfSubfunctordefMathlib.CategoryTheory.Sites.Sieves.Presheaf, function or constantWording
the sieve of f (from the name)
English
Let $f$ be a homomorphism of $R$ and the action of the Yoneda and $X$. Then the sieve of $f$ is a sieve of $X$.
CategoryTheory.Sieve.sieveOfUliftSubfunctordefMathlib.CategoryTheory.Sites.Sieves.Presheaf, function or constantWording
the sieve of f (from the name)
English
Let $f$ be a homomorphism of $R$ and the action of the lift Yoneda and $X$. Then the sieve of $f$ is a sieve of $X$.
CategoryTheory.Sieve.toFunctordefMathlib.CategoryTheory.Sites.Sieves.Presheaf, function or constantWording
the functor of S and f (from the name)
English
Let $S$ be a sieve of $X$. Let $f$ be a homomorphism of $Y$ and $X$. Assume that $\operatorname{arrows}$ holds for $S$. Then the functor of $S$ and $f$ is a homomorphism of the action of the Yoneda and $Y$ and the functor of $S$.
CategoryTheory.Sieve.toUliftFunctordefMathlib.CategoryTheory.Sites.Sieves.Presheaf, function or constantWording
the lift functor of S and f (from the name)
English
Let $S$ be a sieve of $X$. Let $f$ be a homomorphism of $Y$ and $X$. Assume that $\operatorname{arrows}$ holds for $S$. Then the lift functor of $S$ and $f$ is a homomorphism of the action of the lift Yoneda and $Y$ and the lift functor of $S$.
CategoryTheory.Sieve.uliftFunctordefMathlib.CategoryTheory.Sites.Sieves.Presheaf, function or constantWording
the lift functor of S (from the name)
English
Let $S$ be a sieve of $X$. Then the lift functor of $S$ is a functor of the set of opposites of $C$ and the set of sets defined as the composition of the functor of $S$ and the functor embedding.
CategoryTheory.Sieve.uliftFunctorInclusiondefMathlib.CategoryTheory.Sites.Sieves.Presheaf, function or constantWording
the lift functor inclusion of S (from the name)
English
Let $S$ be a sieve of $X$. Then the lift functor inclusion of $S$ is a homomorphism of the lift functor of $S$ and the action of the lift Yoneda and $X$ defined as the right whisker of the functor inclusion of $S$ and the functor embedding.
CategoryTheory.Sieve.uliftNatTransOfLedefMathlib.CategoryTheory.Sites.Sieves.Presheaf, function or constantWording
the lift natural transformation of h (from the name)
English
Assume that $S \leq T$. Then the lift natural transformation of $h$ is a homomorphism of the lift functor of $S$ and the lift functor of $T$.
CategoryTheory.PresievedefMathlib.CategoryTheory.Sites.Sieves.Presieve, typeWording
presieve of X (from the name)
English
Let $X$ be an element of $C$. Then a presieve of $X$ is an element of the function that maps $X$ to the set of functions from elements $Y$ of $C$ and homomorphisms of $Y$ and $X$ to propositions.
CategoryTheory.Presieve.BindStructstructureMathlib.CategoryTheory.Sites.Sieves.Presieve, typeEnglish
Let $S$ be a presieve of $X$. Let $R$ be a function from elements $Y$ of $C$ and homomorphisms $f$ of $Y$ and $X$ and elements of $\mathrm{Proof}$ applied to $S$ applied to $Y$ and $f$ to presieves of $Y$. Let $h$ be a homomorphism of $Z$ and $X$. Then the elements of $\operatorname{BindStruct}$ applied to $S$, $Y$, $f$, $R$ and $h$ are a basic type.
CategoryTheory.Presieve.BindStruct.YdefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{BindStruct}$ applied to $S$, $R$ and $h$. Then $\operatorname{Y}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Presieve.BindStruct.fdefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{BindStruct}$ applied to $S$, $R$ and $h$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{Y}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
CategoryTheory.Presieve.BindStruct.gdefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{BindStruct}$ applied to $S$, $R$ and $h$. Then $\operatorname{g}$ applied to $\mathrm{self}$ is a homomorphism of $Z$ and $\operatorname{Y}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
CategoryTheory.Presieve.HasPairwisePullbacksclassMathlib.CategoryTheory.Sites.Sieves.Presieve, predicateWording
R has pairwise pullbacks (from the name)
English
Let $R$ be a presieve of $X$. Then we can say that $R$ has pairwise pullbacks.
CategoryTheory.Presieve.HasPullbacksclassMathlib.CategoryTheory.Sites.Sieves.Presieve, predicateEnglish
Let $R$ be a presieve of $X$. Let $f$ be a homomorphism of $Y$ and $X$. Then we can say that $\operatorname{HasPullbacks}$ holds for $R$ and $f$.
CategoryTheory.Presieve.binddefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantEnglish
Let $S$ be a presieve of $X$. Let $R$ be a function from elements $Y$ of $C$ and homomorphisms $f$ of $Y$ and $X$ and elements of $\mathrm{Proof}$ applied to $S$ applied to $Y$ and $f$ to presieves of $Y$. Then there is a presieve of $X$. Proof. Let $S$ be arbitrary. Let $R$ be arbitrary. Let $Z$ be arbitrary. Let $h$ be arbitrary. By C. Let $Y$ be arbitrary. By f. By Y. By Quiver__Hom. Let $g$ be arbitrary. By Y. By X. By Quiver__Hom. Let $f$ be arbitrary. By Y. By f. By S. Let $H$ be arbitrary. By Y. By f. By H. By f. By g. By Y. By g. By f. By CategoryTheory__CategoryStruct__comp. By R. By Eqt. By and. By exists. By exists. By exists. By exists.
CategoryTheory.Presieve.bind.bindStructdefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantEnglish
Assume that $\operatorname{bind}$ holds for $S$, $R$, $Z$ and $h$. Then $\operatorname{bindStruct}$ applied to $H$ is an element of $\operatorname{BindStruct}$ applied to $S$, $R$ and $h$.
CategoryTheory.Presieve.bindOfArrowsinductiveMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantEnglish
Let $Y$ be a function from elements of $x_{1}$ to elements of $C$. Let $f$ be a function from elements $i_{1}$ of $x_{1}$ to homomorphisms of $Y$ applied to $i_{1}$ and $X$. Let $R$ be a function from elements $i$ of $x_{1}$ to presieves of $Y$ applied to $i$. Then there is a presieve of $X$.
CategoryTheory.Presieve.categorydefMathlib.CategoryTheory.Sites.Sieves.Presieve, typeWording
category of P (from the name)
English
Let $P$ be a presieve of $X$. Then a category of $P$ is an element of the function that maps $P$ to the set of full subcategories of the function that maps $f$ to $P$ applied to the left of $f$ and the homomorphism of $f$.
CategoryTheory.Presieve.categoryMkdefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantWording
the category of P and f (from the name)
English
Let $P$ be a presieve of $X$. Let $f$ be a homomorphism of $Y$ and $X$ such that $P$ holds for $Y$ and $f$. Then the category of $P$ and $f$ is a category of $P$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $f$ and $\mathrm{hf}$.
CategoryTheory.Presieve.coconedefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantWording
the cocone of S (from the name)
English
Let $S$ be a presieve of $X$. Then the cocone of $S$ is a cocone of the diagram of $S$ defined as the whisker of the inclusion of the function that maps $f$ to $S$ applied to the left of $f$ and the homomorphism of $f$ and the natural cocone over the forgetful functor of $X$.
CategoryTheory.Presieve.diagramdefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantWording
the diagram of S (from the name)
English
Let $S$ be a presieve of $X$. Then the diagram of $S$ is a functor of the set of categories of $S$ and $C$ defined as the composition of the inclusion of the function that maps $f$ to $S$ applied to the left of $f$ and the homomorphism of $f$ and $\operatorname{forget}$ applied to $X$.
CategoryTheory.Presieve.ofArrowsinductiveMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantWording
the presieve of Y and f (from the name)
English
Let $Y$ be a function from elements of $x_{1}$ to elements of $C$. Let $f$ be a function from elements $i$ of $x_{1}$ to homomorphisms of $Y$ applied to $i$ and $X$. Then the presieve of $Y$ and $i$ is a presieve of $X$.
CategoryTheory.Presieve.ofArrows.idxdefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantWording
the index of hf (from the name)
English
Assume that $\operatorname{ofArrows}$ holds for $X$ and $f$. Then the index of $\mathrm{hf}$ is an element of $x_{1}$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Presieve\_\_ofArrows\_surj}$ applied to $f$, $g$ and $\mathrm{hf}$.
CategoryTheory.Presieve.pullbackdefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantWording
the pullback of f and R (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $R$ be a presieve of $Y$. Then the pullback of $f$ and $R$ is a presieve of $X$ defined as the function that maps $x_{1}$ and $g$ to $R$ applied to $x_{1}$ and the composition of $g$ and $f$.
CategoryTheory.Presieve.pullbackArrowsinductiveMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantWording
the pullback arrow of f and R (from the name)
English
Let $f$ be a homomorphism of $Y$ and $X$. Let $R$ be a presieve of $X$. Then the pullback arrow of $f$ and $R$ is a presieve of $Y$.
CategoryTheory.Presieve.pushforwarddefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantEnglish
Let $f$ be a homomorphism of $X$ and $Y$. Let $R$ be a presieve of $X$. Then there is a presieve of $Y$. Proof. Let $f$ be arbitrary. Let $R$ be arbitrary. Let $Z$ be arbitrary. Let $\mathrm{fg}$ be arbitrary. By Z. By X. By Quiver__Hom. Let $g$ be arbitrary. By g. By f. By CategoryTheory__CategoryStruct__comp. By fg. By Eqt. By Z. By g. By R. By and. By exists.
CategoryTheory.Presieve.singletoninductiveMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantWording
the singleton presieve of f (from the docstring)
English
Let $f$ be a homomorphism of $Y$ and $X$. Then the singleton presieve of $f$ is a presieve of $X$.
CategoryTheory.Presieve.uncurrydefMathlib.CategoryTheory.Sites.Sieves.Presieve, function or constantEnglish
Let $s$ be a presieve of $X$. Then $\operatorname{uncurry}$ applied to $s$ is an element of the power set of $\Sigma$ applied to the function that maps $Y$ to the set of homomorphisms of $Y$ and $X$ defined as $\operatorname{ofPred}$ applied to the function that maps $u$ to $s$ applied to $\operatorname{fst}$ applied to $u$ and $\operatorname{snd}$ applied to $u$.
CategoryTheory.Sieve.shrinkFunctordefMathlib.CategoryTheory.Sites.Sieves.Shrink, function or constantWording
the shrink functor of S (from the name)
English
Let $S$ be a sieve of $X$. Then the shrink functor of $S$ is a subfunctor of the action of the Yoneda embedding and $X$.
CategoryTheory.Sieve.shrinkFunctorIsoFunctordefMathlib.CategoryTheory.Sites.Sieves.Shrink, function or constantWording
the shrink functor isomorphism functor of S (from the name)
English
Let $S$ be a sieve of $X$. Then the shrink functor isomorphism functor of $S$ is an isomorphism of the subfunctor as a functor of the shrink functor of $S$ and the functor of $S$.
CategoryTheory.Sieve.shrinkFunctorUliftFunctorIsodefMathlib.CategoryTheory.Sites.Sieves.Shrink, function or constantWording
the shrink functor lift functor isomorphism of S (from the name)
English
Let $S$ be a sieve of $X$. Then the shrink functor lift functor isomorphism of $S$ is an isomorphism of the composition of the subfunctor as a functor of the shrink functor of $S$ and the functor embedding and the subfunctor as a functor of the shrink functor of $S$.
Opens.grothendieckTopologydefMathlib.CategoryTheory.Sites.Spaces, function or constantWording
the Grothendieck topology of T (from the name)
English
Let $T$ be a set. Then the Grothendieck topology of $T$ is a Grothendieck topology of the set of opens of $T$.
Opens.pretopologydefMathlib.CategoryTheory.Sites.Spaces, function or constantWording
the pretopology of T (from the name)
English
Let $T$ be a set. Then the pretopology of $T$ is a pretopology of the set of opens of $T$.
CategoryTheory.GrothendieckTopology.isColimitCofanMkYonedadefMathlib.CategoryTheory.Sites.Subcanonical, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $X$ be a function from elements of $x_{1}$ to elements of $C$ such that the sieve of $X$ and $\operatorname{inj}$ applied to $c$ is an element of $J$ applied to $\operatorname{pt}$ applied to $c$. Assume that for all elements $Y_{1}$ of $C$, for all elements $x_{2}$ of $\operatorname{IsInitial}$ applied to $Y_{1}$, the bottom is an element of $J$ applied to $Y_{1}$. Assume that for all elements $i_{1}$ and $j$ of $x_{1}$, if $i_{1} \neq j$, then for all elements $Y$ of $C$, for all homomorphisms $a$ of $Y$ and $X$ applied to $i_{1}$, for all homomorphisms $b$ of $Y$ and $X$ applied to $j$, if the composition of $a$ and the injection of $c$ and $i_{1}$ is equal to the composition of $b$ and the injection of $c$ and $j$, then $\mathrm{Nonempty}$ holds for $\operatorname{IsInitial}$ applied to $Y$. Then $\operatorname{isColimitCofanMkYoneda}$ applied to $J$, $X$, $H$, $\mathrm{hempty}$ and $\mathrm{hdisj}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the action of the Yoneda of $J$ and $\operatorname{pt}$ applied to $c$ and the function that maps $i$ to the map of the Yoneda of $J$ and the injection of $c$ and $i$.
CategoryTheory.GrothendieckTopology.uliftYonedaEquivdefMathlib.CategoryTheory.Sites.Subcanonical, function or constantWording
the lift Yoneda equivalence of J (from the name)
English
generation took over the time limit
CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyonedadefMathlib.CategoryTheory.Sites.Subcanonical, function or constantWording
the lift Yoneda opposite composition Coyoneda of J (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Then the lift Yoneda opposite composition Coyoneda of $J$ is an isomorphism of the composition of the opposite of the lift Yoneda of $J$ and the Coyoneda and the composition of the evaluation of the set of opposites of $C$ and the set of sets and the composition of the action of the right whiskering of the set of sets and the set of sets and the functor embedding and the action of the left whiskering of the set of functors of the set of opposites of $C$ and the set of sets and the set of sets and the sheaf to presheaf of $J$ and the set of sets defined as the composition of the composition of the left isomorphism whisker of the composition of the opposite of the Yoneda of $J$ and the opposite of $\operatorname{sheafCompose}$ applied to $J$ and the functor embedding and the inverse of the sheaf to presheaf composition Coyoneda composition whiskering left sheaf to presheaf and the right isomorphism whisker of the opposite of the inverse of the lift Yoneda composition sheaf to presheaf of $J$ and the composition of the Coyoneda and the action of the left whiskering of the set of functors of the set of opposites of $C$ and the set of sets and the set of sets and the sheaf to presheaf of $J$ and the set of sets and the right isomorphism whisker of the lift Yoneda opposite composition Coyoneda and the action of the left whiskering of the set of functors of the set of opposites of $C$ and the set of sets and the set of sets and the sheaf to presheaf of $J$ and the set of sets.
CategoryTheory.GrothendieckTopology.yonedaEquivdefMathlib.CategoryTheory.Sites.Subcanonical, function or constantWording
the Yoneda equivalence of J (from the name)
English
generation took over the time limit
CategoryTheory.GrothendieckTopology.yonedaOpCompCoyonedadefMathlib.CategoryTheory.Sites.Subcanonical, function or constantWording
the Yoneda opposite composition Coyoneda of J (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Then the Yoneda opposite composition Coyoneda of $J$ is an isomorphism of the composition of the opposite of the Yoneda of $J$ and the Coyoneda and the composition of the evaluation of the set of opposites of $C$ and the set of sets and the composition of the action of the right whiskering of the set of sets and the set of sets and the functor embedding and the action of the left whiskering of the set of functors of the set of opposites of $C$ and the set of sets and the set of sets and the sheaf to presheaf of $J$ and the set of sets defined as the composition of the composition of the left isomorphism whisker of the opposite of the Yoneda of $J$ and the inverse of the sheaf to presheaf composition Coyoneda composition whiskering left sheaf to presheaf and the right isomorphism whisker of the opposite of the inverse of the Yoneda composition sheaf to presheaf of $J$ and the composition of the Coyoneda and the action of the left whiskering of the set of functors of the set of opposites of $C$ and the set of sets and the set of sets and the sheaf to presheaf of $J$ and the set of sets and the right isomorphism whisker of the curried version of the Yoneda lemma and the action of the left whiskering of the set of functors of the set of opposites of $C$ and the set of sets and the set of sets and the sheaf to presheaf of $J$ and the set of sets.
CategoryTheory.Sheaf.imagedefMathlib.CategoryTheory.Sites.Subsheaf, function or constantWording
the image sheaf of f (from the docstring)
English
Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the image sheaf of $f$ is a sheaf of $J$ and the set of sets.
CategoryTheory.Sheaf.imageιdefMathlib.CategoryTheory.Sites.Subsheaf, function or constantWording
the inclusion of the image sheaf to the target of f (from the docstring)
English
Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the inclusion of the image sheaf to the target of $f$ is a homomorphism of the image sheaf of $f$ and $\mathrm{F'}$ defined as $\operatorname{mk}$ applied to the inclusion of the sheafification of $J$ and the range of the homomorphism of $f$.
CategoryTheory.Sheaf.toImagedefMathlib.CategoryTheory.Sites.Subsheaf, function or constantWording
the image of f (from the name)
English
Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the image of $f$ is a homomorphism of $F$ and the image sheaf of $f$ defined as $\operatorname{mk}$ applied to the range sheafification of $J$ and the homomorphism of $f$.
CategoryTheory.Subfunctor.sheafifydefMathlib.CategoryTheory.Sites.Subsheaf, function or constantWording
the sheafification of J and G (from the docstring)
English
Let $J$ be a Grothendieck topology of $C$. Let $G$ be a subfunctor of $F$. Then the sheafification of $J$ and $G$ is a subfunctor of $F$.
CategoryTheory.Subfunctor.sheafifyLiftdefMathlib.CategoryTheory.Sites.Subsheaf, function or constantWording
the sheafification lift of G and f (from the name)
English
Let $G$ be a subfunctor of $F$. Let $f$ be a homomorphism of the subfunctor as a functor of $G$ and $\mathrm{F'}$. Assume that $J$ is a sheaf. Then the sheafification lift of $G$ and $f$ is a homomorphism of the subfunctor as a functor of the sheafification of $J$ and $G$ and $\mathrm{F'}$.
CategoryTheory.Subfunctor.toRangeSheafifydefMathlib.CategoryTheory.Sites.Subsheaf, function or constantWording
the range sheafification of J and f (from the name)
English
Let $J$ be a Grothendieck topology of $C$. Let $f$ be a homomorphism of $\mathrm{F'}$ and $F$. Then the range sheafification of $J$ and $f$ is a homomorphism of $\mathrm{F'}$ and the subfunctor as a functor of the sheafification of $J$ and the range of $f$.
CategoryTheory.imageFactorizationdefMathlib.CategoryTheory.Sites.Subsheaf, function or constantWording
the image factorization of f (from the name)
English
Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the image factorization of $f$ is an image factorisation of $f$.
CategoryTheory.imageMonoFactorizationdefMathlib.CategoryTheory.Sites.Subsheaf, function or constantWording
the image monomorphism factorization of f (from the name)
English
Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the image monomorphism factorization of $f$ is a monomorphism factorisation of $f$.
CategoryTheory.discretePresievedefMathlib.CategoryTheory.Sites.Types, function or constantWording
the discrete presieve of x (from the name)
English
Let $x$ be a set. Then the discrete presieve of $x$ is a presieve of $x$ defined as the function that maps $x_{1}$ and $x_{2}$ to the proposition that there exists an element $x_{3}$ of $x_{1}$, such that for all elements $y$ of $x_{1}$, $\EqtMACRoH {y}{x_{3}}$.
CategoryTheory.discreteSievedefMathlib.CategoryTheory.Sites.Types, function or constantWording
the discrete sieve of x (from the name)
English
Let $x$ be a set. Then the discrete sieve of $x$ is a sieve of $x$.
CategoryTheory.equivYonedadefMathlib.CategoryTheory.Sites.Types, function or constantWording
the equivalence Yoneda of S and hs (from the name)
English
Let $S$ be a functor of the set of opposites of the set of sets and the set of sets such that $\operatorname{IsSheaf}$ holds for the type Grothendieck topology and $S$. Then the equivalence Yoneda of $S$ and $\mathrm{hs}$ is an isomorphism of $S$ and the action of the Yoneda and the action of $S$ and $\operatorname{op}$ applied to $\mathrm{PUnit}$.
CategoryTheory.equivYoneda'defMathlib.CategoryTheory.Sites.Types, function or constantWording
the equivalence Yoneda of S (from the name)
English
Let $S$ be a sheaf of the type Grothendieck topology and the set of sets. Then the equivalence Yoneda of $S$ is an isomorphism of $S$ and the action of the Yoneda and the action of the object of $S$ and $\operatorname{op}$ applied to $\mathrm{PUnit}$.
CategoryTheory.evaldefMathlib.CategoryTheory.Sites.Types, function or constantWording
the evaluation of P and s (from the name)
English
Let $P$ be a functor of the set of opposites of the set of sets and the set of sets. Let $x$ be a set. Let $s$ be an element of the action of $P$ and $\operatorname{op}$ applied to $x$. Then the evaluation of $P$ and $s$ is a homomorphism of $x$ and the action of $P$ and $\operatorname{op}$ applied to $\mathrm{PUnit}$ defined as the type category of the function that maps $x_{1}$ to $\operatorname{hom}$ applied to the map of $P$ and the opposite in the type category of the function that maps $x_{2}$ to $x_{1}$ and $s$.
CategoryTheory.evalEquivdefMathlib.CategoryTheory.Sites.Types, function or constantWording
the evaluation equivalence of S (from the name)
English
Let $S$ be a functor of the set of opposites of the set of sets and the set of sets such that $\operatorname{IsSheaf}$ holds for the type Grothendieck topology and $S$. Let $x$ be a set. Then the evaluation equivalence of $S$ is an equivalence from the action of $S$ and $\operatorname{op}$ applied to $x$ to the set of homomorphisms of $x$ and the action of $S$ and $\operatorname{op}$ applied to $\mathrm{PUnit}$.
CategoryTheory.typeEquivdefMathlib.CategoryTheory.Sites.Types, function or constantWording
the type equivalence (from the name)
English
The type equivalence is an equivalence of the set of sets and the set of sheaves of the type Grothendieck topology and the set of sets.
CategoryTheory.typesGluedefMathlib.CategoryTheory.Sites.Types, function or constantWording
the type glue of S and f (from the name)
English
Let $S$ be a functor of the set of opposites of the set of sets and the set of sets. Assume that the type Grothendieck topology is a sheaf. Let $x$ be a set. Let $f$ be a function from elements of $x$ to elements of the action of $S$ and $\operatorname{op}$ applied to $\mathrm{PUnit}$. Then the type glue of $S$ and $f$ is an element of the action of $S$ and $\operatorname{op}$ applied to $x$.
CategoryTheory.typesGrothendieckTopologydefMathlib.CategoryTheory.Sites.Types, function or constantWording
the type Grothendieck topology (from the name)
English
The type Grothendieck topology is a Grothendieck topology of the set of sets.
CategoryTheory.yoneda'defMathlib.CategoryTheory.Sites.Types, function or constantWording
the Yoneda (from the name)
English
The Yoneda is a functor of the set of sets and the set of sheaves of the type Grothendieck topology and the set of sets.
CategoryTheory.GrothendieckTopology.Cover.mapMultiforkdefMathlib.CategoryTheory.Sites.Whiskering, function or constantWording
the map multifork of P and S (from the name)
English
Let $F$ be a functor of $A$ and $B$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Let $S$ be a cover of $J$ and $X$. Then the map multifork of $P$ and $S$ is an isomorphism of the map cone of $F$ and the multifork of $S$ and $P$ and the action of the postcomposition of the homomorphism of the multicospan composition of $P$ and $S$ and the multifork of $S$ and the composition of $P$ and $F$.
CategoryTheory.GrothendieckTopology.Cover.multicospanCompdefMathlib.CategoryTheory.Sites.Whiskering, function or constantWording
the multicospan composition of P and S (from the name)
English
Let $F$ be a functor of $A$ and $B$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Let $S$ be a cover of $J$ and $X$. Then the multicospan composition of $P$ and $S$ is an isomorphism of the multicospan of the index of $S$ and the composition of $P$ and $F$ and the composition of the multicospan of the index of $S$ and $P$ and $F$.
CategoryTheory.GrothendieckTopology.HasSheafComposeclassMathlib.CategoryTheory.Sites.Whiskering, predicateEnglish
Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $A$ and $B$. Then we can say that $\operatorname{HasSheafCompose}$ holds for $J$ and $F$.
CategoryTheory.fullyFaithfulSheafComposedefMathlib.CategoryTheory.Sites.Whiskering, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then $\operatorname{fullyFaithfulSheafCompose}$ applied to $J$ and $\mathrm{hF}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{sheafCompose}$ applied to $J$ and $F$ defined as $\operatorname{ofCompFaithful}$ applied to $\operatorname{fullyFaithfulSheafComposeCompSheafToPresheaf}$ applied to $J$ and $\mathrm{hF}$.
CategoryTheory.fullyFaithfulSheafComposeCompSheafToPresheafdefMathlib.CategoryTheory.Sites.Whiskering, function or constantEnglish
generation took over the time limit
CategoryTheory.sheafComposedefMathlib.CategoryTheory.Sites.Whiskering, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $A$ and $B$. Then $\operatorname{sheafCompose}$ applied to $J$ and $F$ is a functor of the set of sheaves of $J$ and $A$ and the set of sheaves of $J$ and $B$.
CategoryTheory.sheafCompose_mapdefMathlib.CategoryTheory.Sites.Whiskering, function or constantEnglish
Let $J$ be a Grothendieck topology of $C$. Let $x_{3}$ be a homomorphism of $F$ and $G$. Then $\mathrm{CategoryTheory\_\_sheafCompose\_map}$ applied to $J$ and $x_{3}$ is a homomorphism of $\operatorname{sheafCompose}$ applied to $J$ and $F$ and $\operatorname{sheafCompose}$ applied to $J$ and $G$.
CategoryTheory.Equivalence.skeletonEquivdefMathlib.CategoryTheory.Skeletal, function or constantWording
the skeleton equivalence of e (from the name)
English
Let $e$ be an equivalence of $C$ and $D$. Then the skeleton equivalence of $e$ is an equivalence from the set of skeletons of $C$ to the set of skeletons of $D$.
CategoryTheory.Equivalence.thinSkeletonOrderIsodefMathlib.CategoryTheory.Skeletal, function or constantWording
the thin skeleton order isomorphism of e (from the name)
English
Let $e$ be an equivalence of $C$ and $x_{1}$. Then the thin skeleton order isomorphism of $e$ is an order isomorphism of the set of thin skeletons of $C$ and $x_{1}$ defined as the order isomorphism of the composition of the equivalence of $C$ and $e$.
CategoryTheory.Functor.mapSkeletondefMathlib.CategoryTheory.Skeletal, function or constantWording
the map skeleton of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the map skeleton of $F$ is a functor of the set of skeletons of $C$ and the set of skeletons of $D$ defined as the composition of the functor of the skeleton equivalence of $C$ and the composition of $F$ and the inverse of the skeleton equivalence of $D$.
CategoryTheory.Functor.toSkeletonFunctorCompMapSkeletonIsodefMathlib.CategoryTheory.Skeletal, function or constantWording
the skeleton functor composition map skeleton isomorphism of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the skeleton functor composition map skeleton isomorphism of $F$ is an isomorphism of the composition of the skeleton functor of $C$ and the map skeleton of $F$ and the composition of $F$ and the skeleton functor of $D$.
CategoryTheory.IsSkeletonOfstructureMathlib.CategoryTheory.Skeletal, predicateEnglish
Let $C$ and $D$ be sets. Let $F$ be a functor of $D$ and $C$. Then we can say that $\operatorname{IsSkeletonOf}$ holds for $C$, $D$ and $F$.
CategoryTheory.SkeletaldefMathlib.CategoryTheory.Skeletal, predicateWording
C is skeletal (from the docstring)
English
Let $C$ be a set. Then $C$ is skeletal, if for all elements $X$ and $Y$ of $C$, if $X$ is isomorphic to $Y$, then $\EqtMACRoH {X}{Y}$.
CategoryTheory.SkeletondefMathlib.CategoryTheory.Skeletal, typeWording
skeleton of C (from the name)
English
Let $C$ be a set. Then a skeleton of $C$ is an element of the function that maps $C$ to the set of induced categories of $C$ and $\operatorname{out}$.
CategoryTheory.Skeleton.isoOfEqdefMathlib.CategoryTheory.Skeletal, function or constantWording
the isomorphism of h (from the name)
English
Assume that the class of $X$ is equal to the class of $Y$. Then the isomorphism of $h$ is an isomorphism of $X$ and $Y$.
CategoryTheory.ThinSkeletondefMathlib.CategoryTheory.Skeletal, typeWording
thin skeleton of C (from the name)
English
Let $C$ be a set. Then a thin skeleton of $C$ is an element of the function that maps $C$ to $\mathrm{Quotient}$ applied to $\operatorname{isIsomorphicSetoid}$ applied to $C$.
CategoryTheory.ThinSkeleton.equivalencedefMathlib.CategoryTheory.Skeletal, function or constantWording
the equivalence of C (from the name)
English
Let $C$ be a set. Then the equivalence of $C$ is an equivalence of the set of thin skeletons of $C$ and $C$.
CategoryTheory.ThinSkeleton.fromThinSkeletondefMathlib.CategoryTheory.Skeletal, function or constantEnglish
Let $C$ be a set. Then $\operatorname{fromThinSkeleton}$ applied to $C$ is a functor of the set of thin skeletons of $C$ and $C$.
CategoryTheory.ThinSkeleton.fromThinSkeletonCompToThinSkeletonIsodefMathlib.CategoryTheory.Skeletal, function or constantEnglish
Let $F$ be a functor of $C$ and $D$. Then $\operatorname{fromThinSkeletonCompToThinSkeletonIso}$ applied to $F$ is an isomorphism of the composition of $\operatorname{fromThinSkeleton}$ applied to $C$ and the composition of $F$ and the functor of $D$ and the map of $F$ defined as the composition of the left isomorphism whisker of $\operatorname{fromThinSkeleton}$ applied to $C$ and the identity of the composition of $F$ and the functor of $D$ and the composition of the right isomorphism whisker of the inverse of the unit isomorphism of the equivalence of $C$ and the map of $F$ and the left unitor of the map of $F$.
CategoryTheory.ThinSkeleton.lowerAdjunctiondefMathlib.CategoryTheory.Skeletal, function or constantWording
the lower adjunction of L and h (from the name)
English
Let $R$ be a functor of $D$ and $C$. Let $L$ be a functor of $C$ and $D$. Let $h$ be an adjunction of $L$ and $R$. Then the lower adjunction of $L$ and $h$ is an adjunction of the map of $L$ and the map of $R$.
CategoryTheory.ThinSkeleton.mapdefMathlib.CategoryTheory.Skeletal, function or constantWording
the map of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the map of $F$ is a functor of the set of thin skeletons of $C$ and the set of thin skeletons of $D$.
CategoryTheory.ThinSkeleton.mapCompFromThinSkeletonIsodefMathlib.CategoryTheory.Skeletal, function or constantWording
the map composition from thin skeleton isomorphism of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the map composition from thin skeleton isomorphism of $F$ is an isomorphism of the composition of the map of $F$ and $\operatorname{fromThinSkeleton}$ applied to $D$ and the composition of $\operatorname{fromThinSkeleton}$ applied to $C$ and $F$ defined as the composition of the right isomorphism whisker of the inverse of $\operatorname{fromThinSkeletonCompToThinSkeletonIso}$ applied to $F$ and $\operatorname{fromThinSkeleton}$ applied to $D$ and the composition of the left isomorphism whisker of the composition of $\operatorname{fromThinSkeleton}$ applied to $C$ and $F$ and the counit isomorphism of the equivalence of $D$ and the right unitor of the composition of $\operatorname{fromThinSkeleton}$ applied to $C$ and $F$.
CategoryTheory.ThinSkeleton.mapNatTransdefMathlib.CategoryTheory.Skeletal, function or constantWording
the map natural transformation of k (from the name)
English
Let $k$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the map natural transformation of $k$ is a homomorphism of the map of $x_{2}$ and the map of $x_{3}$.
CategoryTheory.ThinSkeleton.map₂defMathlib.CategoryTheory.Skeletal, function or constantWording
the map of F (from the name)
English
Let $F$ be a functor of $C$ and the set of functors of $D$ and $E$. Then the map of $F$ is a functor of the set of thin skeletons of $C$ and the set of functors of the set of thin skeletons of $D$ and the set of thin skeletons of $E$.
CategoryTheory.ThinSkeleton.map₂FunctordefMathlib.CategoryTheory.Skeletal, function or constantWording
the map functor of F and x3 (from the name)
English
Let $F$ be a functor of $C$ and the set of functors of $D$ and $E$. Let $x_{3}$ be a thin skeleton of $C$. Then the map functor of $F$ and $x_{3}$ is a functor of the set of thin skeletons of $D$ and the set of thin skeletons of $E$.
CategoryTheory.ThinSkeleton.map₂NatTransdefMathlib.CategoryTheory.Skeletal, function or constantWording
the map natural transformation of F and x5 (from the name)
English
Let $F$ be a functor of $C$ and the set of functors of $D$ and $E$. Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the map natural transformation of $F$ and $x_{5}$ is a homomorphism of the map functor of $F$ and $x_{3}$ and the map functor of $F$ and $x_{4}$.
CategoryTheory.ThinSkeleton.map₂ObjMapdefMathlib.CategoryTheory.Skeletal, function or constantWording
the map object map of x3 and x4 (from the name)
English
Let $F$ be a functor of $C$ and the set of functors of $D$ and $E$. Let $x_{3}$ be a thin skeleton of $C$. Let $x_{4}$ be a thin skeleton of $D$. Then the map object map of $x_{3}$ and $x_{4}$ is a thin skeleton of $E$.
CategoryTheory.ThinSkeleton.mkdefMathlib.CategoryTheory.Skeletal, function or constantEnglish
Let $c$ be an element of $C$. Then $\operatorname{mk}$ applied to $c$ is a thin skeleton of $C$ defined as $\operatorname{mk'}$ applied to $c$.
CategoryTheory.fromSkeletondefMathlib.CategoryTheory.Skeletal, function or constantEnglish
Let $C$ be a set. Then $\operatorname{fromSkeleton}$ applied to $C$ is a functor of the set of skeletons of $C$ and $C$ defined as the induced functor of $\operatorname{out}$.
CategoryTheory.fromSkeletonToSkeletonIsodefMathlib.CategoryTheory.Skeletal, function or constantEnglish
Let $X$ be an element of $C$. Then $\operatorname{fromSkeletonToSkeletonIso}$ applied to $X$ is an isomorphism of the action of $\operatorname{fromSkeleton}$ applied to $C$ and the class of $X$ and $X$.
CategoryTheory.skeletonEquivalencedefMathlib.CategoryTheory.Skeletal, function or constantWording
the skeleton equivalence of C (from the name)
English
Let $C$ be a set. Then the skeleton equivalence of $C$ is an equivalence of the set of skeletons of $C$ and $C$.
CategoryTheory.toSkeletondefMathlib.CategoryTheory.Skeletal, function or constantWording
the class of X (from the docstring)
English
Let $X$ be an element of $C$. Then the class of $X$ is a skeleton of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{isIsomorphicSetoid}$ applied to $C$ and $X$.
CategoryTheory.toSkeletonFunctordefMathlib.CategoryTheory.Skeletal, function or constantWording
the skeleton functor of C (from the name)
English
Let $C$ be a set. Then the skeleton functor of $C$ is a functor of $C$ and the set of skeletons of $C$.
CategoryTheory.toThinSkeletondefMathlib.CategoryTheory.Skeletal, function or constantWording
the functor of C (from the docstring)
English
Let $C$ be a set. Then the functor of $C$ is a functor of $C$ and the set of thin skeletons of $C$.
CategoryTheory.MorphismProperty.HasSmallObjectArgumentclassMathlib.CategoryTheory.SmallObject.Basic, predicateWording
I has small object arguments (from the name)
English
Let $I$ be a morphism property of $C$. Then we can say that $I$ has small object arguments.
CategoryTheory.MorphismProperty.smallObjectκdefMathlib.CategoryTheory.SmallObject.Basic, function or constantWording
the small object of I (from the name)
English
Let $I$ be a morphism property of $C$. Then the small object of $I$ is a cardinal defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_HasSmallObjectArgument\_\_exists\_cardinal}$.
CategoryTheory.SmallObject.FunctorObjIndexstructureMathlib.CategoryTheory.SmallObject.Construction, typeWording
functor object index of f and i (from the name)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Then the functor object indexes of $i$ and $f$ are a basic type.
CategoryTheory.SmallObject.FunctorObjIndex.bdefMathlib.CategoryTheory.SmallObject.Construction, function or constantEnglish
Let $\mathrm{self}$ be a functor object index of $f$ and $x_{1}$. Then $\operatorname{b}$ applied to $\mathrm{self}$ is a homomorphism of $B$ applied to $\operatorname{i}$ applied to $\mathrm{self}$ and $S$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
CategoryTheory.SmallObject.FunctorObjIndex.idefMathlib.CategoryTheory.SmallObject.Construction, function or constantEnglish
Let $\mathrm{self}$ be a functor object index of $f$ and $x_{1}$. Then $\operatorname{i}$ applied to $\mathrm{self}$ is an element of $I$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.SmallObject.FunctorObjIndex.tdefMathlib.CategoryTheory.SmallObject.Construction, function or constantEnglish
Let $\mathrm{self}$ be a functor object index of $f$ and $x_{1}$. Then $\operatorname{t}$ applied to $\mathrm{self}$ is a homomorphism of $A$ applied to $\operatorname{i}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
CategoryTheory.SmallObject.attachCellsιFunctorObjdefMathlib.CategoryTheory.SmallObject.Construction, function or constantEnglish
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Then $\mathrm{CategoryTheory\_\_SmallObject\_\_attachCells\_u3b9\_FunctorObj}$ applied to $i$, $f$ and $x_{1}$ is an element of $\operatorname{AttachCells}$ applied to $f$ and the inclusion functor object of $f$ and $x_{1}$.
CategoryTheory.SmallObject.attachCellsιFunctorObjOfSmalldefMathlib.CategoryTheory.SmallObject.Construction, function or constantEnglish
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Then $\mathrm{CategoryTheory\_\_SmallObject\_\_attachCells\_u3b9\_FunctorObjOfSmall}$ applied to $i$, $f$ and $x_{1}$ is an element of $\operatorname{AttachCells}$ applied to $f$ and the inclusion functor object of $f$ and $x_{1}$ defined as the function that maps $x_{1}$ to the reindexing of $\mathrm{CategoryTheory\_\_SmallObject\_\_attachCells\_u3b9\_FunctorObj}$ applied to $i$ and $f$ and the inverse of the equivalence shrink of the set of inclusions of $\mathrm{CategoryTheory\_\_SmallObject\_\_attachCells\_u3b9\_FunctorObj}$ applied to $i$ and $f$.
CategoryTheory.SmallObject.functordefMathlib.CategoryTheory.SmallObject.Construction, function or constantWording
the functor of f (from the docstring)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Then the functor of $i$ is a functor of the set of arrows of $C$ and the set of arrows of $C$.
CategoryTheory.SmallObject.functorMapdefMathlib.CategoryTheory.SmallObject.Construction, function or constantWording
the functor of f and i (from the docstring)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{3}$ be a homomorphism of $\operatorname{mk}$ applied to $x_{1}$ and $\operatorname{mk}$ applied to $x_{2}$. Then the functor of $i$ and $f$ is a homomorphism of the functor of $f$ and $x_{1}$ and the functor of $f$ and $x_{2}$.
CategoryTheory.SmallObject.functorMapSrcdefMathlib.CategoryTheory.SmallObject.Construction, function or constantEnglish
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{3}$ be a homomorphism of $\operatorname{mk}$ applied to $x_{1}$ and $\operatorname{mk}$ applied to $x_{2}$. Then $\operatorname{functorMapSrc}$ applied to $i$, $f$ and $x_{3}$ is a homomorphism of the sigma object of $\operatorname{functorObjSrcFamily}$ applied to $f$ and $x_{1}$ and the sigma object of $\operatorname{functorObjSrcFamily}$ applied to $f$ and $x_{2}$.
CategoryTheory.SmallObject.functorMapTgtdefMathlib.CategoryTheory.SmallObject.Construction, function or constantEnglish
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{3}$ be a homomorphism of $\operatorname{mk}$ applied to $x_{1}$ and $\operatorname{mk}$ applied to $x_{2}$. Then $\operatorname{functorMapTgt}$ applied to $i$, $f$ and $x_{3}$ is a homomorphism of the sigma object of $\operatorname{functorObjTgtFamily}$ applied to $f$ and $x_{1}$ and the sigma object of $\operatorname{functorObjTgtFamily}$ applied to $f$ and $x_{2}$.
CategoryTheory.SmallObject.functorObjdefMathlib.CategoryTheory.SmallObject.Construction, function or constantWording
the functor of f and i (from the docstring)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Then the functor of $i$ and $f$ is an element of $C$ defined as the function that maps $x_{1}$ to the pushout of the functor object top of $i$ and $f$ and the left functor object of $i$ and $f$.
CategoryTheory.SmallObject.functorObjLeftdefMathlib.CategoryTheory.SmallObject.Construction, function or constantWording
the left functor object of f and i (from the name)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Then the left functor object of $i$ and $f$ is a homomorphism of the sigma object of $\operatorname{functorObjSrcFamily}$ applied to $f$ and $x_{1}$ and the sigma object of $\operatorname{functorObjTgtFamily}$ applied to $f$ and $x_{1}$ defined as the function that maps $x_{1}$ to the map of $\operatorname{functorObjLeftFamily}$ applied to $f$.
CategoryTheory.SmallObject.functorObjLeftFamilydefMathlib.CategoryTheory.SmallObject.Construction, function or constantWording
the functor object left family of i and x1 (from the name)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Let $x_{2}$ be a functor object index of $f$ and $x_{1}$. Then the functor object left family of $f$ and $x_{1}$ is a homomorphism of $\operatorname{functorObjSrcFamily}$ applied to $f$, $x_{1}$ and $x_{2}$ and $\operatorname{functorObjTgtFamily}$ applied to $f$, $x_{1}$ and $x_{2}$ defined as the function that maps $x_{2}$ to $i$ applied to $\operatorname{i}$ applied to $x_{1}$ and $x_{2}$.
CategoryTheory.SmallObject.functorObjSrcFamilydefMathlib.CategoryTheory.SmallObject.Construction, function or constantEnglish
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Let $x_{2}$ be a functor object index of $f$ and $x_{1}$. Then $\operatorname{functorObjSrcFamily}$ applied to $i$, $f$, $x_{1}$ and $x_{2}$ is an element of $C$ defined as the function that maps $x_{2}$ to $A$ applied to $\operatorname{i}$ applied to $x_{1}$ and $x_{2}$.
CategoryTheory.SmallObject.functorObjTgtFamilydefMathlib.CategoryTheory.SmallObject.Construction, function or constantEnglish
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Let $x_{2}$ be a functor object index of $f$ and $x_{1}$. Then $\operatorname{functorObjTgtFamily}$ applied to $i$, $f$, $x_{1}$ and $x_{2}$ is an element of $C$ defined as the function that maps $x_{2}$ to $B$ applied to $\operatorname{i}$ applied to $x_{1}$ and $x_{2}$.
CategoryTheory.SmallObject.functorObjTopdefMathlib.CategoryTheory.SmallObject.Construction, function or constantWording
the functor object top of f and i (from the name)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Then the functor object top of $i$ and $f$ is a homomorphism of the sigma object of $\operatorname{functorObjSrcFamily}$ applied to $f$ and $x_{1}$ and $X$ defined as the function that maps $x_{1}$ to $\operatorname{desc}$ applied to the function that maps $x_{2}$ to $\operatorname{t}$ applied to $x_{2}$ and $x_{1}$.
CategoryTheory.SmallObject.εdefMathlib.CategoryTheory.SmallObject.Construction, function or constantEnglish
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Then $\mathrm{CategoryTheory\_\_SmallObject\_\_\_u3b5\_}$ applied to $i$ and $f$ is a homomorphism of the identity of the set of arrows of $C$ and the functor of $f$.
CategoryTheory.SmallObject.ιFunctorObjdefMathlib.CategoryTheory.SmallObject.Construction, function or constantWording
the inclusion functor object of f and i (from the name)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Then the inclusion functor object of $i$ and $f$ is a homomorphism of $X$ and the functor of $f$ and $x_{1}$ defined as the function that maps $x_{1}$ to the left injection of the functor object top of $i$ and $f$ and the left functor object of $i$ and $f$.
CategoryTheory.SmallObject.π'FunctorObjdefMathlib.CategoryTheory.SmallObject.Construction, function or constantWording
the canonical projection on the base object of f and i (from the docstring)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Then the canonical projection on the base object of $i$ and $f$ is a homomorphism of the sigma object of $\operatorname{functorObjTgtFamily}$ applied to $f$ and $x_{1}$ and $S$ defined as the function that maps $x_{1}$ to $\operatorname{desc}$ applied to the function that maps $x_{2}$ to $\operatorname{b}$ applied to $x_{2}$ and $x_{1}$.
CategoryTheory.SmallObject.πFunctorObjdefMathlib.CategoryTheory.SmallObject.Construction, function or constantWording
the canonical projection on the base object of f and i (from the docstring)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Then the canonical projection on the base object of $i$ and $f$ is a homomorphism of the functor of $f$ and $x_{1}$ and $S$.
CategoryTheory.SmallObject.ρFunctorObjdefMathlib.CategoryTheory.SmallObject.Construction, function or constantWording
the functor object of f and i (from the name)
English
Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $x_{1}$ be a homomorphism of $X$ and $S$. Then the functor object of $i$ and $f$ is a homomorphism of the sigma object of $\operatorname{functorObjTgtFamily}$ applied to $f$ and $x_{1}$ and the functor of $f$ and $x_{1}$ defined as the function that maps $x_{1}$ to the right injection of the functor object top of $i$ and $f$ and the left functor object of $i$ and $f$.
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgumentclassMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, predicateEnglish
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Then we can say that $\operatorname{IsCardinalForSmallObjectArgument}$ holds for $I$ and $x_{1}$.
CategoryTheory.SmallObject.attachCellsOfSuccStructPropdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantEnglish
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal such that $\operatorname{prop}$ holds for $\operatorname{succStruct}$ applied to $I$ and $x_{1}$, $F$, $G$ and $x_{3}$. Let $f$ be an arrow of $C$. Then $\operatorname{attachCellsOfSuccStructProp}$ applied to $I$, $x_{1}$, $h_{2}$ and $f$ is an element of $\operatorname{AttachCells}$ applied to $\operatorname{homFamily}$ applied to $I$ and the left part of the component of $x_{3}$ and $f$ defined as $\operatorname{ofArrowIso}$ applied to $\mathrm{CategoryTheory\_\_SmallObject\_\_attachCells\_u3b9\_FunctorObjOfSmall}$ applied to $\operatorname{homFamily}$ applied to $I$ and the homomorphism of the action of $F$ and $f$ and the map isomorphism of the map arrow of the composition of the action of the evaluation of the set of arrows of $C$ and the set of arrows of $C$ and $f$ and the left function and the inverse of the arrow isomorphism of $h_{2}$.
CategoryTheory.SmallObject.functorialFactorizationDatadefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the functorial factorization of I and x1 (from the docstring)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Then the functorial factorization of $I$ and $x_{1}$ is a functorial factorization data of $\operatorname{llp}$ applied to $\operatorname{rlp}$ applied to $I$ and $\operatorname{rlp}$ applied to $I$.
CategoryTheory.SmallObject.iterationdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the iteration of I and x1 (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Then the iteration of $I$ and $x_{1}$ is a functor of the set of arrows of $C$ and the set of arrows of $C$ defined as the iteration of $\operatorname{succStruct}$ applied to $I$ and $x_{1}$ and the set of types of the order of $x_{1}$.
CategoryTheory.SmallObject.iterationFunctordefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the functor of I and x1 (from the docstring)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Then the functor of $I$ and $x_{1}$ is a functor of the set of types of the order of $x_{1}$ and the set of functors of the set of arrows of $C$ and the set of arrows of $C$ defined as the iteration functor of $\operatorname{succStruct}$ applied to $I$ and $x_{1}$ and the set of types of the order of $x_{1}$.
CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIsodefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the iteration functor map successor application arrow isomorphism of f and j (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Let $f$ be an arrow of $C$. Let $j$ be a type of the order of $x_{1}$. Then the iteration functor map successor application arrow isomorphism of $f$ and $j$ is an isomorphism of $\operatorname{mk}$ applied to the component of the map of the functor of $I$ and $x_{1}$ and the homomorphism of $\mathrm{Order\_\_le\_succ}$ applied to $j$ and $f$ and $\operatorname{mk}$ applied to the component of $\mathrm{CategoryTheory\_\_SmallObject\_\_\_u3b5\_}$ applied to $\operatorname{homFamily}$ applied to $I$ and the action of the action of the functor of $I$ and $x_{1}$ and $j$ and $f$.
CategoryTheory.SmallObject.iterationFunctorObjObjRightIsodefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the iteration functor object object right isomorphism of f and j (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Let $f$ be an arrow of $C$. Let $j$ be a type of the order of $x_{1}$. Then the iteration functor object object right isomorphism of $f$ and $j$ is an isomorphism of the right object of the action of the action of the functor of $I$ and $x_{1}$ and $j$ and $f$ and the right object of $f$ defined as the composition of $\operatorname{asIso}$ applied to the component of the inclusion of $\operatorname{toTransfiniteCompositionOfShape}$ applied to the transfinite composition of $x_{1}$ and $f$ and $j$ and the inverse of the iteration object right isomorphism of $x_{1}$ and $f$.
CategoryTheory.SmallObject.iterationObjRightIsodefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the iteration object right isomorphism of x1 and f (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Let $f$ be an arrow of $C$. Then the iteration object right isomorphism of $x_{1}$ and $f$ is an isomorphism of the right object of $f$ and the right object of the action of the iteration of $I$ and $x_{1}$ and $f$ defined as $\operatorname{asIso}$ applied to the right part of the component of the inclusion iteration of $I$ and $x_{1}$ and $f$.
CategoryTheory.SmallObject.objdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the object of x1 and f (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Let $f$ be a homomorphism of $X$ and $Y$. Then the object of $x_{1}$ and $f$ is an element of $C$ defined as the left object of the action of the iteration of $I$ and $x_{1}$ and $\operatorname{mk}$ applied to $f$.
CategoryTheory.SmallObject.objMapdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the object map of x1 and x3 (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Let $x_{3}$ be a homomorphism of $f$ and $g$. Then the object map of $x_{1}$ and $x_{3}$ is a homomorphism of the object of $x_{1}$ and the homomorphism of $f$ and the object of $x_{1}$ and the homomorphism of $g$ defined as the left part of the map of the iteration of $I$ and $x_{1}$ and $x_{3}$.
CategoryTheory.SmallObject.propArrowdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantEnglish
Let $I$ be a morphism property of $C$. Then there is a morphism property of the set of arrows of $C$. Proof. Let $I$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. Let $f$ be arbitrary. By I. By CategoryTheory__MorphismProperty__coproducts. By CategoryTheory__MorphismProperty__pushouts. By C. By CategoryTheory__MorphismProperty__isomorphisms. By and.
CategoryTheory.SmallObject.relativeCellComplexιObjdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the relative cell complex inclusion object of x1 and f (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Let $f$ be a homomorphism of $X$ and $Y$. Then the relative cell complex inclusion object of $x_{1}$ and $f$ is a relative cell complex of the function that maps $x_{3}$ to $\operatorname{homFamily}$ applied to $I$ and the inclusion object of $x_{1}$ and $f$.
CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIsodefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the relative cell complex inclusion object object successor isomorphism of f and j (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Let $f$ be a homomorphism of $X$ and $Y$. Let $j$ be a type of the order of $x_{1}$. Then the relative cell complex inclusion object object successor isomorphism of $f$ and $j$ is an isomorphism of the action of $\operatorname{F}$ applied to $\operatorname{toTransfiniteCompositionOfShape}$ applied to the relative cell complex inclusion object of $x_{1}$ and $f$ and the successor of $j$ and the functor of $\operatorname{homFamily}$ applied to $I$ and the homomorphism of the action of the action of the functor of $I$ and $x_{1}$ and $j$ and $\operatorname{mk}$ applied to $f$ defined as the map isomorphism of the composition of the right function and the left function and the iteration functor map successor application arrow isomorphism of $\operatorname{mk}$ applied to $f$ and $j$.
CategoryTheory.SmallObject.succStructdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantEnglish
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Then $\operatorname{succStruct}$ applied to $I$ and $x_{1}$ is an element of $\operatorname{SuccStruct}$ applied to the set of functors of the set of arrows of $C$ and the set of arrows of $C$ defined as $\operatorname{ofNatTrans}$ applied to $\mathrm{CategoryTheory\_\_SmallObject\_\_\_u3b5\_}$ applied to $\operatorname{homFamily}$ applied to $I$.
CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropιIterationdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the transfinite composition of I and x1 (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Then the transfinite composition of $I$ and $x_{1}$ is a transfinite composition of shape of the set of types of the order of $x_{1}$ and the inclusion iteration of $I$ and $x_{1}$ defined as the inclusion of $\operatorname{succStruct}$ applied to $I$ and $x_{1}$ and the set of types of the order of $x_{1}$.
CategoryTheory.SmallObject.transfiniteCompositionOfShapeιIterationAppRightdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the transfinite composition of x1 and f (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Let $f$ be an arrow of $C$. Then the transfinite composition of $x_{1}$ and $f$ is a transfinite composition of shape of the set of types of the order of $x_{1}$ and the right part of the component of the inclusion iteration of $I$ and $x_{1}$ and $f$.
CategoryTheory.SmallObject.ιIterationdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the inclusion iteration of I and x1 (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Then the inclusion iteration of $I$ and $x_{1}$ is a homomorphism of the identity of the set of arrows of $C$ and the iteration of $I$ and $x_{1}$ defined as the inclusion iteration of $\operatorname{succStruct}$ applied to $I$ and $x_{1}$ and the set of types of the order of $x_{1}$.
CategoryTheory.SmallObject.ιObjdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the inclusion object of x1 and f (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Let $f$ be a homomorphism of $X$ and $Y$. Then the inclusion object of $x_{1}$ and $f$ is a homomorphism of $X$ and the object of $x_{1}$ and $f$ defined as the left part of the component of the inclusion iteration of $I$ and $x_{1}$ and $\operatorname{mk}$ applied to $f$.
CategoryTheory.SmallObject.πObjdefMathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument, function or constantWording
the projection object of x1 and f (from the name)
English
Let $I$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Let $f$ be a homomorphism of $X$ and $Y$. Then the projection object of $x_{1}$ and $f$ is a homomorphism of the object of $x_{1}$ and $f$ and $Y$ defined as the composition of the homomorphism of the action of the iteration of $I$ and $x_{1}$ and $\operatorname{mk}$ applied to $f$ and the inverse of the right part of the component of the inclusion iteration of $I$ and $x_{1}$ and $\operatorname{mk}$ applied to $f$.
CategoryTheory.SmallObject.SuccStructstructureMathlib.CategoryTheory.SmallObject.Iteration.Basic, typeEnglish
Let $C$ be a set. Then the elements of $\operatorname{SuccStruct}$ applied to $C$ are a basic type.
CategoryTheory.SmallObject.SuccStruct.IterationstructureMathlib.CategoryTheory.SmallObject.Iteration.Basic, typeWording
iteration of x1 and j (from the name)
English
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $j$ be an element of $J$. Then the iterations of $x_{1}$ and $j$ are a basic type.
CategoryTheory.SmallObject.SuccStruct.Iteration.FdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantEnglish
Let $\mathrm{self}$ be an iteration of $x_{1}$ and $j$. Then $\operatorname{F}$ applied to $\mathrm{self}$ is a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.SmallObject.SuccStruct.Iteration.isColimitdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantEnglish
Let $\mathrm{iter}$ be an iteration of $x_{1}$ and $j$. Let $i$ be an element of $J$ such that $i$ is a successor limit and $i \leq j$. Then $\operatorname{isColimit}$ applied to $\mathrm{iter}$, $i$, $\mathrm{hi}$ and $\mathrm{hij}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $\operatorname{F}$ applied to $\mathrm{iter}$ and $\mathrm{hij}$.
CategoryTheory.SmallObject.SuccStruct.Iteration.mapObjdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantWording
the map object of x7 and x8 (from the name)
English
Let $x_{7}$ be an iteration of $x_{1}$ and $x_{5}$. Let $x_{8}$ be an iteration of $x_{1}$ and $x_{6}$. Assume that $x_{9} \leq x_{10}$. Assume that $x_{9} \leq x_{5}$. Assume that $x_{10} \leq x_{6}$. Assume that $x_{5} \leq x_{6}$. Then the map object of $x_{7}$ and $x_{8}$ is a homomorphism of the action of $\operatorname{F}$ applied to $x_{7}$ and $x_{9}$ and the action of $\operatorname{F}$ applied to $x_{8}$ and $x_{10}$.
CategoryTheory.SmallObject.SuccStruct.Iteration.truncdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantWording
the truncation of iter and #2 (from the name)
English
Let $\mathrm{iter}$ be an iteration of $x_{1}$ and $j$. Assume that $\mathrm{j'} \leq j$. Then the truncation of $\mathrm{iter}$ and $\mathrm{hj'}$ is an iteration of $x_{1}$ and $\mathrm{j'}$.
CategoryTheory.SmallObject.SuccStruct.X₀defMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Then $\mathrm{CategoryTheory\_\_SmallObject\_\_SuccStruct\_\_X\_u2080\_}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.SmallObject.SuccStruct.arrowMapdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantWording
the arrow map of x2 and x3 (from the name)
English
Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Let $x_{2}$ and $x_{3}$ be elements of $J$ such that $x_{2} \leq x_{3} \leq j$. Then the arrow map of $x_{2}$ and $x_{3}$ is an arrow of $C$ defined as $\operatorname{mk}$ applied to the map of $F$ and the homomorphism of $h$.
CategoryTheory.SmallObject.SuccStruct.arrowSuccdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantWording
the arrow successor of F and i (from the name)
English
Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Let $i$ be an element of $J$ such that $i < j$. Then the arrow successor of $F$ and $i$ is an arrow of $C$.
CategoryTheory.SmallObject.SuccStruct.arrowιdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantWording
the arrow inclusion of F and k (from the name)
English
Let $F$ be a functor of the set of elements of $\operatorname{Iio}$ applied to $i$ and $C$. Assume that $i$ is a successor limit. Let $k$ be an element of $J$ such that $k < i$. Then the arrow inclusion of $F$ and $k$ is an arrow of $C$ defined as $\operatorname{mk}$ applied to the inclusion of $F$ and $k$.
CategoryTheory.SmallObject.SuccStruct.ofNatTransdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantEnglish
Let $x_{1}$ be a homomorphism of the identity of $C$ and $F$. Then $\operatorname{ofNatTrans}$ applied to $x_{1}$ is an element of $\operatorname{SuccStruct}$ applied to the set of functors of $C$ and $C$ defined as $\operatorname{mk}$ applied to the identity of $C$, the function that maps $G$ to the composition of $G$ and $F$ and the function that maps $G_{1}$ to the left whisker of $G_{1}$ and $x_{1}$.
CategoryTheory.SmallObject.SuccStruct.propdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantEnglish
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Then there is a morphism property of $C$. Proof. Let $x_{1}$ be arbitrary. Let $X$ be arbitrary. By x1. By X. By CategoryTheory__SmallObject__SuccStruct__toSucc. By CategoryTheory__MorphismProperty__ofHoms.
CategoryTheory.SmallObject.SuccStruct.prop.arrowIsodefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantWording
the arrow isomorphism of hf (from the name)
English
Assume that $\operatorname{prop}$ holds for $x_{1}$, $X$, $Y$ and $f$. Then the arrow isomorphism of $\mathrm{hf}$ is an isomorphism of $\operatorname{mk}$ applied to $f$ and the successor arrow of $x_{1}$ and $X$.
CategoryTheory.SmallObject.SuccStruct.succdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantWording
the successor of self and X (from the docstring)
English
Let $\mathrm{self}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $X$ be an element of $C$. Then the successor of $\mathrm{self}$ and $X$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $X$.
CategoryTheory.SmallObject.SuccStruct.toSuccdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantWording
the map to the successor of self and X (from the docstring)
English
Let $\mathrm{self}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $X$ be an element of $C$. Then the map to the successor of $\mathrm{self}$ and $X$ is a homomorphism of $X$ and the successor of $\mathrm{self}$ and $X$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $X$.
CategoryTheory.SmallObject.SuccStruct.toSuccArrowdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantWording
the successor arrow of x1 and X (from the name)
English
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $X$ be an element of $C$. Then the successor arrow of $x_{1}$ and $X$ is an arrow of $C$ defined as $\operatorname{mk}$ applied to the map to the successor of $x_{1}$ and $X$.
CategoryTheory.SmallObject.coconeOfLEdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantWording
the cocone of F and hi (from the name)
English
Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Assume that $i \leq j$. Then the cocone of $F$ and $\mathrm{hi}$ is a cocone of $\operatorname{restrictionLT}$ applied to $F$ and $\mathrm{hi}$ defined as the cocone of $\operatorname{principalSegIioIicOfLE}$ applied to $\mathrm{hi}$ and $F$.
CategoryTheory.SmallObject.restrictionLEdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantEnglish
Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Assume that $i \leq j$. Then $\operatorname{restrictionLE}$ applied to $F$ and $\mathrm{hi}$ is a functor of the set of elements of $\operatorname{Iic}$ applied to $i$ and $C$.
CategoryTheory.SmallObject.restrictionLTdefMathlib.CategoryTheory.SmallObject.Iteration.Basic, function or constantEnglish
Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Assume that $i \leq j$. Then $\operatorname{restrictionLT}$ applied to $F$ and $\mathrm{hi}$ is a functor of the set of elements of $\operatorname{Iio}$ applied to $i$ and $C$.
CategoryTheory.SmallObject.SuccStruct.extendToSuccdefMathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc, function or constantWording
the extension to hj (from the docstring)
English
Assume that $j$ is not a maximum. Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Let $x_{3}$ be a homomorphism of the action of $F$ and $j$ and $X$. Then the extension to $\mathrm{hj}$ is a functor of the set of elements of $\operatorname{Iic}$ applied to the successor of $j$ and $C$.
CategoryTheory.SmallObject.SuccStruct.extendToSucc.mapdefMathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc, function or constantWording
the map of x4 and x5 (from the name)
English
Assume that $j$ is not a maximum. Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Let $x_{3}$ be a homomorphism of the action of $F$ and $j$ and $X$. Let $x_{4}$ and $x_{5}$ be elements of $J$ such that $x_{4} \leq x_{5}$ and $x_{5}$ is less than or equal to the successor of $j$. Then the map of $x_{4}$ and $x_{5}$ is a homomorphism of the object of $X$ and $x_{4}$ and the object of $X$ and $x_{5}$.
CategoryTheory.SmallObject.SuccStruct.extendToSucc.objdefMathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc, function or constantWording
the object of X and i (from the name)
English
Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Let $X$ be an element of $C$. Let $i$ be an element of $\operatorname{Iic}$ applied to the successor of $j$. Then the object of $X$ and $i$ is an element of $C$ defined as $\mathrm{dite}$ applied to $\mathrm{Leq} (i , j)$, the function that maps $\mathrm{hij}$ to the action of $F$ and $i$ and the function that maps $\mathrm{hij1}$ to $X$.
CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIsodefMathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc, function or constantWording
the object isomorphism of X and i (from the name)
English
Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Let $X$ be an element of $C$. Let $i$ be an element of $\operatorname{Iic}$ applied to $j$. Then the object isomorphism of $X$ and $i$ is an isomorphism of the object of $X$ and $i$ and the action of $F$ and $i$ defined as $\operatorname{eqToIso}$ applied to $\mathrm{CategoryTheory\_\_SmallObject\_\_SuccStruct\_\_extendToSucc\_\_obj\_eq}$ applied to $F$, $X$ and $i$.
CategoryTheory.SmallObject.SuccStruct.extendToSucc.objSuccIsodefMathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc, function or constantWording
the object successor isomorphism of F and X (from the name)
English
Assume that $j$ is not a maximum. Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Let $X$ be an element of $C$. Then the object successor isomorphism of $F$ and $X$ is an isomorphism of the object of $X$ and the successor of $j$ and $X$ defined as $\operatorname{eqToIso}$ applied to $\mathrm{CategoryTheory\_\_SmallObject\_\_SuccStruct\_\_extendToSucc\_\_obj\_succ\_eq}$ applied to $\mathrm{hj}$, $F$ and $X$.
CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIsodefMathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc, function or constantEnglish
Assume that $j$ is not a maximum. Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Let $x_{3}$ be a homomorphism of the action of $F$ and $j$ and $X$. Let $i$ be an element of $J$ such that $i \leq j$. Then $\operatorname{extendToSuccObjIso}$ applied to $\mathrm{hj}$, $F$, $x_{3}$, $i$ and $\mathrm{hi}$ is an isomorphism of the action of the extension to $\mathrm{hj}$ and $i$ and the action of $F$ and $i$ defined as the object isomorphism of $X$ and $i$.
CategoryTheory.SmallObject.SuccStruct.extendToSuccObjSuccIsodefMathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc, function or constantEnglish
Assume that $j$ is not a maximum. Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Let $x_{3}$ be a homomorphism of the action of $F$ and $j$ and $X$. Then $\operatorname{extendToSuccObjSuccIso}$ applied to $\mathrm{hj}$, $F$ and $x_{3}$ is an isomorphism of the action of the extension to $\mathrm{hj}$ and the successor of $j$ and $X$ defined as the object successor isomorphism of $F$ and $X$.
CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIsodefMathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc, function or constantEnglish
Assume that $j$ is not a maximum. Let $F$ be a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$. Let $x_{3}$ be a homomorphism of the action of $F$ and $j$ and $X$. Then $\operatorname{extendToSuccRestrictionLEIso}$ applied to $\mathrm{hj}$, $F$ and $x_{3}$ is an isomorphism of $\operatorname{restrictionLE}$ applied to the extension to $\mathrm{hj}$ and $\mathrm{Order\_\_le\_succ}$ applied to $j$ and $F$.
CategoryTheory.SmallObject.SuccStruct.isColimitCoconeOfLEOfCoconedefMathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone, function or constantEnglish
Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitCoconeOfLEOfCocone}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $\operatorname{ofCocone}$ applied to $c$ and $\mathrm{le\_refl}$ applied to $j$.
CategoryTheory.SmallObject.SuccStruct.ofCoconedefMathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone, function or constantEnglish
Let $c$ be a cocone of $F$. Then $\operatorname{ofCocone}$ applied to $c$ is a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$.
CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIsodefMathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone, function or constantEnglish
Let $c$ be a cocone of $F$. Let $i$ be an element of $J$ such that $i < j$. Then $\operatorname{ofCoconeObjIso}$ applied to $c$, $i$ and $\mathrm{hi}$ is an isomorphism of the action of $\operatorname{ofCocone}$ applied to $c$ and $i$ and the action of $F$ and $i$ defined as $\operatorname{objIso}$ applied to $c$, $i$ and $\mathrm{hi}$.
CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIsoPtdefMathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone, function or constantWording
the isomorphism of c (from the docstring)
English
Let $c$ be a cocone of $F$. Then the isomorphism of $c$ is an isomorphism of the action of $\operatorname{ofCocone}$ applied to $c$ and $j$ and $\operatorname{pt}$ applied to $c$ defined as $\operatorname{objIsoPt}$ applied to $c$.
CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIsodefMathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone, function or constantEnglish
Let $c$ be a cocone of $F$. Then $\operatorname{restrictionLTOfCoconeIso}$ applied to $c$ is an isomorphism of $\operatorname{restrictionLT}$ applied to $\operatorname{ofCocone}$ applied to $c$ and $\mathrm{le\_refl}$ applied to $j$ and $F$.
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfBotdefMathlib.CategoryTheory.SmallObject.Iteration.Nonempty, function or constantEnglish
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $J$ be a set. Then $\operatorname{mkOfBot}$ applied to $x_{1}$ and $J$ is an iteration of $x_{1}$ and the bottom.
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimitdefMathlib.CategoryTheory.SmallObject.Iteration.Nonempty, function or constantEnglish
Assume that $j$ is a successor limit. Let $\mathrm{iter}$ be a function from elements $i$ of $J$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (i , j)$ to iterations of $x_{1}$ and $i$. Then $\operatorname{mkOfLimit}$ applied to $\mathrm{hj}$, $i$ and $\mathrm{iter}$ is an iteration of $x_{1}$ and $j$.
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functordefMathlib.CategoryTheory.SmallObject.Iteration.Nonempty, function or constantWording
the functor of hj and iter (from the name)
English
Assume that $j$ is a successor limit. Let $\mathrm{iter}$ be a function from elements $i$ of $J$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (i , j)$ to iterations of $x_{1}$ and $i$. Then the functor of $\mathrm{hj}$ and $i$ is a functor of the set of elements of $\operatorname{Iic}$ applied to $j$ and $C$ defined as the function that maps $\mathrm{iter}$ to $\operatorname{ofCocone}$ applied to the cocone of the inductive system of $i$ and $\mathrm{iter}$.
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystemdefMathlib.CategoryTheory.SmallObject.Iteration.Nonempty, function or constantWording
the inductive system of iter (from the name)
English
Let $\mathrm{iter}$ be a function from elements $i$ of $J$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (i , j)$ to iterations of $x_{1}$ and $i$. Then the inductive system of $i$ is a functor of the set of elements of $\operatorname{Iio}$ applied to $j$ and $C$.
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfSuccdefMathlib.CategoryTheory.SmallObject.Iteration.Nonempty, function or constantEnglish
Assume that $j$ is not a maximum. Let $\mathrm{iter}$ be an iteration of $x_{1}$ and $j$. Then $\operatorname{mkOfSucc}$ applied to $\mathrm{hj}$ and $\mathrm{iter}$ is an iteration of $x_{1}$ and the successor of $j$.
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStructstructureMathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting, typeEnglish
Let $c$ be a cocone of $F$. Let $p$ be a homomorphism of $X$ and $Y$. Let $f$ be a homomorphism of the action of $F$ and the bottom and $X$. Let $g$ be a homomorphism of $\operatorname{pt}$ applied to $c$ and $Y$. Let $j$ be an element of $J$. Then the elements of $\operatorname{SqStruct}$ applied to $c$, $p$, $f$, $g$ and $j$ are a basic type.
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.f'defMathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{SqStruct}$ applied to $c$, $p$, $f$, $g$ and $j$. Then $\operatorname{f'}$ applied to $\mathrm{self}$ is a homomorphism of the action of $F$ and $j$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctordefMathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting, function or constantWording
the square functor of f and g (from the name)
English
Let $c$ be a cocone of $F$. Let $p$ be a homomorphism of $X$ and $Y$. Let $f$ be a homomorphism of the action of $F$ and the bottom and $X$. Let $g$ be a homomorphism of $\operatorname{pt}$ applied to $c$ and $Y$. Then the square functor of $f$ and $g$ is a functor of the set of opposites of $J$ and the set of sets.
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionDatadefMathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting, function or constantEnglish
Let $c$ be a cocone of $F$. Let $f$ be a homomorphism of the action of $F$ and the bottom and $X$. Let $g$ be a homomorphism of $\operatorname{pt}$ applied to $c$ and $Y$ such that for all elements $j$ of $J$, if $j$ is not a maximum, then $\operatorname{HasLiftingPropertyFixedBot}$ holds for the map of $F$ and the homomorphism of $\mathrm{Order\_\_le\_succ}$ applied to $j$, $p$ and the composition of the component of the inclusion of $c$ and the successor of $j$ and $g$. Then $\operatorname{wellOrderInductionData}$ applied to $c$, $f$, $g$ and $\mathrm{hF}$ is an element of $\operatorname{WellOrderInductionData}$ applied to the square functor of $f$ and $g$.
CategoryTheory.SmallObject.SuccStruct.isColimitIterationCoconedefMathlib.CategoryTheory.SmallObject.TransfiniteIteration, function or constantEnglish
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $J$ be a set. Then $\operatorname{isColimitIterationCocone}$ applied to $x_{1}$ and $J$ is an element of $\operatorname{IsColimit}$ applied to the iteration cocone of $x_{1}$ and $J$ defined as $\operatorname{isColimit}$ applied to the iteration functor of $x_{1}$ and $J$.
CategoryTheory.SmallObject.SuccStruct.iterdefMathlib.CategoryTheory.SmallObject.TransfiniteIteration, function or constantEnglish
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $j$ be an element of $J$. Then $\operatorname{iter}$ applied to $x_{1}$ and $j$ is an iteration of $x_{1}$ and $j$ defined as $\operatorname{arbitrary}$ applied to the set of iterations of $x_{1}$ and $j$.
CategoryTheory.SmallObject.SuccStruct.iterationdefMathlib.CategoryTheory.SmallObject.TransfiniteIteration, function or constantWording
the iteration of x1 and J (from the name)
English
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $J$ be a set. Then the iteration of $x_{1}$ and $J$ is an element of $C$ defined as the colimit of the iteration functor of $x_{1}$ and $J$.
CategoryTheory.SmallObject.SuccStruct.iterationCoconedefMathlib.CategoryTheory.SmallObject.TransfiniteIteration, function or constantWording
the iteration cocone of x1 and J (from the name)
English
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $J$ be a set. Then the iteration cocone of $x_{1}$ and $J$ is a cocone of the iteration functor of $x_{1}$ and $J$ defined as the cocone of the iteration functor of $x_{1}$ and $J$.
CategoryTheory.SmallObject.SuccStruct.iterationFunctordefMathlib.CategoryTheory.SmallObject.TransfiniteIteration, function or constantWording
the iteration functor of x1 and J (from the name)
English
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $J$ be a set. Then the iteration functor of $x_{1}$ and $J$ is a functor of $J$ and $C$.
CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjBotIsodefMathlib.CategoryTheory.SmallObject.TransfiniteIteration, function or constantWording
the isomorphism of x1 and J (from the docstring)
English
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $J$ be a set. Then the isomorphism of $x_{1}$ and $J$ is an isomorphism of the action of the iteration functor of $x_{1}$ and $J$ and the bottom and $\mathrm{CategoryTheory\_\_SmallObject\_\_SuccStruct\_\_X\_u2080\_}$ applied to $x_{1}$.
CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjSuccIsodefMathlib.CategoryTheory.SmallObject.TransfiniteIteration, function or constantWording
the iteration functor object successor isomorphism of x1 and j (from the name)
English
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $j$ be an element of $J$ such that $j$ is not a maximum. Then the iteration functor object successor isomorphism of $x_{1}$ and $j$ is an isomorphism of the action of the iteration functor of $x_{1}$ and $J$ and the successor of $j$ and the successor of $x_{1}$ and the action of the iteration functor of $x_{1}$ and $J$ and $j$.
CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIterationdefMathlib.CategoryTheory.SmallObject.TransfiniteIteration, function or constantWording
the inclusion of x1 and J (from the docstring)
English
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $J$ be a set. Then the inclusion of $x_{1}$ and $J$ is a transfinite composition of shape of $J$ and the inclusion iteration of $x_{1}$ and $J$.
CategoryTheory.SmallObject.SuccStruct.ιIterationdefMathlib.CategoryTheory.SmallObject.TransfiniteIteration, function or constantWording
the inclusion iteration of x1 and J (from the name)
English
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $J$ be a set. Then the inclusion iteration of $x_{1}$ and $J$ is a homomorphism of $\mathrm{CategoryTheory\_\_SmallObject\_\_SuccStruct\_\_X\_u2080\_}$ applied to $x_{1}$ and the iteration of $x_{1}$ and $J$ defined as the composition of the inverse of the isomorphism of $x_{1}$ and $J$ and the inclusion of the iteration functor of $x_{1}$ and $J$ and the bottom.
CategoryTheory.SmallObject.SuccStruct.ιIterationFunctordefMathlib.CategoryTheory.SmallObject.TransfiniteIteration, function or constantWording
the inclusion iteration functor of x1 and J (from the name)
English
Let $x_{1}$ be an element of $\operatorname{SuccStruct}$ applied to $C$. Let $J$ be a set. Then the inclusion iteration functor of $x_{1}$ and $J$ is a homomorphism of the action of the constant of $J$ and $\mathrm{CategoryTheory\_\_SmallObject\_\_SuccStruct\_\_X\_u2080\_}$ applied to $x_{1}$ and the iteration functor of $x_{1}$ and $J$.
CategoryTheory.Functor.WellOrderInductionDatastructureMathlib.CategoryTheory.SmallObject.WellOrderInductionData, typeEnglish
Let $F$ be a functor of the set of opposites of $J$ and the set of sets. Then the elements of $\operatorname{WellOrderInductionData}$ applied to $F$ are a basic type.
CategoryTheory.Functor.WellOrderInductionData.ExtensionstructureMathlib.CategoryTheory.SmallObject.WellOrderInductionData, typeWording
extension of x3 and j (from the name)
English
Let $d$ be an element of $\operatorname{WellOrderInductionData}$ applied to $F$. Let $x_{3}$ be an element of the action of $F$ and $\operatorname{op}$ applied to the bottom. Let $j$ be an element of $J$. Then the extensions of $x_{3}$ and $j$ are a basic type.
CategoryTheory.Functor.WellOrderInductionData.Extension.limitdefMathlib.CategoryTheory.SmallObject.WellOrderInductionData, function or constantWording
the limit of j and e (from the name)
English
Let $j$ be an element of $J$ such that $j$ is a successor limit. Let $e$ be a function from elements $i$ of $J$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (i , j)$ to extensions of $x_{3}$ and $i$. Then the limit of $j$ and $i$ is an extension of $x_{3}$ and $j$.
CategoryTheory.Functor.WellOrderInductionData.Extension.ofLEdefMathlib.CategoryTheory.SmallObject.WellOrderInductionData, function or constantWording
the extension of e and hij (from the name)
English
Let $e$ be an extension of $x_{3}$ and $j$. Assume that $i \leq j$. Then the extension of $e$ and $\mathrm{hij}$ is an extension of $x_{3}$ and $i$.
CategoryTheory.Functor.WellOrderInductionData.Extension.succdefMathlib.CategoryTheory.SmallObject.WellOrderInductionData, function or constantWording
the successor of e and hj (from the name)
English
Let $e$ be an extension of $x_{3}$ and $j$. Assume that $j$ is not a maximum. Then the successor of $e$ and $\mathrm{hj}$ is an extension of $x_{3}$ and the successor of $j$.
CategoryTheory.Functor.WellOrderInductionData.Extension.valdefMathlib.CategoryTheory.SmallObject.WellOrderInductionData, function or constantWording
the value of self (from the name)
English
Let $\mathrm{self}$ be an extension of $x_{3}$ and $j$. Then the value of $\mathrm{self}$ is an element of the action of $F$ and $\operatorname{op}$ applied to $j$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Functor.WellOrderInductionData.Extension.zerodefMathlib.CategoryTheory.SmallObject.WellOrderInductionData, function or constantWording
the zero of d and x3 (from the name)
English
Let $d$ be an element of $\operatorname{WellOrderInductionData}$ applied to $F$. Let $x_{3}$ be an element of the action of $F$ and $\operatorname{op}$ applied to the bottom. Then the zero of $d$ and $x_{3}$ is an extension of $x_{3}$ and the bottom.
CategoryTheory.Functor.WellOrderInductionData.liftdefMathlib.CategoryTheory.SmallObject.WellOrderInductionData, function or constantWording
the lift of j and x2 (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{WellOrderInductionData}$ applied to $F$. Let $j$ be an element of $J$ such that $j$ is a successor limit. Let $x_{2}$ be an element of the section of the composition of the opposite of the functor of $\operatorname{monotone}$ applied to the value of the function that maps $x_{3}$ to $\MembershipmemMACRoT {\operatorname{Iio} (j)}{x_{3}}$ and $F$. Then the lift of $j$ and $x_{2}$ is an element of the action of $F$ and $\operatorname{op}$ applied to $j$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $j$, $\mathrm{hj}$ and $x_{2}$.
CategoryTheory.Functor.WellOrderInductionData.ofExistsdefMathlib.CategoryTheory.SmallObject.WellOrderInductionData, function or constantEnglish
Assume that for all elements $j_{1}$ of $J$, if $j_{1}$ is not a maximum, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of the map of $F$ and the opposite in the homomorphism of $\mathrm{Order\_\_le\_succ}$ applied to $j_{1}$. Assume that for all elements $j$ of $J$, if $j$ is a successor limit, then for all elements $x_{2}$ of the section of the composition of the opposite of the functor of $\operatorname{monotone}$ applied to the value of the function that maps $x_{3}$ to $\MembershipmemMACRoT {\operatorname{Iio} (j)}{x_{3}}$ and $F$, there exists an element $y$ of the action of $F$ and $\operatorname{op}$ applied to $j$, such that for all elements $i$ of $J$, for all elements $\mathrm{hi}$ of $\mathrm{Proof}$ applied to $\mathrm{Lt} (i , j)$, $\operatorname{hom}$ applied to the map of $F$ and the opposite in the homomorphism of $\operatorname{le}$ applied to $\mathrm{hi}$ and $y$ is equal to $\operatorname{op}$ applied to $i$. Then $\operatorname{ofExists}$ applied to $h$ and $h_{1}$ is an element of $\operatorname{WellOrderInductionData}$ applied to $F$.
CategoryTheory.Functor.WellOrderInductionData.sectionsMkdefMathlib.CategoryTheory.SmallObject.WellOrderInductionData, function or constantWording
the section of d and x3 (from the name)
English
Let $d$ be an element of $\operatorname{WellOrderInductionData}$ applied to $F$. Let $x_{3}$ be an element of the action of $F$ and $\operatorname{op}$ applied to the bottom. Then the section of $d$ and $x_{3}$ is an element of the section of $F$ defined as the function that maps $j$ to the value of $\operatorname{default}$.
CategoryTheory.Functor.WellOrderInductionData.succdefMathlib.CategoryTheory.SmallObject.WellOrderInductionData, function or constantWording
the successor of j and x2 (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{WellOrderInductionData}$ applied to $F$. Let $j$ be an element of $J$ such that $j$ is not a maximum. Let $x_{2}$ be an element of the action of $F$ and $\operatorname{op}$ applied to $j$. Then the successor of $j$ and $x_{2}$ is an element of the action of $F$ and $\operatorname{op}$ applied to the successor of $j$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $j$, $\mathrm{hj}$ and $x_{2}$.
CategoryTheory.CoreSmallCategoryOfSetstructureMathlib.CategoryTheory.SmallRepresentatives, typeWording
small category of set of x and C (from the name)
English
Let $x$ and $C$ be sets. Then the small categories of set of $x$ and $C$ are a basic type.
CategoryTheory.CoreSmallCategoryOfSet.arrowEquivdefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the arrow equivalence of h (from the name)
English
Let $h$ be a small category of set of $x$ and $C$. Then the arrow equivalence of $h$ is an equivalence from the set of arrows of the set of elements of the object of the small category of $h$ to the set of arrows of $C$.
CategoryTheory.CoreSmallCategoryOfSet.equivalencedefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the equivalence of h (from the name)
English
Let $h$ be a small category of set of $x$ and $C$. Then the equivalence of $h$ is an equivalence of the set of elements of the object of the small category of $h$ and $C$ defined as $\operatorname{asEquivalence}$ applied to the functor of $h$.
CategoryTheory.CoreSmallCategoryOfSet.fullyFaithfulFunctordefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the fully faithful functor of h (from the name)
English
generation took over the time limit
CategoryTheory.CoreSmallCategoryOfSet.functordefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the functor of h (from the name)
English
Let $h$ be a small category of set of $x$ and $C$. Then the functor of $h$ is a functor of the set of elements of the object of the small category of $h$ and $C$.
CategoryTheory.CoreSmallCategoryOfSet.homdefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the homomorphism of X and Y (from the name)
English
Let $\mathrm{self}$ be a small category of set of $x$ and $C$. Let $X$ and $Y$ be elements of the object of $\mathrm{self}$. Then the homomorphism of $X$ and $Y$ is an element of $\wp x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $X$ and $Y$.
CategoryTheory.CoreSmallCategoryOfSet.homEquivdefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the homomorphism equivalence of self (from the name)
English
Let $\mathrm{self}$ be a small category of set of $x$ and $C$. Then the homomorphism equivalence of $\mathrm{self}$ is an equivalence from the set of elements of the homomorphism of $X$ and $Y$ to the set of homomorphisms of $\operatorname{objEquiv}$ applied to $\mathrm{self}$ and $X$ and $\operatorname{objEquiv}$ applied to $\mathrm{self}$ and $Y$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.
CategoryTheory.CoreSmallCategoryOfSet.objdefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the object of self (from the name)
English
Let $\mathrm{self}$ be a small category of set of $x$ and $C$. Then the object of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.CoreSmallCategoryOfSet.objEquivdefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the object equivalence of self (from the name)
English
Let $\mathrm{self}$ be a small category of set of $x$ and $C$. Then the object equivalence of $\mathrm{self}$ is an equivalence from the set of elements of the object of $\mathrm{self}$ to $C$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSetdefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the small category of h (from the name)
English
Let $h$ be a small category of set of $x$ and $C$. Then the small category of $h$ is a small category of set of $x$.
CategoryTheory.SmallCategoryCardinalLTdefMathlib.CategoryTheory.SmallRepresentatives, typeEnglish
Let $x$ be a cardinal. Then an element of $\operatorname{SmallCategoryCardinalLT}$ applied to $x$ is an element of the function that maps $x$ to $\SubtypeSet {S}{\mathrm{HasCardinalLT} (\operatorname{Arrow} (\operatorname{Elem} (\operatorname{obj} (S))), x)}$.
CategoryTheory.SmallCategoryCardinalLT.categoryFamilydefMathlib.CategoryTheory.SmallRepresentatives, typeWording
category family of x and S (from the name)
English
Let $x$ be a cardinal. Let $S$ be an element of $\operatorname{SmallCategoryCardinalLT}$ applied to $x$. Then a category family of $x$ and $S$ is an element of the function that maps $x$ and $S$ to the set of elements of the object of $S$.
CategoryTheory.SmallCategoryOfSetstructureMathlib.CategoryTheory.SmallRepresentatives, typeWording
small category of set of x (from the name)
English
Let $x$ be a set. Then the small categories of set of $x$ are a basic type.
CategoryTheory.SmallCategoryOfSet.categoryFamilydefMathlib.CategoryTheory.SmallRepresentatives, typeWording
category family of x and x1 (from the name)
English
Let $x$ be a set. Let $x_{1}$ be a small category of set of $x$. Then a category family of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of elements of the object of $x_{1}$.
CategoryTheory.SmallCategoryOfSet.compdefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the composition of f and g (from the name)
English
Let $\mathrm{self}$ be a small category of set of $x$. Let $f$ be an element of the homomorphism of $X$ and $Y$. Let $g$ be an element of the homomorphism of $Y$ and $Z$. Then the composition of $f$ and $g$ is an element of the homomorphism of $X$ and $Z$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $f$ and $g$.
CategoryTheory.SmallCategoryOfSet.homdefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the homomorphism of X and Y (from the name)
English
Let $\mathrm{self}$ be a small category of set of $x$. Let $X$ and $Y$ be elements of the object of $\mathrm{self}$. Then the homomorphism of $X$ and $Y$ is an element of $\wp x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $X$ and $Y$.
CategoryTheory.SmallCategoryOfSet.iddefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the identity of self and X (from the name)
English
Let $\mathrm{self}$ be a small category of set of $x$. Let $X$ be an element of the object of $\mathrm{self}$. Then the identity of $\mathrm{self}$ and $X$ is an element of the homomorphism of $X$ and $X$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $X$.
CategoryTheory.SmallCategoryOfSet.objdefMathlib.CategoryTheory.SmallRepresentatives, function or constantWording
the object of self (from the name)
English
Let $\mathrm{self}$ be a small category of set of $x$. Then the object of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.