Definitions: Mathlib.Algebra, part 2 of 17

393 definitions of 44 modules, Mathlib.Algebra.Category.CommAlgCat.FiniteType to Mathlib.Algebra.Category.ModuleCat.Localization. ‹ previous next ›

Mathlib.Algebra.Category.CommAlgCat.FiniteType

FGAlgCatdefMathlib.Algebra.Category.CommAlgCat.FiniteType, type
Wording
no wording
English
Let $R$ be a set. Then an element of $\mathrm{FGAlgCat}$ applied to $R$ is an element of the function that maps $R$ to the set of full subcategories of the function that maps $A$ to $\operatorname{FiniteType}$ applied to $R$ and the set of carriers of $A$.
FGAlgCat.equivUnderdefMathlib.Algebra.Category.CommAlgCat.FiniteType, function or constant
Wording
no wording
English
Let $R$ be a category of commutative rings. Then $\operatorname{equivUnder}$ applied to $R$ is an equivalence of $\mathrm{FGAlgCat}$ applied to the set of carriers of $R$ and $\operatorname{Under}$ applied to the morphism property of the function that maps $x$, $x_{1}$, $x_{2}$ and $x_{3}$ to the proposition that $\operatorname{FiniteType}$, the top and $R$.
FGAlgCat.fullyFaithfulUliftFunctordefMathlib.Algebra.Category.CommAlgCat.FiniteType, function or constant
Wording
the fully faithful lift functor of R (from the name)
English
generation took over the time limit
FGAlgCat.uliftFunctordefMathlib.Algebra.Category.CommAlgCat.FiniteType, function or constant
Wording
the lift functor of R (from the name)
English
Let $R$ be a set. Then the lift functor of $R$ is a functor of $\mathrm{FGAlgCat}$ applied to $R$ and $\mathrm{FGAlgCat}$ applied to $R$.
FGAlgCatSkeletonstructureMathlib.Algebra.Category.CommAlgCat.FiniteType, type
Wording
no wording
English
Let $R$ be a set. Then the elements of $\mathrm{FGAlgCatSkeleton}$ applied to $R$ are a basic type.
FGAlgCatSkeleton.IdefMathlib.Algebra.Category.CommAlgCat.FiniteType, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an element of $\mathrm{FGAlgCatSkeleton}$ applied to $R$. Then $\operatorname{I}$ applied to $\mathrm{self}$ is an ideal of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $\operatorname{n}$ applied to $\mathrm{self}$ and $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
FGAlgCatSkeleton.evaldefMathlib.Algebra.Category.CommAlgCat.FiniteType, function or constant
Wording
the evaluation of R and A (from the name)
English
Let $R$ be a set. Let $A$ be an element of $\mathrm{FGAlgCatSkeleton}$ applied to $R$. Then the evaluation of $R$ and $A$ is an element of $\mathrm{FGAlgCat}$ applied to $R$.
FGAlgCatSkeleton.ndefMathlib.Algebra.Category.CommAlgCat.FiniteType, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an element of $\mathrm{FGAlgCatSkeleton}$ applied to $R$. Then $\operatorname{n}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Algebra.Category.CommAlgCat.Monoidal

CommAlgCat.binaryCofandefMathlib.Algebra.Category.CommAlgCat.Monoidal, function or constant
Wording
the binary cofan of A and B (from the name)
English
Let $A$ and $B$ be commutative algebra categories of $R$. Then the binary cofan of $A$ and $B$ is a binary cofan of $A$ and $B$ defined as $\operatorname{mk}$ applied to the commutative algebra category of $\operatorname{includeLeft}$ and the commutative algebra category of $\operatorname{includeRight}$.
CommAlgCat.binaryCofanIsColimitdefMathlib.Algebra.Category.CommAlgCat.Monoidal, function or constant
Wording
no wording
English
Let $A$ and $B$ be commutative algebra categories of $R$. Then $\operatorname{binaryCofanIsColimit}$ applied to $A$ and $B$ is an element of $\operatorname{IsColimit}$ applied to the binary cofan of $A$ and $B$.
CommAlgCat.isInitialSelfdefMathlib.Algebra.Category.CommAlgCat.Monoidal, function or constant
Wording
no wording
English
$\operatorname{isInitialSelf}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{of}$ applied to $R$ and $R$.

Mathlib.Algebra.Category.CommBialgCat

CommBialgCatstructureMathlib.Algebra.Category.CommBialgCat, type
Wording
commutative bialgebra category of R (from the name)
English
Let $R$ be a set. Then the commutative bialgebra categories of $R$ are a basic type.
CommBialgCat.HomstructureMathlib.Algebra.Category.CommBialgCat, type
Wording
homomorphism of A and B (from the name)
English
Let $A$ and $B$ be commutative bialgebra categories of $R$. Then the homomorphisms of $A$ and $B$ are a basic type.
CommBialgCat.Hom.homdefMathlib.Algebra.Category.CommBialgCat, function or constant
Wording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $A$ and $B$. Then the homomorphism of $f$ is a bialgebra homomorphism of the set of carriers of $A$ and the set of carriers of $B$ defined as the homomorphism of $f$.
CommBialgCat.Hom.hom'defMathlib.Algebra.Category.CommBialgCat, function or constant
Wording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the homomorphism of $\mathrm{self}$ is a bialgebra homomorphism of the set of carriers of $A$ and the set of carriers of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CommBialgCat.bialgEquivOfIsodefMathlib.Algebra.Category.CommBialgCat, function or constant
Wording
the bialgebra equivalence of i (from the name)
English
Let $i$ be an isomorphism of $A$ and $B$. Then the bialgebra equivalence of $i$ is a bialgebra equivalence of the set of carriers of $A$ and the set of carriers of $B$.
CommBialgCat.carrierdefMathlib.Algebra.Category.CommBialgCat, type
Wording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a commutative bialgebra category of $R$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
CommBialgCat.isoEquivBialgEquivdefMathlib.Algebra.Category.CommBialgCat, function or constant
Wording
the isomorphism equivalence bialgebra equivalence (from the name)
English
The isomorphism equivalence bialgebra equivalence is an equivalence from the set of isomorphisms of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$ to the set of bialgebra equivalences of $X$ and $Y$.
CommBialgCat.isoMkdefMathlib.Algebra.Category.CommBialgCat, function or constant
Wording
the isomorphism of e (from the name)
English
Let $e$ be a bialgebra equivalence of $X$ and $Y$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$.
CommBialgCat.ofdefMathlib.Algebra.Category.CommBialgCat, function or constant
Wording
no wording
English
Let $R$ and $X$ be sets. Then $\operatorname{of}$ applied to $R$ and $X$ is a commutative bialgebra category of $R$ defined as $\mathrm{CommBialgCat\_\_\_mkInternal}$ applied to $X$.
CommBialgCat.ofHomdefMathlib.Algebra.Category.CommBialgCat, function or constant
Wording
the commutative bialgebra category of f (from the name)
English
Let $f$ be a bialgebra homomorphism of $X$ and $Y$. Then the commutative bialgebra category of $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$ defined as the concrete category of $f$.
CommBialgCat.ofIsoSelfdefMathlib.Algebra.Category.CommBialgCat, function or constant
Wording
the commutative bialgebra category of M (from the name)
English
Let $M$ be a commutative bialgebra category of $R$. Then the commutative bialgebra category of $M$ is an isomorphism of $\operatorname{of}$ applied to $R$ and the set of carriers of $M$ and $M$.
commBialgCatEquivComonCommAlgCatdefMathlib.Algebra.Category.CommBialgCat, function or constant
Wording
the commutative bialgebra category equivalence comonoid commutative algebra category of R (from the name)
English
Let $R$ be a set. Then the commutative bialgebra category equivalence comonoid commutative algebra category of $R$ is an equivalence of the set of commutative bialgebra categories of $R$ and the set of opposites of the set of monoids of the set of opposites of the set of commutative algebra categories of $R$.

Mathlib.Algebra.Category.CommHopfAlgCat

CommHopfAlgCatstructureMathlib.Algebra.Category.CommHopfAlgCat, type
Wording
commutative Hopf algebra category of R (from the name)
English
Let $R$ be a set. Then the commutative Hopf algebra categories of $R$ are a basic type.
CommHopfAlgCat.HomstructureMathlib.Algebra.Category.CommHopfAlgCat, type
Wording
homomorphism of A and B (from the name)
English
Let $A$ and $B$ be commutative Hopf algebra categories of $R$. Then the homomorphisms of $A$ and $B$ are a basic type.
CommHopfAlgCat.Hom.homdefMathlib.Algebra.Category.CommHopfAlgCat, function or constant
Wording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $A$ and $B$. Then the homomorphism of $f$ is a bialgebra homomorphism of $\operatorname{X}$ applied to $A$ and $\operatorname{X}$ applied to $B$ defined as the homomorphism of $f$.
CommHopfAlgCat.Hom.hom'defMathlib.Algebra.Category.CommHopfAlgCat, function or constant
Wording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the homomorphism of $\mathrm{self}$ is a bialgebra homomorphism of $\operatorname{X}$ applied to $A$ and $\operatorname{X}$ applied to $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CommHopfAlgCat.XdefMathlib.Algebra.Category.CommHopfAlgCat, type
Wording
no wording
English
Let $\mathrm{self}$ be a commutative Hopf algebra category of $R$. Then an element of $\operatorname{X}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
CommHopfAlgCat.isoEquivBialgEquivdefMathlib.Algebra.Category.CommHopfAlgCat, function or constant
Wording
the isomorphism equivalence bialgebra equivalence (from the name)
English
The isomorphism equivalence bialgebra equivalence is an equivalence from the set of isomorphisms of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$ to the set of bialgebra equivalences of $X$ and $Y$.
CommHopfAlgCat.isoMkdefMathlib.Algebra.Category.CommHopfAlgCat, function or constant
Wording
the isomorphism of e (from the name)
English
Let $e$ be a bialgebra equivalence of $X$ and $Y$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$.
CommHopfAlgCat.ofHomdefMathlib.Algebra.Category.CommHopfAlgCat, function or constant
Wording
the commutative Hopf algebra category of f (from the name)
English
Let $f$ be a bialgebra homomorphism of $X$ and $Y$. Then the commutative Hopf algebra category of $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$ defined as the concrete category of $f$.
CommHopfAlgCat.ofIsodefMathlib.Algebra.Category.CommHopfAlgCat, function or constant
Wording
the commutative Hopf algebra category of i (from the name)
English
Let $i$ be an isomorphism of $A$ and $B$. Then the commutative Hopf algebra category of $i$ is a bialgebra equivalence of $\operatorname{X}$ applied to $A$ and $\operatorname{X}$ applied to $B$.
CommHopfAlgCat.ofIsoSelfdefMathlib.Algebra.Category.CommHopfAlgCat, function or constant
Wording
the commutative Hopf algebra category of A (from the name)
English
Let $A$ be a commutative Hopf algebra category of $R$. Then the commutative Hopf algebra category of $A$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $\operatorname{X}$ applied to $A$ and $A$.
commHopfAlgCatEquivCogrpCommAlgCatdefMathlib.Algebra.Category.CommHopfAlgCat, function or constant
Wording
no wording
English
Let $R$ be a set. Then $\mathrm{commHopfAlgCatEquivCogrpCommAlgCat}$ applied to $R$ is an equivalence of the set of commutative Hopf algebra categories of $R$ and the set of opposites of the set of groups of the set of opposites of the set of commutative algebra categories of $R$.

Mathlib.Algebra.Category.FGModuleCat.Basic

FGModuleCatdefMathlib.Algebra.Category.FGModuleCat.Basic, type
Wording
no wording
English
Let $R$ be a set. Then an element of $\mathrm{FGModuleCat}$ applied to $R$ is an element of the function that maps $R$ to the set of full subcategories of $\operatorname{isFG}$ applied to $R$.
FGModuleCat.FGModuleCatCoevaluationdefMathlib.Algebra.Category.FGModuleCat.Basic, function or constant
Wording
the coevaluation map of K and V (from the docstring)
English
Let $K$ be a set. Let $V$ be an element of $\mathrm{FGModuleCat}$ applied to $K$. Then the coevaluation map of $K$ and $V$ is a homomorphism of the tensor unity in the monoidal structure of $\mathrm{FGModuleCat}$ applied to $K$ and the tensor object of $V$ and the dual module of $K$ and $V$ defined as the concrete category of the coevaluation map of $K$ and the set of carriers of $V$.
FGModuleCat.FGModuleCatDualdefMathlib.Algebra.Category.FGModuleCat.Basic, function or constant
Wording
the dual module of K and V (from the docstring)
English
Let $K$ be a set. Let $V$ be an element of $\mathrm{FGModuleCat}$ applied to $K$. Then the dual module of $K$ and $V$ is an element of $\mathrm{FGModuleCat}$ applied to $K$.
FGModuleCat.FGModuleCatEvaluationdefMathlib.Algebra.Category.FGModuleCat.Basic, function or constant
Wording
the evaluation morphism of K and V (from the docstring)
English
Let $K$ be a set. Let $V$ be an element of $\mathrm{FGModuleCat}$ applied to $K$. Then the evaluation morphism of $K$ and $V$ is a homomorphism of the tensor object of the dual module of $K$ and $V$ and $V$ and the tensor unity in the monoidal structure of $\mathrm{FGModuleCat}$ applied to $K$ defined as the concrete category of $\mathrm{contractLeft}$ applied to $K$ and the set of carriers of $V$.
FGModuleCat.carrierdefMathlib.Algebra.Category.FGModuleCat.Basic, type
Wording
carrier of M (from the name)
English
Let $M$ be an element of $\mathrm{FGModuleCat}$ applied to $R$. Then a carrier of $M$ is an element of the function that maps $M$ to the set of carriers of the object of $M$.
FGModuleCat.fullyFaithfulULiftdefMathlib.Algebra.Category.FGModuleCat.Basic, function or constant
Wording
the fully faithful lift of R (from the name)
English
generation took over the time limit
FGModuleCat.isoToLinearEquivdefMathlib.Algebra.Category.FGModuleCat.Basic, function or constant
Wording
the isomorphism to linear equivalence of i (from the name)
English
Let $i$ be an isomorphism of $V$ and $W$. Then the isomorphism to linear equivalence of $i$ is a linear equivalence of the set of carriers of $V$ and the set of carriers of $W$ defined as the linear equivalence of the map isomorphism of the forgetful functor of $\mathrm{FGModuleCat}$ applied to $R$ and the set of module categories of $R$ and $i$.
FGModuleCat.ofdefMathlib.Algebra.Category.FGModuleCat.Basic, function or constant
Wording
no wording
English
Let $R$ and $V$ be sets. Then $\operatorname{of}$ applied to $R$ and $V$ is an element of $\mathrm{FGModuleCat}$ applied to $R$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $R$ and $V$ and $h$.
FGModuleCat.ofHomdefMathlib.Algebra.Category.FGModuleCat.Basic, function or constant
Wording
no wording
English
Let $f$ be a linear map of $V$ and $W$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $V$ and $\operatorname{of}$ applied to $R$ and $W$ defined as the concrete category of $f$.
FGModuleCat.uliftdefMathlib.Algebra.Category.FGModuleCat.Basic, function or constant
Wording
the lift of R (from the name)
English
Let $R$ be a set. Then the lift of $R$ is a functor of $\mathrm{FGModuleCat}$ applied to $R$ and $\mathrm{FGModuleCat}$ applied to $R$.
LinearEquiv.toFGModuleCatIsodefMathlib.Algebra.Category.FGModuleCat.Basic, function or constant
Wording
no wording
English
Let $e$ be a linear equivalence of $V$ and $W$. Then $\operatorname{toFGModuleCatIso}$ applied to $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $V$ and $\operatorname{of}$ applied to $R$ and $W$.
ModuleCat.isFGdefMathlib.Algebra.Category.FGModuleCat.Basic, function or constant
Wording
no wording
English
Let $R$ be a set. Then there is an object property of the set of module categories of $R$. Proof. Let $R$ be arbitrary. Let $V$ be arbitrary. By R. By V. By ModuleCat__carrier. By Module__Finite.

Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall

FGModuleReprstructureMathlib.Algebra.Category.FGModuleCat.EssentiallySmall, type
Wording
no wording
English
Let $R$ be a set. Then the elements of $\mathrm{FGModuleRepr}$ applied to $R$ are a basic type.
FGModuleRepr.SdefMathlib.Algebra.Category.FGModuleCat.EssentiallySmall, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an element of $\mathrm{FGModuleRepr}$ applied to $R$. Then $\operatorname{S}$ applied to $\mathrm{self}$ is a submodule of $R$ and the set of functions from elements of $\mathrm{Fin}$ applied to $\operatorname{n}$ applied to $\mathrm{self}$ to elements of $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
FGModuleRepr.embeddefMathlib.Algebra.Category.FGModuleCat.EssentiallySmall, function or constant
Wording
the embed of R (from the name)
English
Let $R$ be a set. Then the embed of $R$ is a functor of $\mathrm{FGModuleRepr}$ applied to $R$ and $\mathrm{FGModuleCat}$ applied to $R$ defined as the composition of the induced functor of the function that maps $x_{1}$ to $\operatorname{of}$ applied to $R$ and the set of representations of $x_{1}$ and the lift of $R$.
FGModuleRepr.ndefMathlib.Algebra.Category.FGModuleCat.EssentiallySmall, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an element of $\mathrm{FGModuleRepr}$ applied to $R$. Then $\operatorname{n}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
FGModuleRepr.ofFinitedefMathlib.Algebra.Category.FGModuleCat.EssentiallySmall, function or constant
Wording
no wording
English
Let $R$ and $M$ be sets. Then $\operatorname{ofFinite}$ applied to $R$ and $M$ is an element of $\mathrm{FGModuleRepr}$ applied to $R$.
FGModuleRepr.ofFiniteEquivdefMathlib.Algebra.Category.FGModuleCat.EssentiallySmall, function or constant
Wording
no wording
English
Let $R$ and $M$ be sets. Then $\operatorname{ofFiniteEquiv}$ applied to $R$ and $M$ is a linear equivalence of the set of representations of $\operatorname{ofFinite}$ applied to $R$ and $M$ and $M$.
FGModuleRepr.reprdefMathlib.Algebra.Category.FGModuleCat.EssentiallySmall, type
Wording
representation of x1 (from the name)
English
Let $x_{1}$ be an element of $\mathrm{FGModuleRepr}$ applied to $R$. Then a representation of $x_{1}$ is an element of the function that maps $x_{1}$ to the set of quotients of the set of functions from elements of $\mathrm{Fin}$ applied to $\operatorname{n}$ applied to $x_{1}$ to elements of $R$ and $\operatorname{S}$ applied to $x_{1}$.

Mathlib.Algebra.Category.Grp.Adjunctions

AddCommGrpCat.adjdefMathlib.Algebra.Category.Grp.Adjunctions, function or constant
Wording
the adjoint (from the name)
English
The adjoint is an adjunction of the free functor and the forgetful functor of the set of additive commutative group categories.
AddCommGrpCat.freedefMathlib.Algebra.Category.Grp.Adjunctions, function or constant
Wording
the free functor (from the docstring)
English
The free functor is a functor of the set of sets and the set of additive commutative group categories.
CommGrpCat.forget₂CommMonAdjdefMathlib.Algebra.Category.Grp.Adjunctions, function or constant
Wording
no wording
English
$\mathrm{CommGrpCat\_\_forget\_u2082\_CommMonAdj}$ is an adjunction of the forgetful functor of the set of commutative group categories and the set of commutative monoid categories and the unit.
CommMonCat.unitsdefMathlib.Algebra.Category.Grp.Adjunctions, function or constant
Wording
the unit (from the name)
English
The unit is a functor of the set of commutative monoid categories and the set of commutative group categories.
GrpCat.abelianizedefMathlib.Algebra.Category.Grp.Adjunctions, function or constant
Wording
the abelianization functor (from the docstring)
English
The abelianization functor is a functor of the set of group categories and the set of commutative group categories.
GrpCat.abelianizeAdjdefMathlib.Algebra.Category.Grp.Adjunctions, function or constant
Wording
no wording
English
$\operatorname{abelianizeAdj}$ is an adjunction of the abelianization functor and the forgetful functor of the set of commutative group categories and the set of group categories.
GrpCat.adjdefMathlib.Algebra.Category.Grp.Adjunctions, function or constant
Wording
the adjoint (from the name)
English
The adjoint is an adjunction of the free functor and the forgetful functor of the set of group categories.
GrpCat.forget₂MonAdjdefMathlib.Algebra.Category.Grp.Adjunctions, function or constant
Wording
no wording
English
$\mathrm{GrpCat\_\_forget\_u2082\_MonAdj}$ is an adjunction of the forgetful functor of the set of group categories and the set of monoid categories and the unit.
GrpCat.freedefMathlib.Algebra.Category.Grp.Adjunctions, function or constant
Wording
the free functor (from the docstring)
English
The free functor is a functor of the set of sets and the set of group categories.
MonCat.unitsdefMathlib.Algebra.Category.Grp.Adjunctions, function or constant
Wording
the unit (from the name)
English
The unit is a functor of the set of monoid categories and the set of group categories.

Mathlib.Algebra.Category.Grp.Basic

AbdefMathlib.Algebra.Category.Grp.Basic, type
Wording
abelian group (from the name)
English
An abelian group is an additive commutative group category.
AddCommGrpCatstructureMathlib.Algebra.Category.Grp.Basic, type
Wording
additive commutative group category (from the name)
English
The additive commutative group categories are a basic type.
AddCommGrpCat.HomstructureMathlib.Algebra.Category.Grp.Basic, type
Wording
homomorphism of A and B (from the name)
English
Let $A$ and $B$ be additive commutative group categories. Then the homomorphisms of $A$ and $B$ are a basic type.
AddCommGrpCat.Hom.homdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is an additive monoid homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
AddCommGrpCat.Hom.hom'defMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the underlying monoid homomorphism of self (from the docstring)
English
Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the underlying monoid homomorphism of $\mathrm{self}$ is an additive monoid homomorphism of the set of carriers of $A$ and the set of carriers of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
AddCommGrpCat.asHomdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
no wording
English
Let $g$ be a carrier of $G$. Then $\operatorname{asHom}$ applied to $g$ is a homomorphism of $\operatorname{of}$ applied to $\Integer$ and $G$ defined as the additive commutative group category of $\operatorname{zmultiplesHom}$ applied to the set of carriers of $G$ and $g$.
AddCommGrpCat.carrierdefMathlib.Algebra.Category.Grp.Basic, type
Wording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an additive commutative group category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
AddCommGrpCat.fullyFaithfulForget₂ToAddGrpdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
no wording
English
$\mathrm{AddCommGrpCat\_\_fullyFaithfulForget\_u2082\_ToAddGrp}$ is an element of $\operatorname{FullyFaithful}$ applied to the forgetful functor of the set of additive commutative group categories and the set of additive group categories.
AddCommGrpCat.ofdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is an additive commutative group category defined as $\operatorname{mk}$ applied to $M$.
AddCommGrpCat.ofHomdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the additive commutative group category of f (from the name)
English
Let $f$ be an additive monoid homomorphism of $X$ and $Y$. Then the additive commutative group category of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
AddCommGrpCat.uliftFunctordefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the lift functor (from the name)
English
The lift functor is a functor of the set of additive commutative group categories and the set of additive commutative group categories.
AddCommGrpMaxdefMathlib.Algebra.Category.Grp.Basic, type
Wording
additive commutative group maximum (from the name)
English
An additive commutative group maximum is an additive commutative group category.
AddEquiv.toAddCommGrpIsodefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the additive commutative group isomorphism of e (from the name)
English
Let $e$ be an additive equivalence of the set of carriers of $X$ and the set of carriers of $Y$. Then the additive commutative group isomorphism of $e$ is an isomorphism of $X$ and $Y$.
AddEquiv.toAddGrpIsodefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the additive group isomorphism of e (from the name)
English
Let $e$ be an additive equivalence of the set of carriers of $X$ and the set of carriers of $Y$. Then the additive group isomorphism of $e$ is an isomorphism of $X$ and $Y$.
AddGrpCatstructureMathlib.Algebra.Category.Grp.Basic, type
Wording
additive group category (from the name)
English
The additive group categories are a basic type.
AddGrpCat.HomstructureMathlib.Algebra.Category.Grp.Basic, type
Wording
homomorphism of A and B (from the name)
English
Let $A$ and $B$ be additive group categories. Then the homomorphisms of $A$ and $B$ are a basic type.
AddGrpCat.Hom.homdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is an additive monoid homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
AddGrpCat.Hom.hom'defMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the underlying monoid homomorphism of self (from the docstring)
English
Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the underlying monoid homomorphism of $\mathrm{self}$ is an additive monoid homomorphism of the set of carriers of $A$ and the set of carriers of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
AddGrpCat.carrierdefMathlib.Algebra.Category.Grp.Basic, type
Wording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an additive group category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
AddGrpCat.fullyFaithfulForget₂ToAddMonCatdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
no wording
English
$\mathrm{AddGrpCat\_\_fullyFaithfulForget\_u2082\_ToAddMonCat}$ is an element of $\operatorname{FullyFaithful}$ applied to the forgetful functor of the set of additive group categories and the set of additive monoid categories.
AddGrpCat.ofdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is an additive group category defined as $\operatorname{mk}$ applied to $M$.
AddGrpCat.ofHomdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the additive group category of f (from the name)
English
Let $f$ be an additive monoid homomorphism of $X$ and $Y$. Then the additive group category of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
AddGrpCat.uliftFunctordefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the lift functor (from the name)
English
The lift functor is a functor of the set of additive group categories and the set of additive group categories.
AddGrpMaxdefMathlib.Algebra.Category.Grp.Basic, type
Wording
additive group maximum (from the name)
English
An additive group maximum is an additive group category.
CategoryTheory.Aut.isoPermdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the isomorphism permutation (from the name)
English
The isomorphism permutation is an isomorphism of $\operatorname{of}$ applied to the set of automorphisms of $x$ and $\operatorname{of}$ applied to the set of permutations of $x$.
CategoryTheory.Aut.mulEquivPermdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the multiplicative equivalence permutation (from the name)
English
The multiplicative equivalence permutation is a multiplicative equivalence of the set of automorphisms of $x$ and the set of permutations of $x$ defined as the group isomorphism to multiplicative equivalence of the isomorphism permutation.
CategoryTheory.Iso.addCommGroupIsoToAddEquivdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the additive commutative group isomorphism to additive equivalence of i (from the name)
English
Let $i$ be an isomorphism of $X$ and $Y$. Then the additive commutative group isomorphism to additive equivalence of $i$ is an additive equivalence of the set of carriers of $X$ and the set of carriers of $Y$.
CategoryTheory.Iso.addGroupIsoToAddEquivdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the additive group isomorphism to additive equivalence of i (from the name)
English
Let $i$ be an isomorphism of $X$ and $Y$. Then the additive group isomorphism to additive equivalence of $i$ is an additive equivalence of the set of carriers of $X$ and the set of carriers of $Y$.
CategoryTheory.Iso.commGroupIsoToMulEquivdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the commutative group isomorphism to multiplicative equivalence of i (from the name)
English
Let $i$ be an isomorphism of $X$ and $Y$. Then the commutative group isomorphism to multiplicative equivalence of $i$ is a multiplicative equivalence of the set of carriers of $X$ and the set of carriers of $Y$.
CategoryTheory.Iso.groupIsoToMulEquivdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the group isomorphism to multiplicative equivalence of i (from the name)
English
Let $i$ be an isomorphism of $X$ and $Y$. Then the group isomorphism to multiplicative equivalence of $i$ is a multiplicative equivalence of the set of carriers of $X$ and the set of carriers of $Y$.
CommGrpCatstructureMathlib.Algebra.Category.Grp.Basic, type
Wording
commutative group category (from the name)
English
The commutative group categories are a basic type.
CommGrpCat.HomstructureMathlib.Algebra.Category.Grp.Basic, type
Wording
homomorphism of A and B (from the name)
English
Let $A$ and $B$ be commutative group categories. Then the homomorphisms of $A$ and $B$ are a basic type.
CommGrpCat.Hom.homdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a monoid homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
CommGrpCat.Hom.hom'defMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the underlying monoid homomorphism of self (from the docstring)
English
Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the underlying monoid homomorphism of $\mathrm{self}$ is a monoid homomorphism of the set of carriers of $A$ and the set of carriers of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CommGrpCat.carrierdefMathlib.Algebra.Category.Grp.Basic, type
Wording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a commutative group category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
CommGrpCat.fullyFaithfulForget₂ToGrpdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
no wording
English
$\mathrm{CommGrpCat\_\_fullyFaithfulForget\_u2082\_ToGrp}$ is an element of $\operatorname{FullyFaithful}$ applied to the forgetful functor of the set of commutative group categories and the set of group categories.
CommGrpCat.ofdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is a commutative group category defined as $\operatorname{mk}$ applied to $M$.
CommGrpCat.ofHomdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the commutative group category of f (from the name)
English
Let $f$ be a monoid homomorphism of $X$ and $Y$. Then the commutative group category of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
CommGrpCat.uliftFunctordefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the lift functor (from the name)
English
The lift functor is a functor of the set of commutative group categories and the set of commutative group categories.
CommGrpMaxdefMathlib.Algebra.Category.Grp.Basic, type
Wording
commutative group maximum (from the name)
English
A commutative group maximum is a commutative group category.
GrpCatstructureMathlib.Algebra.Category.Grp.Basic, type
Wording
group category (from the name)
English
The group categories are a basic type.
GrpCat.HomstructureMathlib.Algebra.Category.Grp.Basic, type
Wording
homomorphism of A and B (from the name)
English
Let $A$ and $B$ be group categories. Then the homomorphisms of $A$ and $B$ are a basic type.
GrpCat.Hom.homdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a monoid homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
GrpCat.Hom.hom'defMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the underlying monoid homomorphism of self (from the docstring)
English
Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the underlying monoid homomorphism of $\mathrm{self}$ is a monoid homomorphism of the set of carriers of $A$ and the set of carriers of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
GrpCat.carrierdefMathlib.Algebra.Category.Grp.Basic, type
Wording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a group category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
GrpCat.fullyFaithfulForget₂ToMonCatdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
no wording
English
$\mathrm{GrpCat\_\_fullyFaithfulForget\_u2082\_ToMonCat}$ is an element of $\operatorname{FullyFaithful}$ applied to the forgetful functor of the set of group categories and the set of monoid categories.
GrpCat.ofdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is a group category defined as $\operatorname{mk}$ applied to $M$.
GrpCat.ofHomdefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the group category of f (from the name)
English
Let $f$ be a monoid homomorphism of $X$ and $Y$. Then the group category of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
GrpCat.uliftFunctordefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the lift functor (from the name)
English
The lift functor is a functor of the set of group categories and the set of group categories.
GrpMaxdefMathlib.Algebra.Category.Grp.Basic, type
Wording
group maximum (from the name)
English
A group maximum is a group category.
MulEquiv.toCommGrpIsodefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the commutative group isomorphism of e (from the name)
English
Let $e$ be a multiplicative equivalence of the set of carriers of $X$ and the set of carriers of $Y$. Then the commutative group isomorphism of $e$ is an isomorphism of $X$ and $Y$.
MulEquiv.toGrpIsodefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the group isomorphism of e (from the name)
English
Let $e$ be a multiplicative equivalence of the set of carriers of $X$ and the set of carriers of $Y$. Then the group isomorphism of $e$ is an isomorphism of $X$ and $Y$.
addEquivIsoAddCommGroupIsodefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the additive equivalence isomorphism additive commutative group isomorphism (from the name)
English
The additive equivalence isomorphism additive commutative group isomorphism is an isomorphism of the set of additive equivalences of the set of carriers of $X$ and the set of carriers of $Y$ and the set of isomorphisms of $X$ and $Y$.
addEquivIsoAddGroupIsodefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the additive equivalence isomorphism additive group isomorphism (from the name)
English
The additive equivalence isomorphism additive group isomorphism is an isomorphism of the set of additive equivalences of the set of carriers of $X$ and the set of carriers of $Y$ and the set of isomorphisms of $X$ and $Y$.
mulEquivIsoCommGroupIsodefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the multiplicative equivalence isomorphism commutative group isomorphism (from the name)
English
The multiplicative equivalence isomorphism commutative group isomorphism is an isomorphism of the set of multiplicative equivalences of the set of carriers of $X$ and the set of carriers of $Y$ and the set of isomorphisms of $X$ and $Y$.
mulEquivIsoGroupIsodefMathlib.Algebra.Category.Grp.Basic, function or constant
Wording
the multiplicative equivalence isomorphism group isomorphism (from the name)
English
The multiplicative equivalence isomorphism group isomorphism is an isomorphism of the set of multiplicative equivalences of the set of carriers of $X$ and the set of carriers of $Y$ and the set of isomorphisms of $X$ and $Y$.

Mathlib.Algebra.Category.Grp.Biproducts

AddCommGrpCat.HasLimit.liftdefMathlib.Algebra.Category.Grp.Biproducts, function or constant
Wording
the lift of f and s (from the name)
English
Let $f$ be a function from elements of $J$ to additive commutative group categories. Let $s$ be an element of $\operatorname{Fan}$ applied to $f$. Then the lift of $f$ and $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{of}$ applied to the set of functions from elements $j$ of $J$ to carriers of $f$ applied to $j$.
AddCommGrpCat.HasLimit.productLimitConedefMathlib.Algebra.Category.Grp.Biproducts, function or constant
Wording
the product limit cone of f (from the name)
English
Let $f$ be a function from elements of $J$ to additive commutative group categories. Then the product limit cone of $f$ is a limit cone of the functor of $f$.
AddCommGrpCat.binaryProductLimitConedefMathlib.Algebra.Category.Grp.Biproducts, function or constant
Wording
the binary product limit cone of G and H (from the name)
English
Let $G$ and $H$ be additive commutative group categories. Then the binary product limit cone of $G$ and $H$ is a limit cone of the pair of $G$ and $H$.
AddCommGrpCat.biprodIsoProddefMathlib.Algebra.Category.Grp.Biproducts, function or constant
Wording
the biproduct isomorphism product of G and H (from the name)
English
Let $G$ and $H$ be additive commutative group categories. Then the biproduct isomorphism product of $G$ and $H$ is an isomorphism of the biproduct of $G$ and $H$ and $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to the set of carriers of $G$ and the set of carriers of $H$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to the limit cone of $G$ and $H$ and $\operatorname{isLimit}$ applied to the binary product limit cone of $G$ and $H$.
AddCommGrpCat.biproductIsoPidefMathlib.Algebra.Category.Grp.Biproducts, function or constant
Wording
the biproduct isomorphism product of f (from the name)
English
Let $f$ be a function from elements of $J$ to additive commutative group categories. Then the biproduct isomorphism product of $f$ is an isomorphism of the biproduct of $f$ and $\operatorname{of}$ applied to the set of functions from elements $j$ of $J$ to carriers of $f$ applied to $j$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to the limit cone of $f$ and $\operatorname{isLimit}$ applied to the product limit cone of $f$.

Mathlib.Algebra.Category.Grp.CartesianMonoidal

AddGrpCat.binaryProductLimitConedefMathlib.Algebra.Category.Grp.CartesianMonoidal, function or constant
Wording
the binary product limit cone of G and H (from the name)
English
Let $G$ and $H$ be additive group categories. Then the binary product limit cone of $G$ and $H$ is a limit cone of the pair of $G$ and $H$.
CommGrpCat.binaryProductLimitConedefMathlib.Algebra.Category.Grp.CartesianMonoidal, function or constant
Wording
the binary product limit cone of G and H (from the name)
English
Let $G$ and $H$ be commutative group categories. Then the binary product limit cone of $G$ and $H$ is a limit cone of the pair of $G$ and $H$.
GrpCat.binaryProductLimitConedefMathlib.Algebra.Category.Grp.CartesianMonoidal, function or constant
Wording
the binary product limit cone of G and H (from the name)
English
Let $G$ and $H$ be group categories. Then the binary product limit cone of $G$ and $H$ is a limit cone of the pair of $G$ and $H$.

Mathlib.Algebra.Category.Grp.Colimits

AddCommGrpCat.Colimits.QuotdefMathlib.Algebra.Category.Grp.Colimits, type
Wording
quotient of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then a quotient of $F$ is an element of the function that maps $F$ to the set of quotients of the set of finitely supported functions of the function that maps $j$ to the set of carriers of the action of $F$ and $j$ and the relation of $F$.
AddCommGrpCat.Colimits.Quot.descdefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Let $c$ be a cocone of $F$. Then $\operatorname{desc}$ applied to $F$ and $c$ is an additive monoid homomorphism of the set of quotients of $F$ and the set of carriers of $\operatorname{pt}$ applied to $c$.
AddCommGrpCat.Colimits.Quot.ιdefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
the inclusion of F and j (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Let $j$ be an element of $J$. Then the inclusion of $F$ and $j$ is an additive monoid homomorphism of the set of carriers of the action of $F$ and $j$ and the set of quotients of $F$ defined as the composition of $\operatorname{mk'}$ applied to the relation of $F$ and the single additive homomorphism of the function that maps $j_{1}$ to the set of carriers of the action of $F$ and $j_{1}$ and $j$.
AddCommGrpCat.Colimits.RelationsdefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
the relation of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then the relation of $F$ is an additive subgroup of the set of finitely supported functions of the function that maps $j$ to the set of carriers of the action of $F$ and $j$ defined as the closure of $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that there exist elements $j$ and $\mathrm{j'}$ of $J$, such that there exists a homomorphism $u$ of $j$ and $\mathrm{j'}$, such that there exists a carrier $a$ of the action of $F$ and $j$, such that $x_{2}$ is equal to the difference between $\operatorname{single}$ applied to $\mathrm{j'}$ and $\operatorname{hom}$ applied to the map of $F$ and $u$ and $a$ and $\operatorname{single}$ applied to $j$ and $a$.
AddCommGrpCat.Colimits.colimitCoconedefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
the colimit cocone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then the colimit cocone of $F$ is a cocone of $F$.
AddCommGrpCat.Colimits.colimitCoconeIsColimitdefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.
AddCommGrpCat.Colimits.isColimit_of_bijective_descdefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Let $c$ be a cocone of $F$ such that $\operatorname{coe}$ applied to $\operatorname{desc}$ applied to $F$ and $c$ is bijective. Then $\mathrm{AddCommGrpCat\_\_Colimits\_\_isColimit\_of\_bijective\_desc}$ applied to $F$, $c$ and $h$ is an element of $\operatorname{IsColimit}$ applied to $c$.
AddCommGrpCat.Colimits.quotQuotUliftAddEquivdefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
the quotient quotient lift additive equivalence of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then the quotient quotient lift additive equivalence of $F$ is an additive equivalence of the set of quotients of $F$ and the set of quotients of the composition of $F$ and the lift functor.
AddCommGrpCat.Colimits.quotToQuotUliftdefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
the quotient to quotient lift of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then the quotient to quotient lift of $F$ is an additive monoid homomorphism of the set of quotients of $F$ and the set of quotients of the composition of $F$ and the lift functor.
AddCommGrpCat.Colimits.quotUliftToQuotdefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
the quotient lift to quotient of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then the quotient lift to quotient of $F$ is an additive monoid homomorphism of the set of quotients of the composition of $F$ and the lift functor and the set of quotients of $F$.
AddCommGrpCat.Colimits.toCoconedefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
the cocone of F and f (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Let $f$ be an additive monoid homomorphism of the set of quotients of $F$ and $A$. Then the cocone of $F$ and $f$ is a cocone of $F$.
AddCommGrpCat.cokernelIsoQuotientdefMathlib.Algebra.Category.Grp.Colimits, function or constant
Wording
the categorical cokernel in f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the categorical cokernel in $f$ is an isomorphism of the cokernel of $f$ and $\operatorname{of}$ applied to the set of quotients of the set of carriers of $H$ and the range of the homomorphism of $f$.

Mathlib.Algebra.Category.Grp.EpiMono

GrpCat.SurjectiveOfEpiAuxs.XWithInfinityinductiveMathlib.Algebra.Category.Grp.EpiMono, type
Wording
no wording
English
Let $f$ be a homomorphism of $A$ and $B$. Then the elements of $\operatorname{XWithInfinity}$ applied to $f$ are a basic type.
GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.ctorElimTypedefMathlib.Algebra.Category.Grp.EpiMono, type
Wording
no wording
English
Let $\mathrm{ctorIdx}$ be an element of $\Natural$. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x$ of the range of the function that maps $x_{1}$ to $\HSMulhSMulMACRoAL {x_{1}}{\operatorname{range} (\operatorname{hom} (f))}$ to elements of $\mathrm{motive}$ applied to $\operatorname{fromCoset}$ applied to $x$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the infinity.
GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCosetconstructorMathlib.Algebra.Category.Grp.EpiMono, function or constant
Wording
no wording
English
Let $x$ be an element of the range of the function that maps $x_{1}$ to $\HSMulhSMulMACRoAL {x_{1}}{\operatorname{range} (\operatorname{hom} (f))}$. Then $\operatorname{fromCoset}$ applied to $x$ is an element of $\operatorname{XWithInfinity}$ applied to $f$.
GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinityconstructorMathlib.Algebra.Category.Grp.EpiMono, function or constant
Wording
the infinity (from the name)
English
The infinity is an element of $\operatorname{XWithInfinity}$ applied to $f$.
GrpCat.SurjectiveOfEpiAuxs.gdefMathlib.Algebra.Category.Grp.EpiMono, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $A$ and $B$. Then $\operatorname{g}$ applied to $f$ is a monoid homomorphism of the set of carriers of $B$ and the set of permutations of $\operatorname{XWithInfinity}$ applied to $f$.
GrpCat.SurjectiveOfEpiAuxs.hdefMathlib.Algebra.Category.Grp.EpiMono, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $A$ and $B$. Then $\operatorname{h}$ applied to $f$ is a monoid homomorphism of the set of carriers of $B$ and the set of permutations of $\operatorname{XWithInfinity}$ applied to $f$.
GrpCat.SurjectiveOfEpiAuxs.taudefMathlib.Algebra.Category.Grp.EpiMono, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $A$ and $B$. Then $\operatorname{tau}$ applied to $f$ is a permutation of $\operatorname{XWithInfinity}$ applied to $f$ defined as the swap of $\operatorname{fromCoset}$ applied to the range of the homomorphism of $f$ and the infinity.

Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup

AddCommGrpCat.toCommGrpdefMathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup, function or constant
Wording
the commutative group (from the name)
English
The commutative group is a functor of the set of additive commutative group categories and the set of commutative group categories.
AddGrpCat.toGrpdefMathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup, function or constant
Wording
the group (from the name)
English
The group is a functor of the set of additive group categories and the set of group categories.
CommGrpCat.toAddCommGrpdefMathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup, function or constant
Wording
the additive commutative group (from the name)
English
The additive commutative group is a functor of the set of commutative group categories and the set of additive commutative group categories.
GrpCat.toAddGrpdefMathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup, function or constant
Wording
the additive group (from the name)
English
The additive group is a functor of the set of group categories and the set of additive group categories.
commGroupAddCommGroupEquivalencedefMathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup, function or constant
Wording
the commutative group additive commutative group equivalence (from the name)
English
The commutative group additive commutative group equivalence is an equivalence of the set of commutative group categories and the set of additive commutative group categories.
groupAddGroupEquivalencedefMathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup, function or constant
Wording
the group additive group equivalence (from the name)
English
The group additive group equivalence is an equivalence of the set of group categories and the set of additive group categories.

Mathlib.Algebra.Category.Grp.FilteredColimits

AddCommGrpCat.FilteredColimits.GdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then $\operatorname{G}$ applied to $F$ is an additive group category defined as the colimit of the composition of $F$ and the forgetful functor of the set of additive commutative group categories and the set of additive group categories.
AddCommGrpCat.FilteredColimits.colimitdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
the colimit of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then the colimit of $F$ is an additive commutative group category defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{G}$ applied to $F$.
AddCommGrpCat.FilteredColimits.colimitCoconedefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
the colimit cocone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then the colimit cocone of $F$ is a cocone of $F$.
AddCommGrpCat.FilteredColimits.colimitCoconeIsColimitdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$ defined as $\operatorname{isColimitOfReflects}$ applied to the forgetful functor of the set of additive commutative group categories and the set of additive group categories and $\operatorname{colimitCoconeIsColimit}$ applied to the composition of $F$ and the forgetful functor of the set of additive commutative group categories and the set of additive group categories.
AddGrpCat.FilteredColimits.GdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of additive group categories. Then $\operatorname{G}$ applied to $F$ is an additive monoid category defined as the colimit of the composition of $F$ and the forgetful functor of the set of additive group categories and the set of additive monoid categories.
AddGrpCat.FilteredColimits.G.mkdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of additive group categories. Let $x_{1}$ be an element of $\Sigma$ applied to the function that maps $j$ to the set of carriers of the action of $F$ and $j$. Then $\operatorname{mk}$ applied to $F$ and $x_{1}$ is a carrier of $\operatorname{G}$ applied to $F$ defined as the inclusion colimit type of $\operatorname{fst}$ applied to $x_{1}$ and $\operatorname{snd}$ applied to $x_{1}$.
AddGrpCat.FilteredColimits.colimitdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
the colimit of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive group categories. Then the colimit of $F$ is an additive group category defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{G}$ applied to $F$.
AddGrpCat.FilteredColimits.colimitCoconedefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
the colimit cocone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive group categories. Then the colimit cocone of $F$ is a cocone of $F$.
AddGrpCat.FilteredColimits.colimitCoconeIsColimitdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of additive group categories. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$ defined as $\operatorname{isColimitOfReflects}$ applied to the forgetful functor of the set of additive group categories and the set of additive monoid categories and $\operatorname{colimitCoconeIsColimit}$ applied to the composition of $F$ and the forgetful functor of the set of additive group categories and the set of additive monoid categories.
CommGrpCat.FilteredColimits.GdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of commutative group categories. Then $\operatorname{G}$ applied to $F$ is a group category defined as the colimit of the composition of $F$ and the forgetful functor of the set of commutative group categories and the set of group categories.
CommGrpCat.FilteredColimits.colimitdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
the colimit of F (from the name)
English
Let $F$ be a functor of $J$ and the set of commutative group categories. Then the colimit of $F$ is a commutative group category defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{G}$ applied to $F$.
CommGrpCat.FilteredColimits.colimitCoconedefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
the colimit cocone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of commutative group categories. Then the colimit cocone of $F$ is a cocone of $F$.
CommGrpCat.FilteredColimits.colimitCoconeIsColimitdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of commutative group categories. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$ defined as $\operatorname{isColimitOfReflects}$ applied to the forgetful functor of the set of commutative group categories and the set of group categories and $\operatorname{colimitCoconeIsColimit}$ applied to the composition of $F$ and the forgetful functor of the set of commutative group categories and the set of group categories.
GrpCat.FilteredColimits.GdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of group categories. Then $\operatorname{G}$ applied to $F$ is a monoid category defined as the colimit of the composition of $F$ and the forgetful functor of the set of group categories and the set of monoid categories.
GrpCat.FilteredColimits.G.mkdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of group categories. Let $x_{1}$ be an element of $\Sigma$ applied to the function that maps $j$ to the set of carriers of the action of $F$ and $j$. Then $\operatorname{mk}$ applied to $F$ and $x_{1}$ is a carrier of $\operatorname{G}$ applied to $F$ defined as the inclusion colimit type of $\operatorname{fst}$ applied to $x_{1}$ and $\operatorname{snd}$ applied to $x_{1}$.
GrpCat.FilteredColimits.colimitdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
the colimit of F (from the name)
English
Let $F$ be a functor of $J$ and the set of group categories. Then the colimit of $F$ is a group category defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{G}$ applied to $F$.
GrpCat.FilteredColimits.colimitCoconedefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
the colimit cocone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of group categories. Then the colimit cocone of $F$ is a cocone of $F$.
GrpCat.FilteredColimits.colimitCoconeIsColimitdefMathlib.Algebra.Category.Grp.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of group categories. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$ defined as $\operatorname{isColimitOfReflects}$ applied to the forgetful functor of the set of group categories and the set of monoid categories and $\operatorname{colimitCoconeIsColimit}$ applied to the composition of $F$ and the forgetful functor of the set of group categories and the set of monoid categories.

Mathlib.Algebra.Category.Grp.FiniteGrp

FiniteAddGrpstructureMathlib.Algebra.Category.Grp.FiniteGrp, type
Wording
finite additive group (from the name)
English
The finite additive groups are a basic type.
FiniteAddGrp.ofdefMathlib.Algebra.Category.Grp.FiniteGrp, function or constant
Wording
no wording
English
Let $G$ be a set. Then $\operatorname{of}$ applied to $G$ is a finite additive group defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $G$.
FiniteAddGrp.ofHomdefMathlib.Algebra.Category.Grp.FiniteGrp, function or constant
Wording
the finite additive group of f (from the name)
English
Let $f$ be an additive monoid homomorphism of $X$ and $Y$. Then the finite additive group of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the homomorphism of the additive group category of $f$.
FiniteAddGrp.toAddGrpdefMathlib.Algebra.Category.Grp.FiniteGrp, function or constant
Wording
the additive group of self (from the name)
English
Let $\mathrm{self}$ be a finite additive group. Then the additive group of $\mathrm{self}$ is an additive group category defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
FiniteGrpstructureMathlib.Algebra.Category.Grp.FiniteGrp, type
Wording
finite group (from the name)
English
The finite groups are a basic type.
FiniteGrp.ofdefMathlib.Algebra.Category.Grp.FiniteGrp, function or constant
Wording
no wording
English
Let $G$ be a set. Then $\operatorname{of}$ applied to $G$ is a finite group defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $G$.
FiniteGrp.ofHomdefMathlib.Algebra.Category.Grp.FiniteGrp, function or constant
Wording
the finite group of f (from the name)
English
Let $f$ be a monoid homomorphism of $X$ and $Y$. Then the finite group of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the homomorphism of the group category of $f$.
FiniteGrp.toGrpdefMathlib.Algebra.Category.Grp.FiniteGrp, function or constant
Wording
the group of self (from the name)
English
Let $\mathrm{self}$ be a finite group. Then the group of $\mathrm{self}$ is a group category defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Algebra.Category.Grp.ForgetCorepresentable

AddCommGrpCat.coyonedaObjIsoForgetdefMathlib.Algebra.Category.Grp.ForgetCorepresentable, function or constant
Wording
no wording
English
$\operatorname{coyonedaObjIsoForget}$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Integer$ and the forgetful functor of the set of additive commutative group categories.
AddCommGrpCat.uliftZMultiplesAddEquivdefMathlib.Algebra.Category.Grp.ForgetCorepresentable, function or constant
Wording
the additive equivalence of G (from the docstring)
English
Let $G$ be an additive commutative group category. Then the additive equivalence of $G$ is an additive equivalence of the set of homomorphisms of $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Integer$ and $G$ and the set of carriers of $G$.
AddGrpCat.coyonedaObjIsoForgetdefMathlib.Algebra.Category.Grp.ForgetCorepresentable, function or constant
Wording
no wording
English
$\operatorname{coyonedaObjIsoForget}$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Integer$ and the forgetful functor of the set of additive group categories.
CommGrpCat.coyonedaObjIsoForgetdefMathlib.Algebra.Category.Grp.ForgetCorepresentable, function or constant
Wording
no wording
English
$\operatorname{coyonedaObjIsoForget}$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to the set of multiplicatives of $\Integer$ and the forgetful functor of the set of commutative group categories.
GrpCat.coyonedaObjIsoForgetdefMathlib.Algebra.Category.Grp.ForgetCorepresentable, function or constant
Wording
no wording
English
$\operatorname{coyonedaObjIsoForget}$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to the set of multiplicatives of $\Integer$ and the forgetful functor of the set of group categories.
uliftZMultiplesHomdefMathlib.Algebra.Category.Grp.ForgetCorepresentable, function or constant
Wording
the lift multiple homomorphism of G (from the name)
English
Let $G$ be a set. Then the lift multiple homomorphism of $G$ is an equivalence from $G$ to the set of additive monoid homomorphisms of $\mathrm{ULift}$ applied to $\Integer$ and $G$ defined as the composition of $\mathrm{zmultiplesHom}$ applied to $G$ and the equivalence of the inverse of the lift.
uliftZPowersHomdefMathlib.Algebra.Category.Grp.ForgetCorepresentable, function or constant
Wording
the lift power homomorphism of G (from the name)
English
Let $G$ be a set. Then the lift power homomorphism of $G$ is an equivalence from $G$ to the set of monoid homomorphisms of $\mathrm{ULift}$ applied to the set of multiplicatives of $\Integer$ and $G$ defined as the composition of $\mathrm{zpowersHom}$ applied to $G$ and the equivalence of the inverse of the lift.

Mathlib.Algebra.Category.Grp.Images

AddCommGrpCat.factorThruImagedefMathlib.Algebra.Category.Grp.Images, function or constant
Wording
the corestriction map to the image of f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the corestriction map to the image of $f$ is a homomorphism of $G$ and the image in $f$ defined as the additive commutative group category of $\operatorname{rangeRestrict}$ applied to the homomorphism of $f$.
AddCommGrpCat.imagedefMathlib.Algebra.Category.Grp.Images, function or constant
Wording
the image in f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the image in $f$ is an additive commutative group category defined as $\operatorname{of}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{hom} (f))}{x})}$.
AddCommGrpCat.image.liftdefMathlib.Algebra.Category.Grp.Images, function or constant
Wording
the lift of #1 (from the name)
English
Let $\mathrm{F'}$ be a monomorphism factorisation of $f$. Then the lift of $\mathrm{F'}$ is a homomorphism of the image in $f$ and $\operatorname{I}$ applied to $\mathrm{F'}$.
AddCommGrpCat.image.ιdefMathlib.Algebra.Category.Grp.Images, function or constant
Wording
the inclusion of f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the inclusion of $f$ is a homomorphism of the image in $f$ and $H$ defined as the additive commutative group category of the subtype of the range of the homomorphism of $f$.
AddCommGrpCat.imageIsoRangedefMathlib.Algebra.Category.Grp.Images, function or constant
Wording
the categorical image in f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the categorical image in $f$ is an isomorphism of the categorical image of $f$ and $\operatorname{of}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{hom} (f))}{x})}$ defined as the isomorphism extension of $\operatorname{isImage}$ applied to $f$ and $\operatorname{isImage}$ applied to $f$.
AddCommGrpCat.isImagedefMathlib.Algebra.Category.Grp.Images, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $G$ and $H$. Then $\operatorname{isImage}$ applied to $f$ is an element of $\operatorname{IsImage}$ applied to the factorisation in $f$ defined as $\operatorname{mk}$ applied to $\operatorname{lift}$ and $\mathrm{AddCommGrpCat\_\_image\_\_lift\_fac}$.
AddCommGrpCat.monoFactorisationdefMathlib.Algebra.Category.Grp.Images, function or constant
Wording
the factorisation in f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the factorisation in $f$ is a monomorphism factorisation of $f$.

Mathlib.Algebra.Category.Grp.IsFinite

AddCommGrpCat.isFinitedefMathlib.Algebra.Category.Grp.IsFinite, function or constant
Wording
no wording
English
There is an object property of the set of additive commutative group categories. Proof. Let $M$ be arbitrary. By M. By AddCommGrpCat__carrier. By Finite.

Mathlib.Algebra.Category.Grp.Kernels

AddCommGrpCat.cokernelCoconedefMathlib.Algebra.Category.Grp.Kernels, function or constant
Wording
the cokernel cocone induced by the projection onto the quotient of f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the cokernel cocone induced by the projection onto the quotient of $f$ is a cokernel cofork of $f$.
AddCommGrpCat.cokernelIsColimitdefMathlib.Algebra.Category.Grp.Kernels, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $G$ and $H$. Then $\operatorname{cokernelIsColimit}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cocone induced by the projection onto the quotient of $f$.
AddCommGrpCat.kernelConedefMathlib.Algebra.Category.Grp.Kernels, function or constant
Wording
the kernel cone induced by the concrete kernel of f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the kernel cone induced by the concrete kernel of $f$ is a kernel fork of $f$.
AddCommGrpCat.kernelIsLimitdefMathlib.Algebra.Category.Grp.Kernels, function or constant
Wording
the kernel of f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the kernel of $f$ is an element of $\operatorname{IsLimit}$ applied to the kernel cone induced by the concrete kernel of $f$.

Mathlib.Algebra.Category.Grp.LeftExactFunctor

AddCommGrpCat.leftExactFunctorForgetEquivalencedefMathlib.Algebra.Category.Grp.LeftExactFunctor, function or constant
Wording
no wording
English
Let $C$ be a set. Then $\operatorname{leftExactFunctorForgetEquivalence}$ applied to $C$ is an equivalence of the set of left exact functors of $C$ and the set of additive commutative group categories and the set of left exact functors of $C$ and the set of sets.

Mathlib.Algebra.Category.Grp.Limits

AddCommGrpCat.kernelIsoKerdefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the categorical kernel in f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the categorical kernel in $f$ is an isomorphism of the kernel of $f$ and $\operatorname{of}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{hom} (f))}{x})}$.
AddCommGrpCat.kernelIsoKerOverdefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $G$ and $H$. Then $\operatorname{kernelIsoKerOver}$ applied to $f$ is an isomorphism of $\operatorname{mk}$ applied to the inclusion of $f$ and $\operatorname{mk}$ applied to the additive commutative group category of the subtype of the additive kernel of the homomorphism of $f$.
AddCommGrpCat.limitConedefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the limit cone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then the limit cone of $F$ is a cone of $F$ defined as the lift limit of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of additive commutative group categories and the set of additive group categories.
AddCommGrpCat.limitConeIsLimitdefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the chosen cone of F (from the docstring)
English
Let $F$ be a functor of $J$ and the set of additive commutative group categories. Then the chosen cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as the lifted cone of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of additive commutative group categories and the set of additive group categories.
AddGrpCat.limitConedefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the limit cone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive group categories. Then the limit cone of $F$ is a cone of $F$ defined as the lift limit of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of additive group categories and the set of additive monoid categories.
AddGrpCat.limitConeIsLimitdefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the chosen cone of F (from the docstring)
English
Let $F$ be a functor of $J$ and the set of additive group categories. Then the chosen cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as the lifted cone of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of additive group categories and the set of additive monoid categories.
AddGrpCat.sectionsAddSubgroupdefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the section additive subgroup of F (from the name)
English
Let $F$ be a functor of $J$ and the set of additive group categories. Then the section additive subgroup of $F$ is an additive subgroup of the set of functions from elements $j$ of $J$ to carriers of the action of $F$ and $j$.
AddGrpCat.sectionsπAddMonoidHomdefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the section projection additive monoid homomorphism of F and j (from the name)
English
Let $F$ be a functor of $J$ and the set of additive group categories. Let $j$ be an element of $J$. Then the section projection additive monoid homomorphism of $F$ and $j$ is an additive monoid homomorphism of the set of elements of the section of the composition of $F$ and the forgetful functor of the set of additive group categories and the set of carriers of the action of $F$ and $j$.
CommGrpCat.limitConedefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the limit cone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of commutative group categories. Then the limit cone of $F$ is a cone of $F$ defined as the lift limit of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of commutative group categories and the set of group categories.
CommGrpCat.limitConeIsLimitdefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the chosen cone of F (from the docstring)
English
Let $F$ be a functor of $J$ and the set of commutative group categories. Then the chosen cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as the lifted cone of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of commutative group categories and the set of group categories.
GrpCat.limitConedefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the limit cone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of group categories. Then the limit cone of $F$ is a cone of $F$ defined as the lift limit of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of group categories and the set of monoid categories.
GrpCat.limitConeIsLimitdefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the chosen cone of F (from the docstring)
English
Let $F$ be a functor of $J$ and the set of group categories. Then the chosen cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as the lifted cone of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of group categories and the set of monoid categories.
GrpCat.sectionsSubgroupdefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the section subgroup of F (from the name)
English
Let $F$ be a functor of $J$ and the set of group categories. Then the section subgroup of $F$ is a subgroup of the set of functions from elements $j$ of $J$ to carriers of the action of $F$ and $j$.
GrpCat.sectionsπMonoidHomdefMathlib.Algebra.Category.Grp.Limits, function or constant
Wording
the section projection monoid homomorphism of F and j (from the name)
English
Let $F$ be a functor of $J$ and the set of group categories. Let $j$ be an element of $J$. Then the section projection monoid homomorphism of $F$ and $j$ is a monoid homomorphism of the set of elements of the section of the composition of $F$ and the forgetful functor of the set of group categories and the set of carriers of the action of $F$ and $j$.

Mathlib.Algebra.Category.Grp.Preadditive

AddCommGrpCat.homAddEquivdefMathlib.Algebra.Category.Grp.Preadditive, function or constant
Wording
the homomorphism additive equivalence (from the name)
English
The homomorphism additive equivalence is an additive equivalence of the set of homomorphisms of $M$ and $N$ and the set of additive monoid homomorphisms of the set of carriers of $M$ and the set of carriers of $N$.

Mathlib.Algebra.Category.Grp.Shrink

GrpCat.shrinkFunctordefMathlib.Algebra.Category.Grp.Shrink, function or constant
Wording
the shrink functor of F (from the name)
English
Let $F$ be a functor of $C$ and the set of group categories. Then the shrink functor of $F$ is a functor of $C$ and the set of group categories.
GrpCat.shrinkFunctorMapdefMathlib.Algebra.Category.Grp.Shrink, function or constant
Wording
the shrink functor map of x1 (from the name)
English
Let $x_{1}$ be a homomorphism of $F$ and $G$. Then the shrink functor map of $x_{1}$ is a homomorphism of the shrink functor of $F$ and the shrink functor of $G$.

Mathlib.Algebra.Category.Grp.Ulift

AddCommGrpCat.uliftFunctorFullyFaithfuldefMathlib.Algebra.Category.Grp.Ulift, function or constant
Wording
no wording
English
$\operatorname{uliftFunctorFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the lift functor.
AddGrpCat.uliftFunctorFullyFaithfuldefMathlib.Algebra.Category.Grp.Ulift, function or constant
Wording
no wording
English
$\operatorname{uliftFunctorFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the lift functor.
CommGrpCat.uliftFunctorFullyFaithfuldefMathlib.Algebra.Category.Grp.Ulift, function or constant
Wording
no wording
English
$\operatorname{uliftFunctorFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the lift functor.
GrpCat.uliftFunctorFullyFaithfuldefMathlib.Algebra.Category.Grp.Ulift, function or constant
Wording
no wording
English
$\operatorname{uliftFunctorFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the lift functor.

Mathlib.Algebra.Category.Grp.Yoneda

AddCommGrpCat.coyonedadefMathlib.Algebra.Category.Grp.Yoneda, function or constant
Wording
the Coyoneda (from the name)
English
The Coyoneda is a functor of the set of opposites of the set of additive commutative group categories and the set of functors of the set of additive commutative group categories and the set of additive commutative group categories.
AddCommGrpCat.coyonedaForgetdefMathlib.Algebra.Category.Grp.Yoneda, function or constant
Wording
no wording
English
$\operatorname{coyonedaForget}$ is an isomorphism of the composition of the Coyoneda and the action of the right whiskering of the set of additive commutative group categories and the set of sets and the forgetful functor of the set of additive commutative group categories and the Coyoneda.
AddCommGrpCat.coyonedaTypedefMathlib.Algebra.Category.Grp.Yoneda, function or constant
Wording
the Coyoneda type (from the name)
English
The Coyoneda type is a functor of the set of opposites of the set of sets and the set of functors of the set of additive commutative group categories and the set of additive commutative group categories.
CommGrpCat.coyonedadefMathlib.Algebra.Category.Grp.Yoneda, function or constant
Wording
the Coyoneda (from the name)
English
The Coyoneda is a functor of the set of opposites of the set of commutative group categories and the set of functors of the set of commutative group categories and the set of commutative group categories.
CommGrpCat.coyonedaForgetdefMathlib.Algebra.Category.Grp.Yoneda, function or constant
Wording
no wording
English
$\operatorname{coyonedaForget}$ is an isomorphism of the composition of the Coyoneda and the action of the right whiskering of the set of commutative group categories and the set of sets and the forgetful functor of the set of commutative group categories and the Coyoneda.
CommGrpCat.coyonedaTypedefMathlib.Algebra.Category.Grp.Yoneda, function or constant
Wording
the Coyoneda type (from the name)
English
The Coyoneda type is a functor of the set of opposites of the set of sets and the set of functors of the set of commutative group categories and the set of commutative group categories.

Mathlib.Algebra.Category.GrpWithZero

GrpWithZerostructureMathlib.Algebra.Category.GrpWithZero, type
Wording
group with zero (from the name)
English
The groups with zero are a basic type.
GrpWithZero.Iso.mkdefMathlib.Algebra.Category.GrpWithZero, function or constant
Wording
no wording
English
Let $e$ be a multiplicative equivalence of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
GrpWithZero.carrierdefMathlib.Algebra.Category.GrpWithZero, type
Wording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a group with zero. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
GrpWithZero.ofHomdefMathlib.Algebra.Category.GrpWithZero, function or constant
Wording
the group with zero of f (from the name)
English
Let $f$ be a monoid with zero homomorphism of $X$ and $Y$. Then the group with zero of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.

Mathlib.Algebra.Category.HopfAlgCat.Basic

BialgEquiv.toHopfAlgIsodefMathlib.Algebra.Category.HopfAlgCat.Basic, function or constant
Wording
the Hopf algebra isomorphism of e (from the name)
English
Let $e$ be a bialgebra equivalence of $X$ and $Y$. Then the Hopf algebra isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$.
CategoryTheory.Iso.toHopfAlgEquivdefMathlib.Algebra.Category.HopfAlgCat.Basic, function or constant
Wording
the Hopf algebra isomorphism of i (from the name)
English
Let $i$ be an isomorphism of $X$ and $Y$. Then the Hopf algebra isomorphism of $i$ is a bialgebra equivalence of the set of carriers of $X$ and the set of carriers of $Y$.
HopfAlgCatstructureMathlib.Algebra.Category.HopfAlgCat.Basic, type
Wording
Hopf algebra category of R (from the name)
English
Let $R$ be a set. Then the Hopf algebra categories of $R$ are a basic type.
HopfAlgCat.HomstructureMathlib.Algebra.Category.HopfAlgCat.Basic, type
Wording
homomorphism of V and W (from the name)
English
Let $V$ and $W$ be Hopf algebra categories of $R$. Then the homomorphisms of $V$ and $W$ are a basic type.
HopfAlgCat.Hom.toBialgHomdefMathlib.Algebra.Category.HopfAlgCat.Basic, function or constant
Wording
the bialgebra homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the bialgebra homomorphism of $f$ is a bialgebra homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
HopfAlgCat.Hom.toBialgHom'defMathlib.Algebra.Category.HopfAlgCat.Basic, function or constant
Wording
the bialgebra homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $V$ and $W$. Then the bialgebra homomorphism of $\mathrm{self}$ is a bialgebra homomorphism of the set of carriers of $V$ and the set of carriers of $W$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
HopfAlgCat.carrierdefMathlib.Algebra.Category.HopfAlgCat.Basic, type
Wording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a Hopf algebra category of $R$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
HopfAlgCat.ofdefMathlib.Algebra.Category.HopfAlgCat.Basic, function or constant
Wording
no wording
English
Let $R$ and $X$ be sets. Then $\operatorname{of}$ applied to $R$ and $X$ is a Hopf algebra category of $R$ defined as $\mathrm{HopfAlgCat\_\_\_mkInternal}$ applied to $X$.
HopfAlgCat.ofHomdefMathlib.Algebra.Category.HopfAlgCat.Basic, function or constant
Wording
the Hopf algebra category of f (from the name)
English
Let $f$ be a bialgebra homomorphism of $X$ and $Y$. Then the Hopf algebra category of $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$ defined as the concrete category of $f$.

Mathlib.Algebra.Category.HopfAlgCat.Monoidal

HopfAlgCat.MonoidalCategory.inducingFunctorDatadefMathlib.Algebra.Category.HopfAlgCat.Monoidal, function or constant
Wording
no wording
English
Let $R$ be a set. Then $\operatorname{inducingFunctorData}$ applied to $R$ is an element of $\operatorname{InducingFunctorData}$ applied to the forgetful functor of the set of Hopf algebra categories of $R$ and the set of bialgebra categories of $R$.

Mathlib.Algebra.Category.ModuleCat.Adjunctions

CategoryTheory.FreedefMathlib.Algebra.Category.ModuleCat.Adjunctions, type
Wording
free of x and C (from the name)
English
Let $x$ and $C$ be sets. Then a free of $x$ and $C$ is an element of the function that maps $x$ and $C$ to $C$.
CategoryTheory.Free.embeddingdefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the embedding of R and C (from the name)
English
Let $R$ and $C$ be sets. Then the embedding of $R$ and $C$ is a functor of $C$ and the set of frees of $R$ and $C$.
CategoryTheory.Free.embeddingLiftIsodefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the embedding lift isomorphism of R and F (from the name)
English
Let $R$ be a set. Let $F$ be a functor of $C$ and $D$. Then the embedding lift isomorphism of $R$ and $F$ is an isomorphism of the composition of the embedding of $R$ and $C$ and the lift of $R$ and $F$ and $F$.
CategoryTheory.Free.extdefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the extension of R and x5 (from the name)
English
Let $R$ be a set. Let $x_{5}$ be an isomorphism of the composition of the embedding of $R$ and $C$ and $F$ and the composition of the embedding of $R$ and $C$ and $G$. Then the extension of $R$ and $x_{5}$ is an isomorphism of $F$ and $G$.
CategoryTheory.Free.liftdefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the lift of R and F (from the name)
English
Let $R$ be a set. Let $F$ be a functor of $C$ and $D$. Then the lift of $R$ and $F$ is a functor of the set of frees of $R$ and $C$ and $D$.
CategoryTheory.Free.liftUniquedefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
no wording
English
Let $R$ be a set. Let $F$ be a functor of $C$ and $D$. Let $L$ be a functor of the set of frees of $R$ and $C$ and $D$. Let $x_{5}$ be an isomorphism of the composition of the embedding of $R$ and $C$ and $L$ and $F$. Then $\operatorname{liftUnique}$ applied to $R$, $F$, $L$ and $x_{5}$ is an isomorphism of $L$ and the lift of $R$ and $F$ defined as the extension of $R$ and the composition of $x_{5}$ and the inverse of the embedding lift isomorphism of $R$ and $F$.
CategoryTheory.Free.ofdefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
no wording
English
Let $R$ be a set. Let $X$ be an element of $C$. Then $\operatorname{of}$ applied to $R$ and $X$ is a free of $R$ and $C$ defined as $X$.
ModuleCat.FreeMonoidal.εIsodefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the canonical isomorphism of R (from the docstring)
English
Let $R$ be a set. Then the canonical isomorphism of $R$ is an isomorphism of the tensor unity in the monoidal structure of the set of module categories of $R$ and the action of the free functor of $R$ and the tensor unity in the monoidal structure of the set of sets.
ModuleCat.FreeMonoidal.μIsodefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the isomorphism of X and Y (from the name)
English
Let $R$, $X$ and $Y$ be sets. Then the isomorphism of $X$ and $Y$ is an isomorphism of the tensor object of the action of the free functor of $R$ and $X$ and the action of the free functor of $R$ and $Y$ and the action of the free functor of $R$ and the tensor object of $X$ and $Y$ defined as the module isomorphism of the finitely supported function tensor finitely supported function of $X$ and $Y$.
ModuleCat.adjdefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the adjoint of R (from the name)
English
Let $R$ be a set. Then the adjoint of $R$ is an adjunction of the free functor of $R$ and the forgetful functor of the set of module categories of $R$.
ModuleCat.freedefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the free functor of R (from the docstring)
English
Let $R$ be a set. Then the free functor of $R$ is a functor of the set of sets and the set of module categories of $R$.
ModuleCat.freeDescdefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and the set of carriers of $M$. Then $\operatorname{freeDesc}$ applied to $f$ is a homomorphism of the action of the free functor of $R$ and $X$ and $M$ defined as the module category of $\operatorname{lift}$ applied to the set of carriers of $M$, $R$, $X$ and $\operatorname{coe}$ applied to the homomorphism of $f$.
ModuleCat.freeHomEquivdefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the free homomorphism equivalence (from the name)
English
The free homomorphism equivalence is an equivalence from the set of homomorphisms of the action of the free functor of $R$ and $X$ and $M$ to the set of homomorphisms of $X$ and the set of carriers of $M$.
ModuleCat.freeMkdefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the free of x1 (from the name)
English
Let $x_{1}$ be an element of $X$. Then the free of $x_{1}$ is a carrier of the action of the free functor of $R$ and $X$ defined as $\FinsuppsingleMACRoS {x_{1}}{1}$.
ModuleCat.monoidAlgebraFreedefMathlib.Algebra.Category.ModuleCat.Adjunctions, function or constant
Wording
the free functor of R (from the docstring)
English
Let $R$ be a set. Then the free functor of $R$ is a functor of the set of sets and the set of module categories of $R$.

Mathlib.Algebra.Category.ModuleCat.Basic

CategoryTheory.Iso.toLinearEquivdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the linear equivalence of i (from the name)
English
Let $i$ be an isomorphism of $X$ and $Y$. Then the linear equivalence of $i$ is a linear equivalence of the set of carriers of $X$ and the set of carriers of $Y$.
LinearEquiv.toModuleIsodefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the module isomorphism of e (from the name)
English
Let $e$ be a linear equivalence of $x_{1}$ and $x_{2}$. Then the module isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $x_{1}$ and $\operatorname{of}$ applied to $R$ and $x_{2}$.
ModuleCatstructureMathlib.Algebra.Category.ModuleCat.Basic, type
Wording
module category of R (from the name)
English
Let $R$ be a set. Then the module categories of $R$ are a basic type.
ModuleCat.HomstructureMathlib.Algebra.Category.ModuleCat.Basic, type
Wording
homomorphism of M and N (from the name)
English
Let $M$ and $N$ be module categories of $R$. Then the homomorphisms of $M$ and $N$ are a basic type.
ModuleCat.Hom.homdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $A$ and $B$. Then the homomorphism of $f$ is a linear map of the set of carriers of $A$ and the set of carriers of $B$ defined as the homomorphism of $f$.
ModuleCat.Hom.hom'defMathlib.Algebra.Category.ModuleCat.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 linear map of the set of carriers of $M$ and the set of carriers of $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
ModuleCat.Hom.hom₂defMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $M$ and $\operatorname{of}$ applied to $R$ and the set of homomorphisms of $N$ and $P$. Then the homomorphism of $f$ is a linear map of the set of carriers of $M$ and the set of linear maps of the set of carriers of $N$ and the set of carriers of $P$ defined as the homomorphism of the composition of $f$ and the module category of $\operatorname{toLinearMap}$ applied to the homomorphism linear equivalence.
ModuleCat.carrierdefMathlib.Algebra.Category.ModuleCat.Basic, type
Wording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a module category of $R$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
ModuleCat.endRingEquivdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the end ring isomorphism of M (from the name)
English
Let $M$ be a module category of $R$. Then the end ring isomorphism of $M$ is a ring isomorphism of the set of ends of $M$ and the set of linear maps of the set of carriers of $M$ and the set of carriers of $M$.
ModuleCat.equivalenceSemimoduleCatdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the equivalence semimodule category (from the name)
English
The equivalence semimodule category is an equivalence of the set of module categories of $R$ and the set of semimodule categories of $R$.
ModuleCat.homAddEquivdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the homomorphism additive equivalence (from the name)
English
The homomorphism additive equivalence is an additive equivalence of the set of homomorphisms of $M$ and $N$ and the set of linear maps of the set of carriers of $M$ and the set of carriers of $N$.
ModuleCat.homEquivdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the homomorphism equivalence (from the name)
English
The homomorphism equivalence is an equivalence from the set of homomorphisms of $M$ and $N$ to the set of linear maps of the set of carriers of $M$ and the set of carriers of $N$.
ModuleCat.homLinearEquivdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the homomorphism linear equivalence (from the name)
English
The homomorphism linear equivalence is a linear equivalence of the set of homomorphisms of $M$ and $N$ and the set of linear maps of the set of carriers of $M$ and the set of carriers of $N$.
ModuleCat.homMkdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the homomorphism of x1 and h (from the name)
English
Let $x_{1}$ be a homomorphism of the action of the forgetful functor of the set of module categories of $R$ and the set of additive commutative group categories and $M$ and the action of the forgetful functor of the set of module categories of $R$ and the set of additive commutative group categories and $N$ such that for all elements $r$ of $R$, the composition of $x_{1}$ and $\operatorname{asHom}$ applied to $\operatorname{smul}$ applied to $N$ and $r$ is equal to the composition of $\operatorname{asHom}$ applied to $\operatorname{smul}$ applied to $M$ and $r$ and $x_{1}$. Then the homomorphism of $x_{1}$ and $h$ is a homomorphism of $M$ and $N$.
ModuleCat.isoMkdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the isomorphism of x1 and h (from the name)
English
Let $x_{1}$ be an isomorphism of the action of the forgetful functor of the set of module categories of $R$ and the set of abelian groups and $M$ and the action of the forgetful functor of the set of module categories of $R$ and the set of abelian groups and $N$ such that for all elements $r$ of $R$, the composition of the homomorphism of $x_{1}$ and $\operatorname{asHom}$ applied to $\operatorname{smul}$ applied to $N$ and $r$ is equal to the composition of $\operatorname{asHom}$ applied to $\operatorname{smul}$ applied to $M$ and $r$ and the homomorphism of $x_{1}$. Then the isomorphism of $x_{1}$ and $h$ is an isomorphism of $M$ and $N$.
ModuleCat.mkOfSMuldefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
no wording
English
Let $x_{1}$ be a ring homomorphism of $R$ and the set of ends of $A$. Then $\operatorname{mkOfSMul}$ applied to $x_{1}$ is a module category of $R$ defined as $\operatorname{of}$ applied to $R$ and the set of carriers of $\operatorname{mkOfSMul'}$ applied to $x_{1}$.
ModuleCat.mkOfSMul'defMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
no wording
English
Let $x_{1}$ be a ring homomorphism of $R$ and the set of ends of $A$. Then $\operatorname{mkOfSMul'}$ applied to $x_{1}$ is an additive commutative group category defined as $A$.
ModuleCat.ofdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
no wording
English
Let $R$ and $X$ be sets. Then $\operatorname{of}$ applied to $R$ and $X$ is a module category of $R$ defined as $\mathrm{ModuleCat\_\_\_mkInternal}$ applied to $X$.
ModuleCat.ofHomdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the module category of f (from the name)
English
Let $f$ be a linear map of $X$ and $Y$. Then the module category of $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$ defined as the concrete category of $f$.
ModuleCat.ofHom₂defMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the module category of f (from the name)
English
Let $f$ be a linear map of the set of carriers of $M$ and the set of linear maps of the set of carriers of $N$ and the set of carriers of $P$. Then the module category of $f$ is a homomorphism of $M$ and $\operatorname{of}$ applied to $R$ and the set of homomorphisms of $N$ and $P$ defined as the module category of the composition of $\operatorname{toLinearMap}$ applied to the inverse of the homomorphism linear equivalence and $f$.
ModuleCat.smuldefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the scalar multiplication of M (from the docstring)
English
Let $M$ be a module category of $R$. Then the scalar multiplication of $M$ is a ring homomorphism of $R$ and the set of ends of the action of the forgetful functor of the set of module categories of $R$ and the set of additive commutative group categories and $M$.
ModuleCat.smulNatTransdefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the scalar multiple natural transformation of R (from the name)
English
Let $R$ be a set. Then the scalar multiple natural transformation of $R$ is a ring homomorphism of $R$ and the set of ends of the forgetful functor of the set of module categories of $R$ and the set of additive commutative group categories.
linearEquivIsoModuleIsodefMathlib.Algebra.Category.ModuleCat.Basic, function or constant
Wording
the linear equivalence isomorphism module isomorphism (from the name)
English
The linear equivalence isomorphism module isomorphism is an isomorphism of the set of linear equivalences of $X$ and $Y$ and the set of isomorphisms of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$.

Mathlib.Algebra.Category.ModuleCat.Biproducts

ModuleCat.HasLimit.liftdefMathlib.Algebra.Category.ModuleCat.Biproducts, function or constant
Wording
the lift of f and s (from the name)
English
Let $f$ be a function from elements of $J$ to module categories of $R$. Let $s$ be an element of $\operatorname{Fan}$ applied to $f$. Then the lift of $f$ and $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{of}$ applied to $R$ and the set of functions from elements $j$ of $J$ to carriers of $f$ applied to $j$.
ModuleCat.HasLimit.productLimitConedefMathlib.Algebra.Category.ModuleCat.Biproducts, function or constant
Wording
the product limit cone of f (from the name)
English
Let $f$ be a function from elements of $J$ to module categories of $R$. Then the product limit cone of $f$ is a limit cone of the functor of $f$.
ModuleCat.binaryProductLimitConedefMathlib.Algebra.Category.ModuleCat.Biproducts, function or constant
Wording
the binary product limit cone of M and N (from the name)
English
Let $M$ and $N$ be module categories of $R$. Then the binary product limit cone of $M$ and $N$ is a limit cone of the pair of $M$ and $N$.
ModuleCat.biprodIsoProddefMathlib.Algebra.Category.ModuleCat.Biproducts, function or constant
Wording
the biproduct isomorphism product of M and N (from the name)
English
Let $M$ and $N$ be module categories of $R$. Then the biproduct isomorphism product of $M$ and $N$ is an isomorphism of the biproduct of $M$ and $N$ and $\operatorname{of}$ applied to $R$ and $\mathrm{Prod}$ applied to the set of carriers of $M$ and the set of carriers of $N$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to the limit cone of $M$ and $N$ and $\operatorname{isLimit}$ applied to the binary product limit cone of $M$ and $N$.
ModuleCat.biproductIsoPidefMathlib.Algebra.Category.ModuleCat.Biproducts, function or constant
Wording
the biproduct isomorphism product of f (from the name)
English
Let $f$ be a function from elements of $J$ to module categories of $R$. Then the biproduct isomorphism product of $f$ is an isomorphism of the biproduct of $f$ and $\operatorname{of}$ applied to $R$ and the set of functions from elements $j$ of $J$ to carriers of $f$ applied to $j$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to the limit cone of $f$ and $\operatorname{isLimit}$ applied to the product limit cone of $f$.
lequivProdOfLeftSplitExactdefMathlib.Algebra.Category.ModuleCat.Biproducts, function or constant
Wording
the linear equivalence product of exac and h (from the name)
English
Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $g$. Assume that the range of $j$ is equal to the kernel of $g$. Assume that the composition of $f$ and $j$ is equal to the identity. Then the linear equivalence product of $\mathrm{exac}$ and $h$ is a linear equivalence of $\mathrm{Prod}$ applied to $A$ and $B$ and $M$.
lequivProdOfRightSplitExactdefMathlib.Algebra.Category.ModuleCat.Biproducts, function or constant
Wording
the linear equivalence product of exac and h (from the name)
English
Assume that $\operatorname{coe}$ applied to $j$ is injective. Assume that the range of $j$ is equal to the kernel of $g$. Assume that the composition of $g$ and $f$ is equal to the identity. Then the linear equivalence product of $\mathrm{exac}$ and $h$ is a linear equivalence of $\mathrm{Prod}$ applied to $A$ and $B$ and $M$.

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

ModuleCat.CoextendScalars.equivdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the equivalence of f and M (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $M$ be a module category of $R$. Then the equivalence of $f$ and $M$ is a linear equivalence of the set of carriers of the action of $\operatorname{coextendScalars}$ applied to $f$ and $M$ and the set of linear maps of the set of carriers of the action of $\operatorname{restrictScalars}$ applied to $f$ and $\operatorname{of}$ applied to $S$ and $S$ and the set of carriers of $M$.
ModuleCat.CoextendScalars.map'defMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the map of f and g (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $g$ be a homomorphism of $M$ and $\mathrm{M'}$. Then the map of $f$ and $g$ is a homomorphism of the object of $f$ and $M$ and the object of $f$ and $\mathrm{M'}$.
ModuleCat.CoextendScalars.obj'defMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the object of f and M (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $M$ be a module category of $R$. Then the object of $f$ and $M$ is a module category of $S$ defined as $\operatorname{of}$ applied to $S$ and the set of linear maps of the set of carriers of the action of $\operatorname{restrictScalars}$ applied to $f$ and $\operatorname{of}$ applied to $S$ and $S$ and the set of carriers of $M$.
ModuleCat.ExtendRestrictScalarsAdj.Counit.mapdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $f$ is a homomorphism of the action of the composition of $\operatorname{restrictScalars}$ applied to $f$ and $\operatorname{extendScalars}$ applied to $f$ and $Y$ and $Y$.
ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAtdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $s$ be an element of $S$. Let $g$ be a homomorphism of $X$ and the action of $\operatorname{restrictScalars}$ applied to $f$ and $Y$. Then $\operatorname{evalAt}$ applied to $f$, $s$ and $g$ is a linear map of the set of carriers of $X$ and the set of carriers of $Y$.
ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalarsdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $g$ be a homomorphism of $X$ and the action of $\operatorname{restrictScalars}$ applied to $f$ and $Y$. Then $\operatorname{fromExtendScalars}$ applied to $f$ and $g$ is a homomorphism of the action of $\operatorname{extendScalars}$ applied to $f$ and $X$ and $Y$.
ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalarsdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $g$ be a homomorphism of the action of $\operatorname{extendScalars}$ applied to $f$ and $X$ and $Y$. Then $\operatorname{toRestrictScalars}$ applied to $f$ and $g$ is a homomorphism of $X$ and the action of $\operatorname{restrictScalars}$ applied to $f$ and $Y$.
ModuleCat.ExtendRestrictScalarsAdj.Unit.mapdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $f$ is a homomorphism of $X$ and the action of the composition of $\operatorname{extendScalars}$ applied to $f$ and $\operatorname{restrictScalars}$ applied to $f$ and $X$.
ModuleCat.ExtendRestrictScalarsAdj.counitdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the counit of f (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then the counit of $f$ is a homomorphism of the composition of $\operatorname{restrictScalars}$ applied to $f$ and $\operatorname{extendScalars}$ applied to $f$ and the identity of the set of module categories of $S$.
ModuleCat.ExtendRestrictScalarsAdj.homEquivdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the homomorphism equivalence of f (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then the homomorphism equivalence of $f$ is an equivalence from the set of homomorphisms of the action of $\operatorname{extendScalars}$ applied to $f$ and $X$ and $Y$ to the set of homomorphisms of $X$ and the action of $\operatorname{restrictScalars}$ applied to $f$ and $Y$.
ModuleCat.ExtendRestrictScalarsAdj.unitdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the unit of f (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then the unit of $f$ is a homomorphism of the identity of the set of module categories of $R$ and the composition of $\operatorname{extendScalars}$ applied to $f$ and $\operatorname{restrictScalars}$ applied to $f$.
ModuleCat.ExtendScalars.map'defMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the map of f and l (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $l$ be a homomorphism of $M_{1}$ and $M_{2}$. Then the map of $f$ and $l$ is a homomorphism of the object of $f$ and $M_{1}$ and the object of $f$ and $M_{2}$ defined as the module category of the base change of $S$ and the homomorphism of $l$.
ModuleCat.ExtendScalars.obj'defMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the object of f and M (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $M$ be a module category of $R$. Then the object of $f$ and $M$ is a module category of $S$ defined as $\operatorname{of}$ applied to $S$ and the set of tensor products of the set of carriers of the action of $\operatorname{restrictScalars}$ applied to $f$ and $\operatorname{of}$ applied to $S$ and $S$ and the set of carriers of $M$.
ModuleCat.RestrictScalars.map'defMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the map of f and g (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $g$ be a homomorphism of $M$ and $\mathrm{M'}$. Then the map of $f$ and $g$ is a homomorphism of the object of $f$ and $M$ and the object of $f$ and $\mathrm{M'}$.
ModuleCat.RestrictScalars.obj'defMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the object of f and M (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $M$ be a module category of $S$. Then the object of $f$ and $M$ is a module category of $R$ defined as $\operatorname{of}$ applied to $R$ and the set of carriers of $M$.
ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestrictiondefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $g$ be a homomorphism of the action of $\operatorname{restrictScalars}$ applied to $f$ and $Y$ and $X$. Then $\operatorname{fromRestriction}$ applied to $f$ and $g$ is a homomorphism of $Y$ and the action of $\operatorname{coextendScalars}$ applied to $f$ and $X$.
ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestrictiondefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the restriction of f and g (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $g$ be a homomorphism of $Y$ and the action of $\operatorname{coextendScalars}$ applied to $f$ and $X$. Then the restriction of $f$ and $g$ is a homomorphism of the action of $\operatorname{restrictScalars}$ applied to $f$ and $Y$ and $X$.
ModuleCat.RestrictionCoextensionAdj.counit'defMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the counit of f (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then the counit of $f$ is a homomorphism of the composition of $\operatorname{coextendScalars}$ applied to $f$ and $\operatorname{restrictScalars}$ applied to $f$ and the identity of the set of module categories of $R$.
ModuleCat.RestrictionCoextensionAdj.unit'defMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the unit of f (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then the unit of $f$ is a homomorphism of the identity of the set of module categories of $S$ and the composition of $\operatorname{restrictScalars}$ applied to $f$ and $\operatorname{coextendScalars}$ applied to $f$.
ModuleCat.coextendScalarsdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{coextendScalars}$ applied to $f$ is a functor of the set of module categories of $R$ and the set of module categories of $S$.
ModuleCat.extendRestrictScalarsAdjdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{extendRestrictScalarsAdj}$ applied to $f$ is an adjunction of $\operatorname{extendScalars}$ applied to $f$ and $\operatorname{restrictScalars}$ applied to $f$.
ModuleCat.extendScalarsdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{extendScalars}$ applied to $f$ is a functor of the set of module categories of $R$ and the set of module categories of $S$ defined as $\operatorname{mk}$ applied to the function that maps $M$ to the object of $f$ and $M$, the function that maps $x_{2}$, $x_{3}$ and $l$ to the map of $f$ and $l$, the function that maps $x_{4}$ to $\mathrm{ModuleCat\_\_ExtendScalars\_\_map'\_id}$ applied to $f$ and the function that maps $x_{5}$, $x_{6}$ and $x_{7}$ to $\mathrm{ModuleCat\_\_ExtendScalars\_\_map'\_comp}$ applied to $f$.
ModuleCat.extendScalarsCompdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $x_{6}$ be a ring homomorphism of $x$ and $x_{1}$. Let $x_{7}$ be a ring homomorphism of $x_{1}$ and $x_{2}$. Then $\operatorname{extendScalarsComp}$ applied to $x_{6}$ and $x_{7}$ is an isomorphism of $\operatorname{extendScalars}$ applied to the composition of $x_{7}$ and $x_{6}$ and the composition of $\operatorname{extendScalars}$ applied to $x_{6}$ and $\operatorname{extendScalars}$ applied to $x_{7}$ defined as $\operatorname{symm}$ applied to the conjugate isomorphism equivalence of the composition of $\operatorname{extendRestrictScalarsAdj}$ applied to $x_{6}$ and $\operatorname{extendRestrictScalarsAdj}$ applied to $x_{7}$ and $\operatorname{extendRestrictScalarsAdj}$ applied to the composition of $x_{7}$ and $x_{6}$ and the inverse of $\operatorname{restrictScalarsComp}$ applied to $x_{6}$ and $x_{7}$.
ModuleCat.extendScalarsIddefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $R$ be a set. Then $\operatorname{extendScalarsId}$ applied to $R$ is an isomorphism of $\operatorname{extendScalars}$ applied to the identity ring homomorphism of $R$ and the identity of the set of module categories of $R$ defined as the inverse of $\operatorname{symm}$ applied to the conjugate isomorphism equivalence of $\operatorname{extendRestrictScalarsAdj}$ applied to the identity ring homomorphism of $R$ and the adjunction between the identity functor and $\operatorname{restrictScalarsId}$ applied to $R$.
ModuleCat.restrictCoextendScalarsAdjdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{restrictCoextendScalarsAdj}$ applied to $f$ is an adjunction of $\operatorname{restrictScalars}$ applied to $f$ and $\operatorname{coextendScalars}$ applied to $f$.
ModuleCat.restrictScalarsdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{restrictScalars}$ applied to $f$ is a functor of the set of module categories of $S$ and the set of module categories of $R$.
ModuleCat.restrictScalarsCompdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $x$ and $x_{1}$. Let $g$ be a ring homomorphism of $x_{1}$ and $x_{2}$. Then $\operatorname{restrictScalarsComp}$ applied to $f$ and $g$ is an isomorphism of $\operatorname{restrictScalars}$ applied to the composition of $g$ and $f$ and the composition of $\operatorname{restrictScalars}$ applied to $g$ and $\operatorname{restrictScalars}$ applied to $f$.
ModuleCat.restrictScalarsComp'defMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $x$ and $x_{1}$. Let $g$ be a ring homomorphism of $x_{1}$ and $x_{2}$. Let $\mathrm{gf}$ be a ring homomorphism of $x$ and $x_{2}$ such that $\mathrm{gf}$ is equal to the composition of $g$ and $f$. Then $\operatorname{restrictScalarsComp'}$ applied to $f$, $g$, $\mathrm{gf}$ and $\mathrm{hgf}$ is an isomorphism of $\operatorname{restrictScalars}$ applied to $\mathrm{gf}$ and the composition of $\operatorname{restrictScalars}$ applied to $g$ and $\operatorname{restrictScalars}$ applied to $f$.
ModuleCat.restrictScalarsComp'AppdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $x$ and $x_{1}$. Let $g$ be a ring homomorphism of $x_{1}$ and $x_{2}$. Let $\mathrm{gf}$ be a ring homomorphism of $x$ and $x_{2}$ such that $\mathrm{gf}$ is equal to the composition of $g$ and $f$. Let $M$ be a module category of $x_{2}$. Then $\operatorname{restrictScalarsComp'App}$ applied to $f$, $g$, $\mathrm{gf}$, $\mathrm{hgf}$ and $M$ is an isomorphism of the action of $\operatorname{restrictScalars}$ applied to $\mathrm{gf}$ and $M$ and the action of $\operatorname{restrictScalars}$ applied to $f$ and the action of $\operatorname{restrictScalars}$ applied to $g$ and $M$.
ModuleCat.restrictScalarsCongrdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Assume that $\EqtMACRoH {f}{g}$. Then $\operatorname{restrictScalarsCongr}$ applied to $e$ is an isomorphism of $\operatorname{restrictScalars}$ applied to $f$ and $\operatorname{restrictScalars}$ applied to $g$.
ModuleCat.restrictScalarsEquivalenceOfRingEquivdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $e$ be a ring isomorphism of $R$ and $S$. Then $\operatorname{restrictScalarsEquivalenceOfRingEquiv}$ applied to $e$ is an equivalence of the set of module categories of $S$ and the set of module categories of $R$.
ModuleCat.restrictScalarsIddefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $R$ be a set. Then $\operatorname{restrictScalarsId}$ applied to $R$ is an isomorphism of $\operatorname{restrictScalars}$ applied to the identity ring homomorphism of $R$ and the identity of the set of module categories of $R$.
ModuleCat.restrictScalarsId'defMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $R$ such that $f$ is equal to the identity ring homomorphism of $R$. Then $\operatorname{restrictScalarsId'}$ applied to $f$ and $\mathrm{hf}$ is an isomorphism of $\operatorname{restrictScalars}$ applied to $f$ and the identity of the set of module categories of $R$.
ModuleCat.restrictScalarsId'AppdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $R$ such that $f$ is equal to the identity ring homomorphism of $R$. Let $M$ be a module category of $R$. Then $\operatorname{restrictScalarsId'App}$ applied to $f$, $\mathrm{hf}$ and $M$ is an isomorphism of the action of $\operatorname{restrictScalars}$ applied to $f$ and $M$ and $M$.
ModuleCat.restrictScalarsIsoOfEquivdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
no wording
English
Let $e$ be a ring isomorphism of $R$ and $S$. Then $\operatorname{restrictScalarsIsoOfEquiv}$ applied to $e$ is an isomorphism of the action of $\operatorname{restrictScalars}$ applied to the ring homomorphism of $e$ and $\operatorname{of}$ applied to $S$ and $S$ and $\operatorname{of}$ applied to $R$ and $R$.
ModuleCat.semilinearMapAddEquivdefMathlib.Algebra.Category.ModuleCat.ChangeOfRings, function or constant
Wording
the semilinear map additive equivalence of M and N (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $M$ be a module category of $R$. Let $N$ be a module category of $S$. Then the semilinear map additive equivalence of $M$ and $N$ is an additive equivalence of the set of linear maps of the set of carriers of $M$ and the set of carriers of $N$ and the set of homomorphisms of $M$ and the action of $\operatorname{restrictScalars}$ applied to $f$ and $N$.

Mathlib.Algebra.Category.ModuleCat.Colimits

ModuleCat.HasColimit.coconePointSMuldefMathlib.Algebra.Category.ModuleCat.Colimits, function or constant
Wording
the cocone point product of F (from the name)
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Then the cocone point product of $F$ is a ring homomorphism of $R$ and the set of ends of the colimit of the composition of $F$ and the forgetful functor of the set of module categories of $R$ and the set of additive commutative group categories.
ModuleCat.HasColimit.colimitCoconedefMathlib.Algebra.Category.ModuleCat.Colimits, function or constant
Wording
the colimit cocone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Then the colimit cocone of $F$ is a cocone of $F$.
ModuleCat.HasColimit.isColimitColimitCoconedefMathlib.Algebra.Category.ModuleCat.Colimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Then $\operatorname{isColimitColimitCocone}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.
ModuleCat.finsuppCoconedefMathlib.Algebra.Category.ModuleCat.Colimits, function or constant
Wording
the finitely supported function cocone of M and x1 (from the name)
English
Let $R$, $M$ and $x_{1}$ be sets. Then the finitely supported function cocone of $M$ and $x_{1}$ is a cofan of the function that maps $x_{4}$ to $\operatorname{of}$ applied to $R$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $R$ and $\FinsuppMACRoQ {x_{1}}{M}$ and the function that maps $i$ to the module category of $\operatorname{lsingle}$ applied to $i$.
ModuleCat.finsuppCoconeIsColimitdefMathlib.Algebra.Category.ModuleCat.Colimits, function or constant
Wording
no wording
English
Let $R$, $M$ and $x_{1}$ be sets. Then $\operatorname{finsuppCoconeIsColimit}$ applied to $R$, $M$ and $x_{1}$ is an element of $\operatorname{IsColimit}$ applied to the finitely supported function cocone of $M$ and $x_{1}$.

Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

CommRingCat.KaehlerDifferentialdefMathlib.Algebra.Category.ModuleCat.Differentials.Basic, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $A$ and $B$. Then $\operatorname{KaehlerDifferential}$ applied to $f$ is a module category of the set of carriers of $B$ defined as $\operatorname{of}$ applied to the set of carriers of $B$ and $\mathrm{KaehlerDifferential}$ applied to the set of carriers of $A$ and the set of carriers of $B$.
CommRingCat.KaehlerDifferential.DdefMathlib.Algebra.Category.ModuleCat.Differentials.Basic, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $A$ and $B$. Then $\operatorname{D}$ applied to $f$ is a derivation of $\operatorname{KaehlerDifferential}$ applied to $f$ and $f$.
CommRingCat.KaehlerDifferential.ddefMathlib.Algebra.Category.ModuleCat.Differentials.Basic, function or constant
Wording
no wording
English
Let $b$ be a carrier of $B$. Then $\operatorname{d}$ applied to $b$ is a carrier of $\operatorname{KaehlerDifferential}$ applied to $f$ defined as $\operatorname{d}$ applied to $\operatorname{D}$ applied to $f$ and $b$.
CommRingCat.KaehlerDifferential.mapdefMathlib.Algebra.Category.ModuleCat.Differentials.Basic, function or constant
Wording
the map of fac (from the docstring)
English
Assume that the composition of $g$ and $\mathrm{f'}$ is equal to the composition of $f$ and $\mathrm{g'}$. Then the map of $\mathrm{fac}$ is a homomorphism of $\operatorname{KaehlerDifferential}$ applied to $f$ and the action of $\operatorname{restrictScalars}$ applied to the underlying ring hom of $\mathrm{g'}$ and $\operatorname{KaehlerDifferential}$ applied to $\mathrm{f'}$.
ModuleCat.DerivationdefMathlib.Algebra.Category.ModuleCat.Differentials.Basic, type
Wording
derivation of M and f (from the name)
English
Let $M$ be a module category of the set of carriers of $B$. Let $f$ be a homomorphism of $A$ and $B$. Then a derivation of $M$ and $f$ is an element of the function that maps $M$ and $f$ to the set of derivations of the set of carriers of $B$ and the set of carriers of $M$.
ModuleCat.Derivation.ddefMathlib.Algebra.Category.ModuleCat.Differentials.Basic, function or constant
Wording
no wording
English
Let $D$ be a derivation of $M$ and $f$. Let $b$ be a carrier of $B$. Then $\operatorname{d}$ applied to $D$ and $b$ is a carrier of $M$ defined as $\operatorname{toLinearMap}$ applied to $D$ and $b$.
ModuleCat.Derivation.descdefMathlib.Algebra.Category.ModuleCat.Differentials.Basic, function or constant
Wording
no wording
English
Let $D$ be a derivation of $M$ and $f$. Then $\operatorname{desc}$ applied to $D$ is a homomorphism of $\operatorname{KaehlerDifferential}$ applied to $f$ and $M$ defined as the module category of $\operatorname{liftKaehlerDifferential}$ applied to $D$.
ModuleCat.Derivation.mkdefMathlib.Algebra.Category.ModuleCat.Differentials.Basic, function or constant
Wording
no wording
English
Let $d$ be a function from carriers of $B$ to carriers of $M$ such that $\mathrm{autoParam}$ holds for the proposition that for all carriers $b_{1}$ of $B$, for all carriers $\mathrm{b'1}$ of $B$, $\EqtMACRoH {d (b_{1} + \mathrm{b'1})}{d (b_{1})+ d (\mathrm{b'1})}$ and $\mathrm{ModuleCat\_\_Derivation\_\_mk\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for the proposition that for all carriers $b$ of $B$, for all carriers $\mathrm{b'}$ of $B$, $\EqtMACRoH {d (b \times \mathrm{b'})}{\HSMulhSMulMACRoAL {b}{d (\mathrm{b'})}+ \HSMulhSMulMACRoAL {\mathrm{b'}}{d (b)}}$ and $\mathrm{ModuleCat\_\_Derivation\_\_mk\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for the proposition that for all carriers $a$ of $A$, $\EqtMACRoH {d (\operatorname{hom} (f , a))}{0}$ and $\mathrm{ModuleCat\_\_Derivation\_\_mk\_\_\_auto\_5}$. Then $\operatorname{mk}$ applied to $d$, $\mathrm{d\_add}$, $\mathrm{d\_mul}$ and $\mathrm{d\_map}$ is a derivation of $M$ and $f$.

Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

PresheafOfModulesOfCommRing.DerivationstructureMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, type
Wording
derivation of M and x2 (from the name)
English
Let $M$ be a presheaf of module of commutative ring of $R$. Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Then the derivations of $M$ and $x_{2}$ are a basic type.
PresheafOfModulesOfCommRing.Derivation'defMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, type
Wording
derivation of M and x1 (from the name)
English
Let $M$ be a presheaf of module of commutative ring of $R$. Let $x_{1}$ be a homomorphism of $\mathrm{S'}$ and $R$. Then a derivation of $M$ and $x_{1}$ is an element of the function that maps $M$ and $x_{1}$ to the set of derivations of $M$ and $x_{1}$.
PresheafOfModulesOfCommRing.Derivation'.Universal.mkdefMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, function or constant
Wording
no wording
English
Let $\mathrm{desc}$ be a function from presheafs of module of commutative ring $\mathrm{M'2}$ of $R$ and derivations of $\mathrm{M'2}$ and $x_{1}$ to homomorphisms of $M$ and $\mathrm{M'2}$ such that for all presheafs of module of commutative ring $\mathrm{M'1}$ of $R$, for all derivations $\mathrm{d'}$ of $\mathrm{M'1}$ and $x_{1}$, the postcomposition of $d$ and $\mathrm{desc}$ applied to $\mathrm{M'1}$ and $\mathrm{d'}$ is equal to $\mathrm{d'}$. Assume that for all presheafs of module of commutative ring $\mathrm{M'}$ of $R$, for all homomorphisms $x_{2}$ and $x_{3}$ of $M$ and $\mathrm{M'}$, if the postcomposition of $d$ and $x_{2}$ is equal to the postcomposition of $d$ and $x_{3}$, then $\EqtMACRoH {x_{2}}{x_{3}}$. Then $\operatorname{mk}$ applied to $\mathrm{M'2}$, $\mathrm{desc}$, $\mathrm{fac}$ and $\mathrm{postcomp\_injective}$ is an element of $\operatorname{Universal}$ applied to $d$ defined as the function that maps $\mathrm{postcomp\_injective}$ to $\operatorname{mk}$ applied to the function that maps $x_{2}$ to $\mathrm{M'2}$ applied to $x_{2}$, the function that maps $x_{3}$ to $\mathrm{desc}$ applied to $x_{3}$, the function that maps $x_{4}$ to $\mathrm{fac}$ applied to $x_{4}$ and $\mathrm{postcomp\_injective}$.
PresheafOfModulesOfCommRing.Derivation'.appdefMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, function or constant
Wording
the derivation relative to the morphism of commutative rings of d and X (from the docstring)
English
Let $d$ be a derivation of $M$ and $x_{1}$. Let $X$ be an opposite of $D$. Then the derivation relative to the morphism of commutative rings of $d$ and $X$ is a derivation of the object of $M$ and $X$ and the component of $x_{1}$ and $X$.
PresheafOfModulesOfCommRing.Derivation'.mkdefMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, function or constant
Wording
no wording
English
Let $d$ be a function from opposites $X_{1}$ of $D$ to derivations of the object of $M$ and $X_{1}$ and the component of $x_{1}$ and $X_{1}$ such that for all opposites $X$ and $Y$ of $D$, for all homomorphisms $f$ of $X$ and $Y$, for all carriers $x_{2}$ of the action of $R$ and $X$, $\operatorname{d}$ applied to $d$ applied to $Y$ and $\operatorname{hom}$ applied to the map of $R$ and $f$ and $x_{2}$ is equal to $\operatorname{hom}$ applied to the restriction map of $M$ and $f$ and $\operatorname{d}$ applied to $d$ applied to $X$ and $x_{2}$. Then $\operatorname{mk}$ applied to $X_{1}$, $d$ and $\mathrm{d\_map}$ is a derivation of $M$ and $x_{1}$.
PresheafOfModulesOfCommRing.Derivation.UniversalstructureMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, type
Wording
no wording
English
Let $d$ be a derivation of $M$ and $x_{2}$. Then the elements of $\operatorname{Universal}$ applied to $d$ are a basic type.
PresheafOfModulesOfCommRing.Derivation.Universal.descdefMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an element of $\operatorname{Universal}$ applied to $d$. Let $\mathrm{d'}$ be a derivation of $\mathrm{M'}$ and $x_{2}$. Then $\operatorname{desc}$ applied to $\mathrm{self}$ and $\mathrm{d'}$ is a homomorphism of $M$ and $\mathrm{M'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $\mathrm{d'}$.
PresheafOfModulesOfCommRing.Derivation.ddefMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a derivation of $M$ and $x_{2}$. Then $\operatorname{d}$ applied to $\mathrm{self}$ is an additive monoid homomorphism of the set of carriers of the action of $R$ and $X$ and the set of carriers of the object of $M$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
PresheafOfModulesOfCommRing.Derivation.postcompdefMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, function or constant
Wording
the postcomposition of d and f (from the docstring)
English
Let $d$ be a derivation of $M$ and $x_{2}$. Let $f$ be a homomorphism of $M$ and $N$. Then the postcomposition of $d$ and $f$ is a derivation of $N$ and $x_{2}$.
PresheafOfModulesOfCommRing.DifferentialsConstruction.derivation'defMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, function or constant
Wording
the universal derivation of x1 (from the docstring)
English
Let $x_{1}$ be a homomorphism of $\mathrm{S'}$ and $R$. Then the universal derivation of $x_{1}$ is a derivation of the relative differential of $x_{1}$ and $x_{1}$.
PresheafOfModulesOfCommRing.DifferentialsConstruction.isUniversal'defMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, function or constant
Wording
no wording
English
Let $x_{1}$ be a homomorphism of $\mathrm{S'}$ and $R$. Then $\operatorname{isUniversal'}$ applied to $x_{1}$ is an element of $\operatorname{Universal}$ applied to the universal derivation of $x_{1}$.
PresheafOfModulesOfCommRing.DifferentialsConstruction.relativeDifferentials'defMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, function or constant
Wording
the relative differential of x1 (from the name)
English
Let $x_{1}$ be a homomorphism of $\mathrm{S'}$ and $R$. Then the relative differential of $x_{1}$ is a presheaf of module of commutative ring of $R$.
PresheafOfModulesOfCommRing.HasDifferentialsclassMathlib.Algebra.Category.ModuleCat.Differentials.Presheaf, predicate
Wording
x2 has differentials (from the name)
English
Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Then we can say that $x_{2}$ has differentials.

Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting

ModuleCat.projectiveShortComplexdefMathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting, function or constant
Wording
the standard short complex of M (from the docstring)
English
Let $M$ be a module category of $R$. Then the standard short complex of $M$ is a short complex of the set of module categories of $R$ defined as the short complex kernel of $\operatorname{constr}$ applied to $\operatorname{ofRepr}$ applied to the linear equivalence of the linear equivalence of $R$ and $R$, $\Natural$ and $\mathrm{id}$.

Mathlib.Algebra.Category.ModuleCat.ExteriorPower

ModuleCat.AlternatingMapdefMathlib.Algebra.Category.ModuleCat.ExteriorPower, type
Wording
alternating map of N and n (from the name)
English
Let $M$ and $N$ be module categories of $R$. Let $n$ be a natural number. Then an alternating map of $N$ and $n$ is an element of the function that maps $M$, $N$ and $n$ to the set of alternating maps of the set of carriers of $N$ and $\mathrm{Fin}$ applied to $n$.
ModuleCat.AlternatingMap.postcompdefMathlib.Algebra.Category.ModuleCat.ExteriorPower, function or constant
Wording
the postcomposition of x1 and g (from the docstring)
English
Let $x_{1}$ be an alternating map of $N$ and $n$. Let $g$ be a homomorphism of $N$ and $\mathrm{N'}$. Then the postcomposition of $x_{1}$ and $g$ is an alternating map of $\mathrm{N'}$ and $n$ defined as the composition alternating map of the homomorphism of $g$ and $x_{1}$.
ModuleCat.exteriorPowerdefMathlib.Algebra.Category.ModuleCat.ExteriorPower, function or constant
Wording
the exterior power of M and n (from the docstring)
English
Let $M$ be a module category of $R$. Let $n$ be an element of $\Natural$. Then the exterior power of $M$ and $n$ is a module category of $R$ defined as $\operatorname{of}$ applied to $R$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{1}})}$.
ModuleCat.exteriorPower.descdefMathlib.Algebra.Category.ModuleCat.ExteriorPower, function or constant
Wording
no wording
English
Let $x_{1}$ be an alternating map of $N$ and $n$. Then $\operatorname{desc}$ applied to $x_{1}$ is a homomorphism of the exterior power of $M$ and $n$ and $N$ defined as the module category of $\operatorname{alternatingMapLinearEquiv}$ applied to $x_{1}$.
ModuleCat.exteriorPower.functordefMathlib.Algebra.Category.ModuleCat.ExteriorPower, function or constant
Wording
the functor of R and n (from the docstring)
English
Let $R$ be a set. Let $n$ be a natural number. Then the functor of $R$ and $n$ is a functor of the set of module categories of $R$ and the set of module categories of $R$.
ModuleCat.exteriorPower.iso₀defMathlib.Algebra.Category.ModuleCat.ExteriorPower, function or constant
Wording
the isomorphism of M (from the docstring)
English
Let $M$ be a module category of $R$. Then the isomorphism of $M$ is an isomorphism of the exterior power of $M$ and $0$ and $\operatorname{of}$ applied to $R$ and $R$ defined as the module isomorphism of the linear equivalence of $R$ and the set of carriers of $M$.
ModuleCat.exteriorPower.iso₁defMathlib.Algebra.Category.ModuleCat.ExteriorPower, function or constant
Wording
the isomorphism of M (from the docstring)
English
Let $M$ be a module category of $R$. Then the isomorphism of $M$ is an isomorphism of the exterior power of $M$ and $1$ and $M$ defined as the module isomorphism of the linear equivalence of $R$ and the set of carriers of $M$.
ModuleCat.exteriorPower.mapdefMathlib.Algebra.Category.ModuleCat.ExteriorPower, function or constant
Wording
the map of f and n (from the name)
English
Let $f$ be a homomorphism of $M$ and $N$. Let $n$ be a natural number. Then the map of $f$ and $n$ is a homomorphism of the exterior power of $M$ and $n$ and the exterior power of $N$ and $n$ defined as the module category of the map of $n$ and the homomorphism of $f$.
ModuleCat.exteriorPower.mkdefMathlib.Algebra.Category.ModuleCat.ExteriorPower, function or constant
Wording
no wording
English
$\operatorname{mk}$ is an alternating map of the exterior power of $M$ and $n$ and $n$ defined as $\mathrm{exteriorPower\_\_\_u3b9\_Multi}$ applied to $R$ and $n$.
ModuleCat.exteriorPower.natIso₀defMathlib.Algebra.Category.ModuleCat.ExteriorPower, function or constant
Wording
the natural isomorphism of R (from the docstring)
English
Let $R$ be a set. Then the natural isomorphism of $R$ is an isomorphism of the functor of $R$ and $0$ and the action of the constant of the set of module categories of $R$ and $\operatorname{of}$ applied to $R$ and $R$.
ModuleCat.exteriorPower.natIso₁defMathlib.Algebra.Category.ModuleCat.ExteriorPower, function or constant
Wording
the natural isomorphism of R (from the docstring)
English
Let $R$ be a set. Then the natural isomorphism of $R$ is an isomorphism of the functor of $R$ and $1$ and the identity of the set of module categories of $R$.

Mathlib.Algebra.Category.ModuleCat.FilteredColimits

ModuleCat.FilteredColimits.MdefMathlib.Algebra.Category.ModuleCat.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Then $\operatorname{M}$ applied to $F$ is an additive commutative group category defined as the colimit of the composition of $F$ and the forgetful functor of the set of module categories of $R$ and the set of additive commutative group categories.
ModuleCat.FilteredColimits.M.mkdefMathlib.Algebra.Category.ModuleCat.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Let $x_{2}$ be an element of $\Sigma$ applied to the function that maps $j$ to the set of carriers of the action of $F$ and $j$. Then $\operatorname{mk}$ applied to $F$ and $x_{2}$ is a carrier of $\operatorname{M}$ applied to $F$ defined as the inclusion colimit type of $\operatorname{fst}$ applied to $x_{2}$ and $\operatorname{snd}$ applied to $x_{2}$.
ModuleCat.FilteredColimits.coconeMorphismdefMathlib.Algebra.Category.ModuleCat.FilteredColimits, function or constant
Wording
the cocone morphism of F and j (from the name)
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Let $j$ be an element of $J$. Then the cocone morphism of $F$ and $j$ is a homomorphism of the action of $F$ and $j$ and the colimit of $F$.
ModuleCat.FilteredColimits.colimitdefMathlib.Algebra.Category.ModuleCat.FilteredColimits, function or constant
Wording
the colimit of F (from the name)
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Then the colimit of $F$ is a module category of $R$ defined as $\operatorname{of}$ applied to $R$ and the set of carriers of $\operatorname{M}$ applied to $F$.
ModuleCat.FilteredColimits.colimitCoconedefMathlib.Algebra.Category.ModuleCat.FilteredColimits, function or constant
Wording
the colimit cocone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Then the colimit cocone of $F$ is a cocone of $F$.
ModuleCat.FilteredColimits.colimitCoconeIsColimitdefMathlib.Algebra.Category.ModuleCat.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.
ModuleCat.FilteredColimits.colimitDescdefMathlib.Algebra.Category.ModuleCat.FilteredColimits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Let $t$ be a cocone of $F$. Then $\operatorname{colimitDesc}$ applied to $F$ and $t$ is a homomorphism of the colimit of $F$ and $\operatorname{pt}$ applied to $t$.

Mathlib.Algebra.Category.ModuleCat.Free

ModuleCat.Basis.ofShortExactdefMathlib.Algebra.Category.ModuleCat.Free, function or constant
Wording
the basis of bP and #3 (from the name)
English
Assume that $\operatorname{ShortExact}$ holds for $S$. Let $\mathrm{bN}$ be a basis of $R$ and the set of carriers of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$. Let $\mathrm{bP}$ be a basis of $R$ and the set of carriers of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$. Then the basis of $\mathrm{bN}$ and $\mathrm{bP}$ is a basis of $R$ and the set of carriers of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$.

Mathlib.Algebra.Category.ModuleCat.Images

ModuleCat.factorThruImagedefMathlib.Algebra.Category.ModuleCat.Images, function or constant
Wording
the corestriction map to the image of f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the corestriction map to the image of $f$ is a homomorphism of $G$ and the image in $f$ defined as the module category of $\operatorname{rangeRestrict}$ applied to the homomorphism of $f$.
ModuleCat.imagedefMathlib.Algebra.Category.ModuleCat.Images, function or constant
Wording
the image in f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the image in $f$ is a module category of $R$ defined as $\operatorname{of}$ applied to $R$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{hom} (f))}{x_{1}})}$.
ModuleCat.image.liftdefMathlib.Algebra.Category.ModuleCat.Images, function or constant
Wording
the lift of #1 (from the name)
English
Let $\mathrm{F'}$ be a monomorphism factorisation of $f$. Then the lift of $\mathrm{F'}$ is a homomorphism of the image in $f$ and $\operatorname{I}$ applied to $\mathrm{F'}$.
ModuleCat.image.ιdefMathlib.Algebra.Category.ModuleCat.Images, function or constant
Wording
the inclusion of f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the inclusion of $f$ is a homomorphism of the image in $f$ and $H$ defined as the module category of the subtype of the range of the homomorphism of $f$.
ModuleCat.imageIsoRangedefMathlib.Algebra.Category.ModuleCat.Images, function or constant
Wording
the categorical image in f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the categorical image in $f$ is an isomorphism of the categorical image of $f$ and $\operatorname{of}$ applied to $R$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{hom} (f))}{x_{1}})}$ defined as the isomorphism extension of $\operatorname{isImage}$ applied to $f$ and $\operatorname{isImage}$ applied to $f$.
ModuleCat.isImagedefMathlib.Algebra.Category.ModuleCat.Images, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $G$ and $H$. Then $\operatorname{isImage}$ applied to $f$ is an element of $\operatorname{IsImage}$ applied to the factorisation in $f$ defined as $\operatorname{mk}$ applied to $\operatorname{lift}$ and $\mathrm{ModuleCat\_\_image\_\_lift\_fac}$.
ModuleCat.monoFactorisationdefMathlib.Algebra.Category.ModuleCat.Images, function or constant
Wording
the factorisation in f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the factorisation in $f$ is a monomorphism factorisation of $f$.

Mathlib.Algebra.Category.ModuleCat.Kernels

ModuleCat.cokernelCoconedefMathlib.Algebra.Category.ModuleCat.Kernels, function or constant
Wording
the cokernel cocone induced by the projection onto the quotient of f (from the docstring)
English
Let $f$ be a homomorphism of $M$ and $N$. Then the cokernel cocone induced by the projection onto the quotient of $f$ is a cokernel cofork of $f$.
ModuleCat.cokernelIsColimitdefMathlib.Algebra.Category.ModuleCat.Kernels, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $M$ and $N$. Then $\operatorname{cokernelIsColimit}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cocone induced by the projection onto the quotient of $f$.
ModuleCat.cokernelIsoRangeQuotientdefMathlib.Algebra.Category.ModuleCat.Kernels, function or constant
Wording
the categorical cokernel in f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the categorical cokernel in $f$ is an isomorphism of the cokernel of $f$ and $\operatorname{of}$ applied to $R$ and the set of quotients of the set of carriers of $H$ and the range of the homomorphism of $f$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the cokernel cocone induced by the projection onto the quotient of $f$ and $\operatorname{cokernelIsColimit}$ applied to $f$.
ModuleCat.isColimitCokernelCoforkdefMathlib.Algebra.Category.ModuleCat.Kernels, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $M$ and $N$. Let $g$ be a homomorphism of $N$ and $P$ such that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$ and $\operatorname{coe}$ applied to the homomorphism of $g$ and $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $g$. Then $\operatorname{isColimitCokernelCofork}$ applied to $f$, $g$, $H$ and $h$ is an element of $\operatorname{IsColimit}$ applied to the projection of $g$ and $\mathrm{ModuleCat\_\_isLimitKernelFork\_\_\_proof\_1}$ applied to $f$, $g$ and $H$.
ModuleCat.isLimitKernelForkdefMathlib.Algebra.Category.ModuleCat.Kernels, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $M$ and $N$. Let $g$ be a homomorphism of $N$ and $P$ such that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$ and $\operatorname{coe}$ applied to the homomorphism of $g$. Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is injective. Then $\operatorname{isLimitKernelFork}$ applied to $f$, $g$, $H$ and $h$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $\mathrm{ModuleCat\_\_isLimitKernelFork\_\_\_proof\_1}$ applied to $f$, $g$ and $H$.
ModuleCat.kernelConedefMathlib.Algebra.Category.ModuleCat.Kernels, function or constant
Wording
the kernel cone induced by the concrete kernel of f (from the docstring)
English
Let $f$ be a homomorphism of $M$ and $N$. Then the kernel cone induced by the concrete kernel of $f$ is a kernel fork of $f$.
ModuleCat.kernelIsLimitdefMathlib.Algebra.Category.ModuleCat.Kernels, function or constant
Wording
the kernel of f (from the docstring)
English
Let $f$ be a homomorphism of $M$ and $N$. Then the kernel of $f$ is an element of $\operatorname{IsLimit}$ applied to the kernel cone induced by the concrete kernel of $f$.
ModuleCat.kernelIsoKerdefMathlib.Algebra.Category.ModuleCat.Kernels, function or constant
Wording
the categorical kernel in f (from the docstring)
English
Let $f$ be a homomorphism of $G$ and $H$. Then the categorical kernel in $f$ is an isomorphism of the kernel of $f$ and $\operatorname{of}$ applied to $R$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{hom} (f))}{x_{1}})}$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the kernel cone induced by the concrete kernel of $f$ and the kernel of $f$.

Mathlib.Algebra.Category.ModuleCat.LeftResolution

ModuleCat.projectiveResolutiondefMathlib.Algebra.Category.ModuleCat.LeftResolution, function or constant
Wording
the projective resolution of R (from the name)
English
Let $R$ be a set. Then the projective resolution of $R$ is a left resolution of the inclusion of $\operatorname{isProjective}$ applied to the set of module categories of $R$.

Mathlib.Algebra.Category.ModuleCat.Limits

ModuleCat.HasLimits.limitConedefMathlib.Algebra.Category.ModuleCat.Limits, function or constant
Wording
the limit cone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Then the limit cone of $F$ is a cone of $F$.
ModuleCat.HasLimits.limitConeIsLimitdefMathlib.Algebra.Category.ModuleCat.Limits, function or constant
Wording
no wording
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Then $\operatorname{limitConeIsLimit}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$.
ModuleCat.directLimitCoconedefMathlib.Algebra.Category.ModuleCat.Limits, function or constant
Wording
the direct limit cocone of G and f (from the name)
English
Let $G$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Then the direct limit cocone of $G$ and $i$ is a cocone of the direct limit diagram of $G$ and $f$.
ModuleCat.directLimitDiagramdefMathlib.Algebra.Category.ModuleCat.Limits, function or constant
Wording
the direct limit diagram of G and f (from the name)
English
Let $G$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Then the direct limit diagram of $G$ and $i$ is a functor of $x_{1}$ and the set of module categories of $R$.
ModuleCat.directLimitIsColimitdefMathlib.Algebra.Category.ModuleCat.Limits, function or constant
Wording
no wording
English
Let $G$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Then $\operatorname{directLimitIsColimit}$ applied to $G$, $i$, $j$ and $f$ is an element of $\operatorname{IsColimit}$ applied to the direct limit cocone of $G$ and $f$.
ModuleCat.limitπLinearMapdefMathlib.Algebra.Category.ModuleCat.Limits, function or constant
Wording
the limit projection linear map of F and j (from the name)
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Let $j$ be an element of $J$. Then the limit projection linear map of $F$ and $j$ is a linear map of $\operatorname{pt}$ applied to the limit cone of the composition of $F$ and the forgetful functor of the set of module categories of $R$ and the action of the composition of $F$ and the forgetful functor of the set of module categories of $R$ and $j$.
ModuleCat.sectionsSubmoduledefMathlib.Algebra.Category.ModuleCat.Limits, function or constant
Wording
the section submodule of F (from the name)
English
Let $F$ be a functor of $J$ and the set of module categories of $R$. Then the section submodule of $F$ is a submodule of $R$ and the set of functions from elements $j$ of $J$ to carriers of the action of $F$ and $j$.

Mathlib.Algebra.Category.ModuleCat.Localization

ModuleCat.localizedModuledefMathlib.Algebra.Category.ModuleCat.Localization, function or constant
Wording
the localized module of M and S (from the name)
English
Let $M$ be a module category of $R$. Let $S$ be a submonoid of $R$. Then the localized module of $M$ and $S$ is a module category of the set of localizations of $S$ defined as $\operatorname{of}$ applied to the set of localizations of $S$ and the set of shrinks of the set of localized modules of $S$ and the set of carriers of $M$.
ModuleCat.localizedModuleFunctordefMathlib.Algebra.Category.ModuleCat.Localization, function or constant
Wording
the functor of S (from the docstring)
English
Let $S$ be a submonoid of $R$. Then the functor of $S$ is a functor of the set of module categories of $R$ and the set of module categories of the set of localizations of $S$.
ModuleCat.localizedModuleMapdefMathlib.Algebra.Category.ModuleCat.Localization, function or constant
Wording
the localized module map of S and f (from the name)
English
Let $S$ be a submonoid of $R$. Let $f$ be a homomorphism of $M$ and $N$. Then the localized module map of $S$ and $f$ is a homomorphism of the localized module of $M$ and $S$ and the localized module of $N$ and $S$ defined as the module category of $\operatorname{mapExtendScalars}$ applied to $S$, the linear map of $M$ and $S$, the linear map of $N$ and $S$, the set of localizations of $S$ and the homomorphism of $f$.
ModuleCat.localizedModuleMkLinearMapdefMathlib.Algebra.Category.ModuleCat.Localization, function or constant
Wording
the linear map of M and S (from the docstring)
English
Let $M$ be a module category of $R$. Let $S$ be a submonoid of $R$. Then the linear map of $M$ and $S$ is a linear map of the set of carriers of $M$ and the set of carriers of the localized module of $M$ and $S$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the linear equivalence of $R$ and the set of localized modules of $S$ and the set of carriers of $M$ and the linear map of $S$ and the set of carriers of $M$.

‹ previous next ›