Definitions: Mathlib.CategoryTheory, part 21 of 25

CategoryTheory.Profunctor.associatordefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the associator of Q and R (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $Q$ be a profunctor of $D$ and $E$. Let $R$ be a profunctor of $E$ and $F$. Then the associator of $Q$ and $R$ is an isomorphism of the composition of the composition of $P$ and $Q$ and $R$ and the composition of $P$ and the composition of $Q$ and $R$.

CategoryTheory.Profunctor.associatorComponentsdefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the associator component of X and Y (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $Q$ be a profunctor of $D$ and $E$. Let $R$ be a profunctor of $E$ and $F$. Let $X$ be an element of $C$. Let $Y$ be an opposite of $F$. Then the associator component of $X$ and $Y$ is an isomorphism of the action of the action of the composition of the composition of $P$ and $Q$ and $R$ and $X$ and $Y$ and the action of the action of the composition of $P$ and the composition of $Q$ and $R$ and $X$ and $Y$.

CategoryTheory.Profunctor.associatorHomdefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the associator homomorphism of X and Y (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $Q$ be a profunctor of $D$ and $E$. Let $R$ be a profunctor of $E$ and $F$. Let $X$ be an element of $C$. Let $Y$ be an opposite of $F$. Then the associator homomorphism of $X$ and $Y$ is a homomorphism of the action of the action of the composition of the composition of $P$ and $Q$ and $R$ and $X$ and $Y$ and the action of the action of the composition of $P$ and the composition of $Q$ and $R$ and $X$ and $Y$.

CategoryTheory.Profunctor.associatorHomFundefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the associator homomorphism function of r and x4 (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $Q$ be a profunctor of $D$ and $E$. Let $R$ be a profunctor of $E$ and $F$. Let $X$ be an element of $C$. Let $Y$ be an opposite of $F$. Let $e$ be an element of $E$. Let $r$ be an element of the action of the action of $R$ and $e$ and $\operatorname{op}$ applied to the opposite of $Y$. Let $x_{4}$ be an element of $\Sigma$ applied to the function that maps $j_{1}$ to the action of the action of the composition diagram of $X$ and $e$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$. Then the associator homomorphism function of $r$ and $x_{4}$ is an element of $\Sigma$ applied to the function that maps $j$ to the action of the action of the composition diagram of $X$ and the opposite of $Y$ and $\operatorname{op}$ applied to $j$ and $j$.

CategoryTheory.Profunctor.associatorInvdefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the associator inverse of X and Y (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $Q$ be a profunctor of $D$ and $E$. Let $R$ be a profunctor of $E$ and $F$. Let $X$ be an element of $C$. Let $Y$ be an opposite of $F$. Then the associator inverse of $X$ and $Y$ is a homomorphism of the action of the action of the composition of $P$ and the composition of $Q$ and $R$ and $X$ and $Y$ and the action of the action of the composition of the composition of $P$ and $Q$ and $R$ and $X$ and $Y$.

CategoryTheory.Profunctor.associatorInvFundefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the associator inverse function of p and x4 (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $Q$ be a profunctor of $D$ and $E$. Let $R$ be a profunctor of $E$ and $F$. Let $X$ be an element of $C$. Let $Y$ be an opposite of $F$. Let $d$ be an element of $D$. Let $p$ be an element of the action of the action of $P$ and $X$ and $\operatorname{op}$ applied to $d$. Let $x_{4}$ be an element of $\Sigma$ applied to the function that maps $j_{1}$ to the action of the action of the composition diagram of $d$ and the opposite of $Y$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$. Then the associator inverse function of $p$ and $x_{4}$ is an element of $\Sigma$ applied to the function that maps $j$ to the action of the action of the composition diagram of $X$ and the opposite of $Y$ and $\operatorname{op}$ applied to $j$ and $j$.

CategoryTheory.Profunctor.compdefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the composition of P and Q (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $Q$ be a profunctor of $D$ and $E$. Then the composition of $P$ and $Q$ is a profunctor of $C$ and $E$ defined as the universal set composition of $P$ and $Q$.

CategoryTheory.Profunctor.compDiagramdefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the composition diagram of X and Y (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $Q$ be a profunctor of $D$ and $E$. Let $X$ be an element of $C$. Let $Y$ be an element of $E$. Then the composition diagram of $X$ and $Y$ is a functor of the set of opposites of $D$ and the set of functors of $D$ and the set of sets.

CategoryTheory.Profunctor.compDiagramMapdefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the composition diagram map of f and g (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $Q$ be a profunctor of $D$ and $E$. Let $f$ be a homomorphism of $X$ and $\mathrm{X'}$. Let $g$ be a homomorphism of $Y$ and $\mathrm{Y'}$. Then the composition diagram map of $f$ and $g$ is a homomorphism of the composition diagram of $X$ and $\mathrm{Y'}$ and the composition diagram of $\mathrm{X'}$ and $Y$.

CategoryTheory.Profunctor.leftUnitordefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the left unitor isomorphism of P (from the docstring)

English

Let $P$ be a profunctor of $C$ and $D$. Then the left unitor isomorphism of $P$ is an isomorphism of the composition of the identity and $P$ and $P$.

CategoryTheory.Profunctor.rightUnitordefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the right unitor isomorphism of P (from the docstring)

English

Let $P$ be a profunctor of $C$ and $D$. Then the right unitor isomorphism of $P$ is an isomorphism of the composition of $P$ and the identity and $P$.

CategoryTheory.Profunctor.univCompdefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the universal set composition of P and Q (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $Q$ be a profunctor of $D$ and $E$. Then the universal set composition of $P$ and $Q$ is a profunctor of $C$ and $E$.

CategoryTheory.Profunctor.whiskerLeftdefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the left whisker of P and f (from the name)

English

Let $P$ be a profunctor of $C$ and $D$. Let $f$ be a homomorphism of $Q$ and $R$. Then the left whisker of $P$ and $f$ is a homomorphism of the composition of $P$ and $Q$ and the composition of $P$ and $R$.

CategoryTheory.Profunctor.whiskerRightdefMathlib.CategoryTheory.Profunctor.Comp, function or constant

Wording

the right whisker of R and f (from the name)

English

Let $R$ be a profunctor of $D$ and $E$. Let $f$ be a homomorphism of $P$ and $Q$. Then the right whisker of $R$ and $f$ is a homomorphism of the composition of $P$ and $R$ and the composition of $Q$ and $R$.

Mathlib.CategoryTheory.Quotient

CategoryTheory.CongruenceclassMathlib.CategoryTheory.Quotient, predicate

Wording

r is a congruence (from the name)

English

Let $r$ be a homomorphism relation of $C$. Then we can say that $r$ is a congruence.

CategoryTheory.Functor.homReldefMathlib.CategoryTheory.Quotient, function or constant

Wording

the homomorphism relation of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the homomorphism relation of $F$ is a homomorphism relation of $C$ defined as the function that maps $x_{2}$, $x_{3}$, $f$ and $g$ to the proposition that the map of $F$ and $f$ is equal to the map of $F$ and $g$.

CategoryTheory.HomRel.CompClosureinductiveMathlib.CategoryTheory.Quotient, function or constant

Wording

the composition closure of r (from the name)

English

Let $r$ be a homomorphism relation of $C$. Then the composition closure of $r$ is a homomorphism relation of $C$.

CategoryTheory.HomRel.IsStableUnderPostcompclassMathlib.CategoryTheory.Quotient, predicate

Wording

r is stable under postcomposition (from the name)

English

Let $r$ be a homomorphism relation of $C$. Then we can say that $r$ is stable under postcomposition.

CategoryTheory.HomRel.IsStableUnderPrecompclassMathlib.CategoryTheory.Quotient, predicate

Wording

r is stable under precomposition (from the name)

English

Let $r$ be a homomorphism relation of $C$. Then we can say that $r$ is stable under precomposition.

CategoryTheory.QuotientstructureMathlib.CategoryTheory.Quotient, type

Wording

quotient of r (from the name)

English

Let $r$ be a homomorphism relation of $C$. Then the quotients of $r$ are a basic type.

CategoryTheory.Quotient.HomdefMathlib.CategoryTheory.Quotient, type

Wording

homomorphism of s and t (from the name)

English

Let $r$ be a homomorphism relation of $C$. Let $s$ and $t$ be quotients of $r$. Then a homomorphism of $s$ and $t$ is an element of the function that maps $r$, $s$ and $t$ to $\mathrm{Quot}$ applied to the composition closure of $r$.

CategoryTheory.Quotient.asdefMathlib.CategoryTheory.Quotient, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a quotient of $r$. Then $\operatorname{as}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Quotient.compdefMathlib.CategoryTheory.Quotient, function or constant

Wording

the composition of x1 and x2 (from the name)

English

Let $r$ be a homomorphism relation of $C$. Let $x_{1}$ be a homomorphism of $a$ and $b$. Let $x_{2}$ be a homomorphism of $b$ and $c$. Then the composition of $x_{1}$ and $x_{2}$ is a homomorphism of $a$ and $c$.

CategoryTheory.Quotient.equivdefMathlib.CategoryTheory.Quotient, function or constant

Wording

the equivalence of r (from the name)

English

Let $r$ be a homomorphism relation of $C$. Then the equivalence of $r$ is an equivalence from the set of quotients of $r$ to $C$.

CategoryTheory.Quotient.functordefMathlib.CategoryTheory.Quotient, function or constant

Wording

the functor of r (from the docstring)

English

Let $r$ be a homomorphism relation of $C$. Then the functor of $r$ is a functor of $C$ and the set of quotients of $r$.

CategoryTheory.Quotient.invdefMathlib.CategoryTheory.Quotient, function or constant

Wording

the inverse of r and f (from the name)

English

Let $r$ be a homomorphism relation of $G$. Let $f$ be a homomorphism of $X$ and $Y$. Then the inverse of $r$ and $f$ is a homomorphism of $Y$ and $X$.

CategoryTheory.Quotient.liftdefMathlib.CategoryTheory.Quotient, function or constant

Wording

the lift of r and F (from the name)

English

Let $r$ be a homomorphism relation of $C$. Let $F$ be a functor of $C$ and $D$ such that for all elements $x_{2}$ and $y$ of $C$, for all homomorphisms $x_{3}$ and $x_{4}$ of $x_{2}$ and $y$, if $r$ holds for $x_{2}$, $y$, $x_{3}$ and $x_{4}$, then the map of $F$ and $x_{3}$ is equal to the map of $F$ and $x_{4}$. Then the lift of $r$ and $F$ is a functor of the set of quotients of $r$ and $D$.

CategoryTheory.Quotient.lift.isLiftdefMathlib.CategoryTheory.Quotient, function or constant

Wording

no wording

English

Let $r$ be a homomorphism relation of $C$. Let $F$ be a functor of $C$ and $D$ such that for all elements $x_{2}$ and $y$ of $C$, for all homomorphisms $x_{3}$ and $x_{4}$ of $x_{2}$ and $y$, if $r$ holds for $x_{2}$, $y$, $x_{3}$ and $x_{4}$, then the map of $F$ and $x_{3}$ is equal to the map of $F$ and $x_{4}$. Then $\operatorname{isLift}$ applied to $r$, $F$ and $H$ is an isomorphism of the composition of the functor of $r$ and the lift of $r$ and $F$ and $F$.

CategoryTheory.Quotient.natIsoLiftdefMathlib.CategoryTheory.Quotient, function or constant

Wording

the natural isomorphism lift of r and x2 (from the name)

English

Let $r$ be a homomorphism relation of $C$. Let $x_{2}$ be an isomorphism of the composition of the functor of $r$ and $F$ and the composition of the functor of $r$ and $G$. Then the natural isomorphism lift of $r$ and $x_{2}$ is an isomorphism of $F$ and $G$.

CategoryTheory.Quotient.natTransLiftdefMathlib.CategoryTheory.Quotient, function or constant

Wording

the natural transformation lift of r and x2 (from the name)

English

Let $r$ be a homomorphism relation of $C$. Let $x_{2}$ be a homomorphism of the composition of the functor of $r$ and $F$ and the composition of the functor of $r$ and $G$. Then the natural transformation lift of $r$ and $x_{2}$ is a homomorphism of $F$ and $G$.

HomReldefMathlib.CategoryTheory.Quotient, type

Wording

homomorphism relation of C (from the name)

English

Let $C$ be a set. Then a homomorphism relation of $C$ is an element of the function that maps $C$ to the set of functions from elements $X$ of $C$ and elements $Y$ of $C$ and homomorphisms of $X$ and $Y$ and homomorphisms of $X$ and $Y$ to propositions.

Mathlib.CategoryTheory.Quotient.Preadditive

CategoryTheory.Quotient.Preadditive.adddefMathlib.CategoryTheory.Quotient.Preadditive, function or constant

Wording

the sum of f and g (from the name)

English

Let $r$ be a homomorphism relation of $C$ such that for all elements $X_{1}$ and $Y_{1}$ of $C$, for all homomorphisms $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ of $X_{1}$ and $Y_{1}$, if $r$ holds for $X_{1}$, $Y_{1}$, $x_{2}$ and $x_{3}$, then if $r$ holds for $X_{1}$, $Y_{1}$, $x_{4}$ and $x_{5}$, then $r$ holds for $X_{1}$, $Y_{1}$, $x_{2} + x_{4}$ and $x_{3} + x_{5}$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the sum of $f$ and $g$ is a homomorphism of $X$ and $Y$.

CategoryTheory.Quotient.Preadditive.negdefMathlib.CategoryTheory.Quotient.Preadditive, function or constant

Wording

the negation of r and f (from the name)

English

Let $r$ be a homomorphism relation of $C$ such that for all elements $X_{1}$ and $Y_{1}$ of $C$, for all homomorphisms $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ of $X_{1}$ and $Y_{1}$, if $r$ holds for $X_{1}$, $Y_{1}$, $x_{2}$ and $x_{3}$, then if $r$ holds for $X_{1}$, $Y_{1}$, $x_{4}$ and $x_{5}$, then $r$ holds for $X_{1}$, $Y_{1}$, $x_{2} + x_{4}$ and $x_{3} + x_{5}$. Let $f$ be a homomorphism of $X$ and $Y$. Then the negation of $r$ and $f$ is a homomorphism of $X$ and $Y$.

Mathlib.CategoryTheory.RegularCategory.Basic

CategoryTheory.RegularclassMathlib.CategoryTheory.RegularCategory.Basic, predicate

Wording

C is regular (from the name)

English

Let $C$ be a set. Then we can say that $C$ is regular.

CategoryTheory.Regular.frobeniusMorphismdefMathlib.CategoryTheory.RegularCategory.Basic, function or constant

Wording

the Frobenius morphism of #2 and #3 (from the name)

English

Let $f$ be a homomorphism of $A$ and $B$. Let $\mathrm{A'}$ be a subobject of $A$. Let $\mathrm{B'}$ be a subobject of $B$. Then the Frobenius morphism of $\mathrm{A'}$ and $\mathrm{B'}$ is a homomorphism of the action of $\operatorname{underlying}$ and the minimum of $\mathrm{A'}$ and the action of the pullback of $f$ and $\mathrm{B'}$ and the action of $\operatorname{underlying}$ and the minimum of the action of $\operatorname{exists}$ applied to $f$ and $\mathrm{A'}$ and $\mathrm{B'}$.

CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisationdefMathlib.CategoryTheory.RegularCategory.Basic, function or constant

Wording

the Frobenius strong epimorphism monomorphism factorisation of #2 and #3 (from the name)

English

Let $f$ be a homomorphism of $A$ and $B$. Let $\mathrm{A'}$ be a subobject of $A$. Let $\mathrm{B'}$ be a subobject of $B$. Then the Frobenius strong epimorphism monomorphism factorisation of $\mathrm{A'}$ and $\mathrm{B'}$ is a strong epimorphism monomorphism factorisation of the composition of the arrow of the minimum of $\mathrm{A'}$ and the action of the pullback of $f$ and $\mathrm{B'}$ and $f$.

CategoryTheory.Regular.regularEpiOfExtremalEpidefMathlib.CategoryTheory.RegularCategory.Basic, function or constant

Wording

the regular epimorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the regular epimorphism of $f$ is a regular epimorphism of $f$.

CategoryTheory.Regular.strongEpiMonoFactorisationdefMathlib.CategoryTheory.RegularCategory.Basic, function or constant

Wording

the strong epimorphism monomorphism factorisation of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the strong epimorphism monomorphism factorisation of $f$ is a strong epimorphism monomorphism factorisation of $f$.

Mathlib.CategoryTheory.RepresentedBy

CategoryTheory.Functor.IsRepresentedBystructureMathlib.CategoryTheory.RepresentedBy, predicate

Wording

no wording

English

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Let $x_{1}$ be an element of the action of $F$ and $\operatorname{op}$ applied to $X$. Then we can say that $\operatorname{IsRepresentedBy}$ holds for $F$ and $x_{1}$.

CategoryTheory.Functor.IsRepresentedBy.representableBydefMathlib.CategoryTheory.RepresentedBy, function or constant

Wording

the canonical representation induced by the universal element of h (from the docstring)

English

Assume that $\operatorname{IsRepresentedBy}$ holds for $F$ and $x_{1}$. Then the canonical representation induced by the universal element of $h$ is an element of $\operatorname{RepresentableBy}$ applied to $F$ and $X$ defined as $\operatorname{representableByUliftFunctorEquiv}$ applied to $\operatorname{symm}$ applied to the equivalence lift Yoneda isomorphism of the composition of $F$ and the functor embedding and $X$ and the lift Yoneda isomorphism of $h$.

CategoryTheory.Functor.IsRepresentedBy.uliftYonedaIsodefMathlib.CategoryTheory.RepresentedBy, function or constant

Wording

the lift Yoneda isomorphism of h (from the name)

English

Assume that $\operatorname{IsRepresentedBy}$ holds for $F$ and $x_{1}$. Then the lift Yoneda isomorphism of $h$ is an isomorphism of the action of the lift Yoneda and $X$ and the composition of $F$ and the functor embedding defined as $\operatorname{asIso}$ applied to $\operatorname{symm}$ applied to the lift Yoneda equivalence and $\operatorname{up}$ applied to $x_{1}$.

Mathlib.CategoryTheory.Retract

CategoryTheory.Iso.retractdefMathlib.CategoryTheory.Retract, function or constant

Wording

the retract of e (from the name)

English

Let $e$ be an isomorphism of $X$ and $Y$. Then the retract of $e$ is a retract of $X$ and $Y$.

CategoryTheory.NatTrans.retractArrowAppdefMathlib.CategoryTheory.Retract, function or constant

Wording

the retract arrow application of x2 and h (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $h$ be a retract of $X$ and $Y$. Then the retract arrow application of $x_{2}$ and $h$ is a retract arrow of the component of $x_{2}$ and $X$ and the component of $x_{2}$ and $Y$.

CategoryTheory.RetractstructureMathlib.CategoryTheory.Retract, type

Wording

retract of X and Y (from the name)

English

Let $X$ and $Y$ be elements of $C$. Then the retracts of $X$ and $Y$ are a basic type.

CategoryTheory.Retract.idefMathlib.CategoryTheory.Retract, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a retract of $X$ and $Y$. Then $\operatorname{i}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Retract.mapdefMathlib.CategoryTheory.Retract, function or constant

Wording

the map of h and F (from the name)

English

Let $h$ be a retract of $X$ and $Y$. Let $F$ be a functor of $C$ and $D$. Then the map of $h$ and $F$ is a retract of the action of $F$ and $X$ and the action of $F$ and $Y$.

CategoryTheory.Retract.ofIsodefMathlib.CategoryTheory.Retract, function or constant

Wording

the retract of e (from the name)

English

Let $e$ be an isomorphism of $X$ and $Y$. Then the retract of $e$ is a retract of $X$ and $Y$.

CategoryTheory.Retract.opdefMathlib.CategoryTheory.Retract, function or constant

Wording

the opposite of h (from the name)

English

Let $h$ be a retract of $X$ and $Y$. Then the opposite of $h$ is a retract of $\operatorname{op}$ applied to $X$ and $\operatorname{op}$ applied to $Y$.

CategoryTheory.Retract.rdefMathlib.CategoryTheory.Retract, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a retract of $X$ and $Y$. Then $\operatorname{r}$ applied to $\mathrm{self}$ is a homomorphism of $Y$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Retract.refldefMathlib.CategoryTheory.Retract, function or constant

Wording

the identity of X (from the name)

English

Let $X$ be an element of $C$. Then the identity of $X$ is a retract of $X$ and $X$.

CategoryTheory.Retract.splitEpidefMathlib.CategoryTheory.Retract, function or constant

Wording

the split epimorphism of h (from the name)

English

Let $h$ be a retract of $X$ and $Y$. Then the split epimorphism of $h$ is a split epimorphism of $\operatorname{r}$ applied to $h$.

CategoryTheory.Retract.splitMonodefMathlib.CategoryTheory.Retract, function or constant

Wording

the split monomorphism of h (from the name)

English

Let $h$ be a retract of $X$ and $Y$. Then the split monomorphism of $h$ is a split monomorphism of $\operatorname{i}$ applied to $h$.

CategoryTheory.Retract.transdefMathlib.CategoryTheory.Retract, function or constant

Wording

the composition of h and #2 (from the name)

English

Let $h$ be a retract of $X$ and $Y$. Let $\mathrm{h'}$ be a retract of $Y$ and $Z$. Then the composition of $h$ and $\mathrm{h'}$ is a retract of $X$ and $Z$.

CategoryTheory.RetractArrowdefMathlib.CategoryTheory.Retract, type

Wording

retract arrow of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Z$ and $W$. Then a retract arrow of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of retracts of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$.

CategoryTheory.RetractArrow.leftdefMathlib.CategoryTheory.Retract, function or constant

Wording

the left of h (from the name)

English

Let $h$ be a retract arrow of $f$ and $g$. Then the left of $h$ is a retract of $X$ and $Z$ defined as the map of $h$ and the left function.

CategoryTheory.RetractArrow.mapdefMathlib.CategoryTheory.Retract, function or constant

Wording

the map of h and F (from the name)

English

Let $h$ be a retract arrow of $f$ and $g$. Let $F$ be a functor of $C$ and $D$. Then the map of $h$ and $F$ is a retract arrow of the map of $F$ and $f$ and the map of $F$ and $g$ defined as the map of $h$ and the map arrow of $F$.

CategoryTheory.RetractArrow.opdefMathlib.CategoryTheory.Retract, function or constant

Wording

the opposite of h (from the name)

English

Let $h$ be a retract arrow of $f$ and $g$. Then the opposite of $h$ is a retract arrow of the opposite in $f$ and the opposite in $g$.

CategoryTheory.RetractArrow.rightdefMathlib.CategoryTheory.Retract, function or constant

Wording

the right of h (from the name)

English

Let $h$ be a retract arrow of $f$ and $g$. Then the right of $h$ is a retract of $X$ and $Z$ defined as the map of $h$ and the right function.

CategoryTheory.RetractArrow.unopdefMathlib.CategoryTheory.Retract, function or constant

Wording

the opposite of h (from the name)

English

Let $h$ be a retract arrow of $f$ and $g$. Then the opposite of $h$ is a retract arrow of the opposite of $f$ and the opposite of $g$.

Mathlib.CategoryTheory.Shift.Adjunction

CategoryTheory.Adjunction.CommShiftclassMathlib.CategoryTheory.Shift.Adjunction, predicate

Wording

adj is a commutative shift (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $A$ be a set. Then we can say that $\mathrm{adj}$ is a commutative shift.

CategoryTheory.Adjunction.CommShift.CompatibilityCounitdefMathlib.CategoryTheory.Shift.Adjunction, predicate

Wording

no wording

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $x_{5}$ be an isomorphism of the composition of the shift functor of $C$ and $a$ and $F$ and the composition of $F$ and the shift functor of $D$ and $a$. Let $x_{6}$ be an isomorphism of the composition of the shift functor of $D$ and $a$ and $G$ and the composition of $G$ and the shift functor of $C$ and $a$. Then $\operatorname{CompatibilityCounit}$ holds for $\mathrm{adj}$, $x_{5}$ and $x_{6}$, if for all elements $Y$ of $D$, the component of the counit of $\mathrm{adj}$ and the action of the shift functor of $D$ and $a$ and $Y$ is equal to the composition of the map of $F$ and the component of the homomorphism of $x_{6}$ and $Y$ and the composition of the component of the homomorphism of $x_{5}$ and the action of $G$ and $Y$ and the map of the shift functor of $D$ and $a$ and the component of the counit of $\mathrm{adj}$ and $Y$.

CategoryTheory.Adjunction.CommShift.CompatibilityUnitdefMathlib.CategoryTheory.Shift.Adjunction, predicate

Wording

no wording

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $x_{5}$ be an isomorphism of the composition of the shift functor of $C$ and $a$ and $F$ and the composition of $F$ and the shift functor of $D$ and $a$. Let $x_{6}$ be an isomorphism of the composition of the shift functor of $D$ and $a$ and $G$ and the composition of $G$ and the shift functor of $C$ and $a$. Then $\operatorname{CompatibilityUnit}$ holds for $\mathrm{adj}$, $x_{5}$ and $x_{6}$, if for all elements $X$ of $C$, the map of the shift functor of $C$ and $a$ and the component of the unit of $\mathrm{adj}$ and $X$ is equal to the composition of the component of the unit of $\mathrm{adj}$ and the action of the shift functor of $C$ and $a$ and $X$ and the composition of the map of $G$ and the component of the homomorphism of $x_{5}$ and $X$ and the component of the homomorphism of $x_{6}$ and the action of $F$ and $X$.

CategoryTheory.Adjunction.LeftAdjointCommShift.isodefMathlib.CategoryTheory.Shift.Adjunction, function or constant

Wording

the isomorphism of adj and a (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $a$ be an element of $A$. Then the isomorphism of $\mathrm{adj}$ and $a$ is an isomorphism of the composition of the shift functor of $C$ and $a$ and $F$ and the composition of $F$ and the shift functor of $D$ and $a$ defined as $\operatorname{iso'}$ applied to $\mathrm{adj}$, $a$, $\operatorname{neg}$ applied to $a$ and $\mathrm{add\_neg\_cancel}$ applied to $a$.

CategoryTheory.Adjunction.RightAdjointCommShift.isodefMathlib.CategoryTheory.Shift.Adjunction, function or constant

Wording

the isomorphism of adj and a (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $a$ be an element of $A$. Then the isomorphism of $\mathrm{adj}$ and $a$ is an isomorphism of the composition of the shift functor of $D$ and $a$ and $G$ and the composition of $G$ and the shift functor of $C$ and $a$ defined as $\operatorname{iso'}$ applied to $\mathrm{adj}$, $a$, $\operatorname{neg}$ applied to $a$ and $\mathrm{neg\_add\_cancel}$ applied to $a$.

CategoryTheory.Equivalence.CommShiftdefMathlib.CategoryTheory.Shift.Adjunction, predicate

Wording

E is a commutative shift (from the name)

English

Let $E$ be an equivalence of $C$ and $D$. Let $A$ be a set. Then $E$ is a commutative shift, if the adjunction of $E$ is a commutative shift.

Mathlib.CategoryTheory.Shift.Basic

CategoryTheory.HasShiftclassMathlib.CategoryTheory.Shift.Basic, predicate

Wording

no wording

English

Let $C$ and $A$ be sets. Then we can say that $\operatorname{HasShift}$ holds for $C$ and $A$.

CategoryTheory.HasShift.shiftdefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift (from the name)

English

The shift is a functor of $\operatorname{Discrete}$ applied to $A$ and the set of functors of $C$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.ShiftMkCorestructureMathlib.CategoryTheory.Shift.Basic, type

Wording

shift of C and A (from the name)

English

Let $C$ and $A$ be sets. Then the shifts of $C$ and $A$ are a basic type.

CategoryTheory.ShiftMkCore.FdefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a shift of $C$ and $A$. Let $x_{2}$ be an element of $A$. Then $\operatorname{F}$ applied to $\mathrm{self}$ and $x_{2}$ is a functor of $C$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

CategoryTheory.ShiftMkCore.adddefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the sum of n and m (from the name)

English

Let $\mathrm{self}$ be a shift of $C$ and $A$. Let $n$ and $m$ be elements of $A$. Then the sum of $n$ and $m$ is an isomorphism of $\operatorname{F}$ applied to $\mathrm{self}$ and $n + m$ and the composition of $\operatorname{F}$ applied to $\mathrm{self}$ and $n$ and $\operatorname{F}$ applied to $\mathrm{self}$ and $m$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $n$ and $m$.

CategoryTheory.ShiftMkCore.zerodefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the zero of self (from the name)

English

Let $\mathrm{self}$ be a shift of $C$ and $A$. Then the zero of $\mathrm{self}$ is an isomorphism of $\operatorname{F}$ applied to $\mathrm{self}$ and $0$ and the identity of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.shiftAdddefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift sum of i and j (from the name)

English

Let $X$ be an element of $C$. Let $i$ and $j$ be elements of $A$. Then the shift sum of $i$ and $j$ is an isomorphism of the action of the shift functor of $C$ and $i + j$ and $X$ and the action of the shift functor of $C$ and $j$ and the action of the shift functor of $C$ and $i$ and $X$ defined as the application of the shift functor sum of $i$ and $j$ and $X$.

CategoryTheory.shiftCommdefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Let $i$ and $j$ be elements of $A$. Then $\operatorname{shiftComm}$ applied to $X$, $i$ and $j$ is an isomorphism of the action of the shift functor of $C$ and $j$ and the action of the shift functor of $C$ and $i$ and $X$ and the action of the shift functor of $C$ and $i$ and the action of the shift functor of $C$ and $j$ and $X$ defined as the application of $\operatorname{shiftFunctorComm}$ applied to $C$, $i$ and $j$ and $X$.

CategoryTheory.shiftEquivdefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift equivalence of C and n (from the name)

English

Let $C$ be a set. Let $n$ be an element of $A$. Then the shift equivalence of $C$ and $n$ is an equivalence of $C$ and $C$ defined as the shift equivalence of $n$ and $\operatorname{neg}$ applied to $n$.

CategoryTheory.shiftEquiv'defMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift equivalence of i and j (from the name)

English

Let $C$ be a set. Let $i$ and $j$ be elements of $A$ such that $\EqtMACRoH {i + j}{0}$. Then the shift equivalence of $i$ and $j$ is an equivalence of $C$ and $C$.

CategoryTheory.shiftFunctordefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift functor of C and i (from the name)

English

Let $C$ be a set. Let $i$ be an element of $A$. Then the shift functor of $C$ and $i$ is a functor of $C$ and $C$ defined as the action of the shift monoidal functor of $C$ and $A$ and $\operatorname{mk}$ applied to $i$.

CategoryTheory.shiftFunctorAdddefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift functor sum of i and j (from the name)

English

Let $C$ be a set. Let $i$ and $j$ be elements of $A$. Then the shift functor sum of $i$ and $j$ is an isomorphism of the shift functor of $C$ and $i + j$ and the composition of the shift functor of $C$ and $i$ and the shift functor of $C$ and $j$ defined as the inverse of the isomorphism of $\operatorname{mk}$ applied to $i$ and $\operatorname{mk}$ applied to $j$.

CategoryTheory.shiftFunctorAdd'defMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift functor sum of j and k (from the name)

English

Let $C$ be a set. Let $i$, $j$ and $k$ be elements of $A$ such that $\EqtMACRoH {i + j}{k}$. Then the shift functor sum of $j$ and $k$ is an isomorphism of the shift functor of $C$ and $k$ and the composition of the shift functor of $C$ and $i$ and the shift functor of $C$ and $j$.

CategoryTheory.shiftFunctorCommdefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

no wording

English

Let $C$ be a set. Let $i$ and $j$ be elements of $A$. Then $\operatorname{shiftFunctorComm}$ applied to $C$, $i$ and $j$ is an isomorphism of the composition of the shift functor of $C$ and $i$ and the shift functor of $C$ and $j$ and the composition of the shift functor of $C$ and $j$ and the shift functor of $C$ and $i$.

CategoryTheory.shiftFunctorCompIsoIddefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift functor composition isomorphism identity of i and j (from the name)

English

Let $C$ be a set. Let $i$ and $j$ be elements of $A$ such that $\EqtMACRoH {i + j}{0}$. Then the shift functor composition isomorphism identity of $i$ and $j$ is an isomorphism of the composition of the shift functor of $C$ and $i$ and the shift functor of $C$ and $j$ and the identity of $C$ defined as the composition of the inverse of the shift functor sum of $j$ and $0$ and the shift functor zero of $C$ and $A$.

CategoryTheory.shiftFunctorZerodefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift functor zero of C and A (from the name)

English

Let $C$ and $A$ be sets. Then the shift functor zero of $C$ and $A$ is an isomorphism of the shift functor of $C$ and $0$ and the identity of $C$ defined as the inverse of the isomorphism of the shift monoidal functor of $C$ and $A$.

CategoryTheory.shiftFunctorZero'defMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift functor zero of a (from the name)

English

Let $C$ be a set. Let $a$ be an element of $A$ such that $\EqtMACRoH {a}{0}$. Then the shift functor zero of $a$ is an isomorphism of the shift functor of $C$ and $a$ and the identity of $C$.

CategoryTheory.shiftMonoidalFunctordefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift monoidal functor of C and A (from the name)

English

Let $C$ and $A$ be sets. Then the shift monoidal functor of $C$ and $A$ is a functor of $\operatorname{Discrete}$ applied to $A$ and the set of functors of $C$ and $C$ defined as the shift.

CategoryTheory.shiftNegShiftdefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift negation shift of X and i (from the name)

English

Let $X$ be an element of $C$. Let $i$ be an element of $A$. Then the shift negation shift of $X$ and $i$ is an isomorphism of the action of the shift functor of $C$ and $i$ and the action of the shift functor of $C$ and $\operatorname{neg}$ applied to $i$ and $X$ and $X$ defined as the application of the counit isomorphism of the shift equivalence of $C$ and $i$ and $X$.

CategoryTheory.shiftShiftNegdefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift shift negation of X and i (from the name)

English

Let $X$ be an element of $C$. Let $i$ be an element of $A$. Then the shift shift negation of $X$ and $i$ is an isomorphism of the action of the shift functor of $C$ and $\operatorname{neg}$ applied to $i$ and the action of the shift functor of $C$ and $i$ and $X$ and $X$ defined as the application of the inverse of the unit isomorphism of the shift equivalence of $C$ and $i$ and $X$.

CategoryTheory.shiftZerodefMathlib.CategoryTheory.Shift.Basic, function or constant

Wording

the shift zero of A and X (from the name)

English

Let $A$ be a set. Let $X$ be an element of $C$. Then the shift zero of $A$ and $X$ is an isomorphism of the action of the shift functor of $C$ and $0$ and $X$ and $X$ defined as the application of the shift functor zero of $C$ and $A$ and $X$.

Mathlib.CategoryTheory.Shift.CommShift

CategoryTheory.Functor.CommShiftclassMathlib.CategoryTheory.Shift.CommShift, predicate

Wording

F is a commutative shift (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $A$ be a set. Then we can say that $F$ is a commutative shift.

CategoryTheory.Functor.CommShift.commShiftIsodefMathlib.CategoryTheory.Shift.CommShift, function or constant

Wording

the commutative shift isomorphism of F and a (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $a$ be an element of $A$. Then the commutative shift isomorphism of $F$ and $a$ is an isomorphism of the composition of the shift functor of $C$ and $a$ and $F$ and the composition of $F$ and the shift functor of $D$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

CategoryTheory.Functor.CommShift.isoAdddefMathlib.CategoryTheory.Shift.CommShift, function or constant

Wording

the isomorphism sum of x5 and x6 (from the name)

English

Let $x_{5}$ be an isomorphism of the composition of the shift functor of $C$ and $a$ and $F$ and the composition of $F$ and the shift functor of $D$ and $a$. Let $x_{6}$ be an isomorphism of the composition of the shift functor of $C$ and $b$ and $F$ and the composition of $F$ and the shift functor of $D$ and $b$. Then the isomorphism sum of $x_{5}$ and $x_{6}$ is an isomorphism of the composition of the shift functor of $C$ and $a + b$ and $F$ and the composition of $F$ and the shift functor of $D$ and $a + b$.

CategoryTheory.Functor.CommShift.isoAdd'defMathlib.CategoryTheory.Shift.CommShift, function or constant

Wording

the isomorphism sum of x5 and x6 (from the name)

English

Assume that $\EqtMACRoH {a + b}{c}$. Let $x_{5}$ be an isomorphism of the composition of the shift functor of $C$ and $a$ and $F$ and the composition of $F$ and the shift functor of $D$ and $a$. Let $x_{6}$ be an isomorphism of the composition of the shift functor of $C$ and $b$ and $F$ and the composition of $F$ and the shift functor of $D$ and $b$. Then the isomorphism sum of $x_{5}$ and $x_{6}$ is an isomorphism of the composition of the shift functor of $C$ and $c$ and $F$ and the composition of $F$ and the shift functor of $D$ and $c$ defined as the composition of the right isomorphism whisker of the shift functor sum of $b$ and $c$ and $F$ and the composition of the associator of the shift functor of $C$ and $b$ and $F$ and the composition of the left isomorphism whisker of the shift functor of $C$ and $a$ and $x_{6}$ and the composition of the inverse of the associator of $F$ and the shift functor of $D$ and $b$ and the composition of the right isomorphism whisker of $x_{5}$ and the shift functor of $D$ and $b$ and the composition of the associator of the shift functor of $D$ and $a$ and the shift functor of $D$ and $b$ and the left isomorphism whisker of $F$ and the inverse of the shift functor sum of $b$ and $c$.

CategoryTheory.Functor.CommShift.isoZerodefMathlib.CategoryTheory.Shift.CommShift, function or constant

Wording

the isomorphism zero of F and A (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $A$ be a set. Then the isomorphism zero of $F$ and $A$ is an isomorphism of the composition of the shift functor of $C$ and $0$ and $F$ and the composition of $F$ and the shift functor of $D$ and $0$ defined as the composition of the right isomorphism whisker of the shift functor zero of $C$ and $A$ and $F$ and the composition of the left unitor of $F$ and the composition of the inverse of the right unitor of $F$ and the left isomorphism whisker of $F$ and the inverse of the shift functor zero of $D$ and $A$.

CategoryTheory.Functor.CommShift.isoZero'defMathlib.CategoryTheory.Shift.CommShift, function or constant

Wording

the isomorphism zero of F and a (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $A$ be a set. Let $a$ be an element of $A$ such that $\EqtMACRoH {a}{0}$. Then the isomorphism zero of $F$ and $a$ is an isomorphism of the composition of the shift functor of $C$ and $a$ and $F$ and the composition of $F$ and the shift functor of $D$ and $a$ defined as the composition of the right isomorphism whisker of the shift functor zero of $a$ and $F$ and the composition of the left unitor of $F$ and the composition of the inverse of the right unitor of $F$ and the left isomorphism whisker of $F$ and the inverse of the shift functor zero of $a$.

CategoryTheory.NatTrans.CommShiftclassMathlib.CategoryTheory.Shift.CommShift, predicate

Wording

x4 is a commutative shift (from the name)

English

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $A$ be a set. Then we can say that $x_{4}$ is a commutative shift.

Mathlib.CategoryTheory.Shift.CommShiftTwo

CategoryTheory.CommShift₂SetupstructureMathlib.CategoryTheory.Shift.CommShiftTwo, type

Wording

commutative shift setup of D and M (from the name)

English

Let $D$ and $M$ be sets. Then the commutative shift setups of $D$ and $M$ are a basic type.

CategoryTheory.CommShift₂Setup.intdefMathlib.CategoryTheory.Shift.CommShiftTwo, function or constant

Wording

the integer (from the name)

English

The integer is a commutative shift setup of $D$ and $\Integer$.

CategoryTheory.CommShift₂Setup.εdefMathlib.CategoryTheory.Shift.CommShiftTwo, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a commutative shift setup of $D$ and $M$. Let $m$ and $n$ be elements of $M$. Then $\mathrm{CategoryTheory\_\_CommShift\_u2082\_Setup\_\_\_u3b5\_}$ applied to $\mathrm{self}$, $m$ and $n$ is a unit of the set of category centers of $D$ defined as $\mathrm{CategoryTheory\_\_CommShift\_u2082\_Setup\_\_proj3}$ applied to $\mathrm{self}$, $m$ and $n$.

CategoryTheory.Functor.CommShift₂classMathlib.CategoryTheory.Shift.CommShiftTwo, predicate

Wording

no wording

English

Let $G$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $h$ be a commutative shift setup of $D$ and $M$. Then we can say that $\mathrm{CategoryTheory\_\_Functor\_\_CommShift\_u2082\_}$ holds for $G$ and $h$.

CategoryTheory.Functor.CommShift₂IntdefMathlib.CategoryTheory.Shift.CommShiftTwo, type

Wording

commutative shift integer of G (from the name)

English

Let $G$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Then a commutative shift integer of $G$ is an element of the function that maps $G$ to $\mathrm{CategoryTheory\_\_Functor\_\_CommShift\_u2082\_}$ applied to $G$ and the integer.

CategoryTheory.NatTrans.CommShift₂classMathlib.CategoryTheory.Shift.CommShiftTwo, predicate

Wording

no wording

English

Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{10}$. Let $h$ be a commutative shift setup of $D$ and $M$. Then we can say that $\mathrm{CategoryTheory\_\_NatTrans\_\_CommShift\_u2082\_}$ holds for $x_{11}$ and $h$.

CategoryTheory.NatTrans.CommShift₂IntdefMathlib.CategoryTheory.Shift.CommShiftTwo, predicate

Wording

x13 is a commutative shift integer (from the name)

English

Let $x_{13}$ be a homomorphism of $x_{9}$ and $x_{10}$. Then $x_{13}$ is a commutative shift integer, if $\mathrm{CategoryTheory\_\_NatTrans\_\_CommShift\_u2082\_}$ holds for $x_{13}$ and the integer.

Mathlib.CategoryTheory.Shift.Induced

CategoryTheory.HasShift.Induced.adddefMathlib.CategoryTheory.Shift.Induced, function or constant

Wording

the sum of a1 and a (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $s$ be a function from elements of $A$ to functors of $D$ and $D$. Let $i$ be a function from elements $a_{1}$ of $A$ to isomorphisms of the composition of $F$ and $s$ applied to $a_{1}$ and the composition of the shift functor of $C$ and $a_{1}$ and $F$. Let $a$ and $b$ be elements of $A$. Then the sum of $i$ and $a$ is an isomorphism of $s$ applied to $a + b$ and the composition of $s$ applied to $a$ and $s$ applied to $b$ defined as the function that maps $b$ to the preimage isomorphism of the action of the left whiskering of $D$ and $D$ and $F$ and the composition of $a_{1}$ applied to $i + a$ and the composition of the right isomorphism whisker of the shift functor sum of $i$ and $a$ and $F$ and the composition of the associator of the shift functor of $C$ and $a$ and $F$ and the composition of the left isomorphism whisker of the shift functor of $C$ and $i$ and the inverse of $a_{1}$ applied to $a$ and the composition of the inverse of the associator of $F$ and $s$ applied to $a$ and the composition of the right isomorphism whisker of the inverse of $a_{1}$ applied to $i$ and $s$ applied to $a$ and the associator of $s$ applied to $i$ and $s$ applied to $a$.

CategoryTheory.HasShift.Induced.zerodefMathlib.CategoryTheory.Shift.Induced, function or constant

Wording

the zero of s and i (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $s$ be a function from elements of $A$ to functors of $D$ and $D$. Let $i$ be a function from elements $a$ of $A$ to isomorphisms of the composition of $F$ and $s$ applied to $a$ and the composition of the shift functor of $C$ and $a$ and $F$. Then the zero of $s$ and $a$ is an isomorphism of $s$ applied to $0$ and the identity of $D$ defined as the function that maps $i$ to the preimage isomorphism of the action of the left whiskering of $D$ and $D$ and $F$ and the composition of $a$ applied to $0$ and the composition of the right isomorphism whisker of the shift functor zero of $C$ and $A$ and $F$ and the composition of the left unitor of $F$ and the inverse of the right unitor of $F$.

Mathlib.CategoryTheory.Shift.InducedShiftSequence

CategoryTheory.Functor.ShiftSequence.induced.isoZerodefMathlib.CategoryTheory.Shift.InducedShiftSequence, function or constant

Wording

the isomorphism zero of m and #4 (from the name)

English

Let $e$ be an isomorphism of the composition of $L$ and $F$ and $G$. Let $M$ be a set. Let $\mathrm{F'}$ be a function from elements of $M$ to functors of $D$ and $A$. Let $\mathrm{e'}$ be a function from elements $m$ of $M$ to isomorphisms of the composition of $L$ and $\mathrm{F'}$ applied to $m$ and the shift of $G$ and $m$. Then the isomorphism zero of $\mathrm{F'}$ and $m$ is an isomorphism of $\mathrm{F'}$ applied to $0$ and $F$ defined as the function that maps $\mathrm{e'}$ to the preimage isomorphism of the action of the left whiskering of $D$ and $A$ and $L$ and the composition of $m$ applied to $0$ and the composition of the canonical isomorphism of $G$ and $M$ and the inverse of $e$.

CategoryTheory.Functor.ShiftSequence.induced.shiftIsodefMathlib.CategoryTheory.Shift.InducedShiftSequence, function or constant

Wording

the shift isomorphism of #7 and #8 (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $G$ be a functor of $C$ and $A$. Let $M$ be a set. Let $\mathrm{F'}$ be a function from elements of $M$ to functors of $D$ and $A$. Let $\mathrm{e'}$ be a function from elements $m$ of $M$ to isomorphisms of the composition of $L$ and $\mathrm{F'}$ applied to $m$ and the shift of $G$ and $m$. Let $n$, $a$ and $\mathrm{a'}$ be elements of $M$ such that $\EqtMACRoH {n + a}{\mathrm{a'}}$. Then the shift isomorphism of $n$ and $a$ is an isomorphism of the composition of the shift functor of $D$ and $n$ and $\mathrm{F'}$ applied to $a$ and $\mathrm{F'}$ applied to $\mathrm{a'}$ defined as the function that maps $\mathrm{ha'}$ to the preimage isomorphism of the action of the left whiskering of $D$ and $A$ and $L$ and the composition of the inverse of the associator of the shift functor of $D$ and $\mathrm{e'}$ and $\mathrm{F'}$ applied to $n$ and the composition of the right isomorphism whisker of the inverse of the commutative shift isomorphism of $L$ and $\mathrm{e'}$ and $\mathrm{F'}$ applied to $n$ and the composition of the associator of $L$ and $\mathrm{F'}$ applied to $n$ and the composition of the left isomorphism whisker of the shift functor of $C$ and $\mathrm{e'}$ and $m$ applied to $n$ and the composition of the shift isomorphism of $n$ and $a$ and the inverse of $m$ applied to $a$.

Mathlib.CategoryTheory.Shift.Localization

CategoryTheory.MorphismProperty.IsCompatibleWithShiftclassMathlib.CategoryTheory.Shift.Localization, predicate

Wording

W is compatible with shift (from the name)

English

Let $W$ be a morphism property of $C$. Let $A$ be a set. Then we can say that $W$ is compatible with shift.

CategoryTheory.MorphismProperty.shiftLocalizerMorphismdefMathlib.CategoryTheory.Shift.Localization, function or constant

Wording

the shift localizer morphism of W and a (from the name)

English

Let $W$ be a morphism property of $C$. Let $a$ be an element of $A$. Then the shift localizer morphism of $W$ and $a$ is a localizer morphism of $W$ and $W$.

Mathlib.CategoryTheory.Shift.Opposite

CategoryTheory.HasShift.mkShiftCoreOpdefMathlib.CategoryTheory.Shift.Opposite, function or constant

Wording

the shift opposite of C and A (from the name)

English

Let $C$ and $A$ be sets. Then the shift opposite of $C$ and $A$ is a shift of the set of opposites of $C$ and $A$.

CategoryTheory.NatTrans.OppositeShift.natIsoCompdefMathlib.CategoryTheory.Shift.Opposite, function or constant

Wording

the natural isomorphism composition of F and G (from the name)

English

Let $A$ be a set. Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the natural isomorphism composition of $F$ and $G$ is an isomorphism of the functor of $A$ and the composition of $F$ and $G$ and the composition of the functor of $A$ and $F$ and the functor of $A$ and $G$ defined as the identity of the functor of $A$ and the composition of $F$ and $G$.

CategoryTheory.NatTrans.OppositeShift.natIsoIddefMathlib.CategoryTheory.Shift.Opposite, function or constant

Wording

the natural isomorphism identity of C and A (from the name)

English

Let $C$ and $A$ be sets. Then the natural isomorphism identity of $C$ and $A$ is an isomorphism of the identity of the set of opposite shifts of $C$ and $A$ and the functor of $A$ and the identity of $C$ defined as the identity of the identity of the set of opposite shifts of $C$ and $A$.

CategoryTheory.OppositeShiftdefMathlib.CategoryTheory.Shift.Opposite, type

Wording

opposite shift of C and A (from the name)

English

Let $C$ and $A$ be sets. Then an opposite shift of $C$ and $A$ is an element of the function that maps $C$ and $A$ to the set of opposites of $C$.

CategoryTheory.OppositeShift.adjunctiondefMathlib.CategoryTheory.Shift.Opposite, function or constant

Wording

the adjunction of A and adj (from the name)

English

Let $A$ be a set. Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the adjunction of $A$ and $\mathrm{adj}$ is an adjunction of the functor of $A$ and $G$ and the functor of $A$ and $F$.

CategoryTheory.OppositeShift.functordefMathlib.CategoryTheory.Shift.Opposite, function or constant

Wording

the functor of A and F (from the docstring)

English

Let $A$ be a set. Let $F$ be a functor of $C$ and $D$. Then the functor of $A$ and $F$ is a functor of the set of opposite shifts of $C$ and $A$ and the set of opposite shifts of $D$ and $A$ defined as the opposite of $F$.

CategoryTheory.OppositeShift.natTransdefMathlib.CategoryTheory.Shift.Opposite, function or constant

Wording

the natural transformation of A and x5 (from the docstring)

English

Let $A$ be a set. Let $x_{5}$ be a homomorphism of $F$ and $G$. Then the natural transformation of $A$ and $x_{5}$ is a homomorphism of the functor of $A$ and $G$ and the functor of $A$ and $F$ defined as the opposite of $x_{5}$.

Mathlib.CategoryTheory.Shift.Pullback

CategoryTheory.NatTrans.PullbackShift.natIsoCompdefMathlib.CategoryTheory.Shift.Pullback, function or constant

Wording

the natural isomorphism between the pullback of x4 (from the docstring)

English

Let $x_{4}$ be an additive monoid homomorphism of $A$ and $B$. Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the natural isomorphism between the pullback of $x_{4}$ is an isomorphism of the functor of $x_{4}$ and the composition of $F$ and $G$ and the composition of the functor of $x_{4}$ and $F$ and the functor of $x_{4}$ and $G$ defined as the identity of the functor of $x_{4}$ and the composition of $F$ and $G$.

CategoryTheory.NatTrans.PullbackShift.natIsoIddefMathlib.CategoryTheory.Shift.Pullback, function or constant

Wording

the natural isomorphism identity of C and x4 (from the name)

English

Let $C$ be a set. Let $x_{4}$ be an additive monoid homomorphism of $A$ and $B$. Then the natural isomorphism identity of $C$ and $x_{4}$ is an isomorphism of the identity of the set of pullback shifts of $C$ and $x_{4}$ and the functor of $x_{4}$ and the identity of $C$ defined as the identity of the identity of the set of pullback shifts of $C$ and $x_{4}$.

CategoryTheory.PullbackShiftdefMathlib.CategoryTheory.Shift.Pullback, type

Wording

pullback shift of C and x4 (from the name)

English

Let $C$ be a set. Let $x_{4}$ be an additive monoid homomorphism of $A$ and $B$. Then a pullback shift of $C$ and $x_{4}$ is an element of the function that maps $C$ and $x_{4}$ to $C$.

CategoryTheory.PullbackShift.adjunctiondefMathlib.CategoryTheory.Shift.Pullback, function or constant

Wording

the adjunction of x4 and adj (from the name)

English

Let $x_{4}$ be an additive monoid homomorphism of $A$ and $B$. Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the adjunction of $x_{4}$ and $\mathrm{adj}$ is an adjunction of the functor of $x_{4}$ and $F$ and the functor of $x_{4}$ and $G$.

CategoryTheory.PullbackShift.functordefMathlib.CategoryTheory.Shift.Pullback, function or constant

Wording

the functor of x4 and F (from the name)

English

Let $x_{4}$ be an additive monoid homomorphism of $A$ and $B$. Let $F$ be a functor of $C$ and $D$. Then the functor of $x_{4}$ and $F$ is a functor of the set of pullback shifts of $C$ and $x_{4}$ and the set of pullback shifts of $D$ and $x_{4}$ defined as $F$.

CategoryTheory.PullbackShift.natTransdefMathlib.CategoryTheory.Shift.Pullback, function or constant

Wording

the natural transformation of x4 and x7 (from the docstring)

English

Let $x_{4}$ be an additive monoid homomorphism of $A$ and $B$. Let $x_{7}$ be a homomorphism of $F$ and $G$. Then the natural transformation of $x_{4}$ and $x_{7}$ is a homomorphism of the functor of $x_{4}$ and $F$ and the functor of $x_{4}$ and $G$ defined as $x_{7}$.

CategoryTheory.pullbackShiftIsodefMathlib.CategoryTheory.Shift.Pullback, function or constant

Wording

the pullback shift isomorphism of a and b (from the name)

English

Let $C$ be a set. Let $x_{4}$ be an additive monoid homomorphism of $A$ and $B$. Let $a$ be an element of $A$. Let $b$ be an element of $B$ such that $\EqtMACRoH {b}{x_{4} (a)}$. Then the pullback shift isomorphism of $a$ and $b$ is an isomorphism of the shift functor of the set of pullback shifts of $C$ and $x_{4}$ and $a$ and the shift functor of $C$ and $b$.

Mathlib.CategoryTheory.Shift.Quotient

HomRel.IsCompatibleWithShiftclassMathlib.CategoryTheory.Shift.Quotient, predicate

Wording

r is compatible with shift (from the name)

English

Let $r$ be a homomorphism relation of $C$. Let $A$ be a set. Then we can say that $r$ is compatible with shift.

Mathlib.CategoryTheory.Shift.ShiftSequence

CategoryTheory.Functor.ShiftSequenceclassMathlib.CategoryTheory.Shift.ShiftSequence, predicate

Wording

F is a shift sequence (from the name)

English

Let $F$ be a functor of $C$ and $A$. Let $M$ be a set. Then we can say that $F$ is a shift sequence.

CategoryTheory.Functor.ShiftSequence.isoZerodefMathlib.CategoryTheory.Shift.ShiftSequence, function or constant

Wording

the isomorphism zero (from the name)

English

The isomorphism zero is an isomorphism of the sequence of $F$ and $0$ and $F$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Functor.ShiftSequence.sequencedefMathlib.CategoryTheory.Shift.ShiftSequence, function or constant

Wording

the sequence of F and x4 (from the name)

English

Let $F$ be a functor of $C$ and $A$. Let $x_{4}$ be an element of $M$. Then the sequence of $F$ and $x_{4}$ is a functor of $C$ and $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

CategoryTheory.Functor.ShiftSequence.shiftIsodefMathlib.CategoryTheory.Shift.ShiftSequence, function or constant

Wording

the shift isomorphism of a and #3 (from the name)

English

Let $n$, $a$ and $\mathrm{a'}$ be elements of $M$ such that $\EqtMACRoH {n + a}{\mathrm{a'}}$. Then the shift isomorphism of $a$ and $\mathrm{a'}$ is an isomorphism of the composition of the shift functor of $C$ and $n$ and the sequence of $F$ and $a$ and the sequence of $F$ and $\mathrm{a'}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $n$, $a$, $\mathrm{a'}$ and $\mathrm{ha'}$.

CategoryTheory.Functor.isoShiftdefMathlib.CategoryTheory.Shift.ShiftSequence, function or constant

Wording

the canonical isomorphism of F and n (from the docstring)

English

Let $F$ be a functor of $C$ and $A$. Let $n$ be an element of $M$. Then the canonical isomorphism of $F$ and $n$ is an isomorphism of the composition of the shift functor of $C$ and $n$ and $F$ and the shift of $F$ and $n$.

CategoryTheory.Functor.isoShiftZerodefMathlib.CategoryTheory.Shift.ShiftSequence, function or constant

Wording

the canonical isomorphism of F and M (from the docstring)

English

Let $F$ be a functor of $C$ and $A$. Let $M$ be a set. Then the canonical isomorphism of $F$ and $M$ is an isomorphism of the shift of $F$ and $0$ and $F$ defined as the isomorphism zero.

CategoryTheory.Functor.shiftdefMathlib.CategoryTheory.Shift.ShiftSequence, function or constant

Wording

the shift of F and n (from the name)

English

Let $F$ be a functor of $C$ and $A$. Let $n$ be an element of $M$. Then the shift of $F$ and $n$ is a functor of $C$ and $A$ defined as the sequence of $F$ and $n$.

CategoryTheory.Functor.shiftIsodefMathlib.CategoryTheory.Shift.ShiftSequence, function or constant

Wording

the shift isomorphism of a and #4 (from the name)

English

Let $F$ be a functor of $C$ and $A$. Let $n$, $a$ and $\mathrm{a'}$ be elements of $M$ such that $\EqtMACRoH {n + a}{\mathrm{a'}}$. Then the shift isomorphism of $a$ and $\mathrm{a'}$ is an isomorphism of the composition of the shift functor of $C$ and $n$ and the shift of $F$ and $a$ and the shift of $F$ and $\mathrm{a'}$ defined as the shift isomorphism of $a$ and $\mathrm{a'}$.

CategoryTheory.Functor.shiftMapdefMathlib.CategoryTheory.Shift.ShiftSequence, function or constant

Wording

the shift map of a and #4 (from the name)

English

Let $F$ be a functor of $C$ and $A$. Let $f$ be a homomorphism of $X$ and the action of the shift functor of $C$ and $n$ and $Y$. Let $a$ and $\mathrm{a'}$ be elements of $M$ such that $\EqtMACRoH {n + a}{\mathrm{a'}}$. Then the shift map of $a$ and $\mathrm{a'}$ is a homomorphism of the action of the shift of $F$ and $a$ and $X$ and the action of the shift of $F$ and $\mathrm{a'}$ and $Y$ defined as the composition of the map of the shift of $F$ and $a$ and $f$ and the component of the homomorphism of the shift isomorphism of $a$ and $\mathrm{a'}$ and $Y$.

Mathlib.CategoryTheory.Shift.ShiftedHom

CategoryTheory.ShiftedHomdefMathlib.CategoryTheory.Shift.ShiftedHom, type

Wording

shifted homomorphism of Y and m (from the name)

English

Let $X$ and $Y$ be elements of $C$. Let $m$ be an element of $M$. Then a shifted homomorphism of $Y$ and $m$ is an element of the function that maps $X$, $Y$ and $m$ to the set of homomorphisms of $X$ and the action of the shift functor of $C$ and $m$ and $Y$.

CategoryTheory.ShiftedHom.compdefMathlib.CategoryTheory.Shift.ShiftedHom, function or constant

Wording

the composition of f (from the docstring)

English

Let $f$ be a shifted homomorphism of $Y$ and $a$. Let $g$ be a shifted homomorphism of $Z$ and $b$. Assume that $\EqtMACRoH {b + a}{c}$. Then the composition of $f$ is a shifted homomorphism of $Z$ and $c$ defined as the composition of $f$ and the composition of the map of the shift functor of $C$ and $a$ and $g$ and the component of the inverse of the shift functor sum of $a$ and $c$ and $Z$.

CategoryTheory.ShiftedHom.homEquivdefMathlib.CategoryTheory.Shift.ShiftedHom, function or constant

Wording

the homomorphism equivalence of x3 and h (from the name)

English

Let $x_{3}$ be an element of $M$ such that $\EqtMACRoH {x_{3}}{0}$. Then the homomorphism equivalence of $x_{3}$ and $h$ is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of shifted homomorphisms of $Y$ and $x_{3}$.

CategoryTheory.ShiftedHom.mapdefMathlib.CategoryTheory.Shift.ShiftedHom, function or constant

Wording

the map of f and F (from the name)

English

Let $f$ be a shifted homomorphism of $Y$ and $a$. Let $F$ be a functor of $C$ and $D$. Then the map of $f$ and $F$ is a shifted homomorphism of the action of $F$ and $Y$ and $a$ defined as the composition of the map of $F$ and $f$ and the component of the homomorphism of the commutative shift isomorphism of $F$ and $a$ and $Y$.

CategoryTheory.ShiftedHom.mk₀defMathlib.CategoryTheory.Shift.ShiftedHom, function or constant

Wording

no wording

English

Let $x_{3}$ be an element of $M$ such that $\EqtMACRoH {x_{3}}{0}$. Let $f$ be a homomorphism of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_ShiftedHom\_\_mk\_u2080\_}$ applied to $x_{3}$, $h$ and $f$ is a shifted homomorphism of $Y$ and $x_{3}$ defined as the composition of $f$ and the component of the inverse of the shift functor zero of $x_{3}$ and $Y$.

CategoryTheory.ShiftedHom.postcompIsoEquivdefMathlib.CategoryTheory.Shift.ShiftedHom, function or constant

Wording

the postcomposition isomorphism equivalence of e (from the name)

English

Let $e$ be an isomorphism of $Y$ and $Z$. Then the postcomposition isomorphism equivalence of $e$ is an equivalence from the set of shifted homomorphisms of $Y$ and $a$ to the set of shifted homomorphisms of $Z$ and $a$.

CategoryTheory.ShiftedHom.precompIsoEquivdefMathlib.CategoryTheory.Shift.ShiftedHom, function or constant

Wording

the precomposition isomorphism equivalence of e (from the name)

English

Let $e$ be an isomorphism of $X$ and $Y$. Then the precomposition isomorphism equivalence of $e$ is an equivalence from the set of shifted homomorphisms of $Z$ and $a$ to the set of shifted homomorphisms of $Z$ and $a$.

Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

CategoryTheory.ShiftedHom.opEquivdefMathlib.CategoryTheory.Shift.ShiftedHomOpposite, function or constant

Wording

the opposite equivalence of n (from the name)

English

Let $n$ be an integer. Then the opposite equivalence of $n$ is an equivalence from the set of shifted homomorphisms of $Y$ and $n$ to the set of shifted homomorphisms of $\operatorname{op}$ applied to $X$ and $n$ defined as the composition of the opposite equivalence and the homomorphism equivalence of $\operatorname{op}$ applied to $Y$ and $\operatorname{op}$ applied to $X$.

CategoryTheory.ShiftedHom.opEquiv'defMathlib.CategoryTheory.Shift.ShiftedHomOpposite, function or constant

Wording

the opposite equivalence of a and h (from the name)

English

Let $n$, $a$ and $\mathrm{a'}$ be integers such that $n + a = \mathrm{a'}$. Then the opposite equivalence of $a$ and $\mathrm{a'}$ is an equivalence from the set of shifted homomorphisms of $Y$ and $\mathrm{a'}$ to the set of homomorphisms of $\operatorname{op}$ applied to the action of the shift functor of $C$ and $a$ and $Y$ and the action of the shift functor of the set of opposites of $C$ and $n$ and $\operatorname{op}$ applied to $X$.

Mathlib.CategoryTheory.Shift.SingleFunctors

CategoryTheory.SingleFunctorsstructureMathlib.CategoryTheory.Shift.SingleFunctors, type

Wording

single functor of D and A (from the name)

English

Let $C$, $D$ and $A$ be sets. Then the single functors of $D$ and $A$ are a basic type.

CategoryTheory.SingleFunctors.HomstructureMathlib.CategoryTheory.Shift.SingleFunctors, type

Wording

homomorphism of F and G (from the name)

English

Let $F$ and $G$ be single functors of $D$ and $A$. Then the homomorphisms of $F$ and $G$ are a basic type.

CategoryTheory.SingleFunctors.Hom.compdefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the composition of x4 and x5 (from the name)

English

Let $x_{4}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $G$ and $H$. Then the composition of $x_{4}$ and $x_{5}$ is a homomorphism of $F$ and $H$.

CategoryTheory.SingleFunctors.Hom.homdefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the homomorphism of self and a (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $F$ and $G$. Let $a$ be an element of $A$. Then the homomorphism of $\mathrm{self}$ and $a$ is a homomorphism of the functor of $F$ and $a$ and the functor of $G$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

CategoryTheory.SingleFunctors.Hom.iddefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the identity morphism in F (from the docstring)

English

Let $F$ be a single functor of $D$ and $A$. Then the identity morphism in $F$ is a homomorphism of $F$ and $F$.

CategoryTheory.SingleFunctors.evaluationdefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the evaluation of a (from the name)

English

Let $C$ and $D$ be sets. Let $a$ be an element of $A$. Then the evaluation of $a$ is a functor of the set of single functors of $D$ and $A$ and the set of functors of $C$ and $D$.

CategoryTheory.SingleFunctors.functordefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the functor of self and a (from the name)

English

Let $\mathrm{self}$ be a single functor of $D$ and $A$. Let $a$ be an element of $A$. Then the functor of $\mathrm{self}$ and $a$ is a functor of $C$ and $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

CategoryTheory.SingleFunctors.isoMkdefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the isomorphism of iso and a1 (from the name)

English

Let $\mathrm{iso}$ be a function from elements $a_{1}$ of $A$ to isomorphisms of the functor of $F$ and $a_{1}$ and the functor of $G$ and $a_{1}$ such that for all elements $n$, $a$ and $\mathrm{a'}$ of $A$, for all elements $\mathrm{ha'}$ of $\mathrm{Proof}$ applied to $\EqtMACRoH {(n + a)}{\mathrm{a'}}$, the composition of the homomorphism of the shift isomorphism of $a$ and $\mathrm{a'}$ and the homomorphism of $\mathrm{iso}$ applied to $a$ is equal to the composition of the right whisker of the homomorphism of $\mathrm{iso}$ applied to $\mathrm{a'}$ and the shift functor of $D$ and $n$ and the homomorphism of the shift isomorphism of $a$ and $\mathrm{a'}$. Then the isomorphism of $a_{1}$ and $\mathrm{iso}$ is an isomorphism of $F$ and $G$.

CategoryTheory.SingleFunctors.postcompdefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the postcomposition of F and G (from the name)

English

Let $F$ be a single functor of $D$ and $A$. Let $G$ be a functor of $D$ and $E$. Then the postcomposition of $F$ and $G$ is a single functor of $E$ and $A$.

CategoryTheory.SingleFunctors.postcompFunctordefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the postcomposition functor of G (from the name)

English

Let $C$ and $A$ be sets. Let $G$ be a functor of $D$ and $E$. Then the postcomposition functor of $G$ is a functor of the set of single functors of $D$ and $A$ and the set of single functors of $E$ and $A$.

CategoryTheory.SingleFunctors.postcompIsoOfIsodefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the isomorphism of F and e (from the docstring)

English

Let $F$ be a single functor of $D$ and $A$. Let $e$ be an isomorphism of $G$ and $\mathrm{G'}$. Then the isomorphism of $F$ and $e$ is an isomorphism of the postcomposition of $F$ and $G$ and the postcomposition of $F$ and $\mathrm{G'}$.

CategoryTheory.SingleFunctors.postcompPostcompIsodefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the postcomposition postcomposition isomorphism of G and #3 (from the name)

English

Let $F$ be a single functor of $D$ and $A$. Let $G$ be a functor of $D$ and $E$. Let $\mathrm{G'}$ be a functor of $E$ and $\mathrm{E'}$. Then the postcomposition postcomposition isomorphism of $G$ and $\mathrm{G'}$ is an isomorphism of the postcomposition of the postcomposition of $F$ and $G$ and $\mathrm{G'}$ and the postcomposition of $F$ and the composition of $G$ and $\mathrm{G'}$.

CategoryTheory.SingleFunctors.shiftIsodefMathlib.CategoryTheory.Shift.SingleFunctors, function or constant

Wording

the shift isomorphism of a and #4 (from the name)

English

Let $\mathrm{self}$ be a single functor of $D$ and $A$. Let $n$, $a$ and $\mathrm{a'}$ be elements of $A$ such that $\EqtMACRoH {n + a}{\mathrm{a'}}$. Then the shift isomorphism of $a$ and $\mathrm{a'}$ is an isomorphism of the composition of the functor of $\mathrm{self}$ and $\mathrm{a'}$ and the shift functor of $D$ and $n$ and the functor of $\mathrm{self}$ and $a$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $n$, $a$, $\mathrm{a'}$ and $\mathrm{ha'}$.

Mathlib.CategoryTheory.Shift.SingleFunctorsLift

CategoryTheory.SingleFunctors.liftdefMathlib.CategoryTheory.Shift.SingleFunctorsLift, function or constant

Wording

the lift of x7 and x8 (from the name)

English

Let $F$ be a single functor of $E$ and $A$. Let $G$ be a functor of $D$ and $E$. Let $x_{7}$ be a function from elements of $A$ to functors of $C$ and $D$. Let $x_{8}$ be a function from elements $a$ of $A$ to isomorphisms of the composition of $x_{7}$ applied to $a$ and $G$ and the functor of $F$ and $a$. Then the lift of $x_{7}$ and $a$ is a single functor of $D$ and $A$.

CategoryTheory.SingleFunctors.liftPostcompIsodefMathlib.CategoryTheory.Shift.SingleFunctorsLift, function or constant

Wording

the lift postcomposition isomorphism of x7 and x8 (from the name)

English

Let $F$ be a single functor of $E$ and $A$. Let $G$ be a functor of $D$ and $E$. Let $x_{7}$ be a function from elements of $A$ to functors of $C$ and $D$. Let $x_{8}$ be a function from elements $a$ of $A$ to isomorphisms of the composition of $x_{7}$ applied to $a$ and $G$ and the functor of $F$ and $a$. Then the lift postcomposition isomorphism of $x_{7}$ and $a$ is an isomorphism of the postcomposition of the lift of $x_{7}$ and $x_{8}$ and $G$ and $F$.

Mathlib.CategoryTheory.Shift.Twist

CategoryTheory.TwistShiftDatastructureMathlib.CategoryTheory.Shift.Twist, type

Wording

twist shift data of C and A (from the name)

English

Let $C$ and $A$ be sets. Then the twist shift data of $C$ and $A$ are a basic type.

CategoryTheory.TwistShiftData.CategorydefMathlib.CategoryTheory.Shift.Twist, type

Wording

category of x3 (from the name)

English

Let $x_{3}$ be a twist shift data of $C$ and $A$. Then a category of $x_{3}$ is an element of the function that maps $x_{3}$ to $C$.

CategoryTheory.TwistShiftData.shiftIsodefMathlib.CategoryTheory.Shift.Twist, function or constant

Wording

the shift isomorphism of t and m (from the name)

English

Let $t$ be a twist shift data of $C$ and $A$. Let $m$ be an element of $A$. Then the shift isomorphism of $t$ and $m$ is an isomorphism of the shift functor of the set of categories of $t$ and $m$ and the shift functor of $C$ and $m$ defined as the identity of the shift functor of the set of categories of $t$ and $m$.

CategoryTheory.TwistShiftData.shiftMkCoredefMathlib.CategoryTheory.Shift.Twist, function or constant

Wording

the shift of t (from the name)

English

Let $t$ be a twist shift data of $C$ and $A$. Then the shift of $t$ is a shift of the set of categories of $t$ and $A$.

CategoryTheory.TwistShiftData.zdefMathlib.CategoryTheory.Shift.Twist, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a twist shift data of $C$ and $A$. Let $a$ and $b$ be elements of $A$. Then $\operatorname{z}$ applied to $\mathrm{self}$, $a$ and $b$ is a unit of the set of category centers of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $a$ and $b$.

Mathlib.CategoryTheory.ShrinkYoneda

CategoryTheory.FunctorToTypes.SmalldefMathlib.CategoryTheory.ShrinkYoneda, predicate

Wording

F is small (from the name)

English

Let $F$ be a functor of $C$ and the set of sets. Then $F$ is small, if for all elements $X$ of $C$, the action of $F$ and $X$ is small.

CategoryTheory.FunctorToTypes.shrinkdefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink of F (from the name)

English

Let $F$ be a functor of $C$ and the set of sets. Then the shrink of $F$ is a functor of $C$ and the set of sets.

CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIsodefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink composition lift functor isomorphism of F (from the name)

English

Let $F$ be a functor of $C$ and the set of sets. Then the shrink composition lift functor isomorphism of $F$ is an isomorphism of the composition of the shrink of $F$ and the functor embedding and the shrink of $F$.

CategoryTheory.FunctorToTypes.shrinkMapdefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink map of x1 (from the name)

English

Let $x_{1}$ be a homomorphism of $F$ and $G$. Then the shrink map of $x_{1}$ is a homomorphism of the shrink of $F$ and the shrink of $G$.

CategoryTheory.fullyFaithfulShrinkCoyonedadefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the fully faithful shrink Coyoneda of C (from the name)

English

generation took over the time limit

CategoryTheory.fullyFaithfulShrinkYonedadefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the fully faithful shrink Yoneda of C (from the name)

English

generation took over the time limit

CategoryTheory.shrinkCoyonedadefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink Coyoneda (from the name)

English

The shrink Coyoneda is a functor of the set of opposites of $C$ and the set of functors of $C$ and the set of sets defined as the flip of the Yoneda embedding.

CategoryTheory.shrinkCoyonedaCompEvaluationCompUliftFunctorIsoUliftFunctordefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the functor of Y (from the docstring)

English

Let $Y$ be an element of $C$. Then the functor of $Y$ is an isomorphism of the composition of the shrink Coyoneda and the composition of the action of the evaluation of $C$ and the set of sets and $Y$ and the functor embedding and the composition of the action of the Yoneda and $Y$ and the functor embedding.

CategoryTheory.shrinkCoyonedaCorepresentableBydefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

no wording

English

Let $X$ be an opposite of $C$. Then $\operatorname{shrinkCoyonedaCorepresentableBy}$ applied to $X$ is an element of $\operatorname{CorepresentableBy}$ applied to the action of the shrink Coyoneda and $X$ and the opposite of $X$.

CategoryTheory.shrinkCoyonedaEquivdefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink Coyoneda equivalence (from the name)

English

The shrink Coyoneda equivalence is an equivalence from the set of homomorphisms of the action of the shrink Coyoneda and $X$ and $P$ to the action of $P$ and the opposite of $X$.

CategoryTheory.shrinkCoyonedaIsoCoyonedadefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink Coyoneda isomorphism Coyoneda (from the name)

English

The shrink Coyoneda isomorphism Coyoneda is an isomorphism of the shrink Coyoneda and the Coyoneda.

CategoryTheory.shrinkCoyonedaObjObjEquivdefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink Coyoneda object object equivalence (from the name)

English

The shrink Coyoneda object object equivalence is an equivalence from the action of the action of the shrink Coyoneda and $X$ and $Y$ to the set of homomorphisms of the opposite of $X$ and $Y$ defined as the shrink Yoneda object object equivalence.

CategoryTheory.shrinkCoyonedaUliftFunctorIsodefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink Coyoneda lift functor isomorphism (from the name)

English

The shrink Coyoneda lift functor isomorphism is an isomorphism of the composition of the shrink Coyoneda and the action of the right whiskering of the set of sets and the set of sets and the functor embedding and the shrink Coyoneda.

CategoryTheory.shrinkYonedadefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the Yoneda embedding (from the docstring)

English

The Yoneda embedding is a functor of $C$ and the set of functors of the set of opposites of $C$ and the set of sets.

CategoryTheory.shrinkYonedaCompEvaluationCompUliftFunctorIsoUliftFunctordefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the functor of Y (from the docstring)

English

Let $Y$ be an opposite of $C$. Then the functor of $Y$ is an isomorphism of the composition of the Yoneda embedding and the composition of the action of the evaluation of the set of opposites of $C$ and the set of sets and $Y$ and the functor embedding and the composition of the action of the Coyoneda and $Y$ and the functor embedding.

CategoryTheory.shrinkYonedaEquivdefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink Yoneda equivalence (from the name)

English

The shrink Yoneda equivalence is an equivalence from the set of homomorphisms of the action of the Yoneda embedding and $X$ and $P$ to the action of $P$ and $\operatorname{op}$ applied to $X$.

CategoryTheory.shrinkYonedaIsoYonedadefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink Yoneda isomorphism Yoneda (from the name)

English

The shrink Yoneda isomorphism Yoneda is an isomorphism of the Yoneda embedding and the Yoneda.

CategoryTheory.shrinkYonedaObjObjEquivdefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink Yoneda object object equivalence (from the name)

English

The shrink Yoneda object object equivalence is an equivalence from the action of the action of the Yoneda embedding and $X$ and $Y$ to the set of homomorphisms of the opposite of $Y$ and $X$ defined as the inverse of the equivalence shrink of the action of the action of the Yoneda and $X$ and $Y$.

CategoryTheory.shrinkYonedaRepresentableBydefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{shrinkYonedaRepresentableBy}$ applied to $X$ is an element of $\operatorname{RepresentableBy}$ applied to the action of the Yoneda embedding and $X$ and $X$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to the inverse of the shrink Yoneda object object equivalence and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{CategoryTheory\_\_shrinkYonedaObjObjEquiv\_symm\_comp}$.

CategoryTheory.shrinkYonedaUliftFunctorIsodefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the shrink Yoneda lift functor isomorphism (from the name)

English

The shrink Yoneda lift functor isomorphism is an isomorphism of the composition of the Yoneda embedding and the action of the right whiskering of the set of sets and the set of sets and the functor embedding and the Yoneda embedding.

CategoryTheory.uliftYonedaIsoShrinkCoyonedadefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the lift Yoneda isomorphism shrink Coyoneda (from the name)

English

The lift Yoneda isomorphism shrink Coyoneda is an isomorphism of the lift Coyoneda and the shrink Coyoneda.

CategoryTheory.uliftYonedaIsoShrinkYonedadefMathlib.CategoryTheory.ShrinkYoneda, function or constant

Wording

the lift Yoneda isomorphism shrink Yoneda (from the name)

English

The lift Yoneda isomorphism shrink Yoneda is an isomorphism of the lift Yoneda and the Yoneda embedding.

Mathlib.CategoryTheory.Sigma.Basic

CategoryTheory.Sigma.Functor.sigmadefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the sigma of F (from the name)

English

Let $F$ be a function from elements $i_{2}$ of $I$ to functors of $C$ applied to $i_{2}$ and $D$ applied to $i_{2}$. Then the sigma of $i_{2}$ is a functor of $\Sigma$ applied to the function that maps $i$ to $C$ applied to $i$ and $\Sigma$ applied to the function that maps $i_{1}$ to $D$ applied to $i_{1}$ defined as the function that maps $F$ to $\operatorname{desc}$ applied to the function that maps $i$ to the composition of $i_{2}$ applied to $i$ and the inclusion of $i$ and $F$.

CategoryTheory.Sigma.SigmaHominductiveMathlib.CategoryTheory.Sigma.Basic, type

Wording

sigma homomorphism of x1 and x2 (from the name)

English

Let $x_{1}$ be an element of $\Sigma$ applied to the function that maps $i_{1}$ to $C$ applied to $i_{1}$. Let $x_{2}$ be an element of $\Sigma$ applied to the function that maps $i$ to $C$ applied to $i$. Then the sigma homomorphisms of $x_{1}$ and $x_{2}$ are a basic type.

CategoryTheory.Sigma.SigmaHom.compdefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the composition of x1 and x2 (from the name)

English

Let $x_{1}$ be a sigma homomorphism of $X$ and $Y$. Let $x_{2}$ be a sigma homomorphism of $Y$ and $Z$. Then the composition of $x_{1}$ and $x_{2}$ is a sigma homomorphism of $X$ and $Z$.

CategoryTheory.Sigma.SigmaHom.iddefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the identity morphism of X (from the docstring)

English

Let $X$ be an element of $\Sigma$ applied to the function that maps $i$ to $C$ applied to $i$. Then the identity morphism of $X$ is a sigma homomorphism of $X$ and $X$.

CategoryTheory.Sigma.descdefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

no wording

English

Let $F$ be a function from elements $i_{1}$ of $I$ to functors of $C$ applied to $i_{1}$ and $D$. Then $\operatorname{desc}$ applied to $i_{1}$ and $F$ is a functor of $\Sigma$ applied to the function that maps $i$ to $C$ applied to $i$ and $D$.

CategoryTheory.Sigma.descMapdefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

no wording

English

Let $F$ be a function from elements $i_{2}$ of $I$ to functors of $C$ applied to $i_{2}$ and $D$. Let $X$ be an element of $\Sigma$ applied to the function that maps $i_{1}$ to $C$ applied to $i_{1}$. Let $Y$ be an element of $\Sigma$ applied to the function that maps $i$ to $C$ applied to $i$. Let $x_{2}$ be a homomorphism of $X$ and $Y$. Then $\operatorname{descMap}$ applied to $i_{2}$, $F$, $X$, $Y$ and $x_{2}$ is a homomorphism of the action of $F$ applied to $\operatorname{fst}$ applied to $X$ and $\operatorname{snd}$ applied to $X$ and the action of $F$ applied to $\operatorname{fst}$ applied to $Y$ and $\operatorname{snd}$ applied to $Y$.

CategoryTheory.Sigma.descUniqdefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

no wording

English

Let $F$ be a function from elements $i_{2}$ of $I$ to functors of $C$ applied to $i_{2}$ and $D$. Let $q$ be a functor of $\Sigma$ applied to the function that maps $i_{1}$ to $C$ applied to $i_{1}$ and $D$. Let $h$ be a function from elements $i$ of $I$ to isomorphisms of the composition of the inclusion of $i$ and $q$ and $F$ applied to $i$. Then $\operatorname{descUniq}$ applied to $i_{2}$, $F$, $q$, $i$ and $h$ is an isomorphism of $q$ and $\operatorname{desc}$ applied to $F$.

CategoryTheory.Sigma.incldefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the inclusion of i (from the name)

English

Let $i$ be an element of $I$. Then the inclusion of $i$ is a functor of $C$ applied to $i$ and $\Sigma$ applied to the function that maps $i_{1}$ to $C$ applied to $i_{1}$.

CategoryTheory.Sigma.inclCompMapdefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the inclusion composition map of g and j (from the name)

English

Let $C$ be a function from elements of $I$ to sets. Let $g$ be a function from elements of $J$ to elements of $I$. Let $j$ be an element of $J$. Then the inclusion composition map of $g$ and $j$ is an isomorphism of the composition of the inclusion of $j$ and the map of $C$ and $g$ and the inclusion of $g$ applied to $j$ defined as the identity of the composition of the inclusion of $j$ and the map of $C$ and $g$.

CategoryTheory.Sigma.inclDescdefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

no wording

English

Let $F$ be a function from elements $i_{1}$ of $I$ to functors of $C$ applied to $i_{1}$ and $D$. Let $i$ be an element of $I$. Then $\operatorname{inclDesc}$ applied to $i_{1}$, $F$ and $i$ is an isomorphism of the composition of the inclusion of $i$ and $\operatorname{desc}$ applied to $F$ and $F$ applied to $i$.

CategoryTheory.Sigma.mapdefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the map of C and g (from the name)

English

Let $C$ be a function from elements of $I$ to sets. Let $g$ be a function from elements of $J$ to elements of $I$. Then the map of $C$ and $g$ is a functor of $\Sigma$ applied to the function that maps $j$ to $C$ applied to $g$ applied to $j$ and $\Sigma$ applied to the function that maps $i$ to $C$ applied to $i$ defined as $\operatorname{desc}$ applied to the function that maps $j$ to the inclusion of $g$ applied to $j$.

CategoryTheory.Sigma.mapCompdefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the map composition of f and g (from the name)

English

Let $C$ be a function from elements of $I$ to sets. Let $f$ be a function from elements of $K$ to elements of $J$. Let $g$ be a function from elements of $J$ to elements of $I$. Then the map composition of $f$ and $g$ is an isomorphism of the composition of the map of the function that maps $x_{1}$ to $C$ applied to $g$ applied to $x_{1}$ and $f$ and the map of $C$ and $g$ and the map of $C$ and $\operatorname{comp}$ applied to $g$ and $f$ defined as $\operatorname{descUniq}$ applied to the function that maps $j$ to the inclusion of $\operatorname{comp}$ applied to $g$, $f$ and $j$, the composition of the map of the function that maps $x_{1}$ to $C$ applied to $g$ applied to $x_{1}$ and $f$ and the map of $C$ and $g$ and the function that maps $k$ to the composition of the right isomorphism whisker of the inclusion composition map of $f$ and $k$ and the map of $C$ and $g$ and the inclusion composition map of $g$ and $f$ applied to $k$.

CategoryTheory.Sigma.mapIddefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the map identity of I and C (from the name)

English

Let $I$ be a set. Let $C$ be a function from elements of $I$ to sets. Then the map identity of $I$ and $C$ is an isomorphism of the map of $C$ and $\mathrm{id}$ and the identity of $\Sigma$ applied to the function that maps $i$ to $C$ applied to $i$.

CategoryTheory.Sigma.natIsodefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the natural isomorphism of h (from the name)

English

Let $h$ be a function from elements $i$ of $I$ to isomorphisms of the composition of the inclusion of $i$ and $x_{2}$ and the composition of the inclusion of $i$ and $x_{3}$. Then the natural isomorphism of $i$ is an isomorphism of $x_{2}$ and $x_{3}$.

CategoryTheory.Sigma.natTransdefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the natural transformation of h (from the name)

English

Let $h$ be a function from elements $i$ of $I$ to homomorphisms of the composition of the inclusion of $i$ and $F$ and the composition of the inclusion of $i$ and $G$. Then the natural transformation of $i$ is a homomorphism of $F$ and $G$.

CategoryTheory.Sigma.natTrans.sigmadefMathlib.CategoryTheory.Sigma.Basic, function or constant

Wording

the sigma of x2 (from the name)

English

Let $x_{2}$ be a function from elements $i$ of $I$ to homomorphisms of $F$ applied to $i$ and $G$ applied to $i$. Then the sigma of $i$ is a homomorphism of the sigma of $F$ and the sigma of $G$.

Mathlib.CategoryTheory.Simple

CategoryTheory.SimpleclassMathlib.CategoryTheory.Simple, predicate

Wording

X is simple (from the docstring)

English

Let $X$ be an element of $C$. Then we can say that $X$ is simple.

Mathlib.CategoryTheory.SingleObj

CategoryTheory.SingleObjdefMathlib.CategoryTheory.SingleObj, type

Wording

single object of x (from the name)

English

Let $x$ be a set. Then a single object of $x$ is an element of the function that maps $x$ to the set of single objects of $x$.

CategoryTheory.SingleObj.differenceFunctordefMathlib.CategoryTheory.SingleObj, function or constant

Wording

the difference functor of f (from the name)

English

Let $f$ be a function from elements of $C$ to elements of $G$. Then the difference functor of $f$ is a functor of $C$ and the set of single objects of $G$.

CategoryTheory.SingleObj.functordefMathlib.CategoryTheory.SingleObj, function or constant

Wording

the functor of f (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and the set of ends of $X$. Then the functor of $f$ is a functor of the set of single objects of $M$ and $C$.

CategoryTheory.SingleObj.mapHomdefMathlib.CategoryTheory.SingleObj, function or constant

Wording

the map homomorphism of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the map homomorphism of $M$ and $N$ is an equivalence from the set of monoid homomorphisms of $M$ and $N$ to the set of functors of the set of single objects of $M$ and the set of single objects of $N$.

CategoryTheory.SingleObj.natTransdefMathlib.CategoryTheory.SingleObj, function or constant

Wording

the natural transformation of u and h (from the name)

English

Let $u$ be a homomorphism of the action of $F$ and the star of $M$ and the action of $G$ and the star of $M$ such that for all elements $a$ of $M$, the composition of the map of $F$ and $a$ and $u$ is equal to the composition of $u$ and the map of $G$ and $a$. Then the natural transformation of $u$ and $h$ is a homomorphism of $F$ and $G$ defined as $\operatorname{mk}$ applied to the function that maps $x_{2}$ to $u$ and the function that maps $x_{3}$, $x_{4}$ and $a$ to $h$ applied to $a$.

CategoryTheory.SingleObj.stardefMathlib.CategoryTheory.SingleObj, function or constant

Wording

the star of M (from the name)

English

Let $M$ be a set. Then the star of $M$ is a single object of $M$ defined as the star of $M$.

CategoryTheory.SingleObj.toEnddefMathlib.CategoryTheory.SingleObj, function or constant

Wording

the end of M (from the name)

English

Let $M$ be a set. Then the end of $M$ is a multiplicative equivalence of $M$ and the set of ends of the star of $M$.

MonCat.toCatdefMathlib.CategoryTheory.SingleObj, function or constant

Wording

the category (from the name)

English

The category is a functor of the set of monoid categories and the set of categories.

MonoidHom.toFunctordefMathlib.CategoryTheory.SingleObj, function or constant

Wording

the functor of f (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and $N$. Then the functor of $f$ is a functor of the set of single objects of $M$ and the set of single objects of $N$ defined as $\operatorname{mapHom}$ applied to $M$, $N$ and $f$.

MulEquiv.toSingleObjEquivdefMathlib.CategoryTheory.SingleObj, function or constant

Wording

the single object equivalence of e (from the name)

English

Let $e$ be a multiplicative equivalence of $M$ and $N$. Then the single object equivalence of $e$ is an equivalence of the set of single objects of $M$ and the set of single objects of $N$.

Units.toAutdefMathlib.CategoryTheory.SingleObj, function or constant

Wording

the automorphism of M (from the name)

English

Let $M$ be a set. Then the automorphism of $M$ is a multiplicative equivalence of $\UnitsMACRoAO {M}$ and the set of automorphisms of the star of $M$ defined as the composition of the map equivalence of the end of $M$ and the unit end equivalence automorphism of the star of $M$.

Mathlib.CategoryTheory.Sites.Adjunction

CategoryTheory.Sheaf.adjunctiondefMathlib.CategoryTheory.Sites.Adjunction, function or constant

Wording

the adjunction of J and adj (from the name)

English

generation took over the time limit

CategoryTheory.sheafForgetdefMathlib.CategoryTheory.Sites.Adjunction, function or constant

Wording

no wording

English

Let $J$ be a Grothendieck topology of $C$. Then $\operatorname{sheafForget}$ applied to $J$ is a functor of the set of sheaves of $J$ and $D$ and the set of sheaves of $J$ and the set of sets defined as $\operatorname{sheafCompose}$ applied to $J$ and the forgetful functor of $D$.

Mathlib.CategoryTheory.Sites.Canonical

CategoryTheory.GrothendieckTopology.SubcanonicalclassMathlib.CategoryTheory.Sites.Canonical, predicate

Wording

J is subcanonical (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Then we can say that $J$ is subcanonical.

CategoryTheory.GrothendieckTopology.fullyFaithfulUliftYonedadefMathlib.CategoryTheory.Sites.Canonical, function or constant

Wording

the fully faithful lift Yoneda of J (from the name)

English

generation took over the time limit

CategoryTheory.GrothendieckTopology.uliftYonedadefMathlib.CategoryTheory.Sites.Canonical, function or constant

Wording

the lift Yoneda of J (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Then the lift Yoneda of $J$ is a functor of $C$ and the set of sheaves of $J$ and the set of sets defined as the composition of the Yoneda of $J$ and $\operatorname{sheafCompose}$ applied to $J$ and the functor embedding.

CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheafdefMathlib.CategoryTheory.Sites.Canonical, function or constant

Wording

the lift Yoneda composition sheaf to presheaf of J (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Then the lift Yoneda composition sheaf to presheaf of $J$ is an isomorphism of the composition of the lift Yoneda of $J$ and the sheaf to presheaf of $J$ and the set of sets and the lift Yoneda defined as the identity of the composition of the lift Yoneda of $J$ and the sheaf to presheaf of $J$ and the set of sets.

CategoryTheory.GrothendieckTopology.uliftYonedaIsoYonedadefMathlib.CategoryTheory.Sites.Canonical, function or constant

Wording

the lift Yoneda isomorphism Yoneda of J (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Then the lift Yoneda isomorphism Yoneda of $J$ is an isomorphism of the lift Yoneda of $J$ and the Yoneda of $J$.

CategoryTheory.GrothendieckTopology.yonedadefMathlib.CategoryTheory.Sites.Canonical, function or constant

Wording

the Yoneda of J (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Then the Yoneda of $J$ is a functor of $C$ and the set of sheaves of $J$ and the set of sets.

CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheafdefMathlib.CategoryTheory.Sites.Canonical, function or constant

Wording

the Yoneda composition sheaf to presheaf of J (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Then the Yoneda composition sheaf to presheaf of $J$ is an isomorphism of the composition of the Yoneda of $J$ and the sheaf to presheaf of $J$ and the set of sets and the Yoneda defined as the identity of the composition of the Yoneda of $J$ and the sheaf to presheaf of $J$ and the set of sets.

CategoryTheory.GrothendieckTopology.yonedaFullyFaithfuldefMathlib.CategoryTheory.Sites.Canonical, function or constant

Wording

no wording

English

Let $J$ be a Grothendieck topology of $C$. Then $\operatorname{yonedaFullyFaithful}$ applied to $J$ is an element of $\operatorname{FullyFaithful}$ applied to the Yoneda of $J$ defined as $\operatorname{ofCompFaithful}$ applied to $\operatorname{fullyFaithful}$.

CategoryTheory.Sheaf.canonicalTopologydefMathlib.CategoryTheory.Sites.Canonical, function or constant

Wording

the canonical topology of C (from the name)

English

Let $C$ be a set. Then the canonical topology of $C$ is a Grothendieck topology of $C$ defined as $\operatorname{finestTopology}$ applied to the range of $\operatorname{obj}$ applied to the Yoneda.

CategoryTheory.Sheaf.finestTopologydefMathlib.CategoryTheory.Sites.Canonical, function or constant

Wording

no wording

English

Let $\mathrm{Ps}$ be an element of the power set of the set of functors of the set of opposites of $C$ and the set of sets. Then $\operatorname{finestTopology}$ applied to $\mathrm{Ps}$ is a Grothendieck topology of $C$ defined as the infimum of the image of $\operatorname{finestTopologySingle}$ and $\mathrm{Ps}$.

CategoryTheory.Sheaf.finestTopologySingledefMathlib.CategoryTheory.Sites.Canonical, function or constant

Wording

no wording

English

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{finestTopologySingle}$ applied to $P$ is a Grothendieck topology of $C$.

Mathlib.CategoryTheory.Sites.Closed

CategoryTheory.Functor.closedSievesdefMathlib.CategoryTheory.Sites.Closed, function or constant

Wording

the closed sieve of x1 (from the name)

English

Let $x_{1}$ be a Grothendieck topology of $C$. Then the closed sieve of $x_{1}$ is a subfunctor of the sieve of $C$.

CategoryTheory.Functor.sievesdefMathlib.CategoryTheory.Sites.Closed, function or constant

Wording

the sieve of C (from the name)

English

Let $C$ be a set. Then the sieve of $C$ is a functor of the set of opposites of $C$ and the set of sets.

CategoryTheory.GrothendieckTopology.IsCloseddefMathlib.CategoryTheory.Sites.Closed, predicate

Wording

S is closed with respect to x1 (from the name)

English

Let $x_{1}$ be a Grothendieck topology of $C$. Let $S$ be a sieve of $X$. Then $S$ is closed with respect to $x_{1}$, if for all elements $Y$ of $C$, for all homomorphisms $f$ of $Y$ and $X$, if $\operatorname{Covers}$ holds for $x_{1}$, $S$ and $f$, then $\operatorname{arrows}$ holds for $S$.

CategoryTheory.GrothendieckTopology.closedefMathlib.CategoryTheory.Sites.Closed, function or constant

Wording

no wording

English

Let $x_{1}$ be a Grothendieck topology of $C$. Let $S$ be a sieve of $X$. Then $\operatorname{close}$ applied to $x_{1}$ and $S$ is a sieve of $X$ defined as $\operatorname{mk}$ applied to the function that maps $x_{2}$ and $f$ to $\operatorname{Covers}$ applied to $x_{1}$, $S$ and $f$ and the function that maps $x_{3}$, $x_{4}$, $x_{5}$ and $\mathrm{hS}$ to $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_arrow\_stable}$ applied to $x_{1}$, $x_{5}$, $S$ and $\mathrm{hS}$.

CategoryTheory.GrothendieckTopology.closureOperatordefMathlib.CategoryTheory.Sites.Closed, function or constant

Wording

the closure operator of x1 and X (from the name)

English

Let $x_{1}$ be a Grothendieck topology of $C$. Let $X$ be an element of $C$. Then the closure operator of $x_{1}$ and $X$ is a closure operator of the set of sieves of $X$ defined as the closure operator of $\operatorname{close}$ applied to $x_{1}$ and the proposition that $\operatorname{IsClosed}$ holds for $x_{1}$.

CategoryTheory.topologyOfClosureOperatordefMathlib.CategoryTheory.Sites.Closed, function or constant

Wording

the topology of c and X1 (from the name)

English

Let $c$ be a function from elements $X_{1}$ of $C$ to closure operators of the set of sieves of $X_{1}$ such that for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ of $Y$ and $X$, for all sieves $S$ of $X$, $c$ applied to $Y$ and the pullback of $f$ and $S$ is equal to the pullback of $f$ and $c$ applied to $X$ and $S$. Then the topology of $X_{1}$ and $c$ is a Grothendieck topology of $C$.

Mathlib.CategoryTheory.Sites.Coherent.Basic

CategoryTheory.PrecoherentclassMathlib.CategoryTheory.Sites.Coherent.Basic, predicate

Wording

C is precoherent (from the name)

English

Let $C$ be a set. Then we can say that $C$ is precoherent.

CategoryTheory.PreregularclassMathlib.CategoryTheory.Sites.Coherent.Basic, predicate

Wording

C is preregular (from the name)

English

Let $C$ be a set. Then we can say that $C$ is preregular.

CategoryTheory.coherentCoveragedefMathlib.CategoryTheory.Sites.Coherent.Basic, function or constant

Wording

the coherent coverage of C (from the name)

English

Let $C$ be a set. Then the coherent coverage of $C$ is a coverage of $C$.

CategoryTheory.coherentTopologydefMathlib.CategoryTheory.Sites.Coherent.Basic, function or constant

Wording

the coherent topology of C (from the name)

English

Let $C$ be a set. Then the coherent topology of $C$ is a Grothendieck topology of $C$ defined as $\operatorname{toGrothendieck}$ applied to the coherent coverage of $C$.

CategoryTheory.extensiveCoveragedefMathlib.CategoryTheory.Sites.Coherent.Basic, function or constant

Wording

the extensive coverage of C (from the name)

English

Let $C$ be a set. Then the extensive coverage of $C$ is a coverage of $C$.

CategoryTheory.extensiveTopologydefMathlib.CategoryTheory.Sites.Coherent.Basic, function or constant

Wording

the extensive topology of C (from the name)

English

Let $C$ be a set. Then the extensive topology of $C$ is a Grothendieck topology of $C$ defined as $\operatorname{toGrothendieck}$ applied to the extensive coverage of $C$.

CategoryTheory.regularCoveragedefMathlib.CategoryTheory.Sites.Coherent.Basic, function or constant

Wording

the regular coverage of C (from the name)

English

Let $C$ be a set. Then the regular coverage of $C$ is a coverage of $C$.

CategoryTheory.regularTopologydefMathlib.CategoryTheory.Sites.Coherent.Basic, function or constant

Wording

the regular topology of C (from the name)

English

Let $C$ be a set. Then the regular topology of $C$ is a Grothendieck topology of $C$ defined as $\operatorname{toGrothendieck}$ applied to the regular coverage of $C$.

Mathlib.CategoryTheory.Sites.Coherent.Equivalence

CategoryTheory.Equivalence.sheafCongrPrecoherentdefMathlib.CategoryTheory.Sites.Coherent.Equivalence, function or constant

Wording

no wording

English

Let $A$ be a set. Let $e$ be an equivalence of $C$ and $D$. Then $\operatorname{sheafCongrPrecoherent}$ applied to $A$ and $e$ is an equivalence of the set of sheaves of the coherent topology of $C$ and $A$ and the set of sheaves of the coherent topology of $D$ and $A$ defined as the sheaf congruence of the coherent topology of $D$ and $e$.

CategoryTheory.Equivalence.sheafCongrPreregulardefMathlib.CategoryTheory.Sites.Coherent.Equivalence, function or constant

Wording

no wording

English

Let $A$ be a set. Let $e$ be an equivalence of $C$ and $D$. Then $\operatorname{sheafCongrPreregular}$ applied to $A$ and $e$ is an equivalence of the set of sheaves of the regular topology of $C$ and $A$ and the set of sheaves of the regular topology of $D$ and $A$ defined as the sheaf congruence of the regular topology of $D$ and $e$.

Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

CategoryTheory.Presieve.ExtensiveclassMathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves, predicate

Wording

R is extensive (from the docstring)

English

Let $R$ be a presieve of $X$. Then we can say that $R$ is extensive.

Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

CategoryTheory.Presieve.regularclassMathlib.CategoryTheory.Sites.Coherent.RegularSheaves, predicate

Wording

R is regular (from the docstring)

English

Let $R$ be a presieve of $X$. Then we can say that $R$ is regular.

CategoryTheory.regularTopology.EqualizerConditiondefMathlib.CategoryTheory.Sites.Coherent.RegularSheaves, predicate

Wording

P is a equalizer condition (from the name)

English

Let $P$ be a functor of the set of opposites of $C$ and $D$. Then $P$ is an equalizer condition, if for all elements $X$ and $B$ of $C$, for all homomorphisms $x_{2}$ of $X$ and $B$, if $x_{2}$ is an effective epimorphism, then $\operatorname{SingleEqualizerCondition}$ holds for $P$ and $x_{2}$.

CategoryTheory.regularTopology.SingleEqualizerConditiondefMathlib.CategoryTheory.Sites.Coherent.RegularSheaves, predicate

Wording

no wording

English

Let $P$ be a functor of the set of opposites of $C$ and $D$. Let $x_{2}$ be a homomorphism of $X$ and $B$. Then $\operatorname{SingleEqualizerCondition}$ holds for $P$ and $x_{2}$, if for all pullback cones $c$ of $x_{2}$ and $x_{2}$, for all elements $x_{3}$ of $\operatorname{IsLimit}$ applied to $c$, $\mathrm{Nonempty}$ holds for $\operatorname{IsLimit}$ applied to the inclusion of the map of $P$ and the opposite in $x_{2}$ and $\mathrm{CategoryTheory\_\_regularTopology\_\_equalizerCondition\_w}$ applied to $P$ and $c$.

CategoryTheory.regularTopology.isLimit_forkOfι_equivdefMathlib.CategoryTheory.Sites.Coherent.RegularSheaves, function or constant

Wording

no wording

English

Let $P$ be a functor of the set of opposites of $C$ and $D$. Let $x_{2}$ be a homomorphism of $X$ and $B$. Let $c$ be a pullback cone of $x_{2}$ and $x_{2}$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\mathrm{CategoryTheory\_\_regularTopology\_\_isLimit\_forkOf\_u3b9\_\_equiv}$ applied to $P$, $x_{2}$, $c$ and $\mathrm{hc}$ is an equivalence from $\operatorname{IsLimit}$ applied to the inclusion of the map of $P$ and the opposite in $x_{2}$ and $\mathrm{CategoryTheory\_\_regularTopology\_\_equalizerCondition\_w}$ applied to $P$ and $c$ to $\operatorname{IsLimit}$ applied to the map cone of $P$ and the opposite of the cocone of the arrow of the sieve of the function that maps $x_{3}$ to $X$ and the function that maps $x_{4}$ to $x_{2}$.

CategoryTheory.regularTopology.mapToEqualizerdefMathlib.CategoryTheory.Sites.Coherent.RegularSheaves, function or constant

Wording

the map to equalizer of x1 and x2 (from the name)

English

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $f$ be a homomorphism of $X$ and $B$. Let $x_{1}$ and $x_{2}$ be homomorphisms of $W$ and $X$ such that the composition of $x_{1}$ and $f$ is equal to the composition of $x_{2}$ and $f$. Then the map to equalizer of $x_{1}$ and $x_{2}$ is a homomorphism of the action of $P$ and $\operatorname{op}$ applied to $B$ and the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{3}$ to the proposition that $\operatorname{hom}$ applied to the map of $P$ and the opposite in $x_{1}$ and $x_{3}$ is equal to $\operatorname{hom}$ applied to the map of $P$ and the opposite in $x_{2}$ and $x_{3}$ defined as the type category of the function that maps $t$ to $\operatorname{hom}$ applied to the map of $P$ and the opposite in $f$ and $t$.

Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

CategoryTheory.Presheaf.coherentExtensiveEquivalencedefMathlib.CategoryTheory.Sites.Coherent.SheafComparison, function or constant

Wording

the coherent extensive equivalence (from the name)

English

The coherent extensive equivalence is an equivalence of the set of sheaves of the coherent topology of $C$ and $A$ and the set of sheaves of the extensive topology of $C$ and $A$.

CategoryTheory.coherentTopology.equivalencedefMathlib.CategoryTheory.Sites.Coherent.SheafComparison, function or constant

Wording

the equivalence of F and A (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $A$ be a set. Then the equivalence of $F$ and $A$ is an equivalence of the set of sheaves of the coherent topology of $C$ and $A$ and the set of sheaves of the coherent topology of $D$ and $A$ defined as the sheaf equivalence of the coherent topology of $D$ and $F$.

CategoryTheory.coherentTopology.equivalence'defMathlib.CategoryTheory.Sites.Coherent.SheafComparison, function or constant

Wording

the equivalence of F and A (from the name)

English

CategoryTheory.regularTopology.equivalencedefMathlib.CategoryTheory.Sites.Coherent.SheafComparison, function or constant

Wording

the equivalence of F and A (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $A$ be a set. Then the equivalence of $F$ and $A$ is an equivalence of the set of sheaves of the regular topology of $C$ and $A$ and the set of sheaves of the regular topology of $D$ and $A$ defined as the sheaf equivalence of the regular topology of $D$ and $F$.

Mathlib.CategoryTheory.Sites.CompatiblePlus

CategoryTheory.GrothendieckTopology.diagramCompIsodefMathlib.CategoryTheory.Sites.CompatiblePlus, function or constant

Wording

the diagram composition isomorphism of P and X (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $D$ and $E$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Let $X$ be an element of $C$. Then the diagram composition isomorphism of $P$ and $X$ is an isomorphism of the composition of the diagram of $P$ and $X$ and $F$ and the diagram of the composition of $P$ and $F$ and $X$.

CategoryTheory.GrothendieckTopology.plusCompIsodefMathlib.CategoryTheory.Sites.CompatiblePlus, function or constant

Wording

the plus composition isomorphism of F and P (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $D$ and $E$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Then the plus composition isomorphism of $F$ and $P$ is an isomorphism of the composition of the plus object of $J$ and $P$ and $F$ and the plus object of $J$ and the composition of $P$ and $F$.

CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIsodefMathlib.CategoryTheory.Sites.CompatiblePlus, function or constant

Wording

the plus functor whisker left isomorphism 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 plus functor whisker left isomorphism of $J$ and $P$ is an isomorphism of the action of the left whiskering of $D$ and $E$ and the plus object of $J$ and $P$ and the composition of the action of the left whiskering of $D$ and $E$ and $P$ and the plus functor of $J$ and $E$.

CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIsodefMathlib.CategoryTheory.Sites.CompatiblePlus, function or constant

Wording

the plus functor whisker right isomorphism of J and F (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $D$ and $E$. Then the plus functor whisker right isomorphism of $J$ and $F$ is an isomorphism of the composition of the plus functor of $J$ and $D$ and the action of the right whiskering of $D$ and $E$ and $F$ and the composition of the action of the right whiskering of $D$ and $E$ and $F$ and the plus functor of $J$ and $E$ defined as the natural isomorphism of the function that maps $x_{3}$ to the plus composition isomorphism of $F$ and $x_{3}$ and the function that maps $x_{4}$, $x_{5}$ and $x_{6}$ to $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_plusCompIso\_whiskerRight}$ applied to $J$, $F$ and $x_{6}$.

Mathlib.CategoryTheory.Sites.CompatibleSheafification

CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIsodefMathlib.CategoryTheory.Sites.CompatibleSheafification, function or constant

Wording

the sheafification whisker left isomorphism 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 whisker left isomorphism of $J$ and $P$ is an isomorphism of the action of the left whiskering of $D$ and $E$ and the sheafification of $J$ and $P$ and the composition of the action of the left whiskering of $D$ and $E$ and $P$ and the sheafification of $J$ and $E$ defined as the composition of the plus functor whisker left isomorphism of $J$ and the plus object of $J$ and $P$ and the composition of the right isomorphism whisker of the plus functor whisker left isomorphism of $J$ and $P$ and the plus functor of $J$ and $E$ and the associator of the plus functor of $J$ and $E$ and the plus functor of $J$ and $E$.

CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIsodefMathlib.CategoryTheory.Sites.CompatibleSheafification, function or constant

Wording

the sheafification whisker right isomorphism of J and F (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $D$ and $E$. Then the sheafification whisker right isomorphism of $J$ and $F$ is an isomorphism of the composition of the sheafification of $J$ and $D$ and the action of the right whiskering of $D$ and $E$ and $F$ and the composition of the action of the right whiskering of $D$ and $E$ and $F$ and the sheafification of $J$ and $E$ defined as the composition of the associator of the plus functor of $J$ and $D$ and the action of the right whiskering of $D$ and $E$ and $F$ and the composition of the left isomorphism whisker of the plus functor of $J$ and $D$ and the plus functor whisker right isomorphism of $J$ and $F$ and the composition of the composition of the inverse of the associator of the action of the right whiskering of $D$ and $E$ and $F$ and the plus functor of $J$ and $E$ and the right isomorphism whisker of the plus functor whisker right isomorphism of $J$ and $F$ and the plus functor of $J$ and $E$ and the associator of the plus functor of $J$ and $E$ and the plus functor of $J$ and $E$.

CategoryTheory.GrothendieckTopology.sheafifyCompIsodefMathlib.CategoryTheory.Sites.CompatibleSheafification, function or constant

Wording

the sheafification composition isomorphism of F and P (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of $D$ and $E$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Then the sheafification composition isomorphism of $F$ and $P$ is an isomorphism of the composition of the sheafification of $J$ and $P$ and $F$ and the sheafification of $J$ and the composition of $P$ and $F$ defined as the composition of the plus composition isomorphism of $F$ and the plus object of $J$ and $P$ and the map isomorphism of the plus functor of $J$ and $E$ and the plus composition isomorphism of $F$ and $P$.

Mathlib.CategoryTheory.Sites.ConcreteSheafification

CategoryTheory.GrothendieckTopology.Plus.mkdefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

no wording

English

Let $x_{3}$ be an element of $\operatorname{Meq}$ applied to $P$ and $S$. Then $\operatorname{mk}$ applied to $x_{3}$ is a type of the action of the plus object of $J$ and $P$ and $\operatorname{op}$ applied to $X$ defined as $\operatorname{hom}$ applied to the inclusion of the diagram of $P$ and $X$ and $\operatorname{op}$ applied to $S$ and $\operatorname{symm}$ applied to the equivalence of $P$ and $S$ and $x_{3}$.

CategoryTheory.GrothendieckTopology.isoSheafifydefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

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.GrothendieckTopology.sheafificationdefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

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 plus functor of $J$ and $D$ and the plus functor of $J$ and $D$.

CategoryTheory.GrothendieckTopology.sheafifydefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

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 plus object of $J$ and the plus object of $J$ and $P$.

CategoryTheory.GrothendieckTopology.sheafifyLiftdefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

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 plus lift of $J$ and the plus lift of $J$ and $x_{2}$.

CategoryTheory.GrothendieckTopology.sheafifyMapdefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

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 $\operatorname{plusMap}$ applied to $J$ and $\operatorname{plusMap}$ applied to $J$ and $x_{2}$.

CategoryTheory.GrothendieckTopology.toSheafificationdefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

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 composition of the plus natural transformation of $J$ and $D$ and the right whisker of the plus natural transformation of $J$ and $D$ and the plus functor of $J$ and $D$.

CategoryTheory.GrothendieckTopology.toSheafifydefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

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 composition of the plus of $J$ and $P$ and $\operatorname{plusMap}$ applied to $J$ and the plus of $J$ and $P$.

CategoryTheory.MeqdefMathlib.CategoryTheory.Sites.ConcreteSheafification, type

Wording

no wording

English

Let $P$ be a functor of the set of opposites of $C$ and $D$. Let $S$ be a cover of $J$ and $X$. Then an element of $\operatorname{Meq}$ applied to $P$ and $S$ is an element of the function that maps $P$ and $S$ to $\SubtypeSet {x_{4}}{\mathrm{forall} (\operatorname{Relation} (S), \lambda I . \EqtMACRoH {\operatorname{hom} (\operatorname{map} (P , \operatorname{op} (\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2081\_} (\operatorname{r} (I)))), x_{4} (\operatorname{fst} (I)))}{\operatorname{hom} (\operatorname{map} (P , \operatorname{op} (\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2082\_} (\operatorname{r} (I)))), x_{4} (\operatorname{snd} (I)))})}$.

CategoryTheory.Meq.equivdefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

the equivalence of P and S (from the name)

English

Let $P$ be a functor of the set of opposites of $C$ and $D$. Let $S$ be a cover of $J$ and $X$. Then the equivalence of $P$ and $S$ is an equivalence from the set of types of the multiequalizer of the index of $S$ and $P$ to $\operatorname{Meq}$ applied to $P$ and $S$ defined as the multiequalizer equivalence of the index of $S$ and $P$.

CategoryTheory.Meq.mkdefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

no wording

English

Let $S$ be a cover of $J$ and $X$. Let $x_{4}$ be a type of the action of $P$ and $\operatorname{op}$ applied to $X$. Then $\operatorname{mk}$ applied to $S$ and $x_{4}$ is an element of $\operatorname{Meq}$ applied to $P$ and $S$ defined as the function that maps $I$ to $\operatorname{hom}$ applied to the map of $P$ and the opposite in $\operatorname{f}$ applied to $I$ and $x_{4}$.

CategoryTheory.Meq.pullbackdefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

the pullback of x4 and f (from the name)

English

Let $x_{4}$ be an element of $\operatorname{Meq}$ applied to $P$ and $S$. Let $f$ be a homomorphism of $Y$ and $X$. Then the pullback of $x_{4}$ and $f$ is an element of $\operatorname{Meq}$ applied to $P$ and the action of the pullback of $J$ and $f$ and $S$.

CategoryTheory.Meq.refinedefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

no wording

English

Let $x_{4}$ be an element of $\operatorname{Meq}$ applied to $P$ and $T$. Let $e$ be a homomorphism of $S$ and $T$. Then $\operatorname{refine}$ applied to $x_{4}$ and $e$ is an element of $\operatorname{Meq}$ applied to $P$ and $S$.

CategoryTheory.plusPlusAdjunctiondefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

the plus plus adjunction of J and D (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Then the plus plus adjunction of $J$ and $D$ is an adjunction of the plus plus sheaf of $J$ and $D$ and the sheaf to presheaf of $J$ and $D$.

CategoryTheory.plusPlusSheafdefMathlib.CategoryTheory.Sites.ConcreteSheafification, function or constant

Wording

the plus plus sheaf of J and D (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Then the plus plus sheaf 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 sheaves of $J$ and $D$.

Mathlib.CategoryTheory.Sites.ConstantSheaf

CategoryTheory.Sheaf.IsConstantclassMathlib.CategoryTheory.Sites.ConstantSheaf, predicate

Wording

J is constant (from the docstring)

English

Let $J$ be a Grothendieck topology of $C$. Let $F$ be a sheaf of $J$ and $D$. Then we can say that $J$ is constant.

CategoryTheory.constantCommuteComposedefMathlib.CategoryTheory.Sites.ConstantSheaf, function or constant

Wording

no wording

English

Let $J$ be a Grothendieck topology of $C$. Let $U$ be a functor of $D$ and $B$. Then $\operatorname{constantCommuteCompose}$ applied to $J$ and $U$ is an isomorphism of the composition of the constant sheaf of $J$ and $D$ and $\operatorname{sheafCompose}$ applied to $J$ and $U$ and the composition of $U$ and the constant sheaf of $J$ and $B$ defined as the composition of the left isomorphism whisker of the constant of the set of opposites of $C$ and the inverse of $\operatorname{sheafComposeNatIso}$ applied to $J$, $U$, the sheafification adjunction of $J$ and $D$ and the sheafification adjunction of $J$ and $B$ and the right isomorphism whisker of the inverse of the canonical isomorphism of the set of opposites of $C$ and $U$ and the presheaf to sheaf of $J$ and $B$.

CategoryTheory.constantPresheafAdjdefMathlib.CategoryTheory.Sites.ConstantSheaf, function or constant

Wording

the constant presheaf functor of D and hT (from the docstring)

English

Let $D$ be a set. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then the constant presheaf functor of $D$ and $\mathrm{hT}$ is an adjunction of the constant of the set of opposites of $C$ and the action of the evaluation of the set of opposites of $C$ and $D$ and $\operatorname{op}$ applied to $T$.

CategoryTheory.constantSheafdefMathlib.CategoryTheory.Sites.ConstantSheaf, function or constant

Wording

the constant sheaf of J and D (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Then the constant sheaf of $J$ and $D$ is a functor of $D$ and the set of sheaves of $J$ and $D$ defined as the composition of the constant of the set of opposites of $C$ and the presheaf to sheaf of $J$ and $D$.

CategoryTheory.constantSheafAdjdefMathlib.CategoryTheory.Sites.ConstantSheaf, function or constant

Wording

the constant sheaf adjoint of J and hT (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then the constant sheaf adjoint of $J$ and $\mathrm{hT}$ is an adjunction of the constant sheaf of $J$ and $D$ and the action of the sheaf section of $J$ and $D$ and $\operatorname{op}$ applied to $T$ defined as the composition of the constant presheaf functor of $D$ and $\mathrm{hT}$ and the sheafification adjunction of $J$ and $D$.

CategoryTheory.equivCommuteConstantdefMathlib.CategoryTheory.Sites.ConstantSheaf, function or constant

Wording

the equivalence commute constant of hT and #6 (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Let $K$ be a Grothendieck topology of $\mathrm{C'}$. Let $G$ be a functor of $C$ and $\mathrm{C'}$. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Let $\mathrm{hT'}$ be an element of $\operatorname{IsTerminal}$ applied to the action of $G$ and $T$. Then the equivalence commute constant of $\mathrm{hT}$ and $\mathrm{hT'}$ is an isomorphism of the composition of the constant sheaf of $J$ and $D$ and the functor of the sheaf equivalence of $K$ and $G$ and the constant sheaf of $K$ and $D$ defined as $\operatorname{leftAdjointUniq}$ applied to the composition of the constant sheaf adjoint of $J$ and $\mathrm{hT}$ and the adjunction of the sheaf equivalence of $K$ and $G$ and the constant sheaf adjoint of $K$ and $\mathrm{hT'}$.

CategoryTheory.equivCommuteConstant'defMathlib.CategoryTheory.Sites.ConstantSheaf, function or constant

Wording

the equivalence commute constant of hT and #6 (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Let $K$ be a Grothendieck topology of $\mathrm{C'}$. Let $G$ be a functor of $C$ and $\mathrm{C'}$. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Let $\mathrm{hT'}$ be an element of $\operatorname{IsTerminal}$ applied to the action of $G$ and $T$. Then the equivalence commute constant of $\mathrm{hT}$ and $\mathrm{hT'}$ is an isomorphism of the constant sheaf of $J$ and $D$ and the composition of the constant sheaf of $K$ and $D$ and the inverse of the sheaf equivalence of $K$ and $G$ defined as the composition of the left isomorphism whisker of the constant sheaf of $J$ and $D$ and the unit isomorphism of the sheaf equivalence of $K$ and $G$ and the right isomorphism whisker of the equivalence commute constant of $\mathrm{hT}$ and $\mathrm{hT'}$ and the inverse of the sheaf equivalence of $K$ and $G$.

Mathlib.CategoryTheory.Sites.Continuous

CategoryTheory.Adjunction.sheafPushforwardContinuousdefMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

no wording

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Then $\operatorname{sheafPushforwardContinuous}$ applied to $\mathrm{adj}$, $J$ and $K$ is an adjunction of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $E$, $J$ and $K$ and $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $E$, $K$ and $J$.

CategoryTheory.Functor.IsContinuousclassMathlib.CategoryTheory.Sites.Continuous, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Then we can say that $\operatorname{IsContinuous}$ holds for $F$, $J$ and $K$.

CategoryTheory.Functor.PreservesOneHypercoversdefMathlib.CategoryTheory.Sites.Continuous, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Then $\operatorname{PreservesOneHypercovers}$ holds for $F$, $J$ and $K$, if for all elements $X$ of $C$, for all one hypercovers $E$ of $J$ and $X$, $\operatorname{IsPreservedBy}$ holds for $E$, $F$ and $K$.

CategoryTheory.Functor.sheafPushforwardContinuousdefMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

no wording

English

Let $F$ 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{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$ is a functor of the set of sheaves of $K$ and $A$ and the set of sheaves of $J$ and $A$ defined as the lift of $\operatorname{IsSheaf}$ applied to $J$ and the composition of the sheaf to presheaf of $K$ and $A$ and the action of the left whiskering of the set of opposites of $D$ and $A$ and the opposite of $F$.

CategoryTheory.Functor.sheafPushforwardContinuousCompdefMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

the sheaf pushforward continuous composition of K and L (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Let $A$ be a set. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $L$ be a Grothendieck topology of $E$. Then the sheaf pushforward continuous composition of $K$ and $L$ is an isomorphism of the composition of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $K$ and $L$ and $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$ and $\operatorname{sheafPushforwardContinuous}$ applied to the composition of $F$ and $G$, $A$, $J$ and $L$ defined as the identity of the composition of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $K$ and $L$ and $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$.

CategoryTheory.Functor.sheafPushforwardContinuousComp'defMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

the sheaf pushforward continuous composition of K and L (from the name)

English

Let $\mathrm{eFG}$ be an isomorphism of the composition of $F$ and $G$ and $\mathrm{FG}$. Let $A$ be a set. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $L$ be a Grothendieck topology of $E$. Then the sheaf pushforward continuous composition of $K$ and $L$ is an isomorphism of the composition of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $K$ and $L$ and $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$ and $\operatorname{sheafPushforwardContinuous}$ applied to $\mathrm{FG}$, $A$, $J$ and $L$ defined as the composition of the sheaf pushforward continuous composition of $K$ and $L$ and the sheaf pushforward continuous isomorphism of $J$ and $L$.

CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIsodefMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

the sheaf pushforward continuous composition sheaf to presheaf isomorphism of J and K (from the name)

English

Let $F$ 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 pushforward continuous composition sheaf to presheaf isomorphism of $J$ and $K$ is an isomorphism of the composition of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$ and the sheaf to presheaf of $J$ and $A$ and the composition of the sheaf to presheaf of $K$ and $A$ and the action of the left whiskering of the set of opposites of $D$ and $A$ and the opposite of $F$ defined as the identity of the composition of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$ and the sheaf to presheaf of $J$ and $A$.

CategoryTheory.Functor.sheafPushforwardContinuousIddefMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

the sheaf pushforward continuous identity of A and J (from the name)

English

Let $A$ be a set. Let $J$ be a Grothendieck topology of $C$. Then the sheaf pushforward continuous identity of $A$ and $J$ is an isomorphism of $\operatorname{sheafPushforwardContinuous}$ applied to the identity of $C$, $A$, $J$ and $J$ and the identity of the set of sheaves of $J$ and $A$ defined as the identity of $\operatorname{sheafPushforwardContinuous}$ applied to the identity of $C$, $A$, $J$ and $J$.

CategoryTheory.Functor.sheafPushforwardContinuousId'defMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

the sheaf pushforward continuous identity of A and #3 (from the name)

English

Let $\mathrm{eF''}$ be an isomorphism of $\mathrm{F''}$ and the identity of $C$. Let $A$ be a set. Let $J$ be a Grothendieck topology of $C$. Then the sheaf pushforward continuous identity of $\mathrm{eF''}$ and $J$ is an isomorphism of $\operatorname{sheafPushforwardContinuous}$ applied to $\mathrm{F''}$, $A$, $J$ and $J$ and the identity of the set of sheaves of $J$ and $A$ defined as the composition of the sheaf pushforward continuous isomorphism of $J$ and $J$ and the sheaf pushforward continuous identity of $A$ and $J$.

CategoryTheory.Functor.sheafPushforwardContinuousIsodefMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

the sheaf pushforward continuous isomorphism of J and K (from the name)

English

Let $e$ be an isomorphism of $F$ and $\mathrm{F'}$. Let $A$ be a set. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Then the sheaf pushforward continuous isomorphism of $J$ and $K$ is an isomorphism of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$ and $\operatorname{sheafPushforwardContinuous}$ applied to $\mathrm{F'}$, $A$, $J$ and $K$.

CategoryTheory.Functor.sheafPushforwardContinuousNatTransdefMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

the sheaf pushforward continuous natural transformation of J and K (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $\mathrm{F'}$. Let $A$ be a set. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Then the sheaf pushforward continuous natural transformation of $J$ and $K$ is a homomorphism of $\operatorname{sheafPushforwardContinuous}$ applied to $\mathrm{F'}$, $A$, $J$ and $K$ and $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$.

CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedByclassMathlib.CategoryTheory.Sites.Continuous, predicate

Wording

no wording

English

Let $E$ be an one hypercover of $J$ and $X$. Let $F$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Then we can say that $\operatorname{IsPreservedBy}$ holds for $E$, $F$ and $K$.

CategoryTheory.GrothendieckTopology.OneHypercover.mapdefMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

the map of F and K (from the name)

English

Let $E$ be an one hypercover of $J$ and $X$. 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 an one hypercover of $K$ and the action of $F$ and $X$ defined as $\operatorname{mk}$ applied to the map of $\operatorname{toPreOneHypercover}$ applied to $E$ and $F$, $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_OneHypercover\_\_IsPreservedBy\_\_mem\_u2080\_}$ and the function that maps $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$ and $h_{1}$ to $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_OneHypercover\_\_IsPreservedBy\_\_mem\_u2081\_}$ applied to $x_{2}$, $x_{3}$, $x_{5}$, $x_{6}$ and $h_{1}$.

CategoryTheory.PreOneHypercover.isLimitMapMultiforkEquivdefMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

no wording

English

Let $E$ be an one hypercover of $X$. Let $F$ be a functor of $C$ and $D$. Let $P$ be a functor of the set of opposites of $D$ and $A$. Then $\operatorname{isLimitMapMultiforkEquiv}$ applied to $E$, $F$ and $P$ is an equivalence from $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of the map of $E$ and $F$ and $P$ to $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $E$ and the composition of the opposite of $F$ and $P$ defined as the identity of $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of the map of $E$ and $F$ and $P$.

CategoryTheory.PreOneHypercover.mapdefMathlib.CategoryTheory.Sites.Continuous, function or constant

Wording

the map of E and F (from the name)

English

Let $E$ be an one hypercover of $X$. Let $F$ be a functor of $C$ and $D$. Then the map of $E$ and $F$ is an one hypercover of the action of $F$ and $X$.

Mathlib.CategoryTheory.Sites.CoproductSheafCondition

CategoryTheory.PreZeroHypercover.isLimitSigmaOfIsColimitEquivdefMathlib.CategoryTheory.Sites.CoproductSheafCondition, function or constant

Wording

no wording

English

Let $E$ be a zero hypercover of $S$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Assume that $c$ is a universal colimit. Let $F$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{isLimitSigmaOfIsColimitEquiv}$ applied to $E$, $\mathrm{hc}$, $\mathrm{huniv}$ and $F$ is an equivalence from $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of the one hypercover of the sigma of $E$ and $\mathrm{hc}$ and $F$ to $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of the one hypercover of $E$ and $F$.

Mathlib.CategoryTheory.Sites.CoverLifting

CategoryTheory.Functor.IsCocontinuousclassMathlib.CategoryTheory.Sites.CoverLifting, predicate

Wording

no wording

English

Let $G$ be a functor of $C$ and $D$. Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Then we can say that $\operatorname{IsCocontinuous}$ holds for $G$, $J$ and $K$.

CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibilitydefMathlib.CategoryTheory.Sites.CoverLifting, function or constant

Wording

the pushforward continuous sheafification compatibility 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 pushforward continuous sheafification compatibility of $J$ and $K$ is an isomorphism of the composition of the action of the left whiskering of the set of opposites of $D$ and $A$ and the opposite of $G$ and the presheaf to sheaf of $J$ and $A$ and the composition of the presheaf to sheaf of $K$ and $A$ and $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$ defined as $\operatorname{leftAdjointUniq}$ applied to the composition of $\operatorname{ranAdjunction}$ applied to the opposite of $G$ and $A$ and the sheafification adjunction of $J$ and $A$ and the composition of the sheafification adjunction of $K$ and $A$ and $\operatorname{sheafAdjunctionCocontinuous}$ applied to $G$, $A$, $J$ and $K$.

CategoryTheory.Functor.sheafAdjunctionCocontinuousdefMathlib.CategoryTheory.Sites.CoverLifting, function or constant

Wording

no wording

English

generation took over the time limit

CategoryTheory.Functor.sheafPushforwardCocontinuousdefMathlib.CategoryTheory.Sites.CoverLifting, function or constant

Wording

no wording

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 $\operatorname{sheafPushforwardCocontinuous}$ applied to $G$, $A$, $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 lift of $\operatorname{IsSheaf}$ applied to $K$ and the composition of the sheaf to presheaf of $J$ and $A$ and $\operatorname{ran}$ applied to the opposite of $G$.

CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIsodefMathlib.CategoryTheory.Sites.CoverLifting, function or constant

Wording

the sheaf pushforward cocontinuous composition sheaf to presheaf 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 pushforward cocontinuous composition sheaf to presheaf isomorphism of $J$ and $K$ is an isomorphism of the composition of $\operatorname{sheafPushforwardCocontinuous}$ applied to $G$, $A$, $J$ and $K$ and the sheaf to presheaf of $K$ and $A$ and the composition of the sheaf to presheaf of $J$ and $A$ and $\operatorname{ran}$ applied to the opposite of $G$ defined as the identity of the composition of $\operatorname{sheafPushforwardCocontinuous}$ applied to $G$, $A$, $J$ and $K$ and the sheaf to presheaf of $K$ and $A$.

Mathlib.CategoryTheory.Sites.CoverPreserving

CategoryTheory.CompatiblePreservingstructureMathlib.CategoryTheory.Sites.CoverPreserving, predicate

Wording

no wording

English

Let $K$ be a Grothendieck topology of $D$. Let $G$ be a functor of $C$ and $D$. Then we can say that $\operatorname{CompatiblePreserving}$ holds for $K$ and $G$.

CategoryTheory.CoverPreservingstructureMathlib.CategoryTheory.Sites.CoverPreserving, predicate

Wording

no wording

English

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $G$ be a functor of $C$ and $D$. Then we can say that $\operatorname{CoverPreserving}$ holds for $J$, $K$ and $G$.

Mathlib.CategoryTheory.Sites.Coverage

CategoryTheory.CoveragestructureMathlib.CategoryTheory.Sites.Coverage, type

Wording

coverage of C (from the name)

English

Let $C$ be a set. Then the coverages of $C$ are a basic type.

CategoryTheory.Coverage.Saturate.belowinductiveMathlib.CategoryTheory.Sites.Coverage, predicate

Wording

no wording

English

Assume that $\operatorname{Saturate}$ holds for $K$, $X$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.

CategoryTheory.Coverage.gidefMathlib.CategoryTheory.Sites.Coverage, function or constant

Wording

no wording

English

Let $C$ be a set. Then $\operatorname{gi}$ applied to $C$ is a Galois insertion of $\operatorname{toGrothendieck}$ and $\operatorname{toCoverage}$.

CategoryTheory.Coverage.toGrothendieckdefMathlib.CategoryTheory.Sites.Coverage, function or constant

Wording

no wording

English

Let $K$ be a coverage of $C$. Then $\operatorname{toGrothendieck}$ applied to $K$ is a Grothendieck topology of $C$.

CategoryTheory.GrothendieckTopology.toCoveragedefMathlib.CategoryTheory.Sites.Coverage, function or constant

Wording

the coverage of J (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Then the coverage of $J$ is a coverage of $C$.

CategoryTheory.Precoverage.toCoveragedefMathlib.CategoryTheory.Sites.Coverage, function or constant

Wording

the coverage of J (from the name)

English

Let $J$ be a precoverage of $C$. Then the coverage of $J$ is a coverage of $C$.

CategoryTheory.Presieve.FactorsThrudefMathlib.CategoryTheory.Sites.Coverage, predicate

Wording

no wording

English

Let $S$ and $T$ be presieves of $X$. Then $\operatorname{FactorsThru}$ holds for $S$ and $T$, if for all elements $Z$ of $C$, for all homomorphisms $g$ of $Z$ and $X$, if $S$ holds for $Z$ and $g$, then there exists an element $W$ of $C$, such that there exists a homomorphism $i$ of $Z$ and $W$, such that there exists a homomorphism $e$ of $W$ and $X$, such that $T$ holds for $W$ and $e$ and the composition of $i$ and $e$ is equal to $g$.

CategoryTheory.Presieve.FactorsThruAlongdefMathlib.CategoryTheory.Sites.Coverage, predicate

Wording

no wording

English

Let $S$ be a presieve of $Y$. Let $T$ be a presieve of $X$. Let $f$ be a homomorphism of $Y$ and $X$. Then $\operatorname{FactorsThruAlong}$ holds for $S$, $T$ and $f$, if for all elements $Z$ of $C$, for all homomorphisms $g$ of $Z$ and $Y$, if $S$ holds for $Z$ and $g$, then there exists an element $W$ of $C$, such that there exists a homomorphism $i$ of $Z$ and $W$, such that there exists a homomorphism $e$ of $W$ and $X$, such that $T$ holds for $W$ and $e$ and the composition of $i$ and $e$ is equal to the composition of $g$ and $f$.

CategoryTheory.Pretopology.toCoveragedefMathlib.CategoryTheory.Sites.Coverage, function or constant

Wording

the coverage of J (from the name)

English

Let $J$ be a pretopology of $C$. Then the coverage of $J$ is a coverage of $C$.

Mathlib.CategoryTheory.Sites.CoversTop.Basic

CategoryTheory.GrothendieckTopology.CoversTopdefMathlib.CategoryTheory.Sites.CoversTop.Basic, predicate

Wording

no wording

English

Let $J$ be a Grothendieck topology of $C$. Let $Y$ be a function from elements of $I$ to elements of $C$. Then $\operatorname{CoversTop}$ holds for $J$ and $Y$, if for all elements $X$ of $C$, the sieve of $Y$ and $X$ is an element of $J$ applied to $X$.

CategoryTheory.GrothendieckTopology.CoversTop.coverdefMathlib.CategoryTheory.Sites.CoversTop.Basic, function or constant

Wording

the cover of hY and W (from the docstring)

English

Assume that $\operatorname{CoversTop}$ holds for $J$ and $Y$. Let $W$ be an element of $C$. Then the cover of $\mathrm{hY}$ and $W$ is a cover of $J$ and $W$ defined as the sieve of $Y$ and $W$.

CategoryTheory.Presheaf.FamilyOfElementsOnObjectsdefMathlib.CategoryTheory.Sites.CoversTop.Basic, type

Wording

family of element on object of F and Y (from the name)

English

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Let $Y$ be a function from elements of $I$ to elements of $C$. Then a family of element on object of $F$ and $Y$ is an element of the function that maps $F$ and $Y$ to the set of functions from elements $i$ of $I$ to elements of the action of $F$ and $\operatorname{op}$ applied to $Y$ applied to $i$.

CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatibledefMathlib.CategoryTheory.Sites.CoversTop.Basic, predicate

Wording

x1 is compatible (from the docstring)

English

Let $x_{1}$ be a family of element on object of $F$ and $Y$. Then $x_{1}$ is compatible, if for all elements $Z$ of $C$, for all elements $i$ and $j$ of $I$, for all homomorphisms $f$ of $Z$ and $Y$ applied to $i$, for all homomorphisms $g$ of $Z$ and $Y$ applied to $j$, $\operatorname{hom}$ applied to the map of $F$ and the opposite in $f$ and $x_{1}$ applied to $i$ is equal to $\operatorname{hom}$ applied to the map of $F$ and the opposite in $g$ and $x_{1}$ applied to $j$.

CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.section_defMathlib.CategoryTheory.Sites.CoversTop.Basic, function or constant

Wording

the section of hY and hF (from the name)

English

Assume that $x_{1}$ is compatible. Assume that $\operatorname{CoversTop}$ holds for $J$ and $Y$. Assume that $\operatorname{IsSheaf}$ holds for $J$ and $F$. Then the section of $\mathrm{hY}$ and $\mathrm{hF}$ is an element of the section of $F$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Presheaf\_\_FamilyOfElementsOnObjects\_\_IsCompatible\_\_existsUnique\_section}$ applied to $\mathrm{hx}$, $\mathrm{hY}$ and $\mathrm{hF}$.

CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElementsdefMathlib.CategoryTheory.Sites.CoversTop.Basic, function or constant

Wording

the family of x1 and X (from the name)

English

Let $x_{1}$ be a family of element on object of $F$ and $Y$. Let $X$ be an element of $C$. Then the family of $x_{1}$ and $X$ is a family of element of $F$ and the arrow of the sieve of $Y$ and $X$.

Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

CategoryTheory.Functor.IsCoverDenseclassMathlib.CategoryTheory.Sites.DenseSubsite.Basic, predicate

Wording

no wording

English

Let $G$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Then we can say that $\operatorname{IsCoverDense}$ holds for $G$ and $K$.

CategoryTheory.Functor.IsCoverDense.Types.appHomdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the application homomorphism of x4 and X (from the name)

English

Let $x_{4}$ be a homomorphism of the composition of the opposite of $G$ and $x_{2}$ and the composition of the opposite of $G$ and the object of $x_{3}$. Let $X$ be an element of $D$. Then the application homomorphism of $x_{4}$ and $X$ is a homomorphism of the action of $x_{2}$ and $\operatorname{op}$ applied to $X$ and the action of the object of $x_{3}$ and $\operatorname{op}$ applied to $X$.

CategoryTheory.Functor.IsCoverDense.Types.appIsodefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the application isomorphism of i and X (from the name)

English

Let $i$ be an isomorphism of the composition of the opposite of $G$ and the object of $x_{2}$ and the composition of the opposite of $G$ and the object of $x_{3}$. Let $X$ be an element of $D$. Then the application isomorphism of $i$ and $X$ is an isomorphism of the action of the object of $x_{2}$ and $\operatorname{op}$ applied to $X$ and the action of the object of $x_{3}$ and $\operatorname{op}$ applied to $X$.

CategoryTheory.Functor.IsCoverDense.Types.presheafHomdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the presheaf homomorphism of x4 (from the name)

English

Let $x_{4}$ be a homomorphism of the composition of the opposite of $G$ and $x_{2}$ and the composition of the opposite of $G$ and the object of $x_{3}$. Then the presheaf homomorphism of $x_{4}$ is a homomorphism of $x_{2}$ and the object of $x_{3}$.

CategoryTheory.Functor.IsCoverDense.Types.presheafIsodefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the presheaf isomorphism of i (from the name)

English

Let $i$ be an isomorphism of the composition of the opposite of $G$ and the object of $x_{2}$ and the composition of the opposite of $G$ and the object of $x_{3}$. Then the presheaf isomorphism of $i$ is an isomorphism of the object of $x_{2}$ and the object of $x_{3}$.

CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamilydefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the pushforward family of x4 and x5 (from the name)

English

Let $x_{4}$ be a homomorphism of the composition of the opposite of $G$ and $x_{2}$ and the composition of the opposite of $G$ and the object of $x_{3}$. Let $x_{5}$ be an element of the action of $x_{2}$ and $\operatorname{op}$ applied to $X$. Then the pushforward family of $x_{4}$ and $x_{5}$ is a family of element of the object of $x_{3}$ and the cover by image of $G$ and $X$ defined as the function that maps $x_{6}$, $x_{7}$ and $\mathrm{hf}$ to $\operatorname{hom}$ applied to the map of the object of $x_{3}$ and the opposite in the lift of $\operatorname{some}$ applied to $\mathrm{hf}$ and $\operatorname{hom}$ applied to the component of $x_{4}$ and $\operatorname{op}$ applied to $\operatorname{proj0}$ applied to $\operatorname{some}$ applied to $\mathrm{hf}$ and $\operatorname{hom}$ applied to the map of $x_{2}$ and the opposite in the map of $\operatorname{some}$ applied to $\mathrm{hf}$ and $x_{5}$.

CategoryTheory.Functor.IsCoverDense.Types.sheafIsodefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the sheaf isomorphism of i (from the name)

English

generation took over the time limit

CategoryTheory.Functor.IsCoverDense.homOverdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

no wording

English

Let $x_{5}$ be a homomorphism of the composition of the opposite of $G$ and $x_{3}$ and the composition of the opposite of $G$ and the object of $x_{4}$. Let $X$ be an element of $A$. Then $\operatorname{homOver}$ applied to $x_{5}$ and $X$ is a homomorphism of the composition of the opposite of $G$ and the composition of $x_{3}$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and the composition of the opposite of $G$ and the object of $\operatorname{sheafOver}$ applied to $x_{4}$ and $X$ defined as the right whisker of $x_{5}$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$.

CategoryTheory.Functor.IsCoverDense.isoOverdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

no wording

English

Let $x_{5}$ be an isomorphism of the composition of the opposite of $G$ and the object of $x_{3}$ and the composition of the opposite of $G$ and the object of $x_{4}$. Let $X$ be an element of $A$. Then $\operatorname{isoOver}$ applied to $x_{5}$ and $X$ is an isomorphism of the composition of the opposite of $G$ and the object of $\operatorname{sheafOver}$ applied to $x_{3}$ and $X$ and the composition of the opposite of $G$ and the object of $\operatorname{sheafOver}$ applied to $x_{4}$ and $X$ defined as the right isomorphism whisker of $x_{5}$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$.

CategoryTheory.Functor.IsCoverDense.presheafIsodefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the presheaf isomorphism of i (from the name)

English

Let $i$ be an isomorphism of the composition of the opposite of $G$ and the object of $x_{3}$ and the composition of the opposite of $G$ and the object of $x_{4}$. Then the presheaf isomorphism of $i$ is an isomorphism of the object of $x_{3}$ and the object of $x_{4}$ defined as $\operatorname{asIso}$ applied to the sheaf homomorphism of the homomorphism of $i$.

CategoryTheory.Functor.IsCoverDense.restrictHomEquivHomdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

no wording

English

$\operatorname{restrictHomEquivHom}$ is an equivalence from the set of homomorphisms of the composition of the opposite of $G$ and $x_{3}$ and the composition of the opposite of $G$ and the object of $x_{4}$ to the set of homomorphisms of $x_{3}$ and the object of $x_{4}$ defined as $\operatorname{mk}$ applied to $\operatorname{sheafHom}$, $\operatorname{whiskerLeft}$ applied to the opposite of $G$, $\mathrm{CategoryTheory\_\_Functor\_\_IsCoverDense\_\_sheafHom\_restrict\_eq}$ and $\mathrm{CategoryTheory\_\_Functor\_\_IsCoverDense\_\_sheafHom\_eq}$ applied to $G$.

CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHomdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the sheaf Coyoneda homomorphism of x5 (from the name)

English

Let $x_{5}$ be a homomorphism of the composition of the opposite of $G$ and $x_{3}$ and the composition of the opposite of $G$ and the object of $x_{4}$. Then the sheaf Coyoneda homomorphism of $x_{5}$ is a homomorphism of the composition of the Coyoneda and the action of the left whiskering of $A$ and the set of sets and $x_{3}$ and the composition of the Coyoneda and the action of the left whiskering of $A$ and the set of sets and the object of $x_{4}$.

CategoryTheory.Functor.IsCoverDense.sheafHomdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the sheaf homomorphism of x5 (from the name)

English

Let $x_{5}$ be a homomorphism of the composition of the opposite of $G$ and $x_{3}$ and the composition of the opposite of $G$ and the object of $x_{4}$. Then the sheaf homomorphism of $x_{5}$ is a homomorphism of $x_{3}$ and the object of $x_{4}$.

CategoryTheory.Functor.IsCoverDense.sheafIsodefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the sheaf isomorphism of i (from the name)

English

generation took over the time limit

CategoryTheory.Functor.IsCoverDense.sheafYonedaHomdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the sheaf Yoneda homomorphism of x5 (from the name)

English

Let $x_{5}$ be a homomorphism of the composition of the opposite of $G$ and $x_{3}$ and the composition of the opposite of $G$ and the object of $x_{4}$. Then the sheaf Yoneda homomorphism of $x_{5}$ is a homomorphism of the composition of $x_{3}$ and the Yoneda and the composition of the object of $x_{4}$ and the Yoneda.

CategoryTheory.Functor.IsDenseSubsiteclassMathlib.CategoryTheory.Sites.DenseSubsite.Basic, predicate

Wording

no wording

English

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $G$ be a functor of $C$ and $D$. Then we can say that $\operatorname{IsDenseSubsite}$ holds for $J$, $K$ and $G$.

CategoryTheory.Functor.IsDenseSubsite.mapPreimagedefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the map preimage of F and f (from the name)

English

Let $K$ be a Grothendieck topology of $D$. Let $G$ be a functor of $C$ and $D$. Let $F$ be a sheaf of $J$ and $A$. Let $f$ be a homomorphism of the action of $G$ and $X$ and the action of $G$ and $Y$. Then the map preimage of $F$ and $f$ is a homomorphism of the action of the object of $F$ and $\operatorname{op}$ applied to $Y$ and the action of the object of $F$ and $\operatorname{op}$ applied to $X$.

CategoryTheory.Functor.IsDenseSubsite.sheafEquivdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the sheaf equivalence of K and G (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $G$ be a functor of $C$ and $D$. Let $A$ be a set. Then the sheaf equivalence of $K$ and $G$ is an equivalence of the set of sheaves of $J$ and $A$ and the set of sheaves of $K$ and $A$ defined as the inverse of $\operatorname{asEquivalence}$ applied to $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$.

CategoryTheory.Functor.IsDenseSubsite.sheafEquivSheafificationCompatibilitydefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the sheaf equivalence sheafification compatibility of K and G (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $G$ be a functor of $C$ and $D$. Let $A$ be a set. Then the sheaf equivalence sheafification compatibility of $K$ and $G$ is an isomorphism of the composition of the action of the left whiskering of the set of opposites of $D$ and $A$ and the opposite of $G$ and the presheaf to sheaf of $J$ and $A$ and the composition of the presheaf to sheaf of $K$ and $A$ and the inverse of the sheaf equivalence of $K$ and $G$ defined as the composition of the inverse of the sheafification of $K$ and $G$ and the right isomorphism whisker of $\operatorname{leftAdjointUniq}$ applied to the sheafification adjunction of $K$ and $G$ and the sheafification adjunction of $K$ and $A$ and $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$.

CategoryTheory.Functor.IsDenseSubsite.sheafifyAdjunctionOfIsEquivalencedefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the sheafification adjunction of K and G (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $G$ be a functor of $C$ and $D$. Let $A$ be a set. Then the sheafification adjunction of $K$ and $G$ is an adjunction of the sheafification of $K$ and $G$ and the sheaf to presheaf of $K$ and $A$.

CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalencedefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the sheafification of K and G (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $G$ be a functor of $C$ and $D$. Let $A$ be a set. Then the sheafification of $K$ and $G$ is a functor of the set of functors of the set of opposites of $D$ and $A$ and the set of sheaves of $K$ and $A$ defined as the composition of the action of the left whiskering of the set of opposites of $D$ and $A$ and the opposite of $G$ and the composition of the presheaf to sheaf of $J$ and $A$ and the inverse of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$.

CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalenceCompIsodefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the sheafification of K and G (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $G$ be a functor of $C$ and $D$. Let $A$ be a set. Then the sheafification of $K$ and $G$ is an isomorphism of the composition of the sheafification of $K$ and $G$ and $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ 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 $G$ and the presheaf to sheaf of $J$ and $A$ defined as the composition of the associator of the composition of the presheaf to sheaf of $J$ and $A$ and the inverse of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$ and $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$ and the composition of the left isomorphism whisker of the action of the left whiskering of the set of opposites of $D$ and $A$ and the opposite of $G$ and the associator of the inverse of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$ and $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$ and the left isomorphism whisker of the action of the left whiskering of the set of opposites of $D$ and $A$ and the opposite of $G$ and the composition of the left isomorphism whisker of the presheaf to sheaf of $J$ and $A$ and the counit isomorphism of $\operatorname{asEquivalence}$ applied to $\operatorname{sheafPushforwardContinuous}$ applied to $G$, $A$, $J$ and $K$ and the right unitor of the presheaf to sheaf of $J$ and $A$.

CategoryTheory.Presieve.CoverByImageStructure.liftdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the lift of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{CoverByImageStructure}$ applied to $G$ and $f$. Then the lift of $\mathrm{self}$ is a homomorphism of $V$ and the action of $G$ and the object of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Presieve.CoverByImageStructure.mapdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the map of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{CoverByImageStructure}$ applied to $G$ and $f$. Then the map of $\mathrm{self}$ is a homomorphism of the action of $G$ and the object of $\mathrm{self}$ and $U$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.Presieve.CoverByImageStructure.objdefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the object of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{CoverByImageStructure}$ applied to $G$ and $f$. Then the object of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Presieve.coverByImagedefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the cover by image of G and U (from the name)

English

Let $G$ be a functor of $C$ and $D$. Let $U$ be an element of $D$. Then the cover by image of $G$ and $U$ is a presieve of $U$ defined as the function that maps $x_{2}$ and $f$ to $\mathrm{Nonempty}$ applied to $\operatorname{CoverByImageStructure}$ applied to $G$ and $f$.

CategoryTheory.Sieve.coverByImagedefMathlib.CategoryTheory.Sites.DenseSubsite.Basic, function or constant

Wording

the cover by image of G and U (from the name)

English

Let $G$ be a functor of $C$ and $D$. Let $U$ be an element of $D$. Then the cover by image of $G$ and $U$ is a sieve of $U$.

Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

CategoryTheory.Functor.LocallyCoverDenseclassMathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology, predicate

Wording

no wording

English

Let $G$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Then we can say that $\operatorname{LocallyCoverDense}$ holds for $G$ and $K$.

CategoryTheory.Functor.sheafInducedTopologyEquivOfIsCoverDensedefMathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology, function or constant

Wording

the sheaf induced topology equivalence of G and K (from the name)

English

Let $G$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Let $A$ be a set. Then the sheaf induced topology equivalence of $G$ and $K$ is an equivalence of the set of sheaves of the induced topology of $G$ and $K$ and $A$ and the set of sheaves of $K$ and $A$ defined as the sheaf equivalence of $K$ and $G$.

Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

CategoryTheory.Functor.IsOneHypercoverDenseclassMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, predicate

Wording

no wording

English

Let $F$ be a functor of $x$ and $C$. Let $x_{3}$ be a Grothendieck topology of $x$. Let $J$ be a Grothendieck topology of $C$. Then we can say that $\operatorname{IsOneHypercoverDense}$ holds for $F$, $x_{3}$ and $J$.

CategoryTheory.Functor.OneHypercoverDenseDatastructureMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, type

Wording

one hypercover dense data of J and S (from the name)

English

Let $F$ be a functor of $x$ and $C$. Let $x_{3}$ be a Grothendieck topology of $x$. Let $J$ be a Grothendieck topology of $C$. Let $S$ be an element of $C$. Then the one hypercover dense data of $J$ and $S$ are a basic type.

CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.i₀defMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{SieveStruct}$ applied to $\mathrm{data}$, $f$ and $g$. Then $\mathrm{CategoryTheory\_\_Functor\_\_OneHypercoverDenseData\_\_SieveStruct\_\_i\_u2080\_}$ applied to $\mathrm{self}$ is an element of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2080\_}$ applied to $\operatorname{toPreOneHypercoverDenseData}$ applied to $\mathrm{data}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.qdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{SieveStruct}$ applied to $\mathrm{data}$, $f$ and $g$. Then $\operatorname{q}$ applied to $\mathrm{self}$ is a homomorphism of the action of $F$ and $x_{5}$ and the action of $F$ and $\operatorname{X}$ applied to $\operatorname{toPreOneHypercoverDenseData}$ applied to $\mathrm{data}$ and $\mathrm{CategoryTheory\_\_Functor\_\_OneHypercoverDenseData\_\_SieveStruct\_\_i\_u2080\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.compPresheafIsodefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the presheaf of data and X (from the docstring)

English

Let $\mathrm{data}$ be a function from elements $X$ of $C$ to one hypercover dense data of $J$ and $X$. Let $x_{5}$ be a sheaf of $x_{3}$ and $A$. Then the presheaf of $X$ and $\mathrm{data}$ is an isomorphism of the composition of the opposite of $F$ and the presheaf of $\mathrm{data}$ and $x_{5}$ and the object of $x_{5}$.

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the presheaf of data and X (from the name)

English

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the presheaf object of X1 and x5 (from the name)

English

Let $\mathrm{data}$ be a function from elements $X_{1}$ of $C$ to one hypercover dense data of $J$ and $X_{1}$. Let $x_{5}$ be a sheaf of $x_{3}$ and $A$. Let $X$ be an element of $C$. Then the presheaf object of $\mathrm{data}$ and $x_{5}$ is an element of $A$ defined as the function that maps $X$ to the multiequalizer of the multicospan index of $\operatorname{toPreOneHypercoverDenseData}$ applied to $X_{1}$ applied to $x_{5}$ and the object of $\mathrm{data}$.

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjIsLimitdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

no wording

English

Let $\mathrm{data}$ be a function from elements $X_{1}$ of $C$ to one hypercover dense data of $J$ and $X_{1}$. Let $x_{5}$ be a sheaf of $x_{3}$ and $A$. Let $X$ be an element of $C$. Then $\operatorname{presheafObjIsLimit}$ applied to $X_{1}$, $\mathrm{data}$, $x_{5}$ and $X$ is an element of $\operatorname{IsLimit}$ applied to the presheaf object multifork of $x_{5}$ and $X$.

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjMultiforkdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the presheaf object multifork of X1 and x5 (from the name)

English

Let $\mathrm{data}$ be a function from elements $X_{1}$ of $C$ to one hypercover dense data of $J$ and $X_{1}$. Let $x_{5}$ be a sheaf of $x_{3}$ and $A$. Let $X$ be an element of $C$. Then the presheaf object multifork of $\mathrm{data}$ and $x_{5}$ is a multifork of the multicospan index of $\operatorname{toPreOneHypercoverDenseData}$ applied to $\mathrm{data}$ applied to $X$ and the object of $x_{5}$.

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIsodefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the presheaf object object isomorphism of X and x5 (from the name)

English

Let $\mathrm{data}$ be a function from elements $X$ of $C$ to one hypercover dense data of $J$ and $X$. Let $x_{5}$ be a sheaf of $x_{3}$ and $A$. Let $x_{6}$ be an element of $x$. Then the presheaf object object isomorphism of $\mathrm{data}$ and $x_{5}$ is an isomorphism of the action of the presheaf of $\mathrm{data}$ and $x_{5}$ and $\operatorname{op}$ applied to the action of $F$ and $x_{6}$ and the action of the object of $x_{5}$ and $\operatorname{op}$ applied to $x_{6}$.

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the presheaf object projection of x5 and X (from the name)

English

Let $\mathrm{data}$ be a function from elements $X_{1}$ of $C$ to one hypercover dense data of $J$ and $X_{1}$. Let $x_{5}$ be a sheaf of $x_{3}$ and $A$. Let $X$ be an element of $C$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2080\_}$ applied to $\operatorname{toPreOneHypercoverDenseData}$ applied to $\mathrm{data}$ applied to $X$. Then the presheaf object projection of $x_{5}$ and $X$ is a homomorphism of the presheaf object of $x_{5}$ and $X$ and the action of the object of $x_{5}$ and $\operatorname{op}$ applied to $\operatorname{X}$ applied to $\operatorname{toPreOneHypercoverDenseData}$ applied to $\mathrm{data}$ applied to $X$ and $i$ defined as the function that maps $i$ to the inclusion of the multicospan index of $\operatorname{toPreOneHypercoverDenseData}$ applied to $X_{1}$ applied to $x_{5}$ and the object of $\mathrm{data}$ and $X$.

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restrictiondefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the restriction of X1 and x5 (from the name)

English

Let $\mathrm{data}$ be a function from elements $X_{1}$ of $C$ to one hypercover dense data of $J$ and $X_{1}$. Let $x_{5}$ be a sheaf of $x_{3}$ and $A$. Let $f$ be a homomorphism of the action of $F$ and $x_{6}$ and $X$. Then the restriction of $\mathrm{data}$ and $x_{5}$ is a homomorphism of the presheaf object of $x_{5}$ and $X$ and the action of the object of $x_{5}$ and $\operatorname{op}$ applied to $x_{6}$.

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.sheafdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the sheaf of data and X (from the name)

English

Let $\mathrm{data}$ be a function from elements $X$ of $C$ to one hypercover dense data of $J$ and $X$. Let $x_{5}$ be a sheaf of $x_{3}$ and $A$. Then the sheaf of $X$ and $\mathrm{data}$ is a sheaf of $J$ and $A$ defined as the function that maps $x_{5}$ to $\operatorname{mk}$ applied to the presheaf of $X$ and $\mathrm{data}$, $\operatorname{isSheaf}$ applied to $X$ and $\mathrm{data}$ and $x_{5}$.

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.sheafIsodefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the sheaf of data and X (from the docstring)

English

generation took over the time limit

CategoryTheory.Functor.OneHypercoverDenseData.sievedefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the sieve of data and f (from the name)

English

Let $\mathrm{data}$ be an one hypercover dense data of $J$ and $X$. Let $f$ be a homomorphism of the action of $F$ and $x_{4}$ and $X$. Then the sieve of $\mathrm{data}$ and $f$ is a sieve of $x_{4}$.

CategoryTheory.Functor.OneHypercoverDenseData.toOneHypercoverdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the one hypercover of data (from the name)

English

Let $\mathrm{data}$ be an one hypercover dense data of $J$ and $X$. Then the one hypercover of $\mathrm{data}$ is an one hypercover of $J$ and $X$ defined as $\operatorname{mk}$ applied to the one hypercover of $\operatorname{toPreOneHypercoverDenseData}$ applied to $\mathrm{data}$, $\mathrm{CategoryTheory\_\_Functor\_\_OneHypercoverDenseData\_\_mem\_u2080\_}$ applied to $\mathrm{data}$ and $\mathrm{CategoryTheory\_\_Functor\_\_OneHypercoverDenseData\_\_mem\_u2081\_}$ applied to $\mathrm{data}$.

CategoryTheory.Functor.PreOneHypercoverDenseDatastructureMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, type

Wording

one hypercover dense data of F and S (from the name)

English

Let $F$ be a functor of $x$ and $C$. Let $S$ be an element of $C$. Then the one hypercover dense data of $F$ and $S$ are a basic type.

CategoryTheory.Functor.PreOneHypercoverDenseData.I₀defMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, type

Wording

no wording

English

Let $\mathrm{self}$ be an one hypercover dense data of $F$ and $S$. Then an element of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2080\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Functor.PreOneHypercoverDenseData.I₁defMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, type

Wording

no wording

English

Let $\mathrm{self}$ be an one hypercover dense data of $F$ and $S$. Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2080\_}$ applied to $\mathrm{self}$. Then an element of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2081\_}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$ is an element of the function that maps $\mathrm{self}$, $x_{3}$ and $x_{4}$ to $\operatorname{proj3}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$.

CategoryTheory.Functor.PreOneHypercoverDenseData.I₁'defMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, type

Wording

no wording

English

Let $\mathrm{data}$ be an one hypercover dense data of $F$ and $X$. Then an element of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2081\_'}$ applied to $\mathrm{data}$ is an element of the function that maps $\mathrm{data}$ to $\Sigma$ applied to the function that maps $i$ to $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2081\_}$ applied to $\mathrm{data}$, $\ProdfstMACRoZ {i}$ and $\ProdsndMACRoAA {i}$.

CategoryTheory.Functor.PreOneHypercoverDenseData.XdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an one hypercover dense data of $F$ and $S$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2080\_}$ applied to $\mathrm{self}$. Then $\operatorname{X}$ applied to $\mathrm{self}$ and $i$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.

CategoryTheory.Functor.PreOneHypercoverDenseData.YdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an one hypercover dense data of $F$ and $S$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2081\_}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$. Then $\operatorname{Y}$ applied to $\mathrm{self}$ and $j$ is an element of $x$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$ and $j$.

CategoryTheory.Functor.PreOneHypercoverDenseData.fdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an one hypercover dense data of $F$ and $S$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2080\_}$ applied to $\mathrm{self}$. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $i$ is a homomorphism of the action of $F$ and $\operatorname{X}$ applied to $\mathrm{self}$ and $i$ and $S$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $i$.

CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndexdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the multicospan index of data and P (from the name)

English

Let $\mathrm{data}$ be an one hypercover dense data of $F$ and $X$. Let $P$ be a functor of the set of opposites of $x$ and $A$. Then the multicospan index of $\mathrm{data}$ and $P$ is a multicospan index of the multicospan shape of $\mathrm{data}$ and $A$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{X}$ applied to $\mathrm{data}$ and $i$, the function that maps $j$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{Y}$ applied to $\mathrm{data}$ and $\operatorname{snd}$ applied to $j$, the function that maps $j_{1}$ to the map of $P$ and the opposite in $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_p\_u2081\_}$ applied to $\mathrm{data}$ and $\operatorname{snd}$ applied to $j_{1}$ and the function that maps $j_{2}$ to the map of $P$ and the opposite in $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_p\_u2082\_}$ applied to $\mathrm{data}$ and $\operatorname{snd}$ applied to $j_{2}$.

CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMapdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the multicospan map of data and f (from the name)

English

Let $\mathrm{data}$ be an one hypercover dense data of $F$ and $X$. Let $f$ be a homomorphism of $P$ and $Q$. Then the multicospan map of $\mathrm{data}$ and $f$ is a homomorphism of the multicospan of the multicospan index of $\mathrm{data}$ and $P$ and the multicospan of the multicospan index of $\mathrm{data}$ and $Q$.

CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMapIsodefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the multicospan map isomorphism of data and e (from the name)

English

Let $\mathrm{data}$ be an one hypercover dense data of $F$ and $X$. Let $e$ be an isomorphism of $P$ and $Q$. Then the multicospan map isomorphism of $\mathrm{data}$ and $e$ is an isomorphism of the multicospan of the multicospan index of $\mathrm{data}$ and $P$ and the multicospan of the multicospan index of $\mathrm{data}$ and $Q$.

CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShapedefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the multicospan shape of data (from the name)

English

Let $\mathrm{data}$ be an one hypercover dense data of $F$ and $X$. Then the multicospan shape of $\mathrm{data}$ is a shape defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2080\_}$ applied to $\mathrm{data}$, $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2081\_'}$ applied to $\mathrm{data}$, the function that maps $j$ to $\ProdfstMACRoZ {\operatorname{fst} (j)}$ and the function that maps $j_{1}$ to $\ProdsndMACRoAA {\operatorname{fst} (j_{1})}$.

CategoryTheory.Functor.PreOneHypercoverDenseData.p₁defMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an one hypercover dense data of $F$ and $S$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2081\_}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$. Then $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_p\_u2081\_}$ applied to $\mathrm{self}$ and $j$ is a homomorphism of $\operatorname{Y}$ applied to $\mathrm{self}$ and $j$ and $\operatorname{X}$ applied to $\mathrm{self}$ and $x_{3}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$ and $j$.

CategoryTheory.Functor.PreOneHypercoverDenseData.p₂defMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an one hypercover dense data of $F$ and $S$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2081\_}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$. Then $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_p\_u2082\_}$ applied to $\mathrm{self}$ and $j$ is a homomorphism of $\operatorname{Y}$ applied to $\mathrm{self}$ and $j$ and $\operatorname{X}$ applied to $\mathrm{self}$ and $x_{4}$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$ and $j$.

CategoryTheory.Functor.PreOneHypercoverDenseData.sieve₁₀defMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the sieve of x6 and x7 (from the name)

English

Let $\mathrm{data}$ be an one hypercover dense data of $F$ and $X$. Let $x_{6}$ be a homomorphism of $x_{5}$ and $\operatorname{X}$ applied to $\mathrm{data}$ and $x_{3}$. Let $x_{7}$ be a homomorphism of $x_{5}$ and $\operatorname{X}$ applied to $\mathrm{data}$ and $x_{4}$. Then the sieve of $x_{6}$ and $x_{7}$ is a sieve of $x_{5}$.

CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercoverdefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the one hypercover of data (from the name)

English

Let $\mathrm{data}$ be an one hypercover dense data of $F$ and $X$. Then the one hypercover of $\mathrm{data}$ is an one hypercover of $X$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2080\_}$ applied to $\mathrm{data}$, the function that maps $i$ to the action of $F$ and $\operatorname{X}$ applied to $\mathrm{data}$ and $i$ and the function that maps $i_{1}$ to $\operatorname{f}$ applied to $\mathrm{data}$ and $i_{1}$, $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_I\_u2081\_}$ applied to $\mathrm{data}$, the function that maps $x_{3}$, $x_{4}$ and $j$ to the action of $F$ and $\operatorname{Y}$ applied to $\mathrm{data}$ and $j$, the function that maps $x_{5}$, $x_{6}$ and $j_{1}$ to the map of $F$ and $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_p\_u2081\_}$ applied to $\mathrm{data}$ and $j_{1}$, the function that maps $x_{7}$, $x_{8}$ and $j_{2}$ to the map of $F$ and $\mathrm{CategoryTheory\_\_Functor\_\_PreOneHypercoverDenseData\_\_p\_u2082\_}$ applied to $\mathrm{data}$ and $j_{2}$ and $\operatorname{w}$ applied to $\mathrm{data}$.

CategoryTheory.Functor.oneHypercoverDenseDatadefMathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense, function or constant

Wording

the one hypercover dense data of J and X (from the name)

English

Let $F$ be a functor of $x$ and $C$. Let $x_{3}$ be a Grothendieck topology of $x$. Let $J$ be a Grothendieck topology of $C$. Let $X$ be an element of $C$. Then the one hypercover dense data of $J$ and $X$ is an one hypercover dense data of $J$ and $X$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsOneHypercoverDense\_\_nonempty\_oneHypercoverDenseData}$ applied to $X$.

Mathlib.CategoryTheory.Sites.Descent.DescentData

CategoryTheory.Pseudofunctor.DescentDatastructureMathlib.CategoryTheory.Sites.Descent.DescentData, type

Wording

descent data of F and f (from the name)

English

CategoryTheory.Pseudofunctor.DescentData.HomstructureMathlib.CategoryTheory.Sites.Descent.DescentData, type

Wording

homomorphism of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be descent data of $F$ and $f$. Then the homomorphisms of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Pseudofunctor.DescentData.Hom.homdefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

the homomorphism of self and i (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $i$ be an element of $x_{1}$. Then the homomorphism of $\mathrm{self}$ and $i$ is a homomorphism of the object of $x_{2}$ and $i$ and the object of $x_{3}$ and $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

CategoryTheory.Pseudofunctor.DescentData.homdefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

the homomorphism of x4 and x5 (from the name)

English

Let $\mathrm{self}$ be a descent data of $F$ and $f$. Let $q$ be a homomorphism of $Y$ and $S$. Let $x_{4}$ be a homomorphism of $Y$ and $X$ applied to $x_{2}$. Let $x_{5}$ be a homomorphism of $Y$ and $X$ applied to $x_{3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{4}$ and $f$ applied to $x_{2}$ is equal to $q$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{5}$ and $f$ applied to $x_{3}$ is equal to $q$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_\_auto\_3}$. Then the homomorphism of $x_{4}$ and $x_{5}$ is a homomorphism of the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{4}$ and the object of $\mathrm{self}$ and $x_{2}$ and the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{5}$ and the object of $\mathrm{self}$ and $x_{3}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $q$, $x_{4}$, $x_{5}$, $h$ and $h_{1}$.

CategoryTheory.Pseudofunctor.DescentData.isodefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

the isomorphism of x4 and x5 (from the name)

English

Let $D$ be a descent data of $F$ and $f$. Let $q$ be a homomorphism of $Y$ and $S$. Let $x_{4}$ be a homomorphism of $Y$ and $X$ applied to $x_{2}$. Let $x_{5}$ be a homomorphism of $Y$ and $X$ applied to $x_{3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{4}$ and $f$ applied to $x_{2}$ is equal to $q$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_iso\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{5}$ and $f$ applied to $x_{3}$ is equal to $q$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_iso\_\_\_auto\_3}$. Then the isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{4}$ and the object of $D$ and $x_{2}$ and the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{5}$ and the object of $D$ and $x_{3}$.

CategoryTheory.Pseudofunctor.DescentData.isoMkdefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

the isomorphism of e and i (from the name)

English

Let $e$ be a function from elements $i$ of $x_{1}$ to isomorphisms of the object of $x_{2}$ and $i$ and the object of $x_{3}$ and $i$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $Y$ of $C$, for all homomorphisms $q$ of $Y$ and $S$, for all elements $x_{4}$ and $x_{5}$ of $x_{1}$, for all homomorphisms $x_{6}$ of $Y$ and $X$ applied to $x_{4}$, for all homomorphisms $x_{7}$ of $Y$ and $X$ applied to $x_{5}$, for all elements $h$ of $\mathrm{Proof}$ applied to the proposition that the composition of $x_{6}$ and $f$ applied to $x_{4}$ is equal to $q$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to the proposition that the composition of $x_{7}$ and $f$ applied to $x_{5}$ is equal to $q$, the composition of the map of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{6}$ and the homomorphism of $e$ applied to $x_{4}$ and the homomorphism of $x_{6}$ and $x_{7}$ is equal to the composition of the homomorphism of $x_{6}$ and $x_{7}$ and the map of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{7}$ and the homomorphism of $e$ applied to $x_{5}$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $i$ and $e$ is an isomorphism of $x_{2}$ and $x_{3}$.

CategoryTheory.Pseudofunctor.DescentData.objdefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

the object of self and i (from the name)

English

Let $\mathrm{self}$ be a descent data of $F$ and $f$. Let $i$ be an element of $x_{1}$. Then the object of $\mathrm{self}$ and $i$ is an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $X$ applied to $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

CategoryTheory.Pseudofunctor.DescentData.ofObjdefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

the descent data of M (from the name)

English

Let $M$ be an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$. Then the descent data of $M$ is a descent data of $F$ and $f$.

CategoryTheory.Pseudofunctor.DescentData.pullFunctordefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

no wording

English

CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIsodefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

no wording

English

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Assume that for all elements $j$ of $x_{2}$, the composition of $\mathrm{p'}$ applied to $j$ and $f$ applied to $x_{3}$ applied to $j$ is equal to the composition of $\mathrm{f'}$ applied to $j$ and $p$. Assume that for all elements $k_{2}$ of $x_{4}$, the composition of $\mathrm{q'}$ applied to $k_{2}$ and $\mathrm{f'}$ applied to $x_{5}$ applied to $k_{2}$ is equal to the composition of $\mathrm{f''}$ applied to $k_{2}$ and $q$. Let $r$ be a homomorphism of $\mathrm{S''}$ and $S$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $q$ and $p$ is equal to $r$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_pullFunctorCompIso\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that for all elements $k_{1}$ of $x_{4}$, the composition of $\mathrm{q'}$ applied to $k_{1}$ and $\mathrm{p'}$ applied to $x_{5}$ applied to $k_{1}$ is equal to $\mathrm{r'}$ applied to $k_{1}$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_pullFunctorCompIso\_\_\_auto\_3}$. Then $\operatorname{pullFunctorCompIso}$ applied to $F$, $w$, $\mathrm{w'}$, $r$, $\mathrm{hr}$ and $\mathrm{hr'}$ is an isomorphism of the composition of $\operatorname{pullFunctor}$ applied to $F$ and $w$ and $\operatorname{pullFunctor}$ applied to $F$ and $\mathrm{w'}$ and $\operatorname{pullFunctor}$ applied to $F$ and the function that maps $k$ to $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_pullFunctorCompIso\_\_\_proof\_5}$ applied to $w$, $\mathrm{w'}$, $r$, $\mathrm{hr}$, $\mathrm{hr'}$ and $k$.

CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalencedefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

no wording

English

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $e$ be an isomorphism of $\mathrm{S'}$ and $S$ such that for all elements $j$ of $x_{2}$, the composition of $\mathrm{p'}$ applied to $j$ and $f$ applied to $x_{3}$ applied to $j$ is equal to the composition of $\mathrm{f'}$ applied to $j$ and the homomorphism of $e$ and for all elements $i$ of $x_{1}$, the composition of $\mathrm{q'}$ applied to $i$ and $\mathrm{f'}$ applied to $x_{4}$ applied to $i$ is equal to the composition of $f$ applied to $i$ and the inverse of $e$. Then $\operatorname{pullFunctorEquivalence}$ applied to $F$, $e$, $w$ and $\mathrm{w'}$ is an equivalence of the set of descent data of $F$ and $f$ and the set of descent data of $F$ and $\mathrm{f'}$.

CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIsodefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

the functor of F and S (from the docstring)

English

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $S$ be an element of $C$. Then the functor of $F$ and $S$ is an isomorphism of $\operatorname{pullFunctor}$ applied to $F$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_pullFunctorIdIso\_\_\_proof\_1}$ applied to $S$ and the identity of the set of descent data of $F$ and $f$.

CategoryTheory.Pseudofunctor.DescentData.pullFunctorIsodefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

no wording

English

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Assume that for all elements $j_{1}$ of $x_{2}$, the composition of $\mathrm{p'}$ applied to $j_{1}$ and $f$ applied to $x_{3}$ applied to $j_{1}$ is equal to the composition of $\mathrm{f'}$ applied to $j_{1}$ and $p$. Assume that for all elements $j$ of $x_{2}$, the composition of $\mathrm{p''}$ applied to $j$ and $f$ applied to $x_{4}$ applied to $j$ is equal to the composition of $\mathrm{f'}$ applied to $j$ and $p$. Then $\operatorname{pullFunctorIso}$ applied to $F$, $w$ and $\mathrm{w'}$ is an isomorphism of $\operatorname{pullFunctor}$ applied to $F$ and $w$ and $\operatorname{pullFunctor}$ applied to $F$ and $\mathrm{w'}$.

CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquivdefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

the subtype compatible homomorphism equivalence of F and f (from the name)

English

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $f$ be a function from elements $i_{1}$ of $x_{1}$ to homomorphisms of $X$ applied to $i_{1}$ and $S$. Then the subtype compatible homomorphism equivalence of $F$ and $i_{1}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{\operatorname{Compatible} (\operatorname{presheafHom} (M , N), \lambda i . \operatorname{homMk} (f (i), \mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_subtypeCompatibleHomEquiv\_\_\_proof\_2} (f , i)), x_{2})})}{\operatorname{Hom} (\operatorname{obj} (\operatorname{toDescentData} (F , f), M), \operatorname{obj} (\operatorname{toDescentData} (F , f), N))}$.

CategoryTheory.Pseudofunctor.DescentData.toDescentDataCompPullFunctorIsodefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

no wording

English

CategoryTheory.Pseudofunctor.IsPrestackForstructureMathlib.CategoryTheory.Sites.Descent.DescentData, predicate

Wording

no wording

English

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $R$ be a presieve of $S$. Then we can say that $\operatorname{IsPrestackFor}$ holds for $F$ and $R$.

CategoryTheory.Pseudofunctor.IsPrestackFor.fullyFaithfuldefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

no wording

English

Assume that $\operatorname{IsPrestackFor}$ holds for $F$ and $R$. Then $\operatorname{fullyFaithful}$ applied to $\mathrm{hF}$ is an element of $\operatorname{FullyFaithful}$ applied to the descent data of $F$ and the function that maps $f$ to the homomorphism of the object of $f$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_IsPrestackFor\_\_nonempty\_fullyFaithful}$ applied to $\mathrm{hF}$.

CategoryTheory.Pseudofunctor.IsStackForstructureMathlib.CategoryTheory.Sites.Descent.DescentData, predicate

Wording

no wording

English

CategoryTheory.Pseudofunctor.fullyFaithfulToDescentDatadefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

no wording

English

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $f$ be a function from elements $i$ of $x_{1}$ to homomorphisms of $X$ applied to $i$ and $S$ such that the sieve of $X$ and $f$ is an element of $J$ applied to $S$. Then $\operatorname{fullyFaithfulToDescentData}$ applied to $F$, $i$, $f$ and $\mathrm{hf}$ is an element of $\operatorname{FullyFaithful}$ applied to the descent data of $F$ and $f$.

CategoryTheory.Pseudofunctor.toDescentDatadefMathlib.CategoryTheory.Sites.Descent.DescentData, function or constant

Wording

the descent data of F and f (from the name)

English

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $f$ be a function from elements $i$ of $x_{1}$ to homomorphisms of $X$ applied to $i$ and $S$. Then the descent data of $F$ and $i$ is a functor of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$ and the set of descent data of $F$ and $f$.