Definitions: Mathlib.CategoryTheory, part 1 of 25

387 definitions of 60 modules, Mathlib.CategoryTheory.Abelian.Basic to Mathlib.CategoryTheory.Adjunction.Quadruple. ‹ previous next ›

Mathlib.CategoryTheory.Abelian.Basic

CategoryTheory.AbelianclassMathlib.CategoryTheory.Abelian.Basic, predicate
Wording
C is Abelian (from the name)
English
Let $C$ be a set. Then we can say that $C$ is Abelian.
CategoryTheory.Abelian.AbelianStructstructureMathlib.CategoryTheory.Abelian.Basic, type
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the elements of $\operatorname{AbelianStruct}$ applied to $f$ are a basic type.
CategoryTheory.Abelian.AbelianStruct.cokernelCoforkdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the cokernel cofork of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{AbelianStruct}$ applied to $f$. Then the cokernel cofork of $\mathrm{self}$ is a cokernel cofork of $f$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
CategoryTheory.Abelian.AbelianStruct.imagedefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the image of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\operatorname{AbelianStruct}$ applied to $f$. Then the image of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.
CategoryTheory.Abelian.AbelianStruct.imageIsCokerneldefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the image of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\operatorname{AbelianStruct}$ applied to $f$. Then the image of $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection to the image of $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_AbelianStruct\_\_\_u3b9\_\_image\_u3c0\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$.
CategoryTheory.Abelian.AbelianStruct.imageIsKerneldefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the image of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\operatorname{AbelianStruct}$ applied to $f$. Then the image of $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of the image of $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_AbelianStruct\_\_image\_u3b9\_\_\_u3c0\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj10}$ applied to $\mathrm{self}$.
CategoryTheory.Abelian.AbelianStruct.imageιdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the inclusion of the image of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\operatorname{AbelianStruct}$ applied to $f$. Then the inclusion of the image of $\mathrm{self}$ is a homomorphism of the image of $\mathrm{self}$ and $Y$ defined as $\operatorname{proj8}$ applied to $\mathrm{self}$.
CategoryTheory.Abelian.AbelianStruct.imageπdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the projection to the image of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\operatorname{AbelianStruct}$ applied to $f$. Then the projection to the image of $\mathrm{self}$ is a homomorphism of $X$ and the image of $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.
CategoryTheory.Abelian.AbelianStruct.isColimitCokernelCoforkdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the cokernel cofork of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\operatorname{AbelianStruct}$ applied to $f$. Then the cokernel cofork of $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cofork of $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.
CategoryTheory.Abelian.AbelianStruct.isLimitKernelForkdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the kernel fork of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\operatorname{AbelianStruct}$ applied to $f$. Then the kernel fork of $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the kernel fork of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
CategoryTheory.Abelian.AbelianStruct.kernelForkdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the kernel fork of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{AbelianStruct}$ applied to $f$. Then the kernel fork of $\mathrm{self}$ is a kernel fork of $f$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Abelian.BiproductToPushoutIsCokernel.biproductToPushoutdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the biproduct to pushout of f and g (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the biproduct to pushout of $f$ and $g$ is a homomorphism of the biproduct of $Y$ and $Z$ and the pushout of $f$ and $g$ defined as $\operatorname{desc}$ applied to the left injection of $f$ and $g$ and the right injection of $f$ and $g$.
CategoryTheory.Abelian.BiproductToPushoutIsCokernel.biproductToPushoutCoforkdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the biproduct to pushout cofork of f and g (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the biproduct to pushout cofork of $f$ and $g$ is a cokernel cofork of the lift of $f$ and $\operatorname{neg}$ applied to $g$.
CategoryTheory.Abelian.BiproductToPushoutIsCokernel.isColimitBiproductToPushoutdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then $\operatorname{isColimitBiproductToPushout}$ applied to $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to the biproduct to pushout cofork of $f$ and $g$.
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageFactorisationdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the image factorisation of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the image factorisation of $f$ is an image factorisation of $f$.
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisationdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the factorisation of f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the factorisation of $f$ is a monomorphism factorisation of $f$.
CategoryTheory.Abelian.PullbackToBiproductIsKernel.isLimitPullbackToBiproductdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{isLimitPullbackToBiproduct}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the pullback to biproduct fork of $f$ and $g$.
CategoryTheory.Abelian.PullbackToBiproductIsKernel.pullbackToBiproductdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the pullback to biproduct of f and g (from the name)
English
Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback to biproduct of $f$ and $g$ is a homomorphism of the pullback of $f$ and $g$ and the biproduct of $X$ and $Y$ defined as the lift of the first projection of the pullback of $f$ and $g$ and the second projection of the pullback of $f$ and $g$.
CategoryTheory.Abelian.PullbackToBiproductIsKernel.pullbackToBiproductForkdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the pullback to biproduct fork of f and g (from the name)
English
Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback to biproduct fork of $f$ and $g$ is a kernel fork of $\operatorname{desc}$ applied to $f$ and $\operatorname{neg}$ applied to $g$.
CategoryTheory.Abelian.coimdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
no wording
English
$\operatorname{coim}$ is a functor of the set of arrows of $C$ and $C$.
CategoryTheory.Abelian.coimIsoImdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the image and coimage (from the docstring)
English
The image and coimage is an isomorphism of $\operatorname{coim}$ and the imaginary part.
CategoryTheory.Abelian.coimageIsoImagedefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the coimage isomorphism image of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the coimage isomorphism image of $f$ is an isomorphism of the coimage of $f$ and the image of $f$ defined as $\operatorname{asIso}$ applied to the canonical map from the abelian coimage to the abelian image of $f$.
CategoryTheory.Abelian.coimageIsoImage'defMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the coimage isomorphism image of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the coimage isomorphism image of $f$ is an isomorphism of the coimage of $f$ and the categorical image of $f$ defined as the isomorphism extension of $\operatorname{toMonoIsImage}$ applied to the coimage strong epimorphism monomorphism factorisation of $f$ and $\operatorname{isImage}$ applied to $f$.
CategoryTheory.Abelian.coimageStrongEpiMonoFactorisationdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the coimage strong epimorphism monomorphism factorisation of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $Q$. Then the coimage strong epimorphism monomorphism factorisation of $f$ is a strong epimorphism monomorphism factorisation of $f$.
CategoryTheory.Abelian.epiDescdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $T$ such that the composition of the inclusion of $f$ and $g$ is equal to $0$. Then $\operatorname{epiDesc}$ applied to $f$, $g$ and $\mathrm{hg}$ is a homomorphism of $Y$ and $T$ defined as $\operatorname{desc}$ applied to $\operatorname{epiIsCokernelOfKernel}$ applied to the cone of the parallel pair of $f$ and $0$ and $\operatorname{isLimit}$ applied to the parallel pair of $f$ and $0$ and the projection of $g$ and $\mathrm{hg}$.
CategoryTheory.Abelian.epiIsCokernelOfKerneldefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
no wording
English
Let $s$ be a fork of $f$ and $0$. Let $h_{1}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{epiIsCokernelOfKernel}$ applied to $s$ and $h_{1}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{condition}$ applied to $s$ defined as $\operatorname{epiIsCokernelOfKernel}$ applied to $s$ and $h_{1}$.
CategoryTheory.Abelian.imdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the imaginary part (from the name)
English
The imaginary part is a functor of the set of arrows of $C$ and $C$.
CategoryTheory.Abelian.imageIsoImagedefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the image isomorphism image of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the image isomorphism image of $f$ is an isomorphism of the image of $f$ and the categorical image of $f$ defined as the isomorphism extension of $\operatorname{toMonoIsImage}$ applied to the image strong epimorphism monomorphism factorisation of $f$ and $\operatorname{isImage}$ applied to $f$.
CategoryTheory.Abelian.imageStrongEpiMonoFactorisationdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the image strong epimorphism monomorphism factorisation of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $Q$. Then the image strong epimorphism monomorphism factorisation of $f$ is a strong epimorphism monomorphism factorisation of $f$.
CategoryTheory.Abelian.isColimitMapCoconeOfCokernelCoforkOfπdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
no wording
English
Let $p$ be a homomorphism of $X$ and $Y$. Let $F$ be a functor of $D$ and $C$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_isColimitMapCoconeOfCokernelCoforkOf\_u3c0\_}$ applied to $p$ and $F$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of $F$ and the projection of $p$ and $\operatorname{condition}$ applied to $p$.
CategoryTheory.Abelian.isLimitMapConeOfKernelForkOfιdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
no wording
English
Let $i$ be a homomorphism of $X$ and $Y$. Let $F$ be a functor of $D$ and $C$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_isLimitMapConeOfKernelForkOf\_u3b9\_}$ applied to $i$ and $F$ is an element of $\operatorname{IsLimit}$ applied to the map cone of $F$ and the inclusion of $i$ and $\operatorname{condition}$ applied to $i$.
CategoryTheory.Abelian.monoIsKernelOfCokerneldefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
no wording
English
Let $s$ be a cofork of $f$ and $0$. Let $h_{1}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Then $\operatorname{monoIsKernelOfCokernel}$ applied to $s$ and $h_{1}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $\operatorname{condition}$ applied to $s$ defined as $\operatorname{monoIsKernelOfCokernel}$ applied to $s$ and $h_{1}$.
CategoryTheory.Abelian.monoLiftdefMathlib.CategoryTheory.Abelian.Basic, function or constant
Wording
the monomorphism lift of f and g (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $T$ and $Y$ such that the composition of $g$ and the projection of $f$ is equal to $0$. Then the monomorphism lift of $f$ and $g$ is a homomorphism of $T$ and $X$ defined as the lift of $\operatorname{monoIsKernelOfCokernel}$ applied to the cocone of the parallel pair of $f$ and $0$ and $\operatorname{isColimit}$ applied to the parallel pair of $f$ and $0$ and the inclusion of $g$ and $\mathrm{hg}$.

Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

CategoryTheory.kernelCokernelCompSequencedefMathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp, function or constant
Wording
the kernel cokernel composition sequence 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 kernel cokernel composition sequence of $f$ and $g$ is a composable arrow of $C$ and $5$.
CategoryTheory.kernelCokernelCompSequence.isColimitdefMathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{isColimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $f$ and $g$ and $\mathrm{CategoryTheory\_\_kernelCokernelCompSequence\_\_\_u3c6\_\_\_u3c0\_}$ applied to $f$ and $g$.
CategoryTheory.kernelCokernelCompSequence.isLimitdefMathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{isLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $f$ and $g$ and $\mathrm{CategoryTheory\_\_kernelCokernelCompSequence\_\_\_u3b9\_\_\_u3c6\_}$ applied to $f$ and $g$.
CategoryTheory.kernelCokernelCompSequence.snakeInputdefMathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp, function or constant
Wording
the snake input 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 snake input of $f$ and $g$ is a snake input of $C$.
CategoryTheory.kernelCokernelCompSequence.δdefMathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\mathrm{CategoryTheory\_\_kernelCokernelCompSequence\_\_\_u3b4\_}$ applied to $f$ and $g$ is a homomorphism of the kernel of $g$ and the cokernel of $f$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_\_u3b4\_}$ applied to the snake input of $f$ and $g$.
CategoryTheory.kernelCokernelCompSequence.ιdefMathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp, function or constant
Wording
the inclusion 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 inclusion of $f$ and $g$ is a homomorphism of the kernel of the composition of $f$ and $g$ and the biproduct of $X$ and $Y$ defined as the lift of the inclusion of the composition of $f$ and $g$ and the composition of the inclusion of the composition of $f$ and $g$ and $f$.
CategoryTheory.kernelCokernelCompSequence.πdefMathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp, function or constant
Wording
the projection 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 projection of $f$ and $g$ is a homomorphism of the biproduct of $Y$ and $Z$ and the cokernel of the composition of $f$ and $g$ defined as $\operatorname{desc}$ applied to the composition of $g$ and the projection of the composition of $f$ and $g$ and the projection of the composition of $f$ and $g$.
CategoryTheory.kernelCokernelCompSequence.φdefMathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\mathrm{CategoryTheory\_\_kernelCokernelCompSequence\_\_\_u3c6\_}$ applied to $f$ and $g$ is a homomorphism of the biproduct of $X$ and $Y$ and the biproduct of $Y$ and $Z$ defined as $\operatorname{desc}$ applied to the composition of $f$ and the left injection and the lift of $\operatorname{neg}$ applied to the identity morphism of $Y$ and $g$.

Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

CategoryTheory.Abelian.epiWithInjectiveKerneldefMathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel, function or constant
Wording
the epimorphism with injective kernel (from the name)
English
The epimorphism with injective kernel is a morphism property of $C$ defined as the function that maps $x_{2}$, $x_{3}$ and $f$ to the proposition that $f$ is an epimorphism and the kernel of $f$ is injective.

Mathlib.CategoryTheory.Abelian.Exact

CategoryTheory.ShortComplex.Exact.isColimitCoimagedefMathlib.CategoryTheory.Abelian.Exact, function or constant
Wording
no wording
English
Assume that $S$ is exact. Then $\operatorname{isColimitCoimage}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection onto the coimage of $\operatorname{g}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Abelian\_\_comp\_coimage\_\_u3c0\_\_eq\_zero}$ applied to $\operatorname{zero}$ applied to $S$.
CategoryTheory.ShortComplex.Exact.isColimitImagedefMathlib.CategoryTheory.Abelian.Exact, function or constant
Wording
no wording
English
Assume that $S$ is exact. Then $\operatorname{isColimitImage}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to the projection of the map from the source to the image of $\operatorname{g}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Limits\_\_comp\_factorThruImage\_eq\_zero}$ applied to $\operatorname{zero}$ applied to $S$.
CategoryTheory.ShortComplex.Exact.isLimitImagedefMathlib.CategoryTheory.Abelian.Exact, function or constant
Wording
no wording
English
Assume that $S$ is exact. Then $\operatorname{isLimitImage}$ applied to $h$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of the image into the codomain of $\operatorname{f}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Abelian\_\_image\_\_u3b9\_\_comp\_eq\_zero}$ applied to $\operatorname{zero}$ applied to $S$.
CategoryTheory.ShortComplex.Exact.isLimitImage'defMathlib.CategoryTheory.Abelian.Exact, function or constant
Wording
no wording
English
Assume that $S$ is exact. Then $\operatorname{isLimitImage'}$ applied to $h$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of the image of $\operatorname{f}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Limits\_\_image\_\_u3b9\_\_comp\_eq\_zero}$ applied to $\operatorname{zero}$ applied to $S$.

Mathlib.CategoryTheory.Abelian.Ext

CategoryTheory.ProjectiveResolution.isoExtdefMathlib.CategoryTheory.Abelian.Ext, function or constant
Wording
the isomorphism extension of n and Y (from the name)
English
Let $P$ be a projective resolution of $X$. Let $n$ be a natural number. Let $Y$ be an element of $C$. Then the isomorphism extension of $n$ and $Y$ is an isomorphism of the action of the action of the extension of $n$ and $\operatorname{op}$ applied to $X$ and $Y$ and the homology of the linear Yoneda object of the complex of $P$ and $Y$ and $n$ defined as the composition of the inverse of the opposite of the isomorphism left derived object of the right opposite of the action of the linear Yoneda of $R$ and $C$ and $Y$ and $n$ and the inverse of the homology opposite of the action of the map homological complex of the right opposite of the action of the linear Yoneda of $R$ and $C$ and $Y$ and $\operatorname{down}$ applied to $\Natural$ and the complex of $P$ and $n$.
ChainComplex.linearYonedaObjdefMathlib.CategoryTheory.Abelian.Ext, function or constant
Wording
the linear Yoneda object of X and Y (from the name)
English
Let $X$ be a chain complex of $C$ and $x_{2}$. Let $A$ be a set. Let $Y$ be an element of $C$. Then the linear Yoneda object of $X$ and $Y$ is a cochain complex of the set of module categories of $A$ and $x_{2}$ defined as the opposite of the action of the map homological complex of the right opposite of the action of the linear Yoneda of $A$ and $C$ and $Y$ and $\operatorname{down}$ applied to $x_{2}$ and $X$.
ExtdefMathlib.CategoryTheory.Abelian.Ext, function or constant
Wording
the extension of n (from the name)
English
Let $R$ and $C$ be sets. Let $n$ be a natural number. Then the extension of $n$ is a functor of the set of opposites of $C$ and the set of functors of $C$ and the set of module categories of $R$.

Mathlib.CategoryTheory.Abelian.FreydMitchell

CategoryTheory.Abelian.FreydMitchell.EmbeddingRingdefMathlib.CategoryTheory.Abelian.FreydMitchell, type
Wording
embedding ring of C (from the name)
English
Let $C$ be a set. Then an embedding ring of $C$ is an element of the function that maps $C$ to the set of embedding rings of the right opposite of the Yoneda.
CategoryTheory.Abelian.FreydMitchell.functordefMathlib.CategoryTheory.Abelian.FreydMitchell, function or constant
Wording
the functor of C (from the name)
English
Let $C$ be a set. Then the functor of $C$ is a functor of $C$ and the set of module categories of the set of embedding rings of $C$.

Mathlib.CategoryTheory.Abelian.FunctorCategory

CategoryTheory.Abelian.FunctorCategory.coimageObjIsodefMathlib.CategoryTheory.Abelian.FunctorCategory, function or constant
Wording
the coimage object isomorphism of x3 and X (from the name)
English
Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $X$ be an element of $C$. Then the coimage object isomorphism of $x_{3}$ and $X$ is an isomorphism of the action of the coimage of $x_{3}$ and $X$ and the coimage of the component of $x_{3}$ and $X$.
CategoryTheory.Abelian.FunctorCategory.imageObjIsodefMathlib.CategoryTheory.Abelian.FunctorCategory, function or constant
Wording
the image object isomorphism of x3 and X (from the name)
English
Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $X$ be an element of $C$. Then the image object isomorphism of $x_{3}$ and $X$ is an isomorphism of the action of the image of $x_{3}$ and $X$ and the image of the component of $x_{3}$ and $X$.

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

CategoryTheory.AB4defMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
C is a abelian group (from the name)
English
Let $C$ be a set. Then $C$ is an abelian group, if $\operatorname{AB4OfSize}$ holds for $C$.
CategoryTheory.AB4OfSizeclassMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
no wording
English
Let $C$ be a set. Then we can say that $\operatorname{AB4OfSize}$ holds for $C$.
CategoryTheory.AB4StardefMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
C is a abelian group star (from the name)
English
Let $C$ be a set. Then $C$ is an abelian group star, if $\operatorname{AB4StarOfSize}$ holds for $C$.
CategoryTheory.AB4StarOfSizeclassMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
no wording
English
Let $C$ be a set. Then we can say that $\operatorname{AB4StarOfSize}$ holds for $C$.
CategoryTheory.AB5defMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
C is a abelian group (from the name)
English
Let $C$ be a set. Then $C$ is an abelian group, if $\operatorname{AB5OfSize}$ holds for $C$.
CategoryTheory.AB5OfSizeclassMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
no wording
English
Let $C$ be a set. Then we can say that $\operatorname{AB5OfSize}$ holds for $C$.
CategoryTheory.AB5StardefMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
C is a abelian group star (from the name)
English
Let $C$ be a set. Then $C$ is an abelian group star, if $\operatorname{AB5StarOfSize}$ holds for $C$.
CategoryTheory.AB5StarOfSizeclassMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
no wording
English
Let $C$ be a set. Then we can say that $\operatorname{AB5StarOfSize}$ holds for $C$.
CategoryTheory.CountableAB4classMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
C is a countable abelian group (from the name)
English
Let $C$ be a set. Then we can say that $C$ is a countable abelian group.
CategoryTheory.CountableAB4StarclassMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
C is a countable abelian group star (from the name)
English
Let $C$ be a set. Then we can say that $C$ is a countable abelian group star.
CategoryTheory.HasExactColimitsOfShapeclassMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
no wording
English
Let $J$ and $C$ be sets. Then we can say that $\operatorname{HasExactColimitsOfShape}$ holds for $J$ and $C$.
CategoryTheory.HasExactLimitsOfShapeclassMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic, predicate
Wording
no wording
English
Let $J$ and $C$ be sets. Then we can say that $\operatorname{HasExactLimitsOfShape}$ holds for $J$ and $C$.

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

CategoryTheory.Limits.colim.mapShortComplexdefMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim, function or constant
Wording
the map short complex of f and g (from the name)
English
Let $S$ be a short complex of the set of functors of $J$ and $C$. Let $x_{4}$ be an element of $\operatorname{IsColimit}$ applied to $x_{3}$. Let $x_{5}$ be a cocone of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$. Let $x_{6}$ be a cocone of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$. Let $f$ be a homomorphism of $\operatorname{pt}$ applied to $x_{3}$ and $\operatorname{pt}$ applied to $x_{5}$. Let $g$ be a homomorphism of $\operatorname{pt}$ applied to $x_{5}$ and $\operatorname{pt}$ applied to $x_{6}$. Assume that for all elements $j_{1}$ of $J$, the composition of the component of the inclusion of $x_{3}$ and $j_{1}$ and $f$ is equal to the composition of the component of $\operatorname{f}$ applied to $S$ and $j_{1}$ and the component of the inclusion of $x_{5}$ and $j_{1}$. Assume that for all elements $j$ of $J$, the composition of the component of the inclusion of $x_{5}$ and $j$ and $g$ is equal to the composition of the component of $\operatorname{g}$ applied to $S$ and $j$ and the component of the inclusion of $x_{6}$ and $j$. Then the map short complex of $f$ and $g$ is a short complex of $C$.

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

CategoryTheory.Limits.IsColimit.pullbackOfHasExactColimitsOfShapedefMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected, function or constant
Wording
the pullback of hc and f (from the name)
English
Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $f$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $c$. Then the pullback of $\mathrm{hc}$ and $f$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $X$ and the second projection of the pullback of the inclusion of $c$ and the map of the constant of $J$ and $f$ defined as $\mathrm{CategoryTheory\_\_Limits\_\_Cocone\_\_isColimitOfIsIsoColimMap\_u3b9\_}$ applied to $\operatorname{mk}$ applied to $X$ and the second projection of the pullback of the inclusion of $c$ and the map of the constant of $J$ and $f$.
CategoryTheory.Limits.IsLimit.pushoutOfHasExactLimitsOfShapedefMathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected, function or constant
Wording
the pushout of hc and f (from the name)
English
Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $f$ be a homomorphism of $\operatorname{pt}$ applied to $c$ and $X$. Then the pushout of $\mathrm{hc}$ and $f$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $X$ and the right injection of the projection of $c$ and the map of the constant of $J$ and $f$ defined as $\mathrm{CategoryTheory\_\_Limits\_\_Cone\_\_isLimitOfIsIsoLimMap\_u3c0\_}$ applied to $\operatorname{mk}$ applied to $X$ and the right injection of the projection of $c$ and the map of the constant of $J$ and $f$.

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic

CategoryTheory.IsGrothendieckAbelianclassMathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic, predicate
Wording
no wording
English
Let $C$ be a set. Then we can say that $\operatorname{IsGrothendieckAbelian}$ holds for $C$.

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.FdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda, function or constant
Wording
no wording
English
Let $y$ be a homomorphism of $X$ and the action of $Y$ and $x_{3}$. Then $\mathrm{CategoryTheory\_\_IsGrothendieckAbelian\_\_IsPresentable\_\_injectivity\_u2080\_\_\_F}$ applied to $y$ is a functor of $\operatorname{Under}$ applied to $x_{3}$ and $\operatorname{MonoOver}$ applied to $X$.
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.fdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda, function or constant
Wording
no wording
English
Let $y$ be a homomorphism of $X$ and the action of $Y$ and $x_{3}$. Then $\mathrm{CategoryTheory\_\_IsGrothendieckAbelian\_\_IsPresentable\_\_injectivity\_u2080\_\_\_f}$ applied to $y$ is a homomorphism of the colimit of the kernel of $\mathrm{CategoryTheory\_\_IsGrothendieckAbelian\_\_IsPresentable\_\_injectivity\_u2080\_\_\_g}$ applied to $y$ and $X$ defined as the map of the obvious cocone of $\operatorname{Under}$ applied to $x_{3}$ and $X$ and the inclusion of $\mathrm{CategoryTheory\_\_IsGrothendieckAbelian\_\_IsPresentable\_\_injectivity\_u2080\_\_\_g}$ applied to $y$.
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.gdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda, function or constant
Wording
no wording
English
Let $y$ be a homomorphism of $X$ and the action of $Y$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_IsGrothendieckAbelian\_\_IsPresentable\_\_injectivity\_u2080\_\_\_g}$ applied to $y$ is a homomorphism of the action of the constant of $\operatorname{Under}$ applied to $x_{2}$ and $X$ and the composition of $\operatorname{forget}$ applied to $x_{2}$ and $Y$.
CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.FdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda, function or constant
Wording
no wording
English
Let $z$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $c$. Then $\operatorname{F}$ applied to $z$ is a functor of $J$ and $\operatorname{MonoOver}$ applied to $X$.
CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.fdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda, function or constant
Wording
no wording
English
Let $z$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $c$. Then $\operatorname{f}$ applied to $z$ is a homomorphism of the colimit of the pullback of the inclusion of $c$ and the map of the constant of $J$ and $z$ and $X$.

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

CategoryTheory.IsGrothendieckAbelian.generatingMonomorphismsdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives, function or constant
Wording
the generating monomorphism of G (from the name)
English
Let $G$ be an element of $C$. Then the generating monomorphism of $G$ is a morphism property of $C$ defined as the morphism property of the function that maps $X$ to the arrow of $X$.
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functordefMathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives, function or constant
Wording
the functor of x2 (from the name)
English
Assume that $G$ is a separator. Let $x_{2}$ be a subobject of $X$. Let $J$ be a set. Then the functor of $x_{2}$ is a functor of $J$ and $C$ defined as the composition of $\operatorname{functorToMonoOver}$ applied to $\mathrm{hG}$, $x_{2}$ and $J$ and the composition of $\operatorname{forget}$ applied to $X$ and $\operatorname{forget}$ applied to $X$.
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOverdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives, function or constant
Wording
no wording
English
Assume that $G$ is a separator. Let $x_{2}$ be a subobject of $X$. Let $J$ be a set. Then $\operatorname{functorToMonoOver}$ applied to $\mathrm{hG}$, $x_{2}$ and $J$ is a functor of $J$ and $\operatorname{MonoOver}$ applied to $X$.
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobjectdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives, function or constant
Wording
no wording
English
Assume that $G$ is a separator. Let $A$ be a subobject of $X$. Then $\operatorname{largerSubobject}$ applied to $\mathrm{hG}$ and $A$ is a subobject of $X$ defined as $\mathrm{dite}$ applied to the proposition that $A$ is equal to the top, the function that maps $\mathrm{hA}$ to the top and the function that maps $\mathrm{hA1}$ to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_IsGrothendieckAbelian\_\_generatingMonomorphisms\_\_exists\_larger\_subobject}$ applied to $\mathrm{hG}$, $A$ and $\mathrm{hA1}$.
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeMapFromBotdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives, function or constant
Wording
the transfinite composition of x2 and j (from the name)
English
Assume that $G$ is a separator. Let $x_{2}$ be a subobject of $X$. Let $j$ be an element of $J$. Then the transfinite composition of $x_{2}$ and $j$ is a transfinite composition of shape of the set of elements of $\operatorname{Iic}$ applied to $j$ and the map of the functor of $x_{2}$ and the homomorphism of $\mathrm{bot\_le}$.
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeOfEqTopdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives, function or constant
Wording
the transfinite composition of hG and hj (from the name)
English
Assume that $G$ is a separator. Assume that $\mathrm{transfiniteIterate}$ applied to $\operatorname{largerSubobject}$ applied to $\mathrm{hG}$, $j$ and $\operatorname{mk}$ applied to $f$ is equal to the top. Then the transfinite composition of $\mathrm{hG}$ and $\mathrm{hj}$ is a transfinite composition of shape of the set of elements of $\operatorname{Iic}$ applied to $j$ and $f$.
CategoryTheory.IsGrothendieckAbelian.monoMapFactorizationDataRlpdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{monoMapFactorizationDataRlp}$ applied to $f$ is a map factorization data of $\operatorname{rlp}$ applied to the monomorphism of $C$ and $f$ defined as the factorization data of the functorial factorization data of the monomorphism of $C$ and $\operatorname{rlp}$ applied to the monomorphism of $C$.

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ddefMathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu, function or constant
Wording
no wording
English
Let $g$ be a homomorphism of $M$ and $\operatorname{of}$ applied to the set of multiplicative opposites of the set of ends of $G$ and the set of homomorphisms of $G$ and $A$. Then $\operatorname{d}$ applied to $g$ is a homomorphism of the sigma object of the function that maps $x_{2}$ to $G$ and $A$ defined as $\operatorname{desc}$ applied to the function that maps $m$ to $\operatorname{hom}$ applied to $g$ and $m$.
CategoryTheory.IsGrothendieckAbelian.tensorObjdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu, function or constant
Wording
the tensor object of G (from the name)
English
Let $G$ be an element of $C$. Then the tensor object of $G$ is a functor of the set of module categories of the set of multiplicative opposites of the set of ends of $G$ and $C$ defined as the left adjoint of the preadditive Coyoneda object of $G$.
CategoryTheory.IsGrothendieckAbelian.tensorObjPreadditiveCoyonedaObjAdjunctiondefMathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu, function or constant
Wording
the tensor object preadditive Coyoneda object adjunction of G (from the name)
English
Let $G$ be an element of $C$. Then the tensor object preadditive Coyoneda object adjunction of $G$ is an adjunction of the tensor object of $G$ and the preadditive Coyoneda object of $G$ defined as the adjunction of the preadditive Coyoneda object of $G$.

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRingdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite, type
Wording
embedding ring of F (from the name)
English
Let $F$ be a functor of $D$ and the set of opposites of $C$. Then the embedding rings of $F$ are a basic type.
CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embeddingdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite, function or constant
Wording
the embedding of F (from the name)
English
Let $F$ be a functor of $D$ and the set of opposites of $C$. Then the embedding of $F$ is a functor of the set of opposites of $C$ and the set of module categories of the set of embedding rings of $F$.

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

CategoryTheory.IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISupdefMathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and $\operatorname{MonoOver}$ applied to $X$. Let $c$ be a cocone of the composition of $F$ and $\operatorname{forget}$ applied to $X$ such that $\operatorname{mk}$ applied to the homomorphism of $\operatorname{pt}$ applied to $c$ is equal to the supremum of the function that maps $j$ to $\operatorname{mk}$ applied to the homomorphism of the object of the action of $F$ and $j$. Then $\operatorname{isColimitMapCoconeOfSubobjectMkEqISup}$ applied to $F$, $c$ and $h_{3}$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of $\operatorname{forget}$ applied to $X$ and $c$.

Mathlib.CategoryTheory.Abelian.Images

CategoryTheory.Abelian.coimagedefMathlib.CategoryTheory.Abelian.Images, function or constant
Wording
the coimage of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $Q$. Then the coimage of $f$ is an element of $C$ defined as the cokernel of the inclusion of $f$.
CategoryTheory.Abelian.coimage.πdefMathlib.CategoryTheory.Abelian.Images, function or constant
Wording
the projection onto the coimage of f (from the docstring)
English
Let $f$ be a homomorphism of $P$ and $Q$. Then the projection onto the coimage of $f$ is a homomorphism of $P$ and the coimage of $f$ defined as the projection of the inclusion of $f$.
CategoryTheory.Abelian.coimageImageComparisondefMathlib.CategoryTheory.Abelian.Images, function or constant
Wording
the canonical map from the abelian coimage to the abelian image of f (from the docstring)
English
Let $f$ be a homomorphism of $P$ and $Q$. Then the canonical map from the abelian coimage to the abelian image of $f$ is a homomorphism of the coimage of $f$ and the image of $f$.
CategoryTheory.Abelian.coimageImageComparison'defMathlib.CategoryTheory.Abelian.Images, function or constant
Wording
the coimage image comparison of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $Q$. Then the coimage image comparison of $f$ is a homomorphism of the coimage of $f$ and the image of $f$.
CategoryTheory.Abelian.coimageImageComparisonFunctordefMathlib.CategoryTheory.Abelian.Images, function or constant
Wording
the coimage image comparison functor (from the name)
English
The coimage image comparison functor is a functor of the set of arrows of $C$ and the set of arrows of $C$.
CategoryTheory.Abelian.factorThruCoimagedefMathlib.CategoryTheory.Abelian.Images, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $P$ and $Q$. Then $\operatorname{factorThruCoimage}$ applied to $f$ is a homomorphism of the coimage of $f$ and $Q$ defined as $\operatorname{desc}$ applied to the inclusion of $f$, $f$ and $\operatorname{condition}$ applied to $f$.
CategoryTheory.Abelian.factorThruImagedefMathlib.CategoryTheory.Abelian.Images, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $P$ and $Q$. Then $\operatorname{factorThruImage}$ applied to $f$ is a homomorphism of $P$ and the image of $f$ defined as the lift of the projection of $f$ and $f$.
CategoryTheory.Abelian.imagedefMathlib.CategoryTheory.Abelian.Images, function or constant
Wording
the image of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $Q$. Then the image of $f$ is an element of $C$ defined as the kernel of the projection of $f$.
CategoryTheory.Abelian.image.ιdefMathlib.CategoryTheory.Abelian.Images, function or constant
Wording
the inclusion of the image into the codomain of f (from the docstring)
English
Let $f$ be a homomorphism of $P$ and $Q$. Then the inclusion of the image into the codomain of $f$ is a homomorphism of the image of $f$ and $Q$ defined as the inclusion of the projection of $f$.

Mathlib.CategoryTheory.Abelian.Injective.Dimension

CategoryTheory.HasInjectiveDimensionLEdefMathlib.CategoryTheory.Abelian.Injective.Dimension, predicate
Wording
no wording
English
Let $X$ be an element of $C$. Let $n$ be a natural number. Then $\operatorname{HasInjectiveDimensionLE}$ holds for $X$ and $n$, if $\operatorname{HasInjectiveDimensionLT}$ holds for $X$ and $n + 1$.
CategoryTheory.HasInjectiveDimensionLTclassMathlib.CategoryTheory.Abelian.Injective.Dimension, predicate
Wording
no wording
English
Let $X$ be an element of $C$. Let $n$ be a natural number. Then we can say that $\operatorname{HasInjectiveDimensionLT}$ holds for $X$ and $n$.
CategoryTheory.injectiveDimensiondefMathlib.CategoryTheory.Abelian.Injective.Dimension, function or constant
Wording
the injective dimension of X (from the docstring)
English
Let $X$ be an element of $C$. Then the injective dimension of $X$ is an element of $\mathrm{WithBot}$ applied to the set of natural numbers defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that for all natural numbers $i$, if $n < i$, then $\operatorname{HasInjectiveDimensionLT}$ holds for $X$ and $i$.

Mathlib.CategoryTheory.Abelian.Injective.Ext

CategoryTheory.InjectiveResolution.extAddEquivCohomologyClassdefMathlib.CategoryTheory.Abelian.Injective.Ext, function or constant
Wording
the extension additive equivalence cohomology class of R (from the name)
English
Let $R$ be an injective resolution of $Y$. Then the extension additive equivalence cohomology class of $R$ is an additive equivalence of the set of extensions of $Y$ and $n$ and the set of cohomology classes of the cochain complex of $R$ and $n$.
CategoryTheory.InjectiveResolution.extEquivCohomologyClassdefMathlib.CategoryTheory.Abelian.Injective.Ext, function or constant
Wording
the extension equivalence cohomology class of R (from the name)
English
Let $R$ be an injective resolution of $Y$. Then the extension equivalence cohomology class of $R$ is an equivalence from the set of extensions of $Y$ and $n$ to the set of cohomology classes of the cochain complex of $R$ and $n$.
CategoryTheory.InjectiveResolution.extLinearEquivCohomologyClassdefMathlib.CategoryTheory.Abelian.Injective.Ext, function or constant
Wording
the extension linear equivalence cohomology class of R (from the name)
English
Let $R$ be an injective resolution of $Y$. Then the extension linear equivalence cohomology class of $R$ is a linear equivalence of the set of extensions of $Y$ and $n$ and the set of cohomology classes of the cochain complex of $R$ and $n$.
CategoryTheory.InjectiveResolution.extMkdefMathlib.CategoryTheory.Abelian.Injective.Ext, function or constant
Wording
the extension of f and m (from the name)
English
Let $R$ be an injective resolution of $Y$. Let $f$ be a homomorphism of $X$ and $\operatorname{X}$ applied to $\operatorname{cocomplex}$ applied to $R$ and $n$. Let $m$ be a natural number such that $n + 1 = m$ and the composition of $f$ and $\operatorname{d}$ applied to $\operatorname{cocomplex}$ applied to $R$, $n$ and $m$ is equal to $0$. Then the extension of $f$ and $m$ is an extension of $Y$ and $n$.

Mathlib.CategoryTheory.Abelian.Injective.Extend

CategoryTheory.InjectiveResolution.Hom.hom'defMathlib.CategoryTheory.Abelian.Injective.Extend, function or constant
Wording
the homomorphism of x2 (from the name)
English
Let $x_{2}$ be a homomorphism of $\mathrm{R'}$ and $f$. Then the homomorphism of $x_{2}$ is a homomorphism of the cochain complex of $R$ and the cochain complex of $\mathrm{R'}$ defined as $\operatorname{extendMap}$ applied to the homomorphism of $x_{2}$ and $\operatorname{embeddingUpNat}$.
CategoryTheory.InjectiveResolution.cochainComplexdefMathlib.CategoryTheory.Abelian.Injective.Extend, function or constant
Wording
the cochain complex of R (from the name)
English
Let $R$ be an injective resolution of $X$. Then the cochain complex of $R$ is a cochain complex of $C$ and $\Integer$ defined as $\operatorname{extend}$ applied to $\operatorname{cocomplex}$ applied to $R$ and $\operatorname{embeddingUpNat}$.
CategoryTheory.InjectiveResolution.cochainComplexXIsodefMathlib.CategoryTheory.Abelian.Injective.Extend, function or constant
Wording
the cochain complex isomorphism of n and k (from the name)
English
Let $R$ be an injective resolution of $X$. Let $n$ be an integer. Let $k$ be a natural number such that $k = n$. Then the cochain complex isomorphism of $n$ and $k$ is an isomorphism of $\operatorname{X}$ applied to the cochain complex of $R$ and $n$ and $\operatorname{X}$ applied to $\operatorname{cocomplex}$ applied to $R$ and $k$ defined as $\operatorname{extendXIso}$ applied to $\operatorname{cocomplex}$ applied to $R$, $\operatorname{embeddingUpNat}$ and $h_{1}$.
CategoryTheory.InjectiveResolution.ι'defMathlib.CategoryTheory.Abelian.Injective.Extend, function or constant
Wording
the inclusion of R (from the name)
English
Let $R$ be an injective resolution of $X$. Then the inclusion of $R$ is a homomorphism of the action of the single functor of $C$ and $0$ and $X$ and the cochain complex of $R$.

Mathlib.CategoryTheory.Abelian.Injective.Resolution

CategoryTheory.InjectivePresentation.shortComplexdefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
the short complex of ip (from the name)
English
Let $\mathrm{ip}$ be an injective presentation of $X$. Then the short complex of $\mathrm{ip}$ is a short complex of $C$.
CategoryTheory.InjectiveResolution.descdefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $Z$ and $Y$. Let $I$ be an injective resolution of $Y$. Let $J$ be an injective resolution of $Z$. Then $\operatorname{desc}$ applied to $f$, $I$ and $J$ is a homomorphism of $\operatorname{cocomplex}$ applied to $J$ and $\operatorname{cocomplex}$ applied to $I$.
CategoryTheory.InjectiveResolution.descCompHomotopydefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $I$ be an injective resolution of $X$. Let $J$ be an injective resolution of $Y$. Let $K$ be an injective resolution of $Z$. Then $\operatorname{descCompHomotopy}$ applied to $f$, $g$, $I$, $J$ and $K$ is a homotopy of $\operatorname{desc}$ applied to the composition of $f$ and $g$, $K$ and $I$ and the composition of $\operatorname{desc}$ applied to $f$, $J$ and $I$ and $\operatorname{desc}$ applied to $g$, $K$ and $J$.
CategoryTheory.InjectiveResolution.descHomotopydefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $Y$ and $Z$. Let $g$ and $h$ be homomorphisms of $\operatorname{cocomplex}$ applied to $I$ and $\operatorname{cocomplex}$ applied to $J$ such that the composition of the inclusion of $I$ and $g$ is equal to the composition of the map of $\mathrm{CochainComplex\_\_single\_u2080\_}$ applied to $C$ and $f$ and the inclusion of $J$ and the composition of the inclusion of $I$ and $h$ is equal to the composition of the map of $\mathrm{CochainComplex\_\_single\_u2080\_}$ applied to $C$ and $f$ and the inclusion of $J$. Then $\operatorname{descHomotopy}$ applied to $f$, $g$, $h$, $\mathrm{g\_comm}$ and $\mathrm{h\_comm}$ is a homotopy of $g$ and $h$.
CategoryTheory.InjectiveResolution.descHomotopyZerodefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $\operatorname{cocomplex}$ applied to $I$ and $\operatorname{cocomplex}$ applied to $J$ such that the composition of the inclusion of $I$ and $f$ is equal to $0$. Then $\operatorname{descHomotopyZero}$ applied to $f$ and $\mathrm{comm}$ is a homotopy of $f$ and $0$.
CategoryTheory.InjectiveResolution.descIdHomotopydefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
the descent of the identity morphism of X and I (from the docstring)
English
Let $X$ be an element of $C$. Let $I$ be an injective resolution of $X$. Then the descent of the identity morphism of $X$ and $I$ is a homotopy of $\operatorname{desc}$ applied to the identity morphism of $X$, $I$ and $I$ and the identity morphism of $\operatorname{cocomplex}$ applied to $I$.
CategoryTheory.InjectiveResolution.homotopyEquivdefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
the homotopy equivalence of I and J (from the name)
English
Let $I$ and $J$ be injective resolutions of $X$. Then the homotopy equivalence of $I$ and $J$ is a homotopy equivalence of $\operatorname{cocomplex}$ applied to $I$ and $\operatorname{cocomplex}$ applied to $J$.
CategoryTheory.InjectiveResolution.isodefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
the isomorphism of I (from the name)
English
Let $I$ be an injective resolution of $X$. Then the isomorphism of $I$ is an isomorphism of the action of the injective resolution of $C$ and $X$ and the action of the quotient of $C$ and $\operatorname{up}$ applied to $\Natural$ and $\operatorname{cocomplex}$ applied to $I$ defined as the isomorphism of the homotopy equivalence of the injective resolution of $X$ and $I$.
CategoryTheory.InjectiveResolution.ofdefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
no wording
English
Let $Z$ be an element of $C$. Then $\operatorname{of}$ applied to $Z$ is an injective resolution of $Z$ defined as $\operatorname{proj0}$ applied to $\mathrm{CategoryTheory\_\_InjectiveResolution\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_CategoryTheory\_\_Abelian\_\_Injective\_\_Resolution\_\_4211954440\_\_\_hygCtx\_\_\_hyg\_\_8}$ and $Z$.
CategoryTheory.injectiveResolutiondefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
the injective resolution of Z (from the name)
English
Let $Z$ be an element of $C$. Then the injective resolution of $Z$ is an injective resolution of $Z$.
CategoryTheory.injectiveResolutionsdefMathlib.CategoryTheory.Abelian.Injective.Resolution, function or constant
Wording
the injective resolution of C (from the name)
English
Let $C$ be a set. Then the injective resolution of $C$ is a functor of $C$ and the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Natural$.

Mathlib.CategoryTheory.Abelian.LeftDerived

CategoryTheory.Functor.fromLeftDerivedZerodefMathlib.CategoryTheory.Abelian.LeftDerived, function or constant
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Then $\operatorname{fromLeftDerivedZero}$ applied to $F$ is a homomorphism of $\operatorname{leftDerived}$ applied to $F$ and $0$ and $F$.
CategoryTheory.Functor.leftDeriveddefMathlib.CategoryTheory.Abelian.LeftDerived, function or constant
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Let $n$ be a natural number. Then $\operatorname{leftDerived}$ applied to $F$ and $n$ is a functor of $C$ and $D$ defined as the composition of the left derived to homotopy category of $F$ and the homology functor of $\operatorname{down}$ applied to $\Natural$ and $n$.
CategoryTheory.Functor.leftDerivedToHomotopyCategorydefMathlib.CategoryTheory.Abelian.LeftDerived, function or constant
Wording
the left derived to homotopy category of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the left derived to homotopy category of $F$ is a functor of $C$ and the set of homotopy categories of $D$ and $\operatorname{down}$ applied to $\Natural$ defined as the composition of the projective resolution of $C$ and the map homotopy category of $F$ and $\operatorname{down}$ applied to $\Natural$.
CategoryTheory.Functor.leftDerivedZeroIsoSelfdefMathlib.CategoryTheory.Abelian.LeftDerived, function or constant
Wording
the canonical isomorphism of F (from the docstring)
English
Let $F$ be a functor of $C$ and $D$. Then the canonical isomorphism of $F$ is an isomorphism of $\operatorname{leftDerived}$ applied to $F$ and $0$ and $F$ defined as $\operatorname{asIso}$ applied to $\operatorname{fromLeftDerivedZero}$ applied to $F$.
CategoryTheory.NatTrans.leftDeriveddefMathlib.CategoryTheory.Abelian.LeftDerived, function or constant
Wording
no wording
English
Let $x_{4}$ be a homomorphism of $F$ and $G$. Let $n$ be a natural number. Then $\operatorname{leftDerived}$ applied to $x_{4}$ and $n$ is a homomorphism of $\operatorname{leftDerived}$ applied to $F$ and $n$ and $\operatorname{leftDerived}$ applied to $G$ and $n$ defined as the right whisker of the left derived to homotopy category of $x_{4}$ and the homology functor of $\operatorname{down}$ applied to $\Natural$ and $n$.
CategoryTheory.NatTrans.leftDerivedToHomotopyCategorydefMathlib.CategoryTheory.Abelian.LeftDerived, function or constant
Wording
the left derived to homotopy category of x4 (from the name)
English
Let $x_{4}$ be a homomorphism of $F$ and $G$. Then the left derived to homotopy category of $x_{4}$ is a homomorphism of the left derived to homotopy category of $F$ and the left derived to homotopy category of $G$ defined as the left whisker of the projective resolution of $C$ and the map homotopy category of $x_{4}$ and $\operatorname{down}$ applied to $\Natural$.
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'defMathlib.CategoryTheory.Abelian.LeftDerived, function or constant
Wording
no wording
English
Let $P$ be a projective resolution of $X$. Let $F$ be a functor of $C$ and $D$. Then $\operatorname{fromLeftDerivedZero'}$ applied to $P$ and $F$ is a homomorphism of $\operatorname{opcycles}$ applied to the action of the map homological complex of $F$ and $\operatorname{down}$ applied to $\Natural$ and the complex of $P$ and $0$ and the action of $F$ and $X$.
CategoryTheory.ProjectiveResolution.isoLeftDerivedObjdefMathlib.CategoryTheory.Abelian.LeftDerived, function or constant
Wording
the isomorphism left derived object of F and n (from the name)
English
Let $P$ be a projective resolution of $X$. Let $F$ be a functor of $C$ and $D$. Let $n$ be a natural number. Then the isomorphism left derived object of $F$ and $n$ is an isomorphism of the action of $\operatorname{leftDerived}$ applied to $F$ and $n$ and $X$ and the action of the homology functor of $\operatorname{down}$ applied to $\Natural$ and $n$ and the action of the map homological complex of $F$ and $\operatorname{down}$ applied to $\Natural$ and the complex of $P$ defined as the composition of the map isomorphism of the homology functor of $\operatorname{down}$ applied to $\Natural$ and $n$ and the isomorphism left derived to homotopy category object of $P$ and $F$ and the application of the homology functor factor of $\operatorname{down}$ applied to $\Natural$ and $n$ and the action of the map homological complex of $F$ and $\operatorname{down}$ applied to $\Natural$ and the complex of $P$.
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObjdefMathlib.CategoryTheory.Abelian.LeftDerived, function or constant
Wording
the isomorphism left derived to homotopy category object of P and F (from the name)
English
Let $P$ be a projective resolution of $X$. Let $F$ be a functor of $C$ and $D$. Then the isomorphism left derived to homotopy category object of $P$ and $F$ is an isomorphism of the action of the left derived to homotopy category of $F$ and $X$ and the action of the composition of the map homological complex of $F$ and $\operatorname{down}$ applied to $\Natural$ and the quotient of $D$ and $\operatorname{down}$ applied to $\Natural$ and the complex of $P$ defined as the composition of the map isomorphism of the map homotopy category of $F$ and $\operatorname{down}$ applied to $\Natural$ and the isomorphism of $P$ and the application of the map homotopy category factor of $F$ and $\operatorname{down}$ applied to $\Natural$ and the complex of $P$.

Mathlib.CategoryTheory.Abelian.NonPreadditive

CategoryTheory.NonPreadditiveAbelianclassMathlib.CategoryTheory.Abelian.NonPreadditive, predicate
Wording
no wording
English
Let $C$ be a set. Then we can say that $\operatorname{NonPreadditiveAbelian}$ holds for $C$.
CategoryTheory.NonPreadditiveAbelian.epiIsCokernelOfKerneldefMathlib.CategoryTheory.Abelian.NonPreadditive, function or constant
Wording
no wording
English
Let $s$ be a fork of $f$ and $0$. Let $h_{1}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{epiIsCokernelOfKernel}$ applied to $s$ and $h_{1}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{condition}$ applied to $s$.
CategoryTheory.NonPreadditiveAbelian.isColimitσdefMathlib.CategoryTheory.Abelian.NonPreadditive, function or constant
Wording
no wording
English
$\mathrm{CategoryTheory\_\_NonPreadditiveAbelian\_\_isColimit\_u3c3\_}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\mathrm{CategoryTheory\_\_NonPreadditiveAbelian\_\_\_u3c3\_}$ and $\mathrm{CategoryTheory\_\_NonPreadditiveAbelian\_\_diag\_\_u3c3\_}$.
CategoryTheory.NonPreadditiveAbelian.monoIsKernelOfCokerneldefMathlib.CategoryTheory.Abelian.NonPreadditive, function or constant
Wording
no wording
English
Let $s$ be a cofork of $f$ and $0$. Let $h_{1}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Then $\operatorname{monoIsKernelOfCokernel}$ applied to $s$ and $h_{1}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $\operatorname{condition}$ applied to $s$.
CategoryTheory.NonPreadditiveAbelian.rdefMathlib.CategoryTheory.Abelian.NonPreadditive, function or constant
Wording
no wording
English
Let $A$ be an element of $C$. Then $\operatorname{r}$ applied to $A$ is a homomorphism of $A$ and the cokernel of the diagonal of $A$ defined as the composition of the lift of the identity morphism of $A$ and $0$ and the projection of the diagonal of $A$.
CategoryTheory.NonPreadditiveAbelian.σdefMathlib.CategoryTheory.Abelian.NonPreadditive, function or constant
Wording
no wording
English
$\mathrm{CategoryTheory\_\_NonPreadditiveAbelian\_\_\_u3c3\_}$ is a homomorphism of the product of $A$ and $A$ and $A$ defined as the composition of the projection of the diagonal of $A$ and the inverse of $\operatorname{r}$ applied to $A$.

Mathlib.CategoryTheory.Abelian.Opposite

CategoryTheory.cokernelOpOpdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the cokernel of f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the cokernel of $f$ is an isomorphism of the cokernel of the opposite in $f$ and $\operatorname{op}$ applied to the kernel of $f$ defined as the inverse of the opposite isomorphism of the cokernel of $f$.
CategoryTheory.cokernelOpUnopdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the cokernel of f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the cokernel of $f$ is an isomorphism of the opposite of the cokernel of the opposite in $f$ and the kernel of $f$.
CategoryTheory.cokernelUnopOpdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the cokernel of g (from the docstring)
English
Let $g$ be a homomorphism of $A$ and $B$. Then the cokernel of $g$ is an isomorphism of $\operatorname{op}$ applied to the cokernel of the opposite of $g$ and the kernel of $g$ defined as the opposite isomorphism of the kernel of the opposite of $g$.
CategoryTheory.cokernelUnopUnopdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the cokernel of g (from the docstring)
English
Let $g$ be a homomorphism of $A$ and $B$. Then the cokernel of $g$ is an isomorphism of the cokernel of the opposite of $g$ and the opposite of the kernel of $g$ defined as the inverse of the opposite of the cokernel of $g$.
CategoryTheory.imageOpOpdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the opposite of the image of f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the opposite of the image of $f$ is an isomorphism of $\operatorname{op}$ applied to the categorical image of $f$ and the categorical image of the opposite in $f$ defined as the opposite of the image of the opposite in $f$.
CategoryTheory.imageOpUnopdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the image of f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the image of $f$ is an isomorphism of the opposite of the categorical image of the opposite in $f$ and the categorical image of $f$ defined as the opposite of the opposite of the image of the opposite in $f$.
CategoryTheory.imageUnopOpdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the opposite of the image of g (from the docstring)
English
Let $g$ be a homomorphism of $A$ and $B$. Then the opposite of the image of $g$ is an isomorphism of $\operatorname{op}$ applied to the categorical image of the opposite of $g$ and the categorical image of $g$.
CategoryTheory.imageUnopUnopdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the image of g (from the docstring)
English
Let $g$ be a homomorphism of $A$ and $B$. Then the image of $g$ is an isomorphism of the opposite of the categorical image of $g$ and the categorical image of the opposite of $g$ defined as the opposite of the opposite of the image of $g$.
CategoryTheory.kernelOpOpdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the kernel of f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the kernel of $f$ is an isomorphism of the kernel of the opposite in $f$ and $\operatorname{op}$ applied to the cokernel of $f$ defined as the inverse of the opposite isomorphism of the kernel of $f$.
CategoryTheory.kernelOpUnopdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the kernel of f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the kernel of $f$ is an isomorphism of the opposite of the kernel of the opposite in $f$ and the cokernel of $f$.
CategoryTheory.kernelUnopOpdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the kernel of g (from the docstring)
English
Let $g$ be a homomorphism of $A$ and $B$. Then the kernel of $g$ is an isomorphism of $\operatorname{op}$ applied to the kernel of the opposite of $g$ and the cokernel of $g$ defined as the opposite isomorphism of the cokernel of the opposite of $g$.
CategoryTheory.kernelUnopUnopdefMathlib.CategoryTheory.Abelian.Opposite, function or constant
Wording
the kernel of g (from the docstring)
English
Let $g$ be a homomorphism of $A$ and $B$. Then the kernel of $g$ is an isomorphism of the kernel of the opposite of $g$ and the opposite of the cokernel of $g$ defined as the inverse of the opposite of the kernel of $g$.

Mathlib.CategoryTheory.Abelian.Preradical.Basic

CategoryTheory.Abelian.PreradicaldefMathlib.CategoryTheory.Abelian.Preradical.Basic, type
Wording
preradical of C (from the name)
English
Let $C$ be a set. Then a preradical of $C$ is an element of the function that maps $C$ to $\operatorname{MonoOver}$ applied to the identity of $C$.
CategoryTheory.Abelian.Preradical.IsIdempotentclassMathlib.CategoryTheory.Abelian.Preradical.Basic, predicate
Wording
x1 is idempotent (from the name)
English
Let $x_{1}$ be a preradical of $C$. Then we can say that $x_{1}$ is idempotent.
CategoryTheory.Abelian.Preradical.rdefMathlib.CategoryTheory.Abelian.Preradical.Basic, function or constant
Wording
no wording
English
Let $x_{1}$ be a preradical of $C$. Then $\operatorname{r}$ applied to $x_{1}$ is a functor of $C$ and $C$ defined as the left of the object of $x_{1}$.
CategoryTheory.Abelian.Preradical.ιdefMathlib.CategoryTheory.Abelian.Preradical.Basic, function or constant
Wording
the inclusion of x1 (from the name)
English
Let $x_{1}$ be a preradical of $C$. Then the inclusion of $x_{1}$ is a homomorphism of $\operatorname{r}$ applied to $x_{1}$ and the identity of $C$ defined as the homomorphism of the object of $x_{1}$.

Mathlib.CategoryTheory.Abelian.Preradical.Colon

CategoryTheory.Abelian.Preradical.colondefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
the colon of x2 and x3 (from the name)
English
Let $x_{2}$ and $x_{3}$ be preradicals of $C$. Then the colon of $x_{2}$ and $x_{3}$ is a preradical of $C$ defined as $\operatorname{mk}$ applied to the first projection of the pullback of the canonical projection of $x_{2}$ and the composition of the left whisker of the quotient of $x_{2}$ and the inclusion of $x_{3}$ and the homomorphism of the right unitor of the quotient of $x_{2}$.
CategoryTheory.Abelian.Preradical.colonπdefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
the colon projection of x2 and x3 (from the name)
English
Let $x_{2}$ and $x_{3}$ be preradicals of $C$. Then the colon projection of $x_{2}$ and $x_{3}$ is a homomorphism of $\operatorname{r}$ applied to the colon of $x_{2}$ and $x_{3}$ and the composition of the quotient of $x_{2}$ and $\operatorname{r}$ applied to $x_{3}$ defined as the second projection of the pullback of the canonical projection of $x_{2}$ and the composition of the left whisker of the quotient of $x_{2}$ and the inclusion of $x_{3}$ and the homomorphism of the right unitor of the quotient of $x_{2}$.
CategoryTheory.Abelian.Preradical.isColimitCokernelCoforkdefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
the canonical cofork of x2 (from the docstring)
English
Let $x_{2}$ be a preradical of $C$. Then the canonical cofork of $x_{2}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the canonical projection of $x_{2}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_Preradical\_\_\_u3b9\_\_\_u3c0\_}$ applied to $x_{2}$ defined as $\operatorname{cokernelIsCokernel}$ applied to the inclusion of $x_{2}$.
CategoryTheory.Abelian.Preradical.isColimitCokernelCoforkObjdefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
no wording
English
Let $x_{2}$ be a preradical of $C$. Let $X$ be an element of $C$. Then $\operatorname{isColimitCokernelCoforkObj}$ applied to $x_{2}$ and $X$ is an element of $\operatorname{IsColimit}$ applied to the projection of the component of the canonical projection of $x_{2}$ and $X$ and $\mathrm{CategoryTheory\_\_Abelian\_\_Preradical\_\_\_u3b9\_\_\_u3c0\_\_app}$ applied to $x_{2}$ and $X$ defined as $\operatorname{gIsCokernel}$ applied to $\mathrm{CategoryTheory\_\_Abelian\_\_Preradical\_\_shortExact\_shortComplexObj}$ applied to $x_{2}$ and $X$.
CategoryTheory.Abelian.Preradical.isLimitKernelForkdefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
the kernel fork of x2 (from the docstring)
English
Let $x_{2}$ be a preradical of $C$. Then the kernel fork of $x_{2}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $x_{2}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_Preradical\_\_\_u3b9\_\_\_u3c0\_}$ applied to $x_{2}$ defined as $\operatorname{fIsKernel}$ applied to $\mathrm{CategoryTheory\_\_Abelian\_\_Preradical\_\_shortExact\_shortComplex}$ applied to $x_{2}$.
CategoryTheory.Abelian.Preradical.isLimitKernelForkObjdefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
no wording
English
Let $x_{2}$ be a preradical of $C$. Let $X$ be an element of $C$. Then $\operatorname{isLimitKernelForkObj}$ applied to $x_{2}$ and $X$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the component of the inclusion of $x_{2}$ and $X$ and $\mathrm{CategoryTheory\_\_Abelian\_\_Preradical\_\_\_u3b9\_\_\_u3c0\_\_app}$ applied to $x_{2}$ and $X$ defined as $\operatorname{fIsKernel}$ applied to $\mathrm{CategoryTheory\_\_Abelian\_\_Preradical\_\_shortExact\_shortComplexObj}$ applied to $x_{2}$ and $X$.
CategoryTheory.Abelian.Preradical.quotientdefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
the quotient of x2 (from the name)
English
Let $x_{2}$ be a preradical of $C$. Then the quotient of $x_{2}$ is a functor of $C$ and $C$ defined as the cokernel of the inclusion of $x_{2}$.
CategoryTheory.Abelian.Preradical.shortComplexdefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
the short complex of x2 (from the docstring)
English
Let $x_{2}$ be a preradical of $C$. Then the short complex of $x_{2}$ is a short complex of the set of functors of $C$ and $C$.
CategoryTheory.Abelian.Preradical.shortComplexObjdefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
the short complex object of x2 and X (from the name)
English
Let $x_{2}$ be a preradical of $C$. Let $X$ be an element of $C$. Then the short complex object of $x_{2}$ and $X$ is a short complex of $C$.
CategoryTheory.Abelian.Preradical.toColondefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
the colon of x2 and x3 (from the name)
English
Let $x_{2}$ and $x_{3}$ be preradicals of $C$. Then the colon of $x_{2}$ and $x_{3}$ is a homomorphism of $x_{2}$ and the colon of $x_{2}$ and $x_{3}$.
CategoryTheory.Abelian.Preradical.πdefMathlib.CategoryTheory.Abelian.Preradical.Colon, function or constant
Wording
the canonical projection of x2 (from the docstring)
English
Let $x_{2}$ be a preradical of $C$. Then the canonical projection of $x_{2}$ is a homomorphism of the identity of $C$ and the quotient of $x_{2}$ defined as the projection of the inclusion of $x_{2}$.

Mathlib.CategoryTheory.Abelian.Preradical.Radical

CategoryTheory.Abelian.Preradical.isRadicaldefMathlib.CategoryTheory.Abelian.Preradical.Radical, function or constant
Wording
no wording
English
Let $C$ be a set. Then there is an object property of the set of preradicals of $C$. Proof. Let $C$ be arbitrary. Let $x_{2}$ be arbitrary. By x2. By x2. By CategoryTheory__Abelian__Preradical__toColon. By CategoryTheory__IsIso.
CategoryTheory.Abelian.RadicaldefMathlib.CategoryTheory.Abelian.Preradical.Radical, type
Wording
radical of C (from the name)
English
Let $C$ be a set. Then a radical of $C$ is an element of the function that maps $C$ to the set of full subcategories of $\operatorname{isRadical}$ applied to $C$.

Mathlib.CategoryTheory.Abelian.Projective.Dimension

CategoryTheory.HasProjectiveDimensionLEdefMathlib.CategoryTheory.Abelian.Projective.Dimension, predicate
Wording
no wording
English
Let $X$ be an element of $C$. Let $n$ be a natural number. Then $\operatorname{HasProjectiveDimensionLE}$ holds for $X$ and $n$, if $\operatorname{HasProjectiveDimensionLT}$ holds for $X$ and $n + 1$.
CategoryTheory.HasProjectiveDimensionLTclassMathlib.CategoryTheory.Abelian.Projective.Dimension, predicate
Wording
no wording
English
Let $X$ be an element of $C$. Let $n$ be a natural number. Then we can say that $\operatorname{HasProjectiveDimensionLT}$ holds for $X$ and $n$.
CategoryTheory.projectiveDimensiondefMathlib.CategoryTheory.Abelian.Projective.Dimension, function or constant
Wording
the projective dimension of X (from the docstring)
English
Let $X$ be an element of $C$. Then the projective dimension of $X$ is an element of $\mathrm{WithBot}$ applied to the set of natural numbers defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that for all natural numbers $i$, if $n < i$, then $\operatorname{HasProjectiveDimensionLT}$ holds for $X$ and $i$.

Mathlib.CategoryTheory.Abelian.Projective.Ext

CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClassdefMathlib.CategoryTheory.Abelian.Projective.Ext, function or constant
Wording
the extension additive equivalence cohomology class of R (from the name)
English
Let $R$ be a projective resolution of $X$. Then the extension additive equivalence cohomology class of $R$ is an additive equivalence of the set of extensions of $Y$ and $n$ and the set of cohomology classes of the action of the single functor of $C$ and $0$ and $Y$ and $n$.
CategoryTheory.ProjectiveResolution.extEquivCohomologyClassdefMathlib.CategoryTheory.Abelian.Projective.Ext, function or constant
Wording
the extension equivalence cohomology class of R (from the name)
English
Let $R$ be a projective resolution of $X$. Then the extension equivalence cohomology class of $R$ is an equivalence from the set of extensions of $Y$ and $n$ to the set of cohomology classes of the action of the single functor of $C$ and $0$ and $Y$ and $n$.
CategoryTheory.ProjectiveResolution.extLinearEquivCohomologyClassdefMathlib.CategoryTheory.Abelian.Projective.Ext, function or constant
Wording
the extension linear equivalence cohomology class of R (from the name)
English
Let $R$ be a projective resolution of $X$. Then the extension linear equivalence cohomology class of $R$ is a linear equivalence of the set of extensions of $Y$ and $n$ and the set of cohomology classes of the action of the single functor of $C$ and $0$ and $Y$ and $n$.
CategoryTheory.ProjectiveResolution.extMkdefMathlib.CategoryTheory.Abelian.Projective.Ext, function or constant
Wording
the extension of f and m (from the name)
English
Let $R$ be a projective resolution of $X$. Let $f$ be a homomorphism of $\operatorname{X}$ applied to the complex of $R$ and $n$ and $Y$. Let $m$ be a natural number such that $n + 1 = m$ and the composition of $\operatorname{d}$ applied to the complex of $R$, $m$ and $n$ and $f$ is equal to $0$. Then the extension of $f$ and $m$ is an extension of $Y$ and $n$.

Mathlib.CategoryTheory.Abelian.Projective.Extend

CategoryTheory.ProjectiveResolution.Hom.hom'defMathlib.CategoryTheory.Abelian.Projective.Extend, function or constant
Wording
the homomorphism of x2 (from the name)
English
Let $x_{2}$ be a homomorphism of $\mathrm{R'}$ and $f$. Then the homomorphism of $x_{2}$ is a homomorphism of the cochain complex of $R$ and the cochain complex of $\mathrm{R'}$ defined as $\operatorname{extendMap}$ applied to the homomorphism of $x_{2}$ and $\operatorname{embeddingDownNat}$.
CategoryTheory.ProjectiveResolution.cochainComplexdefMathlib.CategoryTheory.Abelian.Projective.Extend, function or constant
Wording
the cochain complex of R (from the name)
English
Let $R$ be a projective resolution of $X$. Then the cochain complex of $R$ is a cochain complex of $C$ and $\Integer$ defined as $\operatorname{extend}$ applied to the complex of $R$ and $\operatorname{embeddingDownNat}$.
CategoryTheory.ProjectiveResolution.cochainComplexXIsodefMathlib.CategoryTheory.Abelian.Projective.Extend, function or constant
Wording
the cochain complex isomorphism of n and k (from the name)
English
Let $R$ be a projective resolution of $X$. Let $n$ be an integer. Let $k$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (\operatorname{neg} (k), n)$ and $\mathrm{CategoryTheory\_\_ProjectiveResolution\_\_cochainComplexXIso\_\_\_auto\_1}$. Then the cochain complex isomorphism of $n$ and $k$ is an isomorphism of $\operatorname{X}$ applied to the cochain complex of $R$ and $n$ and $\operatorname{X}$ applied to the complex of $R$ and $k$ defined as $\operatorname{extendXIso}$ applied to the complex of $R$, $\operatorname{embeddingDownNat}$ and $h_{1}$.
CategoryTheory.ProjectiveResolution.π'defMathlib.CategoryTheory.Abelian.Projective.Extend, function or constant
Wording
the projection of R (from the name)
English
Let $R$ be a projective resolution of $X$. Then the projection of $R$ is a homomorphism of the cochain complex of $R$ and the action of the single functor of $C$ and $0$ and $X$.

Mathlib.CategoryTheory.Abelian.Projective.Resolution

CategoryTheory.ProjectiveResolution.homotopyEquivdefMathlib.CategoryTheory.Abelian.Projective.Resolution, function or constant
Wording
the homotopy equivalence of P and Q (from the name)
English
Let $P$ and $Q$ be projective resolutions of $X$. Then the homotopy equivalence of $P$ and $Q$ is a homotopy equivalence of the complex of $P$ and the complex of $Q$.
CategoryTheory.ProjectiveResolution.isodefMathlib.CategoryTheory.Abelian.Projective.Resolution, function or constant
Wording
the isomorphism of P (from the name)
English
Let $P$ be a projective resolution of $X$. Then the isomorphism of $P$ is an isomorphism of the action of the projective resolution of $C$ and $X$ and the action of the quotient of $C$ and $\operatorname{down}$ applied to $\Natural$ and the complex of $P$ defined as the isomorphism of the homotopy equivalence of the projective resolution of $X$ and $P$.
CategoryTheory.ProjectiveResolution.liftdefMathlib.CategoryTheory.Abelian.Projective.Resolution, function or constant
Wording
the lift of P and Q (from the name)
English
Let $f$ be a homomorphism of $Y$ and $Z$. Let $P$ be a projective resolution of $Y$. Let $Q$ be a projective resolution of $Z$. Then the lift of $P$ and $Q$ is a homomorphism of the complex of $P$ and the complex of $Q$.
CategoryTheory.ProjectiveResolution.liftCompHomotopydefMathlib.CategoryTheory.Abelian.Projective.Resolution, function or constant
Wording
the lift composition homotopy of Q and R (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $P$ be a projective resolution of $X$. Let $Q$ be a projective resolution of $Y$. Let $R$ be a projective resolution of $Z$. Then the lift composition homotopy of $Q$ and $R$ is a homotopy of the lift of $P$ and $R$ and the composition of the lift of $P$ and $Q$ and the lift of $Q$ and $R$.
CategoryTheory.ProjectiveResolution.liftHomotopydefMathlib.CategoryTheory.Abelian.Projective.Resolution, function or constant
Wording
the lift homotopy of g and h (from the name)
English
Let $f$ be a homomorphism of $Y$ and $Z$. Let $g$ and $h$ be homomorphisms of the complex of $P$ and the complex of $Q$ such that the composition of $g$ and the projection of $Q$ is equal to the composition of the projection of $P$ and the map of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to $C$ and $f$ and the composition of $h$ and the projection of $Q$ is equal to the composition of the projection of $P$ and the map of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to $C$ and $f$. Then the lift homotopy of $g$ and $h$ is a homotopy of $g$ and $h$.
CategoryTheory.ProjectiveResolution.liftHomotopyZerodefMathlib.CategoryTheory.Abelian.Projective.Resolution, function or constant
Wording
the lift homotopy zero of f and comm (from the name)
English
Let $f$ be a homomorphism of the complex of $P$ and the complex of $Q$ such that the composition of $f$ and the projection of $Q$ is equal to $0$. Then the lift homotopy zero of $f$ and $\mathrm{comm}$ is a homotopy of $f$ and $0$.
CategoryTheory.ProjectiveResolution.liftIdHomotopydefMathlib.CategoryTheory.Abelian.Projective.Resolution, function or constant
Wording
the lift of the identity morphism of X and P (from the docstring)
English
Let $X$ be an element of $C$. Let $P$ be a projective resolution of $X$. Then the lift of the identity morphism of $X$ and $P$ is a homotopy of the lift of $P$ and $P$ and the identity morphism of the complex of $P$.
CategoryTheory.ProjectiveResolution.ofdefMathlib.CategoryTheory.Abelian.Projective.Resolution, function or constant
Wording
no wording
English
Let $Z$ be an element of $C$. Then $\operatorname{of}$ applied to $Z$ is a projective resolution of $Z$ defined as $\operatorname{proj0}$ applied to $\mathrm{CategoryTheory\_\_ProjectiveResolution\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_CategoryTheory\_\_Abelian\_\_Projective\_\_Resolution\_\_3679249917\_\_\_hygCtx\_\_\_hyg\_\_14}$ and $Z$.
CategoryTheory.projectiveResolutiondefMathlib.CategoryTheory.Abelian.Projective.Resolution, function or constant
Wording
the projective resolution of Z (from the name)
English
Let $Z$ be an element of $C$. Then the projective resolution of $Z$ is a projective resolution of $Z$ defined as $\operatorname{some}$ applied to $\operatorname{out}$.
CategoryTheory.projectiveResolutionsdefMathlib.CategoryTheory.Abelian.Projective.Resolution, function or constant
Wording
the projective resolution of C (from the name)
English
Let $C$ be a set. Then the projective resolution of $C$ is a functor of $C$ and the set of homotopy categories of $C$ and $\operatorname{down}$ applied to $\Natural$.

Mathlib.CategoryTheory.Abelian.Pseudoelements

CategoryTheory.Abelian.PseudoEqualdefMathlib.CategoryTheory.Abelian.Pseudoelements, predicate
Wording
f is a pseudo equal with respect to g (from the name)
English
Let $P$ be an element of $C$. Let $f$ and $g$ be elements of $\operatorname{Over}$ applied to $P$. Then $f$ is a pseudo equal with respect to $g$, if there exists an element $R$ of $C$, such that there exists a homomorphism $p$ of $R$ and the left subobject of $f$, such that there exists a homomorphism $q$ of $R$ and the left subobject of $g$, such that there exists an element $h$ of $\operatorname{Epi}$ applied to $p$, such that there exists an element $h_{1}$ of $\operatorname{Epi}$ applied to $q$, such that the composition of $p$ and the homomorphism of $f$ is equal to the composition of $q$ and the homomorphism of $g$.
CategoryTheory.Abelian.PseudoelementdefMathlib.CategoryTheory.Abelian.Pseudoelements, type
Wording
no wording
English
Let $P$ be an element of $C$. Then an element of $\operatorname{Pseudoelement}$ applied to $P$ is an element of the function that maps $P$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $P$.
CategoryTheory.Abelian.Pseudoelement.pseudoApplydefMathlib.CategoryTheory.Abelian.Pseudoelements, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $P$ and $Q$. Let $x_{2}$ be an element of $\operatorname{Pseudoelement}$ applied to $P$. Then $\operatorname{pseudoApply}$ applied to $f$ and $x_{2}$ is an element of $\operatorname{Pseudoelement}$ applied to $Q$ defined as the map of the function that maps $g$ to $\operatorname{Abelian}$ applied to $f$ and $g$ and $x_{2}$.
CategoryTheory.Abelian.Pseudoelement.pseudoZerodefMathlib.CategoryTheory.Abelian.Pseudoelements, function or constant
Wording
the pseudo zero (from the name)
English
The pseudo zero is an element of $\operatorname{Pseudoelement}$ applied to $P$ defined as $\operatorname{mk}$ applied to $\operatorname{setoid}$ applied to $P$ and $\operatorname{mk}$ applied to $0$.
CategoryTheory.Abelian.appdefMathlib.CategoryTheory.Abelian.Pseudoelements, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $P$ and $Q$. Let $a$ be an element of $\operatorname{Over}$ applied to $P$. Then $\operatorname{Abelian}$ applied to $f$ and $a$ is an element of $\operatorname{Over}$ applied to $Q$ defined as $\operatorname{mk}$ applied to the composition of the homomorphism of $a$ and $f$.

Mathlib.CategoryTheory.Abelian.RightDerived

CategoryTheory.Functor.rightDeriveddefMathlib.CategoryTheory.Abelian.RightDerived, function or constant
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Let $n$ be a natural number. Then $\operatorname{rightDerived}$ applied to $F$ and $n$ is a functor of $C$ and $D$ defined as the composition of the right derived to homotopy category of $F$ and the homology functor of $\operatorname{up}$ applied to $\Natural$ and $n$.
CategoryTheory.Functor.rightDerivedToHomotopyCategorydefMathlib.CategoryTheory.Abelian.RightDerived, function or constant
Wording
the right derived to homotopy category of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the right derived to homotopy category of $F$ is a functor of $C$ and the set of homotopy categories of $D$ and $\operatorname{up}$ applied to $\Natural$ defined as the composition of the injective resolution of $C$ and the map homotopy category of $F$ and $\operatorname{up}$ applied to $\Natural$.
CategoryTheory.Functor.rightDerivedZeroIsoSelfdefMathlib.CategoryTheory.Abelian.RightDerived, function or constant
Wording
the canonical isomorphism of F (from the docstring)
English
Let $F$ be a functor of $C$ and $D$. Then the canonical isomorphism of $F$ is an isomorphism of $\operatorname{rightDerived}$ applied to $F$ and $0$ and $F$ defined as the inverse of $\operatorname{asIso}$ applied to the right derived zero of $F$.
CategoryTheory.Functor.toRightDerivedZerodefMathlib.CategoryTheory.Abelian.RightDerived, function or constant
Wording
the right derived zero of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the right derived zero of $F$ is a homomorphism of $F$ and $\operatorname{rightDerived}$ applied to $F$ and $0$.
CategoryTheory.InjectiveResolution.isoRightDerivedObjdefMathlib.CategoryTheory.Abelian.RightDerived, function or constant
Wording
the isomorphism right derived object of F and n (from the name)
English
Let $I$ be an injective resolution of $X$. Let $F$ be a functor of $C$ and $D$. Let $n$ be a natural number. Then the isomorphism right derived object of $F$ and $n$ is an isomorphism of the action of $\operatorname{rightDerived}$ applied to $F$ and $n$ and $X$ and the action of the homology functor of $\operatorname{up}$ applied to $\Natural$ and $n$ and the action of the map homological complex of $F$ and $\operatorname{up}$ applied to $\Natural$ and $\operatorname{cocomplex}$ applied to $I$ defined as the composition of the map isomorphism of the homology functor of $\operatorname{up}$ applied to $\Natural$ and $n$ and the isomorphism right derived to homotopy category object of $I$ and $F$ and the application of the homology functor factor of $\operatorname{up}$ applied to $\Natural$ and $n$ and the action of the map homological complex of $F$ and $\operatorname{up}$ applied to $\Natural$ and $\operatorname{cocomplex}$ applied to $I$.
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObjdefMathlib.CategoryTheory.Abelian.RightDerived, function or constant
Wording
the isomorphism right derived to homotopy category object of I and F (from the name)
English
Let $I$ be an injective resolution of $X$. Let $F$ be a functor of $C$ and $D$. Then the isomorphism right derived to homotopy category object of $I$ and $F$ is an isomorphism of the action of the right derived to homotopy category of $F$ and $X$ and the action of the composition of the map homological complex of $F$ and $\operatorname{up}$ applied to $\Natural$ and the quotient of $D$ and $\operatorname{up}$ applied to $\Natural$ and $\operatorname{cocomplex}$ applied to $I$ defined as the composition of the map isomorphism of the map homotopy category of $F$ and $\operatorname{up}$ applied to $\Natural$ and the isomorphism of $I$ and the application of the map homotopy category factor of $F$ and $\operatorname{up}$ applied to $\Natural$ and $\operatorname{cocomplex}$ applied to $I$.
CategoryTheory.InjectiveResolution.toRightDerivedZero'defMathlib.CategoryTheory.Abelian.RightDerived, function or constant
Wording
the right derived zero of P and F (from the name)
English
Let $P$ be an injective resolution of $X$. Let $F$ be a functor of $C$ and $D$. Then the right derived zero of $P$ and $F$ is a homomorphism of the action of $F$ and $X$ and the cycle of the action of the map homological complex of $F$ and $\operatorname{up}$ applied to $\Natural$ and $\operatorname{cocomplex}$ applied to $P$ and $0$.
CategoryTheory.NatTrans.rightDeriveddefMathlib.CategoryTheory.Abelian.RightDerived, function or constant
Wording
no wording
English
Let $x_{4}$ be a homomorphism of $F$ and $G$. Let $n$ be a natural number. Then $\operatorname{rightDerived}$ applied to $x_{4}$ and $n$ is a homomorphism of $\operatorname{rightDerived}$ applied to $F$ and $n$ and $\operatorname{rightDerived}$ applied to $G$ and $n$ defined as the right whisker of the right derived to homotopy category of $x_{4}$ and the homology functor of $\operatorname{up}$ applied to $\Natural$ and $n$.
CategoryTheory.NatTrans.rightDerivedToHomotopyCategorydefMathlib.CategoryTheory.Abelian.RightDerived, function or constant
Wording
the right derived to homotopy category of x4 (from the name)
English
Let $x_{4}$ be a homomorphism of $F$ and $G$. Then the right derived to homotopy category of $x_{4}$ is a homomorphism of the right derived to homotopy category of $F$ and the right derived to homotopy category of $G$ defined as the left whisker of the injective resolution of $C$ and the map homotopy category of $x_{4}$ and $\operatorname{up}$ applied to $\Natural$.

Mathlib.CategoryTheory.Abelian.SerreClass.Basic

CategoryTheory.ObjectProperty.IsSerreClassclassMathlib.CategoryTheory.Abelian.SerreClass.Basic, predicate
Wording
no wording
English
Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsSerreClass}$ holds for $P$.

Mathlib.CategoryTheory.Abelian.SerreClass.Localization

CategoryTheory.ObjectProperty.SerreClassLocalization.fullyFaithfulWhiskeringLeftdefMathlib.CategoryTheory.Abelian.SerreClass.Localization, function or constant
Wording
the left fully faithful whiskering of L and P (from the name)
English
generation took over the time limit
CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeftdefMathlib.CategoryTheory.Abelian.SerreClass.Localization, function or constant
Wording
the left whiskering of L and P (from the name)
English
Let $L$ be a functor of $C$ and $D$. Let $P$ be an object property of $C$. Let $E$ be a set. Then the left whiskering of $L$ and $P$ is a functor of the set of exact functors of $D$ and $E$ and the set of exact functors of $C$ and $E$.

Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

CategoryTheory.ObjectProperty.epiModSerredefMathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty, function or constant
Wording
no wording
English
Let $P$ be an object property of $C$. Then there is a morphism property of $C$. Proof. Let $P$ be arbitrary. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $f$ be arbitrary. By f. By CategoryTheory__Limits__cokernel. By P.
CategoryTheory.ObjectProperty.isoModSerredefMathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty, function or constant
Wording
no wording
English
Let $P$ be an object property of $C$. Then there is a morphism property of $C$. Proof. Let $P$ be arbitrary. By P. By CategoryTheory__ObjectProperty__monoModSerre. By P. By CategoryTheory__ObjectProperty__epiModSerre. By Min__min.
CategoryTheory.ObjectProperty.monoModSerredefMathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty, function or constant
Wording
no wording
English
Let $P$ be an object property of $C$. Then there is a morphism property of $C$. Proof. Let $P$ be arbitrary. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $f$ be arbitrary. By f. By CategoryTheory__Limits__kernel. By P.

Mathlib.CategoryTheory.Abelian.Subobject

CategoryTheory.Abelian.subobjectIsoSubobjectOpdefMathlib.CategoryTheory.Abelian.Subobject, function or constant
Wording
the subobject isomorphism subobject opposite of X (from the name)
English
Let $X$ be an element of $C$. Then the subobject isomorphism subobject opposite of $X$ is an order isomorphism of the set of subobjects of $X$ and the set of order duals of the set of subobjects of $\operatorname{op}$ applied to $X$.

Mathlib.CategoryTheory.Abelian.TorsionTheory.Basic

CategoryTheory.Abelian.IsTorsionClassclassMathlib.CategoryTheory.Abelian.TorsionTheory.Basic, predicate
Wording
P is a torsion class (from the name)
English
Let $P$ be an object property of $C$. Then we can say that $P$ is a torsion class.
CategoryTheory.Abelian.IsTorsionFreeClassclassMathlib.CategoryTheory.Abelian.TorsionTheory.Basic, predicate
Wording
P is a torsion free class (from the name)
English
Let $P$ be an object property of $C$. Then we can say that $P$ is a torsion free class.
CategoryTheory.Abelian.TorsionTheorystructureMathlib.CategoryTheory.Abelian.TorsionTheory.Basic, predicate
Wording
no wording
English
Let $T$ and $F$ be object properties of $C$. Then we can say that $\operatorname{TorsionTheory}$ holds for $T$ and $F$.

Mathlib.CategoryTheory.Action

CategoryTheory.ActionCategorydefMathlib.CategoryTheory.Action, type
Wording
action category of M and X (from the name)
English
Let $M$ and $X$ be sets. Then an action category of $M$ and $X$ is an element of the function that maps $M$ and $X$ to the set of elements of the action as functor of $M$ and $X$.
CategoryTheory.ActionCategory.backdefMathlib.CategoryTheory.Action, function or constant
Wording
no wording
English
Let $x_{2}$ be an action category of $M$ and $X$. Then $\operatorname{back}$ applied to $x_{2}$ is an element of $X$ defined as the value of the element of $x_{2}$.
CategoryTheory.ActionCategory.casesdefMathlib.CategoryTheory.Action, function or constant
Wording
the case of hyp and t (from the name)
English
Let $\mathrm{hyp}$ be a function from elements $t$ of $X$ and elements $g$ of $G$ to elements of $P$ applied to the element of $\operatorname{unit}$ and $\HSMulhSMulMACRoAL {\operatorname{inv} (g)}{t}$, the element of $\operatorname{unit}$ and $t$ and the homomorphism of $t$ and $g$. Let $f$ be a homomorphism of $a$ and $b$. Then the case of $t$ and $g$ is an element of $P$ applied to $a$, $b$ and $f$.
CategoryTheory.ActionCategory.currydefMathlib.CategoryTheory.Action, function or constant
Wording
the curry of F (from the name)
English
Let $F$ be a functor of the set of action categories of $G$ and $X$ and the set of single objects of $H$. Then the curry of $F$ is a monoid homomorphism of $G$ and the set of semidirect products of $G$ and the multiplicative automorphism arrow.
CategoryTheory.ActionCategory.endMulEquivSubgroupdefMathlib.CategoryTheory.Action, function or constant
Wording
the end multiplicative equivalence subgroup of H (from the name)
English
Let $H$ be a subgroup of $G$. Then the end multiplicative equivalence subgroup of $H$ is a multiplicative equivalence of the set of ends of $\operatorname{objEquiv}$ applied to $G$, the set of quotients of $G$ and $H$ and $\operatorname{mk}$ applied to $1$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ defined as the composition of the inverse of the stabilizer of $G$ and $\operatorname{mk}$ applied to $1$ and the subgroup congruence of $\mathrm{MulAction\_\_stabilizer\_quotient}$ applied to $H$.
CategoryTheory.ActionCategory.homOfPairdefMathlib.CategoryTheory.Action, function or constant
Wording
the homomorphism of t and g (from the name)
English
Let $t$ be an element of $X$. Let $g$ be an element of $G$. Then the homomorphism of $t$ and $g$ is a homomorphism of the element of $\operatorname{unit}$ and $\HSMulhSMulMACRoAL {\operatorname{inv} (g)}{t}$ and the element of $\operatorname{unit}$ and $t$ defined as the homomorphism of $g$ and $\mathrm{smul\_inv\_smul}$ applied to $g$ and $t$.
CategoryTheory.ActionCategory.objEquivdefMathlib.CategoryTheory.Action, function or constant
Wording
the object equivalence of M and X (from the name)
English
Let $M$ and $X$ be sets. Then the object equivalence of $M$ and $X$ is an equivalence from $X$ to the set of action categories of $M$ and $X$ defined as $\operatorname{mk}$ applied to the function that maps $x_{2}$ to the element of $\operatorname{unit}$ and $x_{2}$, the function that maps $x_{3}$ to $\operatorname{back}$ applied to $x_{3}$, $\mathrm{CategoryTheory\_\_ActionCategory\_\_coe\_back}$ and $\mathrm{CategoryTheory\_\_ActionCategory\_\_back\_coe}$.
CategoryTheory.ActionCategory.stabilizerIsoEnddefMathlib.CategoryTheory.Action, function or constant
Wording
the stabilizer of M and x2 (from the docstring)
English
Let $M$ be a set. Let $x_{2}$ be an element of $X$. Then the stabilizer of $M$ and $x_{2}$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{stabilizerSubmonoid} (M , x_{2})}{x_{3}})}$ and the set of ends of the element of $\operatorname{unit}$ and $x_{2}$.
CategoryTheory.ActionCategory.uncurrydefMathlib.CategoryTheory.Action, function or constant
Wording
no wording
English
Let $F$ be a monoid homomorphism of $G$ and the set of semidirect products of $G$ and the multiplicative automorphism arrow such that for all elements $g$ of $G$, the right of $F$ applied to $g$ is equal to $g$. Then $\operatorname{uncurry}$ applied to $F$ and $\mathrm{sane}$ is a functor of the set of action categories of $G$ and $X$ and the set of single objects of $H$.
CategoryTheory.ActionCategory.πdefMathlib.CategoryTheory.Action, function or constant
Wording
the projection of M and X (from the name)
English
Let $M$ and $X$ be sets. Then the projection of $M$ and $X$ is a functor of the set of action categories of $M$ and $X$ and the set of single objects of $M$ defined as the projection of the action as functor of $M$ and $X$.
CategoryTheory.actionAsFunctordefMathlib.CategoryTheory.Action, function or constant
Wording
the action as functor of M and X (from the name)
English
Let $M$ and $X$ be sets. Then the action as functor of $M$ and $X$ is a functor of the set of single objects of $M$ and the set of sets.

Mathlib.CategoryTheory.Action.Basic

ActionstructureMathlib.CategoryTheory.Action.Basic, type
Wording
action of V and G (from the name)
English
Let $V$ and $G$ be sets. Then the actions of $V$ and $G$ are a basic type.
Action.HomstructureMathlib.CategoryTheory.Action.Basic, type
Wording
homomorphism of M and N (from the name)
English
Let $M$ and $N$ be actions of $V$ and $G$. Then the homomorphisms of $M$ and $N$ are a basic type.
Action.Hom.compdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the composition of two of p and q (from the docstring)
English
Let $p$ be a homomorphism of $M$ and $N$. Let $q$ be a homomorphism of $N$ and $K$. Then the composition of two of $p$ and $q$ is a homomorphism of $M$ and $K$.
Action.Hom.homdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $M$ and $N$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of $\operatorname{V}$ applied to $M$ and $\operatorname{V}$ applied to $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Action.Hom.iddefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the identity of M (from the name)
English
Let $M$ be an action of $V$ and $G$. Then the identity of $M$ is a homomorphism of $M$ and $M$.
Action.HomSubtypedefMathlib.CategoryTheory.Action.Basic, type
Wording
homomorphism subtype of M and N (from the name)
English
Let $V$ and $G$ be sets. Let $M$ and $N$ be actions of $V$ and $G$. Then a homomorphism subtype of $M$ and $N$ is an element of the function that maps $V$, $G$, $M$ and $N$ to $\SubtypeSet {f}{\mathrm{forall} (G , \lambda g . \EqtMACRoH {\operatorname{comp} (\operatorname{coe} (f), \operatorname{coe} (\operatorname{hom} (\operatorname{asHom} (\mathrm{Action\_\_\_u3c1\_\_\_app} (M , g)))))}{\operatorname{comp} (\operatorname{coe} (\operatorname{hom} (\operatorname{asHom} (\mathrm{Action\_\_\_u3c1\_\_\_app} (N , g)))), \operatorname{coe} (f))})}$.
Action.VdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an action of $V$ and $G$. Then $\operatorname{V}$ applied to $\mathrm{self}$ is an element of $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Action.actionPUnitEquivalencedefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the action unit equivalence (from the name)
English
The action unit equivalence is an equivalence of the set of actions of $V$ and $\mathrm{PUnit}$ and $V$.
Action.forgetdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
no wording
English
Let $V$ and $G$ be sets. Then $\operatorname{forget}$ applied to $V$ and $G$ is a functor of the set of actions of $V$ and $G$ and $V$.
Action.functorCategoryEquivalencedefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the functor category equivalence of V and G (from the name)
English
Let $V$ and $G$ be sets. Then the functor category equivalence of $V$ and $G$ is an equivalence of the set of actions of $V$ and $G$ and the set of functors of the set of single objects of $G$ and $V$.
Action.functorCategoryEquivalenceCompEvaluationdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the forgetful functor of V and G (from the docstring)
English
Let $V$ and $G$ be sets. Then the forgetful functor of $V$ and $G$ is an isomorphism of the composition of the functor of the functor category equivalence of $V$ and $G$ and the action of the evaluation of the set of single objects of $G$ and $V$ and $\operatorname{unit}$ and $\operatorname{forget}$ applied to $V$ and $G$ defined as the identity of the composition of the functor of the functor category equivalence of $V$ and $G$ and the action of the evaluation of the set of single objects of $G$ and $V$ and $\operatorname{unit}$.
Action.mkIsodefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the isomorphism of f and comm (from the name)
English
Let $f$ be an isomorphism of $\operatorname{V}$ applied to $M$ and $\operatorname{V}$ applied to $N$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $g$ of $G$, the composition of $\operatorname{asHom}$ applied to $\mathrm{Action\_\_\_u3c1\_\_\_app}$ applied to $M$ and $g$ and the homomorphism of $f$ is equal to the composition of the homomorphism of $f$ and $\operatorname{asHom}$ applied to $\mathrm{Action\_\_\_u3c1\_\_\_app}$ applied to $N$ and $g$ and $\mathrm{Action\_\_mkIso\_\_\_auto\_1}$. Then the isomorphism of $f$ and $\mathrm{comm}$ is an isomorphism of $M$ and $N$.
Action.resdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the restriction of V and f (from the name)
English
Let $V$ be a set. Let $f$ be a monoid homomorphism of $G$ and $H$. Then the restriction of $V$ and $f$ is a functor of the set of actions of $V$ and $H$ and the set of actions of $V$ and $G$.
Action.resCompdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the restriction composition of f and g (from the name)
English
Let $V$ be a set. Let $f$ be a monoid homomorphism of $G$ and $H$. Let $g$ be a monoid homomorphism of $H$ and $K$. Then the restriction composition of $f$ and $g$ is an isomorphism of the composition of the restriction of $V$ and $g$ and the restriction of $V$ and $f$ and the restriction of $V$ and the composition of $g$ and $f$.
Action.resCongrdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the restriction congruence of V and h (from the name)
English
Let $V$ be a set. Assume that $\EqtMACRoH {f}{\mathrm{f'}}$. Then the restriction congruence of $V$ and $h$ is an isomorphism of the restriction of $V$ and $f$ and the restriction of $V$ and $\mathrm{f'}$.
Action.resEquivdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the restriction equivalence of V and f (from the name)
English
Let $V$ be a set. Let $f$ be a multiplicative equivalence of $G$ and $H$. Then the restriction equivalence of $V$ and $f$ is an equivalence of the set of actions of $V$ and $H$ and the set of actions of $V$ and $G$.
Action.resIddefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the restriction identity of V (from the name)
English
Let $V$ be a set. Then the restriction identity of $V$ is an isomorphism of the restriction of $V$ and the identity map of $G$ and the identity of the set of actions of $V$ and $G$.
Action.trivialdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
no wording
English
Let $G$ be a set. Let $X$ be an element of $V$. Then $\operatorname{trivial}$ applied to $G$ and $X$ is an action of $V$ and $G$ defined as $\operatorname{mk}$ applied to $X$ and $1$.
Action.ρdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an action of $V$ and $G$. Then $\mathrm{Action\_\_\_u3c1\_}$ applied to $\mathrm{self}$ is a monoid homomorphism of $G$ and the set of ends of $\operatorname{V}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
Action.ρAutdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the automorphism of A (from the name)
English
Let $A$ be an action of $V$ and $G$. Then the automorphism of $A$ is a monoid homomorphism of $G$ and the set of automorphisms of $\operatorname{V}$ applied to $A$.
CategoryTheory.Equivalence.mapActiondefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the map action of G and E (from the name)
English
Let $G$ be a set. Let $E$ be an equivalence of $V$ and $W$. Then the map action of $G$ and $E$ is an equivalence of the set of actions of $V$ and $G$ and the set of actions of $W$ and $G$.
CategoryTheory.Functor.FullyFaithful.mapActiondefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the map action of h and G (from the name)
English
Let $h$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Let $G$ be a set. Then the map action of $h$ and $G$ is an element of $\operatorname{FullyFaithful}$ applied to the map action of $F$ and $G$.
CategoryTheory.Functor.mapActiondefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the map action of F and G (from the name)
English
Let $F$ be a functor of $V$ and $W$. Let $G$ be a set. Then the map action of $F$ and $G$ is a functor of the set of actions of $V$ and $G$ and the set of actions of $W$ and $G$.
CategoryTheory.Functor.mapActionCompdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the map action composition of F and #3 (from the name)
English
Let $G$ be a set. Let $F$ be a functor of $V$ and $W$. Let $\mathrm{F'}$ be a functor of $W$ and $T$. Then the map action composition of $F$ and $\mathrm{F'}$ is an isomorphism of the map action of the composition of $F$ and $\mathrm{F'}$ and $G$ and the composition of the map action of $F$ and $G$ and the map action of $\mathrm{F'}$ and $G$.
CategoryTheory.Functor.mapActionCongrdefMathlib.CategoryTheory.Action.Basic, function or constant
Wording
the map action congruence of G and e (from the name)
English
Let $G$ be a set. Let $e$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the map action congruence of $G$ and $e$ is an isomorphism of the map action of $F$ and $G$ and the map action of $\mathrm{F'}$ and $G$.

Mathlib.CategoryTheory.Action.Concrete

Action.FintypeCat.ofMulActiondefMathlib.CategoryTheory.Action.Concrete, function or constant
Wording
the finite type category of G and H (from the name)
English
Let $G$ be a set. Let $H$ be a finite type category. Then the finite type category of $G$ and $H$ is an action of the set of finite type categories and $G$ defined as $\operatorname{mk}$ applied to $H$ and the composition of the monoid homomorphism of the inverse of the end equivalence and the composition of the monoid homomorphism of the end equivalence of the object of $H$ and the end homomorphism.
Action.FintypeCat.quotientToEndHomdefMathlib.CategoryTheory.Action.Concrete, function or constant
Wording
the quotient to end homomorphism of H and N (from the name)
English
Let $H$ and $N$ be subgroups of $G$. Then the quotient to end homomorphism of $H$ and $N$ is a monoid homomorphism of the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ and the subgroup of $N$ and $H$ and the set of ends of the finite type category of $G$ and $\operatorname{of}$ applied to the set of quotients of $G$ and $N$.
Action.FintypeCat.quotientToQuotientOfLEdefMathlib.CategoryTheory.Action.Concrete, function or constant
Wording
the quotient to quotient of H and N (from the name)
English
Let $H$ and $N$ be subgroups of $G$ such that $N \leq H$. Then the quotient to quotient of $H$ and $N$ is a homomorphism of the finite type category of $G$ and $\operatorname{of}$ applied to the set of quotients of $G$ and $N$ and the finite type category of $G$ and $\operatorname{of}$ applied to the set of quotients of $G$ and $H$.
Action.FintypeCat.toEndHomdefMathlib.CategoryTheory.Action.Concrete, function or constant
Wording
the end homomorphism of N (from the name)
English
Let $N$ be a subgroup of $G$. Then the end homomorphism of $N$ is a monoid homomorphism of $G$ and the set of ends of the finite type category of $G$ and $\operatorname{of}$ applied to the set of quotients of $G$ and $N$.
Action.diagonaldefMathlib.CategoryTheory.Action.Concrete, function or constant
Wording
the diagonal of G and n (from the name)
English
Let $G$ be a set. Let $n$ be a natural number. Then the diagonal of $G$ and $n$ is an action of the set of sets and $G$ defined as the action of $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$.
Action.diagonalOneIsoLeftRegulardefMathlib.CategoryTheory.Action.Concrete, function or constant
Wording
the diagonal one isomorphism left regular of G (from the name)
English
Let $G$ be a set. Then the diagonal one isomorphism left regular of $G$ is an isomorphism of the diagonal of $G$ and $1$ and the left regular of $G$.
Action.leftRegulardefMathlib.CategoryTheory.Action.Concrete, function or constant
Wording
the left regular of G (from the name)
English
Let $G$ be a set. Then the left regular of $G$ is an action of the set of sets and $G$ defined as the action of $G$ and $G$.
Action.ofMulActiondefMathlib.CategoryTheory.Action.Concrete, function or constant
Wording
the action of G and H (from the name)
English
Let $G$ and $H$ be sets. Then the action of $G$ and $H$ is an action of the set of sets and $G$ defined as $\operatorname{mk}$ applied to $H$ and the composition of the monoid homomorphism of the end equivalence of $H$ and the end homomorphism.
Action.ofMulActionLimitConedefMathlib.CategoryTheory.Action.Concrete, function or constant
Wording
the action of G and F (from the name)
English
Let $G$ be a set. Let $F$ be a function from elements of $x$ to sets. Then the action of $G$ and $F$ is a limit cone of the functor of the function that maps $i$ to the action of $G$ and $F$ applied to $i$.
TypeCat.endEquivdefMathlib.CategoryTheory.Action.Concrete, function or constant
Wording
the end equivalence of X (from the name)
English
Let $X$ be a set. Then the end equivalence of $X$ is a multiplicative equivalence of the set of ends of $X$ and the set of ends of $X$.

Mathlib.CategoryTheory.Action.Continuous

Action.IsContinuousdefMathlib.CategoryTheory.Action.Continuous, predicate
Wording
X is continuous (from the name)
English
Let $X$ be an action of $V$ and $G$. Then $X$ is continuous, if $\mathrm{ContinuousSMul}$ holds for $G$ and the set of carriers of the action of the forgetful functor of the set of actions of $V$ and $G$ and the set of topological categories and $X$.
Action.isContinuousdefMathlib.CategoryTheory.Action.Continuous, function or constant
Wording
no wording
English
Let $V$ and $G$ be sets. Then there is an object property of the set of actions of $V$ and $G$. Proof. Let $V$ be arbitrary. Let $G$ be arbitrary. By Action__IsContinuous.
CategoryTheory.Equivalence.mapContActiondefMathlib.CategoryTheory.Action.Continuous, function or constant
Wording
the map continuous action of E (from the name)
English
Let $G$ be a set. Let $E$ be an equivalence of $V$ and $W$ such that for all continuous actions $X_{1}$ of $V$ and $G$, the action of the map action of the functor of $E$ and $G$ and the object of $X_{1}$ is continuous and for all continuous actions $X$ of $W$ and $G$, the action of the map action of the inverse of $E$ and $G$ and the object of $X$ is continuous. Then the map continuous action of $E$ is an equivalence of the set of continuous actions of $V$ and $G$ and the set of continuous actions of $W$ and $G$.
CategoryTheory.Functor.mapContActiondefMathlib.CategoryTheory.Action.Continuous, function or constant
Wording
the map continuous action of F (from the name)
English
Let $G$ be a set. Let $F$ be a functor of $V$ and $W$ such that for all continuous actions $X$ of $V$ and $G$, the action of the map action of $F$ and $G$ and the object of $X$ is continuous. Then the map continuous action of $F$ is a functor of the set of continuous actions of $V$ and $G$ and the set of continuous actions of $W$ and $G$ defined as the lift of $\operatorname{isContinuous}$ applied to $W$ and $G$ and the composition of the inclusion of $\operatorname{isContinuous}$ applied to $V$ and $G$ and the map action of $F$ and $G$.
CategoryTheory.Functor.mapContActionCompdefMathlib.CategoryTheory.Action.Continuous, function or constant
Wording
the map continuous action composition of F and #4 (from the name)
English
Let $G$ be a set. Let $F$ be a functor of $V$ and $W$ such that for all continuous actions $X_{2}$ of $V$ and $G$, the action of the map action of $F$ and $G$ and the object of $X_{2}$ is continuous. Let $\mathrm{F'}$ be a functor of $W$ and $T$ such that for all continuous actions $X_{1}$ of $W$ and $G$, the action of the map action of $\mathrm{F'}$ and $G$ and the object of $X_{1}$ is continuous. Then the map continuous action composition of $F$ and $\mathrm{F'}$ is an isomorphism of the map continuous action of the composition of $F$ and $\mathrm{F'}$ and the composition of the map continuous action of $F$ and the map continuous action of $\mathrm{F'}$.
CategoryTheory.Functor.mapContActionCongrdefMathlib.CategoryTheory.Action.Continuous, function or constant
Wording
the map continuous action congruence of e (from the name)
English
Let $G$ be a set. Let $e$ be an isomorphism of $F$ and $\mathrm{F'}$. Assume that for all continuous actions $X_{1}$ of $V$ and $G$, the action of the map action of $F$ and $G$ and the object of $X_{1}$ is continuous. Assume that for all continuous actions $X$ of $V$ and $G$, the action of the map action of $\mathrm{F'}$ and $G$ and the object of $X$ is continuous. Then the map continuous action congruence of $e$ is an isomorphism of the map continuous action of $F$ and the map continuous action of $\mathrm{F'}$.
ContActiondefMathlib.CategoryTheory.Action.Continuous, type
Wording
continuous action of V and G (from the name)
English
Let $V$ and $G$ be sets. Then a continuous action of $V$ and $G$ is an element of the function that maps $V$ and $G$ to the set of full subcategories of $\operatorname{isContinuous}$ applied to $V$ and $G$.
ContAction.IsDiscretedefMathlib.CategoryTheory.Action.Continuous, predicate
Wording
X is discrete (from the name)
English
Let $X$ be a continuous action of $V$ and $G$. Then $X$ is discrete, if the set of carriers of the action of the forgetful functor of the set of continuous actions of $V$ and $G$ and the set of topological categories and $X$ is discrete.
ContAction.resdefMathlib.CategoryTheory.Action.Continuous, function or constant
Wording
the restriction of V and f (from the name)
English
Let $V$ be a set. Let $f$ be a continuous monoid homomorphism of $G$ and $H$. Then the restriction of $V$ and $f$ is a functor of the set of continuous actions of $V$ and $H$ and the set of continuous actions of $V$ and $G$.
ContAction.resCompdefMathlib.CategoryTheory.Action.Continuous, function or constant
Wording
the restriction composition of f and h (from the name)
English
Let $V$ be a set. Let $f$ be a continuous monoid homomorphism of $G$ and $H$. Let $h$ be a continuous monoid homomorphism of $H$ and $K$. Then the restriction composition of $f$ and $h$ is an isomorphism of the restriction of $V$ and the composition of $h$ and $f$ and the composition of the restriction of $V$ and $h$ and the restriction of $V$ and $f$.
ContAction.resCongrdefMathlib.CategoryTheory.Action.Continuous, function or constant
Wording
the restriction congruence of f and h (from the name)
English
Let $V$ be a set. Let $f$ and $\mathrm{f'}$ be continuous monoid homomorphisms of $G$ and $H$ such that $\EqtMACRoH {f}{\mathrm{f'}}$. Then the restriction congruence of $f$ and $\mathrm{f'}$ is an isomorphism of the restriction of $V$ and $f$ and the restriction of $V$ and $\mathrm{f'}$.
ContAction.resEquivdefMathlib.CategoryTheory.Action.Continuous, function or constant
Wording
the restriction equivalence of V and f (from the name)
English
Let $V$ be a set. Let $f$ be a continuous multiplicative equivalence of $G$ and $H$. Then the restriction equivalence of $V$ and $f$ is an equivalence of the set of continuous actions of $V$ and $H$ and the set of continuous actions of $V$ and $G$.
DiscreteContActiondefMathlib.CategoryTheory.Action.Continuous, type
Wording
discrete continuous action of V and G (from the name)
English
Let $V$ and $G$ be sets. Then a discrete continuous action of $V$ and $G$ is an element of the function that maps $V$ and $G$ to the set of full subcategories of the proposition that $\operatorname{IsDiscrete}$.

Mathlib.CategoryTheory.Action.Monoidal

Action.diagonalSuccIsoTensorDiagonaldefMathlib.CategoryTheory.Action.Monoidal, function or constant
Wording
the diagonal successor isomorphism tensor diagonal of G and n (from the name)
English
Let $G$ be a set. Let $n$ be a natural number. Then the diagonal successor isomorphism tensor diagonal of $G$ and $n$ is an isomorphism of the diagonal of $G$ and $n + 1$ and the tensor object of the left regular of $G$ and the diagonal of $G$ and $n$.
Action.diagonalSuccIsoTensorTrivialdefMathlib.CategoryTheory.Action.Monoidal, function or constant
Wording
no wording
English
Let $G$ be a set. Let $n$ be a natural number. Then $\operatorname{diagonalSuccIsoTensorTrivial}$ applied to $G$ and $n$ is an isomorphism of the diagonal of $G$ and $n + 1$ and the tensor object of the left regular of $G$ and $\operatorname{trivial}$ applied to $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$ defined as $\operatorname{brecOn}$ applied to $n$ and $\mathrm{Action\_\_diagonalSuccIsoTensorTrivial\_\_\_f}$ applied to $G$.
Action.leftRegularTensorIsodefMathlib.CategoryTheory.Action.Monoidal, function or constant
Wording
the left regular tensor isomorphism of G and X (from the name)
English
Let $G$ be a set. Let $X$ be an action of the set of sets and $G$. Then the left regular tensor isomorphism of $G$ and $X$ is an isomorphism of the tensor object of the left regular of $G$ and $X$ and the tensor object of the left regular of $G$ and $\operatorname{trivial}$ applied to $G$ and $\operatorname{V}$ applied to $X$.
Action.tensorUnitIsodefMathlib.CategoryTheory.Action.Monoidal, function or constant
Wording
the tensor unit isomorphism of f (from the name)
English
Let $f$ be an isomorphism of the tensor unity in the monoidal structure of $V$ and $X$. Then the tensor unit isomorphism of $f$ is an isomorphism of the tensor unity in the monoidal structure of the set of actions of $V$ and $G$ and $\operatorname{mk}$ applied to $X$ and $1$.

Mathlib.CategoryTheory.Adhesive.Basic

CategoryTheory.AdhesiveclassMathlib.CategoryTheory.Adhesive.Basic, predicate
Wording
no wording
English
Let $C$ be a set. Then we can say that $\operatorname{Adhesive}$ holds for $C$.
CategoryTheory.IsPushout.IsVanKampendefMathlib.CategoryTheory.Adhesive.Basic, predicate
Wording
no wording
English
Assume that $\operatorname{IsPushout}$ holds for $f$, $g$, $h$ and $i$. Then $\operatorname{IsVanKampen}$ holds for $h_{1}$, if for all elements $\mathrm{W'}$, $\mathrm{X'}$, $\mathrm{Y'}$ and $\mathrm{Z'}$ of $C$, for all homomorphisms $\mathrm{f'}$ of $\mathrm{W'}$ and $\mathrm{X'}$, for all homomorphisms $\mathrm{g'}$ of $\mathrm{W'}$ and $\mathrm{Y'}$, for all homomorphisms $\mathrm{h'}$ of $\mathrm{X'}$ and $\mathrm{Z'}$, for all homomorphisms $\mathrm{i'}$ of $\mathrm{Y'}$ and $\mathrm{Z'}$, for all homomorphisms $x_{1}$ of $\mathrm{W'}$ and $W$, for all homomorphisms $x_{2}$ of $\mathrm{X'}$ and $X$, for all homomorphisms $x_{3}$ of $\mathrm{Y'}$ and $Y$, for all homomorphisms $x_{4}$ of $\mathrm{Z'}$ and $Z$, if $\operatorname{IsPullback}$ holds for $\mathrm{f'}$, $x_{1}$, $x_{2}$ and $f$, then if $\operatorname{IsPullback}$ holds for $\mathrm{g'}$, $x_{1}$, $x_{3}$ and $g$, then if $\operatorname{CommSq}$ holds for $\mathrm{h'}$, $x_{2}$, $x_{4}$ and $h$, then if $\operatorname{CommSq}$ holds for $\mathrm{i'}$, $x_{3}$, $x_{4}$ and $i$, then if $\operatorname{CommSq}$ holds for $\mathrm{f'}$, $\mathrm{g'}$, $\mathrm{h'}$ and $\mathrm{i'}$, then $\operatorname{IsPushout}$ holds for $\mathrm{f'}$, $\mathrm{g'}$, $\mathrm{h'}$ and $\mathrm{i'}$, if and only if $\operatorname{IsPullback}$ holds for $\mathrm{h'}$, $x_{2}$, $x_{4}$ and $h$ and $\operatorname{IsPullback}$ holds for $\mathrm{i'}$, $x_{3}$, $x_{4}$ and $i$.

Mathlib.CategoryTheory.Adhesive.Subobject

CategoryTheory.Adhesive.isColimitBinaryCofandefMathlib.CategoryTheory.Adhesive.Subobject, function or constant
Wording
no wording
English
Let $a$ and $b$ be subobjects of $X$. Then $\operatorname{isColimitBinaryCofan}$ applied to $a$ and $b$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the homomorphism of $\mathrm{CategoryTheory\_\_Subobject\_\_le\_mk\_of\_comm}$ applied to the left injection of the first projection of the pullback of the arrow of $a$ and the arrow of $b$ and the second projection of the pullback of the arrow of $a$ and the arrow of $b$ and $\mathrm{CategoryTheory\_\_Limits\_\_pushout\_\_inl\_desc}$ applied to the arrow of $a$, the arrow of $b$ and $\operatorname{condition}$ and the homomorphism of $\mathrm{CategoryTheory\_\_Subobject\_\_le\_mk\_of\_comm}$ applied to the right injection of the first projection of the pullback of the arrow of $a$ and the arrow of $b$ and the second projection of the pullback of the arrow of $a$ and the arrow of $b$ and $\mathrm{CategoryTheory\_\_Limits\_\_pushout\_\_inr\_desc}$ applied to the arrow of $a$, the arrow of $b$ and $\operatorname{condition}$.

Mathlib.CategoryTheory.Adjunction.Additive

CategoryTheory.Adjunction.compPreadditiveYonedaIsodefMathlib.CategoryTheory.Adjunction.Additive, function or constant
Wording
the composition preadditive Yoneda isomorphism of adj (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the composition preadditive Yoneda isomorphism of $\mathrm{adj}$ is an isomorphism of the composition of $G$ and the composition of the preadditive Yoneda and the action of the right whiskering of the set of additive commutative group categories and the set of additive commutative group categories and the lift functor and the composition of the preadditive Yoneda and the composition of the action of the left whiskering of the set of opposites of $D$ and the set of additive commutative group categories and the opposite of $F$ and the action of the right whiskering of the set of additive commutative group categories and the set of additive commutative group categories and the lift functor.
CategoryTheory.Adjunction.homAddEquivdefMathlib.CategoryTheory.Adjunction.Additive, function or constant
Wording
the homomorphism additive equivalence of X and Y (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $X$ be an element of $C$. Let $Y$ be an element of $D$. Then the homomorphism additive equivalence of $X$ and $Y$ is an additive equivalence of the set of homomorphisms of the action of $F$ and $X$ and $Y$ and the set of homomorphisms of $X$ and the action of $G$ and $Y$.

Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

CategoryTheory.SolutionSetConditiondefMathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems, predicate
Wording
G is a solution set condition (from the name)
English
Let $G$ be a functor of $D$ and $C$. Then $G$ is a solution set condition, if for all elements $A$ of $C$, there exists a set $x_{2}$, such that there exists a function $B$ from elements of $x_{2}$ to elements of $D$, such that there exists a function $f$ from elements $i_{1}$ of $x_{2}$ to homomorphisms of $A$ and the action of $G$ and $B$ applied to $i_{1}$, such that for all elements $X$ of $D$, for all homomorphisms $h$ of $A$ and the action of $G$ and $X$, there exists an element $i$ of $x_{2}$, such that there exists a homomorphism $g$ of $B$ applied to $i$ and $X$, such that the composition of $f$ applied to $i$ and the map of $G$ and $g$ is equal to $h$.

Mathlib.CategoryTheory.Adjunction.Basic

CategoryTheory.AdjunctionstructureMathlib.CategoryTheory.Adjunction.Basic, type
Wording
adjunction of F and G (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $C$. Then the adjunctions of $F$ and $G$ are a basic type.
CategoryTheory.Adjunction.CoreHomEquivstructureMathlib.CategoryTheory.Adjunction.Basic, type
Wording
homomorphism equivalence of F and G (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $C$. Then the homomorphism equivalences of $F$ and $G$ are a basic type.
CategoryTheory.Adjunction.CoreHomEquiv.homEquivdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the homomorphism equivalence of X and Y (from the name)
English
Let $\mathrm{self}$ be a homomorphism equivalence of $F$ and $G$. Let $X$ be an element of $C$. Let $Y$ be an element of $D$. Then the homomorphism equivalence of $X$ and $Y$ is an equivalence from the set of homomorphisms of the action of $F$ and $X$ and $Y$ to the set of homomorphisms of $X$ and the action of $G$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $X$ and $Y$.
CategoryTheory.Adjunction.CoreHomEquivUnitCounitstructureMathlib.CategoryTheory.Adjunction.Basic, type
Wording
homomorphism equivalence unit counit of F and G (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $C$. Then the homomorphism equivalence unit counits of $F$ and $G$ are a basic type.
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.counitdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the counit of self (from the docstring)
English
Let $\mathrm{self}$ be a homomorphism equivalence unit counit of $F$ and $G$. Then the counit of $\mathrm{self}$ is a homomorphism of the composition of $G$ and $F$ and the identity of $D$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquivdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the homomorphism equivalence of X and Y (from the name)
English
Let $\mathrm{self}$ be a homomorphism equivalence unit counit of $F$ and $G$. Let $X$ be an element of $C$. Let $Y$ be an element of $D$. Then the homomorphism equivalence of $X$ and $Y$ is an equivalence from the set of homomorphisms of the action of $F$ and $X$ and $Y$ to the set of homomorphisms of $X$ and the action of $G$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $X$ and $Y$.
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.unitdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the unit of self (from the docstring)
English
Let $\mathrm{self}$ be a homomorphism equivalence unit counit of $F$ and $G$. Then the unit of $\mathrm{self}$ is a homomorphism of the identity of $C$ and the composition of $F$ and $G$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
CategoryTheory.Adjunction.CoreUnitCounitstructureMathlib.CategoryTheory.Adjunction.Basic, type
Wording
unit counit of F and G (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $C$. Then the unit counits of $F$ and $G$ are a basic type.
CategoryTheory.Adjunction.CoreUnitCounit.counitdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the counit of self (from the docstring)
English
Let $\mathrm{self}$ be a unit counit of $F$ and $G$. Then the counit of $\mathrm{self}$ is a homomorphism of the composition of $G$ and $F$ and the identity of $D$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
CategoryTheory.Adjunction.CoreUnitCounit.unitdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the unit of self (from the docstring)
English
Let $\mathrm{self}$ be a unit counit of $F$ and $G$. Then the unit of $\mathrm{self}$ is a homomorphism of the identity of $C$ and the composition of $F$ and $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Adjunction.adjunctionOfEquivLeftdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the adjunction of e and X1 (from the name)
English
Let $e$ be a function from elements $X_{1}$ of $C$ and elements $Y_{1}$ of $D$ to equivalences from the set of homomorphisms of $\mathrm{F\_obj}$ applied to $X_{1}$ and $Y_{1}$ to the set of homomorphisms of $X_{1}$ and the action of $G$ and $Y_{1}$ such that for all elements $X$ of $C$, for all elements $Y$ and $\mathrm{Y'}$ of $D$, for all homomorphisms $g$ of $Y$ and $\mathrm{Y'}$, for all homomorphisms $h$ of $\mathrm{F\_obj}$ applied to $X$ and $Y$, $e$ applied to $X$, $\mathrm{Y'}$ and the composition of $h$ and $g$ is equal to the composition of $e$ applied to $X$, $Y$ and $h$ and the map of $G$ and $g$. Then the adjunction of $X_{1}$ and $Y_{1}$ is an adjunction of the left adjoint of $e$ and $\mathrm{he}$ and $G$.
CategoryTheory.Adjunction.adjunctionOfEquivRightdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the adjunction of e and X1 (from the name)
English
Let $e$ be a function from elements $X_{1}$ of $C$ and elements $Y_{1}$ of $D$ to equivalences from the set of homomorphisms of the action of $F$ and $X_{1}$ and $Y_{1}$ to the set of homomorphisms of $X_{1}$ and $\mathrm{G\_obj}$ applied to $Y_{1}$ such that for all elements $\mathrm{X'}$ and $X$ of $C$, for all elements $Y$ of $D$, for all homomorphisms $f$ of $\mathrm{X'}$ and $X$, for all homomorphisms $g$ of the action of $F$ and $X$ and $Y$, $e$ applied to $\mathrm{X'}$, $Y$ and the composition of the map of $F$ and $f$ and $g$ is equal to the composition of $f$ and $e$ applied to $X$, $Y$ and $g$. Then the adjunction of $X_{1}$ and $Y_{1}$ is an adjunction of $F$ and the right adjoint of $e$ and $\mathrm{he}$.
CategoryTheory.Adjunction.compdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the composition of x3 and x4 (from the name)
English
Let $x_{3}$ be an adjunction of $F$ and $G$. Let $x_{4}$ be an adjunction of $H$ and $I$. Then the composition of $x_{3}$ and $x_{4}$ is an adjunction of the composition of $F$ and $H$ and the composition of $I$ and $G$.
CategoryTheory.Adjunction.compCoyonedaIsodefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the composition Coyoneda isomorphism of adj (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the composition Coyoneda isomorphism of $\mathrm{adj}$ is an isomorphism of the composition of the opposite of $F$ and the Coyoneda and the composition of the Coyoneda and the action of the left whiskering of $C$ and the set of sets and $G$.
CategoryTheory.Adjunction.compUliftCoyonedaIsodefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the composition lift Coyoneda isomorphism of adj (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the composition lift Coyoneda isomorphism of $\mathrm{adj}$ is an isomorphism of the composition of the opposite of $F$ and the lift Coyoneda and the composition of the lift Coyoneda and the action of the left whiskering of $C$ and the set of sets and $G$.
CategoryTheory.Adjunction.compYonedaIsodefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the composition Yoneda isomorphism of adj (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the composition Yoneda isomorphism of $\mathrm{adj}$ is an isomorphism of the composition of $G$ and the Yoneda and the composition of the Yoneda and the action of the left whiskering of the set of opposites of $D$ and the set of sets and the opposite of $F$.
CategoryTheory.Adjunction.corepresentableBydefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
no wording
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $X$ be an element of $C$. Then $\operatorname{corepresentableBy}$ applied to $\mathrm{adj}$ and $X$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of $G$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and the action of $F$ and $X$.
CategoryTheory.Adjunction.counitdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the counit of self (from the docstring)
English
Let $\mathrm{self}$ be an adjunction of $F$ and $G$. Then the counit of $\mathrm{self}$ is a homomorphism of the composition of $G$ and $F$ and the identity of $D$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
CategoryTheory.Adjunction.equivHomsetLeftOfNatIsodefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the left equivalence homset of iso (from the name)
English
Let $\mathrm{iso}$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the left equivalence homset of $\mathrm{iso}$ is an equivalence from the set of homomorphisms of the action of $F$ and $X$ and $Y$ to the set of homomorphisms of the action of $\mathrm{F'}$ and $X$ and $Y$.
CategoryTheory.Adjunction.equivHomsetRightOfNatIsodefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the right equivalence homset of iso (from the name)
English
Let $\mathrm{iso}$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the right equivalence homset of $\mathrm{iso}$ is an equivalence from the set of homomorphisms of $Y$ and the action of $F$ and $X$ to the set of homomorphisms of $Y$ and the action of $\mathrm{F'}$ and $X$.
CategoryTheory.Adjunction.homEquivdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the homomorphism equivalence of X and Y (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $X$ be an element of $C$. Let $Y$ be an element of $D$. Then the homomorphism equivalence of $X$ and $Y$ is an equivalence from the set of homomorphisms of the action of $F$ and $X$ and $Y$ to the set of homomorphisms of $X$ and the action of $G$ and $Y$.
CategoryTheory.Adjunction.homEquiv'defMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the homomorphism equivalence of X and Y (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $G$ and $F$. Let $X$ be an element of $C$. Let $Y$ be an element of $D$. Then the homomorphism equivalence of $X$ and $Y$ is an equivalence from the set of homomorphisms of $Y$ and the action of $F$ and $X$ to the set of homomorphisms of the action of $G$ and $Y$ and $X$ defined as the inverse of the homomorphism equivalence of $Y$ and $X$.
CategoryTheory.Adjunction.iddefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the adjunction between the identity functor (from the docstring)
English
The adjunction between the identity functor is an adjunction of the identity of $C$ and the identity of $C$.
CategoryTheory.Adjunction.leftAdjointOfEquivdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the left adjoint of e and X1 (from the name)
English
Let $e$ be a function from elements $X_{1}$ of $C$ and elements $Y_{1}$ of $D$ to equivalences from the set of homomorphisms of $\mathrm{F\_obj}$ applied to $X_{1}$ and $Y_{1}$ to the set of homomorphisms of $X_{1}$ and the action of $G$ and $Y_{1}$ such that for all elements $X$ of $C$, for all elements $Y$ and $\mathrm{Y'}$ of $D$, for all homomorphisms $g$ of $Y$ and $\mathrm{Y'}$, for all homomorphisms $h$ of $\mathrm{F\_obj}$ applied to $X$ and $Y$, $e$ applied to $X$, $\mathrm{Y'}$ and the composition of $h$ and $g$ is equal to the composition of $e$ applied to $X$, $Y$ and $h$ and the map of $G$ and $g$. Then the left adjoint of $X_{1}$ and $Y_{1}$ is a functor of $C$ and $D$.
CategoryTheory.Adjunction.mk'defMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
no wording
English
Let $\mathrm{adj}$ be a homomorphism equivalence unit counit of $F$ and $G$. Then $\operatorname{mk'}$ applied to $\mathrm{adj}$ is an adjunction of $F$ and $G$.
CategoryTheory.Adjunction.mkOfHomEquivdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
no wording
English
Let $\mathrm{adj}$ be a homomorphism equivalence of $F$ and $G$. Then $\operatorname{mkOfHomEquiv}$ applied to $\mathrm{adj}$ is an adjunction of $F$ and $G$.
CategoryTheory.Adjunction.mkOfUnitCounitdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
no wording
English
Let $\mathrm{adj}$ be a unit counit of $F$ and $G$. Then $\operatorname{mkOfUnitCounit}$ applied to $\mathrm{adj}$ is an adjunction of $F$ and $G$.
CategoryTheory.Adjunction.ofIsLeftAdjointdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the adjunction of left (from the name)
English
Let $\mathrm{left}$ be a functor of $C$ and $D$. Then the adjunction of $\mathrm{left}$ is an adjunction of $\mathrm{left}$ and the right adjoint of $\mathrm{left}$.
CategoryTheory.Adjunction.ofIsRightAdjointdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the adjunction of right (from the name)
English
Let $\mathrm{right}$ be a functor of $C$ and $D$. Then the adjunction of $\mathrm{right}$ is an adjunction of the left adjoint of $\mathrm{right}$ and $\mathrm{right}$.
CategoryTheory.Adjunction.ofNatIsoLeftdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the adjunction of adj and iso (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $H$. Let $\mathrm{iso}$ be an isomorphism of $F$ and $G$. Then the adjunction of $\mathrm{adj}$ and $\mathrm{iso}$ is an adjunction of $G$ and $H$.
CategoryTheory.Adjunction.ofNatIsoRightdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the adjunction of adj and iso (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $H$ and $F$. Let $\mathrm{iso}$ be an isomorphism of $F$ and $G$. Then the adjunction of $\mathrm{adj}$ and $\mathrm{iso}$ is an adjunction of $H$ and $G$.
CategoryTheory.Adjunction.representableBydefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
no wording
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $Y$ be an element of $D$. Then $\operatorname{representableBy}$ applied to $\mathrm{adj}$ and $Y$ is an element of $\operatorname{RepresentableBy}$ applied to the composition of the opposite of $F$ and the action of the Yoneda and $Y$ and the action of $G$ and $Y$.
CategoryTheory.Adjunction.rightAdjointOfEquivdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the right adjoint of e and X1 (from the name)
English
Let $e$ be a function from elements $X_{1}$ of $C$ and elements $Y_{1}$ of $D$ to equivalences from the set of homomorphisms of the action of $F$ and $X_{1}$ and $Y_{1}$ to the set of homomorphisms of $X_{1}$ and $\mathrm{G\_obj}$ applied to $Y_{1}$ such that for all elements $\mathrm{X'}$ and $X$ of $C$, for all elements $Y$ of $D$, for all homomorphisms $f$ of $\mathrm{X'}$ and $X$, for all homomorphisms $g$ of the action of $F$ and $X$ and $Y$, $e$ applied to $\mathrm{X'}$, $Y$ and the composition of the map of $F$ and $f$ and $g$ is equal to the composition of $f$ and $e$ applied to $X$, $Y$ and $g$. Then the right adjoint of $X_{1}$ and $Y_{1}$ is a functor of $D$ and $C$.
CategoryTheory.Adjunction.toEquivalencedefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the equivalence of adj (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the equivalence of $\mathrm{adj}$ is an equivalence of $C$ and $D$.
CategoryTheory.Adjunction.unitdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the unit of self (from the docstring)
English
Let $\mathrm{self}$ be an adjunction of $F$ and $G$. Then the unit of $\mathrm{self}$ is a homomorphism of the identity of $C$ and the composition of $F$ and $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Equivalence.toAdjunctiondefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the adjunction of e (from the name)
English
Let $e$ be an equivalence of $C$ and $D$. Then the adjunction of $e$ is an adjunction of the functor of $e$ and the inverse of $e$.
CategoryTheory.Equivalence.toAdjunction'defMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the adjunction of e (from the name)
English
Let $e$ be an equivalence of $C$ and $D$. Then the adjunction of $e$ is an adjunction of the inverse of $e$ and the functor of $e$ defined as the adjunction of the inverse of $e$.
CategoryTheory.Functor.IsLeftAdjointclassMathlib.CategoryTheory.Adjunction.Basic, predicate
Wording
left is a left adjoint (from the name)
English
Let $\mathrm{left}$ be a functor of $C$ and $D$. Then we can say that $\mathrm{left}$ is a left adjoint.
CategoryTheory.Functor.IsRightAdjointclassMathlib.CategoryTheory.Adjunction.Basic, predicate
Wording
right is a right adjoint (from the name)
English
Let $\mathrm{right}$ be a functor of $D$ and $C$. Then we can say that $\mathrm{right}$ is a right adjoint.
CategoryTheory.Functor.adjunctiondefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the adjunction of E (from the name)
English
Let $E$ be a functor of $C$ and $D$. Then the adjunction of $E$ is an adjunction of $E$ and the inverse of $E$ defined as the adjunction of $\operatorname{asEquivalence}$ applied to $E$.
CategoryTheory.Functor.leftAdjointdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the left adjoint of R (from the name)
English
Let $R$ be a functor of $D$ and $C$. Then the left adjoint of $R$ is a functor of $C$ and $D$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsRightAdjoint\_\_exists\_leftAdjoint}$.
CategoryTheory.Functor.rightAdjointdefMathlib.CategoryTheory.Adjunction.Basic, function or constant
Wording
the right adjoint of R (from the name)
English
Let $R$ be a functor of $D$ and $C$. Then the right adjoint of $R$ is a functor of $C$ and $D$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsLeftAdjoint\_\_exists\_rightAdjoint}$.

Mathlib.CategoryTheory.Adjunction.Comma

CategoryTheory.adjunctionOfCostructuredArrowTerminalsdefMathlib.CategoryTheory.Adjunction.Comma, function or constant
Wording
the adjunction of G (from the name)
English
Let $G$ be a functor of $D$ and $C$. Then the adjunction of $G$ is an adjunction of $G$ and the right adjoint of $G$.
CategoryTheory.adjunctionOfStructuredArrowInitialsdefMathlib.CategoryTheory.Adjunction.Comma, function or constant
Wording
the adjunction of G (from the name)
English
Let $G$ be a functor of $D$ and $C$. Then the adjunction of $G$ is an adjunction of the left adjoint of $G$ and $G$.
CategoryTheory.leftAdjointOfStructuredArrowInitialsdefMathlib.CategoryTheory.Adjunction.Comma, function or constant
Wording
the left adjoint of G (from the name)
English
Let $G$ be a functor of $D$ and $C$. Then the left adjoint of $G$ is a functor of $C$ and $D$.
CategoryTheory.mkInitialOfLeftAdjointdefMathlib.CategoryTheory.Adjunction.Comma, function or constant
Wording
no wording
English
Let $G$ be a functor of $D$ and $C$. Let $h$ be an adjunction of $F$ and $G$. Let $A$ be an element of $C$. Then $\operatorname{mkInitialOfLeftAdjoint}$ applied to $G$, $h$ and $A$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{mk}$ applied to the component of the unit of $h$ and $A$.
CategoryTheory.mkTerminalOfRightAdjointdefMathlib.CategoryTheory.Adjunction.Comma, function or constant
Wording
the terminal of h and A (from the name)
English
Let $G$ be a functor of $D$ and $C$. Let $h$ be an adjunction of $F$ and $G$. Let $A$ be an element of $D$. Then the terminal of $h$ and $A$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{mk}$ applied to the component of the counit of $h$ and $A$.
CategoryTheory.rightAdjointOfCostructuredArrowTerminalsdefMathlib.CategoryTheory.Adjunction.Comma, function or constant
Wording
the right adjoint of G (from the name)
English
Let $G$ be a functor of $D$ and $C$. Then the right adjoint of $G$ is a functor of $C$ and $D$.

Mathlib.CategoryTheory.Adjunction.CompositionIso

CategoryTheory.Adjunction.leftAdjointCompIsodefMathlib.CategoryTheory.Adjunction.CompositionIso, function or constant
Wording
the left adjoint composition isomorphism of x14 and x15 (from the name)
English
Let $x_{12}$ be an adjunction of $x_{6}$ and $x_{9}$. Let $x_{13}$ be an adjunction of $x_{7}$ and $x_{10}$. Let $x_{14}$ be an adjunction of $x_{8}$ and $x_{11}$. Let $x_{15}$ be an isomorphism of the composition of $x_{10}$ and $x_{9}$ and $x_{11}$. Then the left adjoint composition isomorphism of $x_{14}$ and $x_{15}$ is an isomorphism of the composition of $x_{6}$ and $x_{7}$ and $x_{8}$ defined as $\operatorname{symm}$ applied to the conjugate isomorphism equivalence of $x_{14}$ and the composition of $x_{12}$ and $x_{13}$ and the inverse of $x_{15}$.
CategoryTheory.Adjunction.leftAdjointCompNatTransdefMathlib.CategoryTheory.Adjunction.CompositionIso, function or constant
Wording
the left adjoint composition natural transformation of x14 and x15 (from the name)
English
Let $x_{12}$ be an adjunction of $x_{6}$ and $x_{9}$. Let $x_{13}$ be an adjunction of $x_{7}$ and $x_{10}$. Let $x_{14}$ be an adjunction of $x_{8}$ and $x_{11}$. Let $x_{15}$ be a homomorphism of $x_{11}$ and the composition of $x_{10}$ and $x_{9}$. Then the left adjoint composition natural transformation of $x_{14}$ and $x_{15}$ is a homomorphism of the composition of $x_{6}$ and $x_{7}$ and $x_{8}$ defined as $\operatorname{symm}$ applied to the conjugate equivalence of $x_{14}$ and the composition of $x_{12}$ and $x_{13}$ and $x_{15}$.
CategoryTheory.Adjunction.leftAdjointIdIsodefMathlib.CategoryTheory.Adjunction.CompositionIso, function or constant
Wording
the left adjoint identity isomorphism of adj and e (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $e$ be an isomorphism of $G$ and the identity of $x$. Then the left adjoint identity isomorphism of $\mathrm{adj}$ and $e$ is an isomorphism of $F$ and the identity of $x$ defined as $\operatorname{symm}$ applied to the conjugate isomorphism equivalence of the adjunction between the identity functor and $\mathrm{adj}$ and the inverse of $e$.

Mathlib.CategoryTheory.Adjunction.Evaluation

CategoryTheory.evaluationAdjunctionLeftdefMathlib.CategoryTheory.Adjunction.Evaluation, function or constant
Wording
the left evaluation adjunction of D and c (from the name)
English
Let $D$ be a set. Let $c$ be an element of $C$. Then the left evaluation adjunction of $D$ and $c$ is an adjunction of the action of the evaluation of $C$ and $D$ and $c$ and the right adjoint of evaluation of $D$ and $c$.
CategoryTheory.evaluationAdjunctionRightdefMathlib.CategoryTheory.Adjunction.Evaluation, function or constant
Wording
the right evaluation adjunction of D and c (from the name)
English
Let $D$ be a set. Let $c$ be an element of $C$. Then the right evaluation adjunction of $D$ and $c$ is an adjunction of the left adjoint of evaluation of $D$ and $c$ and the action of the evaluation of $C$ and $D$ and $c$.
CategoryTheory.evaluationLeftAdjointdefMathlib.CategoryTheory.Adjunction.Evaluation, function or constant
Wording
the left adjoint of evaluation of D and c (from the docstring)
English
Let $D$ be a set. Let $c$ be an element of $C$. Then the left adjoint of evaluation of $D$ and $c$ is a functor of $D$ and the set of functors of $C$ and $D$.
CategoryTheory.evaluationRightAdjointdefMathlib.CategoryTheory.Adjunction.Evaluation, function or constant
Wording
the right adjoint of evaluation of D and c (from the docstring)
English
Let $D$ be a set. Let $c$ be an element of $C$. Then the right adjoint of evaluation of $D$ and $c$ is a functor of $D$ and the set of functors of $C$ and $D$.

Mathlib.CategoryTheory.Adjunction.FullyFaithful

CategoryTheory.Adjunction.counitSplitMonoOfRFulldefMathlib.CategoryTheory.Adjunction.FullyFaithful, function or constant
Wording
the counit split monomorphism of h and X (from the name)
English
Let $h$ be an adjunction of $L$ and $R$. Let $X$ be an element of $D$. Then the counit split monomorphism of $h$ and $X$ is a split monomorphism of the component of the counit of $h$ and $X$.
CategoryTheory.Adjunction.fullyFaithfulLOfIsIsoUnitdefMathlib.CategoryTheory.Adjunction.FullyFaithful, function or constant
Wording
no wording
English
Let $h$ be an adjunction of $L$ and $R$. Then $\operatorname{fullyFaithfulLOfIsIsoUnit}$ applied to $h$ is an element of $\operatorname{FullyFaithful}$ applied to $L$.
CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounitdefMathlib.CategoryTheory.Adjunction.FullyFaithful, function or constant
Wording
no wording
English
Let $h$ be an adjunction of $L$ and $R$. Then $\operatorname{fullyFaithfulROfIsIsoCounit}$ applied to $h$ is an element of $\operatorname{FullyFaithful}$ applied to $R$.
CategoryTheory.Adjunction.unitSplitEpiOfLFulldefMathlib.CategoryTheory.Adjunction.FullyFaithful, function or constant
Wording
the unit split epimorphism of h and X (from the name)
English
Let $h$ be an adjunction of $L$ and $R$. Let $X$ be an element of $C$. Then the unit split epimorphism of $h$ and $X$ is a split epimorphism of the component of the unit of $h$ and $X$.
CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnitdefMathlib.CategoryTheory.Adjunction.FullyFaithful, function or constant
Wording
the whisker left counit isomorphism of h (from the name)
English
Let $h$ be an adjunction of $L$ and $R$. Then the whisker left counit isomorphism of $h$ is an isomorphism of the composition of $L$ and the composition of $R$ and $L$ and $L$ defined as the composition of the inverse of the associator of $R$ and $L$ and the composition of the right isomorphism whisker of the inverse of $\operatorname{asIso}$ applied to the unit of $h$ and $L$ and the left unitor of $L$.
CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounitdefMathlib.CategoryTheory.Adjunction.FullyFaithful, function or constant
Wording
the whisker left unit isomorphism of h (from the name)
English
Let $h$ be an adjunction of $L$ and $R$. Then the whisker left unit isomorphism of $h$ is an isomorphism of the composition of $R$ and the composition of $L$ and $R$ and $R$ defined as the composition of the inverse of the associator of $L$ and $R$ and the composition of the right isomorphism whisker of $\operatorname{asIso}$ applied to the counit of $h$ and $R$ and the left unitor of $R$.

Mathlib.CategoryTheory.Adjunction.Lifting.Left

CategoryTheory.LiftLeftAdjoint.constructLeftAdjointdefMathlib.CategoryTheory.Adjunction.Lifting.Left, function or constant
Wording
the construct left adjoint of h1 and X (from the name)
English
Let $R$ be a functor of $A$ and $B$. Let $\mathrm{F'}$ be a functor of $C$ and $A$. Let $x_{3}$ be an adjunction of $F$ and $U$. Let $x_{4}$ be an adjunction of $\mathrm{F'}$ and the composition of $R$ and $U$. Let $h_{1}$ be a function from elements $X$ of $B$ to regular epimorphisms of the component of the counit of $x_{3}$ and $X$. Then the construct left adjoint of $x_{4}$ and $X$ is a functor of $B$ and $A$.
CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquivdefMathlib.CategoryTheory.Adjunction.Lifting.Left, function or constant
Wording
the construct left adjoint equivalence of Y and X (from the name)
English
Let $R$ be a functor of $A$ and $B$. Let $\mathrm{F'}$ be a functor of $C$ and $A$. Let $x_{3}$ be an adjunction of $F$ and $U$. Let $x_{4}$ be an adjunction of $\mathrm{F'}$ and the composition of $R$ and $U$. Let $h_{1}$ be a function from elements $X_{1}$ of $B$ to regular epimorphisms of the component of the counit of $x_{3}$ and $X_{1}$. Let $Y$ be an element of $A$. Let $X$ be an element of $B$. Then the construct left adjoint equivalence of $h_{1}$ and $Y$ is an equivalence from the set of homomorphisms of the construct left adjoint object of $x_{4}$ and $X$ and $Y$ to the set of homomorphisms of $X$ and the action of $R$ and $Y$.
CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObjdefMathlib.CategoryTheory.Adjunction.Lifting.Left, function or constant
Wording
the construct left adjoint object of Y and #5 (from the name)
English
Let $R$ be a functor of $A$ and $B$. Let $\mathrm{F'}$ be a functor of $C$ and $A$. Let $x_{3}$ be an adjunction of $F$ and $U$. Let $x_{4}$ be an adjunction of $\mathrm{F'}$ and the composition of $R$ and $U$. Let $Y$ be an element of $B$. Then the construct left adjoint object of $x_{4}$ and $Y$ is an element of $A$ defined as the coequalizer of the map of $\mathrm{F'}$ and the map of $U$ and the component of the counit of $x_{3}$ and $Y$ and the other map of $x_{4}$ and $Y$.
CategoryTheory.LiftLeftAdjoint.counitCoequalizesdefMathlib.CategoryTheory.Adjunction.Lifting.Left, function or constant
Wording
no wording
English
Let $x_{2}$ be an adjunction of $F$ and $U$. Let $h$ be a function from elements $X_{1}$ of $B$ to regular epimorphisms of the component of the counit of $x_{2}$ and $X_{1}$. Let $X$ be an element of $B$. Then $\operatorname{counitCoequalizes}$ applied to $x_{2}$, $X_{1}$, $h$ and $X$ is an element of $\operatorname{IsColimit}$ applied to the projection of the component of the counit of $x_{2}$ and $X$ and $\mathrm{CategoryTheory\_\_Adjunction\_\_counit\_naturality}$ applied to $x_{2}$ and the component of the counit of $x_{2}$ and $X$.
CategoryTheory.LiftLeftAdjoint.otherMapdefMathlib.CategoryTheory.Adjunction.Lifting.Left, function or constant
Wording
the other map of X and #5 (from the name)
English
Let $R$ be a functor of $A$ and $B$. Let $\mathrm{F'}$ be a functor of $C$ and $A$. Let $x_{3}$ be an adjunction of $F$ and $U$. Let $x_{4}$ be an adjunction of $\mathrm{F'}$ and the composition of $R$ and $U$. Let $X$ be an element of $B$. Then the other map of $x_{4}$ and $X$ is a homomorphism of the action of $\mathrm{F'}$ and the action of $U$ and the action of $F$ and the action of $U$ and $X$ and the action of $\mathrm{F'}$ and the action of $U$ and $X$ defined as the composition of the map of $\mathrm{F'}$ and the map of $U$ and the composition of the map of $F$ and the component of the unit of $x_{4}$ and $\operatorname{proj0}$ applied to $U$ and $X$ and the component of the counit of $x_{3}$ and the action of $R$ and the action of $\mathrm{F'}$ and $\operatorname{proj0}$ applied to $U$ and $X$ and the component of the counit of $x_{4}$ and the action of $\mathrm{F'}$ and $\operatorname{proj0}$ applied to $U$ and $X$.

Mathlib.CategoryTheory.Adjunction.Lifting.Right

CategoryTheory.LiftRightAdjoint.constructRightAdjointdefMathlib.CategoryTheory.Adjunction.Lifting.Right, function or constant
Wording
the construct right adjoint of h1 and X (from the name)
English
Let $L$ be a functor of $C$ and $B$. Let $\mathrm{U'}$ be a functor of $A$ and $C$. Let $x_{3}$ be an adjunction of $F$ and $U$. Let $x_{4}$ be an adjunction of the composition of $L$ and $F$ and $\mathrm{U'}$. Let $h_{1}$ be a function from elements $X$ of $B$ to regular monomorphisms of the component of the unit of $x_{3}$ and $X$. Then the construct right adjoint of $x_{4}$ and $X$ is a functor of $B$ and $C$.
CategoryTheory.LiftRightAdjoint.constructRightAdjointEquivdefMathlib.CategoryTheory.Adjunction.Lifting.Right, function or constant
Wording
the construct right adjoint equivalence of Y and X (from the name)
English
Let $L$ be a functor of $C$ and $B$. Let $\mathrm{U'}$ be a functor of $A$ and $C$. Let $x_{3}$ be an adjunction of $F$ and $U$. Let $x_{4}$ be an adjunction of the composition of $L$ and $F$ and $\mathrm{U'}$. Let $h_{1}$ be a function from elements $X_{1}$ of $B$ to regular monomorphisms of the component of the unit of $x_{3}$ and $X_{1}$. Let $Y$ be an element of $C$. Let $X$ be an element of $B$. Then the construct right adjoint equivalence of $h_{1}$ and $Y$ is an equivalence from the set of homomorphisms of $Y$ and the construct right adjoint object of $x_{4}$ and $X$ to the set of homomorphisms of the action of $L$ and $Y$ and $X$.
CategoryTheory.LiftRightAdjoint.constructRightAdjointObjdefMathlib.CategoryTheory.Adjunction.Lifting.Right, function or constant
Wording
the construct right adjoint object of Y and #5 (from the name)
English
Let $L$ be a functor of $C$ and $B$. Let $\mathrm{U'}$ be a functor of $A$ and $C$. Let $x_{3}$ be an adjunction of $F$ and $U$. Let $x_{4}$ be an adjunction of the composition of $L$ and $F$ and $\mathrm{U'}$. Let $Y$ be an element of $B$. Then the construct right adjoint object of $x_{4}$ and $Y$ is an element of $C$ defined as the equalizer of the map of $\mathrm{U'}$ and the map of $F$ and the component of the unit of $x_{3}$ and $Y$ and the other map of $x_{4}$ and $Y$.
CategoryTheory.LiftRightAdjoint.otherMapdefMathlib.CategoryTheory.Adjunction.Lifting.Right, function or constant
Wording
the other map of X and #5 (from the name)
English
Let $L$ be a functor of $C$ and $B$. Let $\mathrm{U'}$ be a functor of $A$ and $C$. Let $x_{3}$ be an adjunction of $F$ and $U$. Let $x_{4}$ be an adjunction of the composition of $L$ and $F$ and $\mathrm{U'}$. Let $X$ be an element of $B$. Then the other map of $x_{4}$ and $X$ is a homomorphism of the action of $\mathrm{U'}$ and the action of $F$ and $X$ and the action of $\mathrm{U'}$ and the action of $F$ and the action of $U$ and the action of $F$ and $X$ defined as the composition of the component of the unit of $x_{4}$ and $\operatorname{proj0}$ applied to $\mathrm{U'}$ and the action of $F$ and $X$ and the map of $\mathrm{U'}$ and the map of $F$ and the composition of the component of the unit of $x_{3}$ and $\operatorname{proj0}$ applied to $L$ and $\operatorname{proj0}$ applied to $\mathrm{U'}$ and the action of $F$ and $X$ and the map of $U$ and the component of the counit of $x_{4}$ and the action of $F$ and $X$.
CategoryTheory.LiftRightAdjoint.unitEqualizesdefMathlib.CategoryTheory.Adjunction.Lifting.Right, function or constant
Wording
no wording
English
Let $x_{2}$ be an adjunction of $F$ and $U$. Let $h$ be a function from elements $X_{1}$ of $B$ to regular monomorphisms of the component of the unit of $x_{2}$ and $X_{1}$. Let $X$ be an element of $B$. Then $\operatorname{unitEqualizes}$ applied to $x_{2}$, $X_{1}$, $h$ and $X$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the component of the unit of $x_{2}$ and $X$ and $\mathrm{CategoryTheory\_\_Adjunction\_\_unit\_naturality}$ applied to $x_{2}$ and the component of the unit of $x_{2}$ and $X$.

Mathlib.CategoryTheory.Adjunction.Limits

CategoryTheory.Adjunction.coconesIsodefMathlib.CategoryTheory.Adjunction.Limits, function or constant
Wording
the cocone isomorphism of adj (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the cocone isomorphism of $\mathrm{adj}$ is an isomorphism of the action of the cocone of $J$ and $D$ and $\operatorname{op}$ applied to the composition of $K$ and $F$ and the composition of $G$ and the action of the cocone of $J$ and $C$ and $\operatorname{op}$ applied to $K$.
CategoryTheory.Adjunction.conesIsodefMathlib.CategoryTheory.Adjunction.Limits, function or constant
Wording
the cone isomorphism of adj (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the cone isomorphism of $\mathrm{adj}$ is an isomorphism of the composition of the opposite of $F$ and the action of the cone of $J$ and $D$ and $K$ and the action of the cone of $J$ and $C$ and the composition of $K$ and $G$.
CategoryTheory.Adjunction.functorialityAdjunctiondefMathlib.CategoryTheory.Adjunction.Limits, function or constant
Wording
the functor of adj and K (from the docstring)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $K$ be a functor of $J$ and $C$. Then the functor of $\mathrm{adj}$ and $K$ is an adjunction of the functoriality of $K$ and $F$ and the functoriality right adjoint of $\mathrm{adj}$ and $K$.
CategoryTheory.Adjunction.functorialityAdjunction'defMathlib.CategoryTheory.Adjunction.Limits, function or constant
Wording
the functor of adj and K (from the docstring)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $K$ be a functor of $J$ and $D$. Then the functor of $\mathrm{adj}$ and $K$ is an adjunction of the functoriality left adjoint of $\mathrm{adj}$ and $K$ and the functoriality of $K$ and $G$.
CategoryTheory.Adjunction.functorialityCounitdefMathlib.CategoryTheory.Adjunction.Limits, function or constant
Wording
the functoriality counit of adj and K (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $K$ be a functor of $J$ and $C$. Then the functoriality counit of $\mathrm{adj}$ and $K$ is a homomorphism of the composition of the functoriality right adjoint of $\mathrm{adj}$ and $K$ and the functoriality of $K$ and $F$ and the identity of the set of cocones of the composition of $K$ and $F$.
CategoryTheory.Adjunction.functorialityCounit'defMathlib.CategoryTheory.Adjunction.Limits, function or constant
Wording
the functoriality counit of adj and K (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $K$ be a functor of $J$ and $D$. Then the functoriality counit of $\mathrm{adj}$ and $K$ is a homomorphism of the composition of the functoriality of $K$ and $G$ and the functoriality left adjoint of $\mathrm{adj}$ and $K$ and the identity of the set of cones of $K$.
CategoryTheory.Adjunction.functorialityLeftAdjointdefMathlib.CategoryTheory.Adjunction.Limits, function or constant
Wording
the functoriality left adjoint of adj and K (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $K$ be a functor of $J$ and $D$. Then the functoriality left adjoint of $\mathrm{adj}$ and $K$ is a functor of the set of cones of the composition of $K$ and $G$ and the set of cones of $K$ defined as the composition of the functoriality of the composition of $K$ and $G$ and $F$ and the postcomposition of the composition of the homomorphism of the associator of $G$ and $F$ and the composition of the left whisker of $K$ and the counit of $\mathrm{adj}$ and the homomorphism of the right unitor of $K$.
CategoryTheory.Adjunction.functorialityRightAdjointdefMathlib.CategoryTheory.Adjunction.Limits, function or constant
Wording
the functoriality right adjoint of adj and K (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $K$ be a functor of $J$ and $C$. Then the functoriality right adjoint of $\mathrm{adj}$ and $K$ is a functor of the set of cocones of the composition of $K$ and $F$ and the set of cocones of $K$ defined as the composition of the functoriality of the composition of $K$ and $F$ and $G$ and the precomposition of the composition of the inverse of the right unitor of $K$ and the composition of the left whisker of $K$ and the unit of $\mathrm{adj}$ and the inverse of the associator of $F$ and $G$.
CategoryTheory.Adjunction.functorialityUnitdefMathlib.CategoryTheory.Adjunction.Limits, function or constant
Wording
the functoriality unit of adj and K (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $K$ be a functor of $J$ and $C$. Then the functoriality unit of $\mathrm{adj}$ and $K$ is a homomorphism of the identity of the set of cocones of $K$ and the composition of the functoriality of $K$ and $F$ and the functoriality right adjoint of $\mathrm{adj}$ and $K$.
CategoryTheory.Adjunction.functorialityUnit'defMathlib.CategoryTheory.Adjunction.Limits, function or constant
Wording
the functoriality unit of adj and K (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $K$ be a functor of $J$ and $D$. Then the functoriality unit of $\mathrm{adj}$ and $K$ is a homomorphism of the identity of the set of cones of the composition of $K$ and $G$ and the composition of the functoriality left adjoint of $\mathrm{adj}$ and $K$ and the functoriality of $K$ and $G$.

Mathlib.CategoryTheory.Adjunction.Mates

CategoryTheory.conjugateEquivdefMathlib.CategoryTheory.Adjunction.Mates, function or constant
Wording
the conjugate equivalence of x6 and x7 (from the name)
English
Let $x_{6}$ be an adjunction of $x_{2}$ and $x_{4}$. Let $x_{7}$ be an adjunction of $x_{3}$ and $x_{5}$. Then the conjugate equivalence of $x_{6}$ and $x_{7}$ is an equivalence from the set of homomorphisms of $x_{3}$ and $x_{2}$ to the set of homomorphisms of $x_{4}$ and $x_{5}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the homomorphism congruence of the left unitor of $x_{3}$ and the right unitor of $x_{2}$ and $\operatorname{mateEquiv}$ applied to $x_{6}$ and $x_{7}$ and the homomorphism congruence of the right unitor of $x_{4}$ and the left unitor of $x_{5}$.
CategoryTheory.conjugateIsoEquivdefMathlib.CategoryTheory.Adjunction.Mates, function or constant
Wording
the conjugate isomorphism equivalence of x6 and x7 (from the name)
English
Let $x_{6}$ be an adjunction of $x_{2}$ and $x_{4}$. Let $x_{7}$ be an adjunction of $x_{3}$ and $x_{5}$. Then the conjugate isomorphism equivalence of $x_{6}$ and $x_{7}$ is an equivalence from the set of isomorphisms of $x_{3}$ and $x_{2}$ to the set of isomorphisms of $x_{4}$ and $x_{5}$.
CategoryTheory.mateEquivdefMathlib.CategoryTheory.Adjunction.Mates, function or constant
Wording
no wording
English
Let $x_{8}$ be an adjunction of $x_{4}$ and $x_{5}$. Let $x_{9}$ be an adjunction of $x_{6}$ and $x_{7}$. Then $\operatorname{mateEquiv}$ applied to $x_{8}$ and $x_{9}$ is an element of $\EquivMACRoAE {\operatorname{TwoSquare} (G , x_{4} , x_{6} , H)}{\operatorname{TwoSquare} (x_{5} , H , G , x_{7})}$.

Mathlib.CategoryTheory.Adjunction.Opposites

CategoryTheory.Adjunction.leftOpdefMathlib.CategoryTheory.Adjunction.Opposites, function or constant
Wording
the left opposite of a (from the name)
English
Let $a$ be an adjunction of $F$ and the left opposite of $G$. Then the left opposite of $a$ is an adjunction of $G$ and the left opposite of $F$.
CategoryTheory.Adjunction.opdefMathlib.CategoryTheory.Adjunction.Opposites, function or constant
Wording
the opposite of h (from the name)
English
Let $h$ be an adjunction of $G$ and $F$. Then the opposite of $h$ is an adjunction of the opposite of $F$ and the opposite of $G$.
CategoryTheory.Adjunction.rightOpdefMathlib.CategoryTheory.Adjunction.Opposites, function or constant
Wording
the right opposite of a (from the name)
English
Let $a$ be an adjunction of the right opposite of $F$ and $G$. Then the right opposite of $a$ is an adjunction of the right opposite of $G$ and $F$.
CategoryTheory.Adjunction.unopdefMathlib.CategoryTheory.Adjunction.Opposites, function or constant
Wording
the opposite of h (from the name)
English
Let $h$ be an adjunction of $G$ and $F$. Then the opposite of $h$ is an adjunction of the opposite of $F$ and the opposite of $G$.

Mathlib.CategoryTheory.Adjunction.Parametrized

CategoryTheory.ParametrizedAdjunctionstructureMathlib.CategoryTheory.Adjunction.Parametrized, type
Wording
parametrized adjunction of F and G (from the name)
English
Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $G$ be a functor of the set of opposites of $x$ and the set of functors of $x_{2}$ and $x_{1}$. Then the parametrized adjunctions of $F$ and $G$ are a basic type.
CategoryTheory.ParametrizedAdjunction.adjdefMathlib.CategoryTheory.Adjunction.Parametrized, function or constant
Wording
the adjoint of self and x6 (from the name)
English
Let $\mathrm{self}$ be a parametrized adjunction of $F$ and $G$. Let $x_{6}$ be an element of $x$. Then the adjoint of $\mathrm{self}$ and $x_{6}$ is an adjunction of the action of $F$ and $x_{6}$ and the action of $G$ and $\operatorname{op}$ applied to $x_{6}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{6}$.
CategoryTheory.ParametrizedAdjunction.homEquivdefMathlib.CategoryTheory.Adjunction.Parametrized, function or constant
Wording
the homomorphism equivalence of x6 (from the name)
English
Let $x_{6}$ be a parametrized adjunction of $F$ and $G$. Then the homomorphism equivalence of $x_{6}$ is an equivalence from the set of homomorphisms of the action of the action of $F$ and $x_{7}$ and $x_{8}$ and $x_{9}$ to the set of homomorphisms of $x_{8}$ and the action of the action of $G$ and $\operatorname{op}$ applied to $x_{7}$ and $x_{9}$ defined as the homomorphism equivalence of $x_{8}$ and $x_{9}$.
CategoryTheory.ParametrizedAdjunction.mk'defMathlib.CategoryTheory.Adjunction.Parametrized, function or constant
Wording
no wording
English
Let $\mathrm{adj}$ be a function from elements $x_{10}$ of $x$ to adjunctions of the action of $F$ and $x_{10}$ and the action of $G$ and $\operatorname{op}$ applied to $x_{10}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{6}$ and $x_{7}$ of $x$, for all homomorphisms $f$ of $x_{6}$ and $x_{7}$, for all elements $x_{8}$ of $x_{1}$, for all elements $x_{9}$ of $x_{2}$, for all homomorphisms $g$ of the action of the action of $F$ and $x_{7}$ and $x_{8}$ and $x_{9}$, $\operatorname{homEquiv}$ applied to $\mathrm{adj}$ applied to $x_{6}$, $x_{8}$, $x_{9}$ and the composition of the component of the map of $F$ and $f$ and $x_{8}$ and $g$ is equal to the composition of $\operatorname{homEquiv}$ applied to $\mathrm{adj}$ applied to $x_{7}$, $x_{8}$, $x_{9}$ and $g$ and the component of the map of $G$ and the opposite in $f$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_ParametrizedAdjunction\_\_mk'\_\_\_auto\_1}$. Then $\operatorname{mk'}$ applied to $x_{10}$, $\mathrm{adj}$ and $h$ is a parametrized adjunction of $F$ and $G$.

Mathlib.CategoryTheory.Adjunction.PartialAdjoint

CategoryTheory.Functor.PartialLeftAdjointSourcedefMathlib.CategoryTheory.Adjunction.PartialAdjoint, type
Wording
partial left adjoint source of F (from the name)
English
Let $F$ be a functor of $D$ and $C$. Then a partial left adjoint source of $F$ is an element of the function that maps $F$ to the set of full subcategories of $\operatorname{leftAdjointObjIsDefined}$ applied to $F$.
CategoryTheory.Functor.PartialRightAdjointSourcedefMathlib.CategoryTheory.Adjunction.PartialAdjoint, type
Wording
partial right adjoint source of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then a partial right adjoint source of $F$ is an element of the function that maps $F$ to the set of full subcategories of $\operatorname{rightAdjointObjIsDefined}$ applied to $F$.
CategoryTheory.Functor.leftAdjointObjIsDefineddefMathlib.CategoryTheory.Adjunction.PartialAdjoint, function or constant
Wording
no wording
English
Let $F$ be a functor of $D$ and $C$. Then there is an object property of $C$. Proof. Let $F$ be arbitrary. Let $X$ be arbitrary. By F. By CategoryTheory__coyoneda. By X. By Opposite__op. By CategoryTheory__Functor__obj. By CategoryTheory__Functor__comp. By CategoryTheory__Functor__IsCorepresentable.
CategoryTheory.Functor.partialLeftAdjointdefMathlib.CategoryTheory.Adjunction.PartialAdjoint, function or constant
Wording
the partial left adjoint of F (from the name)
English
Let $F$ be a functor of $D$ and $C$. Then the partial left adjoint of $F$ is a functor of the set of partial left adjoint sources of $F$ and $D$.
CategoryTheory.Functor.partialLeftAdjointHomEquivdefMathlib.CategoryTheory.Adjunction.PartialAdjoint, function or constant
Wording
the partial left adjoint homomorphism equivalence of F (from the name)
English
Let $F$ be a functor of $D$ and $C$. Then the partial left adjoint homomorphism equivalence of $F$ is an equivalence from the set of homomorphisms of the partial left adjoint object of $F$ and $X$ and $Y$ to the set of homomorphisms of the object of $X$ and the action of $F$ and $Y$ defined as the homomorphism equivalence of $\operatorname{corepresentableBy}$ applied to the composition of $F$ and the action of the Coyoneda and $\operatorname{op}$ applied to the object of $X$.
CategoryTheory.Functor.partialLeftAdjointMapdefMathlib.CategoryTheory.Adjunction.PartialAdjoint, function or constant
Wording
the partial left adjoint map of F and f (from the name)
English
Let $F$ be a functor of $D$ and $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then the partial left adjoint map of $F$ and $f$ is a homomorphism of the partial left adjoint object of $F$ and $X$ and the partial left adjoint object of $F$ and $Y$ defined as $\operatorname{symm}$ applied to the partial left adjoint homomorphism equivalence of $F$ and the composition of the homomorphism of $f$ and $\operatorname{partialLeftAdjointHomEquiv}$ applied to $F$ and the identity morphism of the partial left adjoint object of $F$ and $Y$.
CategoryTheory.Functor.partialLeftAdjointObjdefMathlib.CategoryTheory.Adjunction.PartialAdjoint, function or constant
Wording
the partial left adjoint object of F and X (from the name)
English
Let $F$ be a functor of $D$ and $C$. Let $X$ be a partial left adjoint source of $F$. Then the partial left adjoint object of $F$ and $X$ is an element of $D$ defined as $\operatorname{coreprX}$ applied to the composition of $F$ and the action of the Coyoneda and $\operatorname{op}$ applied to the object of $X$.
CategoryTheory.Functor.partialRightAdjointdefMathlib.CategoryTheory.Adjunction.PartialAdjoint, function or constant
Wording
the partial right adjoint of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the partial right adjoint of $F$ is a functor of the set of partial right adjoint sources of $F$ and $C$.
CategoryTheory.Functor.partialRightAdjointHomEquivdefMathlib.CategoryTheory.Adjunction.PartialAdjoint, function or constant
Wording
the partial right adjoint homomorphism equivalence of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the partial right adjoint homomorphism equivalence of $F$ is an equivalence from the set of homomorphisms of $X$ and the partial right adjoint object of $F$ and $Y$ to the set of homomorphisms of the action of $F$ and $X$ and the object of $Y$ defined as the homomorphism equivalence of $\operatorname{representableBy}$ applied to the composition of the opposite of $F$ and the action of the Yoneda and the object of $Y$.
CategoryTheory.Functor.partialRightAdjointMapdefMathlib.CategoryTheory.Adjunction.PartialAdjoint, function or constant
Wording
the partial right adjoint map of F and f (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the partial right adjoint map of $F$ and $f$ is a homomorphism of the partial right adjoint object of $F$ and $X$ and the partial right adjoint object of $F$ and $Y$ defined as $\operatorname{symm}$ applied to the partial right adjoint homomorphism equivalence of $F$ and the composition of $\operatorname{partialRightAdjointHomEquiv}$ applied to $F$ and the identity morphism of the partial right adjoint object of $F$ and $X$ and the homomorphism of $f$.
CategoryTheory.Functor.partialRightAdjointObjdefMathlib.CategoryTheory.Adjunction.PartialAdjoint, function or constant
Wording
the partial right adjoint object of F and Y (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $Y$ be a partial right adjoint source of $F$. Then the partial right adjoint object of $F$ and $Y$ is an element of $C$ defined as the representation of the composition of the opposite of $F$ and the action of the Yoneda and the object of $Y$.
CategoryTheory.Functor.rightAdjointObjIsDefineddefMathlib.CategoryTheory.Adjunction.PartialAdjoint, function or constant
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Then there is an object property of $D$. Proof. Let $F$ be arbitrary. Let $Y$ be arbitrary. By F. By CategoryTheory__Functor__op. By CategoryTheory__yoneda. By Y. By CategoryTheory__Functor__obj. By CategoryTheory__Functor__comp. By CategoryTheory__Functor__IsRepresentable.

Mathlib.CategoryTheory.Adjunction.Quadruple

CategoryTheory.Adjunction.QuadruplestructureMathlib.CategoryTheory.Adjunction.Quadruple, type
Wording
quadruple of G and R (from the name)
English
Let $L$ and $G$ be functors of $C$ and $D$. Let $F$ and $R$ be functors of $D$ and $C$. Then the quadruples of $G$ and $R$ are a basic type.
CategoryTheory.Adjunction.Quadruple.adj₁defMathlib.CategoryTheory.Adjunction.Quadruple, function or constant
Wording
the adjoint of self (from the name)
English
Let $\mathrm{self}$ be a quadruple of $G$ and $R$. Then the adjoint of $\mathrm{self}$ is an adjunction of $L$ and $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Adjunction.Quadruple.adj₂defMathlib.CategoryTheory.Adjunction.Quadruple, function or constant
Wording
the adjoint of self (from the name)
English
Let $\mathrm{self}$ be a quadruple of $G$ and $R$. Then the adjoint of $\mathrm{self}$ is an adjunction of $F$ and $G$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
CategoryTheory.Adjunction.Quadruple.adj₃defMathlib.CategoryTheory.Adjunction.Quadruple, function or constant
Wording
the adjoint of self (from the name)
English
Let $\mathrm{self}$ be a quadruple of $G$ and $R$. Then the adjoint of $\mathrm{self}$ is an adjunction of $G$ and $R$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
CategoryTheory.Adjunction.Quadruple.leftTripledefMathlib.CategoryTheory.Adjunction.Quadruple, function or constant
Wording
the left part of q (from the docstring)
English
Let $q$ be a quadruple of $G$ and $R$. Then the left part of $q$ is a triple of $F$ and $G$ defined as $\operatorname{mk}$ applied to the adjoint of $q$ and the adjoint of $q$.
CategoryTheory.Adjunction.Quadruple.opdefMathlib.CategoryTheory.Adjunction.Quadruple, function or constant
Wording
the opposite of q (from the name)
English
Let $q$ be a quadruple of $G$ and $R$. Then the opposite of $q$ is a quadruple of the opposite of $F$ and the opposite of $L$ defined as $\operatorname{mk}$ applied to the opposite of the adjoint of $q$, the opposite of the adjoint of $q$ and the opposite of the adjoint of $q$.
CategoryTheory.Adjunction.Quadruple.rightTripledefMathlib.CategoryTheory.Adjunction.Quadruple, function or constant
Wording
the right part of q (from the docstring)
English
Let $q$ be a quadruple of $G$ and $R$. Then the right part of $q$ is a triple of $G$ and $R$ defined as $\operatorname{mk}$ applied to the adjoint of $q$ and the adjoint of $q$.

‹ previous next ›