Definitions: Mathlib.Algebra, part 3 of 17

the tensor lift of f (from the name)

Let $f$ be a function from carriers of $x_{1}$ and carriers of $x_{2}$ to carriers of $x_{3}$ such that for all carriers $x_{6}$ of $x_{1}$, for all carriers $x_{7}$ of $x_{1}$, for all carriers $n_{2}$ of $x_{2}$, $\EqtMACRoH {f (x_{6} + x_{7} , n_{2})}{f (x_{6} , n_{2})+ f (x_{7} , n_{2})}$, for all elements $a_{1}$ of $R$, for all carriers $m_{2}$ of $x_{1}$, for all carriers $n_{1}$ of $x_{2}$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {a_{1}}{m_{2}}, n_{1})}{\HSMulhSMulMACRoAL {a_{1}}{f (m_{2} , n_{1})}}$, for all carriers $m_{1}$ of $x_{1}$, for all carriers $x_{4}$ of $x_{2}$, for all carriers $x_{5}$ of $x_{2}$, $\EqtMACRoH {f (m_{1} , x_{4} + x_{5})}{f (m_{1} , x_{4})+ f (m_{1} , x_{5})}$ and for all elements $a$ of $R$, for all carriers $m$ of $x_{1}$, for all carriers $n$ of $x_{2}$, $\EqtMACRoH {f (m , \HSMulhSMulMACRoAL {a}{n})}{\HSMulhSMulMACRoAL {a}{f (m , n)}}$. Then the tensor lift of $f$ is a homomorphism of the tensor object of $x_{1}$ and $x_{2}$ and $x_{3}$ defined as the module category of the lift of $\mathrm{LinearMap\_\_mk\_u2082\_}$ applied to $R$, $f$, $h$, $h_{1}$, $h_{2}$ and $h_{3}$.

the associator of N and K (from the name)

Let $M$, $N$ and $K$ be semimodule categories of $R$. Then the associator of $N$ and $K$ is an isomorphism of the tensor object of the tensor object of $M$ and $N$ and $K$ and the tensor object of $M$ and the tensor object of $N$ and $K$ defined as the module isomorphism of the associator of the set of carriers of $N$ and the set of carriers of $K$.

the left unitor of M (from the name)

Let $M$ be a semimodule category of $R$. Then the left unitor of $M$ is an isomorphism of $\operatorname{of}$ applied to $R$ and the set of tensor products of $R$ and the set of carriers of $M$ and $M$ defined as the module isomorphism of $\operatorname{lid}$ applied to $R$ and the set of carriers of $M$.

the right unitor of M (from the name)

Let $M$ be a semimodule category of $R$. Then the right unitor of $M$ is an isomorphism of $\operatorname{of}$ applied to $R$ and the set of tensor products of the set of carriers of $M$ and $R$ and $M$ defined as the module isomorphism of $\operatorname{rid}$ applied to $R$ and the set of carriers of $M$.

the tensor homomorphism of f and g (from the name)

Let $f$ be a homomorphism of $M$ and $N$. Let $g$ be a homomorphism of $\mathrm{M'}$ and $\mathrm{N'}$. Then the tensor homomorphism of $f$ and $g$ is a homomorphism of the tensor object of $M$ and $\mathrm{M'}$ and the tensor object of $N$ and $\mathrm{N'}$ defined as the semimodule category of the tensor product of the homomorphism of $f$ and the homomorphism of $g$.

the tensor lift of f (from the name)

Let $f$ be a function from carriers of $x_{1}$ and carriers of $x_{2}$ to carriers of $x_{3}$ such that for all carriers $x_{6}$ of $x_{1}$, for all carriers $x_{7}$ of $x_{1}$, for all carriers $n_{2}$ of $x_{2}$, $\EqtMACRoH {f (x_{6} + x_{7} , n_{2})}{f (x_{6} , n_{2})+ f (x_{7} , n_{2})}$, for all elements $a_{1}$ of $R$, for all carriers $m_{2}$ of $x_{1}$, for all carriers $n_{1}$ of $x_{2}$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {a_{1}}{m_{2}}, n_{1})}{\HSMulhSMulMACRoAL {a_{1}}{f (m_{2} , n_{1})}}$, for all carriers $m_{1}$ of $x_{1}$, for all carriers $x_{4}$ of $x_{2}$, for all carriers $x_{5}$ of $x_{2}$, $\EqtMACRoH {f (m_{1} , x_{4} + x_{5})}{f (m_{1} , x_{4})+ f (m_{1} , x_{5})}$ and for all elements $a$ of $R$, for all carriers $m$ of $x_{1}$, for all carriers $n$ of $x_{2}$, $\EqtMACRoH {f (m , \HSMulhSMulMACRoAL {a}{n})}{\HSMulhSMulMACRoAL {a}{f (m , n)}}$. Then the tensor lift of $f$ is a homomorphism of the tensor object of $x_{1}$ and $x_{2}$ and $x_{3}$ defined as the semimodule category of the lift of $\mathrm{LinearMap\_\_mk\_u2082\_}$ applied to $R$, $f$, $h$, $h_{1}$, $h_{2}$ and $h_{3}$.

the tensor object of M and N (from the name)

Let $M$ and $N$ be semimodule categories of $R$. Then the tensor object of $M$ and $N$ is a semimodule category of $R$ defined as $\operatorname{of}$ applied to $R$ and the set of tensor products of the set of carriers of $M$ and the set of carriers of $N$.

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

Let $M$ be a semimodule category of $R$. Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Then the left whisker of $M$ and $f$ is a homomorphism of the tensor object of $M$ and $x_{1}$ and the tensor object of $M$ and $x_{2}$ defined as the semimodule category of the tensor of the set of carriers of $M$ and the homomorphism of $f$.

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

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $N$ be a semimodule category of $R$. Then the right whisker of $f$ and $N$ is a homomorphism of the tensor object of $x_{1}$ and $N$ and the tensor object of $x_{2}$ and $N$ defined as the semimodule category of the tensor of the set of carriers of $N$ and the homomorphism of $f$.

the braiding of M and N (from the name)

Let $M$ and $N$ be semimodule categories of $R$. Then the braiding of $M$ and $N$ is an isomorphism of the tensor object of $M$ and $N$ and the tensor object of $N$ and $M$ defined as the module isomorphism of $\operatorname{comm}$ applied to $R$, the set of carriers of $M$ and the set of carriers of $N$.

presheaf of module of R (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of rings. Then the presheafs of module of $R$ are a basic type.

homomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be presheafs of module of $R$. Then the homomorphisms of $x_{1}$ and $x_{2}$ are a basic type.

the homomorphism of self and X (from the name)

Let $\mathrm{self}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $X$ be an opposite of $C$. Then the homomorphism of $\mathrm{self}$ and $X$ is a homomorphism of the object of $x_{1}$ and $X$ and the object of $x_{2}$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $X$.

the evaluation of R and X (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of rings. Let $X$ be an opposite of $C$. Then the evaluation of $R$ and $X$ is a functor of the set of presheafs of module of $R$ and the set of module categories of the set of carriers of the action of $R$ and $X$.

Let $X$ be an opposite of $C$. Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Then $\operatorname{forgetToPresheafModuleCat}$ applied to $X$ and $\mathrm{hX}$ is a functor of the set of presheafs of module of $R$ and the set of functors of the set of opposites of $C$ and the set of module categories of the set of carriers of the action of $R$ and $X$.

the homomorphism of x3 and h (from the name)

Let $x_{3}$ be a homomorphism of the presheaf of $x_{1}$ and the presheaf of $x_{2}$ such that for all opposites $X$ of $C$, for all carriers $r$ of the action of $R$ and $X$, for all carriers $m$ of the object of $x_{1}$ and $X$, $\EqtMACRoH {\operatorname{hom} (\operatorname{NatTrans} (x_{3} , X), \HSMulhSMulMACRoAL {r}{m})}{\HSMulhSMulMACRoAL {r}{\operatorname{hom} (\operatorname{NatTrans} (x_{3} , X), m)}}$. Then the homomorphism of $x_{3}$ and $h$ is a homomorphism of $x_{1}$ and $x_{2}$.

the isomorphism of app and X1 (from the name)

Let $\mathrm{app}$ be a function from opposites $X_{1}$ of $C$ to isomorphisms of the object of $x_{1}$ and $X_{1}$ and the object of $x_{2}$ and $X_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all opposites $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, the composition of the map of $x_{1}$ and $f$ and the map of $\operatorname{restrictScalars}$ applied to the homomorphism of the map of $R$ and $f$ and the homomorphism of $\mathrm{app}$ applied to $Y$ is equal to the composition of the homomorphism of $\mathrm{app}$ applied to $X$ and the map of $x_{2}$ and $f$ and $\mathrm{PresheafOfModules\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $X_{1}$ and $\mathrm{app}$ is an isomorphism of $x_{1}$ and $x_{2}$.

the map of self and f (from the name)

Let $\mathrm{self}$ be a presheaf of module of $R$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $\mathrm{self}$ and $f$ is a homomorphism of the object of $\mathrm{self}$ and $X$ and the action of $\operatorname{restrictScalars}$ applied to the homomorphism of the map of $R$ and $f$ and the object of $\mathrm{self}$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $f$.

the object of self and X (from the name)

Let $\mathrm{self}$ be a presheaf of module of $R$. Let $X$ be an opposite of $C$. Then the object of $\mathrm{self}$ and $X$ is a module category of the set of carriers of the action of $R$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $X$.

the presheaf of module of M and map_smul (from the name)

Let $M$ be a functor of the set of opposites of $C$ and the set of abelian groups such that for all opposites $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, for all carriers $r$ of the action of $R$ and $X$, for all carriers $m$ of the action of $M$ and $X$, $\EqtMACRoH {\operatorname{hom} (\operatorname{map} (M , f), \HSMulhSMulMACRoAL {r}{m})}{\HSMulhSMulMACRoAL {\operatorname{hom} (\operatorname{map} (R , f), r)}{\operatorname{hom} (\operatorname{map} (M , f), m)}}$. Then the presheaf of module of $M$ and $\mathrm{map\_smul}$ is a presheaf of module of $R$.

the presheaf of M (from the name)

Let $M$ be a presheaf of module of $R$. Then the presheaf of $M$ is a functor of the set of opposites of $C$ and the set of abelian groups.

the restriction of R and f (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of rings. Let $f$ be a homomorphism of $X$ and $Y$. Then the restriction of $R$ and $f$ is a homomorphism of the evaluation of $R$ and $X$ and the composition of the evaluation of $R$ and $Y$ and $\operatorname{restrictScalars}$ applied to the homomorphism of the map of $R$ and $f$.

the restriction map of M and f (from the docstring)

Let $M$ be a presheaf of module of $R$. Let $f$ be a homomorphism of $X$ and $Y$. Then the restriction map of $M$ and $f$ is a linear map of the set of carriers of the object of $M$ and $X$ and the set of carriers of the object of $M$ and $Y$.

section of M (from the name)

Let $M$ be a presheaf of module of $R$. Then a section of $M$ is an element of the function that maps $M$ to the set of elements of the section of the composition of the presheaf of $M$ and the forgetful functor of the set of abelian groups.

the evaluation of s and X (from the name)

Let $s$ be a section of $M$. Let $X$ be an opposite of $C$. Then the evaluation of $s$ and $X$ is a carrier of the object of $M$ and $X$ defined as $X$.

the map of f and s (from the docstring)

Let $f$ be a homomorphism of $M$ and $N$. Let $s$ be a section of $M$. Then the map of $f$ and $s$ is a section of $N$.

the section of s and X1 (from the name)

Let $s$ be a function from opposites $X_{1}$ of $C$ to carriers of the object of $M$ and $X_{1}$ such that for all opposites $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, $\operatorname{hom}$ applied to the map of $M$ and $f$ and $s$ applied to $X$ is equal to $s$ applied to $Y$. Then the section of $X_{1}$ and $s$ is a section of $M$ defined as the function that maps $\mathrm{hs}$ to $X_{1}$ applied to $\mathrm{hs}$.

the presheaf of R (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of rings. Then the presheaf of $R$ is a functor of the set of presheafs of module of $R$ and the set of functors of the set of opposites of $C$ and the set of abelian groups.

the unit of R (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of rings. Then the unit of $R$ is a presheaf of module of $R$.

the unit homomorphism equivalence of M (from the name)

Let $M$ be a presheaf of module of $R$. Then the unit homomorphism equivalence of $M$ is an equivalence from the set of homomorphisms of the unit of $R$ and $M$ to the set of sections of $M$.

Let $x_{1}$ be a homomorphism of $R$ and $\mathrm{R'}$. Then $\operatorname{restrictScalars}$ applied to $x_{1}$ is a functor of the set of presheafs of module of $\mathrm{R'}$ and the set of presheafs of module of $R$.

Let $x_{1}$ be a homomorphism of $R$ and $\mathrm{R'}$. Then $\operatorname{restrictScalarsCompToPresheaf}$ applied to $x_{1}$ is an isomorphism of the composition of $\operatorname{restrictScalars}$ applied to $x_{1}$ and the presheaf of $R$ and the presheaf of $\mathrm{R'}$ defined as the identity of the composition of $\operatorname{restrictScalars}$ applied to $x_{1}$ and the presheaf of $R$.

Let $\mathrm{M'}$ be a presheaf of module of $\mathrm{R'}$. Let $x_{1}$ be a homomorphism of $R$ and $\mathrm{R'}$. Then $\operatorname{restrictScalarsObj}$ applied to $\mathrm{M'}$ and $x_{1}$ is a presheaf of module of $R$.

module colimit of x1 and x2 (from the name)

Let $x_{1}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cR}$. Let $x_{2}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cM}$. Then a module colimit of $x_{1}$ and $x_{2}$ is an element of the function that maps $x_{1}$ and $x_{2}$ to the set of carriers of $\operatorname{pt}$ applied to $\mathrm{cM}$.

the cocone product of hcR and hcM (from the name)

Let $\mathrm{hcR}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cR}$. Let $\mathrm{hcM}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cM}$. Then the cocone product of $\mathrm{hcR}$ and $\mathrm{hcM}$ is a cocone of the tensor object of the composition of $R$ and the forgetful functor of the set of categories of rings and the composition of the presheaf of $M$ and the forgetful functor of the set of abelian groups.

the homomorphism equivalence of hcR and hcM (from the name)

Let $\mathrm{hcR}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cR}$. Let $\mathrm{hcM}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cM}$. Then the homomorphism equivalence of $\mathrm{hcR}$ and $\mathrm{hcM}$ is an additive equivalence of the set of homomorphisms of $\operatorname{of}$ applied to the set of carriers of $\operatorname{pt}$ applied to $\mathrm{cR}$ and the set of module colimits of $\mathrm{hcR}$ and $\mathrm{hcM}$ and $N$ and the set of homomorphisms of $M$ and the action of the constant functor of $\mathrm{cR}$ and $N$.

the map of f and #4 (from the name)

Let $\mathrm{hcR}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cR}$. Let $\mathrm{hcM}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cM}$. Let $\mathrm{hcM'}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cM'}$. Let $f$ be a homomorphism of $M$ and $\mathrm{M'}$. Then the map of $\mathrm{hcM'}$ and $f$ is a linear map of the set of module colimits of $\mathrm{hcR}$ and $\mathrm{hcM}$ and the set of module colimits of $\mathrm{hcR}$ and $\mathrm{hcM'}$.

the inclusion (from the name)

The inclusion is an additive monoid homomorphism of the set of carriers of the object of $M$ and $U$ and the set of module colimits of $\mathrm{hcR}$ and $\mathrm{hcM}$ defined as the homomorphism of the component of the inclusion of $\mathrm{cM}$ and $U$.

the inclusion of cR (from the name)

Let $\mathrm{cR}$ be a cocone of $R$. Then the inclusion of $\mathrm{cR}$ is a ring homomorphism of the set of carriers of the action of $R$ and $U$ and the set of carriers of $\operatorname{pt}$ applied to $\mathrm{cR}$ defined as the homomorphism of the component of the inclusion of $\mathrm{cR}$ and $U$.

the colimit adjunction of hcR (from the name)

Let $\mathrm{hcR}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cR}$. Then the colimit adjunction of $\mathrm{hcR}$ is an adjunction of the colimit functor of $\mathrm{hcR}$ and the constant functor of $\mathrm{cR}$.

the colimit functor of hcR (from the name)

Let $\mathrm{hcR}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cR}$. Then the colimit functor of $\mathrm{hcR}$ is a functor of the set of presheafs of module of $R$ and the set of module categories of the set of carriers of $\operatorname{pt}$ applied to $\mathrm{cR}$.

the constant functor of cR (from the name)

Let $\mathrm{cR}$ be a cocone of $R$. Then the constant functor of $\mathrm{cR}$ is a functor of the set of module categories of the set of carriers of $\operatorname{pt}$ applied to $\mathrm{cR}$ and the set of presheafs of module of $R$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of presheafs of module of $R$. Then the colimit cocone of $F$ is a cocone of $F$.

the colimit presheaf of F (from the name)

Let $F$ be a functor of $J$ and the set of presheafs of module of $R$. Then the colimit presheaf of $F$ is a presheaf of module of $R$.

Let $F$ be a functor of $J$ and the set of presheafs of module of $R$. Let $c$ be a cocone of $F$. Let $\mathrm{hc}$ be a function from opposites $X$ of $C$ to elements of $\operatorname{IsColimit}$ applied to the map cocone of the evaluation of $R$ and $X$ and $c$. Then $\operatorname{evaluationJointlyReflectsColimits}$ applied to $F$, $c$, $X$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$.

the cocone of F (from the docstring)

Let $F$ be a functor of $J$ and the set of presheafs of module of $R$. Then the cocone of $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$ defined as $\operatorname{evaluationJointlyReflectsColimits}$ applied to $F$, the colimit cocone of $F$ and the function that maps $x_{2}$ to $\operatorname{isColimit}$ applied to the composition of $F$ and the evaluation of $R$ and $x_{2}$.

the free of R (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of rings. Then the free of $R$ is a functor of the set of functors of the set of opposites of $C$ and the set of sets and the set of presheafs of module of $R$.

the free adjunction of R (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of rings. Then the free adjunction of $R$ is an adjunction of the free of $R$ and the composition of the presheaf of $R$ and the action of the right whiskering of the set of abelian groups and the set of sets and the forgetful functor of the set of abelian groups.

the free adjunction unit of R and F (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of rings. Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the free adjunction unit of $R$ and $F$ is a homomorphism of $F$ and the composition of the presheaf of the free object of $F$ and the forgetful functor of the set of abelian groups.

the free homomorphism equivalence (from the name)

The free homomorphism equivalence is an equivalence from the set of homomorphisms of the free object of $F$ and $G$ to the set of homomorphisms of $F$ and the composition of the presheaf of $G$ and the forgetful functor of the set of abelian groups.

the free object of F (from the name)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the free object of $F$ is a presheaf of module of $R$.

Let $x_{1}$ be a homomorphism of $F$ and the composition of the presheaf of $G$ and the forgetful functor of the set of abelian groups. Then $\operatorname{freeObjDesc}$ applied to $x_{1}$ is a homomorphism of the free object of $F$ and $G$.

element of M (from the name)

Let $M$ be a presheaf of module of $R$. Then an element of $M$ is an element of the function that maps $M$ to the set of elements of the composition of the action of the presheaf of $R$ and $M$ and the forgetful functor of the set of abelian groups.

the free Yoneda of m (from the name)

Let $m$ be an element of $M$. Then the free Yoneda of $m$ is a presheaf of module of $R$ defined as the action of the free of $R$ and the action of the Yoneda and the opposite of the underlying object of $m$.

Let $m$ be an element of $M$. Then $\operatorname{fromFreeYoneda}$ applied to $m$ is a homomorphism of the free Yoneda of $m$ and $M$ defined as $\operatorname{symm}$ applied to the free Yoneda equivalence and the value of the element of $m$.

the element of X and x1 (from the name)

Let $M$ be a presheaf of module of $R$. Let $X$ be an opposite of $C$. Let $x_{1}$ be a carrier of the object of $M$ and $X$. Then the element of $X$ and $x_{1}$ is an element of $M$ defined as the element of $X$ and $x_{1}$.

the free Yoneda of R (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of rings. Then the free Yoneda of $R$ is an object property of the set of presheafs of module of $R$ defined as the object property of $\operatorname{obj}$ applied to the composition of the Yoneda and the free of $R$.

the free Yoneda coproduct of M (from the name)

Let $M$ be a presheaf of module of $R$. Then the free Yoneda coproduct of $M$ is a presheaf of module of $R$ defined as the sigma object of $\operatorname{freeYoneda}$.

the free Yoneda coproduct of M and m (from the name)

Let $M$ be a presheaf of module of $R$. Let $m$ be an element of $M$. Then the free Yoneda coproduct of $M$ and $m$ is a carrier of the object of the free Yoneda coproduct of $M$ and the underlying object of $m$ defined as $\operatorname{hom}$ applied to the homomorphism of the inclusion free Yoneda coproduct of $M$ and $m$ and the underlying object of $m$ and the free of the identity morphism of the opposite of the underlying object of $m$.

the free Yoneda coproduct cokernel cofork of M (from the name)

Let $M$ be a presheaf of module of $R$. Then the free Yoneda coproduct cokernel cofork of $M$ is a cokernel cofork of the free Yoneda coproduct of $M$ defined as the projection of $\operatorname{fromFreeYonedaCoproduct}$ applied to $M$ and $\mathrm{PresheafOfModules\_\_toFreeYonedaCoproduct\_fromFreeYonedaCoproduct}$ applied to $M$.

the free Yoneda equivalence (from the name)

The free Yoneda equivalence is an equivalence from the set of homomorphisms of the action of the free of $R$ and the action of the Yoneda and $X$ and $M$ to the set of carriers of the object of $M$ and $\operatorname{op}$ applied to $X$ defined as the composition of the free homomorphism equivalence and the Yoneda equivalence.

Let $M$ be a presheaf of module of $R$. Then $\operatorname{fromFreeYonedaCoproduct}$ applied to $M$ is a homomorphism of the free Yoneda coproduct of $M$ and $M$ defined as $\operatorname{desc}$ applied to $\operatorname{fromFreeYoneda}$.

Let $M$ be a presheaf of module of $R$. Then $\operatorname{isColimitFreeYonedaCoproductsCokernelCofork}$ applied to $M$ is an element of $\operatorname{IsColimit}$ applied to the free Yoneda coproduct cokernel cofork of $M$.

the free Yoneda coproduct of M (from the name)

Let $M$ be a presheaf of module of $R$. Then the free Yoneda coproduct of $M$ is a homomorphism of the free Yoneda coproduct of the kernel of $\operatorname{fromFreeYonedaCoproduct}$ applied to $M$ and the free Yoneda coproduct of $M$ defined as the composition of $\operatorname{fromFreeYonedaCoproduct}$ applied to the kernel of $\operatorname{fromFreeYonedaCoproduct}$ applied to $M$ and the inclusion of $\operatorname{fromFreeYonedaCoproduct}$ applied to $M$.

the inclusion free Yoneda coproduct of M and m (from the name)

Let $M$ be a presheaf of module of $R$. Let $m$ be an element of $M$. Then the inclusion free Yoneda coproduct of $M$ and $m$ is a homomorphism of the free Yoneda of $m$ and the free Yoneda coproduct of $M$ defined as the inclusion of $\operatorname{freeYoneda}$ and $m$.

Let $F$ be a functor of $J$ and the set of presheafs of module of $R$. Let $c$ be a cone of $F$. Let $\mathrm{hc}$ be a function from opposites $X$ of $C$ to elements of $\operatorname{IsLimit}$ applied to the map cone of the evaluation of $R$ and $X$ and $c$. Then $\operatorname{evaluationJointlyReflectsLimits}$ applied to $F$, $c$, $X$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$.

the cone of F (from the docstring)

Let $F$ be a functor of $J$ and the set of presheafs of module of $R$. Then the cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as $\operatorname{evaluationJointlyReflectsLimits}$ applied to $F$, the limit cone of $F$ and the function that maps $x_{2}$ to $\operatorname{isLimit}$ applied to the composition of $F$ and the evaluation of $R$ and $x_{2}$.

the limit cone of F (from the name)

Let $F$ be a functor of $J$ and the set of presheafs of module of $R$. Then the limit cone of $F$ is a cone of $F$.

the limit presheaf of F (from the name)

Let $F$ be a functor of $J$ and the set of presheafs of module of $R$. Then the limit presheaf of $F$ is a presheaf of module of $R$.

the tensor homomorphism of f and g (from the name)

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the tensor homomorphism of $f$ and $g$ is a homomorphism of the tensor object of $x_{1}$ and $x_{3}$ and the tensor object of $x_{2}$ and $x_{4}$.

the tensor object of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be presheafs of module of commutative ring of $R$. Then the tensor object of $x_{1}$ and $x_{2}$ is a presheaf of module of commutative ring of $R$.

the application of f and X (from the name)

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $X$ be an opposite of $C$. Then the application of $f$ and $X$ is a homomorphism of the object of $x_{1}$ and $X$ and the object of $x_{2}$ and $X$ defined as the homomorphism of $f$ and $X$.

presheaf of module of commutative ring of R (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of commutative rings. Then a presheaf of module of commutative ring of $R$ is an element of the function that maps $R$ to the set of presheafs of module of the composition of $R$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

the homomorphism of app and X1 (from the name)

Let $\mathrm{app}$ be a function from opposites $X_{1}$ of $C$ to homomorphisms of the object of $x_{1}$ and $X_{1}$ and the object of $x_{2}$ and $X_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all opposites $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, the composition of the restriction map of $x_{1}$ and $f$ and the map of $\operatorname{restrictScalars}$ applied to the underlying ring hom of the map of $R$ and $f$ and $\mathrm{app}$ applied to $Y$ is equal to the composition of $\mathrm{app}$ applied to $X$ and the restriction map of $x_{2}$ and $f$ and $\mathrm{PresheafOfModulesOfCommRing\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $X_{1}$ and $\mathrm{app}$ is a homomorphism of $x_{1}$ and $x_{2}$ defined as the function that maps $\mathrm{naturality}$ to $\operatorname{mk}$ applied to $X_{1}$, the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{app}$ applied to $x_{3}$ and $x_{4}$ and $\mathrm{naturality}$.

the isomorphism of app and X1 (from the name)

Let $\mathrm{app}$ be a function from opposites $X_{1}$ of $C$ to isomorphisms of the object of $x_{1}$ and $X_{1}$ and the object of $x_{2}$ and $X_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all opposites $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, the composition of the restriction map of $x_{1}$ and $f$ and the map of $\operatorname{restrictScalars}$ applied to the underlying ring hom of the map of $R$ and $f$ and the homomorphism of $\mathrm{app}$ applied to $Y$ is equal to the composition of the homomorphism of $\mathrm{app}$ applied to $X$ and the restriction map of $x_{2}$ and $f$ and $\mathrm{PresheafOfModulesOfCommRing\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $X_{1}$ and $\mathrm{app}$ is an isomorphism of $x_{1}$ and $x_{2}$ defined as the function that maps $\mathrm{naturality}$ to the isomorphism of $X_{1}$ and $\mathrm{app}$.

the restriction map of F and f (from the docstring)

Let $F$ be a presheaf of module of commutative ring of $R$. Let $f$ be a homomorphism of $X$ and $Y$. Then the restriction map of $F$ and $f$ is a homomorphism of the object of $F$ and $X$ and the action of $\operatorname{restrictScalars}$ applied to the underlying ring hom of the map of $R$ and $f$ and the object of $F$ and $Y$ defined as the map of $F$ and $f$.

Let $\mathrm{obj}$ be a function from opposites $X_{3}$ of $C$ to module categories of the set of carriers of the action of $R$ and $X_{3}$. Let $\mathrm{map}$ be a function from opposites $X_{2}$ of $C$ and opposites $Y_{1}$ of $C$ and homomorphisms $f_{1}$ of $X_{2}$ and $Y_{1}$ to homomorphisms of $\mathrm{obj}$ applied to $X_{2}$ and the action of $\operatorname{restrictScalars}$ applied to the underlying ring hom of the map of $R$ and $f_{1}$ and $\mathrm{obj}$ applied to $Y_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all opposites $X_{1}$ of $C$, $\mathrm{map}$ applied to $X_{1}$, $X_{1}$ and the identity morphism of $X_{1}$ is equal to the component of the inverse of $\operatorname{restrictScalarsId'}$ applied to the underlying ring hom of the map of $R$ and the identity morphism of $X_{1}$ and $\mathrm{congrArg}$ applied to $\operatorname{hom}$ and $\mathrm{CategoryTheory\_\_Functor\_\_map\_id}$ applied to $R$ and $X_{1}$ and $\mathrm{obj}$ applied to $X_{1}$ and $\mathrm{PresheafOfModulesOfCommRing\_\_mk\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all opposites $X$ of $C$, for all opposites $Y$ of $C$, for all opposites $Z$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, for all homomorphisms $g$ of $Y$ and $Z$, $\mathrm{map}$ applied to $X$, $Z$ and the composition of $f$ and $g$ is equal to the composition of $\mathrm{map}$ applied to $X$, $Y$ and $f$ and the composition of the map of $\operatorname{restrictScalars}$ applied to the underlying ring hom of the map of $R$ and $f$ and $\mathrm{map}$ applied to $Y$, $Z$ and $g$ and the component of the inverse of $\operatorname{restrictScalarsComp'}$ applied to the underlying ring hom of the map of $R$ and $f$, the underlying ring hom of the map of $R$ and $g$, the underlying ring hom of the map of $R$ and the composition of $f$ and $g$ and $\mathrm{congrArg}$ applied to $\operatorname{hom}$ and $\mathrm{CategoryTheory\_\_Functor\_\_map\_comp}$ applied to $R$, $f$ and $g$ and $\mathrm{obj}$ applied to $Z$ and $\mathrm{PresheafOfModulesOfCommRing\_\_mk\_\_\_auto\_3}$. Then $\operatorname{mk}$ applied to $X_{3}$, $\mathrm{obj}$, $X_{2}$, $Y_{1}$, $f_{1}$, $\mathrm{map}$, $\mathrm{map\_id}$ and $\mathrm{map\_comp}$ is a presheaf of module of commutative ring of $R$ defined as the function that maps $f_{1}$, $\mathrm{map}$, $\mathrm{map\_id}$ and $\mathrm{map\_comp}$ to $\operatorname{mk}$ applied to $X_{3}$, the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{obj}$ applied to $x_{1}$ and $x_{2}$, $X_{2}$, the function that maps $x_{3}$, $x_{4}$ and $x_{5}$ to $Y_{1}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$, $f_{1}$, $\mathrm{map}$, $\mathrm{map\_id}$ and $\mathrm{map\_comp}$.

the object of F and X (from the name)

Let $F$ be a presheaf of module of commutative ring of $R$. Let $X$ be an opposite of $C$. Then the object of $F$ and $X$ is a module category of the set of carriers of the action of $R$ and $X$ defined as the object of $F$ and $X$.

the pullback of x2 (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Then the pullback of $x_{2}$ is a functor of the set of presheafs of module of commutative ring of $S$ and the set of presheafs of module of commutative ring of $R$ defined as the pullback functor of the right whisker of $x_{2}$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

the pullback pushforward adjunction of x2 (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Then the pullback pushforward adjunction of $x_{2}$ is an adjunction of the pullback of $x_{2}$ and $\operatorname{pushforward}$ applied to $x_{2}$ defined as the pullback pushforward adjunction of the right whisker of $x_{2}$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Then $\operatorname{pushforward}$ applied to $x_{2}$ is a functor of the set of presheafs of module of commutative ring of $R$ and the set of presheafs of module of commutative ring of $S$ defined as the pushforward functor of the right whisker of $x_{2}$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

Let $F$ be a functor of $C$ and $D$. Let $R$ be a functor of the set of opposites of $D$ and the set of categories of commutative rings. Then $\mathrm{PresheafOfModulesOfCommRing\_\_pushforward\_u2080\_}$ applied to $F$ and $R$ is a functor of the set of presheafs of module of commutative ring of $R$ and the set of presheafs of module of commutative ring of the composition of the opposite of $F$ and $R$ defined as $\mathrm{PresheafOfModules\_\_pushforward\_u2080\_}$ applied to $F$ and the composition of $R$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

Let $x_{1}$ be a homomorphism of $R$ and $S$. Then $\operatorname{restrictScalars}$ applied to $x_{1}$ is a functor of the set of presheafs of module of commutative ring of $S$ and the set of presheafs of module of commutative ring of $R$ defined as $\operatorname{restrictScalars}$ applied to the right whisker of $x_{1}$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

the unit of R (from the name)

Let $R$ be a functor of the set of opposites of $C$ and the set of categories of commutative rings. Then the unit of $R$ is a presheaf of module of commutative ring of $R$ defined as the unit of the composition of $R$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

the pullback functor of x2 (from the docstring)

Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Then the pullback functor of $x_{2}$ is a functor of the set of presheafs of module of $S$ and the set of presheafs of module of $R$ defined as the left adjoint of the pushforward functor of $x_{2}$.

the pullback composition of x3 and x4 (from the name)

Let $x_{3}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Let $x_{4}$ be a homomorphism of $R$ and the composition of the opposite of $G$ and $T$. Then the pullback composition of $x_{3}$ and $x_{4}$ is an isomorphism of the composition of the pullback functor of $x_{3}$ and the pullback functor of $x_{4}$ and the pullback functor of the composition of $x_{3}$ and the left whisker of the opposite of $F$ and $x_{4}$ defined as the left adjoint composition isomorphism of the pullback pushforward adjunction of the composition of $x_{3}$ and the left whisker of the opposite of $F$ and $x_{4}$ and the pushforward composition of $x_{3}$ and $x_{4}$.

the pullback identity of S (from the name)

Let $S$ be a functor of the set of opposites of $C$ and the set of categories of rings. Then the pullback identity of $S$ is an isomorphism of the pullback functor of the identity morphism of $S$ and the identity of the set of presheafs of module of $S$ defined as the left adjoint identity isomorphism of the pullback pushforward adjunction of the identity morphism of $S$ and the pushforward identity of $S$.

Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Then there is an object property of the set of presheafs of module of $S$. Proof. Let $x_{2}$ be arbitrary. By x2. By PresheafOfModules__pushforward. By CategoryTheory__Functor__leftAdjointObjIsDefined.

the pullback pushforward adjunction of x2 (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Then the pullback pushforward adjunction of $x_{2}$ is an adjunction of the pullback functor of $x_{2}$ and the pushforward functor of $x_{2}$ defined as the adjunction of the pushforward functor of $x_{2}$.

Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Let $X$ be an element of $C$. Then $\operatorname{pushforwardCompCoyonedaFreeYonedaCorepresentableBy}$ applied to $x_{2}$ and $X$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of the pushforward functor of $x_{2}$ and the action of the Coyoneda and $\operatorname{op}$ applied to the action of the free of $S$ and the action of the Yoneda and $X$ and the action of the free of $R$ and the action of the Yoneda and the action of $F$ and $X$.

the pushforward functor of x2 (from the docstring)

Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Then the pushforward functor of $x_{2}$ is a functor of the set of presheafs of module of $R$ and the set of presheafs of module of $S$ defined as the composition of $\mathrm{PresheafOfModules\_\_pushforward\_u2080\_}$ applied to $F$ and $R$ and $\operatorname{restrictScalars}$ applied to $x_{2}$.

the pushforward composition of x3 and x4 (from the name)

Let $x_{3}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Let $x_{4}$ be a homomorphism of $R$ and the composition of the opposite of $G$ and $T$. Then the pushforward composition of $x_{3}$ and $x_{4}$ is an isomorphism of the composition of the pushforward functor of $x_{4}$ and the pushforward functor of $x_{3}$ and the pushforward functor of the composition of $x_{3}$ and the left whisker of the opposite of $F$ and $x_{4}$ defined as the identity of the composition of the pushforward functor of $x_{4}$ and the pushforward functor of $x_{3}$.

the pushforward composition to presheaf of x2 (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the composition of the opposite of $F$ and $R$. Then the pushforward composition to presheaf of $x_{2}$ is an isomorphism of the composition of the pushforward functor of $x_{2}$ and the presheaf of $S$ and the composition of the presheaf of $R$ and the action of the left whiskering of the set of opposites of $D$ and the set of abelian groups and the opposite of $F$ defined as the identity of the composition of the pushforward functor of $x_{2}$ and the presheaf of $S$.

the pushforward identity of R (from the name)

Let $R$ be a functor of the set of opposites of $D$ and the set of categories of rings. Then the pushforward identity of $R$ is an isomorphism of the pushforward functor of the identity morphism of $R$ and the identity of the set of presheafs of module of $R$ defined as the identity of the pushforward functor of the identity morphism of $R$.

Let $F$ be a functor of $C$ and $D$. Let $R$ be a functor of the set of opposites of $D$ and the set of categories of rings. Then $\mathrm{PresheafOfModules\_\_pushforward\_u2080\_}$ applied to $F$ and $R$ is a functor of the set of presheafs of module of $R$ and the set of presheafs of module of the composition of the opposite of $F$ and $R$.

the pushforward composition to presheaf of F and R (from the name)

Let $F$ be a functor of $C$ and $D$. Let $R$ be a functor of the set of opposites of $D$ and the set of categories of rings. Then the pushforward composition to presheaf of $F$ and $R$ is an isomorphism of the composition of $\mathrm{PresheafOfModules\_\_pushforward\_u2080\_}$ applied to $F$ and $R$ and the presheaf of the composition of the opposite of $F$ and $R$ and the composition of the presheaf of $R$ and the action of the left whiskering of the set of opposites of $D$ and the set of abelian groups and the opposite of $F$ defined as the identity of the composition of $\mathrm{PresheafOfModules\_\_pushforward\_u2080\_}$ applied to $F$ and $R$ and the presheaf of the composition of the opposite of $F$ and $R$.

Let $F$ be a functor of $C$ and $D$. Let $R$ be a functor of the set of opposites of $D$ and the set of categories of commutative rings. Then $\mathrm{PresheafOfModules\_\_pushforward\_u2080\_OfCommRingCat}$ applied to $F$ and $R$ is a functor of the set of presheafs of module of the composition of $R$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings and the set of presheafs of module of the composition of the composition of the opposite of $F$ and $R$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings defined as $\mathrm{PresheafOfModules\_\_pushforward\_u2080\_}$ applied to $F$ and the composition of $R$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

the sheafification of x2 (from the name)

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Then the sheafification of $x_{2}$ is a functor of the set of presheafs of module of $x_{1}$ and the set of sheaves of module of $R$.

the sheafification adjunction of x2 (from the name)

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Then the sheafification adjunction of $x_{2}$ is an adjunction of the sheafification of $x_{2}$ and the composition of the forgetful functor of $R$ and $\operatorname{restrictScalars}$ applied to $x_{2}$.

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Then $\operatorname{sheafificationCompForgetCompToPresheaf}$ applied to $x_{2}$ is an isomorphism of the composition of the sheafification of $x_{2}$ and the composition of the forgetful functor of $R$ and the presheaf of the object of $R$ and the composition of the presheaf of $x_{1}$ and the composition of the presheaf to sheaf of $J$ and the set of additive commutative group categories and the sheaf to presheaf of $J$ and the set of additive commutative group categories defined as the identity of the composition of the sheafification of $x_{2}$ and the composition of the forgetful functor of $R$ and the presheaf of the object of $R$.

the sheafification composition to sheaf of x2 (from the name)

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Then the sheafification composition to sheaf of $x_{2}$ is an isomorphism of the composition of the sheafification of $x_{2}$ and the sheaf of $R$ and the composition of the presheaf of $x_{1}$ and the presheaf to sheaf of $J$ and the set of additive commutative group categories defined as the identity of the composition of the sheafification of $x_{2}$ and the sheaf of $R$.

the sheafification homomorphism equivalence of x2 (from the name)

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Then the sheafification homomorphism equivalence of $x_{2}$ is an equivalence from the set of homomorphisms of the action of the sheafification of $x_{2}$ and $P$ and $F$ to the set of homomorphisms of $P$ and the action of $\operatorname{restrictScalars}$ applied to $x_{2}$ and the action of the forgetful functor of $R$ and $F$ defined as the sheafification homomorphism equivalence of $x_{2}$ and the sheafification of $J$ and the presheaf of $P$.

the scalar multiple of r and m (from the name)

Let $r$ be a family of element of the composition of $R$ and the forgetful functor of the set of categories of rings and $P$. Let $m$ be a family of element of the composition of the presheaf of $M$ and the forgetful functor of the set of abelian groups and $P$. Then the scalar multiple of $r$ and $m$ is a family of element of the composition of the presheaf of $M$ and the forgetful functor of the set of abelian groups and $P$ defined as the function that maps $Y$, $f$ and $\mathrm{hf}$ to $\HSMulhSMulMACRoAL {r (Y , f , \mathrm{hf})}{m (Y , f , \mathrm{hf})}$.

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Let $x_{4}$ be a homomorphism of the presheaf of $x_{3}$ and the object of $A$. Let $r$ be a carrier of the action of the object of $R$ and $X$. Let $m$ be a carrier of the action of the object of $A$ and $X$. Then the elements of $\operatorname{SMulCandidate}$ applied to $x_{2}$, $x_{4}$, $r$ and $m$ are a basic type.

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Let $x_{4}$ be a homomorphism of the presheaf of $x_{3}$ and the object of $A$. Let $r$ be a carrier of the action of the object of $R$ and $X$. Let $m$ and $a$ be carriers of the action of the object of $A$ and $X$. Let $S$ be a sieve of the opposite of $X$ such that $S$ is an element of $J$ applied to the opposite of $X$. Let $x_{5}$ be a family of element of the composition of $x_{1}$ and the forgetful functor of the set of categories of rings and the arrow of $S$. Let $x_{6}$ be a family of element of the composition of the presheaf of $x_{3}$ and the forgetful functor of the set of abelian groups and the arrow of $S$. Assume that $\operatorname{IsAmalgamation}$ holds for the map of $x_{5}$ and the right whisker of $x_{2}$ and the forgetful functor of the set of categories of rings and $r$. Assume that $\operatorname{IsAmalgamation}$ holds for the map of $x_{6}$ and the right whisker of $x_{4}$ and the forgetful functor of the set of abelian groups and $m$. Assume that $\operatorname{IsAmalgamation}$ holds for the map of the scalar multiple of $x_{5}$ and $x_{6}$ and the right whisker of $x_{4}$ and the forgetful functor of the set of abelian groups and $a$. Then $\operatorname{mk'}$ applied to $x_{2}$, $x_{4}$, $r$, $m$, $S$, $\mathrm{hS}$, $x_{5}$, $x_{6}$, $h_{2}$, $h_{3}$, $a$ and $\mathrm{ha}$ is an element of $\operatorname{SMulCandidate}$ applied to $x_{2}$, $x_{4}$, $r$ and $m$.

Let $\mathrm{self}$ be an element of $\operatorname{SMulCandidate}$ applied to $x_{2}$, $x_{4}$, $r$ and $m$. Then $\operatorname{x}$ applied to $\mathrm{self}$ is a carrier of the action of the object of $A$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the scalar multiple of r and m (from the name)

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Let $x_{4}$ be a homomorphism of the presheaf of $x_{3}$ and the object of $A$. Let $r$ be a carrier of the action of the object of $R$ and $X$. Let $m$ be a carrier of the action of the object of $A$ and $X$. Then the scalar multiple of $r$ and $m$ is a carrier of the action of the object of $A$ and $X$ defined as $\operatorname{x}$ applied to $\operatorname{smulCandidate}$ applied to $x_{2}$, $x_{4}$, $r$ and $m$.

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Let $x_{4}$ be a homomorphism of the presheaf of $x_{3}$ and the object of $A$. Let $r$ be a carrier of the action of the object of $R$ and $X$. Let $m$ be a carrier of the action of the object of $A$ and $X$. Then $\operatorname{smulCandidate}$ applied to $x_{2}$, $x_{4}$, $r$ and $m$ is an element of $\operatorname{SMulCandidate}$ applied to $x_{2}$, $x_{4}$, $r$ and $m$ defined as $\operatorname{default}$.

the sheafification of x2 and x4 (from the name)

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Let $x_{4}$ be a homomorphism of the presheaf of $x_{3}$ and the object of $A$. Then the sheafification of $x_{2}$ and $x_{4}$ is a sheaf of module of $R$.

the sheafification homomorphism equivalence of x2 and x4 (from the name)

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Let $x_{4}$ be a homomorphism of the presheaf of $x_{3}$ and the object of $A$. Then the sheafification homomorphism equivalence of $x_{2}$ and $x_{4}$ is an equivalence from the set of homomorphisms of the sheafification of $x_{2}$ and $x_{4}$ and $F$ to the set of homomorphisms of $x_{3}$ and the action of $\operatorname{restrictScalars}$ applied to $x_{2}$ and the action of the forgetful functor of $R$ and $F$ defined as the composition of the equivalence of $\operatorname{fullyFaithfulForget}$ applied to $R$ and the sheafification homomorphism equivalence of $x_{2}$ and $x_{4}$.

the sheafification homomorphism equivalence of x2 and x4 (from the name)

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Let $x_{4}$ be a homomorphism of the presheaf of $x_{3}$ and the object of $A$. Assume that $\operatorname{IsSheaf}$ holds for $J$ and the presheaf of $F$. Then the sheafification homomorphism equivalence of $x_{2}$ and $x_{4}$ is an equivalence from the set of homomorphisms of the value of the sheafification of $x_{2}$ and $x_{4}$ and $F$ to the set of homomorphisms of $x_{3}$ and the action of $\operatorname{restrictScalars}$ applied to $x_{2}$ and $F$ defined as the composition of $\operatorname{restrictHomEquivOfIsLocallySurjective}$ applied to $x_{2}$ and $\mathrm{hF}$ and the bijection of the sheafification of $x_{2}$ and $x_{4}$ and $\mathrm{hF}$.

the sheafification map of x7 and x8 (from the name)

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Let $x_{4}$ be a homomorphism of the presheaf of $x_{3}$ and the object of $A$. Let $x_{6}$ be a homomorphism of the presheaf of $x_{5}$ and the object of $\mathrm{A'}$. Let $x_{7}$ be a homomorphism of $x_{3}$ and $x_{5}$. Let $x_{8}$ be a homomorphism of $A$ and $\mathrm{A'}$ such that the composition of the map of the presheaf of $x_{1}$ and $x_{7}$ and $x_{6}$ is equal to the composition of $x_{4}$ and the homomorphism of $x_{8}$. Then the sheafification map of $x_{7}$ and $x_{8}$ is a homomorphism of the sheafification of $x_{2}$ and $x_{4}$ and the sheafification of $x_{2}$ and $x_{6}$.

the sheafification of x2 and x4 (from the name)

Let $x_{2}$ be a homomorphism of $x_{1}$ and the object of $R$. Let $x_{4}$ be a homomorphism of the presheaf of $x_{3}$ and the object of $A$. Then the sheafification of $x_{2}$ and $x_{4}$ is a homomorphism of $x_{3}$ and the action of $\operatorname{restrictScalars}$ applied to $x_{2}$ and the value of the sheafification of $x_{2}$ and $x_{4}$.

submodule of M (from the name)

Let $M$ be a presheaf of module of $R$. Then the submodules of $M$ are a basic type.

the homomorphism of hle (from the name)

Assume that $x_{1} \leq x_{2}$. Then the homomorphism of $\mathrm{hle}$ is a homomorphism of the presheaf of $x_{1}$ and the presheaf of $x_{2}$.

the object of self and X (from the name)

Let $\mathrm{self}$ be a submodule of $M$. Let $X$ be an opposite of $C$. Then the object of $\mathrm{self}$ and $X$ is a submodule 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}$ and $X$.

the presheaf of N (from the name)

Let $N$ be a submodule of $M$. Then the presheaf of $N$ is a presheaf of module of $R$.

the subfunctor of N (from the name)

Let $N$ be a submodule of $M$. Then the subfunctor of $N$ is a subfunctor of the composition of the presheaf of $M$ and the forgetful functor of the set of additive commutative group categories defined as $\operatorname{mk}$ applied to the function that maps $X$ to $\operatorname{ofPred}$ applied to the function that maps $r$ to the proposition that $r$ is an element of the object of $N$ and $X$ and the function that maps $x_{1}$, $x_{2}$, $f$, $x_{3}$ and $\mathrm{hr}$ to $\mathrm{PresheafOfModules\_\_Submodule\_\_map\_mem}$ applied to $N$, $f$ and $\mathrm{hr}$.

the inclusion of N (from the docstring)

Let $N$ be a submodule of $M$. Then the inclusion of $N$ is a homomorphism of the presheaf of $N$ and $M$.

the categorical coproduct in Z (from the docstring)

Let $Z$ be a function from elements of $x_{1}$ to module categories of $R$. Then the categorical coproduct in $Z$ is an isomorphism of the sigma object of $Z$ and $\operatorname{of}$ applied to $R$ and the set of direct sums of $x_{1}$ and the function that maps $i$ to the set of carriers of $Z$ applied to $i$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the coproduct cone induced by the concrete coproduct of $Z$ and the concrete coproduct cone of $Z$.

the coproduct cone induced by the concrete coproduct of Z (from the docstring)

Let $Z$ be a function from elements of $x_{1}$ to module categories of $R$. Then the coproduct cone induced by the concrete coproduct of $Z$ is a cofan of $Z$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $R$ and the set of direct sums of $x_{1}$ and the function that maps $i$ to the set of carriers of $Z$ applied to $i$ and the function that maps $i_{1}$ to the module category of $\operatorname{lof}$ applied to $R$, $x_{1}$, the function that maps $i_{2}$ to the set of carriers of $Z$ applied to $i_{2}$ and $i_{1}$.

the concrete coproduct cone of Z (from the docstring)

Let $Z$ be a function from elements of $x_{1}$ to module categories of $R$. Then the concrete coproduct cone of $Z$ is an element of $\operatorname{IsColimit}$ applied to the coproduct cone induced by the concrete coproduct of $Z$.

the categorical product in Z (from the docstring)

Let $Z$ be a function from elements of $x_{1}$ to module categories of $R$. Then the categorical product in $Z$ is an isomorphism of the product object of $Z$ and $\operatorname{of}$ applied to $R$ and the set of functions from elements $i$ of $x_{1}$ to carriers of $Z$ applied to $i$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the product cone induced by the concrete product of $Z$ and the concrete product cone of $Z$.

the product cone induced by the concrete product of Z (from the docstring)

Let $Z$ be a function from elements of $x_{1}$ to module categories of $R$. Then the product cone induced by the concrete product of $Z$ is an element of $\operatorname{Fan}$ applied to $Z$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $R$ and the set of functions from elements $i$ of $x_{1}$ to carriers of $Z$ applied to $i$ and the function that maps $i_{1}$ to the module category of the projection of $i_{1}$.

the concrete product cone of Z (from the docstring)

Let $Z$ be a function from elements of $x_{1}$ to module categories of $R$. Then the concrete product cone of $Z$ is an element of $\operatorname{IsLimit}$ applied to the product cone induced by the concrete product of $Z$.

$\operatorname{moduleCatExtendScalarsPseudofunctor}$ is a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of categories of commutative rings and the set of categories.

$\operatorname{moduleCatRestrictScalarsPseudofunctor}$ is a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of the set of categories of commutative rings and the set of categories.

$\operatorname{moduleCatRestrictScalarsPseudofunctor}$ is a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of the set of categories of rings and the set of categories.

the linear equivalence of i (from the name)

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$.

the module isomorphism of e (from the name)

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}$.

semimodule category of R (from the name)

Let $R$ be a set. Then the semimodule categories of $R$ are a basic type.

homomorphism of M and N (from the name)

Let $M$ and $N$ be semimodule categories of $R$. Then the homomorphisms of $M$ and $N$ are a basic type.

the homomorphism of f (from the name)

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$.

the homomorphism of self (from the name)

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}$.

the homomorphism of f (from the name)

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 semimodule category of $\operatorname{toLinearMap}$ applied to the homomorphism linear equivalence.

carrier of self (from the name)

Let $\mathrm{self}$ be a semimodule 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}$.

the homomorphism additive equivalence (from the name)

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$.

the homomorphism equivalence (from the name)

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$.

the homomorphism linear equivalence (from the name)

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$.

Let $R$ and $X$ be sets. Then $\operatorname{of}$ applied to $R$ and $X$ is a semimodule category of $R$ defined as $\mathrm{SemimoduleCat\_\_\_mkInternal}$ applied to $X$.

the semimodule category of f (from the name)

Let $f$ be a linear map of $X$ and $Y$. Then the semimodule 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$.

the semimodule category of f (from the name)

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 semimodule 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 semimodule category of the composition of $\operatorname{toLinearMap}$ applied to the inverse of the homomorphism linear equivalence and $f$.

the linear equivalence isomorphism module isomorphism (from the name)

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$.

J is locally injective (from the docstring)

J is locally surjective (from the docstring)

the bijection of f and hN (from the docstring)

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Assume that $\operatorname{IsSheaf}$ holds for $J$ and the presheaf of $N$. Then the bijection of $f$ and $\mathrm{hN}$ is an equivalence from the set of homomorphisms of $x_{2}$ and $N$ to the set of homomorphisms of $x_{1}$ and $N$.

sheaf of module of R (from the name)

Let $R$ be a sheaf of $J$ and the set of categories of rings. Then the sheaves of module of $R$ are a basic type.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be sheaves of module of $R$. Then the homomorphisms of $X$ and $Y$ are a basic type.

the value of self (from the name)

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

the evaluation of R and X (from the name)

Let $R$ be a sheaf of $J$ and the set of categories of rings. Let $X$ be an opposite of $C$. Then the evaluation of $R$ and $X$ is a functor of the set of sheaves of module of $R$ and the set of module categories of the set of carriers of the action of the object of $R$ and $X$ defined as the composition of the forgetful functor of $R$ and the evaluation of the object of $R$ and $X$.

the forgetful functor of R (from the docstring)

Let $R$ be a sheaf of $J$ and the set of categories of rings. Then the forgetful functor of $R$ is a functor of the set of sheaves of module of $R$ and the set of presheafs of module of the object of $R$.

Let $R$ be a sheaf of $J$ and the set of categories of rings. Let $X$ be an opposite of $C$. Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Then $\operatorname{forgetToSheafModuleCat}$ applied to $R$, $X$ and $\mathrm{hX}$ is a functor of the set of sheaves of module of $R$ and the set of sheaves of $J$ and the set of module categories of the set of carriers of the action of the object of $R$ and $X$.

Let $R$ be a sheaf of $J$ and the set of categories of rings. Let $X$ and $Y$ be opposites of $C$. Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Let $\mathrm{hY}$ be an element of $\operatorname{IsInitial}$ applied to $Y$. Let $x_{1}$ be an isomorphism of $X$ and $Y$. Then $\operatorname{forgetToSheafModuleCatOfIso}$ applied to $R$, $X$, $Y$, $\mathrm{hX}$, $\mathrm{hY}$ and $x_{1}$ is an isomorphism of $\operatorname{forgetToSheafModuleCat}$ applied to $R$, $X$ and $\mathrm{hX}$ and the composition of $\operatorname{forgetToSheafModuleCat}$ applied to $R$, $Y$ and $\mathrm{hY}$ and $\operatorname{sheafCompose}$ applied to $J$ and $\operatorname{restrictScalars}$ applied to the homomorphism of the map of the object of $R$ and the homomorphism of $x_{1}$.

Let $R$ be a sheaf of $J$ and the set of categories of rings. Then $\operatorname{fullyFaithfulForget}$ applied to $R$ is an element of $\operatorname{FullyFaithful}$ applied to the forgetful functor of $R$.

section of M (from the name)

Let $M$ be a sheaf of module of $R$. Then a section of $M$ is an element of the function that maps $M$ to the set of sections of the value of $M$.

the section functor of R (from the name)

Let $R$ be a sheaf of $J$ and the set of categories of rings. Then the section functor of $R$ is a functor of the set of sheaves of module of $R$ and the set of sets.

the map of f and s (from the docstring)

Let $f$ be a homomorphism of $M$ and $N$. Let $s$ be a section of $M$. Then the map of $f$ and $s$ is a section of $N$ defined as the map of the value of $f$ and $s$.

the sheaf of R (from the name)

Let $R$ be a sheaf of $J$ and the set of categories of rings. Then the sheaf of $R$ is a functor of the set of sheaves of module of $R$ and the set of sheaves of $J$ and the set of additive commutative group categories.

the sheaf composition sheaf to presheaf isomorphism of R (from the name)

Let $R$ be a sheaf of $J$ and the set of categories of rings. Then the sheaf composition sheaf to presheaf isomorphism of $R$ is an isomorphism of the composition of the sheaf of $R$ and the sheaf to presheaf of $J$ and the set of additive commutative group categories and the composition of the forgetful functor of $R$ and the presheaf of the object of $R$ defined as the identity of the composition of the sheaf of $R$ and the sheaf to presheaf of $J$ and the set of additive commutative group categories.

the unit of R (from the name)

Let $R$ be a sheaf of $J$ and the set of categories of rings. Then the unit of $R$ is a sheaf of module of $R$.

the unit homomorphism equivalence of M (from the name)

Let $M$ be a sheaf of module of $R$. Then the unit homomorphism equivalence of $M$ is an equivalence from the set of homomorphisms of the unit of $R$ and $M$ to the set of sections of $M$ defined as the composition of the equivalence of $\operatorname{fullyFaithfulForget}$ applied to $R$ and the unit homomorphism equivalence of the value of $M$.

the value of self (from the name)

Let $\mathrm{self}$ be a sheaf of module of $R$. Then the value of $\mathrm{self}$ is a presheaf of module of the object of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $x_{1}$ be a homomorphism of $R$ and $\mathrm{R'}$. Assume that $\operatorname{IsSheaf}$ holds for $J$ and the presheaf of $x_{3}$. Then $\operatorname{restrictHomEquivOfIsLocallySurjective}$ applied to $x_{1}$ and $h$ is an equivalence from the set of homomorphisms of $x_{2}$ and $x_{3}$ to the set of homomorphisms of the action of $\operatorname{restrictScalars}$ applied to $x_{1}$ and $x_{2}$ and the action of $\operatorname{restrictScalars}$ applied to $x_{1}$ and $x_{3}$.

Let $x_{1}$ be a homomorphism of $R$ and $\mathrm{R'}$. Then $\operatorname{restrictScalars}$ applied to $x_{1}$ is a functor of the set of sheaves of module of $\mathrm{R'}$ and the set of sheaves of module of $R$.

the free of I (from the name)

Let $I$ be a set. Then the free of $I$ is a sheaf of module of $R$ defined as the sigma object of the function that maps $x_{1}$ to the unit of $R$.

the tautological cofan with point of I (from the docstring)

Let $I$ be a set. Then the tautological cofan with point of $I$ is a cofan of the function that maps $x_{1}$ to the unit of $R$ defined as $\operatorname{mk}$ applied to the free of $I$ and $\mathrm{SheafOfModules\_\_\_u3b9\_Free}$.

the functor (from the docstring)

The functor is a functor of the set of sets and the set of sheaves of module of $R$ defined as the action of the sigma constant and the unit of $R$.

the free homomorphism equivalence of M (from the name)

Let $M$ be a sheaf of module of $R$. Then the free homomorphism equivalence of $M$ is an equivalence from the set of homomorphisms of the free of $I$ and $M$ to the set of functions from elements of $I$ to sections of $M$.

the free map of f (from the name)

Let $f$ be a function from elements of $I$ to elements of $J_{1}$. Then the free map of $f$ is a homomorphism of the free of $I$ and the free of $J_{1}$ defined as $\operatorname{symm}$ applied to the free homomorphism equivalence of the free of $J_{1}$ and the function that maps $i_{1}$ to the tautological section of $f$ applied to $i_{1}$.

the tautological section of i (from the docstring)

Let $i$ be an element of $I$. Then the tautological section of $i$ is a section of the free of $I$ defined as $\operatorname{freeHomEquiv}$ applied to the free of $I$, the identity morphism of the free of $I$ and $i$.

the free sum isomorphism of I and J1 (from the name)

Let $I$ and $J_{1}$ be sets. Then the free sum isomorphism of $I$ and $J_{1}$ is an isomorphism of the coproduct of the free of $I$ and the free of $J_{1}$ and the free of $\mathrm{Sum}$ applied to $I$ and $J_{1}$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{coprodIsCoprod}$ applied to the free of $I$ and the free of $J_{1}$ and $\operatorname{mapIsColimitOfPreservesOfIsColimit}$ applied to the functor, the type category of $\operatorname{inl}$, the type category of $\operatorname{inr}$ and the binary coproduct colimit of $I$ and $J_{1}$.

Let $I$ be a set. Then $\operatorname{isColimitFreeCofan}$ applied to $I$ is an element of $\operatorname{IsColimit}$ applied to the tautological cofan with point of $I$ defined as $\operatorname{coproductIsCoproduct}$ applied to the function that maps $x_{1}$ to the unit of $R$.

the map free of F and x2 (from the name)

Let $F$ be a functor of the set of sheaves of module of $R$ and the set of sheaves of module of $S$. Let $I$ be a set. Let $x_{2}$ be a homomorphism of the unit of $S$ and the action of $F$ and the unit of $R$. Then the map free of $F$ and $x_{2}$ is a homomorphism of the free of $I$ and the action of $F$ and the free of $I$ defined as the map of the map cocone of $F$ and the tautological cofan with point of $I$ and the natural transformation of the function that maps $x_{3}$ to $x_{2}$.

the map free isomorphism of F and x2 (from the name)

Let $F$ be a functor of the set of sheaves of module of $R$ and the set of sheaves of module of $S$. Let $I$ be a set. Let $x_{2}$ be an isomorphism of the unit of $S$ and the action of $F$ and the unit of $R$. Then the map free isomorphism of $F$ and $x_{2}$ is an isomorphism of the free of $I$ and the action of $F$ and the free of $I$ defined as the cocone point isomorphism of $\operatorname{isColimitOfPreserves}$ applied to $F$ and $\operatorname{isColimitFreeCofan}$ applied to $I$ and the natural isomorphism of the function that maps $x_{3}$ to $x_{2}$.

the inclusion free of i (from the name)

Let $i$ be an element of $I$. Then the inclusion free of $i$ is a homomorphism of the unit of $R$ and the free of $I$ defined as the inclusion of the function that maps $x_{1}$ to the unit of $R$ and $i$.

generating section of M (from the name)

Let $M$ be a sheaf of module of $R$. Then the generating sections of $M$ are a basic type.

Let $\mathrm{self}$ be a generating section of $M$. Then an element of $\operatorname{I}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

x1 is a finite type (from the name)

Let $x_{1}$ be a generating section of $M$. Then we can say that $x_{1}$ is a finite type.

the equivalence of e (from the name)

Let $e$ be an isomorphism of $M$ and $N$. Then the equivalence of $e$ is an equivalence from the set of generating sections of $M$ to the set of generating sections of $N$.

the local generator data of G (from the name)

Let $G$ be a generating section of $M$. Then the local generator data of $G$ is a local generator data of $M$.

the map of F and x2 (from the name)

Let $G$ be a generating section of $M$. Let $F$ be a functor of the set of sheaves of module of $R$ and the set of sheaves of module of $S$. Let $x_{2}$ be an isomorphism of the unit of $S$ and the action of $F$ and the unit of $R$. Then the map of $F$ and $x_{2}$ is a generating section of the action of $F$ and $M$.

the map free homomorphism of F and x2 (from the name)

Let $G$ be a generating section of $M$. Let $F$ be a functor of the set of sheaves of module of $R$ and the set of sheaves of module of $S$. Let $x_{2}$ be an isomorphism of the unit of $S$ and the action of $F$ and the unit of $R$. Then the map free homomorphism of $F$ and $x_{2}$ is a homomorphism of the free of $\operatorname{I}$ applied to $G$ and the action of $F$ and $M$ defined as the composition of the homomorphism of the map free isomorphism of $F$ and $x_{2}$ and the map of $F$ and the projection of $G$.

the generating section of x1 and p (from the name)

Let $x_{1}$ be a generating section of $M$. Let $p$ be a homomorphism of $M$ and $N$. Then the generating section of $x_{1}$ and $p$ is a generating section of $N$.

Let $\mathrm{self}$ be a generating section of $M$. Let $x_{1}$ be an element of $\operatorname{I}$ applied to $\mathrm{self}$. Then $\operatorname{s}$ applied to $\mathrm{self}$ and $x_{1}$ is a section of $M$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.

the projection of x1 (from the name)

Let $x_{1}$ be a generating section of $M$. Then the projection of $x_{1}$ is a homomorphism of the free of $\operatorname{I}$ applied to $x_{1}$ and $M$ defined as $\operatorname{symm}$ applied to the free homomorphism equivalence of $M$ and $\operatorname{s}$ applied to $x_{1}$.

M is a finite type (from the name)

Let $M$ be a sheaf of module of $R$. Then we can say that $M$ is a finite type.

local generator data of M (from the name)

Let $M$ be a sheaf of module of $R$. Then the local generator data of $M$ are a basic type.

Let $\mathrm{self}$ be a local generator data of $M$. Then an element of $\operatorname{I}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

p is a finite type (from the name)

Let $p$ be a local generator data of $M$. Then we can say that $p$ is a finite type.

Let $\mathrm{self}$ be a local generator data of $M$. Let $x_{1}$ be an element of $\operatorname{I}$ applied to $\mathrm{self}$. Then $\operatorname{X}$ applied to $\mathrm{self}$ and $x_{1}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.

the generator of self and i (from the name)

Let $\mathrm{self}$ be a local generator data of $M$. Let $i$ be an element of $\operatorname{I}$ applied to $\mathrm{self}$. Then the generator of $\mathrm{self}$ and $i$ is a generating section of $\operatorname{over}$ applied to $M$ and $\operatorname{X}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $i$.

the shrink of q (from the name)

Let $q$ be a local generator data of $M$. Then the shrink of $q$ is a local generator data of $M$.

M is locally free (from the docstring)

q is a locally free data (from the name)

Let $q$ be a local generator data of $M$. Then $\operatorname{quasiCoherentData}$ applied to $q$ is a quasicoherent data of $M$.

the generating section of I (from the name)

Let $I$ be a set. Then the generating section of $I$ is a generating section of the free of $I$.

the adjunction of x2 (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Then the adjunction of $x_{2}$ is an adjunction of the composition of the forgetful functor of $S$ and the composition of the pullback functor of the homomorphism of $x_{2}$ and the sheafification of the identity morphism of the object of $R$ and $\operatorname{pushforward}$ applied to $x_{2}$.

the pullback functor of x2 (from the docstring)

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Then the pullback functor of $x_{2}$ is a functor of the set of sheaves of module of $S$ and the set of sheaves of module of $R$ defined as the left adjoint of $\operatorname{pushforward}$ applied to $x_{2}$.

the pullback composition of x3 and x4 (from the name)

Let $x_{3}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Let $x_{4}$ be a homomorphism of $R$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, the set of categories of rings, $K$ and $\mathrm{K'}$ and $\mathrm{R'}$. Then the pullback composition of $x_{3}$ and $x_{4}$ is an isomorphism of the composition of the pullback functor of $x_{3}$ and the pullback functor of $x_{4}$ and the pullback functor of the composition of $x_{3}$ and the map of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $x_{4}$ defined as the left adjoint composition isomorphism of the pullback pushforward adjunction of the composition of $x_{3}$ and the map of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $x_{4}$ and the pushforward composition of $x_{3}$ and $x_{4}$.

the pullback identity of S (from the name)

Let $S$ be a sheaf of $J$ and the set of categories of rings. Then the pullback identity of $S$ is an isomorphism of the pullback functor of the identity morphism of $S$ and the identity of the set of sheaves of module of $S$ defined as the left adjoint identity isomorphism of the pullback pushforward adjunction of the identity morphism of $S$ and the pushforward identity of $S$.

the pullback isomorphism of x2 (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Then the pullback isomorphism of $x_{2}$ is an isomorphism of the pullback functor of $x_{2}$ and the composition of the forgetful functor of $S$ and the composition of the pullback functor of the homomorphism of $x_{2}$ and the sheafification of the identity morphism of the object of $R$ defined as $\operatorname{leftAdjointUniq}$ applied to the pullback pushforward adjunction of $x_{2}$ and the adjunction of $x_{2}$.

the pullback pushforward adjunction of x2 (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Then the pullback pushforward adjunction of $x_{2}$ is an adjunction of the pullback functor of $x_{2}$ and $\operatorname{pushforward}$ applied to $x_{2}$ defined as the adjunction of $\operatorname{pushforward}$ applied to $x_{2}$.

the sheafification composition pullback of x2 (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Then the sheafification composition pullback of $x_{2}$ is an isomorphism of the composition of the sheafification of the identity morphism of the object of $S$ and the pullback functor of $x_{2}$ and the composition of the pullback functor of the homomorphism of $x_{2}$ and the sheafification of the identity morphism of the object of $R$ defined as $\operatorname{leftAdjointUniq}$ applied to the composition of the sheafification adjunction of the identity morphism of the object of $S$ and the pullback pushforward adjunction of $x_{2}$ and the composition of the pullback pushforward adjunction of the homomorphism of $x_{2}$ and the sheafification adjunction of the identity morphism of the object of $R$.

the canonical isomorphism of x2 (from the docstring)

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Then the canonical isomorphism of $x_{2}$ is an isomorphism of the composition of the functor and the pullback functor of $x_{2}$ and the functor.

the pullback of x2 and I (from the docstring)

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Let $I$ be a set. Then the pullback of $x_{2}$ and $I$ is an isomorphism of the action of the pullback functor of $x_{2}$ and the free of $I$ and the free of $I$ defined as the composition of the inverse of $\operatorname{asIso}$ applied to the sigma comparison of the pullback functor of $x_{2}$ and the function that maps $x_{3}$ to the unit of $S$ and the map isomorphism of the function that maps $x_{4}$ to $\operatorname{asIso}$ applied to the pullback object unit to unit of $x_{2}$.

the pullback object unit to unit of x2 (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Then the pullback object unit to unit of $x_{2}$ is a homomorphism of the action of the pullback functor of $x_{2}$ and the unit of $S$ and the unit of $R$ defined as $\operatorname{symm}$ applied to the homomorphism equivalence of the unit of $S$ and the unit of $R$ and the unit to pushforward object unit of $x_{2}$.

the pushforward section of x2 and s (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Let $s$ be a section of $M$. Then the pushforward section of $x_{2}$ and $s$ is a section of the action of $\operatorname{pushforward}$ applied to $x_{2}$ and $M$ defined as the function that maps $x_{3}$ to the action of the opposite of $F$ and $x_{3}$.

the unit to pushforward object unit of x2 (from the name)

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Then the unit to pushforward object unit of $x_{2}$ is a homomorphism of the unit of $S$ and the action of $\operatorname{pushforward}$ applied to $x_{2}$ and the unit of $R$.

Let $f$ be a homomorphism of $M$ and $N$. Let $X$ be an element of $D$. Then $\operatorname{over}$ applied to $f$ and $X$ is a homomorphism of $\operatorname{over}$ applied to $M$ and $X$ and $\operatorname{over}$ applied to $N$ and $X$ defined as the map of $\operatorname{overFunctor}$ applied to $R$ and $X$ and $f$.

Let $M$ be a sheaf of module of $R$. Let $X$ be an element of $D$. Then $\operatorname{over}$ applied to $M$ and $X$ is a sheaf of module of $\operatorname{over}$ applied to $R$ and $X$ defined as the action of $\operatorname{overFunctor}$ applied to $R$ and $X$ and $M$.

Let $R$ be a sheaf of $K$ and the set of categories of rings. Let $X$ be an element of $D$. Then $\operatorname{overFunctor}$ applied to $R$ and $X$ is a functor of the set of sheaves of module of $R$ and the set of sheaves of module of $\operatorname{over}$ applied to $R$ and $X$ defined as $\operatorname{pushforward}$ applied to the identity morphism of $\operatorname{over}$ applied to $R$ and $X$.

Let $R$ be a sheaf of $K$ and the set of categories of rings. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{overFunctorMap}$ applied to $R$ and $f$ is an isomorphism of the composition of $\operatorname{overFunctor}$ applied to $R$ and $Y$ and $\operatorname{overMap}$ applied to $R$ and $f$ and $\operatorname{overFunctor}$ applied to $R$ and $X$.

Let $R$ be a sheaf of $K$ and the set of categories of rings. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{overMap}$ applied to $R$ and $f$ is a functor of the set of sheaves of module of $\operatorname{over}$ applied to $R$ and $Y$ and the set of sheaves of module of $\operatorname{over}$ applied to $R$ and $X$ defined as $\operatorname{pushforward}$ applied to the inverse of $\operatorname{pushforwardOverMapIso}$ applied to $R$ and $f$.

Let $R$ be a sheaf of $J$ and the set of categories of rings. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{overMapPushforwardAdj}$ applied to $R$ and $f$ is an adjunction of $\operatorname{overMap}$ applied to $R$ and $f$ and $\operatorname{overPullback}$ applied to $R$ and $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{overMapUnitIso}$ applied to $f$ is an isomorphism of the action of $\operatorname{overMap}$ applied to $R$ and $f$ and the unit of $\operatorname{over}$ applied to $R$ and $Y$ and the unit of $\operatorname{over}$ applied to $R$ and $X$ defined as the identity of the action of $\operatorname{overMap}$ applied to $R$ and $f$ and the unit of $\operatorname{over}$ applied to $R$ and $Y$.

Let $R$ be a sheaf of $K$ and the set of categories of rings. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{overPullback}$ applied to $R$ and $f$ is a functor of the set of sheaves of module of $\operatorname{over}$ applied to $R$ and $X$ and the set of sheaves of module of $\operatorname{over}$ applied to $R$ and $Y$ defined as $\operatorname{pushforward}$ applied to $\operatorname{toPushforwardOverPullback}$ applied to $R$ and $f$.

Let $x_{1}$ be an element of $C$. Then $\operatorname{overPushforwardOverAdj}$ applied to $x_{1}$ is an adjunction of $\operatorname{pushforward}$ applied to the identity morphism of $\operatorname{over}$ applied to $R$ and $x_{1}$ and $\operatorname{pushforward}$ applied to $\operatorname{pushforwardOver}$ applied to $x_{1}$.

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Then $\operatorname{pushforward}$ applied to $x_{2}$ is a functor of the set of sheaves of module of $R$ and the set of sheaves of module of $S$.

the pushforward composition of x3 and x4 (from the name)

Let $x_{3}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Let $x_{4}$ be a homomorphism of $R$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, the set of categories of rings, $K$ and $\mathrm{K'}$ and $\mathrm{R'}$. Then the pushforward composition of $x_{3}$ and $x_{4}$ is an isomorphism of the composition of $\operatorname{pushforward}$ applied to $x_{4}$ and $\operatorname{pushforward}$ applied to $x_{3}$ and $\operatorname{pushforward}$ applied to the composition of $x_{3}$ and the map of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $x_{4}$ defined as the identity of the composition of $\operatorname{pushforward}$ applied to $x_{4}$ and $\operatorname{pushforward}$ applied to $x_{3}$.

Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Let $X$ be an opposite of $C$. Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Let $\mathrm{hX'}$ be an element of $\operatorname{IsInitial}$ applied to the action of the opposite of $F$ and $X$. Then $\operatorname{pushforwardCompForgetToSheafModuleCat}$ applied to $x_{2}$, $X$, $\mathrm{hX}$ and $\mathrm{hX'}$ is an isomorphism of the composition of $\operatorname{pushforward}$ applied to $x_{2}$ and $\operatorname{forgetToSheafModuleCat}$ applied to $S$, $X$ and $\mathrm{hX}$ and the composition of $\operatorname{forgetToSheafModuleCat}$ applied to $R$, the action of the opposite of $F$ and $X$ and $\mathrm{hX'}$ and the composition of $\operatorname{sheafCompose}$ applied to $K$ and $\operatorname{restrictScalars}$ applied to the homomorphism of the component of the homomorphism of $x_{2}$ and $X$ and $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of module categories of the set of carriers of the action of the object of $S$ and $X$, $J$ and $K$.

the pushforward congruence of e (from the name)

Assume that $\EqtMACRoH {x_{2}}{x_{3}}$. Then the pushforward congruence of $e$ is an isomorphism of $\operatorname{pushforward}$ applied to $x_{2}$ and $\operatorname{pushforward}$ applied to $x_{3}$.

the pushforward congruence of x2 and e (from the name)

Let $x_{2}$ be a homomorphism of $T$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, the set of categories of rings, $J$ and $K$ and $S$. Let $e$ be an isomorphism of $F$ and $G$. Assume that the composition of $x_{2}$ and the component of the sheaf pushforward continuous natural transformation of $J$ and $K$ and $S$ is equal to $x_{3}$. Then the pushforward congruence of $x_{2}$ and $e$ is an isomorphism of $\operatorname{pushforward}$ applied to $x_{2}$ and $\operatorname{pushforward}$ applied to $x_{3}$ defined as the composition of the pushforward natural isomorphism of $x_{2}$ and $e$ and the pushforward congruence of $\mathrm{he}$.

the pushforward identity of R (from the name)

Let $R$ be a sheaf of $K$ and the set of categories of rings. Then the pushforward identity of $R$ is an isomorphism of $\operatorname{pushforward}$ applied to the identity morphism of $R$ and the identity of the set of sheaves of module of $R$ defined as the identity of $\operatorname{pushforward}$ applied to the identity morphism of $R$.

the pushforward natural isomorphism of x2 and x3 (from the name)

Let $x_{2}$ be a homomorphism of $T$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, the set of categories of rings, $J$ and $K$ and $S$. Let $x_{3}$ be an isomorphism of $F$ and $G$. Then the pushforward natural isomorphism of $x_{2}$ and $x_{3}$ is an isomorphism of $\operatorname{pushforward}$ applied to $x_{2}$ and $\operatorname{pushforward}$ applied to the composition of $x_{2}$ and the component of the sheaf pushforward continuous natural transformation of $J$ and $K$ and $S$.

the pushforward natural transformation of x2 and x3 (from the name)

Let $x_{2}$ be a homomorphism of $T$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, the set of categories of rings, $J$ and $K$ and $S$. Let $x_{3}$ be a homomorphism of $F$ and $G$. Then the pushforward natural transformation of $x_{2}$ and $x_{3}$ is a homomorphism of $\operatorname{pushforward}$ applied to $x_{2}$ and $\operatorname{pushforward}$ applied to the composition of $x_{2}$ and the component of the sheaf pushforward continuous natural transformation of $J$ and $K$ and $S$.

Let $x_{1}$ be an element of $C$. Then $\operatorname{pushforwardOver}$ applied to $x_{1}$ is a homomorphism of $R$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to the star of $x_{1}$, the set of categories of rings, $J$ and $\operatorname{over}$ applied to $J$ and $x_{1}$ and $\operatorname{over}$ applied to $R$ and $x_{1}$.

the pushforward pushforward adjoint of x2 and x3 (from the name)

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $F$, the set of categories of rings, $J$ and $K$ and $R$. Let $x_{3}$ be a homomorphism of $R$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, the set of categories of rings, $K$ and $J$ and $S$ such that the right whisker of the opposite of the counit of $\mathrm{adj}$ and the object of $R$ is equal to the composition of the homomorphism of $x_{3}$ and the left whisker of the opposite of $G$ and the homomorphism of $x_{2}$ and the composition of the homomorphism of $x_{2}$ and the composition of the left whisker of the opposite of $F$ and the homomorphism of $x_{3}$ and the right whisker of the opposite of the unit of $\mathrm{adj}$ and the object of $S$ is equal to the identity morphism of the object of $S$. Then the pushforward pushforward adjoint of $x_{2}$ and $x_{3}$ is an adjunction of $\operatorname{pushforward}$ applied to $x_{2}$ and $\operatorname{pushforward}$ applied to $x_{3}$.

the pushforward pushforward equivalence of x2 and x3 (from the name)

Let $\mathrm{eqv}$ be an equivalence of $C$ and $D$. Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to the functor of $\mathrm{eqv}$, the set of categories of rings, $J$ and $K$ and $R$. Let $x_{3}$ be a homomorphism of $R$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to the inverse of $\mathrm{eqv}$, the set of categories of rings, $K$ and $J$ and $S$ such that the right whisker of the opposite of the counit of $\mathrm{eqv}$ and the object of $R$ is equal to the composition of the homomorphism of $x_{3}$ and the left whisker of the opposite of the inverse of $\mathrm{eqv}$ and the homomorphism of $x_{2}$ and the composition of the homomorphism of $x_{2}$ and the composition of the left whisker of the opposite of the functor of $\mathrm{eqv}$ and the homomorphism of $x_{3}$ and the right whisker of the opposite of the unit of $\mathrm{eqv}$ and the object of $S$ is equal to the identity morphism of the object of $S$. Then the pushforward pushforward equivalence of $x_{2}$ and $x_{3}$ is an equivalence of the set of sheaves of module of $R$ and the set of sheaves of module of $S$.

M is a finite presentation (from the name)

Let $M$ be a sheaf of module of $R$. Then we can say that $M$ is a finite presentation.

M is quasicoherent (from the name)

Let $M$ be a sheaf of module of $R$. Then we can say that $M$ is quasicoherent.

presentation of M (from the name)

Let $M$ be a sheaf of module of $R$. Then the presentations of $M$ are a basic type.

p is finite (from the name)

Let $p$ be a presentation of $M$. Then we can say that $p$ is finite.

the generator of self (from the name)

Let $\mathrm{self}$ be a presentation of $M$. Then the generator of $\mathrm{self}$ is a generating section of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $P$ be a presentation of $M$. Then $\operatorname{isColimit}$ applied to $P$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of the generator of $P$ and $\mathrm{SheafOfModules\_\_Presentation\_\_isColimit\_\_\_proof\_1}$ applied to $P$.

the map of F and x2 (from the name)

Let $P$ be a presentation of $M$. Let $F$ be a functor of the set of sheaves of module of $R$ and the set of sheaves of module of $S$. Let $x_{2}$ be an isomorphism of the unit of $S$ and the action of $F$ and the unit of $R$. Then the map of $F$ and $x_{2}$ is a presentation of the action of $F$ and $M$.

the map generator of F and x2 (from the name)

Let $P$ be a presentation of $M$. Let $F$ be a functor of the set of sheaves of module of $R$ and the set of sheaves of module of $S$. Let $x_{2}$ be an isomorphism of the unit of $S$ and the action of $F$ and the unit of $R$. Then the map generator of $F$ and $x_{2}$ is a homomorphism of the free of $\operatorname{I}$ applied to the generator of $P$ and the action of $F$ and $M$ defined as the map free homomorphism of $F$ and $x_{2}$.

the map relation of F and x2 (from the name)

Let $P$ be a presentation of $M$. Let $F$ be a functor of the set of sheaves of module of $R$ and the set of sheaves of module of $S$. Let $x_{2}$ be an isomorphism of the unit of $S$ and the action of $F$ and the unit of $R$. Then the map relation of $F$ and $x_{2}$ is a homomorphism of the free of $\operatorname{I}$ applied to the relation of $P$ and the free of $\operatorname{I}$ applied to the generator of $P$ defined as the composition of the homomorphism of the map free isomorphism of $F$ and $x_{2}$ and the composition of the map of $F$ and $\operatorname{symm}$ applied to the free homomorphism equivalence of the kernel of the projection of the generator of $P$ and $\operatorname{s}$ applied to the relation of $P$ and the composition of the map of $F$ and the inclusion of the projection of the generator of $P$ and the inverse of the map free isomorphism of $F$ and $x_{2}$.

the presentation of f and x1 (from the name)

Let $f$ be a homomorphism of $M$ and $N$. Let $x_{1}$ be a presentation of $M$. Then the presentation of $f$ and $x_{1}$ is a presentation of $N$.

the quasicoherent data of P (from the name)

Let $P$ be a presentation of $M$. Then the quasicoherent data of $P$ is a quasicoherent data of $M$.

the relation of self (from the name)

Let $\mathrm{self}$ be a presentation of $M$. Then the relation of $\mathrm{self}$ is a generating section of the kernel of the projection of the generator of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

quasicoherent data of M (from the name)

Let $M$ be a sheaf of module of $R$. Then the quasicoherent data of $M$ are a basic type.

Let $\mathrm{self}$ be a quasicoherent data of $M$. Then an element of $\operatorname{I}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

q is a finite presentation (from the name)

Let $q$ be a quasicoherent data of $M$. Then we can say that $q$ is a finite presentation.

Let $\mathrm{self}$ be a quasicoherent data of $M$. Let $x_{1}$ be an element of $\operatorname{I}$ applied to $\mathrm{self}$. Then $\operatorname{X}$ applied to $\mathrm{self}$ and $x_{1}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.

Let $M$ be a sheaf of module of $R$. Let $X$ be a function from elements of $I$ to elements of $C$ such that $\operatorname{CoversTop}$ holds for $J$ and $X$. Let $D$ be a function from elements $i$ of $I$ to quasicoherent data of $\operatorname{over}$ applied to $M$ and $X$ applied to $i$. Then $\operatorname{bind}$ applied to $M$, $X$, $\mathrm{hX}$, $i$ and $D$ is a quasicoherent data of $M$.

the local generator data of q (from the name)

Let $q$ be a quasicoherent data of $M$. Then the local generator data of $q$ is a local generator data of $M$ defined as $\operatorname{mk}$ applied to $\operatorname{I}$ applied to $q$, $\operatorname{X}$ applied to $q$, $\operatorname{coversTop}$ applied to $q$ and the function that maps $i$ to the generator of the presentation of $q$ and $i$.

the quasicoherent data of f and x1 (from the name)

Let $f$ be a homomorphism of $M$ and $N$. Let $x_{1}$ be a quasicoherent data of $M$. Then the quasicoherent data of $f$ and $x_{1}$ is a quasicoherent data of $N$.

the presentation of self and i (from the name)

Let $\mathrm{self}$ be a quasicoherent data of $M$. Let $i$ be an element of $\operatorname{I}$ applied to $\mathrm{self}$. Then the presentation of $\mathrm{self}$ and $i$ is a presentation of $\operatorname{over}$ applied to $M$ and $\operatorname{X}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $i$.

Let $G$ be a functor of $D$ and $C$. Let $x_{2}$ be a homomorphism of $S$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to $G$, the set of categories of rings, $K$ and $J$ and $R$. Let $x_{3}$ be an isomorphism of the action of $\operatorname{pushforward}$ applied to $x_{2}$ and the unit of $R$ and the unit of $S$. Assume that for all elements $X$ of $D$, for all elements $Y$ of $C$, for all homomorphisms $f$ of the action of $G$ and $X$ and $Y$, $\operatorname{PreservesColimitsOfSize}$ holds for $\operatorname{pushforward}$ applied to the map of $\operatorname{sheafPushforwardContinuous}$ applied to $\operatorname{forget}$ applied to $X$, the set of categories of rings, $\operatorname{over}$ applied to $K$ and $X$ and $K$ and $x_{2}$. Let $P$ be a quasicoherent data of $M$. Then $\operatorname{pushforward}$ applied to $G$, $x_{2}$, $x_{3}$, $h_{8}$ and $P$ is a quasicoherent data of the action of $\operatorname{pushforward}$ applied to $x_{2}$ and $M$.

the shrink of q (from the name)

Let $q$ be a quasicoherent data of $M$. Then the shrink of $q$ is a quasicoherent data of $M$.

the generator of g and #4 (from the name)

Let $f$ be a homomorphism of the free of $x_{1}$ and the free of $x_{2}$. Let $g$ be a homomorphism of the free of $x_{2}$ and $M$ such that the composition of $f$ and $g$ is equal to $0$. Let $\mathrm{H'}$ be an element of $\operatorname{IsColimit}$ applied to the projection of $g$ and $H$. Then the generator of $g$ and $\mathrm{H'}$ is a generating section of $M$.

Let $R$ be a sheaf of $J$ and the set of categories of rings. Then there is an object property of the set of sheaves of module of $R$. Proof. Let $R$ be arbitrary. By SheafOfModules__IsFinitePresentation.

Let $R$ be a sheaf of $J$ and the set of categories of rings. Then there is an object property of the set of sheaves of module of $R$. Proof. Let $R$ be arbitrary. By SheafOfModules__IsQuasicoherent.

the presentation of g and #4 (from the name)

Let $f$ be a homomorphism of the free of $x_{1}$ and the free of $x_{2}$. Let $g$ be a homomorphism of the free of $x_{2}$ and $M$ such that the composition of $f$ and $g$ is equal to $0$. Let $\mathrm{H'}$ be an element of $\operatorname{IsColimit}$ applied to the projection of $g$ and $H$. Then the presentation of $g$ and $\mathrm{H'}$ is a presentation of $M$ defined as $\operatorname{mk}$ applied to the generator of $g$ and $\mathrm{H'}$ and the relation of $g$ and $\mathrm{H'}$.

the relation of g and #4 (from the name)

Let $f$ be a homomorphism of the free of $x_{1}$ and the free of $x_{2}$. Let $g$ be a homomorphism of the free of $x_{2}$ and $M$ such that the composition of $f$ and $g$ is equal to $0$. Let $\mathrm{H'}$ be an element of $\operatorname{IsColimit}$ applied to the projection of $g$ and $H$. Then the relation of $g$ and $\mathrm{H'}$ is a generating section of the kernel of the projection of the generator of $g$ and $\mathrm{H'}$.

submodule of M (from the name)

Let $M$ be a sheaf of module of $R$. Then the submodules of $M$ are a basic type.

the sheaf of N (from the name)

Let $N$ be a submodule of $M$. Then the sheaf of $N$ is a sheaf of module of $R$.

the inclusion of N (from the name)

Let $N$ be a submodule of $M$. Then the inclusion of $N$ is a homomorphism of the sheaf of $N$ and $M$ defined as $\operatorname{mk}$ applied to the inclusion of $\operatorname{toSubmodule}$ applied to $N$.

the scalar multiple of r and m (from the name)

Let $R$ be a functor of $C$ and the set of categories of rings. Let $M$ be a functor of $C$ and the set of abelian groups such that for all elements $i$ and $j$ of $C$, for all homomorphisms $f$ of $i$ and $j$, for all carriers $r_{1}$ of the action of $R$ and $i$, for all carriers $m_{1}$ of the action of $M$ and $i$, $\EqtMACRoH {\operatorname{hom} (\operatorname{map} (M , f), \HSMulhSMulMACRoAL {r_{1}}{m_{1}})}{\HSMulhSMulMACRoAL {\operatorname{hom} (\operatorname{map} (R , f), r_{1})}{\operatorname{hom} (\operatorname{map} (M , f), m_{1})}}$. Let $r$ be a colimit type of the composition of $R$ and the forgetful functor of the set of categories of rings. Let $m$ be a colimit type of the composition of $M$ and the forgetful functor of the set of abelian groups. Then the scalar multiple of $r$ and $m$ is a colimit type of the composition of $M$ and the forgetful functor of the set of abelian groups.

the subobject module of M (from the name)

Let $M$ be a module category of $R$. Then the subobject module of $M$ is an order isomorphism of the set of subobjects of $M$ and the set of submodules of $R$ and the set of carriers of $M$.

the kernel subobject (from the name)

The kernel subobject is a linear map of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{hom} (f))}{x_{1}})}$ and the set of carriers of the action of $\operatorname{underlying}$ and the kernel of $f$ defined as the homomorphism of the inverse of the composition of the kernel subobject isomorphism of $f$ and the categorical kernel in $f$.

Let $R$ be a set. Then $\mathrm{ringEquivEndForget\_u2082\_}$ applied to $R$ is a ring isomorphism of $R$ and the set of ends of $\operatorname{of}$ applied to the forgetful functor of the set of module categories of $R$ and the set of additive commutative group categories.

the continuous linear equivalence of e (from the name)

Let $e$ be an isomorphism of $X$ and $Y$. Then the continuous linear equivalence of $e$ is a continuous linear equivalence of the set of carriers of $\operatorname{toModuleCat}$ applied to $X$ and the set of carriers of $\operatorname{toModuleCat}$ applied to $Y$.

top module category of R (from the name)

Let $R$ be a set. Then the top module categories of $R$ are a basic type.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be top module categories of $R$. Then the homomorphisms of $X$ and $Y$ are a basic type.

the homomorphism of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a continuous linear map of the set of carriers of $\operatorname{toModuleCat}$ applied to $X$ and the set of carriers of $\operatorname{toModuleCat}$ applied to $Y$ defined as the homomorphism of $f$.

the homomorphism of self (from the name)

Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a continuous linear map of the set of carriers of $\operatorname{toModuleCat}$ applied to $X$ and the set of carriers of $\operatorname{toModuleCat}$ applied to $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $\operatorname{toModuleCat}$ applied to $X$ applied to $i$ and $M$. Then $\operatorname{coinduced}$ applied to $i$ and $f$ is a top module category of $R$ defined as the function that maps $f$ to $\operatorname{of}$ applied to $R$, the set of carriers of $M$ and $f$.

the ring isomorphism between the endomorphisms of M (from the docstring)

Let $M$ be a top module category of $R$. Then the ring isomorphism between the endomorphisms of $M$ is a ring isomorphism of the set of ends of $M$ and the set of continuous linear maps of the set of carriers of $\operatorname{toModuleCat}$ applied to $M$ and the set of carriers of $\operatorname{toModuleCat}$ applied to $M$.

the free topological module of R (from the docstring)

Let $R$ be a set. Then the free topological module of $R$ is a functor of the set of topological categories and the set of top module categories of $R$.

the free adjoint of R (from the name)

Let $R$ be a set. Then the free adjoint of $R$ is an adjunction of the free topological module of $R$ and the forgetful functor of the set of top module categories of $R$ and the set of topological categories.

the free topological module of R and f (from the docstring)

Let $R$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the free topological module of $R$ and $f$ is a homomorphism of the free topological module of $R$ and $X$ and the free topological module of $R$ and $Y$.

the free topological module of R and X (from the docstring)

Let $R$ be a set. Let $X$ be a topological category. Then the free topological module of $R$ and $X$ is a top module category of $R$ defined as $\operatorname{of}$ applied to $R$ and the set of finitely supported functions from the set of carriers of $X$ to $R$.

Let $f$ be a function from elements $i_{1}$ of $I$ to homomorphisms of $M$ and $\operatorname{toModuleCat}$ applied to $X$ applied to $i_{1}$. Let $i$ be an element of $I$. Then $\operatorname{fromInduced}$ applied to $i_{1}$, $f$ and $i$ is a homomorphism of $\operatorname{induced}$ applied to $f$ and $X$ applied to $i$.

Let $R$ be a set. Then $\operatorname{indiscrete}$ applied to $R$ is a functor of the set of module categories of $R$ and the set of top module categories of $R$.

the indiscrete adjoint of R (from the name)

Let $R$ be a set. Then the indiscrete adjoint of $R$ is an adjunction of the forgetful functor of the set of top module categories of $R$ and the set of module categories of $R$ and $\operatorname{indiscrete}$ applied to $R$.

Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $M$ and $\operatorname{toModuleCat}$ applied to $X$ applied to $i$. Then $\operatorname{induced}$ applied to $i$ and $f$ is a top module category of $R$ defined as the function that maps $f$ to $\operatorname{of}$ applied to $R$, the set of carriers of $M$ and $f$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimit}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the top module category of $c$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimit}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the top module category of $c$.

Let $R$ and $M$ be sets. Then $\operatorname{of}$ applied to $R$ and $M$ is a top module category of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $R$ and $M$.

the top module category of c (from the name)

Let $c$ be a cocone of the composition of $F$ and the forgetful functor of the set of top module categories of $R$ and the set of module categories of $R$. Then the top module category of $c$ is a cocone of $F$.

the top module category of c (from the name)

Let $c$ be a cone of the composition of $F$ and the forgetful functor of the set of top module categories of $R$ and the set of module categories of $R$. Then the top module category of $c$ is a cone of $F$.

the top module category of f (from the name)

Let $f$ be a continuous linear map of $X$ and $Y$. Then the top 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$.

the top module category of e (from the name)

Let $e$ be a continuous linear equivalence of the set of carriers of $\operatorname{toModuleCat}$ applied to $X$ and the set of carriers of $\operatorname{toModuleCat}$ applied to $Y$. Then the top module category of $e$ is an isomorphism of $X$ and $Y$.

Let $f$ be a function from elements $i_{1}$ of $I$ to homomorphisms of $\operatorname{toModuleCat}$ applied to $X$ applied to $i_{1}$ and $M$. Let $i$ be an element of $I$. Then $\operatorname{toCoinduced}$ applied to $i_{1}$, $f$ and $i$ is a homomorphism of $X$ applied to $i$ and $\operatorname{coinduced}$ applied to $f$.

Let $R$ be a set. Then $\operatorname{withModuleTopology}$ applied to $R$ is a functor of the set of module categories of $R$ and the set of top module categories of $R$.

Let $R$ be a set. Then $\operatorname{withModuleTopologyAdj}$ applied to $R$ is an adjunction of $\operatorname{withModuleTopology}$ applied to $R$ and the forgetful functor of the set of top module categories of $R$ and the set of module categories of $R$.

the cokernel of x2 (from the name)

Let $x_{2}$ be a homomorphism of $M$ and $N$. Then the cokernel of $x_{2}$ is a top module category of $R$ defined as $\operatorname{of}$ applied to $R$ and the set of quotients of the set of carriers of $\operatorname{toModuleCat}$ applied to $N$ and the range of $\operatorname{toLinearMap}$ applied to the homomorphism of $x_{2}$.

the projection map to the cokernel in x2 (from the docstring)

Let $x_{2}$ be a homomorphism of $M$ and $N$. Then the projection map to the cokernel in $x_{2}$ is a homomorphism of $N$ and the cokernel of $x_{2}$.

Let $x_{2}$ be a homomorphism of $M$ and $N$. Then $\operatorname{isColimitCoker}$ applied to $x_{2}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection map to the cokernel in $x_{2}$ and $\mathrm{TopModuleCat\_\_comp\_coker\_u3c0\_}$ applied to $x_{2}$.

Let $x_{2}$ be a homomorphism of $M$ and $N$. Then $\operatorname{isLimitKer}$ applied to $x_{2}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion map from the kernel in $x_{2}$ and $\mathrm{TopModuleCat\_\_ker\_u3b9\_\_comp}$ applied to $x_{2}$.

the kernel of x2 (from the name)

Let $x_{2}$ be a homomorphism of $M$ and $N$. Then the kernel of $x_{2}$ is a top module category of $R$ defined as $\operatorname{of}$ applied to $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{toLinearMap} (\operatorname{hom} (x_{2})))}{x_{3}})}$.

the inclusion map from the kernel in x2 (from the docstring)

Let $x_{2}$ be a homomorphism of $M$ and $N$. Then the inclusion map from the kernel in $x_{2}$ is a homomorphism of the kernel of $x_{2}$ and $M$.

the fully faithful lift functor of R (from the name)

the lift functor of R (from the name)

Let $R$ be a set. Then the lift functor of $R$ is a functor of the set of module categories of $R$ and the set of module categories of $R$.

Let $R$ be a set. Then $\operatorname{uliftFunctorForgetIso}$ applied to $R$ is an isomorphism of the composition of the lift functor of $R$ and the forgetful functor of the set of module categories of $R$ and the composition of the forgetful functor of the set of module categories of $R$ and the functor embedding defined as the identity of the composition of the lift functor of $R$ and the forgetful functor of the set of module categories of $R$.

the adjoint (from the name)

The adjoint is an adjunction of the free functor and the forgetful functor of the set of additive commutative monoid categories.

the free functor (from the docstring)

The free functor is a functor of the set of sets and the set of additive commutative monoid categories.

the adjoint (from the name)

The adjoint is an adjunction of the free functor and the forgetful functor of the set of additive monoid categories.

$\operatorname{adjoinZero}$ is a functor of $\mathrm{AddSemigrp}$ and the set of additive monoid categories.

$\operatorname{adjoinZeroAdj}$ is an adjunction of $\operatorname{adjoinZero}$ and the forgetful functor of the set of additive monoid categories and $\mathrm{AddSemigrp}$.

the free functor (from the docstring)

The free functor is a functor of the set of sets and the set of additive monoid categories.

the adjoint (from the name)

The adjoint is an adjunction of the free functor and the forgetful functor of the set of monoid categories.

$\operatorname{adjoinOne}$ is a functor of $\mathrm{Semigrp}$ and the set of monoid categories.

$\operatorname{adjoinOneAdj}$ is an adjunction of $\operatorname{adjoinOne}$ and the forgetful functor of the set of monoid categories and $\mathrm{Semigrp}$.

the free functor (from the docstring)

The free functor is a functor of the set of sets and the set of monoid categories.

additive commutative monoid category (from the name)

The additive commutative monoid categories are a basic type.

homomorphism of A and B (from the name)

Let $A$ and $B$ be additive commutative monoid categories. Then the homomorphisms of $A$ and $B$ are a basic type.

the homomorphism of f (from the name)

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$.

the underlying monoid homomorphism of self (from the docstring)

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}$.

carrier of self (from the name)

Let $\mathrm{self}$ be an additive commutative monoid category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

the equivalence (from the name)

The equivalence is an equivalence of the set of additive commutative monoid categories and the set of commutative monoid categories.

$\operatorname{fullyFaithfulForgetToAddMonCat}$ is an element of $\operatorname{FullyFaithful}$ applied to the forgetful functor of the set of additive commutative monoid categories and the set of additive monoid categories.

Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is an additive commutative monoid category defined as $\operatorname{mk}$ applied to $M$.

the additive commutative monoid category of f (from the name)

Let $f$ be an additive monoid homomorphism of $X$ and $Y$. Then the additive commutative monoid 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$.

the lift functor (from the name)

The lift functor is a functor of the set of additive commutative monoid categories and the set of additive commutative monoid categories.

the additive commutative monoid category isomorphism of e (from the name)

Let $e$ be an additive equivalence of $X$ and $Y$. Then the additive commutative monoid category isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

the additive monoid category isomorphism of e (from the name)

Let $e$ be an additive equivalence of $X$ and $Y$. Then the additive monoid category isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

additive monoid category (from the name)

The additive monoid categories are a basic type.

homomorphism of A and B (from the name)

Let $A$ and $B$ be additive monoid categories. Then the homomorphisms of $A$ and $B$ are a basic type.

the homomorphism of f (from the name)

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$.

the underlying monoid homomorphism of self (from the docstring)

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}$.

carrier of self (from the name)

Let $\mathrm{self}$ be an additive monoid category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

the equivalence (from the name)

The equivalence is an equivalence of the set of additive monoid categories and the set of monoid categories.

Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is an additive monoid category defined as $\operatorname{mk}$ applied to $M$.

the additive monoid category of f (from the name)

Let $f$ be an additive monoid homomorphism of $X$ and $Y$. Then the additive monoid 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$.

the lift functor (from the name)

The lift functor is a functor of the set of additive monoid categories and the set of additive monoid categories.

the additive monoid category isomorphism to additive equivalence of i (from the name)

Let $i$ be an isomorphism of $X$ and $Y$. Then the additive monoid category isomorphism to additive equivalence of $i$ is an additive equivalence of the set of carriers of $X$ and the set of carriers of $Y$.

the commutative monoid category isomorphism to additive equivalence of i (from the name)

Let $i$ be an isomorphism of $X$ and $Y$. Then the commutative monoid category isomorphism to additive equivalence of $i$ is an additive equivalence of the set of carriers of $X$ and the set of carriers of $Y$.

the commutative monoid category isomorphism to multiplicative equivalence of i (from the name)

Let $i$ be an isomorphism of $X$ and $Y$. Then the commutative monoid category isomorphism to multiplicative equivalence of $i$ is a multiplicative equivalence of the set of carriers of $X$ and the set of carriers of $Y$.

the monoid category isomorphism to multiplicative equivalence of i (from the name)

Let $i$ be an isomorphism of $X$ and $Y$. Then the monoid category isomorphism to multiplicative equivalence of $i$ is a multiplicative equivalence of the set of carriers of $X$ and the set of carriers of $Y$.

commutative monoid category (from the name)

The commutative monoid categories are a basic type.

homomorphism of A and B (from the name)

Let $A$ and $B$ be commutative monoid categories. Then the homomorphisms of $A$ and $B$ are a basic type.

the homomorphism of f (from the name)

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$.

the underlying monoid homomorphism of self (from the docstring)

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}$.

carrier of self (from the name)

Let $\mathrm{self}$ be a commutative monoid category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

$\operatorname{fullyFaithfulForgetToMonCat}$ is an element of $\operatorname{FullyFaithful}$ applied to the forgetful functor of the set of commutative monoid categories and the set of monoid categories.

Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is a commutative monoid category defined as $\operatorname{mk}$ applied to $M$.

the commutative monoid category of f (from the name)

Let $f$ be a monoid homomorphism of $X$ and $Y$. Then the commutative monoid 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$.

the lift functor (from the name)

The lift functor is a functor of the set of commutative monoid categories and the set of commutative monoid categories.

monoid category (from the name)

The monoid categories are a basic type.

homomorphism of A and B (from the name)

Let $A$ and $B$ be monoid categories. Then the homomorphisms of $A$ and $B$ are a basic type.

the homomorphism of f (from the name)

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$.

the underlying monoid homomorphism of self (from the docstring)

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}$.

carrier of self (from the name)

Let $\mathrm{self}$ be a monoid category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is a monoid category defined as $\operatorname{mk}$ applied to $M$.

the monoid category of f (from the name)

Let $f$ be a monoid homomorphism of $X$ and $Y$. Then the monoid 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$.

the lift functor (from the name)

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

the commutative monoid category isomorphism of e (from the name)

Let $e$ be a multiplicative equivalence of $X$ and $Y$. Then the commutative monoid category isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

the monoid category isomorphism of e (from the name)

Let $e$ be a multiplicative equivalence of $X$ and $Y$. Then the monoid category isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

the additive equivalence isomorphism additive commutative monoid category isomorphism (from the name)

The additive equivalence isomorphism additive commutative monoid category isomorphism is an isomorphism of the set of additive equivalences of $X$ and $Y$ and the set of isomorphisms of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

the additive equivalence isomorphism additive monoid category isomorphism (from the name)

The additive equivalence isomorphism additive monoid category isomorphism is an isomorphism of the set of additive equivalences of $X$ and $Y$ and the set of isomorphisms of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

the multiplicative equivalence isomorphism commutative monoid category isomorphism (from the name)

The multiplicative equivalence isomorphism commutative monoid category isomorphism is an isomorphism of the set of multiplicative equivalences of $X$ and $Y$ and the set of isomorphisms of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

the multiplicative equivalence isomorphism monoid category isomorphism (from the name)

The multiplicative equivalence isomorphism monoid category isomorphism is an isomorphism of the set of multiplicative equivalences of $X$ and $Y$ and the set of isomorphisms of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

underlying type of the colimit in F (from the docstring)

Let $F$ be a functor of $J$ and the set of monoid categories. Then an underlying type of the colimit in $F$ is an element of the function that maps $F$ to $\mathrm{Quotient}$ applied to $\operatorname{colimitSetoid}$ applied to $F$.

Let $F$ be a functor of $J$ and the set of monoid categories. Then the elements of $\operatorname{Prequotient}$ applied to $F$ are a basic type.

Let $\mathrm{ctorIdx}$ be a natural number. 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 $j$ of $J$ and carriers $x_{1}$ of the action of $F$ and $j$ to elements of $\mathrm{motive}$ applied to $\operatorname{of}$ applied to $j$ and $x_{1}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the one and $\mathrm{PULift}$ applied to the set of functions from elements $x_{2}$ of $\operatorname{Prequotient}$ applied to $F$ and elements $x_{3}$ of $\operatorname{Prequotient}$ applied to $F$ to elements of $\mathrm{motive}$ applied to the product of $x_{2}$ and $x_{3}$.

the product of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{Prequotient}$ applied to $F$. Then the product of $x_{1}$ and $x_{2}$ is an element of $\operatorname{Prequotient}$ applied to $F$.

Let $j$ be an element of $J$. Let $x_{1}$ be a carrier of the action of $F$ and $j$. Then $\operatorname{of}$ applied to $j$ and $x_{1}$ is an element of $\operatorname{Prequotient}$ applied to $F$.

the one (from the name)

The one is an element of $\operatorname{Prequotient}$ applied to $F$.

Let $F$ be a functor of $J$ and the set of monoid categories. Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{Prequotient}$ applied to $F$. Then we can say that $\operatorname{Relation}$ holds for $F$, $x_{1}$ and $x_{2}$.

Assume that $\operatorname{Relation}$ holds for $F$, $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.

the cocone function of j and x1 (from the name)

Let $F$ be a functor of $J$ and the set of monoid categories. Let $j$ be an element of $J$. Let $x_{1}$ be a carrier of the action of $F$ and $j$. Then the cocone function of $j$ and $x_{1}$ is an underlying type of the colimit in $F$ defined as $\operatorname{mk}$ applied to $\operatorname{r}$ and $\operatorname{of}$ applied to $j$ and $x_{1}$.

the cocone morphism of F and j (from the name)

Let $F$ be a functor of $J$ and the set of monoid categories. 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$.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of monoid categories. Then the colimit of $F$ is a monoid category defined as $\operatorname{of}$ applied to the set of underlying types of the colimit in $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of monoid categories. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of monoid categories. Then $\operatorname{colimitIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.

Let $F$ be a functor of $J$ and the set of monoid categories. Let $s$ be a cocone of $F$. Let $x_{1}$ be an underlying type of the colimit in $F$. Then $\operatorname{descFun}$ applied to $F$, $s$ and $x_{1}$ is a carrier of $\operatorname{pt}$ applied to $s$.

Let $F$ be a functor of $J$ and the set of monoid categories. Let $s$ be a cocone of $F$. Let $x_{1}$ be an element of $\operatorname{Prequotient}$ applied to $F$. Then $\operatorname{descFunLift}$ applied to $F$, $s$ and $x_{1}$ is a carrier of $\operatorname{pt}$ applied to $s$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{MonCat\_\_Colimits\_\_descFunLift\_\_\_f}$ applied to $F$ and $s$.

Let $F$ be a functor of $J$ and the set of monoid categories. Let $s$ be a cocone of $F$. Then $\operatorname{descMorphism}$ applied to $F$ and $s$ is a homomorphism of the colimit of $F$ and $\operatorname{pt}$ applied to $s$.

Let $F$ be a functor of $J$ and the set of additive commutative monoid categories. Then $\operatorname{M}$ 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 commutative monoid categories and the set of additive monoid categories.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of additive commutative monoid categories. Then the colimit of $F$ is an additive commutative monoid category defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{M}$ applied to $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of additive commutative monoid categories. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of additive commutative monoid 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 monoid 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 commutative monoid categories and the set of additive monoid categories.

Let $F$ be a functor of $J$ and the set of additive monoid categories. Then an element of $\operatorname{M}$ applied to $F$ is an element of the function that maps $F$ to the set of colimit types of the composition of $F$ and the forgetful functor of the set of additive monoid categories.

Let $F$ be a functor of $J$ and the set of additive monoid 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 an element of $\operatorname{M}$ applied to $F$ defined as the inclusion colimit type of $\operatorname{fst}$ applied to $x_{1}$ and $\operatorname{snd}$ applied to $x_{1}$.

the cocone morphism of F and j (from the name)

Let $F$ be a functor of $J$ and the set of additive monoid categories. 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$.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of additive monoid categories. Then the colimit of $F$ is an additive monoid category defined as $\operatorname{of}$ applied to $\operatorname{M}$ applied to $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of additive monoid categories. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of additive monoid categories. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.

Let $F$ be a functor of $J$ and the set of additive monoid categories. 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$.

Let $F$ be a functor of $J$ and the set of commutative monoid categories. Then $\operatorname{M}$ applied to $F$ is a monoid category defined as the colimit of the composition of $F$ and the forgetful functor of the set of commutative monoid categories and the set of monoid categories.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of commutative monoid categories. Then the colimit of $F$ is a commutative monoid category defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{M}$ applied to $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of commutative monoid categories. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of commutative monoid 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 monoid categories and the set of monoid categories and $\operatorname{colimitCoconeIsColimit}$ applied to the composition of $F$ and the forgetful functor of the set of commutative monoid categories and the set of monoid categories.

Let $F$ be a functor of $J$ and the set of monoid categories. Then an element of $\operatorname{M}$ applied to $F$ is an element of the function that maps $F$ to the set of colimit types of the composition of $F$ and the forgetful functor of the set of monoid categories.

Let $F$ be a functor of $J$ and the set of monoid 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 an element of $\operatorname{M}$ applied to $F$ defined as the inclusion colimit type of $\operatorname{fst}$ applied to $x_{1}$ and $\operatorname{snd}$ applied to $x_{1}$.

the cocone morphism of F and j (from the name)

Let $F$ be a functor of $J$ and the set of monoid categories. 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$.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of monoid categories. Then the colimit of $F$ is a monoid category defined as $\operatorname{of}$ applied to $\operatorname{M}$ applied to $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of monoid categories. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of monoid categories. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.

Let $F$ be a functor of $J$ and the set of monoid categories. 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$.

the forgetful functor (from the docstring)

The forgetful functor is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Natural$ and the forgetful functor of the set of additive commutative monoid categories.

the forgetful functor (from the docstring)

The forgetful functor is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Natural$ and the forgetful functor of the set of additive monoid categories.

the forgetful functor (from the docstring)

The forgetful functor 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 $\Natural$ and the forgetful functor of the set of commutative monoid categories.

the forgetful functor (from the docstring)

The forgetful functor 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 $\Natural$ and the forgetful functor of the set of monoid categories.

the lift multiple homomorphism of M (from the name)

Let $M$ be a set. Then the lift multiple homomorphism of $M$ is an equivalence from $M$ to the set of additive monoid homomorphisms of $\mathrm{ULift}$ applied to $\Natural$ and $M$ defined as the composition of the multiple homomorphism of $M$ and the equivalence of the inverse of the lift.

the lift power homomorphism of M (from the name)

Let $M$ be a set. Then the lift power homomorphism of $M$ is an equivalence from $M$ to the set of monoid homomorphisms of $\mathrm{ULift}$ applied to the set of multiplicatives of $\Natural$ and $M$ defined as the composition of the power homomorphism of $M$ and the equivalence of the inverse of the lift.