Definitions: Mathlib.CategoryTheory, part 16 of 25

CategoryTheory.Localization.Preadditive.adddefMathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive, function or constant

Wording

the sum of x3 and x4 (from the name)

English

Let $W$ be a morphism property of $C$. Let $\mathrm{eX}$ be an isomorphism of the action of $L$ and $X$ and $\mathrm{X'}$. Let $\mathrm{eY}$ be an isomorphism of the action of $L$ and $Y$ and $\mathrm{Y'}$. Let $x_{3}$ and $x_{4}$ be homomorphisms of $\mathrm{X'}$ and $\mathrm{Y'}$. Then the sum of $x_{3}$ and $x_{4}$ is a homomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$ defined as $\operatorname{symm}$ applied to the homomorphism equivalence of $\mathrm{eX}$ and $\mathrm{eY}$ and the sum of $\operatorname{homEquiv}$ applied to $\mathrm{eX}$, $\mathrm{eY}$ and $x_{3}$ and $\operatorname{homEquiv}$ applied to $\mathrm{eX}$, $\mathrm{eY}$ and $x_{4}$.

CategoryTheory.Localization.Preadditive.add'defMathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive, function or constant

Wording

the sum of x3 and x4 (from the name)

English

Let $W$ be a morphism property of $C$. Let $x_{3}$ and $x_{4}$ be homomorphisms of the action of $L$ and $X$ and the action of $L$ and $Y$. Then the sum of $x_{3}$ and $x_{4}$ is a homomorphism of the action of $L$ and $X$ and the action of $L$ and $Y$ defined as the map of the sum of $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Localization\_\_exists\_leftFraction\_u2082\_}$ applied to $L$, $W$, $x_{3}$ and $x_{4}$ and $L$.

CategoryTheory.Localization.Preadditive.homEquivdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive, function or constant

Wording

the homomorphism equivalence of eX and eY (from the name)

English

Let $\mathrm{eX}$ be an isomorphism of the action of $L$ and $X$ and $\mathrm{X'}$. Let $\mathrm{eY}$ be an isomorphism of the action of $L$ and $Y$ and $\mathrm{Y'}$. Then the homomorphism equivalence of $\mathrm{eX}$ and $\mathrm{eY}$ is an equivalence from the set of homomorphisms of $\mathrm{X'}$ and $\mathrm{Y'}$ to the set of homomorphisms of the action of $L$ and $X$ and the action of $L$ and $Y$.

CategoryTheory.Localization.Preadditive.neg'defMathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive, function or constant

Wording

the negation of W and f (from the name)

English

Let $W$ be a morphism property of $C$. Let $f$ be a homomorphism of the action of $L$ and $X$ and the action of $L$ and $Y$. Then the negation of $W$ and $f$ is a homomorphism of the action of $L$ and $X$ and the action of $L$ and $Y$ defined as the map of the negation of $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Localization\_\_exists\_leftFraction}$ applied to $L$, $W$ and $f$ and $L$.

CategoryTheory.MorphismProperty.LeftFraction.negdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive, function or constant

Wording

the negation of x2 (from the name)

English

Let $x_{2}$ be a left fraction of $X$ and $Y$. Then the negation of $x_{2}$ is a left fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{neg}$ applied to $\operatorname{f}$ applied to $x_{2}$, $\operatorname{s}$ applied to $x_{2}$ and $\operatorname{hs}$ applied to $x_{2}$.

CategoryTheory.MorphismProperty.LeftFraction₂.adddefMathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive, function or constant

Wording

the sum of x2 (from the name)

English

Let $x_{2}$ be a left fraction of $X$ and $Y$. Then the sum of $x_{2}$ is a left fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f} (x_{2})+ \mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f'} (x_{2})$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_s}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_hs}$ applied to $x_{2}$.

Mathlib.CategoryTheory.Localization.Composition

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.compdefMathlib.CategoryTheory.Localization.Composition, function or constant

Wording

the composition of x12 and x13 (from the name)

English

Let $x_{11}$ be a strict universal property fixed target of $x_{9}$ and $E$. Let $x_{12}$ be a strict universal property fixed target of $x_{10}$ and $E$. Let $x_{13}$ be a morphism property of $x$ such that $\operatorname{IsInvertedBy}$ holds for $x_{13}$ and the composition of $x_{7}$ and $x_{8}$, $x_{9} \leq x_{13}$ and $x_{10}$ is less than or equal to the map of $x_{13}$ and $x_{7}$. Then the composition of $x_{12}$ and $x_{13}$ is a strict universal property fixed target of $x_{13}$ and $E$.

Mathlib.CategoryTheory.Localization.Construction

CategoryTheory.Localization.Construction.LocQuiverstructureMathlib.CategoryTheory.Localization.Construction, type

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then the elements of $\operatorname{LocQuiver}$ applied to $W$ are a basic type.

CategoryTheory.Localization.Construction.LocQuiver.objdefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the object of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{LocQuiver}$ applied to $W$. Then the object of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Localization.Construction.NatTransExtension.appdefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the natural transformation extension of x4 and X (from the name)

English

Let $x_{4}$ be a homomorphism of the composition of $\operatorname{Q}$ applied to $W$ and $x_{2}$ and the composition of $\operatorname{Q}$ applied to $W$ and $x_{3}$. Let $X$ be a localization of $W$. Then the natural transformation extension of $x_{4}$ and $X$ is a homomorphism of the action of $x_{2}$ and $X$ and the action of $x_{3}$ and $X$.

CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIsodefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the counit isomorphism of W and D (from the name)

English

Let $W$ be a morphism property of $C$. Let $D$ be a set. Then the counit isomorphism of $W$ and $D$ is an isomorphism of the composition of the inverse of $W$ and $D$ and the functor of $W$ and $D$ and the identity of $\operatorname{FunctorsInverting}$ applied to $W$ and $D$.

CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functordefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the functor of W and D (from the docstring)

English

Let $W$ be a morphism property of $C$. Let $D$ be a set. Then the functor of $W$ and $D$ is a functor of the set of functors of the set of localizations of $W$ and $D$ and $\operatorname{FunctorsInverting}$ applied to $W$ and $D$.

CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inversedefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the inverse of W and D (from the name)

English

Let $W$ be a morphism property of $C$. Let $D$ be a set. Then the inverse of $W$ and $D$ is a functor of $\operatorname{FunctorsInverting}$ applied to $W$ and $D$ and the set of functors of the set of localizations of $W$ and $D$.

CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIsodefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the unit isomorphism of W and D (from the name)

English

Let $W$ be a morphism property of $C$. Let $D$ be a set. Then the unit isomorphism of $W$ and $D$ is an isomorphism of the identity of the set of functors of the set of localizations of $W$ and $D$ and the composition of the functor of $W$ and $D$ and the inverse of $W$ and $D$.

CategoryTheory.Localization.Construction.liftdefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the lifting of G and hG (from the docstring)

English

Let $G$ be a functor of $C$ and $D$ such that $\operatorname{IsInvertedBy}$ holds for $W$ and $G$. Then the lifting of $G$ and $\mathrm{hG}$ is a functor of the set of localizations of $W$ and $D$.

CategoryTheory.Localization.Construction.liftToPathCategorydefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the lifting of G and hG (from the docstring)

English

Let $G$ be a functor of $C$ and $D$ such that $\operatorname{IsInvertedBy}$ holds for $W$ and $G$. Then the lifting of $G$ and $\mathrm{hG}$ is a functor of the set of paths of $\operatorname{LocQuiver}$ applied to $W$ and $D$.

CategoryTheory.Localization.Construction.natTransExtensiondefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the natural transformation extension of x4 (from the name)

English

Let $x_{4}$ be a homomorphism of the composition of $\operatorname{Q}$ applied to $W$ and $x_{2}$ and the composition of $\operatorname{Q}$ applied to $W$ and $x_{3}$. Then the natural transformation extension of $x_{4}$ is a homomorphism of $x_{2}$ and $x_{3}$.

CategoryTheory.Localization.Construction.objEquivdefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the object equivalence of W (from the name)

English

Let $W$ be a morphism property of $C$. Then the object equivalence of $W$ is an equivalence from $C$ to the set of localizations of $W$.

CategoryTheory.Localization.Construction.relationsinductiveMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the relation of W (from the name)

English

Let $W$ be a morphism property of $C$. Then the relation of $W$ is a homomorphism relation of the set of paths of $\operatorname{LocQuiver}$ applied to $W$.

CategoryTheory.Localization.Construction.wInvdefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the inverse of w and hw (from the name)

English

Let $w$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $w$. Then the inverse of $w$ and $\mathrm{hw}$ is a homomorphism of the action of $\operatorname{Q}$ applied to $W$ and $Y$ and the action of $\operatorname{Q}$ applied to $W$ and $X$ defined as the inverse of the isomorphism of $w$ and $\mathrm{hw}$.

CategoryTheory.Localization.Construction.wIsodefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the isomorphism of w and hw (from the name)

English

Let $w$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $w$. Then the isomorphism of $w$ and $\mathrm{hw}$ is an isomorphism of the action of $\operatorname{Q}$ applied to $W$ and $X$ and the action of $\operatorname{Q}$ applied to $W$ and $Y$.

CategoryTheory.Localization.Construction.whiskeringLeftEquivalencedefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the whiskering left equivalence of W and D (from the name)

English

Let $W$ be a morphism property of $C$. Let $D$ be a set. Then the whiskering left equivalence of $W$ and $D$ is an equivalence of the set of functors of the set of localizations of $W$ and $D$ and $\operatorname{FunctorsInverting}$ applied to $W$ and $D$.

CategoryTheory.Localization.Construction.ιPathsdefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

the inclusion path of W and X (from the name)

English

Let $W$ be a morphism property of $C$. Let $X$ be an element of $C$. Then the inclusion path of $W$ and $X$ is a path of $\operatorname{LocQuiver}$ applied to $W$ defined as $\operatorname{mk}$ applied to $X$.

CategoryTheory.Localization.Construction.ψ₁defMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_Localization\_\_Construction\_\_\_u3c8\_\_u2081\_}$ applied to $W$ and $f$ is a homomorphism of the inclusion path of $W$ and $X$ and the inclusion path of $W$ and $Y$ defined as the map of $\operatorname{of}$ applied to $\operatorname{LocQuiver}$ applied to $W$ and $\operatorname{inl}$ applied to $f$.

CategoryTheory.Localization.Construction.ψ₂defMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $w$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $w$. Then $\mathrm{CategoryTheory\_\_Localization\_\_Construction\_\_\_u3c8\_\_u2082\_}$ applied to $W$, $w$ and $\mathrm{hw}$ is a homomorphism of the inclusion path of $W$ and $Y$ and the inclusion path of $W$ and $X$ defined as the map of $\operatorname{of}$ applied to $\operatorname{LocQuiver}$ applied to $W$ and $\operatorname{inr}$ applied to $w$.

CategoryTheory.MorphismProperty.LocalizationdefMathlib.CategoryTheory.Localization.Construction, type

Wording

localization of W (from the name)

English

Let $W$ be a morphism property of $C$. Then a localization of $W$ is an element of the function that maps $W$ to the set of quotients of the relation of $W$.

CategoryTheory.MorphismProperty.QdefMathlib.CategoryTheory.Localization.Construction, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then $\operatorname{Q}$ applied to $W$ is a functor of $C$ and the set of localizations of $W$.

Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructureclassMathlib.CategoryTheory.Localization.DerivabilityStructure.Basic, predicate

Wording

x6 is a left derivability structure (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then we can say that $x_{6}$ is a left derivability structure.

CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructureclassMathlib.CategoryTheory.Localization.DerivabilityStructure.Basic, predicate

Wording

x6 is a right derivability structure (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then we can say that $x_{6}$ is a right derivability structure.

Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolutiondefMathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor, function or constant

Wording

no wording

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Let $L$ be a functor of $x_{1}$ and $D$. Let $y$ be a homomorphism of the action of $L$ and $x_{8}$ and $x_{9}$. Then $\operatorname{fromRightResolution}$ applied to $x_{6}$, $L$ and $y$ is a functor of the set of right resolutions of $x_{6}$ and $x_{8}$ and $\operatorname{CostructuredArrowDownwards}$ applied to $\operatorname{mk}$ applied to the functor of $x_{6}$, the composition of the functor of $x_{6}$ and $L$, $L$, the identity of $D$ and the inverse of the right unitor of the composition of the functor of $x_{6}$ and $L$ and $y$.

Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives

CategoryTheory.LocalizerMorphism.DerivesdefMathlib.CategoryTheory.Localization.DerivabilityStructure.Derives, predicate

Wording

no wording

English

Let $x_{7}$ be a localizer morphism of $x_{5}$ and $x_{6}$. Let $F$ be a functor of $x_{1}$ and $H$. Then $\operatorname{Derives}$ holds for $x_{7}$ and $F$, if $\operatorname{IsInvertedBy}$ holds for $x_{5}$ and the composition of the functor of $x_{7}$ and $F$.

Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

CategoryTheory.LocalizerMorphism.functorialRightResolutions.localizerMorphismInvdefMathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions, function or constant

Wording

the localizer morphism inverse of hi and h (from the name)

English

Assume that for all elements $x_{8}$ of $x_{1}$, $x_{5}$ holds for the action of the identity of $x_{1}$ and $x_{8}$, the action of the composition of $x_{7}$ and the functor of $x_{6}$ and $x_{8}$ and the component of $i$ and $x_{8}$. Assume that $x_{4}$ is equal to the inverse image of $x_{5}$ and the functor of $x_{6}$. Then the localizer morphism inverse of $\mathrm{hi}$ and $h$ is a localizer morphism of $x_{5}$ and $x_{4}$.

CategoryTheory.LocalizerMorphism.functorialRightResolutions.ιdefMathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions, function or constant

Wording

the inclusion of i (from the name)

English

Let $i$ be a homomorphism of the identity of $x_{1}$ and the composition of $x_{7}$ and the functor of $x_{6}$. Then the inclusion of $i$ is a homomorphism of the identity of $x$ and the composition of the functor of $x_{6}$ and $x_{7}$ defined as the choice of the action of the right whiskering of $x$ and $x_{1}$ and the functor of $x_{6}$ and the left whisker of the functor of $x_{6}$ and $i$.

Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseLeftDerived

CategoryTheory.LocalizerMorphism.leftDerivedFunctorComparisondefMathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseLeftDerived, function or constant

Wording

the left derived functor comparison of x16 and x17 (from the name)

English

Let $x_{11}$ be a localizer morphism of $x_{9}$ and $x_{10}$. Let $x_{12}$ be a functor of $x$ and $x_{2}$. Let $x_{13}$ be a functor of $x_{1}$ and $x_{3}$. Let $F$ be a functor of $x_{1}$ and $H$. Let $x_{14}$ be a functor of $x_{2}$ and $H$. Let $x_{15}$ be a homomorphism of the composition of $x_{12}$ and $x_{14}$ and the composition of the functor of $x_{11}$ and $F$. Let $x_{16}$ be a functor of $x_{3}$ and $H$. Let $x_{17}$ be a homomorphism of the composition of $x_{13}$ and $x_{16}$ and $F$. Then the left derived functor comparison of $x_{16}$ and $x_{17}$ is a homomorphism of the composition of the localized functor of $x_{12}$ and $x_{13}$ and $x_{16}$ and $x_{14}$ defined as the left derived lift of the composition of the localized functor of $x_{12}$ and $x_{13}$ and $x_{16}$ and the composition of the inverse of the associator of the localized functor of $x_{12}$ and $x_{13}$ and $x_{16}$ and the composition of the right whisker of the inverse of the isomorphism of $x_{13}$ and the localized functor of $x_{12}$ and $x_{13}$ and $x_{16}$ and the composition of the homomorphism of the associator of $x_{13}$ and $x_{16}$ and the left whisker of the functor of $x_{11}$ and $x_{17}$.

Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparisondefMathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived, function or constant

Wording

the right derived functor comparison of x16 and x17 (from the name)

English

Let $x_{11}$ be a localizer morphism of $x_{9}$ and $x_{10}$. Let $x_{12}$ be a functor of $x$ and $x_{5}$. Let $x_{13}$ be a functor of $x_{1}$ and $x_{6}$. Let $F$ be a functor of $x_{1}$ and $H$. Let $x_{14}$ be a functor of $x_{5}$ and $H$. Let $x_{15}$ be a homomorphism of the composition of the functor of $x_{11}$ and $F$ and the composition of $x_{12}$ and $x_{14}$. Let $x_{16}$ be a functor of $x_{6}$ and $H$. Let $x_{17}$ be a homomorphism of $F$ and the composition of $x_{13}$ and $x_{16}$. Then the right derived functor comparison of $x_{16}$ and $x_{17}$ is a homomorphism of $x_{14}$ and the composition of the localized functor of $x_{12}$ and $x_{13}$ and $x_{16}$ defined as $\operatorname{rightDerivedDesc}$ applied to $x_{14}$, $x_{15}$, $x_{9}$, the composition of the localized functor of $x_{12}$ and $x_{13}$ and $x_{16}$ and the composition of the left whisker of the functor of $x_{11}$ and $x_{17}$ and the composition of the inverse of the associator of $x_{13}$ and $x_{16}$ and the composition of the right whisker of the homomorphism of the isomorphism of $x_{13}$ and the localized functor of $x_{12}$ and $x_{13}$ and $x_{16}$ and the homomorphism of the associator of the localized functor of $x_{12}$ and $x_{13}$ and $x_{16}$.

Mathlib.CategoryTheory.Localization.Equivalence

CategoryTheory.Localization.equivalencedefMathlib.CategoryTheory.Localization.Equivalence, function or constant

Wording

the equivalence of #9 and #10 (from the name)

English

Let $x_{8}$ be a functor of $x$ and $x_{2}$. Let $x_{9}$ be a morphism property of $x$. Let $x_{10}$ be a functor of $x_{1}$ and $x_{3}$. Let $x_{11}$ be a morphism property of $x_{1}$. Let $G$ be a functor of $x$ and $x_{3}$. Let $\mathrm{G'}$ be a functor of $x_{2}$ and $x_{3}$. Let $F$ be a functor of $x_{1}$ and $x_{2}$. Let $\mathrm{F'}$ be a functor of $x_{3}$ and $x_{2}$. Let $x_{14}$ be an isomorphism of the composition of $G$ and $\mathrm{F'}$ and $x_{8}$. Let $x_{15}$ be an isomorphism of the composition of $F$ and $\mathrm{G'}$ and $x_{10}$. Then the equivalence of $x_{14}$ and $x_{15}$ is an equivalence of $x_{2}$ and $x_{3}$ defined as $\operatorname{mk}$ applied to $\mathrm{G'}$, $\mathrm{F'}$, the lift natural isomorphism of the composition of $\mathrm{G'}$ and $\mathrm{F'}$ and the inverse of $x_{14}$ and the lift natural isomorphism of the identity of $x_{3}$ and $x_{15}$.

Mathlib.CategoryTheory.Localization.FiniteProducts

CategoryTheory.Localization.HasProductsOfShapeAux.adjdefMathlib.CategoryTheory.Localization.FiniteProducts, function or constant

Wording

the adjoint of L and W (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $J$ be a set. Then the adjoint of $L$ and $W$ is an adjunction of the constant of $\operatorname{Discrete}$ applied to $J$ and the limit functor of $L$ and $W$ defined as the localization of the constant of $\operatorname{Discrete}$ applied to $J$ and the limit functor of $L$ and $W$.

CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIsodefMathlib.CategoryTheory.Localization.FiniteProducts, function or constant

Wording

the composition limit functor isomorphism of L and W (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $J$ be a set. Then the composition limit functor isomorphism of $L$ and $W$ is an isomorphism of the composition of the action of the right whiskering of $C$ and $D$ and $L$ and the limit functor of $L$ and $W$ and the composition of the limit and $L$ defined as the factor of the composition of the limit and $L$ and the action of the right whiskering of $C$ and $D$ and $L$.

CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctordefMathlib.CategoryTheory.Localization.FiniteProducts, function or constant

Wording

the limit functor of L and W (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $J$ be a set. Then the limit functor of $L$ and $W$ is a functor of the set of functors of $\operatorname{Discrete}$ applied to $J$ and $D$ and $D$ defined as the lift of the composition of the limit and $L$ and the action of the right whiskering of $C$ and $D$ and $L$.

Mathlib.CategoryTheory.Localization.HasLocalization

CategoryTheory.MorphismProperty.HasLocalizationclassMathlib.CategoryTheory.Localization.HasLocalization, predicate

Wording

W has localizations (from the name)

English

Let $W$ be a morphism property of $C$. Then we can say that $W$ has localizations.

CategoryTheory.MorphismProperty.HasLocalization.DdefMathlib.CategoryTheory.Localization.HasLocalization, type

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then an element of $\operatorname{D}$ applied to $W$ is an element of the function that maps $W$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.HasLocalization.LdefMathlib.CategoryTheory.Localization.HasLocalization, function or constant

Wording

no wording

English

$\operatorname{L}$ is a functor of $C$ and $\operatorname{D}$ applied to $W$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.Localization'defMathlib.CategoryTheory.Localization.HasLocalization, type

Wording

localization of W (from the name)

English

Let $W$ be a morphism property of $C$. Then a localization of $W$ is an element of the function that maps $W$ to $\operatorname{D}$ applied to $W$.

CategoryTheory.MorphismProperty.Q'defMathlib.CategoryTheory.Localization.HasLocalization, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then $\operatorname{Q'}$ applied to $W$ is a functor of $C$ and the set of localizations of $W$ defined as $\operatorname{L}$.

Mathlib.CategoryTheory.Localization.HomEquiv

CategoryTheory.Localization.homEquivdefMathlib.CategoryTheory.Localization.HomEquiv, function or constant

Wording

the homomorphism equivalence of x5 and x6 (from the name)

English

Let $W$ be a morphism property of $C$. Let $x_{5}$ be a functor of $C$ and $x$. Let $x_{6}$ be a functor of $C$ and $x_{1}$. Then the homomorphism equivalence of $x_{5}$ and $x_{6}$ is an equivalence from the set of homomorphisms of the action of $x_{5}$ and $X$ and the action of $x_{5}$ and $Y$ to the set of homomorphisms of the action of $x_{6}$ and $X$ and the action of $x_{6}$ and $Y$.

CategoryTheory.LocalizerMorphism.homMapdefMathlib.CategoryTheory.Localization.HomEquiv, function or constant

Wording

the homomorphism map of x12 and f (from the name)

English

Let $x_{10}$ be a localizer morphism of $x_{8}$ and $x_{9}$. Let $x_{11}$ be a functor of $x$ and $x_{2}$. Let $x_{12}$ be a functor of $x_{1}$ and $x_{3}$. Let $f$ be a homomorphism of the action of $x_{11}$ and $X$ and the action of $x_{11}$ and $Y$. Then the homomorphism map of $x_{12}$ and $f$ is a homomorphism of the action of $x_{12}$ and the action of the functor of $x_{10}$ and $X$ and the action of $x_{12}$ and the action of the functor of $x_{10}$ and $Y$ defined as $\operatorname{homCongr}$ applied to the application of the inverse of the isomorphism of $x_{12}$ and the localized functor of $x_{11}$ and $x_{12}$ and $X$, the application of the inverse of the isomorphism of $x_{12}$ and the localized functor of $x_{11}$ and $x_{12}$ and $Y$ and the map of the localized functor of $x_{11}$ and $x_{12}$ and $f$.

Mathlib.CategoryTheory.Localization.LocalizerMorphism

CategoryTheory.LocalizerMorphismstructureMathlib.CategoryTheory.Localization.LocalizerMorphism, type

Wording

localizer morphism of x4 and x5 (from the name)

English

Let $x_{4}$ be a morphism property of $x$. Let $x_{5}$ be a morphism property of $x_{1}$. Then the localizer morphisms of $x_{4}$ and $x_{5}$ are a basic type.

CategoryTheory.LocalizerMorphism.IsInducedclassMathlib.CategoryTheory.Localization.LocalizerMorphism, predicate

Wording

x6 is induced (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then we can say that $x_{6}$ is induced.

CategoryTheory.LocalizerMorphism.IsLocalizedEquivalenceclassMathlib.CategoryTheory.Localization.LocalizerMorphism, predicate

Wording

x6 is a localized equivalence (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then we can say that $x_{6}$ is a localized equivalence.

CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithfulclassMathlib.CategoryTheory.Localization.LocalizerMorphism, predicate

Wording

no wording

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then we can say that $\operatorname{IsLocalizedFullyFaithful}$ holds for $x_{6}$.

CategoryTheory.LocalizerMorphism.arrowdefMathlib.CategoryTheory.Localization.LocalizerMorphism, function or constant

Wording

the arrow of x6 (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then the arrow of $x_{6}$ is a localizer morphism of the arrow of $x_{4}$ and the arrow of $x_{5}$.

CategoryTheory.LocalizerMorphism.compdefMathlib.CategoryTheory.Localization.LocalizerMorphism, function or constant

Wording

the composition of x9 and x10 (from the name)

English

Let $x_{9}$ be a localizer morphism of $x_{6}$ and $x_{7}$. Let $x_{10}$ be a localizer morphism of $x_{7}$ and $x_{8}$. Then the composition of $x_{9}$ and $x_{10}$ is a localizer morphism of $x_{6}$ and $x_{8}$.

CategoryTheory.LocalizerMorphism.fullyFaithfuldefMathlib.CategoryTheory.Localization.LocalizerMorphism, function or constant

Wording

no wording

English

Let $x_{10}$ be a localizer morphism of $x_{8}$ and $x_{9}$. Let $x_{11}$ be a functor of $x$ and $x_{2}$. Let $x_{12}$ be a functor of $x_{1}$ and $x_{3}$. Let $G$ be a functor of $x_{2}$ and $x_{3}$. Then $\operatorname{fullyFaithful}$ applied to $x_{10}$, $x_{11}$, $x_{12}$ and $G$ is an element of $\operatorname{FullyFaithful}$ applied to $G$.

CategoryTheory.LocalizerMorphism.fullyFaithfulLocalizedFunctordefMathlib.CategoryTheory.Localization.LocalizerMorphism, function or constant

Wording

the fully faithful localized functor of x11 and x12 (from the name)

English

generation took over the time limit

CategoryTheory.LocalizerMorphism.functordefMathlib.CategoryTheory.Localization.LocalizerMorphism, function or constant

Wording

the functor of self (from the name)

English

Let $\mathrm{self}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then the functor of $\mathrm{self}$ is a functor of $x$ and $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.LocalizerMorphism.iddefMathlib.CategoryTheory.Localization.LocalizerMorphism, function or constant

Wording

the identity functor of x2 (from the docstring)

English

Let $x_{2}$ be a morphism property of $x$. Then the identity functor of $x_{2}$ is a localizer morphism of $x_{2}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the identity of $x$ and the function that maps $x_{3}$, $x_{4}$, $x_{5}$ and $\mathrm{hf}$ to $\mathrm{hf}$.

CategoryTheory.LocalizerMorphism.invdefMathlib.CategoryTheory.Localization.LocalizerMorphism, function or constant

Wording

the inverse of x6 (from the docstring)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then the inverse of $x_{6}$ is a localizer morphism of $x_{5}$ and $x_{4}$.

CategoryTheory.LocalizerMorphism.localizedFunctordefMathlib.CategoryTheory.Localization.LocalizerMorphism, function or constant

Wording

the localized functor of x11 and x12 (from the name)

English

Let $x_{10}$ be a localizer morphism of $x_{8}$ and $x_{9}$. Let $x_{11}$ be a functor of $x$ and $x_{2}$. Let $x_{12}$ be a functor of $x_{1}$ and $x_{3}$. Then the localized functor of $x_{11}$ and $x_{12}$ is a functor of $x_{2}$ and $x_{3}$ defined as the lift of the composition of the functor of $x_{10}$ and $x_{12}$ and $x_{11}$.

CategoryTheory.LocalizerMorphism.ofEqdefMathlib.CategoryTheory.Localization.LocalizerMorphism, function or constant

Wording

the localizer morphism of hW (from the name)

English

Assume that $x_{4}$ is equal to the inverse image of $x_{5}$ and $F$. Then the localizer morphism of $\mathrm{hW}$ is a localizer morphism of $x_{4}$ and $x_{5}$.

CategoryTheory.LocalizerMorphism.opdefMathlib.CategoryTheory.Localization.LocalizerMorphism, function or constant

Wording

the opposite localizer morphism of x6 (from the docstring)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then the opposite localizer morphism of $x_{6}$ is a localizer morphism of the opposite of $x_{4}$ and the opposite of $x_{5}$.

Mathlib.CategoryTheory.Localization.Monoidal.Basic

CategoryTheory.Localization.Monoidal.associatordefMathlib.CategoryTheory.Localization.Monoidal.Basic, function or constant

Wording

the associator of W and x3 (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ be an isomorphism of the action of $L$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$. Then the associator of $W$ and $x_{3}$ is an isomorphism of the bifunctor composition of the tensor bifunctor of $W$ and $x_{3}$ and the tensor bifunctor of $W$ and $x_{3}$ and the bifunctor composition of the tensor bifunctor of $W$ and $x_{3}$ and the tensor bifunctor of $W$ and $x_{3}$ defined as the associator of the tensor bifunctor of $W$ and $x_{3}$ and the tensor bifunctor of $W$ and $x_{3}$.

CategoryTheory.Localization.Monoidal.leftUnitordefMathlib.CategoryTheory.Localization.Monoidal.Basic, function or constant

Wording

the left unitor of W and x3 (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ be an isomorphism of the action of $L$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$. Then the left unitor of $W$ and $x_{3}$ is an isomorphism of the action of the tensor bifunctor of $W$ and $x_{3}$ and $\mathrm{unit}$ and the identity of $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ defined as the composition of the map isomorphism of the tensor bifunctor of $W$ and $x_{3}$ and the inverse of $x_{3}$ and the lift natural isomorphism of the identity of $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ and the composition of the right isomorphism whisker of the left unitor of $C$ and the monoidal category of $W$ and $x_{3}$ and the left unitor of $L$.

CategoryTheory.Localization.Monoidal.rightUnitordefMathlib.CategoryTheory.Localization.Monoidal.Basic, function or constant

Wording

the right unitor of W and x3 (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ be an isomorphism of the action of $L$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$. Then the right unitor of $W$ and $x_{3}$ is an isomorphism of the action of the flip of the tensor bifunctor of $W$ and $x_{3}$ and $\mathrm{unit}$ and the identity of $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ defined as the composition of the map isomorphism of the flip of the tensor bifunctor of $W$ and $x_{3}$ and the inverse of $x_{3}$ and the lift natural isomorphism of the identity of $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ and the composition of the right isomorphism whisker of the right unitor of $C$ and the monoidal category of $W$ and $x_{3}$ and the left unitor of $L$.

CategoryTheory.Localization.Monoidal.tensorBifunctordefMathlib.CategoryTheory.Localization.Monoidal.Basic, function or constant

Wording

the tensor bifunctor of W and x3 (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ be an isomorphism of the action of $L$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$. Then the tensor bifunctor of $W$ and $x_{3}$ is a functor of $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ and the set of functors of $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ and $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ defined as the lift of $L$ and $L$.

CategoryTheory.Localization.Monoidal.tensorBifunctorIsodefMathlib.CategoryTheory.Localization.Monoidal.Basic, function or constant

Wording

the tensor bifunctor isomorphism of W and x3 (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ be an isomorphism of the action of $L$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$. Then the tensor bifunctor isomorphism of $W$ and $x_{3}$ is an isomorphism of the action of the action of the action of the left whiskering of $D$ and the monoidal category of $W$ and $x_{3}$ and the monoidal category of $W$ and $x_{3}$ and the tensor bifunctor of $W$ and $x_{3}$ and the action of the action of the postcomposition and the monoidal category of $W$ and $x_{3}$ and the tensor product bifunctor of $C$ defined as the isomorphism of the composition of the tensor product bifunctor of $C$ and the action of the right whiskering of $C$ and $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ and the monoidal category of $W$ and $x_{3}$ and the tensor bifunctor of $W$ and $x_{3}$.

CategoryTheory.Localization.Monoidal.toMonoidalCategorydefMathlib.CategoryTheory.Localization.Monoidal.Basic, function or constant

Wording

the monoidal category of W and x3 (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ be an isomorphism of the action of $L$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$. Then the monoidal category of $W$ and $x_{3}$ is a functor of $C$ and $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ defined as $L$.

CategoryTheory.Localization.Monoidal.ε'defMathlib.CategoryTheory.Localization.Monoidal.Basic, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ be an isomorphism of the action of $L$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$. Then $\mathrm{CategoryTheory\_\_Localization\_\_Monoidal\_\_\_u3b5\_'}$ applied to $L$, $W$ and $x_{3}$ is an isomorphism of the action of the monoidal category of $W$ and $x_{3}$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$ defined as $x_{3}$.

CategoryTheory.Localization.Monoidal.μdefMathlib.CategoryTheory.Localization.Monoidal.Basic, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ be an isomorphism of the action of $L$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$. Let $X$ and $Y$ be elements of $C$. Then $\mathrm{CategoryTheory\_\_Localization\_\_Monoidal\_\_\_u3bc\_}$ applied to $L$, $W$, $x_{3}$, $X$ and $Y$ is an isomorphism of the tensor object of the action of the monoidal category of $W$ and $x_{3}$ and $X$ and the action of the monoidal category of $W$ and $x_{3}$ and $Y$ and the action of the monoidal category of $W$ and $x_{3}$ and the tensor object of $X$ and $Y$ defined as the application of the application of the tensor bifunctor isomorphism of $W$ and $x_{3}$ and $X$ and $Y$.

CategoryTheory.LocalizedMonoidaldefMathlib.CategoryTheory.Localization.Monoidal.Basic, type

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ be an isomorphism of the action of $L$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$. Then an element of $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ is an element of the function that maps $L$, $W$ and $x_{3}$ to $D$.

CategoryTheory.MorphismProperty.IsMonoidalclassMathlib.CategoryTheory.Localization.Monoidal.Basic, predicate

Wording

W is monoidal (from the name)

English

Let $W$ be a morphism property of $C$. Then we can say that $W$ is monoidal.

Mathlib.CategoryTheory.Localization.Monoidal.Braided

CategoryTheory.Localization.Monoidal.braidingNatIsodefMathlib.CategoryTheory.Localization.Monoidal.Braided, function or constant

Wording

the braiding natural isomorphism of W and x3 (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ be an isomorphism of the action of $L$ and the tensor unity in the monoidal structure of $C$ and $\mathrm{unit}$. Then the braiding natural isomorphism of $W$ and $x_{3}$ is an isomorphism of the tensor bifunctor of $W$ and $x_{3}$ and the flip of the tensor bifunctor of $W$ and $x_{3}$ defined as the lift natural isomorphism of the flip of the tensor bifunctor of $W$ and $x_{3}$ and the right isomorphism whisker of the braiding isomorphism of $C$ and the action of the right whiskering of $C$ and $\operatorname{LocalizedMonoidal}$ applied to $L$, $W$ and $x_{3}$ and the monoidal category of $W$ and $x_{3}$.

Mathlib.CategoryTheory.Localization.Monoidal.Functor

CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPostdefMathlib.CategoryTheory.Localization.Monoidal.Functor, function or constant

Wording

the curried tensor isomorphism post of F and G (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $F$ be a functor of $D$ and $E$. Let $G$ be a functor of $C$ and $E$. Then the curried tensor isomorphism post of $F$ and $G$ is an isomorphism of the curried tensor of $F$ and the curried tensor post of $F$ defined as the lift natural isomorphism of the curried tensor post of $F$ and the curried tensor isomorphism post of $G$.

CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfCompdefMathlib.CategoryTheory.Localization.Monoidal.Functor, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $F$ be a functor of $D$ and $E$. Let $G$ be a functor of $C$ and $E$. Then $\operatorname{functorCoreMonoidalOfComp}$ applied to $L$, $W$, $F$ and $G$ is an element of $\operatorname{CoreMonoidal}$ applied to $F$.

Mathlib.CategoryTheory.Localization.Opposite

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.opdefMathlib.CategoryTheory.Localization.Opposite, function or constant

Wording

the opposite of h (from the name)

English

Let $h$ be a strict universal property fixed target of $W$ and the set of opposites of $E$. Then the opposite of $h$ is a strict universal property fixed target of the opposite of $W$ and $E$.

Mathlib.CategoryTheory.Localization.Predicate

CategoryTheory.AreEqualizedByLocalizationdefMathlib.CategoryTheory.Localization.Predicate, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $\operatorname{AreEqualizedByLocalization}$ holds for $W$, $f$ and $g$, if the map of $\operatorname{Q}$ applied to $W$ and $f$ is equal to the map of $\operatorname{Q}$ applied to $W$ and $g$.

CategoryTheory.Functor.IsLocalizationclassMathlib.CategoryTheory.Localization.Predicate, predicate

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{IsLocalization}$ holds for $L$ and $W$.

CategoryTheory.Localization.LiftingclassMathlib.CategoryTheory.Localization.Predicate, predicate

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $F$ be a functor of $C$ and $E$. Let $\mathrm{F'}$ be a functor of $D$ and $E$. Then we can say that $\operatorname{Lifting}$ holds for $L$, $W$, $F$ and $\mathrm{F'}$.

CategoryTheory.Localization.Lifting.isodefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the isomorphism of F and #4 (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $F$ be a functor of $C$ and $E$. Let $\mathrm{F'}$ be a functor of $D$ and $E$. Then the isomorphism of $F$ and $\mathrm{F'}$ is an isomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Localization.StrictUniversalPropertyFixedTargetstructureMathlib.CategoryTheory.Localization.Predicate, type

Wording

strict universal property fixed target of W and E (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $E$ be a set. Then the strict universal property fixed targets of $W$ and $E$ are a basic type.

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.liftdefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the lift of self and F (from the name)

English

Let $\mathrm{self}$ be a strict universal property fixed target of $W$ and $E$. Let $F$ be a functor of $C$ and $E$ such that $\operatorname{IsInvertedBy}$ holds for $W$ and $F$. Then the lift of $\mathrm{self}$ and $F$ is a functor of $D$ and $E$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $F$ and $h$.

CategoryTheory.Localization.compEquivalenceFromModelInverseIsodefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the composition equivalence from model inverse isomorphism of L and W (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Then the composition equivalence from model inverse isomorphism of $L$ and $W$ is an isomorphism of the composition of $L$ and the inverse of the equivalence from model of $L$ and $W$ and $\operatorname{Q}$ applied to $W$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the right isomorphism whisker of the inverse of the composition equivalence from model functor isomorphism of $L$ and $W$ and the inverse of the equivalence from model of $L$ and $W$ and the associator of the functor of the equivalence from model of $L$ and $W$ and the inverse of the equivalence from model of $L$ and $W$ and the left isomorphism whisker of $\operatorname{Q}$ applied to $W$ and the inverse of the unit isomorphism of the equivalence from model of $L$ and $W$ and the right unitor of $\operatorname{Q}$ applied to $W$.

CategoryTheory.Localization.compUniqFunctordefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

no wording

English

Let $x_{5}$ be a functor of $C$ and $x_{1}$. Let $x_{6}$ be a functor of $C$ and $x_{2}$. Let $\mathrm{W'}$ be a morphism property of $C$. Then $\operatorname{compUniqFunctor}$ applied to $x_{5}$, $x_{6}$ and $\mathrm{W'}$ is an isomorphism of the composition of $x_{5}$ and the functor of $\operatorname{uniq}$ applied to $x_{5}$, $x_{6}$ and $\mathrm{W'}$ and $x_{6}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the associator of the functor of the inverse of the equivalence from model of $x_{5}$ and $\mathrm{W'}$ and the functor of the equivalence from model of $x_{6}$ and $\mathrm{W'}$ and the right isomorphism whisker of the composition equivalence from model inverse isomorphism of $x_{5}$ and $\mathrm{W'}$ and the functor of the equivalence from model of $x_{6}$ and $\mathrm{W'}$ and the composition equivalence from model functor isomorphism of $x_{6}$ and $\mathrm{W'}$.

CategoryTheory.Localization.compUniqInversedefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

no wording

English

Let $x_{5}$ be a functor of $C$ and $x_{1}$. Let $x_{6}$ be a functor of $C$ and $x_{2}$. Let $\mathrm{W'}$ be a morphism property of $C$. Then $\operatorname{compUniqInverse}$ applied to $x_{5}$, $x_{6}$ and $\mathrm{W'}$ is an isomorphism of the composition of $x_{6}$ and the inverse of $\operatorname{uniq}$ applied to $x_{5}$, $x_{6}$ and $\mathrm{W'}$ and $x_{5}$ defined as $\operatorname{compUniqFunctor}$ applied to $x_{6}$, $x_{5}$ and $\mathrm{W'}$.

CategoryTheory.Localization.equivalenceFromModeldefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the equivalence from model of L and W (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Then the equivalence from model of $L$ and $W$ is an equivalence of the set of localizations of $W$ and $D$ defined as $\operatorname{asEquivalence}$ applied to the lifting of $L$ and $\operatorname{inverts}$ applied to $L$ and $W$.

CategoryTheory.Localization.facdefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the factor of F and L (from the name)

English

Let $F$ be a functor of $C$ and $E$ such that $\operatorname{IsInvertedBy}$ holds for $W$ and $F$. Let $L$ be a functor of $C$ and $D$. Then the factor of $F$ and $L$ is an isomorphism of the composition of $L$ and the lift of $F$ and $L$ and $F$ defined as the isomorphism of $F$ and the lift of $F$ and $L$.

CategoryTheory.Localization.fullyFaithfulWhiskeringLeftdefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the left fully faithful whiskering of L and W (from the name)

English

generation took over the time limit

CategoryTheory.Localization.functorEquivalencedefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the functor equivalence of L and W (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $E$ be a set. Then the functor equivalence of $L$ and $W$ is an equivalence of the set of functors of $D$ and $E$ and $\operatorname{FunctorsInverting}$ applied to $W$ and $E$ defined as $\operatorname{asEquivalence}$ applied to the whiskering left functor of $L$ and $W$.

CategoryTheory.Localization.isoOfHomdefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the isomorphism of W and f (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $f$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $f$. Then the isomorphism of $W$ and $f$ is an isomorphism of the action of $L$ and $X$ and the action of $L$ and $Y$ defined as $\operatorname{asIso}$ applied to the map of $L$ and $f$.

CategoryTheory.Localization.isoUniqFunctordefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

no wording

English

Let $x_{5}$ be a functor of $C$ and $x_{1}$. Let $x_{6}$ be a functor of $C$ and $x_{2}$. Let $\mathrm{W'}$ be a morphism property of $C$. Let $F$ be a functor of $x_{1}$ and $x_{2}$. Let $e$ be an isomorphism of the composition of $x_{5}$ and $F$ and $x_{6}$. Then $\operatorname{isoUniqFunctor}$ applied to $x_{5}$, $x_{6}$, $\mathrm{W'}$, $F$ and $e$ is an isomorphism of $F$ and the functor of $\operatorname{uniq}$ applied to $x_{5}$, $x_{6}$ and $\mathrm{W'}$ defined as the lift natural isomorphism of the functor of $\operatorname{uniq}$ applied to $x_{5}$, $x_{6}$ and $\mathrm{W'}$ and the identity of $x_{6}$.

CategoryTheory.Localization.liftdefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the lift of F and L (from the name)

English

Let $F$ be a functor of $C$ and $E$ such that $\operatorname{IsInvertedBy}$ holds for $W$ and $F$. Let $L$ be a functor of $C$ and $D$. Then the lift of $F$ and $L$ is a functor of $D$ and $E$ defined as the action of the inverse of the functor equivalence of $L$ and $W$ and $\operatorname{mk}$ applied to $F$ and $\mathrm{hF}$.

CategoryTheory.Localization.liftNatIsodefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the lift natural isomorphism of x6 and e (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ and $x_{4}$ be functors of $C$ and $E$. Let $x_{5}$ and $x_{6}$ be functors of $D$ and $E$. Let $e$ be an isomorphism of $x_{3}$ and $x_{4}$. Then the lift natural isomorphism of $x_{6}$ and $e$ is an isomorphism of $x_{5}$ and $x_{6}$.

CategoryTheory.Localization.liftNatTransdefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the lift natural transformation of x6 and x9 (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $x_{3}$ and $x_{4}$ be functors of $C$ and $E$. Let $x_{5}$ and $x_{6}$ be functors of $D$ and $E$. Let $x_{9}$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the lift natural transformation of $x_{6}$ and $x_{9}$ is a homomorphism of $x_{5}$ and $x_{6}$ defined as the choice of the whiskering left functor of $L$ and $W$ and the composition of the homomorphism of the isomorphism of $x_{3}$ and $x_{5}$ and the composition of $x_{9}$ and the inverse of the isomorphism of $x_{4}$ and $x_{6}$.

CategoryTheory.Localization.qCompEquivalenceFromModelFunctorIsodefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the composition equivalence from model functor isomorphism of L and W (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Then the composition equivalence from model functor isomorphism of $L$ and $W$ is an isomorphism of the composition of $\operatorname{Q}$ applied to $W$ and the functor of the equivalence from model of $L$ and $W$ and $L$.

CategoryTheory.Localization.strictUniversalPropertyFixedTargetIddefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the strict universal property fixed target identity of W (from the name)

English

Let $W$ be a morphism property of $C$. Let $E$ be a set. Assume that $W$ is less than or equal to the isomorphism of $C$. Then the strict universal property fixed target identity of $W$ is a strict universal property fixed target of $W$ and $E$.

CategoryTheory.Localization.strictUniversalPropertyFixedTargetQdefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the strict universal property fixed target of W and E (from the name)

English

Let $W$ be a morphism property of $C$. Let $E$ be a set. Then the strict universal property fixed target of $W$ and $E$ is a strict universal property fixed target of $W$ and $E$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Q\_inverts}$ applied to $W$, $\operatorname{lift}$, $\operatorname{fac}$ and $\operatorname{uniq}$.

CategoryTheory.Localization.uniqdefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

no wording

English

Let $x_{5}$ be a functor of $C$ and $x_{1}$. Let $x_{6}$ be a functor of $C$ and $x_{2}$. Let $\mathrm{W'}$ be a morphism property of $C$. Then $\operatorname{uniq}$ applied to $x_{5}$, $x_{6}$ and $\mathrm{W'}$ is an equivalence of $x_{1}$ and $x_{2}$ defined as the composition of the inverse of the equivalence from model of $x_{5}$ and $\mathrm{W'}$ and the equivalence from model of $x_{6}$ and $\mathrm{W'}$.

CategoryTheory.Localization.whiskeringLeftFunctordefMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the whiskering left functor of L and W (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $E$ be a set. Then the whiskering left functor of $L$ and $W$ is a functor of the set of functors of $D$ and $E$ and $\operatorname{FunctorsInverting}$ applied to $W$ and $E$.

CategoryTheory.Localization.whiskeringLeftFunctor'defMathlib.CategoryTheory.Localization.Predicate, function or constant

Wording

the whiskering left functor of L and W (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Let $E$ be a set. Then the whiskering left functor of $L$ and $W$ is a functor of the set of functors of $D$ and $E$ and the set of functors of $C$ and $E$ defined as the action of the left whiskering of $D$ and $E$ and $L$.

Mathlib.CategoryTheory.Localization.Prod

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.proddefMathlib.CategoryTheory.Localization.Prod, function or constant

Wording

the product of x4 and x5 (from the name)

English

Let $x_{4}$ be a morphism property of $x$. Let $x_{5}$ be a morphism property of $x_{1}$. Then the product of $x_{4}$ and $x_{5}$ is a strict universal property fixed target of the product of $x_{4}$ and $x_{5}$ and $E$.

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLiftdefMathlib.CategoryTheory.Localization.Prod, function or constant

Wording

the lifting of F and hF (from the docstring)

English

Let $F$ be a functor of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $E$ such that $\operatorname{IsInvertedBy}$ holds for the product of $x_{4}$ and $x_{5}$ and $F$. Then the lifting of $F$ and $\mathrm{hF}$ is a functor of $\mathrm{Prod}$ applied to the set of localizations of $x_{4}$ and the set of localizations of $x_{5}$ and $E$.

Mathlib.CategoryTheory.Localization.Quadrifunctor

CategoryTheory.Localization.Lifting₄classMathlib.CategoryTheory.Localization.Quadrifunctor, predicate

Wording

no wording

English

Let $x_{17}$ be a functor of $x$ and $x_{4}$. Let $x_{18}$ be a functor of $x_{1}$ and $x_{5}$. Let $x_{19}$ be a functor of $x_{2}$ and $x_{6}$. Let $x_{20}$ be a functor of $x_{3}$ and $x_{7}$. Let $x_{21}$ be a morphism property of $x$. Let $x_{22}$ be a morphism property of $x_{1}$. Let $x_{23}$ be a morphism property of $x_{2}$. Let $x_{24}$ be a morphism property of $x_{3}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$. Let $\mathrm{F'}$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and the set of functors of $x_{6}$ and the set of functors of $x_{7}$ and $E$. Then we can say that $\mathrm{CategoryTheory\_\_Localization\_\_Lifting\_u2084\_}$ holds for $x_{17}$, $x_{18}$, $x_{19}$, $x_{20}$, $x_{21}$, $x_{22}$, $x_{23}$, $x_{24}$, $F$ and $\mathrm{F'}$.

CategoryTheory.Localization.Lifting₄.isodefMathlib.CategoryTheory.Localization.Quadrifunctor, function or constant

Wording

the isomorphism of F and #10 (from the name)

English

Let $x_{17}$ be a functor of $x$ and $x_{4}$. Let $x_{18}$ be a functor of $x_{1}$ and $x_{5}$. Let $x_{19}$ be a functor of $x_{2}$ and $x_{6}$. Let $x_{20}$ be a functor of $x_{3}$ and $x_{7}$. Let $x_{21}$ be a morphism property of $x$. Let $x_{22}$ be a morphism property of $x_{1}$. Let $x_{23}$ be a morphism property of $x_{2}$. Let $x_{24}$ be a morphism property of $x_{3}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$. Let $\mathrm{F'}$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and the set of functors of $x_{6}$ and the set of functors of $x_{7}$ and $E$. Then the isomorphism of $F$ and $\mathrm{F'}$ is an isomorphism of the action of the action of the action of the action of the action of the left whiskering of $E$ and $x_{17}$ and $x_{18}$ and $x_{19}$ and $x_{20}$ and $\mathrm{F'}$ and $F$ defined as $\mathrm{CategoryTheory\_\_Localization\_\_Lifting\_u2084\_\_\_proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Localization.lift₄defMathlib.CategoryTheory.Localization.Quadrifunctor, function or constant

Wording

the lift of x23 and x24 (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$ such that $\mathrm{CategoryTheory\_\_MorphismProperty\_\_IsInvertedBy\_u2084\_}$ holds for $x_{17}$, $x_{18}$, $x_{19}$, $x_{20}$ and $F$. Let $x_{21}$ be a functor of $x$ and $x_{4}$. Let $x_{22}$ be a functor of $x_{1}$ and $x_{5}$. Let $x_{23}$ be a functor of $x_{2}$ and $x_{6}$. Let $x_{24}$ be a functor of $x_{3}$ and $x_{7}$. Then the lift of $x_{23}$ and $x_{24}$ is a functor of $x_{4}$ and the set of functors of $x_{5}$ and the set of functors of $x_{6}$ and the set of functors of $x_{7}$ and $E$ defined as the action of the curry and the lift of the action of $\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_u2084\_}$ and $F$ and the product of $x_{21}$ and the product of $x_{22}$ and the product of $x_{23}$ and $x_{24}$.

CategoryTheory.Localization.lift₄NatIsodefMathlib.CategoryTheory.Localization.Quadrifunctor, function or constant

Wording

the lift natural isomorphism of x28 and e (from the name)

English

Let $x_{17}$ be a functor of $x$ and $x_{4}$. Let $x_{18}$ be a functor of $x_{1}$ and $x_{5}$. Let $x_{19}$ be a functor of $x_{2}$ and $x_{6}$. Let $x_{20}$ be a functor of $x_{3}$ and $x_{7}$. Let $x_{21}$ be a morphism property of $x$. Let $x_{22}$ be a morphism property of $x_{1}$. Let $x_{23}$ be a morphism property of $x_{2}$. Let $x_{24}$ be a morphism property of $x_{3}$. Let $x_{25}$ and $x_{26}$ be functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$. Let $x_{27}$ and $x_{28}$ be functors of $x_{4}$ and the set of functors of $x_{5}$ and the set of functors of $x_{6}$ and the set of functors of $x_{7}$ and $E$. Let $e$ be an isomorphism of $x_{25}$ and $x_{26}$. Then the lift natural isomorphism of $x_{28}$ and $e$ is an isomorphism of $x_{27}$ and $x_{28}$.

CategoryTheory.Localization.lift₄NatTransdefMathlib.CategoryTheory.Localization.Quadrifunctor, function or constant

Wording

the lift natural transformation of x28 and x31 (from the name)

English

Let $x_{17}$ be a functor of $x$ and $x_{4}$. Let $x_{18}$ be a functor of $x_{1}$ and $x_{5}$. Let $x_{19}$ be a functor of $x_{2}$ and $x_{6}$. Let $x_{20}$ be a functor of $x_{3}$ and $x_{7}$. Let $x_{21}$ be a morphism property of $x$. Let $x_{22}$ be a morphism property of $x_{1}$. Let $x_{23}$ be a morphism property of $x_{2}$. Let $x_{24}$ be a morphism property of $x_{3}$. Let $x_{25}$ and $x_{26}$ be functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$. Let $x_{27}$ and $x_{28}$ be functors of $x_{4}$ and the set of functors of $x_{5}$ and the set of functors of $x_{6}$ and the set of functors of $x_{7}$ and $E$. Let $x_{31}$ be a homomorphism of $x_{25}$ and $x_{26}$. Then the lift natural transformation of $x_{28}$ and $x_{31}$ is a homomorphism of $x_{27}$ and $x_{28}$ defined as the preimage of $\mathrm{CategoryTheory\_\_Functor\_\_fullyFaithfulUncurry\_u2084\_}$ and the lift natural transformation of the action of $\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_u2084\_}$ and $x_{28}$ and the map of $\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_u2084\_}$ and $x_{31}$.

CategoryTheory.MorphismProperty.IsInvertedBy₄defMathlib.CategoryTheory.Localization.Quadrifunctor, predicate

Wording

no wording

English

Let $x_{9}$ be a morphism property of $x$. Let $x_{10}$ be a morphism property of $x_{1}$. Let $x_{11}$ be a morphism property of $x_{2}$. Let $x_{12}$ be a morphism property of $x_{3}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_IsInvertedBy\_u2084\_}$ holds for $x_{9}$, $x_{10}$, $x_{11}$, $x_{12}$ and $F$, if $\operatorname{IsInvertedBy}$ holds for the product of $x_{9}$ and the product of $x_{10}$ and the product of $x_{11}$ and $x_{12}$ and the action of the functor of the currying and $F$.

Mathlib.CategoryTheory.Localization.Quotient

HomRel.FactorsThroughLocalizationdefMathlib.CategoryTheory.Localization.Quotient, predicate

Wording

no wording

English

Let $\mathrm{homRel}$ be a homomorphism relation of $C$. Let $W$ be a morphism property of $C$. Then $\operatorname{FactorsThroughLocalization}$ holds for $\mathrm{homRel}$ and $W$, if for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ and $g$ of $X$ and $Y$, if $\mathrm{homRel}$ holds for $X$, $Y$, $f$ and $g$, then $\operatorname{AreEqualizedByLocalization}$ holds for $W$, $f$ and $g$.

HomRel.FactorsThroughLocalization.strictUniversalPropertyFixedTargetdefMathlib.CategoryTheory.Localization.Quotient, function or constant

Wording

the strict universal property fixed target of univ and #4 (from the name)

English

Assume that $\operatorname{FactorsThroughLocalization}$ holds for $\mathrm{homRel}$ and $W$. Assume that $W$ is equal to the inverse image of $\mathrm{W'}$ and the functor of $\mathrm{homRel}$. Let $\mathrm{L'}$ be a functor of the set of quotients of $\mathrm{homRel}$ and $D$. Let $\mathrm{univ}$ be a strict universal property fixed target of $\mathrm{W'}$ and $E$. Then the strict universal property fixed target of $\mathrm{L'}$ and $\mathrm{univ}$ is a strict universal property fixed target of $W$ and $E$.

HomRel.FactorsThroughLocalization.strictUniversalPropertyFixedTarget'defMathlib.CategoryTheory.Localization.Quotient, function or constant

Wording

the strict universal property fixed target of hW and E (from the name)

English

Assume that $\operatorname{FactorsThroughLocalization}$ holds for $\mathrm{homRel}$ and $W$. Assume that $W$ is equal to the inverse image of $\mathrm{W'}$ and the functor of $\mathrm{homRel}$. Let $E$ be a set. Then the strict universal property fixed target of $\mathrm{hW}$ and $E$ is a strict universal property fixed target of $W$ and $E$ defined as the strict universal property fixed target of $\operatorname{Q}$ applied to $\mathrm{W'}$ and the strict universal property fixed target of $\mathrm{W'}$ and $E$.

Mathlib.CategoryTheory.Localization.Resolution

CategoryTheory.LocalizerMorphism.HasLeftResolutionsdefMathlib.CategoryTheory.Localization.Resolution, predicate

Wording

x6 has left resolutions (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then $x_{6}$ has left resolutions, if for all elements $x_{7}$ of $x_{1}$, $\mathrm{Nonempty}$ holds for the set of left resolutions of $x_{6}$ and $x_{7}$.

CategoryTheory.LocalizerMorphism.HasRightResolutionsdefMathlib.CategoryTheory.Localization.Resolution, predicate

Wording

x6 has right resolutions (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Then $x_{6}$ has right resolutions, if for all elements $x_{7}$ of $x_{1}$, $\mathrm{Nonempty}$ holds for the set of right resolutions of $x_{6}$ and $x_{7}$.

CategoryTheory.LocalizerMorphism.LeftResolutionstructureMathlib.CategoryTheory.Localization.Resolution, type

Wording

left resolution of x6 and x7 (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Let $x_{7}$ be an element of $x_{1}$. Then the left resolutions of $x_{6}$ and $x_{7}$ are a basic type.

CategoryTheory.LocalizerMorphism.LeftResolution.HomstructureMathlib.CategoryTheory.Localization.Resolution, type

Wording

homomorphism of L and #2 (from the name)

English

Let $L$ and $\mathrm{L'}$ be left resolutions of $x_{6}$ and $x_{7}$. Then the homomorphisms of $L$ and $\mathrm{L'}$ are a basic type.

CategoryTheory.LocalizerMorphism.LeftResolution.Hom.compdefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the composition of x8 and x9 (from the name)

English

Let $x_{8}$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $x_{9}$ be a homomorphism of $\mathrm{L'}$ and $\mathrm{L''}$. Then the composition of $x_{8}$ and $x_{9}$ is a homomorphism of $L$ and $\mathrm{L''}$.

CategoryTheory.LocalizerMorphism.LeftResolution.Hom.fdefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a homomorphism of $L$ and $\mathrm{L'}$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_LocalizerMorphism\_\_LeftResolution\_\_X\_u2081\_}$ applied to $L$ and $\mathrm{CategoryTheory\_\_LocalizerMorphism\_\_LeftResolution\_\_X\_u2081\_}$ applied to $\mathrm{L'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.LocalizerMorphism.LeftResolution.Hom.iddefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the identity in L (from the docstring)

English

Let $L$ be a left resolution of $x_{6}$ and $x_{7}$. Then the identity in $L$ is a homomorphism of $L$ and $L$.

CategoryTheory.LocalizerMorphism.LeftResolution.X₁defMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left resolution of $x_{6}$ and $x_{7}$. Then $\mathrm{CategoryTheory\_\_LocalizerMorphism\_\_LeftResolution\_\_X\_u2081\_}$ applied to $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.LocalizerMorphism.LeftResolution.opdefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the opposite of L (from the name)

English

Let $L$ be a left resolution of $x_{6}$ and $x_{7}$. Then the opposite of $L$ is a right resolution of the opposite localizer morphism of $x_{6}$ and $\operatorname{op}$ applied to $x_{7}$ defined as $\operatorname{mk}$ applied to the opposite in $\operatorname{w}$ applied to $L$ and $\operatorname{hw}$ applied to $L$.

CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalencedefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the opposite equivalence of x6 and x7 (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Let $x_{7}$ be an element of $x_{1}$. Then the opposite equivalence of $x_{6}$ and $x_{7}$ is an equivalence of the set of opposites of the set of left resolutions of $x_{6}$ and $x_{7}$ and the set of right resolutions of the opposite localizer morphism of $x_{6}$ and $\operatorname{op}$ applied to $x_{7}$.

CategoryTheory.LocalizerMorphism.LeftResolution.opFunctordefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the functor of x6 and x7 (from the docstring)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Let $x_{7}$ be an element of $x_{1}$. Then the functor of $x_{6}$ and $x_{7}$ is a functor of the set of opposites of the set of left resolutions of $x_{6}$ and $x_{7}$ and the set of right resolutions of the opposite localizer morphism of $x_{6}$ and $\operatorname{op}$ applied to $x_{7}$.

CategoryTheory.LocalizerMorphism.LeftResolution.unopdefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the opposite of L (from the name)

English

Let $L$ be a left resolution of the opposite localizer morphism of $x_{6}$ and $x_{7}$. Then the opposite of $L$ is a right resolution of $x_{6}$ and the opposite of $x_{7}$.

CategoryTheory.LocalizerMorphism.LeftResolution.wdefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left resolution of $x_{6}$ and $x_{7}$. Then $\operatorname{w}$ applied to $\mathrm{self}$ is a homomorphism of the action of the functor of $x_{6}$ and $\mathrm{CategoryTheory\_\_LocalizerMorphism\_\_LeftResolution\_\_X\_u2081\_}$ applied to $\mathrm{self}$ and $x_{7}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.LocalizerMorphism.RightResolutionstructureMathlib.CategoryTheory.Localization.Resolution, type

Wording

right resolution of x6 and x7 (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Let $x_{7}$ be an element of $x_{1}$. Then the right resolutions of $x_{6}$ and $x_{7}$ are a basic type.

CategoryTheory.LocalizerMorphism.RightResolution.HomstructureMathlib.CategoryTheory.Localization.Resolution, type

Wording

homomorphism of R and #2 (from the name)

English

Let $R$ and $\mathrm{R'}$ be right resolutions of $x_{6}$ and $x_{7}$. Then the homomorphisms of $R$ and $\mathrm{R'}$ are a basic type.

CategoryTheory.LocalizerMorphism.RightResolution.Hom.compdefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the composition of x8 and x9 (from the name)

English

Let $x_{8}$ be a homomorphism of $R$ and $\mathrm{R'}$. Let $x_{9}$ be a homomorphism of $\mathrm{R'}$ and $\mathrm{R''}$. Then the composition of $x_{8}$ and $x_{9}$ is a homomorphism of $R$ and $\mathrm{R''}$.

CategoryTheory.LocalizerMorphism.RightResolution.Hom.fdefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a homomorphism of $R$ and $\mathrm{R'}$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_LocalizerMorphism\_\_RightResolution\_\_X\_u2081\_}$ applied to $R$ and $\mathrm{CategoryTheory\_\_LocalizerMorphism\_\_RightResolution\_\_X\_u2081\_}$ applied to $\mathrm{R'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.LocalizerMorphism.RightResolution.Hom.iddefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the identity in R (from the docstring)

English

Let $R$ be a right resolution of $x_{6}$ and $x_{7}$. Then the identity in $R$ is a homomorphism of $R$ and $R$.

CategoryTheory.LocalizerMorphism.RightResolution.X₁defMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a right resolution of $x_{6}$ and $x_{7}$. Then $\mathrm{CategoryTheory\_\_LocalizerMorphism\_\_RightResolution\_\_X\_u2081\_}$ applied to $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.LocalizerMorphism.RightResolution.opdefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the opposite of L (from the name)

English

Let $L$ be a right resolution of $x_{6}$ and $x_{7}$. Then the opposite of $L$ is a left resolution of the opposite localizer morphism of $x_{6}$ and $\operatorname{op}$ applied to $x_{7}$ defined as $\operatorname{mk}$ applied to the opposite in $\operatorname{w}$ applied to $L$ and $\operatorname{hw}$ applied to $L$.

CategoryTheory.LocalizerMorphism.RightResolution.unopdefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the opposite of L (from the name)

English

Let $L$ be a right resolution of the opposite localizer morphism of $x_{6}$ and $x_{7}$. Then the opposite of $L$ is a left resolution of $x_{6}$ and the opposite of $x_{7}$.

CategoryTheory.LocalizerMorphism.RightResolution.unopFunctordefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

the functor of x6 and x7 (from the docstring)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Let $x_{7}$ be an opposite of $x_{1}$. Then the functor of $x_{6}$ and $x_{7}$ is a functor of the set of opposites of the set of right resolutions of the opposite localizer morphism of $x_{6}$ and $x_{7}$ and the set of left resolutions of $x_{6}$ and the opposite of $x_{7}$.

CategoryTheory.LocalizerMorphism.RightResolution.wdefMathlib.CategoryTheory.Localization.Resolution, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a right resolution of $x_{6}$ and $x_{7}$. Then $\operatorname{w}$ applied to $\mathrm{self}$ is a homomorphism of $x_{7}$ and the action of the functor of $x_{6}$ and $\mathrm{CategoryTheory\_\_LocalizerMorphism\_\_RightResolution\_\_X\_u2081\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Mathlib.CategoryTheory.Localization.SmallHom

CategoryTheory.Localization.HasSmallLocalizedHomclassMathlib.CategoryTheory.Localization.SmallHom, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $X$ and $Y$ be elements of $C$. Then we can say that $\operatorname{HasSmallLocalizedHom}$ holds for $W$, $X$ and $Y$.

CategoryTheory.Localization.SmallHomdefMathlib.CategoryTheory.Localization.SmallHom, type

Wording

small homomorphism of X and Y (from the name)

English

Let $W$ be a morphism property of $C$. Let $X$ and $Y$ be elements of $C$. Then a small homomorphism of $X$ and $Y$ is an element of the function that maps $W$, $X$ and $Y$ to the set of shrinks of the set of homomorphisms of the action of $\operatorname{Q}$ applied to $W$ and $X$ and the action of $\operatorname{Q}$ applied to $W$ and $Y$.

CategoryTheory.Localization.SmallHom.chgUnivdefMathlib.CategoryTheory.Localization.SmallHom, function or constant

Wording

no wording

English

$\operatorname{chgUniv}$ is an equivalence from the set of small homomorphisms of $X$ and $Y$ to the set of small homomorphisms of $X$ and $Y$ defined as the composition of the equivalence of $W$ and $\operatorname{Q}$ applied to $W$ and the inverse of the equivalence of $W$ and $\operatorname{Q}$ applied to $W$.

CategoryTheory.Localization.SmallHom.compdefMathlib.CategoryTheory.Localization.SmallHom, function or constant

Wording

the composition of x1 and x2 (from the name)

English

Let $x_{1}$ be a small homomorphism of $X$ and $Y$. Let $x_{2}$ be a small homomorphism of $Y$ and $Z$. Then the composition of $x_{1}$ and $x_{2}$ is a small homomorphism of $X$ and $Z$ defined as $\operatorname{symm}$ applied to the equivalence of $W$ and $\operatorname{Q}$ applied to $W$ and the composition of $\operatorname{equiv}$ applied to $W$, $\operatorname{Q}$ applied to $W$ and $x_{1}$ and $\operatorname{equiv}$ applied to $W$, $\operatorname{Q}$ applied to $W$ and $x_{2}$.

CategoryTheory.Localization.SmallHom.equivdefMathlib.CategoryTheory.Localization.SmallHom, function or constant

Wording

the equivalence of W and L (from the name)

English

Let $W$ be a morphism property of $C$. Let $L$ be a functor of $C$ and $D$. Then the equivalence of $W$ and $L$ is an equivalence from the set of small homomorphisms of $X$ and $Y$ to the set of homomorphisms of the action of $L$ and $X$ and the action of $L$ and $Y$ defined as the composition of the inverse of the equivalence shrink of the set of homomorphisms of the action of $\operatorname{Q}$ applied to $W$ and $X$ and the action of $\operatorname{Q}$ applied to $W$ and $Y$ and the homomorphism equivalence of $\operatorname{Q}$ applied to $W$ and $L$.

CategoryTheory.Localization.SmallHom.mkdefMathlib.CategoryTheory.Localization.SmallHom, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{mk}$ applied to $W$ and $f$ is a small homomorphism of $X$ and $Y$ defined as $\operatorname{symm}$ applied to the equivalence of $W$ and $\operatorname{Q}$ applied to $W$ and the map of $\operatorname{Q}$ applied to $W$ and $f$.

CategoryTheory.Localization.SmallHom.mkInvdefMathlib.CategoryTheory.Localization.SmallHom, function or constant

Wording

the inverse of f and hf (from the name)

English

Let $f$ be a homomorphism of $Y$ and $X$ such that $W$ holds for $Y$, $X$ and $f$. Then the inverse of $f$ and $\mathrm{hf}$ is a small homomorphism of $X$ and $Y$ defined as $\operatorname{symm}$ applied to the equivalence of $W$ and $\operatorname{Q}$ applied to $W$ and the inverse of the isomorphism of $W$ and $f$.

CategoryTheory.LocalizerMorphism.smallHomMapdefMathlib.CategoryTheory.Localization.SmallHom, function or constant

Wording

the small homomorphism map of x6 and f (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{2}$ and $x_{5}$. Let $f$ be a small homomorphism of $X$ and $Y$. Then the small homomorphism map of $x_{6}$ and $f$ is a small homomorphism of the action of the functor of $x_{6}$ and $X$ and the action of the functor of $x_{6}$ and $Y$ defined as $\operatorname{symm}$ applied to the equivalence of $x_{5}$ and $\operatorname{Q}$ applied to $x_{5}$ and $\operatorname{homCongr}$ applied to the application of the inverse of the isomorphism of $\operatorname{Q}$ applied to $x_{5}$ and the localized functor of $\operatorname{Q}$ applied to $x_{2}$ and $\operatorname{Q}$ applied to $x_{5}$ and $X$, the application of the inverse of the isomorphism of $\operatorname{Q}$ applied to $x_{5}$ and the localized functor of $\operatorname{Q}$ applied to $x_{2}$ and $\operatorname{Q}$ applied to $x_{5}$ and $Y$ and the map of the localized functor of $\operatorname{Q}$ applied to $x_{2}$ and $\operatorname{Q}$ applied to $x_{5}$ and $\operatorname{equiv}$ applied to $x_{2}$, $\operatorname{Q}$ applied to $x_{2}$ and $f$.

CategoryTheory.LocalizerMorphism.smallHomMap'defMathlib.CategoryTheory.Localization.SmallHom, function or constant

Wording

the small homomorphism map of eY and f (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{2}$ and $x_{5}$. Let $\mathrm{eX}$ be an isomorphism of the action of the functor of $x_{6}$ and $X$ and $\mathrm{X'}$. Let $\mathrm{eY}$ be an isomorphism of the action of the functor of $x_{6}$ and $Y$ and $\mathrm{Y'}$. Let $f$ be a small homomorphism of $X$ and $Y$. Then the small homomorphism map of $\mathrm{eY}$ and $f$ is a small homomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$ defined as the composition of $\operatorname{mk}$ applied to $x_{5}$ and the inverse of $\mathrm{eX}$ and the composition of the small homomorphism map of $x_{6}$ and $f$ and $\operatorname{mk}$ applied to $x_{5}$ and the homomorphism of $\mathrm{eY}$.

Mathlib.CategoryTheory.Localization.SmallShiftedHom

CategoryTheory.Localization.HasSmallLocalizedShiftedHomdefMathlib.CategoryTheory.Localization.SmallShiftedHom, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $M$ be a set. Let $X$ and $Y$ be elements of $C$. Then $\operatorname{HasSmallLocalizedShiftedHom}$ holds for $W$, $M$, $X$ and $Y$, if for all elements $a$ and $b$ of $M$, $\operatorname{HasSmallLocalizedHom}$ holds for $W$, the action of the shift functor of $C$ and $a$ and $X$ and the action of the shift functor of $C$ and $b$ and $Y$.

CategoryTheory.Localization.SmallHom.shiftdefMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

the shift of f and a (from the name)

English

Let $f$ be a small homomorphism of $X$ and $Y$. Let $a$ be an element of $M$. Then the shift of $f$ and $a$ is a small homomorphism of the action of the shift functor of $C$ and $a$ and $X$ and the action of the shift functor of $C$ and $a$ and $Y$ defined as the small homomorphism map of the shift localizer morphism of $W$ and $a$ and $f$.

CategoryTheory.Localization.SmallShiftedHomdefMathlib.CategoryTheory.Localization.SmallShiftedHom, type

Wording

small shifted homomorphism of Y and m (from the name)

English

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

CategoryTheory.Localization.SmallShiftedHom.chgUnivdefMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

no wording

English

$\operatorname{chgUniv}$ is an equivalence from the set of small shifted homomorphisms of $Y$ and $m$ to the set of small shifted homomorphisms of $Y$ and $m$ defined as $\operatorname{chgUniv}$.

CategoryTheory.Localization.SmallShiftedHom.compdefMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

the composition of f and g (from the name)

English

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

CategoryTheory.Localization.SmallShiftedHom.equivdefMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

the equivalence of W and L (from the name)

English

Let $W$ be a morphism property of $C$. Let $L$ be a functor of $C$ and $D$. Then the equivalence of $W$ and $L$ is an equivalence from the set of small shifted homomorphisms of $Y$ and $m$ to the set of shifted homomorphisms of the action of $L$ and $Y$ and $m$ defined as the composition of the equivalence of $W$ and $L$ and the homomorphism to equivalence of the application of the commutative shift isomorphism of $L$ and $m$ and $Y$.

CategoryTheory.Localization.SmallShiftedHom.mkdefMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $f$ be a shifted homomorphism of $Y$ and $m$. Then $\operatorname{mk}$ applied to $W$ and $f$ is a small shifted homomorphism of $Y$ and $m$ defined as $\operatorname{mk}$ applied to $W$ and $f$.

CategoryTheory.Localization.SmallShiftedHom.mk₀defMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. 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\_\_Localization\_\_SmallShiftedHom\_\_mk\_u2080\_}$ applied to $W$, $x_{3}$, $h_{1}$ and $f$ is a small shifted homomorphism of $Y$ and $x_{3}$ defined as $\operatorname{mk}$ applied to $W$ and $\mathrm{CategoryTheory\_\_ShiftedHom\_\_mk\_u2080\_}$ applied to $x_{3}$, $h_{1}$ and $f$.

CategoryTheory.Localization.SmallShiftedHom.mk₀InvdefMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

the formal inverse in x3 (from the docstring)

English

Let $x_{3}$ be an element of $M$ such that $\EqtMACRoH {x_{3}}{0}$. Let $f$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $f$. Then the formal inverse in $x_{3}$ is a small shifted homomorphism of $X$ and $x_{3}$.

CategoryTheory.Localization.SmallShiftedHom.postcompEquivdefMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

the postcomposition on the types of f and hf (from the docstring)

English

Let $f$ be a homomorphism of $Y$ and $Z$ such that $W$ holds for $Y$, $Z$ and $f$. Then the postcomposition on the types of $f$ and $\mathrm{hf}$ is an equivalence from the set of small shifted homomorphisms of $Y$ and $a$ to the set of small shifted homomorphisms of $Z$ and $a$.

CategoryTheory.Localization.SmallShiftedHom.precompEquivdefMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

the precomposition on the types of f and hf (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $f$. Then the precomposition on the types of $f$ and $\mathrm{hf}$ is an equivalence from the set of small shifted homomorphisms of $Z$ and $a$ to the set of small shifted homomorphisms of $Z$ and $a$.

CategoryTheory.Localization.SmallShiftedHom.shiftdefMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

the shift of n and h3 (from the name)

English

Let $f$ be a small shifted homomorphism of $Y$ and $a$. Let $n$ and $\mathrm{a'}$ be elements of $M$ such that $\EqtMACRoH {a + n}{\mathrm{a'}}$. Then the shift of $n$ and $\mathrm{a'}$ is a small homomorphism of the action of the shift functor of $C$ and $n$ and $X$ and the action of the shift functor of $C$ and $\mathrm{a'}$ and $Y$ defined as the composition of the shift of $f$ and $n$ and $\operatorname{mk}$ applied to $W$ and the component of the inverse of the shift functor sum of $n$ and $\mathrm{a'}$ and $Y$.

CategoryTheory.LocalizerMorphism.smallShiftedHomMapdefMathlib.CategoryTheory.Localization.SmallShiftedHom, function or constant

Wording

the small shifted homomorphism map of eY and f (from the name)

English

Let $x_{6}$ be a localizer morphism of $x_{4}$ and $x_{5}$. Let $\mathrm{eX}$ be an isomorphism of the action of the functor of $x_{6}$ and $x_{11}$ and $x_{13}$. Let $\mathrm{eY}$ be an isomorphism of the action of the functor of $x_{6}$ and $x_{12}$ and $x_{14}$. Let $f$ be a small shifted homomorphism of $x_{12}$ and $m$. Then the small shifted homomorphism map of $\mathrm{eY}$ and $f$ is a small shifted homomorphism of $x_{14}$ and $m$ defined as the small homomorphism map of the composition of the application of the commutative shift isomorphism of the functor of $x_{6}$ and $m$ and $x_{12}$ and the map isomorphism of the shift functor of $x_{2}$ and $m$ and $\mathrm{eY}$ and $f$.

Mathlib.CategoryTheory.Localization.StructuredArrow

CategoryTheory.Localization.structuredArrowEquivdefMathlib.CategoryTheory.Localization.StructuredArrow, function or constant

Wording

the structured arrow equivalence of L and #3 (from the name)

English

Let $W$ be a morphism property of $C$. Let $L$ be a functor of $C$ and $D$. Let $\mathrm{L'}$ be a functor of $C$ and $\mathrm{D'}$. Then the structured arrow equivalence of $L$ and $\mathrm{L'}$ is an equivalence from the set of structured arrows of the action of $L$ and $X$ and $L$ to the set of structured arrows of the action of $\mathrm{L'}$ and $X$ and $\mathrm{L'}$.

Mathlib.CategoryTheory.Localization.Triangulated

CategoryTheory.Functor.essImageDistTriangdefMathlib.CategoryTheory.Localization.Triangulated, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Then $\operatorname{essImageDistTriang}$ applied to $L$ is an element of the power set of the set of triangles of $D$ defined as $\operatorname{ofPred}$ applied to the function that maps $T$ to the proposition that there exists a triangle $\mathrm{T'}$ of $C$, such that there exists an isomorphism $x_{7}$ of $T$ and the action of the map triangle of $L$ and $\mathrm{T'}$, such that $\mathrm{T'}$ is an element of the distinguished triangle.

CategoryTheory.MorphismProperty.IsCompatibleWithTriangulationclassMathlib.CategoryTheory.Localization.Triangulated, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{IsCompatibleWithTriangulation}$ holds for $W$.

Mathlib.CategoryTheory.Localization.Trifunctor

CategoryTheory.Localization.Lifting₃classMathlib.CategoryTheory.Localization.Trifunctor, predicate

Wording

no wording

English

CategoryTheory.Localization.Lifting₃.isodefMathlib.CategoryTheory.Localization.Trifunctor, function or constant

Wording

the isomorphism of F and #8 (from the name)

English

Let $x_{13}$ be a functor of $x$ and $x_{3}$. Let $x_{14}$ be a functor of $x_{1}$ and $x_{4}$. Let $x_{15}$ be a functor of $x_{2}$ and $x_{5}$. Let $x_{16}$ be a morphism property of $x$. Let $x_{17}$ be a morphism property of $x_{1}$. Let $x_{18}$ be a morphism property of $x_{2}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$. Let $\mathrm{F'}$ be a functor of $x_{3}$ and the set of functors of $x_{4}$ and the set of functors of $x_{5}$ and $E$. Then the isomorphism of $F$ and $\mathrm{F'}$ is an isomorphism of the action of the action of the action of the action of the left whiskering of $E$ and $x_{13}$ and $x_{14}$ and $x_{15}$ and $\mathrm{F'}$ and $F$ defined as $\mathrm{CategoryTheory\_\_Localization\_\_Lifting\_u2083\_\_\_proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Localization.associatordefMathlib.CategoryTheory.Localization.Trifunctor, function or constant

Wording

the associator of #15 and #16 (from the name)

English

Let $x_{22}$ be a functor of $x$ and $x_{5}$. Let $x_{23}$ be a functor of $x_{1}$ and $x_{6}$. Let $x_{24}$ be a functor of $x_{2}$ and $x_{7}$. Let $x_{25}$ be a functor of $x_{3}$ and $x_{8}$. Let $x_{26}$ be a functor of $x_{4}$ and $x_{9}$. Let $L$ be a functor of $C$ and $D$. Let $x_{27}$ be a morphism property of $x$. Let $x_{28}$ be a morphism property of $x_{1}$. Let $x_{29}$ be a morphism property of $x_{2}$. Let $x_{30}$ be a morphism property of $x_{3}$. Let $x_{31}$ be a morphism property of $x_{4}$. Let $\mathrm{iso}$ be an isomorphism of the bifunctor composition of $x_{32}$ and $G$ and the bifunctor composition of $F$ and $x_{33}$. Let $x_{34}$ be a functor of $x_{5}$ and the set of functors of $x_{6}$ and $x_{8}$. Let $\mathrm{G'}$ be a functor of $x_{8}$ and the set of functors of $x_{7}$ and $D$. Let $\mathrm{F'}$ be a functor of $x_{5}$ and the set of functors of $x_{9}$ and $D$. Let $x_{35}$ be a functor of $x_{6}$ and the set of functors of $x_{7}$ and $x_{9}$. Then the associator of $\mathrm{F'}$ and $x_{35}$ is an isomorphism of the bifunctor composition of $x_{34}$ and $\mathrm{G'}$ and the bifunctor composition of $\mathrm{F'}$ and $x_{35}$ defined as the lift natural isomorphism of the bifunctor composition of $\mathrm{F'}$ and $x_{35}$ and the map isomorphism of the action of the postcomposition and $L$ and $\mathrm{iso}$.

CategoryTheory.Localization.lift₃defMathlib.CategoryTheory.Localization.Trifunctor, function or constant

Wording

the lift of x17 and x18 (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$ such that $\mathrm{CategoryTheory\_\_MorphismProperty\_\_IsInvertedBy\_u2083\_}$ holds for $x_{13}$, $x_{14}$, $x_{15}$ and $F$. Let $x_{16}$ be a functor of $x$ and $x_{3}$. Let $x_{17}$ be a functor of $x_{1}$ and $x_{4}$. Let $x_{18}$ be a functor of $x_{2}$ and $x_{5}$. Then the lift of $x_{17}$ and $x_{18}$ is a functor of $x_{3}$ and the set of functors of $x_{4}$ and the set of functors of $x_{5}$ and $E$ defined as the action of the curry and the lift of the action of $\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_u2083\_}$ and $F$ and the product of $x_{16}$ and the product of $x_{17}$ and $x_{18}$.

CategoryTheory.Localization.lift₃NatIsodefMathlib.CategoryTheory.Localization.Trifunctor, function or constant

Wording

the lift natural isomorphism of x22 and e (from the name)

English

CategoryTheory.Localization.lift₃NatTransdefMathlib.CategoryTheory.Localization.Trifunctor, function or constant

Wording

the lift natural transformation of x22 and x25 (from the name)

English

Let $x_{13}$ be a functor of $x$ and $x_{3}$. Let $x_{14}$ be a functor of $x_{1}$ and $x_{4}$. Let $x_{15}$ be a functor of $x_{2}$ and $x_{5}$. Let $x_{16}$ be a morphism property of $x$. Let $x_{17}$ be a morphism property of $x_{1}$. Let $x_{18}$ be a morphism property of $x_{2}$. Let $x_{19}$ and $x_{20}$ be functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$. Let $x_{21}$ and $x_{22}$ be functors of $x_{3}$ and the set of functors of $x_{4}$ and the set of functors of $x_{5}$ and $E$. Let $x_{25}$ be a homomorphism of $x_{19}$ and $x_{20}$. Then the lift natural transformation of $x_{22}$ and $x_{25}$ is a homomorphism of $x_{21}$ and $x_{22}$ defined as the preimage of $\mathrm{CategoryTheory\_\_Functor\_\_fullyFaithfulUncurry\_u2083\_}$ and the lift natural transformation of the action of $\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_u2083\_}$ and $x_{22}$ and the map of $\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_u2083\_}$ and $x_{25}$.

CategoryTheory.MorphismProperty.IsInvertedBy₃defMathlib.CategoryTheory.Localization.Trifunctor, predicate

Wording

no wording

English

Let $x_{7}$ be a morphism property of $x$. Let $x_{8}$ be a morphism property of $x_{1}$. Let $x_{9}$ be a morphism property of $x_{2}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_IsInvertedBy\_u2083\_}$ holds for $x_{7}$, $x_{8}$, $x_{9}$ and $F$, if $\operatorname{IsInvertedBy}$ holds for the product of $x_{7}$ and the product of $x_{8}$ and $x_{9}$ and the action of the functor of the currying and $F$.

Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

CategoryTheory.ChosenPullbacksdefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, type

Wording

chosen pullback of C (from the name)

English

Let $C$ be a set. Then a chosen pullback 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 $f$ of $Y$ and $X$ to elements of $\operatorname{ChosenPullbacksAlong}$ applied to $f$.

CategoryTheory.ChosenPullbacksAlongclassMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, predicate

Wording

no wording

English

Let $f$ be a homomorphism of $Y$ and $X$. Then we can say that $\operatorname{ChosenPullbacksAlong}$ holds for $f$.

CategoryTheory.ChosenPullbacksAlong.fstdefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the first component of f and g (from the name)

English

Let $f$ be a homomorphism of $Y$ and $X$. Let $g$ be a homomorphism of $Z$ and $X$. Then the first component of $f$ and $g$ is a homomorphism of the pullback object of $f$ and $g$ and $Y$ defined as the left of the first component of $f$ and $g$.

CategoryTheory.ChosenPullbacksAlong.fst'defMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the first component of f and g (from the name)

English

Let $f$ be a homomorphism of $Y$ and $X$. Let $g$ be a homomorphism of $Z$ and $X$. Then the first component of $f$ and $g$ is a homomorphism of the action of the map of $g$ and the action of the pullback of $g$ and $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $f$ defined as the component of the counit of the map pullback adjoint of $g$ and $\operatorname{mk}$ applied to $f$.

CategoryTheory.ChosenPullbacksAlong.isLimitPullbackConedefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the canonical pullback cone of f and g (from the docstring)

English

Let $f$ be a homomorphism of $Y$ and $X$. Let $g$ be a homomorphism of $Z$ and $X$. Then the canonical pullback cone of $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the canonical pullback cone from the data of $f$ and $g$.

CategoryTheory.ChosenPullbacksAlong.liftdefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the lift of a and b (from the name)

English

Let $a$ be a homomorphism of $W$ and $Y$. Let $b$ be a homomorphism of $W$ and $Z$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $a$ and $f$ is equal to the composition of $b$ and $g$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_LocallyCartesianClosed\_\_ChosenPullbacksAlong\_\_0\_\_\_auto\_75}$. Then the lift of $a$ and $b$ is a homomorphism of $W$ and the pullback object of $f$ and $g$.

CategoryTheory.ChosenPullbacksAlong.mapPullbackAdjdefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the map pullback adjoint of f (from the name)

English

Let $f$ be a homomorphism of $Y$ and $X$. Then the map pullback adjoint of $f$ is an adjunction of the map of $f$ and the pullback of $f$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.ChosenPullbacksAlong.pullbackdefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the pullback of f (from the name)

English

Let $f$ be a homomorphism of $Y$ and $X$. Then the pullback of $f$ is a functor of $\operatorname{Over}$ applied to $X$ and $\operatorname{Over}$ applied to $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.ChosenPullbacksAlong.pullbackCompdefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

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

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback composition of $f$ and $g$ is an isomorphism of the pullback of the composition of $f$ and $g$ and the composition of the pullback of $g$ and the pullback of $f$ defined as $\operatorname{rightAdjointUniq}$ applied to the map pullback adjoint of the composition of $f$ and $g$ and the map pullback adjoint of the composition of $f$ and $g$.

CategoryTheory.ChosenPullbacksAlong.pullbackConedefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the canonical pullback cone from the data of f and g (from the docstring)

English

Let $f$ be a homomorphism of $Y$ and $X$. Let $g$ be a homomorphism of $Z$ and $X$. Then the canonical pullback cone from the data of $f$ and $g$ is a pullback cone of $f$ and $g$.

CategoryTheory.ChosenPullbacksAlong.pullbackIddefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the pullback identity of X (from the name)

English

Let $X$ be an element of $C$. Then the pullback identity of $X$ is an isomorphism of the pullback of the identity morphism of $X$ and the identity of $\operatorname{Over}$ applied to $X$ defined as $\operatorname{rightAdjointUniq}$ applied to the map pullback adjoint of the identity morphism of $X$ and the map pullback adjoint of the identity morphism of $X$.

CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullbackdefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the pullback isomorphism over pullback of g (from the name)

English

Let $g$ be a homomorphism of $Z$ and $X$. Then the pullback isomorphism over pullback of $g$ is an isomorphism of the pullback of $g$ and the pullback of $g$ defined as $\operatorname{rightAdjointUniq}$ applied to the map pullback adjoint of $g$ and the map pullback adjoint of $g$.

CategoryTheory.ChosenPullbacksAlong.pullbackMapdefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the pullback map of h and h1 (from the name)

English

Let $f$ be a homomorphism of $Y$ and $X$. Let $g$ be a homomorphism of $Z$ and $X$. Let $\mathrm{f'}$ be a homomorphism of $\mathrm{Y'}$ and $\mathrm{X'}$. Let $\mathrm{g'}$ be a homomorphism of $\mathrm{Z'}$ and $\mathrm{X'}$. Let $x_{3}$ be a homomorphism of $\mathrm{Y'}$ and $Y$. Let $x_{4}$ be a homomorphism of $\mathrm{Z'}$ and $Z$. Let $x_{5}$ be a homomorphism of $\mathrm{X'}$ and $X$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $\mathrm{f'}$ and $x_{5}$ is equal to the composition of $x_{3}$ and $f$ and $\mathrm{CategoryTheory\_\_ChosenPullbacksAlong\_\_pullbackMap\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of $\mathrm{g'}$ and $x_{5}$ is equal to the composition of $x_{4}$ and $g$ and $\mathrm{CategoryTheory\_\_ChosenPullbacksAlong\_\_pullbackMap\_\_\_auto\_3}$. Then the pullback map of $x_{4}$ and $x_{5}$ is a homomorphism of the pullback object of $\mathrm{f'}$ and $\mathrm{g'}$ and the pullback object of $f$ and $g$.

CategoryTheory.ChosenPullbacksAlong.pullbackObjdefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the pullback object of f and g (from the name)

English

Let $f$ be a homomorphism of $Y$ and $X$. Let $g$ be a homomorphism of $Z$ and $X$. Then the pullback object of $f$ and $g$ is an element of $C$ defined as the left of the action of the pullback of $g$ and $\operatorname{mk}$ applied to $f$.

CategoryTheory.ChosenPullbacksAlong.snddefMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the second component of f and g (from the name)

English

Let $f$ be a homomorphism of $Y$ and $X$. Let $g$ be a homomorphism of $Z$ and $X$. Then the second component of $f$ and $g$ is a homomorphism of the pullback object of $f$ and $g$ and $Z$ defined as the homomorphism of the action of the pullback of $g$ and $\operatorname{mk}$ applied to $f$.

CategoryTheory.ChosenPullbacksAlong.snd'defMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong, function or constant

Wording

the second component of f and g (from the name)

English

Let $f$ be a homomorphism of $Y$ and $X$. Let $g$ be a homomorphism of $Z$ and $X$. Then the second component of $f$ and $g$ is a homomorphism of the action of the map of $g$ and the action of the pullback of $g$ and $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$.

Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

CategoryTheory.ExponentiableMorphismclassMathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism, predicate

Wording

f is a exponentiable morphism (from the name)

English

Let $f$ be a homomorphism of $I$ and $J$. Then we can say that $f$ is an exponentiable morphism.

CategoryTheory.ExponentiableMorphism.coevdefMathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism, function or constant

Wording

the dependent coevaluation natural transformation of f (from the docstring)

English

Let $f$ be a homomorphism of $I$ and $J$. Then the dependent coevaluation natural transformation of $f$ is a homomorphism of the identity of $\operatorname{Over}$ applied to $J$ and the composition of the pullback of $f$ and the pushforward functor of $f$ defined as the unit of the pushforward functor of $f$.

CategoryTheory.ExponentiableMorphism.evdefMathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $I$ and $J$. Then $\operatorname{ev}$ applied to $f$ is a homomorphism of the composition of the pushforward functor of $f$ and the pullback of $f$ and the identity of $\operatorname{Over}$ applied to $I$ defined as the counit of the pushforward functor of $f$.

CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdjdefMathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism, function or constant

Wording

the pushforward functor of f (from the docstring)

English

Let $f$ be a homomorphism of $I$ and $J$. Then the pushforward functor of $f$ is an adjunction of the pullback of $f$ and the pushforward functor of $f$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.ExponentiableMorphism.pushforwarddefMathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism, function or constant

Wording

the pushforward functor of f (from the docstring)

English

Let $f$ be a homomorphism of $I$ and $J$. Then the pushforward functor of $f$ is a functor of $\operatorname{Over}$ applied to $I$ and $\operatorname{Over}$ applied to $J$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.ExponentiableMorphism.pushforwardCompdefMathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism, function or constant

Wording

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

English

Let $f$ be a homomorphism of $I$ and $J$. Let $g$ be a homomorphism of $J$ and $K$. Then the pushforward composition of $f$ and $g$ is an isomorphism of the pushforward functor of the composition of $f$ and $g$ and the composition of the pushforward functor of $f$ and the pushforward functor of $g$ defined as $\operatorname{rightAdjointUniq}$ applied to the pushforward functor of the composition of $f$ and $g$ and the pushforward functor of the composition of $f$ and $g$.

CategoryTheory.ExponentiableMorphism.pushforwardCurrydefMathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism, function or constant

Wording

the currying of u (from the docstring)

English

Let $u$ be a homomorphism of the action of the pullback of $f$ and $A$ and $X$. Then the currying of $u$ is a homomorphism of $A$ and the action of the pushforward functor of $f$ and $X$ defined as $\operatorname{homEquiv}$ applied to the pushforward functor of $f$, $A$, $X$ and $u$.

CategoryTheory.ExponentiableMorphism.pushforwardIddefMathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism, function or constant

Wording

the pushforward identity of I (from the name)

English

Let $I$ be an element of $C$. Then the pushforward identity of $I$ is an isomorphism of the pushforward functor of the identity morphism of $I$ and the identity of $\operatorname{Over}$ applied to $I$ defined as $\operatorname{rightAdjointUniq}$ applied to the pushforward functor of the identity morphism of $I$ and the pushforward functor of the identity morphism of $I$.

CategoryTheory.ExponentiableMorphism.pushforwardUncurrydefMathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism, function or constant

Wording

no wording

English

Let $v$ be a homomorphism of $A$ and the action of the pushforward functor of $f$ and $X$. Then $\operatorname{pushforwardUncurry}$ applied to $v$ is a homomorphism of the action of the pullback of $f$ and $A$ and $X$ defined as the inverse function of the homomorphism equivalence of $A$ and $X$ and $v$.

CategoryTheory.IsExponentiabledefMathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism, function or constant

Wording

no wording

English

There is a morphism property of $C$. Proof. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $f$ be arbitrary. By f. By CategoryTheory__ChosenPullbacksAlong__pullback. By CategoryTheory__Functor__IsLeftAdjoint.

Mathlib.CategoryTheory.LocallyCartesianClosed.Over

CategoryTheory.ChosenPullbacksAlong.binaryFandefMathlib.CategoryTheory.LocallyCartesianClosed.Over, function or constant

Wording

no wording

English

Let $Y$ and $Z$ be elements of $\operatorname{Over}$ applied to $X$. Then $\operatorname{binaryFan}$ applied to $Y$ and $Z$ is an element of $\operatorname{BinaryFan}$ applied to $Y$ and $Z$ defined as $\operatorname{mk}$ applied to the first component of the homomorphism of $Y$ and the homomorphism of $Z$ and the second component of the homomorphism of $Y$ and the homomorphism of $Z$.

CategoryTheory.ChosenPullbacksAlong.binaryFanIsBinaryProductdefMathlib.CategoryTheory.LocallyCartesianClosed.Over, function or constant

Wording

no wording

English

Let $Y$ and $Z$ be elements of $\operatorname{Over}$ applied to $X$. Then $\operatorname{binaryFanIsBinaryProduct}$ applied to $Y$ and $Z$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{binaryFan}$ applied to $Y$ and $Z$.

CategoryTheory.equivToOverUnitdefMathlib.CategoryTheory.LocallyCartesianClosed.Over, function or constant

Wording

the slice category over the terminal unit object of C (from the docstring)

English

Let $C$ be a set. Then the slice category over the terminal unit object of $C$ is an equivalence of $\operatorname{Over}$ applied to the tensor unity in the monoidal structure of $C$ and $C$.

CategoryTheory.forgetAdjToOverdefMathlib.CategoryTheory.LocallyCartesianClosed.Over, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{forgetAdjToOver}$ applied to $X$ is an adjunction of $\operatorname{forget}$ applied to $X$ and $\operatorname{toOver}$ applied to $X$.

CategoryTheory.toOverdefMathlib.CategoryTheory.LocallyCartesianClosed.Over, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{toOver}$ applied to $X$ is a functor of $C$ and $\operatorname{Over}$ applied to $X$.

CategoryTheory.toOverIsoToOverUnitdefMathlib.CategoryTheory.LocallyCartesianClosed.Over, function or constant

Wording

no wording

English

$\operatorname{toOverIsoToOverUnit}$ is an isomorphism of $\operatorname{toOver}$ applied to the tensor unity in the monoidal structure of $C$ and $\operatorname{toOverUnit}$ applied to $C$ defined as $\operatorname{rightAdjointUniq}$ applied to $\operatorname{forgetAdjToOver}$ applied to the tensor unity in the monoidal structure of $C$ and the adjunction of the slice category over the terminal unit object of $C$.

CategoryTheory.toOverIteratedSliceForwardIsoPullbackdefMathlib.CategoryTheory.LocallyCartesianClosed.Over, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $Y$ and $X$. Then $\operatorname{toOverIteratedSliceForwardIsoPullback}$ applied to $f$ is an isomorphism of the composition of $\operatorname{toOver}$ applied to $\operatorname{mk}$ applied to $f$ and $\operatorname{iteratedSliceForward}$ applied to $\operatorname{mk}$ applied to $f$ and the pullback of $f$.

CategoryTheory.toOverPullbackIsoToOverdefMathlib.CategoryTheory.LocallyCartesianClosed.Over, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $Y$ and $X$. Then $\operatorname{toOverPullbackIsoToOver}$ applied to $f$ is an isomorphism of the composition of $\operatorname{toOver}$ applied to $X$ and the pullback of $f$ and $\operatorname{toOver}$ applied to $Y$ defined as $\operatorname{conjugateIsoEquiv}$ applied to the composition of the map pullback adjoint of $f$ and $\operatorname{forgetAdjToOver}$ applied to $X$, $\operatorname{forgetAdjToOver}$ applied to $Y$ and $\operatorname{mapForget}$ applied to $f$.

CategoryTheory.toOverUnitdefMathlib.CategoryTheory.LocallyCartesianClosed.Over, function or constant

Wording

no wording

English

Let $C$ be a set. Then $\operatorname{toOverUnit}$ applied to $C$ is a functor of $C$ and $\operatorname{Over}$ applied to the tensor unity in the monoidal structure of $C$.

CategoryTheory.toOverUnitPullbackdefMathlib.CategoryTheory.LocallyCartesianClosed.Over, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{toOverUnitPullback}$ applied to $X$ is an isomorphism of the composition of $\operatorname{toOverUnit}$ applied to $C$ and the pullback of the unit of $X$ and $\operatorname{toOver}$ applied to $X$.

Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

CategoryTheory.Over.sectionsdefMathlib.CategoryTheory.LocallyCartesianClosed.Sections, function or constant

Wording

the section of I (from the name)

English

Let $I$ be an element of $C$. Then the section of $I$ is a functor of $\operatorname{Over}$ applied to $I$ and $C$.

CategoryTheory.Over.sectionsCurrydefMathlib.CategoryTheory.LocallyCartesianClosed.Sections, function or constant

Wording

the currying operation of u (from the docstring)

English

Let $u$ be a homomorphism of the action of $\operatorname{toOver}$ applied to $I$ and $A$ and $X$. Then the currying operation of $u$ is a homomorphism of $A$ and the action of the section of $I$ and $X$.

CategoryTheory.Over.sectionsUncurrydefMathlib.CategoryTheory.LocallyCartesianClosed.Sections, function or constant

Wording

the uncurrying operation of v (from the docstring)

English

Let $v$ be a homomorphism of $A$ and the action of the section of $I$ and $X$. Then the uncurrying operation of $v$ is a homomorphism of the action of $\operatorname{toOver}$ applied to $I$ and $A$ and $X$.

CategoryTheory.Over.toOverSectionsAdjdefMathlib.CategoryTheory.LocallyCartesianClosed.Sections, function or constant

Wording

no wording

English

Let $I$ be an element of $C$. Then $\operatorname{toOverSectionsAdj}$ applied to $I$ is an adjunction of $\operatorname{toOver}$ applied to $I$ and the section of $I$ defined as $\operatorname{mkOfHomEquiv}$ applied to $\operatorname{coreHomEquivToOverSections}$ applied to $I$.

CategoryTheory.curryRightUnitorHomdefMathlib.CategoryTheory.LocallyCartesianClosed.Sections, function or constant

Wording

the curry right unitor homomorphism of I (from the name)

English

Let $I$ be an element of $C$. Then the curry right unitor homomorphism of $I$ is a homomorphism of the tensor unity in the monoidal structure of $C$ and the action of $\operatorname{ihom}$ applied to $I$ and $I$ defined as the curry of the homomorphism of the right unitor of $I$.

Mathlib.CategoryTheory.LocallyDirected

CategoryTheory.Functor.IsLocallyDirectedclassMathlib.CategoryTheory.LocallyDirected, predicate

Wording

F is locally directed (from the name)

English

generation took over the time limit

Mathlib.CategoryTheory.MarkovCategory.Basic

CategoryTheory.MarkovCategoryclassMathlib.CategoryTheory.MarkovCategory.Basic, predicate

Wording

C is a Markov category (from the name)

English

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

CategoryTheory.MarkovCategory.isTerminalUnitdefMathlib.CategoryTheory.MarkovCategory.Basic, function or constant

Wording

the monoidal unit (from the docstring)

English

The monoidal unit is an element of $\operatorname{IsTerminal}$ applied to the tensor unity in the monoidal structure of $C$ defined as $\operatorname{ofUniqueHom}$ applied to the function that maps $Y$ to the counit morphism and $\mathrm{CategoryTheory\_\_MarkovCategory\_\_eq\_discard}$.

Mathlib.CategoryTheory.MarkovCategory.Positive

CategoryTheory.PositiveCategoryclassMathlib.CategoryTheory.MarkovCategory.Positive, predicate

Wording

C is a positive category (from the name)

English

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

Mathlib.CategoryTheory.Monad.Adjunction

CategoryTheory.Adjunction.adjToComonadIsodefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the adjoint to comonad isomorphism of G (from the name)

English

Let $G$ be a comonad of $C$. Then the adjoint to comonad isomorphism of $G$ is an isomorphism of the comonad of the adjoint of $G$ and $G$.

CategoryTheory.Adjunction.adjToMonadIsodefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the adjoint to monad isomorphism of T (from the name)

English

Let $T$ be a monad of $C$. Then the adjoint to monad isomorphism of $T$ is an isomorphism of the monad of the adjoint of $T$ and $T$.

CategoryTheory.Adjunction.counitAsIsoOfIsodefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the counit as isomorphism of adj and j (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $L$ and $R$. Let $j$ be an isomorphism of the composition of $R$ and $L$ and the identity of $D$. Then the counit as isomorphism of $\mathrm{adj}$ and $j$ is an isomorphism of the composition of $R$ and $L$ and the identity of $D$.

CategoryTheory.Adjunction.fullyFaithfulLOfCompIsoIddefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

no wording

English

Let $\mathrm{adj}$ be an adjunction of $L$ and $R$. Let $i$ be an isomorphism of the composition of $L$ and $R$ and the identity of $C$. Then $\operatorname{fullyFaithfulLOfCompIsoId}$ applied to $\mathrm{adj}$ and $i$ is an element of $\operatorname{FullyFaithful}$ applied to $L$ defined as $\operatorname{fullyFaithfulLOfIsIsoUnit}$ applied to $\mathrm{adj}$.

CategoryTheory.Adjunction.fullyFaithfulROfCompIsoIddefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

no wording

English

Let $\mathrm{adj}$ be an adjunction of $L$ and $R$. Let $j$ be an isomorphism of the composition of $R$ and $L$ and the identity of $D$. Then $\operatorname{fullyFaithfulROfCompIsoId}$ applied to $\mathrm{adj}$ and $j$ is an element of $\operatorname{FullyFaithful}$ applied to $R$ defined as $\operatorname{fullyFaithfulROfIsIsoCounit}$ applied to $\mathrm{adj}$.

CategoryTheory.Adjunction.toComonaddefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the comonad of h (from the name)

English

Let $h$ be an adjunction of $L$ and $R$. Then the comonad of $h$ is a comonad of $D$.

CategoryTheory.Adjunction.toMonaddefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the monad of h (from the name)

English

Let $h$ be an adjunction of $L$ and $R$. Then the monad of $h$ is a monad of $C$.

CategoryTheory.Adjunction.unitAsIsoOfIsodefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the unit as isomorphism of adj and i (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $L$ and $R$. Let $i$ be an isomorphism of the composition of $L$ and $R$ and the identity of $C$. Then the unit as isomorphism of $\mathrm{adj}$ and $i$ is an isomorphism of the identity of $C$ and the composition of $L$ and $R$.

CategoryTheory.Comonad.comparisondefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the comparison of h (from the name)

English

Let $h$ be an adjunction of $L$ and $R$. Then the comparison of $h$ is a functor of $C$ and the set of coalgebras of the comonad of $h$.

CategoryTheory.Comonad.comparisonForgetdefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

no wording

English

Let $h$ be an adjunction of $L$ and $R$. Then $\operatorname{comparisonForget}$ applied to $h$ is an isomorphism of the composition of the comparison of $h$ and $\operatorname{forget}$ applied to the comonad of $h$ and $L$.

CategoryTheory.ComonadicLeftAdjointclassMathlib.CategoryTheory.Monad.Adjunction, predicate

Wording

L is a comonadic left adjoint (from the name)

English

Let $L$ be a functor of $C$ and $D$. Then we can say that $L$ is a comonadic left adjoint.

CategoryTheory.ComonadicLeftAdjoint.RdefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Then $\operatorname{R}$ applied to $L$ is a functor of $D$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.ComonadicLeftAdjoint.adjdefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the left adjoint (from the docstring)

English

The left adjoint is an adjunction of $L$ and $\operatorname{R}$ applied to $L$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Monad.comparisondefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the comparison of h (from the name)

English

Let $h$ be an adjunction of $L$ and $R$. Then the comparison of $h$ is a functor of $D$ and the set of algebras of the monad of $h$.

CategoryTheory.Monad.comparisonForgetdefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

no wording

English

CategoryTheory.MonadicRightAdjointclassMathlib.CategoryTheory.Monad.Adjunction, predicate

Wording

R is a monadic right adjoint (from the name)

English

Let $R$ be a functor of $D$ and $C$. Then we can say that $R$ is a monadic right adjoint.

CategoryTheory.MonadicRightAdjoint.LdefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

no wording

English

Let $R$ be a functor of $D$ and $C$. Then $\operatorname{L}$ applied to $R$ is a functor of $C$ and $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.MonadicRightAdjoint.adjdefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the right adjoint (from the docstring)

English

The right adjoint is an adjunction of $\operatorname{L}$ applied to $R$ and $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.comonadicAdjunctiondefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the adjunction of L (from the docstring)

English

Let $L$ be a functor of $C$ and $D$. Then the adjunction of $L$ is an adjunction of $L$ and the comonadic right adjoint of $L$ defined as the left adjoint.

CategoryTheory.comonadicRightAdjointdefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the comonadic right adjoint of L (from the name)

English

Let $L$ be a functor of $C$ and $D$. Then the comonadic right adjoint of $L$ is a functor of $D$ and $C$ defined as $\operatorname{R}$ applied to $L$.

CategoryTheory.monadicAdjunctiondefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the adjunction of R (from the docstring)

English

Let $R$ be a functor of $D$ and $C$. Then the adjunction of $R$ is an adjunction of the monadic left adjoint of $R$ and $R$ defined as the right adjoint.

CategoryTheory.monadicLeftAdjointdefMathlib.CategoryTheory.Monad.Adjunction, function or constant

Wording

the monadic left adjoint of R (from the name)

English

Let $R$ be a functor of $D$ and $C$. Then the monadic left adjoint of $R$ is a functor of $C$ and $D$ defined as $\operatorname{L}$ applied to $R$.

Mathlib.CategoryTheory.Monad.Algebra

CategoryTheory.Comonad.CoalgebrastructureMathlib.CategoryTheory.Monad.Algebra, type

Wording

coalgebra of T (from the name)

English

Let $T$ be a comonad of $C$. Then the coalgebras of $T$ are a basic type.

CategoryTheory.Comonad.Coalgebra.AdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

no wording

English

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

CategoryTheory.Comonad.Coalgebra.HomstructureMathlib.CategoryTheory.Monad.Algebra, type

Wording

homomorphism of A and B (from the name)

English

Let $A$ and $B$ be coalgebras of $T$. Then the homomorphisms of $A$ and $B$ are a basic type.

CategoryTheory.Comonad.Coalgebra.Hom.compdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a homomorphism of $R$ and $Q$. Let $f$ be a homomorphism of $Q$ and $P$. Then the composition of $g$ and $f$ is a homomorphism of $R$ and $P$.

CategoryTheory.Comonad.Coalgebra.Hom.fdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{A}$ applied to $A$ and $\operatorname{A}$ applied to $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Comonad.Coalgebra.Hom.iddefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the identity of A (from the name)

English

Let $A$ be a coalgebra of $T$. Then the identity of $A$ is a homomorphism of $A$ and $A$.

CategoryTheory.Comonad.Coalgebra.adefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a coalgebra of $T$. Then $\operatorname{a}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{A}$ applied to $\mathrm{self}$ and the action of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{A}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Comonad.Coalgebra.isoMkdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the isomorphism of h and w (from the name)

English

Let $h$ be an isomorphism of $\operatorname{A}$ applied to $A$ and $\operatorname{A}$ applied to $B$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $\operatorname{a}$ applied to $A$ and the map of $\operatorname{toFunctor}$ applied to $T$ and the homomorphism of $h$ is equal to the composition of the homomorphism of $h$ and $\operatorname{a}$ applied to $B$ and $\mathrm{CategoryTheory\_\_Comonad\_\_Coalgebra\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $h$ and $w$ is an isomorphism of $A$ and $B$.

CategoryTheory.Comonad.adjdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the adjoint of T (from the name)

English

Let $T$ be a comonad of $C$. Then the adjoint of $T$ is an adjunction of $\operatorname{forget}$ applied to $T$ and the cofree of $T$.

CategoryTheory.Comonad.cofreedefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the cofree of T (from the name)

English

Let $T$ be a comonad of $C$. Then the cofree of $T$ is a functor of $C$ and the set of coalgebras of $T$.

CategoryTheory.Comonad.forgetdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

no wording

English

Let $T$ be a comonad of $C$. Then $\operatorname{forget}$ applied to $T$ is a functor of the set of coalgebras of $T$ and $C$.

CategoryTheory.Monad.AlgebrastructureMathlib.CategoryTheory.Monad.Algebra, type

Wording

algebra of T (from the name)

English

Let $T$ be a monad of $C$. Then the algebras of $T$ are a basic type.

CategoryTheory.Monad.Algebra.AdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an algebra of $T$. Then $\operatorname{A}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Monad.Algebra.HomstructureMathlib.CategoryTheory.Monad.Algebra, type

Wording

homomorphism of A and B (from the name)

English

Let $A$ and $B$ be algebras of $T$. Then the homomorphisms of $A$ and $B$ are a basic type.

CategoryTheory.Monad.Algebra.Hom.compdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a homomorphism of $P$ and $Q$. Let $g$ be a homomorphism of $Q$ and $R$. Then the composition of $f$ and $g$ is a homomorphism of $P$ and $R$.

CategoryTheory.Monad.Algebra.Hom.fdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

no wording

English

CategoryTheory.Monad.Algebra.Hom.iddefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the identity of A (from the name)

English

Let $A$ be an algebra of $T$. Then the identity of $A$ is a homomorphism of $A$ and $A$.

CategoryTheory.Monad.Algebra.adefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an algebra of $T$. Then $\operatorname{a}$ applied to $\mathrm{self}$ is a homomorphism of the action of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{A}$ applied to $\mathrm{self}$ and $\operatorname{A}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Monad.Algebra.isoMkdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the isomorphism of h and w (from the name)

English

Let $h$ be an isomorphism of $\operatorname{A}$ applied to $A$ and $\operatorname{A}$ applied to $B$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $\operatorname{toFunctor}$ applied to $T$ and the homomorphism of $h$ and $\operatorname{a}$ applied to $B$ is equal to the composition of $\operatorname{a}$ applied to $A$ and the homomorphism of $h$ and $\mathrm{CategoryTheory\_\_Monad\_\_Algebra\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $h$ and $w$ is an isomorphism of $A$ and $B$.

CategoryTheory.Monad.adjdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the adjoint of T (from the name)

English

Let $T$ be a monad of $C$. Then the adjoint of $T$ is an adjunction of the free of $T$ and $\operatorname{forget}$ applied to $T$.

CategoryTheory.Monad.algebraEquivOfIsoMonadsdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the algebra equivalence of h (from the name)

English

Let $h$ be an isomorphism of $x_{1}$ and $x_{2}$. Then the algebra equivalence of $h$ is an equivalence of the set of algebras of $x_{1}$ and the set of algebras of $x_{2}$.

CategoryTheory.Monad.algebraFunctorOfMonadHomdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the algebra functor of h (from the name)

English

Let $h$ be a homomorphism of $x_{2}$ and $x_{1}$. Then the algebra functor of $h$ is a functor of the set of algebras of $x_{1}$ and the set of algebras of $x_{2}$.

CategoryTheory.Monad.algebraFunctorOfMonadHomCompdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the algebra functor of f and g (from the name)

English

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the algebra functor of $f$ and $g$ is an isomorphism of the algebra functor of the composition of $f$ and $g$ and the composition of the algebra functor of $g$ and the algebra functor of $f$.

CategoryTheory.Monad.algebraFunctorOfMonadHomEqdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the algebra functor of h (from the name)

English

Assume that $\EqtMACRoH {f}{g}$. Then the algebra functor of $h$ is an isomorphism of the algebra functor of $f$ and the algebra functor of $g$.

CategoryTheory.Monad.algebraFunctorOfMonadHomIddefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the algebra functor (from the name)

English

The algebra functor is an isomorphism of the algebra functor of the identity morphism of $x_{1}$ and the identity of the set of algebras of $x_{1}$.

CategoryTheory.Monad.forgetdefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

no wording

English

Let $T$ be a monad of $C$. Then $\operatorname{forget}$ applied to $T$ is a functor of the set of algebras of $T$ and $C$.

CategoryTheory.Monad.freedefMathlib.CategoryTheory.Monad.Algebra, function or constant

Wording

the free of T (from the name)

English

Let $T$ be a monad of $C$. Then the free of $T$ is a functor of $C$ and the set of algebras of $T$.

Mathlib.CategoryTheory.Monad.Basic

CategoryTheory.ComonadstructureMathlib.CategoryTheory.Monad.Basic, type

Wording

comonad of C (from the name)

English

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

CategoryTheory.Comonad.iddefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

the identity comonad of C (from the docstring)

English

Let $C$ be a set. Then the identity comonad of $C$ is a comonad of $C$.

CategoryTheory.Comonad.transportdefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

the transport of T and i (from the name)

English

Let $T$ be a comonad of $C$. Let $i$ be an isomorphism of $\operatorname{toFunctor}$ applied to $T$ and $F$. Then the transport of $T$ and $i$ is a comonad of $C$.

CategoryTheory.Comonad.δdefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a comonad of $C$. Then $\mathrm{CategoryTheory\_\_Comonad\_\_\_u3b4\_}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{toFunctor}$ applied to $\mathrm{self}$ and the composition of $\operatorname{toFunctor}$ applied to $\mathrm{self}$ and $\operatorname{toFunctor}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.Comonad.εdefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a comonad of $C$. Then $\mathrm{CategoryTheory\_\_Comonad\_\_\_u3b5\_}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{toFunctor}$ applied to $\mathrm{self}$ and the identity of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.ComonadHomstructureMathlib.CategoryTheory.Monad.Basic, type

Wording

comonad homomorphism of M and N (from the name)

English

Let $M$ and $N$ be comonads of $C$. Then the comonad homomorphisms of $M$ and $N$ are a basic type.

CategoryTheory.ComonadIso.mkdefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

no wording

English

Let $f$ be an isomorphism of $\operatorname{toFunctor}$ applied to $M$ and $\operatorname{toFunctor}$ applied to $N$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $X_{1}$ of $C$, the composition of the component of the homomorphism of $f$ and $X_{1}$ and the component of $\mathrm{CategoryTheory\_\_Comonad\_\_\_u3b5\_}$ applied to $N$ and $X_{1}$ is equal to the component of $\mathrm{CategoryTheory\_\_Comonad\_\_\_u3b5\_}$ applied to $M$ and $X_{1}$ and $\mathrm{CategoryTheory\_\_ComonadIso\_\_mk\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $X$ of $C$, the composition of the component of the homomorphism of $f$ and $X$ and the component of $\mathrm{CategoryTheory\_\_Comonad\_\_\_u3b4\_}$ applied to $N$ and $X$ is equal to the composition of the component of $\mathrm{CategoryTheory\_\_Comonad\_\_\_u3b4\_}$ applied to $M$ and $X$ and the composition of the component of the homomorphism of $f$ and the action of $\operatorname{toFunctor}$ applied to $M$ and $X$ and the map of $\operatorname{toFunctor}$ applied to $N$ and the component of the homomorphism of $f$ and $X$ and $\mathrm{CategoryTheory\_\_ComonadIso\_\_mk\_\_\_auto\_3}$. Then $\operatorname{mk}$ applied to $f$, $h$ and $h_{1}$ is an isomorphism of $M$ and $N$.

CategoryTheory.ComonadIso.toNatIsodefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

the natural isomorphism of h (from the name)

English

Let $h$ be an isomorphism of $M$ and $N$. Then the natural isomorphism of $h$ is an isomorphism of $\operatorname{toFunctor}$ applied to $M$ and $\operatorname{toFunctor}$ applied to $N$ defined as the map isomorphism of the comonad to functor of $C$ and $h$.

CategoryTheory.MonadstructureMathlib.CategoryTheory.Monad.Basic, type

Wording

monad of C (from the name)

English

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

CategoryTheory.Monad.iddefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

the identity monad of C (from the docstring)

English

Let $C$ be a set. Then the identity monad of $C$ is a monad of $C$.

CategoryTheory.Monad.transportdefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

the transport of T and i (from the name)

English

Let $T$ be a monad of $C$. Let $i$ be an isomorphism of $\operatorname{toFunctor}$ applied to $T$ and $F$. Then the transport of $T$ and $i$ is a monad of $C$.

CategoryTheory.Monad.ηdefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a monad of $C$. Then $\mathrm{CategoryTheory\_\_Monad\_\_\_u3b7\_}$ applied to $\mathrm{self}$ is a homomorphism of the identity of $C$ and $\operatorname{toFunctor}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Monad.μdefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a monad of $C$. Then $\mathrm{CategoryTheory\_\_Monad\_\_\_u3bc\_}$ applied to $\mathrm{self}$ is a homomorphism of the composition of $\operatorname{toFunctor}$ applied to $\mathrm{self}$ and $\operatorname{toFunctor}$ applied to $\mathrm{self}$ and $\operatorname{toFunctor}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.MonadHomstructureMathlib.CategoryTheory.Monad.Basic, type

Wording

monad homomorphism of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be monads of $C$. Then the monad homomorphisms of $x_{1}$ and $x_{2}$ are a basic type.

CategoryTheory.MonadIso.mkdefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

no wording

English

Let $f$ be an isomorphism of $\operatorname{toFunctor}$ applied to $M$ and $\operatorname{toFunctor}$ applied to $N$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $X_{1}$ of $C$, the composition of the component of $\mathrm{CategoryTheory\_\_Monad\_\_\_u3b7\_}$ applied to $M$ and $X_{1}$ and the component of the homomorphism of $f$ and $X_{1}$ is equal to the component of $\mathrm{CategoryTheory\_\_Monad\_\_\_u3b7\_}$ applied to $N$ and $X_{1}$ and $\mathrm{CategoryTheory\_\_MonadIso\_\_mk\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $X$ of $C$, the composition of the component of $\mathrm{CategoryTheory\_\_Monad\_\_\_u3bc\_}$ applied to $M$ and $X$ and the component of the homomorphism of $f$ and $X$ is equal to the composition of the composition of the map of $\operatorname{toFunctor}$ applied to $M$ and the component of the homomorphism of $f$ and $X$ and the component of the homomorphism of $f$ and the action of $\operatorname{toFunctor}$ applied to $N$ and $X$ and the component of $\mathrm{CategoryTheory\_\_Monad\_\_\_u3bc\_}$ applied to $N$ and $X$ and $\mathrm{CategoryTheory\_\_MonadIso\_\_mk\_\_\_auto\_3}$. Then $\operatorname{mk}$ applied to $f$, $h$ and $h_{1}$ is an isomorphism of $M$ and $N$.

CategoryTheory.MonadIso.toNatIsodefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

the natural isomorphism of h (from the name)

English

CategoryTheory.comonadToFunctordefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

the comonad to functor of C (from the name)

English

Let $C$ be a set. Then the comonad to functor of $C$ is a functor of the set of comonads of $C$ and the set of functors of $C$ and $C$.

CategoryTheory.monadToFunctordefMathlib.CategoryTheory.Monad.Basic, function or constant

Wording

the monad to functor of C (from the name)

English

Let $C$ be a set. Then the monad to functor of $C$ is a functor of the set of monads of $C$ and the set of functors of $C$ and $C$.

Mathlib.CategoryTheory.Monad.Coequalizer

CategoryTheory.Monad.FreeCoequalizer.bottomMapdefMathlib.CategoryTheory.Monad.Coequalizer, function or constant

Wording

the bottom map of X (from the name)

English

Let $X$ be an algebra of $T$. Then the bottom map of $X$ is a homomorphism of the action of the free of $T$ and the action of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{A}$ applied to $X$ and the action of the free of $T$ and $\operatorname{A}$ applied to $X$.

CategoryTheory.Monad.FreeCoequalizer.topMapdefMathlib.CategoryTheory.Monad.Coequalizer, function or constant

Wording

the top map of X (from the name)

English

Let $X$ be an algebra of $T$. Then the top map of $X$ is a homomorphism of the action of the free of $T$ and the action of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{A}$ applied to $X$ and the action of the free of $T$ and $\operatorname{A}$ applied to $X$ defined as the map of the free of $T$ and $\operatorname{a}$ applied to $X$.

CategoryTheory.Monad.FreeCoequalizer.πdefMathlib.CategoryTheory.Monad.Coequalizer, function or constant

Wording

the projection of X (from the name)

English

Let $X$ be an algebra of $T$. Then the projection of $X$ is a homomorphism of the action of the free of $T$ and $\operatorname{A}$ applied to $X$ and $X$.

CategoryTheory.Monad.beckAlgebraCoequalizerdefMathlib.CategoryTheory.Monad.Coequalizer, function or constant

Wording

the Beck algebra coequalizer of X (from the name)

English

Let $X$ be an algebra of $T$. Then the Beck algebra coequalizer of $X$ is an element of $\operatorname{IsColimit}$ applied to the Beck algebra cofork of $X$.

CategoryTheory.Monad.beckAlgebraCoforkdefMathlib.CategoryTheory.Monad.Coequalizer, function or constant

Wording

the Beck algebra cofork of X (from the name)

English

Let $X$ be an algebra of $T$. Then the Beck algebra cofork of $X$ is a cofork of the top map of $X$ and the bottom map of $X$ defined as the projection of the projection of $X$ and $\operatorname{condition}$ applied to $X$.

CategoryTheory.Monad.beckCoequalizerdefMathlib.CategoryTheory.Monad.Coequalizer, function or constant

Wording

the Beck cofork of X (from the docstring)

English

Let $X$ be an algebra of $T$. Then the Beck cofork of $X$ is an element of $\operatorname{IsColimit}$ applied to the Beck cofork of $X$ defined as the cofork induced by a split coequalizer of the Beck cofork of $X$.

CategoryTheory.Monad.beckCoforkdefMathlib.CategoryTheory.Monad.Coequalizer, function or constant

Wording

the Beck cofork of X (from the name)

English

Let $X$ be an algebra of $T$. Then the Beck cofork of $X$ is a cofork of the map of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{a}$ applied to $X$ and the component of $\mathrm{CategoryTheory\_\_Monad\_\_\_u3bc\_}$ applied to $T$ and $\operatorname{A}$ applied to $X$ defined as $\operatorname{asCofork}$ applied to the Beck cofork of $X$.

CategoryTheory.Monad.beckSplitCoequalizerdefMathlib.CategoryTheory.Monad.Coequalizer, function or constant

Wording

the Beck cofork of X (from the docstring)

English

Let $X$ be an algebra of $T$. Then the Beck cofork of $X$ is an element of $\operatorname{IsSplitCoequalizer}$ applied to the map of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{a}$ applied to $X$, the component of $\mathrm{CategoryTheory\_\_Monad\_\_\_u3bc\_}$ applied to $T$ and $\operatorname{A}$ applied to $X$ and $\operatorname{a}$ applied to $X$.

Mathlib.CategoryTheory.Monad.Comonadicity

CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunctiondefMathlib.CategoryTheory.Monad.Comonadicity, function or constant

Wording

the comparison adjunction of adj (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the comparison adjunction of $\mathrm{adj}$ is an adjunction of the comparison of $\mathrm{adj}$ and the right adjoint comparison of $\mathrm{adj}$.

CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquivdefMathlib.CategoryTheory.Monad.Comonadicity, function or constant

Wording

the comparison right adjoint homomorphism equivalence of A and B (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $A$ be a coalgebra of the comonad of $\mathrm{adj}$. Let $B$ be an element of $C$. Then the comparison right adjoint homomorphism equivalence of $A$ and $B$ is an equivalence from the set of homomorphisms of the action of the comparison of $\mathrm{adj}$ and $B$ and $A$ to the set of homomorphisms of $B$ and the comparison right adjoint object of $\mathrm{adj}$ and $A$.

CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObjdefMathlib.CategoryTheory.Monad.Comonadicity, function or constant

Wording

the comparison right adjoint object of adj and A (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $A$ be a coalgebra of the comonad of $\mathrm{adj}$. Then the comparison right adjoint object of $\mathrm{adj}$ and $A$ is an element of $C$ defined as the equalizer of the map of $G$ and $\operatorname{a}$ applied to $A$ and the component of the unit of $\mathrm{adj}$ and $\operatorname{proj0}$ applied to $G$ and $\operatorname{A}$ applied to $A$.

CategoryTheory.Comonad.ComonadicityInternal.counitForkdefMathlib.CategoryTheory.Monad.Comonadicity, function or constant

Wording

the counit fork of A (from the name)

English

Let $A$ be a coalgebra of the comonad of $\mathrm{adj}$. Then the counit fork of $A$ is a fork of the map of $F$ and the map of $G$ and $\operatorname{a}$ applied to $A$ and the map of $F$ and the component of the unit of $\mathrm{adj}$ and the action of $G$ and $\operatorname{A}$ applied to $A$.

CategoryTheory.Comonad.ComonadicityInternal.counitLimitOfPreservesEqualizerdefMathlib.CategoryTheory.Monad.Comonadicity, function or constant

Wording

the counit fork of A (from the docstring)

English

Let $A$ be a coalgebra of the comonad of $\mathrm{adj}$. Then the counit fork of $A$ is an element of $\operatorname{IsLimit}$ applied to the counit fork of $A$ defined as $\operatorname{isLimitOfHasEqualizerOfPreservesLimit}$ applied to $F$, the map of $G$ and $\operatorname{a}$ applied to $A$ and the component of the unit of $\mathrm{adj}$ and the action of $G$ and $\operatorname{A}$ applied to $A$.

CategoryTheory.Comonad.ComonadicityInternal.rightAdjointComparisondefMathlib.CategoryTheory.Monad.Comonadicity, function or constant

Wording

the right adjoint comparison of adj (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the right adjoint comparison of $\mathrm{adj}$ is a functor of the set of coalgebras of the comonad of $\mathrm{adj}$ and $C$.

CategoryTheory.Comonad.ComonadicityInternal.unitEqualizerOfCoreflectsEqualizerdefMathlib.CategoryTheory.Monad.Comonadicity, function or constant

Wording

the unit fork of adj and B (from the docstring)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $B$ be an element of $C$. Then the unit fork of $\mathrm{adj}$ and $B$ is an element of $\operatorname{IsLimit}$ applied to the unit fork of $\mathrm{adj}$ and $B$.

CategoryTheory.Comonad.ComonadicityInternal.unitForkdefMathlib.CategoryTheory.Monad.Comonadicity, function or constant

Wording

the unit fork of adj and B (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $B$ be an element of $C$. Then the unit fork of $\mathrm{adj}$ and $B$ is a fork of the map of $G$ and the map of $F$ and the component of the unit of $\mathrm{adj}$ and $B$ and the component of the unit of $\mathrm{adj}$ and the action of $G$ and the action of $F$ and $B$.

CategoryTheory.Comonad.CreatesLimitOfIsCosplitPairclassMathlib.CategoryTheory.Monad.Comonadicity, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{CreatesLimitOfIsCosplitPair}$ holds for $F$.

CategoryTheory.Comonad.HasEqualizerOfIsCosplitPairclassMathlib.CategoryTheory.Monad.Comonadicity, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{HasEqualizerOfIsCosplitPair}$ holds for $F$.

CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePairclassMathlib.CategoryTheory.Monad.Comonadicity, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{PreservesLimitOfIsCoreflexivePair}$ holds for $F$.

CategoryTheory.Comonad.PreservesLimitOfIsCosplitPairclassMathlib.CategoryTheory.Monad.Comonadicity, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{PreservesLimitOfIsCosplitPair}$ holds for $F$.

CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPairclassMathlib.CategoryTheory.Monad.Comonadicity, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{ReflectsLimitOfIsCosplitPair}$ holds for $F$.

Mathlib.CategoryTheory.Monad.Equalizer

CategoryTheory.Comonad.CofreeEqualizer.bottomMapdefMathlib.CategoryTheory.Monad.Equalizer, function or constant

Wording

the bottom map of X (from the name)

English

Let $X$ be a coalgebra of $T$. Then the bottom map of $X$ is a homomorphism of the action of the cofree of $T$ and $\operatorname{A}$ applied to $X$ and the action of the cofree of $T$ and the action of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{A}$ applied to $X$.

CategoryTheory.Comonad.CofreeEqualizer.topMapdefMathlib.CategoryTheory.Monad.Equalizer, function or constant

Wording

the top map of X (from the name)

English

Let $X$ be a coalgebra of $T$. Then the top map of $X$ is a homomorphism of the action of the cofree of $T$ and $\operatorname{A}$ applied to $X$ and the action of the cofree of $T$ and the action of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{A}$ applied to $X$ defined as the map of the cofree of $T$ and $\operatorname{a}$ applied to $X$.

CategoryTheory.Comonad.CofreeEqualizer.ιdefMathlib.CategoryTheory.Monad.Equalizer, function or constant

Wording

the inclusion of X (from the name)

English

Let $X$ be a coalgebra of $T$. Then the inclusion of $X$ is a homomorphism of $X$ and the action of the cofree of $T$ and $\operatorname{A}$ applied to $X$.

CategoryTheory.Comonad.beckCoalgebraEqualizerdefMathlib.CategoryTheory.Monad.Equalizer, function or constant

Wording

the Beck coalgebra equalizer of X (from the name)

English

Let $X$ be a coalgebra of $T$. Then the Beck coalgebra equalizer of $X$ is an element of $\operatorname{IsLimit}$ applied to the Beck coalgebra fork of $X$.

CategoryTheory.Comonad.beckCoalgebraForkdefMathlib.CategoryTheory.Monad.Equalizer, function or constant

Wording

the Beck coalgebra fork of X (from the name)

English

Let $X$ be a coalgebra of $T$. Then the Beck coalgebra fork of $X$ is a fork of the top map of $X$ and the bottom map of $X$ defined as the inclusion of the inclusion of $X$ and $\operatorname{condition}$ applied to $X$.

CategoryTheory.Comonad.beckEqualizerdefMathlib.CategoryTheory.Monad.Equalizer, function or constant

Wording

the Beck fork of X (from the docstring)

English

Let $X$ be a coalgebra of $T$. Then the Beck fork of $X$ is an element of $\operatorname{IsLimit}$ applied to the Beck fork of $X$ defined as the fork induced by a split equalizer of the Beck fork of $X$.

CategoryTheory.Comonad.beckForkdefMathlib.CategoryTheory.Monad.Equalizer, function or constant

Wording

the Beck fork of X (from the name)

English

Let $X$ be a coalgebra of $T$. Then the Beck fork of $X$ is a fork of the map of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{a}$ applied to $X$ and the component of $\mathrm{CategoryTheory\_\_Comonad\_\_\_u3b4\_}$ applied to $T$ and $\operatorname{A}$ applied to $X$ defined as $\operatorname{asFork}$ applied to the Beck fork of $X$.

CategoryTheory.Comonad.beckSplitEqualizerdefMathlib.CategoryTheory.Monad.Equalizer, function or constant

Wording

the Beck fork of X (from the docstring)

English

Let $X$ be a coalgebra of $T$. Then the Beck fork of $X$ is an element of $\operatorname{IsSplitEqualizer}$ applied to the map of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{a}$ applied to $X$, the component of $\mathrm{CategoryTheory\_\_Comonad\_\_\_u3b4\_}$ applied to $T$ and $\operatorname{A}$ applied to $X$ and $\operatorname{a}$ applied to $X$.

Mathlib.CategoryTheory.Monad.EquivMon

CategoryTheory.Monad.monToMonaddefMathlib.CategoryTheory.Monad.EquivMon, function or constant

Wording

the monoid to monad of C (from the name)

English

Let $C$ be a set. Then the monoid to monad of $C$ is a functor of the set of monoids of the set of functors of $C$ and $C$ and the set of monads of $C$.

CategoryTheory.Monad.monadMonEquivdefMathlib.CategoryTheory.Monad.EquivMon, function or constant

Wording

the monad monoid equivalence of C (from the name)

English

Let $C$ be a set. Then the monad monoid equivalence of $C$ is an equivalence of the set of monads of $C$ and the set of monoids of the set of functors of $C$ and $C$.

CategoryTheory.Monad.monadToMondefMathlib.CategoryTheory.Monad.EquivMon, function or constant

Wording

the monad to monoid of C (from the name)

English

Let $C$ be a set. Then the monad to monoid of $C$ is a functor of the set of monads of $C$ and the set of monoids of the set of functors of $C$ and $C$.

CategoryTheory.Monad.ofMondefMathlib.CategoryTheory.Monad.EquivMon, function or constant

Wording

the monad of M (from the name)

English

Let $M$ be a monoid of the set of functors of $C$ and $C$. Then the monad of $M$ is a monad of $C$.

CategoryTheory.Monad.toMondefMathlib.CategoryTheory.Monad.EquivMon, function or constant

Wording

the monoid of M (from the name)

English

Let $M$ be a monad of $C$. Then the monoid of $M$ is a monoid of the set of functors of $C$ and $C$ defined as $\operatorname{mk}$ applied to $\operatorname{toFunctor}$ applied to $M$.

Mathlib.CategoryTheory.Monad.Kleisli

CategoryTheory.CokleislistructureMathlib.CategoryTheory.Monad.Kleisli, type

Wording

no wording

English

Let $U$ be a comonad of $C$. Then the elements of $\operatorname{Cokleisli}$ applied to $U$ are a basic type.

CategoryTheory.Cokleisli.Adjunction.adjdefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

the adjoint of T (from the name)

English

Let $T$ be a comonad of $C$. Then the adjoint of $T$ is an adjunction of $\operatorname{fromCokleisli}$ applied to $T$ and $\operatorname{toCokleisli}$ applied to $T$.

CategoryTheory.Cokleisli.Adjunction.fromCokleislidefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

no wording

English

Let $T$ be a comonad of $C$. Then $\operatorname{fromCokleisli}$ applied to $T$ is a functor of $\operatorname{Cokleisli}$ applied to $T$ and $C$.

CategoryTheory.Cokleisli.Adjunction.toCokleislidefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

no wording

English

Let $T$ be a comonad of $C$. Then $\operatorname{toCokleisli}$ applied to $T$ is a functor of $C$ and $\operatorname{Cokleisli}$ applied to $T$.

CategoryTheory.Cokleisli.Adjunction.toCokleisliCompFromCokleisliIsoSelfdefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

no wording

English

Let $T$ be a comonad of $C$. Then $\operatorname{toCokleisliCompFromCokleisliIsoSelf}$ applied to $T$ is an isomorphism of the composition of $\operatorname{toCokleisli}$ applied to $T$ and $\operatorname{fromCokleisli}$ applied to $T$ and $\operatorname{toFunctor}$ applied to $T$.

CategoryTheory.Cokleisli.HomstructureMathlib.CategoryTheory.Monad.Kleisli, type

Wording

homomorphism of c and #2 (from the name)

English

Let $c$ and $\mathrm{c'}$ be elements of $\operatorname{Cokleisli}$ applied to $U$. Then the homomorphisms of $c$ and $\mathrm{c'}$ are a basic type.

CategoryTheory.Cokleisli.Hom.ofdefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a homomorphism of $c$ and $\mathrm{c'}$. Then $\operatorname{of}$ applied to $\mathrm{self}$ is a homomorphism of the action of $\operatorname{toFunctor}$ applied to $U$ and $\operatorname{of}$ applied to $c$ and $\operatorname{of}$ applied to $\mathrm{c'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Cokleisli.ofdefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

no wording

English

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

CategoryTheory.KleislistructureMathlib.CategoryTheory.Monad.Kleisli, type

Wording

no wording

English

Let $T$ be a monad of $C$. Then the elements of $\operatorname{Kleisli}$ applied to $T$ are a basic type.

CategoryTheory.Kleisli.Adjunction.adjdefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

the adjoint of T (from the name)

English

Let $T$ be a monad of $C$. Then the adjoint of $T$ is an adjunction of $\operatorname{toKleisli}$ applied to $T$ and $\operatorname{fromKleisli}$ applied to $T$.

CategoryTheory.Kleisli.Adjunction.fromKleislidefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

no wording

English

Let $T$ be a monad of $C$. Then $\operatorname{fromKleisli}$ applied to $T$ is a functor of $\operatorname{Kleisli}$ applied to $T$ and $C$.

CategoryTheory.Kleisli.Adjunction.toKleislidefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

no wording

English

Let $T$ be a monad of $C$. Then $\operatorname{toKleisli}$ applied to $T$ is a functor of $C$ and $\operatorname{Kleisli}$ applied to $T$.

CategoryTheory.Kleisli.Adjunction.toKleisliCompFromKleisliIsoSelfdefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

no wording

English

Let $T$ be a monad of $C$. Then $\operatorname{toKleisliCompFromKleisliIsoSelf}$ applied to $T$ is an isomorphism of the composition of $\operatorname{toKleisli}$ applied to $T$ and $\operatorname{fromKleisli}$ applied to $T$ and $\operatorname{toFunctor}$ applied to $T$.

CategoryTheory.Kleisli.HomstructureMathlib.CategoryTheory.Monad.Kleisli, type

Wording

homomorphism of c and #2 (from the name)

English

Let $c$ and $\mathrm{c'}$ be elements of $\operatorname{Kleisli}$ applied to $T$. Then the homomorphisms of $c$ and $\mathrm{c'}$ are a basic type.

CategoryTheory.Kleisli.Hom.ofdefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a homomorphism of $c$ and $\mathrm{c'}$. Then $\operatorname{of}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{of}$ applied to $c$ and the action of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{of}$ applied to $\mathrm{c'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Kleisli.ofdefMathlib.CategoryTheory.Monad.Kleisli, function or constant

Wording

no wording

English

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

Mathlib.CategoryTheory.Monad.Limits

CategoryTheory.Comonad.ForgetCreatesColimits'.coconePointdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the cocone point of c and t (from the name)

English

Let $D$ be a functor of $J$ and the set of coalgebras of $T$. Let $c$ be a cocone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the cocone point of $c$ and $t$ is a coalgebra of $T$.

CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconedefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the lifted cocone of c and t (from the name)

English

CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimitdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

no wording

English

Let $D$ be a functor of $J$ and the set of coalgebras of $T$. Let $c$ be a cocone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{liftedCoconeIsColimit}$ applied to $D$, $c$ and $t$ is an element of $\operatorname{IsColimit}$ applied to the lifted cocone of $c$ and $t$.

CategoryTheory.Comonad.ForgetCreatesColimits'.newCoconedefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the new cocone of D and c (from the name)

English

Let $D$ be a functor of $J$ and the set of coalgebras of $T$. Let $c$ be a cocone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Then the new cocone of $D$ and $c$ is a cocone of the composition of $D$ and $\operatorname{forget}$ applied to $T$ defined as $\operatorname{mk}$ applied to the action of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{pt}$ applied to $c$ and the composition of $\mathrm{CategoryTheory\_\_Comonad\_\_ForgetCreatesColimits'\_\_\_u3b3\_}$ applied to $D$ and the composition of the right whisker of the inclusion of $c$ and $\operatorname{toFunctor}$ applied to $T$ and the homomorphism of the constant composition of $\operatorname{pt}$ applied to $c$ and $\operatorname{toFunctor}$ applied to $T$.

CategoryTheory.Comonad.ForgetCreatesColimits'.γdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

no wording

English

Let $D$ be a functor of $J$ and the set of coalgebras of $T$. Then $\mathrm{CategoryTheory\_\_Comonad\_\_ForgetCreatesColimits'\_\_\_u3b3\_}$ applied to $D$ is a homomorphism of the composition of $D$ and $\operatorname{forget}$ applied to $T$ and the composition of $D$ and the composition of $\operatorname{forget}$ applied to $T$ and $\operatorname{toFunctor}$ applied to $T$.

CategoryTheory.Comonad.ForgetCreatesLimits'.conePointdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the cone point of c and t (from the name)

English

Let $c$ be a cone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the cone point of $c$ and $t$ is a coalgebra of $T$.

CategoryTheory.Comonad.ForgetCreatesLimits'.lambdadefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the lambda of c and t (from the name)

English

Let $c$ be a cone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the lambda of $c$ and $t$ is a homomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to the map cone of $\operatorname{toFunctor}$ applied to $T$ and $c$ defined as the lift of $\operatorname{isLimitOfPreserves}$ applied to $\operatorname{toFunctor}$ applied to $T$ and $t$ and the new cone of $c$.

CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConedefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the lifted cone of c and t (from the name)

English

Let $c$ be a cone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the lifted cone of $c$ and $t$ is a cone of $D$.

CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimitdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

no wording

English

Let $c$ be a cone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{liftedConeIsLimit}$ applied to $c$ and $t$ is an element of $\operatorname{IsLimit}$ applied to the lifted cone of $c$ and $t$.

CategoryTheory.Comonad.ForgetCreatesLimits'.newConedefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the new cone of c (from the name)

English

Let $c$ be a cone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Then the new cone of $c$ is a cone of the composition of the composition of $D$ and $\operatorname{forget}$ applied to $T$ and $\operatorname{toFunctor}$ applied to $T$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and the composition of the projection of $c$ and $\mathrm{CategoryTheory\_\_Comonad\_\_ForgetCreatesLimits'\_\_\_u3b3\_}$.

CategoryTheory.Comonad.ForgetCreatesLimits'.γdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

no wording

English

$\mathrm{CategoryTheory\_\_Comonad\_\_ForgetCreatesLimits'\_\_\_u3b3\_}$ is a homomorphism of the composition of $D$ and $\operatorname{forget}$ applied to $T$ and the composition of the composition of $D$ and $\operatorname{forget}$ applied to $T$ and $\operatorname{toFunctor}$ applied to $T$.

CategoryTheory.Monad.ForgetCreatesColimits.coconePointdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the cocone point of c and t (from the name)

English

Let $c$ be a cocone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the cocone point of $c$ and $t$ is an algebra of $T$.

CategoryTheory.Monad.ForgetCreatesColimits.lambdadefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the lambda of c and t (from the name)

English

Let $c$ be a cocone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the lambda of $c$ and $t$ is a homomorphism of $\operatorname{pt}$ applied to the map cocone of $\operatorname{toFunctor}$ applied to $T$ and $c$ and $\operatorname{pt}$ applied to $c$ defined as $\operatorname{desc}$ applied to $\operatorname{isColimitOfPreserves}$ applied to $\operatorname{toFunctor}$ applied to $T$ and $t$ and the new cocone of $c$.

CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconedefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the lifted cocone of c and t (from the name)

English

Let $c$ be a cocone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the lifted cocone of $c$ and $t$ is a cocone of $D$.

CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimitdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

no wording

English

Let $c$ be a cocone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{liftedCoconeIsColimit}$ applied to $c$ and $t$ is an element of $\operatorname{IsColimit}$ applied to the lifted cocone of $c$ and $t$.

CategoryTheory.Monad.ForgetCreatesColimits.newCoconedefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the new cocone of c (from the name)

English

Let $c$ be a cocone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Then the new cocone of $c$ is a cocone of the composition of the composition of $D$ and $\operatorname{forget}$ applied to $T$ and $\operatorname{toFunctor}$ applied to $T$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and the composition of $\mathrm{CategoryTheory\_\_Monad\_\_ForgetCreatesColimits\_\_\_u3b3\_}$ and the inclusion of $c$.

CategoryTheory.Monad.ForgetCreatesColimits.γdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

no wording

English

$\mathrm{CategoryTheory\_\_Monad\_\_ForgetCreatesColimits\_\_\_u3b3\_}$ is a homomorphism of the composition of the composition of $D$ and $\operatorname{forget}$ applied to $T$ and $\operatorname{toFunctor}$ applied to $T$ and the composition of $D$ and $\operatorname{forget}$ applied to $T$.

CategoryTheory.Monad.ForgetCreatesLimits.conePointdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the cone point of c and t (from the name)

English

Let $D$ be a functor of $J$ and the set of algebras of $T$. Let $c$ be a cone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the cone point of $c$ and $t$ is an algebra of $T$.

CategoryTheory.Monad.ForgetCreatesLimits.liftedConedefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the lifted cone of c and t (from the name)

English

CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimitdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

no wording

English

Let $D$ be a functor of $J$ and the set of algebras of $T$. Let $c$ be a cone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{liftedConeIsLimit}$ applied to $D$, $c$ and $t$ is an element of $\operatorname{IsLimit}$ applied to the lifted cone of $c$ and $t$.

CategoryTheory.Monad.ForgetCreatesLimits.newConedefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

the new cone of D and c (from the name)

English

Let $D$ be a functor of $J$ and the set of algebras of $T$. Let $c$ be a cone of the composition of $D$ and $\operatorname{forget}$ applied to $T$. Then the new cone of $D$ and $c$ is a cone of the composition of $D$ and $\operatorname{forget}$ applied to $T$ defined as $\operatorname{mk}$ applied to the action of $\operatorname{toFunctor}$ applied to $T$ and $\operatorname{pt}$ applied to $c$ and the composition of the inverse of the constant composition of $\operatorname{pt}$ applied to $c$ and $\operatorname{toFunctor}$ applied to $T$ and the composition of the right whisker of the projection of $c$ and $\operatorname{toFunctor}$ applied to $T$ and $\mathrm{CategoryTheory\_\_Monad\_\_ForgetCreatesLimits\_\_\_u3b3\_}$ applied to $D$.

CategoryTheory.Monad.ForgetCreatesLimits.γdefMathlib.CategoryTheory.Monad.Limits, function or constant

Wording

no wording

English

Let $D$ be a functor of $J$ and the set of algebras of $T$. Then $\mathrm{CategoryTheory\_\_Monad\_\_ForgetCreatesLimits\_\_\_u3b3\_}$ applied to $D$ is a homomorphism of the composition of $D$ and the composition of $\operatorname{forget}$ applied to $T$ and $\operatorname{toFunctor}$ applied to $T$ and the composition of $D$ and $\operatorname{forget}$ applied to $T$.

Mathlib.CategoryTheory.Monad.Monadicity

CategoryTheory.Monad.CreatesColimitOfIsSplitPairclassMathlib.CategoryTheory.Monad.Monadicity, predicate

Wording

no wording

English

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

CategoryTheory.Monad.HasCoequalizerOfIsSplitPairclassMathlib.CategoryTheory.Monad.Monadicity, predicate

Wording

no wording

English

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

CategoryTheory.Monad.MonadicityInternal.comparisonAdjunctiondefMathlib.CategoryTheory.Monad.Monadicity, function or constant

Wording

the comparison adjunction of adj (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the comparison adjunction of $\mathrm{adj}$ is an adjunction of the left adjoint comparison of $\mathrm{adj}$ and the comparison of $\mathrm{adj}$.

CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquivdefMathlib.CategoryTheory.Monad.Monadicity, function or constant

Wording

the comparison left adjoint homomorphism equivalence of A and B (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $A$ be an algebra of the monad of $\mathrm{adj}$. Let $B$ be an element of $D$. Then the comparison left adjoint homomorphism equivalence of $A$ and $B$ is an equivalence from the set of homomorphisms of the object function for the left adjoint to the comparison functor of $\mathrm{adj}$ and $A$ and $B$ to the set of homomorphisms of $A$ and the action of the comparison of $\mathrm{adj}$ and $B$.

CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObjdefMathlib.CategoryTheory.Monad.Monadicity, function or constant

Wording

the object function for the left adjoint to the comparison functor of adj and A (from the docstring)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $A$ be an algebra of the monad of $\mathrm{adj}$. Then the object function for the left adjoint to the comparison functor of $\mathrm{adj}$ and $A$ is an element of $D$ defined as the coequalizer of the map of $F$ and $\operatorname{a}$ applied to $A$ and the component of the counit of $\mathrm{adj}$ and the action of $F$ and $\operatorname{A}$ applied to $A$.

CategoryTheory.Monad.MonadicityInternal.counitCoequalizerOfReflectsCoequalizerdefMathlib.CategoryTheory.Monad.Monadicity, function or constant

Wording

the counit cofork of adj and B (from the docstring)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $B$ be an element of $D$. Then the counit cofork of $\mathrm{adj}$ and $B$ is an element of $\operatorname{IsColimit}$ applied to the counit cofork of $\mathrm{adj}$ and $B$.

CategoryTheory.Monad.MonadicityInternal.counitCoforkdefMathlib.CategoryTheory.Monad.Monadicity, function or constant

Wording

the counit cofork of adj and B (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $B$ be an element of $D$. Then the counit cofork of $\mathrm{adj}$ and $B$ is a cofork of the map of $F$ and the map of $G$ and the component of the counit of $\mathrm{adj}$ and $B$ and the component of the counit of $\mathrm{adj}$ and the action of $F$ and the action of $G$ and $B$.

CategoryTheory.Monad.MonadicityInternal.leftAdjointComparisondefMathlib.CategoryTheory.Monad.Monadicity, function or constant

Wording

the left adjoint comparison of adj (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the left adjoint comparison of $\mathrm{adj}$ is a functor of the set of algebras of the monad of $\mathrm{adj}$ and $D$.

CategoryTheory.Monad.MonadicityInternal.unitCoforkdefMathlib.CategoryTheory.Monad.Monadicity, function or constant

Wording

the unit cofork of A (from the name)

English

Let $A$ be an algebra of the monad of $\mathrm{adj}$. Then the unit cofork of $A$ is a cofork of the map of $G$ and the map of $F$ and $\operatorname{a}$ applied to $A$ and the map of $G$ and the component of the counit of $\mathrm{adj}$ and the action of $F$ and $\operatorname{A}$ applied to $A$.

CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizerdefMathlib.CategoryTheory.Monad.Monadicity, function or constant

Wording

the unit cofork of A (from the docstring)

English

Let $A$ be an algebra of the monad of $\mathrm{adj}$. Then the unit cofork of $A$ is an element of $\operatorname{IsColimit}$ applied to the unit cofork of $A$ defined as $\operatorname{isColimitOfHasCoequalizerOfPreservesColimit}$ applied to $G$, the map of $F$ and $\operatorname{a}$ applied to $A$ and the component of the counit of $\mathrm{adj}$ and the action of $F$ and $\operatorname{A}$ applied to $A$.

CategoryTheory.Monad.PreservesColimitOfIsReflexivePairclassMathlib.CategoryTheory.Monad.Monadicity, predicate

Wording

no wording

English

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

CategoryTheory.Monad.PreservesColimitOfIsSplitPairclassMathlib.CategoryTheory.Monad.Monadicity, predicate

Wording

no wording

English

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

CategoryTheory.Monad.ReflectsColimitOfIsSplitPairclassMathlib.CategoryTheory.Monad.Monadicity, predicate

Wording

no wording

English

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

Mathlib.CategoryTheory.Monad.Products

CategoryTheory.algebraEquivUnderdefMathlib.CategoryTheory.Monad.Products, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{algebraEquivUnder}$ applied to $X$ is an equivalence of the set of algebras of the coproduct monad of $X$ and $\operatorname{Under}$ applied to $X$.

CategoryTheory.algebraToUnderdefMathlib.CategoryTheory.Monad.Products, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{algebraToUnder}$ applied to $X$ is a functor of the set of algebras of the coproduct monad of $X$ and $\operatorname{Under}$ applied to $X$.

CategoryTheory.coalgebraEquivOverdefMathlib.CategoryTheory.Monad.Products, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{coalgebraEquivOver}$ applied to $X$ is an equivalence of the set of coalgebras of the product comonad of $X$ and $\operatorname{Over}$ applied to $X$.

CategoryTheory.coalgebraToOverdefMathlib.CategoryTheory.Monad.Products, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{coalgebraToOver}$ applied to $X$ is a functor of the set of coalgebras of the product comonad of $X$ and $\operatorname{Over}$ applied to $X$.

CategoryTheory.coprodMonaddefMathlib.CategoryTheory.Monad.Products, function or constant

Wording

the coproduct monad of X (from the name)

English

Let $X$ be an element of $C$. Then the coproduct monad of $X$ is a monad of $C$.

CategoryTheory.overToCoalgebradefMathlib.CategoryTheory.Monad.Products, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{overToCoalgebra}$ applied to $X$ is a functor of $\operatorname{Over}$ applied to $X$ and the set of coalgebras of the product comonad of $X$.

CategoryTheory.prodComonaddefMathlib.CategoryTheory.Monad.Products, function or constant

Wording

the product comonad of X (from the name)

English

Let $X$ be an element of $C$. Then the product comonad of $X$ is a comonad of $C$.

CategoryTheory.underToAlgebradefMathlib.CategoryTheory.Monad.Products, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{underToAlgebra}$ applied to $X$ is a functor of $\operatorname{Under}$ applied to $X$ and the set of algebras of the coproduct monad of $X$.

Mathlib.CategoryTheory.Monad.Types

CategoryTheory.kleisliCatEquivKleislidefMathlib.CategoryTheory.Monad.Types, function or constant

Wording

no wording

English

Let $m$ be a function from sets to sets. Then $\operatorname{kleisliCatEquivKleisli}$ applied to $m$ is an equivalence of $\operatorname{KleisliCat}$ applied to $m$ and $\operatorname{Kleisli}$ applied to the category theory of $m$.

CategoryTheory.ofTypeMonaddefMathlib.CategoryTheory.Monad.Types, function or constant

Wording

the category theory of m (from the name)

English

Let $m$ be a function from sets to sets. Then the category theory of $m$ is a monad of the set of sets.

Mathlib.CategoryTheory.Monoidal.Action.Basic

CategoryTheory.MonoidalCategory.MonoidalLeftActionclassMathlib.CategoryTheory.Monoidal.Action.Basic, predicate

Wording

no wording

English

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

CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIsodefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action associator natural isomorphism of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the action associator natural isomorphism of $C$ and $D$ is an isomorphism of the bifunctor composition of the tensor product bifunctor of $C$ and the curried action of $C$ and $D$ and the bifunctor composition of the curried action of $C$ and $D$ and the curried action of $C$ and $D$.

CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the left action of D and c (from the name)

English

Let $D$ be a set. Let $c$ be an element of $C$. Then the left action of $D$ and $c$ is a functor of $D$ and $D$ defined as the action of the curried action of $C$ and $D$ and $c$.

CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionRightdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the right action of C and d (from the name)

English

Let $C$ be a set. Let $d$ be an element of $D$. Then the right action of $C$ and $d$ is a functor of $C$ and $D$ defined as the action of the flip of the curried action of $C$ and $D$ and $d$.

CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIsodefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action unit natural isomorphism of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the action unit natural isomorphism of $C$ and $D$ is an isomorphism of the left action of $D$ and the tensor unity in the monoidal structure of $C$ and the identity of $D$.

CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActiondefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the curried action of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the curried action of $C$ and $D$ is a functor of $C$ and the set of functors of $D$ and $D$.

CategoryTheory.MonoidalCategory.MonoidalLeftActionStructclassMathlib.CategoryTheory.Monoidal.Action.Basic, predicate

Wording

no wording

English

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

CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIsodefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action associator isomorphism of d and #3 (from the name)

English

Let $c$ and $\mathrm{c'}$ be elements of $C$. Let $d$ be an element of $D$. Then the action associator isomorphism of $\mathrm{c'}$ and $d$ is an isomorphism of the action object of the tensor object of $c$ and $\mathrm{c'}$ and $d$ and the action object of $c$ and the action object of $\mathrm{c'}$ and $d$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$, $c$, $\mathrm{c'}$ and $d$.

CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action of f and g (from the docstring)

English

Let $f$ be a homomorphism of $c$ and $\mathrm{c'}$. Let $g$ be a homomorphism of $d$ and $\mathrm{d'}$. Then the action of $f$ and $g$ is a homomorphism of the action object of $c$ and $d$ and the action object of $\mathrm{c'}$ and $\mathrm{d'}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $f$ and $g$.

CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeftdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the left action of f and d (from the docstring)

English

Let $f$ be a homomorphism of $c$ and $\mathrm{c'}$. Let $d$ be an element of $D$. Then the left action of $f$ and $d$ is a homomorphism of the action object of $c$ and $d$ and the action object of $\mathrm{c'}$ and $d$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $f$ and $d$.

CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRightdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action of c and f (from the docstring)

English

Let $c$ be an element of $C$. Let $f$ be a homomorphism of $d$ and $\mathrm{d'}$. Then the action of $c$ and $f$ is a homomorphism of the action object of $c$ and $d$ and the action object of $c$ and $\mathrm{d'}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $c$ and $f$.

CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObjdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action object of x3 and x4 (from the name)

English

Let $x_{3}$ be an element of $C$. Let $x_{4}$ be an element of $D$. Then the action object of $x_{3}$ and $x_{4}$ is an element of $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$.

CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIsodefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action unit isomorphism of d (from the name)

English

Let $d$ be an element of $D$. Then the action unit isomorphism of $d$ is an isomorphism of the action object of the tensor unity in the monoidal structure of $C$ and $d$ and $d$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$ and $d$.

CategoryTheory.MonoidalCategory.MonoidalRightActionclassMathlib.CategoryTheory.Monoidal.Action.Basic, predicate

Wording

no wording

English

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

CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIsodefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action associator natural isomorphism of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the action associator natural isomorphism of $C$ and $D$ is an isomorphism of the bifunctor composition of the tensor product bifunctor of $C$ and the curried action of $C$ and $D$ and the flip of the bifunctor composition of the curried action of $C$ and $D$ and the curried action of $C$ and $D$.

CategoryTheory.MonoidalCategory.MonoidalRightAction.actionLeftdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the left action of C and d (from the name)

English

Let $C$ be a set. Let $d$ be an element of $D$. Then the left action of $C$ and $d$ is a functor of $C$ and $D$ defined as the action of the flip of the curried action of $C$ and $D$ and $d$.

CategoryTheory.MonoidalCategory.MonoidalRightAction.actionRightdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the right action of D and c (from the name)

English

Let $D$ be a set. Let $c$ be an element of $C$. Then the right action of $D$ and $c$ is a functor of $D$ and $D$ defined as the action of the curried action of $C$ and $D$ and $c$.

CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIsodefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action unit natural isomorphism of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the action unit natural isomorphism of $C$ and $D$ is an isomorphism of the right action of $D$ and the tensor unity in the monoidal structure of $C$ and the identity of $D$.

CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActiondefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the curried action of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the curried action of $C$ and $D$ is a functor of $C$ and the set of functors of $D$ and $D$.

CategoryTheory.MonoidalCategory.MonoidalRightActionStructclassMathlib.CategoryTheory.Monoidal.Action.Basic, predicate

Wording

no wording

English

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

CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIsodefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action associator isomorphism of c and #3 (from the name)

English

Let $d$ be an element of $D$. Let $c$ and $\mathrm{c'}$ be elements of $C$. Then the action associator isomorphism of $c$ and $\mathrm{c'}$ is an isomorphism of the action object of $d$ and the tensor object of $c$ and $\mathrm{c'}$ and the action object of the action object of $d$ and $c$ and $\mathrm{c'}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$, $d$, $c$ and $\mathrm{c'}$.

CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action of f and g (from the docstring)

English

Let $f$ be a homomorphism of $d$ and $\mathrm{d'}$. Let $g$ be a homomorphism of $c$ and $\mathrm{c'}$. Then the action of $f$ and $g$ is a homomorphism of the action object of $d$ and $c$ and the action object of $\mathrm{d'}$ and $\mathrm{c'}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $f$ and $g$.

CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeftdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action of f and c (from the docstring)

English

Let $f$ be a homomorphism of $d$ and $\mathrm{d'}$. Let $c$ be an element of $C$. Then the action of $f$ and $c$ is a homomorphism of the action object of $d$ and $c$ and the action object of $\mathrm{d'}$ and $c$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $f$ and $c$.

CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRightdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the right action of d and f (from the docstring)

English

Let $d$ be an element of $D$. Let $f$ be a homomorphism of $c$ and $\mathrm{c'}$. Then the right action of $d$ and $f$ is a homomorphism of the action object of $d$ and $c$ and the action object of $d$ and $\mathrm{c'}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $d$ and $f$.

CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObjdefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action object of x3 and x4 (from the name)

English

Let $x_{3}$ be an element of $D$. Let $x_{4}$ be an element of $C$. Then the action object of $x_{3}$ and $x_{4}$ is an element of $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$.

CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIsodefMathlib.CategoryTheory.Monoidal.Action.Basic, function or constant

Wording

the action unit isomorphism of d (from the name)

English

Let $d$ be an element of $D$. Then the action unit isomorphism of $d$ is an isomorphism of the action object of $d$ and the tensor unity in the monoidal structure of $C$ and $d$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$ and $d$.

Mathlib.CategoryTheory.Monoidal.Action.End

CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIsodefMathlib.CategoryTheory.Monoidal.Action.End, function or constant

Wording

the curried action action of F (from the name)

English

Let $F$ be a functor of $C$ and the set of monoidal opposites of the set of functors of $D$ and $D$. Then the curried action action of $F$ is an isomorphism of $\operatorname{curriedActionMop}$ applied to $C$ and $D$ and $F$ defined as the identity of $\operatorname{curriedActionMop}$ applied to $C$ and $D$.

CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopdefMathlib.CategoryTheory.Monoidal.Action.End, function or constant

Wording

no wording

English

Let $C$ and $D$ be sets. Then $\operatorname{curriedActionMop}$ applied to $C$ and $D$ is a functor of $C$ and the set of monoidal opposites of the set of functors of $D$ and $D$ defined as the composition of the curried action of $C$ and $D$ and $\operatorname{mopFunctor}$ applied to the set of functors of $D$ and $D$.

CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIsodefMathlib.CategoryTheory.Monoidal.Action.End, function or constant

Wording

the curried action action of F (from the name)

English

Let $F$ be a functor of $C$ and the set of functors of $D$ and $D$. Then the curried action action of $F$ is an isomorphism of the curried action of $C$ and $D$ and $F$ defined as the identity of the curried action of $C$ and $D$.