Definitions: Mathlib.AlgebraicGeometry, part 2 of 3

AlgebraicGeometry.Scheme.toSpecΓdefMathlib.AlgebraicGeometry.GammaSpecAdjunction, function or constant

Wording

the spectrum of X (from the name)

English

Let $X$ be a scheme. Then the spectrum of $X$ is a homomorphism of $X$ and the spectrum of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the top defined as the component of the unit of the adjunction and $X$.

AlgebraicGeometry.Spec.fullyFaithfuldefMathlib.AlgebraicGeometry.GammaSpecAdjunction, function or constant

Wording

no wording

English

$\operatorname{fullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the spectrum defined as $\operatorname{fullyFaithfulROfIsIsoCounit}$ applied to the adjunction.

AlgebraicGeometry.Spec.fullyFaithfulToLocallyRingedSpacedefMathlib.AlgebraicGeometry.GammaSpecAdjunction, function or constant

Wording

no wording

English

generation took over the time limit

AlgebraicGeometry.Spec.homEquivdefMathlib.AlgebraicGeometry.GammaSpecAdjunction, function or constant

Wording

the homomorphism equivalence (from the name)

English

The homomorphism equivalence is an equivalence from the set of homomorphisms of the spectrum of $S$ and the spectrum of $R$ to the set of homomorphisms of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{preimage}$, $\operatorname{map}$, $\mathrm{AlgebraicGeometry\_\_Spec\_\_map\_preimage}$ and $\mathrm{AlgebraicGeometry\_\_Spec\_\_preimage\_map}$.

AlgebraicGeometry.Spec.homEquivAlgHomdefMathlib.AlgebraicGeometry.GammaSpecAdjunction, function or constant

Wording

the homomorphism equivalence algebra homomorphism (from the name)

English

The homomorphism equivalence algebra homomorphism is an element of $\EquivMACRoAE {(\SubtypeSet {f}{(\EqtMACRoH {\operatorname{comp} (f , \operatorname{algebraMap} (R , A))}{\operatorname{algebraMap} (R , B)})})}{\mathrm{AlgHom} (A , B)}$.

AlgebraicGeometry.Spec.homEquivRingHomdefMathlib.AlgebraicGeometry.GammaSpecAdjunction, function or constant

Wording

the homomorphism equivalence ring homomorphism (from the name)

English

The homomorphism equivalence ring homomorphism is an equivalence from the set of homomorphisms of the spectrum of $\operatorname{of}$ applied to $S$ and the spectrum of $\operatorname{of}$ applied to $R$ to the set of ring homomorphisms of $R$ and $S$ defined as the composition of the homomorphism equivalence and the composition of the homomorphism equivalence and the identity of the set of homomorphisms of $\operatorname{of}$ applied to $R$ and $\operatorname{of}$ applied to $S$.

AlgebraicGeometry.Spec.preimagedefMathlib.AlgebraicGeometry.GammaSpecAdjunction, function or constant

Wording

the preimage of f (from the name)

English

Let $f$ be a homomorphism of the spectrum of $S$ and the spectrum of $R$. Then the preimage of $f$ is a homomorphism of $R$ and $S$ defined as the opposite of the choice of the spectrum and $f$.

AlgebraicGeometry.identityToΓSpecdefMathlib.AlgebraicGeometry.GammaSpecAdjunction, function or constant

Wording

the identity to spectrum (from the name)

English

generation took over the time limit

AlgebraicGeometry.ΓSpec.adjunctiondefMathlib.AlgebraicGeometry.GammaSpecAdjunction, function or constant

Wording

the adjunction (from the docstring)

English

The adjunction is an adjunction of the right opposite of $\mathrm{AlgebraicGeometry\_\_Scheme\_\_\_u393\_}$ and the spectrum.

AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunctiondefMathlib.AlgebraicGeometry.GammaSpecAdjunction, function or constant

Wording

the adjunction (from the docstring)

English

generation took over the time limit

Mathlib.AlgebraicGeometry.Geometrically.Basic

AlgebraicGeometry.geometricallydefMathlib.AlgebraicGeometry.Geometrically.Basic, function or constant

Wording

no wording

English

Let $P$ be an object property of the set of schemes. Then there is a morphism property of the set of schemes. Proof. Let $P$ be arbitrary. Let $X$ be arbitrary. Let $Y$ be arbitrary. Let $f$ be arbitrary. By Set. Let $K$ be arbitrary. By K. By Field. Let $x$ be arbitrary. By K. By CommRingCat__of. By AlgebraicGeometry__Spec. By Y. By Quiver__Hom. Let $y$ be arbitrary. By AlgebraicGeometry__Scheme. Let $Z$ be arbitrary. By Z. By X. By Quiver__Hom. Let $\mathrm{fst}$ be arbitrary. By Z. By K. By CommRingCat__of. By AlgebraicGeometry__Spec. By Quiver__Hom. Let $\mathrm{snd}$ be arbitrary. By fst. By snd. By f. By y. By CategoryTheory__IsPullback. By Z. By P. By if. By forall. By forall. By forall. By forall. By forall. By forall.

Mathlib.AlgebraicGeometry.Geometrically.Connected

AlgebraicGeometry.GeometricallyConnectedclassMathlib.AlgebraicGeometry.Geometrically.Connected, predicate

Wording

f is geometrically connected (from the name)

English

generation took over the time limit

AlgebraicGeometry.Scheme.Hom.connectedComponentsHomeomorphdefMathlib.AlgebraicGeometry.Geometrically.Connected, function or constant

Wording

the connected component homeomorphism of f and hf (from the name)

English

Let $f$ be a homomorphism of $X$ and $S$ such that $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ is an open map. Then the connected component homeomorphism of $f$ and $\mathrm{hf}$ is a homeomorphism of the set of connected components of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the set of connected components of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $S$.

Mathlib.AlgebraicGeometry.Geometrically.Integral

AlgebraicGeometry.GeometricallyIntegralclassMathlib.AlgebraicGeometry.Geometrically.Integral, predicate

Wording

f is geometrically integral (from the name)

English

generation took over the time limit

Mathlib.AlgebraicGeometry.Geometrically.Irreducible

AlgebraicGeometry.GeometricallyIrreducibleclassMathlib.AlgebraicGeometry.Geometrically.Irreducible, predicate

Wording

f is geometrically irreducible (from the name)

English

generation took over the time limit

AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquivdefMathlib.AlgebraicGeometry.Geometrically.Irreducible, function or constant

Wording

the irreducible component equivalence of f and hf (from the name)

English

Let $f$ be a homomorphism of $X$ and $S$ such that $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ is an open map. Then the irreducible component equivalence of $f$ and $\mathrm{hf}$ is an equivalence from the set of elements of the irreducible component of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ to the set of elements of the irreducible component of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $S$.

Mathlib.AlgebraicGeometry.Geometrically.Reduced

AlgebraicGeometry.GeometricallyReducedclassMathlib.AlgebraicGeometry.Geometrically.Reduced, predicate

Wording

f is geometrically reduced (from the name)

English

generation took over the time limit

Mathlib.AlgebraicGeometry.Gluing

AlgebraicGeometry.Scheme.Cover.fromGlueddefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the canonical morphism from the gluing of x (from the docstring)

English

Let $x$ be an open cover of $X$. Then the canonical morphism from the gluing of $x$ is a homomorphism of the glued scheme of the glue data associated with an open cover of $x$ and $X$.

AlgebraicGeometry.Scheme.Cover.glueMorphismsdefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the glue morphism of x and f (from the name)

English

Let $x$ be an open cover of $X$. Let $f$ be a function from elements $x_{2}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ to homomorphisms of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $x_{2}$ and $Y$ such that for all elements $x_{1}$ and $y$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$, the composition of the first projection of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $x_{1}$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $y$ and $f$ applied to $x_{1}$ is equal to the composition of the second projection of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $x_{1}$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $y$ and $f$ applied to $y$. Then the glue morphism of $x$ and $x_{2}$ is a homomorphism of $X$ and $Y$.

AlgebraicGeometry.Scheme.Cover.gluedCoverdefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the glue data associated with an open cover of x (from the docstring)

English

Let $x$ be an open cover of $X$. Then the glue data associated with an open cover of $x$ is a glue data.

AlgebraicGeometry.Scheme.Cover.gluedCoverT'defMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the glued cover of y and z (from the name)

English

Let $x$ be an open cover of $X$. Let $x_{1}$, $y$ and $z$ be elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$. Then the glued cover of $y$ and $z$ is a homomorphism of the pullback of the first projection of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $x_{1}$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $y$ and the first projection of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $x_{1}$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $z$ and the pullback of the first projection of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $y$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $z$ and the first projection of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $y$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $x_{1}$.

AlgebraicGeometry.Scheme.GlueDatastructureMathlib.AlgebraicGeometry.Gluing, type

Wording

glue data (from the name)

English

The glue data are a basic type.

AlgebraicGeometry.Scheme.GlueData.ReldefMathlib.AlgebraicGeometry.Gluing, predicate

Wording

no wording

English

Let $D$ be a glue data. Let $a$ be an element of $\Sigma$ applied to the function that maps $i_{1}$ to the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i_{1}$. Let $b$ be an element of $\Sigma$ applied to the function that maps $i$ to the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$. Then $\operatorname{Rel}$ holds for $D$, $a$ and $b$, if there exists a carrier $x$ of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $\operatorname{V}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $\ProdmkMACRoU {\operatorname{fst} (a)}{\operatorname{fst} (b)}$, such that $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $\operatorname{f}$ applied to $\operatorname{toGlueData}$ applied to $D$, $\operatorname{fst}$ applied to $a$ and $\operatorname{fst}$ applied to $b$ and $x$ is equal to $\operatorname{snd}$ applied to $a$ and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the composition of $\operatorname{t}$ applied to $\operatorname{toGlueData}$ applied to $D$, $\operatorname{fst}$ applied to $a$ and $\operatorname{fst}$ applied to $b$ and $\operatorname{f}$ applied to $\operatorname{toGlueData}$ applied to $D$, $\operatorname{fst}$ applied to $b$ and $\operatorname{fst}$ applied to $a$ and $x$ is equal to $\operatorname{snd}$ applied to $b$.

AlgebraicGeometry.Scheme.GlueData.glueddefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the glued scheme of D (from the docstring)

English

Let $D$ be a glue data. Then the glued scheme of $D$ is a scheme defined as $\operatorname{glued}$ applied to $\operatorname{toGlueData}$ applied to $D$.

AlgebraicGeometry.Scheme.GlueData.gluedSchemedefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the glued scheme of D (from the name)

English

Let $D$ be a glue data. Then the glued scheme of $D$ is a scheme.

AlgebraicGeometry.Scheme.GlueData.isoCarrierdefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the isomorphism carrier of D (from the name)

English

generation took over the time limit

AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpacedefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the isomorphism locally ringed space of D (from the name)

English

generation took over the time limit

AlgebraicGeometry.Scheme.GlueData.openCoverdefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the open cover of D (from the name)

English

Let $D$ be a glue data. Then the open cover of $D$ is an open cover of the glued scheme of $D$.

AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueDatadefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the locally ringed space glue data of D (from the name)

English

generation took over the time limit

AlgebraicGeometry.Scheme.GlueData.vPullbackConedefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the pullback cone of i and j (from the name)

English

Let $D$ be a glue data. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$. Then the pullback cone of $i$ and $j$ is a pullback cone of the inclusion of $D$ and $i$ and the inclusion of $D$ and $j$.

AlgebraicGeometry.Scheme.GlueData.vPullbackConeIsLimitdefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

no wording

English

generation took over the time limit

AlgebraicGeometry.Scheme.GlueData.ιdefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the inclusion of D and i (from the name)

English

Let $D$ be a glue data. Let $i$ be an element of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$. Then the inclusion of $D$ and $i$ is a homomorphism of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$ and the glued scheme of $D$ defined as the inclusion of $\operatorname{toGlueData}$ applied to $D$ and $i$.

AlgebraicGeometry.Scheme.IsLocallyDirected.VdefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of schemes. Let $i$ and $j$ be elements of $J$. Then $\operatorname{V}$ applied to $F$, $i$ and $j$ is an open of the action of $F$ and $i$ defined as the supremum of the function that maps $k$ to the image of the map of $F$ and $\ProdfstMACRoZ {\operatorname{snd} (k)}$.

AlgebraicGeometry.Scheme.IsLocallyDirected.coconedefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the cocone of F (from the name)

English

Let $F$ be a functor of $J$ and the set of schemes. Then the cocone of $F$ is a cocone of $F$.

AlgebraicGeometry.Scheme.IsLocallyDirected.glueDatadefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the glue data of F (from the name)

English

Let $F$ be a functor of $J$ and the set of schemes. Then the glue data of $F$ is a glue data.

AlgebraicGeometry.Scheme.IsLocallyDirected.isColimitdefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

no wording

English

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

AlgebraicGeometry.Scheme.IsLocallyDirected.isColimitForgetToLocallyRingedSpacedefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of schemes. Then $\operatorname{isColimitForgetToLocallyRingedSpace}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of $\operatorname{forgetToLocallyRingedSpace}$ and the cocone of $F$.

AlgebraicGeometry.Scheme.IsLocallyDirected.openCoverdefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

the open cover of the colimit of F (from the docstring)

English

Let $F$ be a functor of $J$ and the set of schemes. Then the open cover of the colimit of $F$ is an open cover of the colimit of $F$.

AlgebraicGeometry.Scheme.IsLocallyDirected.tdefMathlib.AlgebraicGeometry.Gluing, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of schemes. Let $i$ and $j$ be elements of $J$. Then $\operatorname{t}$ applied to $F$, $i$ and $j$ is a homomorphism of the scheme of $\operatorname{V}$ applied to $F$, $i$ and $j$ and the scheme of $\operatorname{V}$ applied to $F$, $j$ and $i$.

Mathlib.AlgebraicGeometry.GluingOneHypercover

AlgebraicGeometry.Scheme.GlueData.oneHypercoverdefMathlib.AlgebraicGeometry.GluingOneHypercover, function or constant

Wording

the one hypercover of D (from the name)

English

Let $D$ be a glue data. Then the one hypercover of $D$ is an one hypercover of the Zariski topology and the glued scheme of $D$.

AlgebraicGeometry.Scheme.GlueData.sheafValGluedMkdefMathlib.AlgebraicGeometry.GluingOneHypercover, function or constant

Wording

no wording

English

Let $D$ be a glue data. Let $s$ be a function from elements $j_{1}$ of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$ to elements of the action of the object of $F$ and $\operatorname{op}$ applied to $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $j_{1}$ such that for all elements $i$ and $j$ of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$, $\operatorname{hom}$ applied to the map of the object of $F$ and the opposite in $\operatorname{f}$ applied to $\operatorname{toGlueData}$ applied to $D$, $i$ and $j$ and $s$ applied to $i$ is equal to $\operatorname{hom}$ applied to the map of the object of $F$ and the composition of the opposite in $\operatorname{f}$ applied to $\operatorname{toGlueData}$ applied to $D$, $j$ and $i$ and the opposite in $\operatorname{t}$ applied to $\operatorname{toGlueData}$ applied to $D$, $i$ and $j$ and $s$ applied to $j$. Then $\operatorname{sheafValGluedMk}$ applied to $D$, $j_{1}$, $s$ and $h$ is an element of the action of the object of $F$ and $\operatorname{op}$ applied to the glued scheme of $D$.

Mathlib.AlgebraicGeometry.Group.Affine

AlgebraicGeometry.Spec.mapMulEquivdefMathlib.AlgebraicGeometry.Group.Affine, function or constant

Wording

the map multiplicative equivalence (from the name)

English

The map multiplicative equivalence is a multiplicative equivalence of $\mathrm{WithConv}$ applied to the set of algebra homomorphisms of $S$ and $T$ and the set of homomorphisms of $\operatorname{asOver}$ applied to the spectrum of $\operatorname{of}$ applied to $T$ and the spectrum of $\operatorname{of}$ applied to $R$ and $\operatorname{asOver}$ applied to the spectrum of $\operatorname{of}$ applied to $S$ and the spectrum of $\operatorname{of}$ applied to $R$.

AlgebraicGeometry.algSpecdefMathlib.AlgebraicGeometry.Group.Affine, function or constant

Wording

the algebra spectrum of R (from the name)

English

Let $R$ be a category of commutative rings. Then the algebra spectrum of $R$ is a functor of the set of opposites of the set of commutative algebra categories of the set of carriers of $R$ and $\operatorname{Over}$ applied to the spectrum of $R$ defined as the composition of the functor of the opposite of $\mathrm{commAlgCatEquivUnder}$ applied to $R$ and the composition of the inverse of $\operatorname{opEquivOpUnder}$ applied to $R$ and the post of the spectrum.

AlgebraicGeometry.algSpec.fullyFaithfuldefMathlib.AlgebraicGeometry.Group.Affine, function or constant

Wording

no wording

English

$\operatorname{fullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the algebra spectrum of $R$ defined as the composition of the functor of the composition of the opposite of $\mathrm{commAlgCatEquivUnder}$ applied to $R$ and the inverse of $\operatorname{opEquivOpUnder}$ applied to $R$ and $\operatorname{over}$ applied to $\operatorname{op}$ applied to $R$, the spectrum and $\operatorname{fullyFaithful}$.

AlgebraicGeometry.algΓdefMathlib.AlgebraicGeometry.Group.Affine, function or constant

Wording

the algebra of R (from the name)

English

Let $R$ be a category of commutative rings. Then the algebra of $R$ is a functor of $\operatorname{Over}$ applied to the spectrum of $R$ and the set of opposites of the set of commutative algebra categories of the set of carriers of $R$ defined as the composition of the post of the right opposite of $\mathrm{AlgebraicGeometry\_\_Scheme\_\_\_u393\_}$ and the composition of the map of the opposite in the inverse of the spectrum isomorphism of $R$ and the composition of the functor of $\operatorname{opEquivOpUnder}$ applied to $R$ and the opposite of the inverse of $\mathrm{commAlgCatEquivUnder}$ applied to $R$.

AlgebraicGeometry.algΓAlgSpecAdjunctiondefMathlib.AlgebraicGeometry.Group.Affine, function or constant

Wording

the algebra algebra spectrum adjunction of R (from the name)

English

Let $R$ be a category of commutative rings. Then the algebra algebra spectrum adjunction of $R$ is an adjunction of the algebra of $R$ and the algebra spectrum of $R$.

AlgebraicGeometry.bialgSpecdefMathlib.AlgebraicGeometry.Group.Affine, function or constant

Wording

the bialgebra spectrum of R (from the name)

English

Let $R$ be a category of commutative rings. Then the bialgebra spectrum of $R$ is a functor of the set of opposites of the set of commutative bialgebra categories of the set of carriers of $R$ and the set of monoids of $\operatorname{Over}$ applied to the spectrum of $R$ defined as the composition of the left opposite of the functor of the commutative bialgebra category equivalence comonoid commutative algebra category of the set of carriers of $R$ and the map monoid of the algebra spectrum of $R$.

AlgebraicGeometry.bialgSpec.fullyFaithfuldefMathlib.AlgebraicGeometry.Group.Affine, function or constant

Wording

no wording

English

$\operatorname{fullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the bialgebra spectrum of $R$ defined as the composition of the opposite of the functor of the commutative bialgebra category equivalence comonoid commutative algebra category of the set of carriers of $R$ and the map monoid of $\operatorname{fullyFaithful}$.

AlgebraicGeometry.hopfSpecdefMathlib.AlgebraicGeometry.Group.Affine, function or constant

Wording

the Hopf spectrum of R (from the name)

English

Let $R$ be a category of commutative rings. Then the Hopf spectrum of $R$ is a functor of the set of opposites of the set of commutative Hopf algebra categories of the set of carriers of $R$ and the set of groups of $\operatorname{Over}$ applied to the spectrum of $R$ defined as the composition of the left opposite of the functor of $\mathrm{commHopfAlgCatEquivCogrpCommAlgCat}$ applied to the set of carriers of $R$ and the map group of the algebra spectrum of $R$.

AlgebraicGeometry.hopfSpec.fullyFaithfuldefMathlib.AlgebraicGeometry.Group.Affine, function or constant

Wording

no wording

English

$\operatorname{fullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the Hopf spectrum of $R$ defined as the composition of the opposite of the functor of $\mathrm{commHopfAlgCatEquivCogrpCommAlgCat}$ applied to the set of carriers of $R$ and the map group of $\operatorname{fullyFaithful}$.

AlgebraicGeometry.pullbackSpecIso'defMathlib.AlgebraicGeometry.Group.Affine, function or constant

Wording

the pullback spectrum isomorphism of S and T (from the name)

English

Let $R$, $S$ and $T$ be sets. Then the pullback spectrum isomorphism of $S$ and $T$ is an isomorphism of the pullback of $\operatorname{over}$ applied to the spectrum of $\operatorname{of}$ applied to $S$, the spectrum of $\operatorname{of}$ applied to $R$ and $\mathrm{inferInstance}$ and $\operatorname{over}$ applied to the spectrum of $\operatorname{of}$ applied to $T$, the spectrum of $\operatorname{of}$ applied to $R$ and $\mathrm{inferInstance}$ and the spectrum of $\operatorname{of}$ applied to the set of tensor products of $S$ and $T$ defined as the pullback spectrum isomorphism of the set of carriers of $\operatorname{of}$ applied to $S$ and the set of carriers of $\operatorname{of}$ applied to $T$.

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

AlgebraicGeometry.Scheme.Hom.kerdefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the kernel of $f$ is an ideal sheaf data of $Y$ defined as the ideal sheaf data of the function that maps $U$ to the kernel of the underlying ring hom of the homomorphism of $f$ and $U$.

AlgebraicGeometry.Scheme.IdealSheafDatastructureMathlib.AlgebraicGeometry.IdealSheaf.Basic, type

Wording

ideal sheaf data of X (from the name)

English

Let $X$ be a scheme. Then the ideal sheaf data of $X$ are a basic type.

AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffinedefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an order ring isomorphism of the set of ideal sheaf data of $X$ and the set of ideals of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the top.

AlgebraicGeometry.Scheme.IdealSheafData.gcidefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

no wording

English

$\operatorname{gci}$ is a Galois coinsertion of $\operatorname{ideal}$ and $\operatorname{ofIdeals}$.

AlgebraicGeometry.Scheme.IdealSheafData.idealdefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the component of self and U (from the docstring)

English

Let $\mathrm{self}$ be an ideal sheaf data of $X$. Let $U$ be an element of the affine open of $X$. Then the component of $\mathrm{self}$ and $U$ is an ideal of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $U$.

AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIffdefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

no wording

English

Let $\mathrm{ideal}$ be a function from elements $U_{2}$ of the affine open of $X$ to ideals of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U_{2}$ such that for all elements $U_{1}$ of the affine open of $X$, for all carriers $f$ of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U_{1}$, the map of the underlying ring hom of the map of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the opposite in the homomorphism of $\mathrm{AlgebraicGeometry\_\_Scheme\_\_basicOpen\_le}$ applied to $X$ and $f$ and $\mathrm{ideal}$ applied to $U_{1}$ is equal to $\mathrm{ideal}$ applied to $\operatorname{affineBasicOpen}$ applied to $X$ and $f$. Let $\mathrm{supportSet}$ be an element of the power set of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ such that for all elements $U$ of the affine open of $X$, for all carriers $x$ of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$, if $x$ is an element of $U$, then $x$ is an element of $\mathrm{supportSet}$, if and only if $x$ is an element of the zero locus of $X$ and $\mathrm{ideal}$ applied to $U$. Then $\operatorname{mkOfMemSupportIff}$ applied to $U_{2}$, $\mathrm{ideal}$, $\mathrm{map\_ideal\_basicOpen}$, $\mathrm{supportSet}$ and $\mathrm{supportSet\_inter}$ is an ideal sheaf data of $X$.

AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTopdefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the ideal sheaf induced by an ideal of the global sections of I (from the docstring)

English

Let $I$ be an ideal of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the top. Then the ideal sheaf induced by an ideal of the global sections of $I$ is an ideal sheaf data of $X$.

AlgebraicGeometry.Scheme.IdealSheafData.ofIdealsdefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the ideal sheaf data of I (from the name)

English

Let $I$ be a function from elements $U$ of the affine open of $X$ to ideals of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$. Then the ideal sheaf data of $U$ is an ideal sheaf data of $X$ defined as the function that maps $I$ to the supremum of $\operatorname{ofPred}$ applied to the function that maps $J$ to the proposition that $\operatorname{ideal}$ applied to $J$ is less than or equal to $U$.

AlgebraicGeometry.Scheme.IdealSheafData.radicaldefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the radical of I (from the docstring)

English

Let $I$ be an ideal sheaf data of $X$. Then the radical of $I$ is an ideal sheaf data of $X$.

AlgebraicGeometry.Scheme.IdealSheafData.supportdefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the support of I (from the docstring)

English

Let $I$ be an ideal sheaf data of $X$. Then the support of $I$ is an element of $\operatorname{Closeds}$ applied to the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ defined as $\operatorname{mk}$ applied to the support of $I$ and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_IdealSheafData\_\_isClosed\_supportSet}$ applied to $I$.

AlgebraicGeometry.Scheme.IdealSheafData.supportSetdefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the support of self (from the docstring)

English

Let $\mathrm{self}$ be an ideal sheaf data of $X$. Then the support of $\mathrm{self}$ is an element of the power set of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdealdefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the vanishing ideal sheaf of Z (from the docstring)

English

Let $Z$ be an element of $\operatorname{Closeds}$ applied to the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the vanishing ideal sheaf of $Z$ is an ideal sheaf data of $X$.

AlgebraicGeometry.Scheme.kerFunctordefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the kernel functor of Y (from the name)

English

Let $Y$ be a scheme. Then the kernel functor of $Y$ is a functor of the set of opposites of $\operatorname{Over}$ applied to $Y$ and the set of ideal sheaf data of $Y$.

AlgebraicGeometry.Scheme.nilradicaldefMathlib.AlgebraicGeometry.IdealSheaf.Basic, function or constant

Wording

the nilradical of X (from the docstring)

English

Let $X$ be a scheme. Then the nilradical of $X$ is an ideal sheaf data of $X$ defined as the radical of the bottom.

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

AlgebraicGeometry.Scheme.IdealSheafData.comapdefMathlib.AlgebraicGeometry.IdealSheaf.Functorial, function or constant

Wording

the preimage of I and f (from the name)

English

Let $I$ be an ideal sheaf data of $Y$. Let $f$ be a homomorphism of $X$ and $Y$. Then the preimage of $I$ and $f$ is an ideal sheaf data of $X$ defined as the kernel of the first projection of the pullback of $f$ and the subscheme inclusion of $I$.

AlgebraicGeometry.Scheme.IdealSheafData.comapIsodefMathlib.AlgebraicGeometry.IdealSheaf.Functorial, function or constant

Wording

the preimage isomorphism of I and f (from the name)

English

Let $I$ be an ideal sheaf data of $Y$. Let $f$ be a homomorphism of $X$ and $Y$. Then the preimage isomorphism of $I$ and $f$ is an isomorphism of the subscheme of the preimage of $I$ and $f$ and the pullback of $f$ and the subscheme inclusion of $I$ defined as the inverse of $\operatorname{asIso}$ applied to the image of the first projection of the pullback of $f$ and the subscheme inclusion of $I$.

AlgebraicGeometry.Scheme.IdealSheafData.mapdefMathlib.AlgebraicGeometry.IdealSheaf.Functorial, function or constant

Wording

the map of I and f (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $I$ and $f$ is an ideal sheaf data of $Y$ defined as the kernel of the composition of the subscheme inclusion of $I$ and $f$.

AlgebraicGeometry.Scheme.IdealSheafData.subschemeMapdefMathlib.AlgebraicGeometry.IdealSheaf.Functorial, function or constant

Wording

the subscheme map of J and f (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Let $J$ be an ideal sheaf data of $Y$. Let $f$ be a homomorphism of $X$ and $Y$ such that $J$ is less than or equal to the map of $I$ and $f$. Then the subscheme map of $J$ and $f$ is a homomorphism of the subscheme of $I$ and the subscheme of $J$.

Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

AlgebraicGeometry.Scheme.irreducibleComponentdefMathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent, function or constant

Wording

the irreducible component of X and Z (from the name)

English

Let $X$ be a scheme. Let $Z$ be an element of the power set of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ such that $Z$ is an element of the irreducible component of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the irreducible component of $X$ and $Z$ is a scheme defined as the subscheme of the irreducible component ideal of $X$ and $Z$.

AlgebraicGeometry.Scheme.irreducibleComponentIdealdefMathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent, function or constant

Wording

the irreducible component ideal of X and Z (from the name)

English

Let $X$ be a scheme. Let $Z$ be an element of the power set of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ such that $Z$ is an element of the irreducible component of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the irreducible component ideal of $X$ and $Z$ is an ideal sheaf data of $X$.

AlgebraicGeometry.Scheme.irreducibleComponentOpendefMathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent, function or constant

Wording

the irreducible component open of X and Z (from the name)

English

AlgebraicGeometry.Scheme.irreducibleComponentιdefMathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent, function or constant

Wording

the irreducible component inclusion of X and Z (from the name)

English

Let $X$ be a scheme. Let $Z$ be an element of the power set of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ such that $Z$ is an element of the irreducible component of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the irreducible component inclusion of $X$ and $Z$ is a homomorphism of the irreducible component of $X$ and $Z$ and $X$ defined as the subscheme inclusion of the irreducible component ideal of $X$ and $Z$.

Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

AlgebraicGeometry.Scheme.Hom.imagedefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the image of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the image of $f$ is a scheme defined as the subscheme of the kernel of $f$.

AlgebraicGeometry.Scheme.Hom.imageιdefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the image inclusion of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the image inclusion of $f$ is a homomorphism of the image of $f$ and $Y$ defined as the subscheme inclusion of the kernel of $f$.

AlgebraicGeometry.Scheme.Hom.toImagedefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the image of f (from the name)

English

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

AlgebraicGeometry.Scheme.IdealSheafData.glueDatadefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the glue data of I (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Then the glue data of $I$ is a glue data.

AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjdefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the glue data object of I and U (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Let $U$ be an element of the affine open of $X$. Then the glue data object of $I$ and $U$ is a scheme defined as the spectrum of $\operatorname{of}$ applied to the set of quotients of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$ and the component of $I$ and $U$.

AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjCarrierIsodefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the glue data object carrier isomorphism of I and U (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Let $U$ be an element of the affine open of $X$. Then the glue data object carrier isomorphism of $I$ and $U$ is an isomorphism of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the glue data object of $I$ and $U$ and $\operatorname{of}$ applied to the set of elements of $\operatorname{inter}$ applied to the zero locus of $X$ and the component of $I$ and $U$ and $U$.

AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHomdefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the glue data object homomorphism of h and U (from the name)

English

Assume that $I \leq J$. Let $U$ be an element of the affine open of $X$. Then the glue data object homomorphism of $h$ and $U$ is a homomorphism of the glue data object of $J$ and $U$ and the glue data object of $I$ and $U$ defined as the induced map of the commutative ring category of the factor of $h$ applied to $U$.

AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMapdefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the glue data object map of I and h (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Assume that $U \leq V$. Then the glue data object map of $I$ and $h$ is a homomorphism of the glue data object of $I$ and $U$ and the glue data object of $I$ and $V$ defined as the induced map of the commutative ring category of the quotient map of the component of $I$ and $U$ and the underlying ring hom of the map of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the opposite in the homomorphism of $h$.

AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjPullbackdefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the glue data object pullback of U and V (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Let $U$ and $V$ be elements of the affine open of $X$. Then the glue data object pullback of $U$ and $V$ is a scheme.

AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjιdefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the glue data object inclusion of I and U (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Let $U$ be an element of the affine open of $X$. Then the glue data object inclusion of $I$ and $U$ is a homomorphism of the glue data object of $I$ and $U$ and the scheme of $U$.

AlgebraicGeometry.Scheme.IdealSheafData.glueDataTdefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the glue data of U and V (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Let $U$ and $V$ be elements of the affine open of $X$. Then the glue data of $U$ and $V$ is a homomorphism of the glue data object pullback of $U$ and $V$ and the glue data object pullback of $V$ and $U$.

AlgebraicGeometry.Scheme.IdealSheafData.gluedHomeodefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the glued homeomorphism of I (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Then the glued homeomorphism of $I$ is a homeomorphism of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the glued scheme of the glue data of $I$ and $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{support} (I)}{x})}$.

AlgebraicGeometry.Scheme.IdealSheafData.gluedTodefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

no wording

English

Let $I$ be an ideal sheaf data of $X$. Then $\operatorname{gluedTo}$ applied to $I$ is a homomorphism of the glued scheme of the glue data of $I$ and $X$.

AlgebraicGeometry.Scheme.IdealSheafData.inclusiondefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the inclusion of h (from the name)

English

Assume that $I \leq J$. Then the inclusion of $h$ is a homomorphism of the subscheme of $J$ and the subscheme of $I$.

AlgebraicGeometry.Scheme.IdealSheafData.subschemedefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the subscheme of I (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Then the subscheme of $I$ is a scheme.

AlgebraicGeometry.Scheme.IdealSheafData.subschemeCoverdefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the subscheme cover of I (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Then the subscheme cover of $I$ is an affine open cover of the subscheme of $I$.

AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctordefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the subscheme functor of Y (from the name)

English

Let $Y$ be a scheme. Then the subscheme functor of $Y$ is a functor of the set of opposites of the set of ideal sheaf data of $Y$ and $\operatorname{Over}$ applied to $Y$.

AlgebraicGeometry.Scheme.IdealSheafData.subschemeIsodefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the subscheme isomorphism of I (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Then the subscheme isomorphism of $I$ is an isomorphism of the subscheme of $I$ and the glued scheme of the glue data of $I$.

AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIsodefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the subscheme object isomorphism of I and U (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Let $U$ be an element of the affine open of $X$. Then the subscheme object isomorphism of $I$ and $U$ is an isomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the subscheme of $I$ and $\operatorname{op}$ applied to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the subscheme inclusion of $I$ and $U$ and $\operatorname{of}$ applied to the set of quotients of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$ and the component of $I$ and $U$.

AlgebraicGeometry.Scheme.IdealSheafData.subschemeιdefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the subscheme inclusion of I (from the name)

English

Let $I$ be an ideal sheaf data of $X$. Then the subscheme inclusion of $I$ is a homomorphism of the subscheme of $I$ and $X$.

AlgebraicGeometry.Scheme.kerAdjunctiondefMathlib.AlgebraicGeometry.IdealSheaf.Subscheme, function or constant

Wording

the kernel adjunction of Y (from the name)

English

Let $Y$ be a scheme. Then the kernel adjunction of $Y$ is an adjunction of the right opposite of the subscheme functor of $Y$ and the kernel functor of $Y$.

Mathlib.AlgebraicGeometry.Limits

AlgebraicGeometry.Scheme.coprodPresheafObjIsodefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

the coproduct presheaf object isomorphism of U (from the name)

English

Let $U$ be an open of the coproduct of $X$ and $Y$. Then the coproduct presheaf object isomorphism of $U$ is an isomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the coproduct of $X$ and $Y$ and $\operatorname{op}$ applied to $U$ and the product of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the left injection and $U$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the right injection and $U$.

AlgebraicGeometry.Scheme.emptyTodefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

the map from the empty scheme of X (from the docstring)

English

Let $X$ be a scheme. Then the map from the empty scheme of $X$ is a homomorphism of $\operatorname{emptyCollection}$ and $X$.

AlgebraicGeometry.coprodIsoSigmadefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

the coproduct isomorphism sigma of X and Y (from the name)

English

Let $X$ and $Y$ be schemes. Then the coproduct isomorphism sigma of $X$ and $Y$ is an isomorphism of the coproduct of $X$ and $Y$ and the sigma object of the function that maps $i$ to $\operatorname{casesOn}$ applied to $\operatorname{down}$ applied to $i$, $X$ and $Y$.

AlgebraicGeometry.coprodMkdefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

the underlying topological space of the coproduct of X and Y (from the docstring)

English

Let $X$ and $Y$ be schemes. Then the underlying topological space of the coproduct of $X$ and $Y$ is a homeomorphism of $\mathrm{Sum}$ applied to the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the coproduct of $X$ and $Y$ defined as the homeomorphism of the composition of the inverse of the isomorphism colimit cocone of $\operatorname{mk}$ applied to the binary cofan of the action of $\operatorname{forgetToTop}$ and $X$ and the action of $\operatorname{forgetToTop}$ and $Y$ and $\operatorname{binaryCofanIsColimit}$ applied to the action of $\operatorname{forgetToTop}$ and $X$ and the action of $\operatorname{forgetToTop}$ and $Y$ and the isomorphism of $X$ and $Y$.

AlgebraicGeometry.coprodOpenCoverdefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

the open cover of the coproduct of two schemes of X and Y (from the docstring)

English

Let $X$ and $Y$ be schemes. Then the open cover of the coproduct of two schemes of $X$ and $Y$ is an open cover of the coproduct of $X$ and $Y$.

AlgebraicGeometry.coprodSpecdefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

the coproduct spectrum of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the coproduct spectrum of $R$ and $S$ is a homomorphism of the coproduct of the spectrum of $\operatorname{of}$ applied to $R$ and the spectrum of $\operatorname{of}$ applied to $S$ and the spectrum of $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to $R$ and $S$ defined as $\operatorname{desc}$ applied to the induced map of the commutative ring category of the first component of $R$ and $S$ and the induced map of the commutative ring category of the second component of $R$ and $S$.

AlgebraicGeometry.emptyIsInitialdefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

the empty scheme (from the docstring)

English

The empty scheme is an element of $\operatorname{IsInitial}$ applied to $\operatorname{emptyCollection}$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{emptyCollection}$.

AlgebraicGeometry.isInitialOfIsEmptydefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

no wording

English

$\operatorname{isInitialOfIsEmpty}$ is an element of $\operatorname{IsInitial}$ applied to $X$ defined as $\operatorname{ofIso}$ applied to the empty scheme and $\operatorname{asIso}$ applied to $\operatorname{to}$ applied to the empty scheme and $X$.

AlgebraicGeometry.sigmaMkdefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

the sigma of f (from the name)

English

Let $f$ be a function from elements of $x$ to schemes. Then the sigma of $f$ is a homeomorphism of $\Sigma$ applied to the function that maps $i$ to the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $f$ applied to $i$ and the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the sigma object of $f$ defined as the homeomorphism of the composition of the inverse of the isomorphism colimit cocone of $\operatorname{mk}$ applied to the explicit cofan of the function that maps $j$ to the action of $\operatorname{forgetToTop}$ and $f$ applied to $j$ and $\operatorname{sigmaCofanIsColimit}$ applied to the function that maps $j_{1}$ to the action of $\operatorname{forgetToTop}$ and $f$ applied to $j_{1}$ and the inverse of the isomorphism of $\operatorname{forgetToTop}$ and $f$.

AlgebraicGeometry.sigmaOpenCoverdefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

the cover of g (from the docstring)

English

Let $g$ be a function from elements of $x$ to schemes. Then the cover of $g$ is an open cover of the sigma object of $g$.

AlgebraicGeometry.sigmaSpecdefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

the sigma spectrum of R (from the name)

English

Let $R$ be a function from elements of $x$ to categories of commutative rings. Then the sigma spectrum of $R$ is a homomorphism of the sigma object of the function that maps $i$ to the spectrum of $R$ applied to $i$ and the spectrum of $\operatorname{of}$ applied to the set of functions from elements $i_{1}$ of $x$ to carriers of $R$ applied to $i_{1}$ defined as $\operatorname{desc}$ applied to the function that maps $i$ to the induced map of the commutative ring category of the evaluation ring homomorphism of the function that maps $i_{1}$ to the set of carriers of $R$ applied to $i_{1}$ and $i$.

AlgebraicGeometry.specPUnitIsInitialdefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

no wording

English

$\operatorname{specPUnitIsInitial}$ is an element of $\operatorname{IsInitial}$ applied to the spectrum of $\operatorname{of}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{ofIso}$ applied to the empty scheme and $\operatorname{asIso}$ applied to $\operatorname{to}$ applied to the empty scheme and the spectrum of $\operatorname{of}$ applied to $\mathrm{PUnit}$.

AlgebraicGeometry.specULiftZIsTerminaldefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

no wording

English

$\operatorname{specULiftZIsTerminal}$ is an element of $\operatorname{IsTerminal}$ applied to the spectrum of $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Integer$ defined as $\operatorname{isTerminalObj}$ applied to the spectrum, $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Integer$ and $\operatorname{terminalOpOfInitial}$ applied to $\operatorname{isInitial}$.

AlgebraicGeometry.specZIsTerminaldefMathlib.AlgebraicGeometry.Limits, function or constant

Wording

no wording

English

$\operatorname{specZIsTerminal}$ is an element of $\operatorname{IsTerminal}$ applied to the spectrum of $\operatorname{of}$ applied to $\Integer$ defined as $\operatorname{isTerminalObj}$ applied to the spectrum, $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\Integer$ and $\operatorname{terminalOpOfInitial}$ applied to $\operatorname{zIsInitial}$.

Mathlib.AlgebraicGeometry.Modules.Presheaf

AlgebraicGeometry.Scheme.Hom.toRingCatSheafHomdefMathlib.AlgebraicGeometry.Modules.Presheaf, function or constant

Wording

the ring category sheaf homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the ring category sheaf homomorphism of $f$ is a homomorphism of the underlying sheaf of rings of $Y$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$, the set of categories of rings, the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the underlying sheaf of rings of $X$ defined as $\operatorname{mk}$ applied to the right whisker of $\operatorname{c}$ applied to $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

AlgebraicGeometry.Scheme.PresheafOfModulesdefMathlib.AlgebraicGeometry.Modules.Presheaf, type

Wording

presheaf of module of X (from the name)

English

Let $X$ be a scheme. Then a presheaf of module of $X$ is an element of the function that maps $X$ to the set of presheafs of module of the object of the underlying sheaf of rings of $X$.

AlgebraicGeometry.Scheme.ringCatSheafdefMathlib.AlgebraicGeometry.Modules.Presheaf, function or constant

Wording

the underlying sheaf of rings of X (from the docstring)

English

Let $X$ be a scheme. Then the underlying sheaf of rings of $X$ is a sheaf of the set of categories of rings and the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ defined as the action of $\operatorname{sheafCompose}$ applied to the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings and the structure sheaf of $X$.

Mathlib.AlgebraicGeometry.Modules.Sheaf

AlgebraicGeometry.Scheme.ModulesdefMathlib.AlgebraicGeometry.Modules.Sheaf, type

Wording

module of X (from the name)

English

Let $X$ be a scheme. Then a module of $X$ is an element of the function that maps $X$ to the set of sheaves of module of the underlying sheaf of rings of $X$.

AlgebraicGeometry.Scheme.Modules.HomdefMathlib.AlgebraicGeometry.Modules.Sheaf, type

Wording

homomorphism of M and N (from the name)

English

Let $M$ and $N$ be modules of $X$. Then a homomorphism of $M$ and $N$ is an element of the function that maps $M$ and $N$ to the set of homomorphisms of $M$ and $N$.

AlgebraicGeometry.Scheme.Modules.Hom.appdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the homomorphism of x and U (from the name)

English

Let $x$ be a homomorphism of $M$ and $N$. Let $U$ be an open of $X$. Then the homomorphism of $x$ and $U$ is a homomorphism of the action of the underlying abelian presheaf of $M$ and $\operatorname{op}$ applied to $U$ and the action of the underlying abelian presheaf of $N$ and $\operatorname{op}$ applied to $U$ defined as the map of the forgetful functor of the set of module categories of the set of carriers of the action of the object of the underlying sheaf of rings of $X$ and $\operatorname{op}$ applied to $U$ and the set of abelian groups and the homomorphism of the value of $x$ and $\operatorname{op}$ applied to $U$.

AlgebraicGeometry.Scheme.Modules.Hom.mapPresheafdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the map presheaf of x (from the name)

English

Let $x$ be a homomorphism of $M$ and $N$. Then the map presheaf of $x$ is a homomorphism of the underlying abelian presheaf of $M$ and the underlying abelian presheaf of $N$ defined as the map of the presheaf of $X$ and $x$.

AlgebraicGeometry.Scheme.Modules.fullyFaithfulToPresheafOfModulesdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

$\operatorname{fullyFaithfulToPresheafOfModules}$ is an element of $\operatorname{FullyFaithful}$ applied to the presheaf of $X$ defined as $\operatorname{fullyFaithfulForget}$ applied to the underlying sheaf of rings of $X$.

AlgebraicGeometry.Scheme.Modules.overEquivdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $U$ be an open of $X$. Then $\operatorname{overEquiv}$ applied to $U$ is an equivalence of the set of sheaves of module of $\operatorname{over}$ applied to the underlying sheaf of rings of $X$ and $U$ and the set of modules of the scheme of $U$ defined as the sheaf of $U$ and the underlying sheaf of rings of $X$.

AlgebraicGeometry.Scheme.Modules.overFunctorEquivdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $U$ be an open of $X$. Then $\operatorname{overFunctorEquiv}$ applied to $U$ is an isomorphism of the composition of $\operatorname{overFunctor}$ applied to the underlying sheaf of rings of $X$ and $U$ and the functor of $\operatorname{overEquiv}$ applied to $U$ and $\operatorname{restrictFunctor}$ applied to the inclusion of $U$.

AlgebraicGeometry.Scheme.Modules.overMapCompOverEquivdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $V$ and $U$. Then $\operatorname{overMapCompOverEquiv}$ applied to $f$ is an isomorphism of the composition of $\operatorname{overMap}$ applied to the underlying sheaf of rings of $X$ and $f$ and the functor of $\operatorname{overEquiv}$ applied to $V$ and the composition of the functor of $\operatorname{overEquiv}$ applied to $U$ and $\operatorname{restrictFunctor}$ applied to the homomorphism of $X$ and $\operatorname{leOfHom}$ applied to $f$.

AlgebraicGeometry.Scheme.Modules.presheafdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the underlying abelian presheaf of M (from the docstring)

English

Let $M$ be a module of $X$. Then the underlying abelian presheaf of $M$ is a presheaf of the set of abelian groups and the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ defined as the presheaf of the value of $M$.

AlgebraicGeometry.Scheme.Modules.pseudofunctordefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the pseudofunctor (from the name)

English

The pseudofunctor is a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of the set of schemes and the set of adjoints of the set of categories.

AlgebraicGeometry.Scheme.Modules.pullbackdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the pullback of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback of $f$ is a functor of the set of modules of $Y$ and the set of modules of $X$ defined as the pullback functor of the ring category sheaf homomorphism of $f$.

AlgebraicGeometry.Scheme.Modules.pullbackCompdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

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

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback composition of $f$ and $g$ is an isomorphism of the composition of the pullback of $g$ and the pullback of $f$ and the pullback of the composition of $f$ and $g$ defined as the pullback composition of the ring category sheaf homomorphism of $g$ and the ring category sheaf homomorphism of $f$.

AlgebraicGeometry.Scheme.Modules.pullbackCongrdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the pullback congruence of hf (from the name)

English

Assume that $\EqtMACRoH {f}{g}$. Then the pullback congruence of $\mathrm{hf}$ is an isomorphism of the pullback of $f$ and the pullback of $g$.

AlgebraicGeometry.Scheme.Modules.pullbackIddefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the pullback identity of X (from the name)

English

Let $X$ be a scheme. Then the pullback identity of $X$ is an isomorphism of the pullback of the identity morphism of $X$ and the identity of the set of modules of $X$ defined as the pullback identity of the underlying sheaf of rings of $X$.

AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunctiondefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the pullback pushforward adjunction of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback pushforward adjunction of $f$ is an adjunction of the pullback of $f$ and $\operatorname{pushforward}$ applied to $f$ defined as the pullback pushforward adjunction of the ring category sheaf homomorphism of $f$.

AlgebraicGeometry.Scheme.Modules.pushforwarddefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{pushforward}$ applied to $f$ is a functor of the set of modules of $X$ and the set of modules of $Y$ defined as $\operatorname{pushforward}$ applied to the ring category sheaf homomorphism of $f$.

AlgebraicGeometry.Scheme.Modules.pushforwardCompdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

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

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pushforward composition of $f$ and $g$ is an isomorphism of the composition of $\operatorname{pushforward}$ applied to $f$ and $\operatorname{pushforward}$ applied to $g$ and $\operatorname{pushforward}$ applied to the composition of $f$ and $g$ defined as the pushforward composition of the ring category sheaf homomorphism of $g$ and the ring category sheaf homomorphism of $f$.

AlgebraicGeometry.Scheme.Modules.pushforwardCongrdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the pushforward congruence of hf (from the name)

English

Assume that $\EqtMACRoH {f}{g}$. Then the pushforward congruence of $\mathrm{hf}$ is an isomorphism of $\operatorname{pushforward}$ applied to $f$ and $\operatorname{pushforward}$ applied to $g$.

AlgebraicGeometry.Scheme.Modules.pushforwardIddefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the pushforward identity of X (from the name)

English

Let $X$ be a scheme. Then the pushforward identity of $X$ is an isomorphism of $\operatorname{pushforward}$ applied to the identity morphism of $X$ and the identity of the set of modules of $X$ defined as the pushforward identity of the underlying sheaf of rings of $X$.

AlgebraicGeometry.Scheme.Modules.restrictdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the restriction of M and f (from the docstring)

English

Let $M$ be a module of $Y$. Let $f$ be a homomorphism of $X$ and $Y$. Then the restriction of $M$ and $f$ is a module of $X$ defined as the action of $\operatorname{restrictFunctor}$ applied to $f$ and $M$.

AlgebraicGeometry.Scheme.Modules.restrictAdjunctiondefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{restrictAdjunction}$ applied to $f$ is an adjunction of $\operatorname{restrictFunctor}$ applied to $f$ and $\operatorname{pushforward}$ applied to $f$.

AlgebraicGeometry.Scheme.Modules.restrictAppIsodefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $M$ be a module of $Y$. Let $U$ be an open of $X$. Then $\operatorname{restrictAppIso}$ applied to $f$, $M$ and $U$ is an isomorphism of the action of the underlying abelian presheaf of the restriction of $M$ and $f$ and $\operatorname{op}$ applied to $U$ and the action of the underlying abelian presheaf of $M$ and $\operatorname{op}$ applied to the action of the functor of $f$ and $U$ defined as the identity of the action of the underlying abelian presheaf of the restriction of $M$ and $f$ and $\operatorname{op}$ applied to $U$.

AlgebraicGeometry.Scheme.Modules.restrictFunctordefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{restrictFunctor}$ applied to $f$ is a functor of the set of modules of $Y$ and the set of modules of $X$.

AlgebraicGeometry.Scheme.Modules.restrictFunctorAdjCounitIsodefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the restriction of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the restriction of $f$ is an isomorphism of the composition of $\operatorname{pushforward}$ applied to $f$ and $\operatorname{restrictFunctor}$ applied to $f$ and the identity of the set of modules of $X$.

AlgebraicGeometry.Scheme.Modules.restrictFunctorCompdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{restrictFunctorComp}$ applied to $f$ and $g$ is an isomorphism of $\operatorname{restrictFunctor}$ applied to the composition of $f$ and $g$ and the composition of $\operatorname{restrictFunctor}$ applied to $g$ and $\operatorname{restrictFunctor}$ applied to $f$.

AlgebraicGeometry.Scheme.Modules.restrictFunctorCongrdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Assume that $\EqtMACRoH {f}{g}$. Then $\operatorname{restrictFunctorCongr}$ applied to $\mathrm{hf}$ is an isomorphism of $\operatorname{restrictFunctor}$ applied to $f$ and $\operatorname{restrictFunctor}$ applied to $g$.

AlgebraicGeometry.Scheme.Modules.restrictFunctorIddefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

$\operatorname{restrictFunctorId}$ is an isomorphism of $\operatorname{restrictFunctor}$ applied to the identity morphism of $X$ and the identity of the set of modules of $X$.

AlgebraicGeometry.Scheme.Modules.restrictFunctorIsoPullbackdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{restrictFunctorIsoPullback}$ applied to $f$ is an isomorphism of $\operatorname{restrictFunctor}$ applied to $f$ and the pullback of $f$ defined as $\operatorname{leftAdjointUniq}$ applied to $\operatorname{restrictAdjunction}$ applied to $f$ and the pullback pushforward adjunction of $f$.

AlgebraicGeometry.Scheme.Modules.restrictStalkNatIsodefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then $\operatorname{restrictStalkNatIso}$ applied to $f$ and $x$ is an isomorphism of the composition of $\operatorname{restrictFunctor}$ applied to $f$ and the composition of the presheaf of $X$ and the stalk functor of the set of abelian groups and $x$ and the composition of the presheaf of $Y$ and the stalk functor of the set of abelian groups and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $x$ defined as the left isomorphism whisker of the composition of the presheaf of $Y$ and the action of the left whiskering of the set of opposites of the set of opens of $Y$ and the set of abelian groups and the opposite of the inclusion of $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $x$ and the colimit isomorphism of the opposite of the functor neighbourhood filter of $\operatorname{isOpenEmbedding}$ applied to $f$ and $x$.

AlgebraicGeometry.Scheme.Modules.restrictUnitIsodefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{restrictUnitIso}$ applied to $f$ is an isomorphism of the restriction of the unit of the underlying sheaf of rings of $Y$ and $f$ and the unit of the underlying sheaf of rings of $X$.

AlgebraicGeometry.Scheme.Modules.sheafComposePushforwardCompdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

no wording

English

Let $x$ be a homomorphism of $R$ and $S$. Then $\operatorname{sheafComposePushforwardComp}$ applied to $x$ is an isomorphism of the composition of $\operatorname{sheafCompose}$ applied to the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $S$ and $\operatorname{restrictScalars}$ applied to the underlying ring hom of the application top of the induced map of $x$ and the composition of the pushforward functor of the set of module categories of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and $\operatorname{op}$ applied to the top and the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the induced map of $x$ and $\operatorname{sheafCompose}$ applied to the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and $\operatorname{restrictScalars}$ applied to the underlying ring hom of the inverse of the spectrum isomorphism of $R$ and the composition of $\operatorname{sheafCompose}$ applied to the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $S$ and $\operatorname{restrictScalars}$ applied to the underlying ring hom of the inverse of the spectrum isomorphism of $S$ and the composition of the pushforward functor of the set of module categories of the set of carriers of $S$ and the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the induced map of $x$ and $\operatorname{sheafCompose}$ applied to the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and $\operatorname{restrictScalars}$ applied to the underlying ring hom of $x$.

AlgebraicGeometry.Scheme.Modules.smuldefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the scalar multiple (from the name)

English

The scalar multiple is a ring homomorphism of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$ and the set of ends of the action of the underlying abelian presheaf of $M$ and $\operatorname{op}$ applied to $U$ defined as the scalar multiplication of the object of the value of $M$ and $\operatorname{op}$ applied to $U$.

AlgebraicGeometry.Scheme.Modules.toPresheafdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the presheaf of X (from the name)

English

Let $X$ be a scheme. Then the presheaf of $X$ is a functor of the set of modules of $X$ and the set of presheafs of the set of abelian groups and the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ defined as the composition of the presheaf of $X$ and the presheaf of the object of the underlying sheaf of rings of $X$.

AlgebraicGeometry.Scheme.Modules.toPresheafOfModulesdefMathlib.AlgebraicGeometry.Modules.Sheaf, function or constant

Wording

the presheaf of X (from the name)

English

Let $X$ be a scheme. Then the presheaf of $X$ is a functor of the set of modules of $X$ and the set of presheafs of module of $X$ defined as the forgetful functor of the underlying sheaf of rings of $X$.

Mathlib.AlgebraicGeometry.Modules.Tilde

AlgebraicGeometry.IsLocalizingdefMathlib.AlgebraicGeometry.Modules.Tilde, predicate

Wording

M is a localizing (from the name)

English

Let $M$ be a sheaf of the set of module categories of the set of carriers of $R$ and the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$. Then $M$ is a localizing, if for all carriers $f$ of $R$, $\mathrm{IsLocalizedModule}$ holds for the power of $f$ and the homomorphism of the map of the object of $M$ and the opposite in $\operatorname{leTop}$ applied to $\operatorname{basicOpen}$ applied to $f$.

AlgebraicGeometry.Scheme.Modules.fromTildeΓdefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

no wording

English

Let $M$ be a module of the spectrum of $R$. Then $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Modules\_\_fromTilde\_u393\_}$ applied to $M$ is a homomorphism of the tilde of the action of the underlying presheaf of the action of the module spectrum to sheaf and $M$ and $\operatorname{op}$ applied to the top and $M$.

AlgebraicGeometry.Scheme.Modules.fromTildeΓNatTransdefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

no wording

English

$\mathrm{AlgebraicGeometry\_\_Scheme\_\_Modules\_\_fromTilde\_u393\_NatTrans}$ is a homomorphism of the composition of the module spectrum functor and the functor of $R$ and the identity of the set of modules of the spectrum of $R$.

AlgebraicGeometry.Scheme.Modules.presentationRestrictdefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $Y$ and $X$. Let $\mathrm{pres}$ be a presentation of $M$. Then $\operatorname{presentationRestrict}$ applied to $f$ and $\mathrm{pres}$ is a presentation of the restriction of $M$ and $f$ defined as the map of $\operatorname{restrictFunctor}$ applied to $f$ and the inverse of $\operatorname{restrictUnitIso}$ applied to $f$.

AlgebraicGeometry.SpecModulesToSheafFullyFaithfuldefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

no wording

English

$\operatorname{SpecModulesToSheafFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the module spectrum to sheaf.

AlgebraicGeometry.moduleSpecΓFunctordefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the module spectrum functor (from the name)

English

The module spectrum functor is a functor of the set of modules of the spectrum of $R$ and the set of module categories of the set of carriers of $R$ defined as the composition of the module spectrum to sheaf and the composition of $\operatorname{forget}$ applied to the set of module categories of the set of carriers of $R$ and the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and the action of the evaluation of the set of opposites of the set of opens of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and the set of module categories of the set of carriers of $R$ and $\operatorname{op}$ applied to the top.

AlgebraicGeometry.modulesSpecToSheafdefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the module spectrum to sheaf (from the name)

English

The module spectrum to sheaf is a functor of the set of modules of the spectrum of $R$ and the set of sheaves of the set of module categories of the set of carriers of $R$ and the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ defined as the composition of $\operatorname{forgetToSheafModuleCat}$ applied to the underlying sheaf of rings of the spectrum of $R$, $\operatorname{op}$ applied to the top and the initial opposite of $\operatorname{isTerminalTop}$ and $\operatorname{sheafCompose}$ applied to the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and $\operatorname{restrictScalars}$ applied to the underlying ring hom of the inverse of the spectrum isomorphism of $R$.

AlgebraicGeometry.presentationTildedefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the presentation tilde of s and t (from the name)

English

Let $M$ be a module category of the set of carriers of $R$. Let $s$ be an element of the power set of the set of carriers of $M$ such that the span of the set of carriers of $R$ and $s$ is equal to the top. Let $t$ be an element of the power set of the set of finitely supported functions from the set of elements of $s$ to the set of carriers of $R$ such that the span of the set of carriers of $R$ and $t$ is equal to the kernel of the linear combination of the set of carriers of $R$ and the function that maps $x$ to $\MembershipmemMACRoT {s}{x}$. Then the presentation tilde of $s$ and $t$ is a presentation of the tilde of $M$.

AlgebraicGeometry.pushforwardCompModulesSpecToSheafIsodefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the pushforward composition module spectrum to sheaf isomorphism of x (from the name)

English

Let $x$ be a homomorphism of $R$ and $S$. Then the pushforward composition module spectrum to sheaf isomorphism of $x$ is an isomorphism of the composition of $\operatorname{pushforward}$ applied to the induced map of $x$ and the module spectrum to sheaf and the composition of the module spectrum to sheaf and the composition of the pushforward functor of the set of module categories of the set of carriers of $S$ and the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the induced map of $x$ and $\operatorname{sheafCompose}$ applied to the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and $\operatorname{restrictScalars}$ applied to the underlying ring hom of $x$.

AlgebraicGeometry.tildedefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the tilde of M (from the name)

English

Let $M$ be a module category of the set of carriers of $R$. Then the tilde of $M$ is a module of the spectrum of $R$.

AlgebraicGeometry.tilde.adjunctiondefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the adjunction (from the name)

English

The adjunction is an adjunction of the functor of $R$ and the module spectrum functor.

AlgebraicGeometry.tilde.fullyFaithfulFunctordefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the tilde functor (from the docstring)

English

The tilde functor is an element of $\operatorname{FullyFaithful}$ applied to the functor of $R$ defined as $\operatorname{fullyFaithfulLOfIsIsoUnit}$ applied to the adjunction.

AlgebraicGeometry.tilde.functordefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the functor of R (from the name)

English

Let $R$ be a category of commutative rings. Then the functor of $R$ is a functor of the set of module categories of the set of carriers of $R$ and the set of modules of the spectrum of $R$.

AlgebraicGeometry.tilde.isoTopdefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the isomorphism between the global sections of M (from the docstring)

English

Let $M$ be a module category of the set of carriers of $R$. Then the isomorphism between the global sections of $M$ is an isomorphism of $M$ and the action of the underlying presheaf of the action of the module spectrum to sheaf and the tilde of $M$ and $\operatorname{op}$ applied to the top defined as $\operatorname{asIso}$ applied to the open of $M$ and the top.

AlgebraicGeometry.tilde.mapdefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the map of f (from the name)

English

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

AlgebraicGeometry.tilde.modulesSpecToSheafIsodefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the module spectrum to sheaf isomorphism of M (from the name)

English

Let $M$ be a module category of the set of carriers of $R$. Then the module spectrum to sheaf isomorphism of $M$ is an isomorphism of the object of the action of the module spectrum to sheaf and the tilde of $M$ and the structure presheaf in module category of the set of carriers of $R$ and the set of carriers of $M$.

AlgebraicGeometry.tilde.toOpendefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the open of M and U (from the name)

English

Let $M$ be a module category of the set of carriers of $R$. Let $U$ be an open of the spectrum of $R$. Then the open of $M$ and $U$ is a homomorphism of $M$ and the action of the underlying presheaf of the action of the module spectrum to sheaf and the tilde of $M$ and $\operatorname{op}$ applied to $U$ defined as the composition of the module category of the open of $U$ and the inverse of the application of the module spectrum to sheaf isomorphism of $M$ and $\operatorname{op}$ applied to $U$.

AlgebraicGeometry.tilde.toStalkdefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the stalk of M and x (from the name)

English

Let $M$ be a module category of the set of carriers of $R$. Let $x$ be a carrier of the top of the set of carriers of $R$. Then the stalk of $M$ and $x$ is a homomorphism of $\operatorname{of}$ applied to the set of carriers of $R$ and the set of carriers of $M$ and $\operatorname{of}$ applied to the set of carriers of $R$ and the set of carriers of the stalk of the underlying abelian presheaf of the tilde of $M$ and $x$ defined as the module category of the stalk of $x$.

AlgebraicGeometry.tilde.toTildeΓNatIsodefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the tilde natural isomorphism (from the name)

English

The tilde natural isomorphism is an isomorphism of the identity of the set of module categories of the set of carriers of $R$ and the composition of the functor of $R$ and the module spectrum functor.

AlgebraicGeometry.tildeEquivdefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the tilde equivalence (from the name)

English

The tilde equivalence is an equivalence of the set of module categories of the set of carriers of $R$ and the set of full subcategories of $\operatorname{isQuasicoherent}$ applied to the underlying sheaf of rings of the spectrum of $R$.

AlgebraicGeometry.tildeFinsuppdefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the tilde finitely supported function of x (from the name)

English

Let $x$ be a set. Then the tilde finitely supported function of $x$ is an isomorphism of the tilde of $\operatorname{of}$ applied to the set of carriers of $R$ and the set of finitely supported functions from $x$ to the set of carriers of $R$ and the free of $x$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{symm}$ applied to the precomposition homomorphism equivalence of the inverse of the natural isomorphism of the function that maps $x_{3}$ to the tilde self and the map cocone of the functor of $R$ and the finitely supported function cocone of the set of carriers of $R$ and $x$ and $\operatorname{isColimitOfPreserves}$ applied to the functor of $R$ and $\operatorname{finsuppCoconeIsColimit}$ applied to the set of carriers of $R$, the set of carriers of $R$ and $x$ and $\operatorname{coproductIsCoproduct}$ applied to the function that maps $x_{4}$ to the unit of the underlying sheaf of rings of the spectrum of $R$.

AlgebraicGeometry.tildeSelfdefMathlib.AlgebraicGeometry.Modules.Tilde, function or constant

Wording

the tilde self (from the name)

English

The tilde self is an isomorphism of the tilde of $\operatorname{of}$ applied to the set of carriers of $R$ and the set of carriers of $R$ and the unit of the underlying sheaf of rings of the spectrum of $R$ defined as the identity of the tilde of $\operatorname{of}$ applied to the set of carriers of $R$ and the set of carriers of $R$.

Mathlib.AlgebraicGeometry.Morphisms.Affine

AlgebraicGeometry.IsAffineHomclassMathlib.AlgebraicGeometry.Morphisms.Affine, predicate

Wording

f is a affine homomorphism (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is an affine homomorphism.

Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

AlgebraicGeometry.affineAnddefMathlib.AlgebraicGeometry.Morphisms.AffineAnd, function or constant

Wording

no wording

English

Let $Q$ be a function from sets $R$ and sets $S$ and elements $x$ of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $S$ is a commutative ring and ring homomorphisms of $R$ and $S$ to propositions. Then there is an affine target morphism property. Proof. Let $Q$ be arbitrary. Let $X$ be arbitrary. Let $x$ be arbitrary. Let $f$ be arbitrary. Let $h$ be arbitrary. By S. By AlgebraicGeometry__IsAffine. By x. By AlgebraicGeometry__Scheme__toLocallyRingedSpace. By AlgebraicGeometry__LocallyRingedSpace__toSheafedSpace. By AlgebraicGeometry__SheafedSpace__toPresheafedSpace. By AlgebraicGeometry__PresheafedSpace__presheaf. By Top__top. By Opposite__op. By CategoryTheory__Functor__obj. By CommRingCat__carrier. By S. By AlgebraicGeometry__Scheme__toLocallyRingedSpace. By AlgebraicGeometry__LocallyRingedSpace__toSheafedSpace. By AlgebraicGeometry__SheafedSpace__toPresheafedSpace. By AlgebraicGeometry__PresheafedSpace__presheaf. By Top__top. By Opposite__op. By CategoryTheory__Functor__obj. By CommRingCat__carrier. By CommRingCat__instCommRingObjForgetRingHomCarrier. By CommRingCat__instCommRingObjForgetRingHomCarrier. By x1. By AlgebraicGeometry__Scheme__Hom__appTop. By CommRingCat__Hom__hom. By R. By and.

Mathlib.AlgebraicGeometry.Morphisms.Basic

AlgebraicGeometry.AffineTargetMorphismPropertydefMathlib.AlgebraicGeometry.Morphisms.Basic, type

Wording

affine target morphism property (from the name)

English

An affine target morphism property is a function from schemes $X$ and schemes $Y$ and homomorphisms of $X$ and $Y$ and elements of $\mathrm{Proof}$ applied to the proposition that $Y$ is affine to propositions.

AlgebraicGeometry.AffineTargetMorphismProperty.IsLocalclassMathlib.AlgebraicGeometry.Morphisms.Basic, predicate

Wording

P is local (from the name)

English

Let $P$ be an affine target morphism property. Then we can say that $P$ is local.

AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChangedefMathlib.AlgebraicGeometry.Morphisms.Basic, predicate

Wording

P is stable under base change (from the name)

English

Let $P$ be an affine target morphism property. Then $P$ is stable under base change, if for all schemes $Z$, $X$, $Y$ and $S$, for all elements $h$ of $\mathrm{Proof}$ applied to the proposition that $S$ is affine, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to the proposition that $X$ is affine, for all homomorphisms $f$ of $X$ and $S$, for all homomorphisms $g$ of $Y$ and $S$, for all homomorphisms $\mathrm{f'}$ of $Z$ and $Y$, for all homomorphisms $\mathrm{g'}$ of $Z$ and $X$, if $\operatorname{IsPullback}$ holds for $\mathrm{g'}$, $\mathrm{f'}$, $f$ and $g$, then if $P$ holds for $Y$, $S$, $g$ and $h$, then $P$ holds for $Z$, $X$, $\mathrm{g'}$ and $h_{1}$.

AlgebraicGeometry.AffineTargetMorphismProperty.ofdefMathlib.AlgebraicGeometry.Morphisms.Basic, function or constant

Wording

no wording

English

Let $P$ be a morphism property of the set of schemes. Then there is an affine target morphism property. Proof. Let $P$ be arbitrary. Let $x$ be arbitrary. Let $x_{1}$ be arbitrary. Let $f$ be arbitrary. Let $h$ be arbitrary. By x. By x1. By f. By P.

AlgebraicGeometry.AffineTargetMorphismProperty.toPropertydefMathlib.AlgebraicGeometry.Morphisms.Basic, function or constant

Wording

the property of P (from the name)

English

Let $P$ be an affine target morphism property. Then the property of $P$ is a morphism property of the set of schemes defined as the function that maps $x$, $x_{1}$ and $f$ to the proposition that there exists an element $h$ of $\operatorname{IsAffine}$ applied to $x_{1}$, such that $P$ holds for $x$, $x_{1}$, $f$ and $h$.

AlgebraicGeometry.HasAffinePropertyclassMathlib.AlgebraicGeometry.Morphisms.Basic, predicate

Wording

no wording

English

Let $P$ be a morphism property of the set of schemes. Let $Q$ be an element of $\mathrm{outParam}$ applied to the set of affine target morphism properties. Then we can say that $\operatorname{HasAffineProperty}$ holds for $P$ and $Q$.

AlgebraicGeometry.IsZariskiLocalAtSourcedefMathlib.AlgebraicGeometry.Morphisms.Basic, predicate

Wording

P is a Zariski local at source (from the name)

English

Let $P$ be a morphism property of the set of schemes. Then $P$ is a Zariski local at source, if $P$ is local at source to the Zariski precoverage.

AlgebraicGeometry.IsZariskiLocalAtTargetdefMathlib.AlgebraicGeometry.Morphisms.Basic, predicate

Wording

P is a Zariski local at target (from the name)

English

Let $P$ be a morphism property of the set of schemes. Then $P$ is a Zariski local at target, if $P$ is local at target to the Zariski precoverage.

AlgebraicGeometry.targetAffineLocallydefMathlib.AlgebraicGeometry.Morphisms.Basic, function or constant

Wording

no wording

English

Let $P$ be an affine target morphism property. Then there is a morphism property of the set of schemes. Proof. Let $P$ be arbitrary. Let $X$ be arbitrary. Let $Y$ be arbitrary. Let $f$ be arbitrary. By Y. By AlgebraicGeometry__Scheme__affineOpens. By Set__Elem. Let $U$ be arbitrary. By f. By AlgebraicGeometry__Scheme__Hom__toLRSHom'. By AlgebraicGeometry__LocallyRingedSpace__Hom__toHom. By AlgebraicGeometry__PresheafedSpace__Hom__base. By TopologicalSpace__Opens__map. By U. By CategoryTheory__Functor__obj. By AlgebraicGeometry__Scheme__Opens__toScheme. By U. By AlgebraicGeometry__Scheme__Opens__toScheme. By f. By U. By AlgebraicGeometry__morphismRestrict. By U. By AlgebraicGeometry__instIsAffineToSchemeValOpensMemSetAffineOpens. By P. By forall.

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

AlgebraicGeometry.IsClosedImmersionclassMathlib.AlgebraicGeometry.Morphisms.ClosedImmersion, predicate

Wording

f is a closed immersion (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is a closed immersion.

AlgebraicGeometry.IsClosedImmersion.liftdefMathlib.AlgebraicGeometry.Morphisms.ClosedImmersion, function or constant

Wording

the lift of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$ such that the kernel of $f$ is less than or equal to the kernel of $g$. Then the lift of $f$ and $g$ is a homomorphism of $Y$ and $X$ defined as the composition of the image of $g$ and the composition of the inclusion of $H$ and the inverse of the image of $f$.

AlgebraicGeometry.IsClosedImmersion.overEquivIdealSheafDatadefMathlib.AlgebraicGeometry.Morphisms.ClosedImmersion, function or constant

Wording

no wording

English

Let $X$ be a scheme. Then $\operatorname{overEquivIdealSheafData}$ applied to $X$ is an equivalence of the set of opposites of $\operatorname{Over}$ applied to the proposition that $\operatorname{IsClosedImmersion}$, the top and $X$ and the set of ideal sheaf data of $X$.

Mathlib.AlgebraicGeometry.Morphisms.Constructors

AlgebraicGeometry.AffineTargetMorphismProperty.diagonaldefMathlib.AlgebraicGeometry.Morphisms.Constructors, function or constant

Wording

the diagonal of P (from the name)

English

Let $P$ be an affine target morphism property. Then the diagonal of $P$ is an affine target morphism property.

AlgebraicGeometry.stalkwisedefMathlib.AlgebraicGeometry.Morphisms.Constructors, function or constant

Wording

no wording

English

Let $P$ be a function from sets $R$ and sets $S$ and elements $x$ of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $S$ is a commutative ring and ring homomorphisms of $R$ and $S$ to propositions. Then there is a morphism property of the set of schemes. Proof. Let $P$ be arbitrary. Let $x$ be arbitrary. Let $x_{1}$ be arbitrary. Let $f$ be arbitrary. Let $P$ be arbitrary. By S. By AlgebraicGeometry__Scheme__toLocallyRingedSpace. By AlgebraicGeometry__LocallyRingedSpace__toSheafedSpace. By AlgebraicGeometry__SheafedSpace__toPresheafedSpace. By AlgebraicGeometry__PresheafedSpace__carrier. By TopCat__carrier. Let $x_{2}$ be arbitrary. By x. By AlgebraicGeometry__Scheme__toLocallyRingedSpace. By AlgebraicGeometry__LocallyRingedSpace__toSheafedSpace. By AlgebraicGeometry__SheafedSpace__toPresheafedSpace. By AlgebraicGeometry__PresheafedSpace__presheaf. By x1. By AlgebraicGeometry__Scheme__Hom__toLRSHom'. By AlgebraicGeometry__LocallyRingedSpace__Hom__toHom. By AlgebraicGeometry__PresheafedSpace__Hom__base. By x2. By CategoryTheory__ConcreteCategory__hom__app. By TopCat__Presheaf__stalk. By CommRingCat__carrier. By S. By AlgebraicGeometry__Scheme__toLocallyRingedSpace. By AlgebraicGeometry__LocallyRingedSpace__toSheafedSpace. By AlgebraicGeometry__SheafedSpace__toPresheafedSpace. By AlgebraicGeometry__PresheafedSpace__presheaf. By x2. By TopCat__Presheaf__stalk. By CommRingCat__carrier. By CommRingCat__instCommRingObjForgetRingHomCarrier. By CommRingCat__instCommRingObjForgetRingHomCarrier. By x1. By x2. By AlgebraicGeometry__Scheme__Hom__stalkMap. By CommRingCat__Hom__hom. By R. By P. By forall.

AlgebraicGeometry.topologicallydefMathlib.AlgebraicGeometry.Morphisms.Constructors, function or constant

Wording

no wording

English

Let $P$ be a function from sets $x$ and sets $x_{1}$ and elements of $\mathrm{Proof}$ applied to the proposition that $x$ is a topological space and elements of $\mathrm{Proof}$ applied to the proposition that $x_{1}$ is a topological space and functions from elements of $x$ to elements of $x_{1}$ to propositions. Then there is a morphism property of the set of schemes. Proof. Let $P$ be arbitrary. Let $x$ be arbitrary. Let $x_{1}$ be arbitrary. Let $f$ be arbitrary. By x1. By AlgebraicGeometry__Scheme__toLocallyRingedSpace. By AlgebraicGeometry__LocallyRingedSpace__toSheafedSpace. By AlgebraicGeometry__SheafedSpace__toPresheafedSpace. By AlgebraicGeometry__PresheafedSpace__carrier. By TopCat__carrier. By P. By AlgebraicGeometry__Scheme__toLocallyRingedSpace. By AlgebraicGeometry__LocallyRingedSpace__toSheafedSpace. By AlgebraicGeometry__SheafedSpace__toPresheafedSpace. By AlgebraicGeometry__PresheafedSpace__carrier. By TopCat__carrier. By x1. By AlgebraicGeometry__Scheme__toLocallyRingedSpace. By AlgebraicGeometry__LocallyRingedSpace__toSheafedSpace. By AlgebraicGeometry__SheafedSpace__instTopologicalSpaceCarrierCarrier. By P. By AlgebraicGeometry__Scheme__toLocallyRingedSpace. By AlgebraicGeometry__LocallyRingedSpace__toSheafedSpace. By AlgebraicGeometry__SheafedSpace__instTopologicalSpaceCarrierCarrier. By f. By AlgebraicGeometry__Scheme__Hom__toLRSHom'. By AlgebraicGeometry__LocallyRingedSpace__Hom__toHom. By AlgebraicGeometry__PresheafedSpace__Hom__base. By CategoryTheory__ConcreteCategory__hom. By DFunLike__coe. By x.

Mathlib.AlgebraicGeometry.Morphisms.Etale

AlgebraicGeometry.EtaleclassMathlib.AlgebraicGeometry.Morphisms.Etale, predicate

Wording

f is a etale (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is an etale.

AlgebraicGeometry.Scheme.EtaledefMathlib.AlgebraicGeometry.Morphisms.Etale, type

Wording

etale of X (from the name)

English

Let $X$ be a scheme. Then an etale of $X$ is an element of the function that maps $X$ to $\operatorname{Over}$ applied to the proposition that $\operatorname{Etale}$, the top and $X$.

AlgebraicGeometry.Scheme.Etale.forgetdefMathlib.AlgebraicGeometry.Morphisms.Etale, function or constant

Wording

no wording

English

Let $X$ be a scheme. Then $\operatorname{forget}$ applied to $X$ is a functor of the set of etales of $X$ and $\operatorname{Over}$ applied to $X$ defined as the forgetful functor from the full subcategory of the proposition that $\operatorname{Etale}$.

AlgebraicGeometry.Scheme.Etale.forgetFullyFaithfuldefMathlib.AlgebraicGeometry.Morphisms.Etale, function or constant

Wording

no wording

English

Let $X$ be a scheme. Then $\operatorname{forgetFullyFaithful}$ applied to $X$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{forget}$ applied to $X$ defined as the forgetful functor from the full subcategory of the identity of the set of schemes.

AlgebraicGeometry.Scheme.Etale.mkdefMathlib.AlgebraicGeometry.Morphisms.Etale, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $Y$ and $X$. Then $\operatorname{mk}$ applied to $f$ is an etale of $X$.

Mathlib.AlgebraicGeometry.Morphisms.Finite

AlgebraicGeometry.IsFiniteclassMathlib.AlgebraicGeometry.Morphisms.Finite, predicate

Wording

f is finite (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is finite.

Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

AlgebraicGeometry.LocallyOfFinitePresentationclassMathlib.AlgebraicGeometry.Morphisms.FinitePresentation, predicate

Wording

no wording

English

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

Mathlib.AlgebraicGeometry.Morphisms.FiniteType

AlgebraicGeometry.LocallyOfFiniteTypeclassMathlib.AlgebraicGeometry.Morphisms.FiniteType, predicate

Wording

no wording

English

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

Mathlib.AlgebraicGeometry.Morphisms.Flat

AlgebraicGeometry.FlatclassMathlib.AlgebraicGeometry.Morphisms.Flat, predicate

Wording

f is flat (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is flat.

AlgebraicGeometry.pushoutSectiondefMathlib.AlgebraicGeometry.Morphisms.Flat, function or constant

Wording

the pushout section of hUSX and hUY (from the name)

English

Assume that $\operatorname{IsPullback}$ holds for $g$, $\mathrm{iY}$, $\mathrm{iX}$ and $f$. Assume that $\mathrm{UT}$ is less than or equal to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $\mathrm{US}$. Assume that $\mathrm{UX}$ is less than or equal to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $\mathrm{iX}$ and $\mathrm{US}$. Assume that $\mathrm{UY}$ is equal to the minimum of the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $g$ and $\mathrm{UX}$ and the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $\mathrm{iY}$ and $\mathrm{UT}$. Then the pushout section of $\mathrm{hUSX}$ and $\mathrm{hUY}$ is a homomorphism of the pushout of $\operatorname{appLE}$ applied to $\mathrm{iX}$, $\mathrm{US}$, $\mathrm{UX}$ and $\mathrm{hUSX}$ and $\operatorname{appLE}$ applied to $f$, $\mathrm{US}$, $\mathrm{UT}$ and $\mathrm{hUST}$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to $\mathrm{UY}$.

Mathlib.AlgebraicGeometry.Morphisms.FlatRank

AlgebraicGeometry.Scheme.Hom.finrankdefMathlib.AlgebraicGeometry.Morphisms.FlatRank, function or constant

Wording

the rank of f and s (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $S$. Let $s$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $S$. Then the rank of $f$ and $s$ is a natural number.

Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

AlgebraicGeometry.FormallyUnramifiedclassMathlib.AlgebraicGeometry.Morphisms.FormallyUnramified, predicate

Wording

f is formally unramified (from the name)

English

generation took over the time limit

Mathlib.AlgebraicGeometry.Morphisms.Immersion

AlgebraicGeometry.IsImmersionclassMathlib.AlgebraicGeometry.Morphisms.Immersion, predicate

Wording

f is a immersion (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is an immersion.

AlgebraicGeometry.Scheme.Hom.coborderRangedefMathlib.AlgebraicGeometry.Morphisms.Immersion, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{coborderRange}$ applied to $f$ is an open of $Y$.

AlgebraicGeometry.Scheme.Hom.liftCoborderdefMathlib.AlgebraicGeometry.Morphisms.Immersion, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{liftCoborder}$ applied to $f$ is a homomorphism of $X$ and the scheme of $\operatorname{coborderRange}$ applied to $f$.

Mathlib.AlgebraicGeometry.Morphisms.Integral

AlgebraicGeometry.IsIntegralHomclassMathlib.AlgebraicGeometry.Morphisms.Integral, predicate

Wording

f is a integral homomorphism (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is an integral homomorphism.

Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

AlgebraicGeometry.sourceLocalClosuredefMathlib.AlgebraicGeometry.Morphisms.LocalClosure, function or constant

Wording

the source local closure of W and P (from the name)

English

Let $W$ and $P$ be morphism properties of the set of schemes. Then the source local closure of $W$ and $P$ is a morphism property of the set of schemes defined as the function that maps $X$, $x$ and $f$ to the proposition that there exists a cover $x_{1}$ of the precoverage of $W$ and $X$, such that for all elements $i$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$, $P$ holds for $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $i$, $x$ and the composition of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $i$ and $f$.

AlgebraicGeometry.sourceLocalClosure.coverdefMathlib.AlgebraicGeometry.Morphisms.LocalClosure, function or constant

Wording

the cover of hf (from the name)

English

Assume that $\operatorname{sourceLocalClosure}$ holds for $W$ and $P$. Then the cover of $\mathrm{hf}$ is a cover of the precoverage of $W$ and $X$ defined as $\operatorname{choose}$ applied to $\mathrm{hf}$.

Mathlib.AlgebraicGeometry.Morphisms.LocalIso

AlgebraicGeometry.IsLocalIsoclassMathlib.AlgebraicGeometry.Morphisms.LocalIso, predicate

Wording

f is a local isomorphism (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is a local isomorphism.

Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

AlgebraicGeometry.IsPreimmersionclassMathlib.AlgebraicGeometry.Morphisms.Preimmersion, predicate

Wording

no wording

English

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

Mathlib.AlgebraicGeometry.Morphisms.Proper

AlgebraicGeometry.IsProperclassMathlib.AlgebraicGeometry.Morphisms.Proper, predicate

Wording

f is proper (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is proper.

Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

AlgebraicGeometry.QuasiCompactclassMathlib.AlgebraicGeometry.Morphisms.QuasiCompact, predicate

Wording

no wording

English

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

Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

AlgebraicGeometry.LocallyQuasiFiniteclassMathlib.AlgebraicGeometry.Morphisms.QuasiFinite, predicate

Wording

no wording

English

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

AlgebraicGeometry.Scheme.Hom.QuasiFiniteAtdefMathlib.AlgebraicGeometry.Morphisms.QuasiFinite, predicate

Wording

no wording

English

Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

AlgebraicGeometry.QuasiSeparatedclassMathlib.AlgebraicGeometry.Morphisms.QuasiSeparated, predicate

Wording

no wording

English

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

Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

AlgebraicGeometry.HasRingHomPropertyclassMathlib.AlgebraicGeometry.Morphisms.RingHomProperties, predicate

Wording

no wording

English

Let $P$ be a morphism property of the set of schemes. Let $Q$ be an element of $\mathrm{outParam}$ applied to the set of functions from sets $R$ and sets $S$ and elements $x$ of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $S$ is a commutative ring and ring homomorphisms of $R$ and $S$ to propositions. Then we can say that $\operatorname{HasRingHomProperty}$ holds for $P$ and $Q$.

AlgebraicGeometry.affineLocallydefMathlib.AlgebraicGeometry.Morphisms.RingHomProperties, function or constant

Wording

no wording

English

AlgebraicGeometry.sourceAffineLocallydefMathlib.AlgebraicGeometry.Morphisms.RingHomProperties, function or constant

Wording

no wording

English

Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

AlgebraicGeometry.IsSchemeTheoreticallyDominantclassMathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant, predicate

Wording

no wording

English

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

Mathlib.AlgebraicGeometry.Morphisms.Separated

AlgebraicGeometry.IsSeparatedclassMathlib.AlgebraicGeometry.Morphisms.Separated, predicate

Wording

f is separated (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is separated.

AlgebraicGeometry.Scheme.IsSeparatedclassMathlib.AlgebraicGeometry.Morphisms.Separated, predicate

Wording

X is separated (from the name)

English

Let $X$ be a scheme. Then we can say that $X$ is separated.

Mathlib.AlgebraicGeometry.Morphisms.Smooth

AlgebraicGeometry.Scheme.Hom.smoothLocusdefMathlib.AlgebraicGeometry.Morphisms.Smooth, function or constant

Wording

the smooth locus of f (from the name)

English

generation took over the time limit

AlgebraicGeometry.SmoothclassMathlib.AlgebraicGeometry.Morphisms.Smooth, predicate

Wording

f is smooth (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is smooth.

AlgebraicGeometry.SmoothOfRelativeDimensionclassMathlib.AlgebraicGeometry.Morphisms.Smooth, predicate

Wording

no wording

English

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

Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

AlgebraicGeometry.SurjectiveOnStalksclassMathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks, predicate

Wording

no wording

English

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

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

AlgebraicGeometry.IsDominantclassMathlib.AlgebraicGeometry.Morphisms.UnderlyingMap, predicate

Wording

f is dominant (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is dominant.

AlgebraicGeometry.Scheme.Hom.coverdefMathlib.AlgebraicGeometry.Morphisms.UnderlyingMap, function or constant

Wording

the cover of f and hf (from the name)

English

Let $f$ be a homomorphism of $X$ and $S$ such that $P$ holds for $X$, $S$ and $f$. Then the cover of $f$ and $\mathrm{hf}$ is a cover of the precoverage of $P$ and $S$.

AlgebraicGeometry.SurjectiveclassMathlib.AlgebraicGeometry.Morphisms.UnderlyingMap, predicate

Wording

f is surjective (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is surjective.

Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

AlgebraicGeometry.UniversallyClosedclassMathlib.AlgebraicGeometry.Morphisms.UniversallyClosed, predicate

Wording

f is universally closed (from the name)

English

generation took over the time limit

Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

AlgebraicGeometry.UniversallyInjectiveclassMathlib.AlgebraicGeometry.Morphisms.UniversallyInjective, predicate

Wording

f is universally injective (from the name)

English

generation took over the time limit

Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

AlgebraicGeometry.UniversallyOpenclassMathlib.AlgebraicGeometry.Morphisms.UniversallyOpen, predicate

Wording

f is universally open (from the name)

English

generation took over the time limit

Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

AlgebraicGeometry.WeaklyEtaleclassMathlib.AlgebraicGeometry.Morphisms.WeaklyEtale, predicate

Wording

no wording

English

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

Mathlib.AlgebraicGeometry.Noetherian

AlgebraicGeometry.IsLocallyNoetherianclassMathlib.AlgebraicGeometry.Noetherian, predicate

Wording

X is locally Noetherian (from the name)

English

generation took over the time limit

AlgebraicGeometry.IsNoetherianclassMathlib.AlgebraicGeometry.Noetherian, predicate

Wording

X is Noetherian (from the name)

English

Let $X$ be a scheme. Then we can say that $X$ is Noetherian.

Mathlib.AlgebraicGeometry.Normalization

AlgebraicGeometry.Scheme.Hom.fromNormalizationdefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{fromNormalization}$ applied to $f$ is a homomorphism of the normalization of $f$ and $Y$ defined as the base of the normalization glue data of $f$.

AlgebraicGeometry.Scheme.Hom.normalizationdefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

the normalization of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the normalization of $f$ is a scheme defined as the glued scheme of the normalization glue data of $f$.

AlgebraicGeometry.Scheme.Hom.normalizationCoprodIsodefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

the normalization coproduct isomorphism of f and e (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $e$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\mathrm{iU}$ and $\mathrm{iV}$. Then the normalization coproduct isomorphism of $f$ and $e$ is an isomorphism of the coproduct of the normalization of the composition of $\mathrm{iU}$ and $f$ and the normalization of the composition of $\mathrm{iV}$ and $f$ and the normalization of $f$.

AlgebraicGeometry.Scheme.Hom.normalizationDescdefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be a homomorphism of $X$ and $T$. Let $x_{1}$ be a homomorphism of $T$ and $Y$ such that $f$ is equal to the composition of $x$ and $x_{1}$. Then $\operatorname{normalizationDesc}$ applied to $f$, $x$, $x_{1}$ and $H$ is a homomorphism of the normalization of $f$ and $T$.

AlgebraicGeometry.Scheme.Hom.normalizationDiagramdefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

the normalization diagram of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the normalization diagram of $f$ is a functor of the set of opposites of the set of opens of $Y$ and the set of categories of commutative rings.

AlgebraicGeometry.Scheme.Hom.normalizationDiagramMapdefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

the normalization diagram map of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the normalization diagram map of $f$ is a homomorphism of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and the normalization diagram of $f$.

AlgebraicGeometry.Scheme.Hom.normalizationGlueDatadefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

the normalization glue data of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the normalization glue data of $f$ is a relative gluing data of the directed cover of $Y$ defined as the relative gluing data of $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Hom\_\_coequifibered\_normalizationDiagramMap}$ applied to $f$.

AlgebraicGeometry.Scheme.Hom.normalizationObjIsodefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

the normalization object isomorphism of f and hU (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Assume that $U$ is affine. Then the normalization object isomorphism of $f$ and $\mathrm{hU}$ is an isomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the normalization of $f$ and $\operatorname{op}$ applied to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $\operatorname{fromNormalization}$ applied to $f$ and $U$ and $\operatorname{of}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\mathrm{integralClosure} (\operatorname{carrier} (\operatorname{obj} (\operatorname{presheaf} (\operatorname{toPresheafedSpace} (\operatorname{toSheafedSpace} (\operatorname{toLocallyRingedSpace} (Y)))), \operatorname{op} (U))), \operatorname{carrier} (\operatorname{obj} (\operatorname{presheaf} (\operatorname{toPresheafedSpace} (\operatorname{toSheafedSpace} (\operatorname{toLocallyRingedSpace} (X)))), \operatorname{op} (\operatorname{obj} (\operatorname{map} (\operatorname{base} (\operatorname{toHom} (\operatorname{toLRSHom'} (f)))), U)))))}{x})}$.

AlgebraicGeometry.Scheme.Hom.normalizationOpenCoverdefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

the normalization open cover of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the normalization open cover of $f$ is an open cover of the normalization of $f$ defined as the cover of the normalization glue data of $f$.

AlgebraicGeometry.Scheme.Hom.normalizationPullbackdefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

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

English

Let $f$ be a homomorphism of $X$ and $S$. Let $g$ be a homomorphism of $Y$ and $S$. Then the normalization pullback of $f$ and $g$ is a homomorphism of the normalization of the second projection of the pullback of $f$ and $g$ and the pullback of $\operatorname{fromNormalization}$ applied to $f$ and $g$.

AlgebraicGeometry.Scheme.Hom.toNormalizationdefMathlib.AlgebraicGeometry.Normalization, function or constant

Wording

the dominant morphism into the relative normalization of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the dominant morphism into the relative normalization of $f$ is a homomorphism of $X$ and the normalization of $f$.

Mathlib.AlgebraicGeometry.OpenImmersion

AlgebraicGeometry.IsOpenImmersiondefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

no wording

English

There is a morphism property of the set of schemes. Proof. Let $x$ be arbitrary. Let $x_{1}$ be arbitrary. Let $f$ be arbitrary. By f. By AlgebraicGeometry__Scheme__Hom__toLRSHom. By AlgebraicGeometry__LocallyRingedSpace__IsOpenImmersion.

AlgebraicGeometry.IsOpenImmersion.isoOfRangeEqdefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the isomorphism of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$ such that the range of $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ is equal to the range of $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $g$. Then the isomorphism of $f$ and $g$ is an isomorphism of $X$ and $Y$.

AlgebraicGeometry.IsOpenImmersion.isoRestrictdefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Z$. Then $\operatorname{isoRestrict}$ applied to $f$ is an isomorphism of $X$ and the restriction of $Z$ and $\operatorname{isOpenEmbedding}$ applied to $f$ defined as the unique isomorphism of $\operatorname{fullyFaithfulForgetToLocallyRingedSpace}$ and $\operatorname{isoRestrict}$ applied to $\operatorname{toLRSHom}$ applied to $f$.

AlgebraicGeometry.IsOpenImmersion.liftdefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the lift of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$ such that the range of $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $g$ is less than or equal to the range of $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$. Then the lift of $f$ and $g$ is a homomorphism of $Y$ and $X$ defined as $\operatorname{mk}$ applied to the lift of $\operatorname{toLRSHom}$ applied to $f$ and $\operatorname{toLRSHom}$ applied to $g$.

AlgebraicGeometry.IsOpenImmersion.opensEquivdefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the open equivalence of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the open equivalence of $f$ is an element of $\EquivMACRoAE {\operatorname{Opens} (X)}{(\SubtypeSet {U}{\mathrm{Leq} (U , \operatorname{opensRange} (f))})}$.

AlgebraicGeometry.IsOpenImmersion.ΓIsodefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the isomorphism of f and U (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Then the isomorphism of $f$ and $U$ is an isomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to the minimum of the image of $f$ and $U$.

AlgebraicGeometry.IsOpenImmersion.ΓIsoTopdefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the isomorphism top of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the isomorphism top of $f$ is an isomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the top and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to the image of $f$.

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.schemedefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the scheme of X and h (from the name)

English

generation took over the time limit

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemedefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the scheme of Y and f (from the name)

English

Let $Y$ be a scheme. Let $f$ be a homomorphism of $X$ and $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$. Then the scheme of $Y$ and $f$ is a scheme.

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHomdefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the scheme homomorphism of Y and f (from the name)

English

generation took over the time limit

AlgebraicGeometry.Scheme.Hom.appIsodefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the isomorphism of f and U (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $X$. Then the isomorphism of $f$ and $U$ is an isomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to the action of the functor of $f$ and $U$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$ defined as the inverse of $\operatorname{asIso}$ applied to the inverse application of $\operatorname{toLRSHom}$ applied to $f$ and $U$.

AlgebraicGeometry.Scheme.Hom.opensFunctordefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the functor of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the functor of $f$ is a functor of the set of opens of $X$ and the set of opens of $Y$ defined as the functor of $\operatorname{toLRSHom}$ applied to $f$.

AlgebraicGeometry.Scheme.Hom.opensFunctorAdjunctiondefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the open functor adjunction of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the open functor adjunction of $f$ is an adjunction of the functor of $f$ and the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$.

AlgebraicGeometry.Scheme.Hom.opensRangedefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the image of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the image of $f$ is an open of $Y$.

AlgebraicGeometry.Scheme.ofRestrictdefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the canonical map from the restriction to the subspace of X and h (from the docstring)

English

Let $X$ be a scheme. Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Then the canonical map from the restriction to the subspace of $X$ and $h$ is a homomorphism of the restriction of $X$ and $h$ and $X$ defined as $\operatorname{mk}$ applied to the canonical map from the restriction to the subspace of $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $h$.

AlgebraicGeometry.Scheme.restrictdefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the restriction of X and h (from the docstring)

English

Let $X$ be a scheme. Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Then the restriction of $X$ and $h$ is a scheme.

AlgebraicGeometry.Scheme.stalkMapIsoOfIsPullbackdefMathlib.AlgebraicGeometry.OpenImmersion, function or constant

Wording

the stalk map isomorphism of p and x (from the name)

English

Assume that $\operatorname{IsPullback}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Let $p$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $P$. Let $x$ be an element of $\mathrm{optParam}$ applied to the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $\mathrm{fst}$ and $p$ such that $\mathrm{autoParam}$ holds for the proposition that $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $\mathrm{fst}$ and $p$ is equal to $x$ and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_stalkMapIsoOfIsPullback\_\_\_auto\_1}$. Then the stalk map isomorphism of $p$ and $x$ is an isomorphism of $\operatorname{mk}$ applied to the stalk map of $f$ and $x$ and $\operatorname{mk}$ applied to the stalk map of $\mathrm{snd}$ and $p$.

Mathlib.AlgebraicGeometry.OrderOfVanishing

AlgebraicGeometry.Scheme.orddefMathlib.AlgebraicGeometry.OrderOfVanishing, function or constant

Wording

the order of vanishing of f and z (from the docstring)

English

Let $f$ be a carrier of the function field of $X$. Let $z$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the order of vanishing of $f$ and $z$ is an integer defined as $\mathrm{dite}$ applied to $\EqtMACRoH {\operatorname{coheight} (z)}{1}$, the function that maps $\mathrm{hz}$ to $\operatorname{toAdd}$ applied to $\operatorname{unzeroD}$ applied to $1$ and $\operatorname{ordHom}$ applied to $z$, $\mathrm{hz}$ and $f$ and the function that maps $\mathrm{hz1}$ to $0$.

AlgebraicGeometry.Scheme.ordHomdefMathlib.AlgebraicGeometry.OrderOfVanishing, function or constant

Wording

the order homomorphism of z and hz (from the name)

English

Let $z$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ such that $\EqtMACRoH {\operatorname{coheight} (z)}{1}$. Then the order homomorphism of $z$ and $\mathrm{hz}$ is a monoid with zero homomorphism of the set of carriers of the function field of $X$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$ defined as $\operatorname{ordFrac}$ applied to the set of carriers of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $z$.

Mathlib.AlgebraicGeometry.Over

AlgebraicGeometry.Scheme.CanonicallyOverdefMathlib.AlgebraicGeometry.Over, type

Wording

no wording

English

Let $X$ and $S$ be schemes. Then an element of $\operatorname{CanonicallyOver}$ applied to $X$ and $S$ is an element of the function that maps $X$ and $S$ to $\operatorname{CanonicallyOverClass}$ applied to $X$ and $S$.

AlgebraicGeometry.Scheme.Hom.IsOverdefMathlib.AlgebraicGeometry.Over, predicate

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $S$ be a scheme. Then $\operatorname{IsOver}$ holds for $f$ and $S$, if $\operatorname{HomIsOver}$ holds for $f$ and $S$.

AlgebraicGeometry.Scheme.Hom.asOverdefMathlib.AlgebraicGeometry.Over, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $S$ be a scheme. Then $\operatorname{asOver}$ applied to $f$ and $S$ is a homomorphism of $\operatorname{asOver}$ applied to $X$ and $S$ and $\operatorname{asOver}$ applied to $Y$ and $S$ defined as $\operatorname{asOverHom}$ applied to $S$ and $f$.

AlgebraicGeometry.Scheme.OverdefMathlib.AlgebraicGeometry.Over, type

Wording

no wording

English

Let $X$ and $S$ be schemes. Then an element of $\operatorname{Over}$ applied to $X$ and $S$ is an element of the function that maps $X$ and $S$ to $\operatorname{OverClass}$ applied to $X$ and $S$.

AlgebraicGeometry.Scheme.asOverdefMathlib.AlgebraicGeometry.Over, function or constant

Wording

no wording

English

Let $X$ and $S$ be schemes. Then $\operatorname{asOver}$ applied to $X$ and $S$ is an element of $\operatorname{Over}$ applied to $S$ defined as $\operatorname{asOver}$ applied to $X$ and $S$.

Mathlib.AlgebraicGeometry.PointsPi

AlgebraicGeometry.pointsPidefMathlib.AlgebraicGeometry.PointsPi, function or constant

Wording

the point product of x1 and i1 (from the name)

English

Let $R$ be a function from elements of $x$ to categories of commutative rings. Let $X$ be a scheme. Let $x_{1}$ be a homomorphism of the spectrum of $\operatorname{of}$ applied to the set of functions from elements $i_{1}$ of $x$ to carriers of $R$ applied to $i_{1}$ and $X$. Let $i$ be an element of $x$. Then the point product of $x_{1}$ and $i$ is a homomorphism of the spectrum of $R$ applied to $i$ and $X$ defined as the composition of the induced map of the commutative ring category of the evaluation ring homomorphism of the function that maps $x_{2}$ to the set of carriers of $R$ applied to $x_{2}$ and $i$ and $x_{1}$.

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

AlgebraicGeometry.Proj.affineOpenCoverdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

the affine open cover of x3 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then the affine open cover of $x_{3}$ is an affine open cover of the projection of $x_{3}$.

AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpandefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

the affine open cover of x3 and f (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be a function from elements of $x_{5}$ to elements of $A$ such that for all elements $i_{1}$ of $x_{5}$, $\MembershipmemMACRoT {x_{3} (m (i_{1}))}{f (i_{1})}$. Assume that for all elements $i$ of $x_{5}$, $0 < m (i)$. Assume that the ideal of $\operatorname{irrelevant}$ applied to $x_{3}$ is less than or equal to the span of the range of $f$. Then the affine open cover of $x_{3}$ and $f$ is an affine open cover of the projection of $x_{3}$.

AlgebraicGeometry.Proj.awayToSectiondefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be an element of $A$. Then $\operatorname{awayToSection}$ applied to $x_{3}$ and $f$ is a homomorphism of $\operatorname{of}$ applied to $\operatorname{Away}$ applied to $x_{3}$ and $f$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the projection of $x_{3}$ and $\operatorname{op}$ applied to $\operatorname{basicOpen}$ applied to $x_{3}$ and $f$ defined as $\operatorname{awayToSection}$ applied to $x_{3}$ and $f$.

AlgebraicGeometry.Proj.awayιdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be an element of $A$ such that $\MembershipmemMACRoT {x_{3} (m)}{f}$. Assume that $0 < m$. Then $\mathrm{AlgebraicGeometry\_\_Proj\_\_away\_u3b9\_}$ applied to $x_{3}$, $f$, $\mathrm{f\_deg}$ and $\mathrm{hm}$ is a homomorphism of the spectrum of $\operatorname{of}$ applied to $\operatorname{Away}$ applied to $x_{3}$ and $f$ and the projection of $x_{3}$ defined as the composition of the inverse of $\operatorname{basicOpenIsoSpec}$ applied to $x_{3}$, $f$, $\mathrm{f\_deg}$ and $\mathrm{hm}$ and the inclusion of $\operatorname{basicOpen}$ applied to $x_{3}$ and $f$.

AlgebraicGeometry.Proj.basicOpendefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be an element of $A$. Then $\operatorname{basicOpen}$ applied to $x_{3}$ and $f$ is an open of the projection of $x_{3}$ defined as $\operatorname{basicOpen}$ applied to $x_{3}$ and $f$.

AlgebraicGeometry.Proj.basicOpenIsoAwaydefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be an element of $A$ such that $\MembershipmemMACRoT {x_{3} (m)}{f}$. Assume that $0 < m$. Then $\operatorname{basicOpenIsoAway}$ applied to $x_{3}$, $f$, $\mathrm{f\_deg}$ and $\mathrm{hm}$ is an isomorphism of $\operatorname{of}$ applied to $\operatorname{Away}$ applied to $x_{3}$ and $f$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the projection of $x_{3}$ and $\operatorname{op}$ applied to $\operatorname{basicOpen}$ applied to $x_{3}$ and $f$ defined as $\operatorname{asIso}$ applied to $\operatorname{awayToSection}$ applied to $x_{3}$ and $f$.

AlgebraicGeometry.Proj.basicOpenIsoSpecdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be an element of $A$ such that $\MembershipmemMACRoT {x_{3} (m)}{f}$. Assume that $0 < m$. Then $\operatorname{basicOpenIsoSpec}$ applied to $x_{3}$, $f$, $\mathrm{f\_deg}$ and $\mathrm{hm}$ is an isomorphism of the scheme of $\operatorname{basicOpen}$ applied to $x_{3}$ and $f$ and the spectrum of $\operatorname{of}$ applied to $\operatorname{Away}$ applied to $x_{3}$ and $f$ defined as $\operatorname{asIso}$ applied to $\operatorname{basicOpenToSpec}$ applied to $x_{3}$ and $f$.

AlgebraicGeometry.Proj.basicOpenToSpecdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be an element of $A$. Then $\operatorname{basicOpenToSpec}$ applied to $x_{3}$ and $f$ is a homomorphism of the scheme of $\operatorname{basicOpen}$ applied to $x_{3}$ and $f$ and the spectrum of $\operatorname{of}$ applied to $\operatorname{Away}$ applied to $x_{3}$ and $f$ defined as the composition of the spectrum of $\operatorname{basicOpen}$ applied to $x_{3}$ and $f$ and the induced map of $\operatorname{awayToSection}$ applied to $x_{3}$ and $f$.

AlgebraicGeometry.Proj.fromOfGlobalSectionsdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be a ring homomorphism of $A$ and the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the top such that the map of $f$ and the ideal of $\operatorname{irrelevant}$ applied to $x_{3}$ is equal to the top. Then $\operatorname{fromOfGlobalSections}$ applied to $x_{3}$, $f$ and $\mathrm{hf}$ is a homomorphism of $X$ and the projection of $x_{3}$.

AlgebraicGeometry.Proj.openCoverOfMapIrrelevantEqTopdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

the open cover of x3 and f (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be a ring homomorphism of $A$ and the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the top such that the map of $f$ and the ideal of $\operatorname{irrelevant}$ applied to $x_{3}$ is equal to the top. Then the open cover of $x_{3}$ and $f$ is an open cover of $X$.

AlgebraicGeometry.Proj.pullbackAwayιIsodefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$ such that $\MembershipmemMACRoT {x_{3} (m)}{f}$. Assume that $0 < m$. Assume that $\MembershipmemMACRoT {x_{3} (\mathrm{m'})}{g}$. Assume that $0 < \mathrm{m'}$. Assume that $\EqtMACRoH {x_{5}}{f \times g}$. Then $\mathrm{AlgebraicGeometry\_\_Proj\_\_pullbackAway\_u3b9\_Iso}$ applied to $x_{3}$, $\mathrm{f\_deg}$, $\mathrm{hm}$, $\mathrm{g\_deg}$, $\mathrm{hm'}$ and $\mathrm{hx}$ is an isomorphism of the pullback of $\mathrm{AlgebraicGeometry\_\_Proj\_\_away\_u3b9\_}$ applied to $x_{3}$, $f$, $\mathrm{f\_deg}$ and $\mathrm{hm}$ and $\mathrm{AlgebraicGeometry\_\_Proj\_\_away\_u3b9\_}$ applied to $x_{3}$, $g$, $\mathrm{g\_deg}$ and $\mathrm{hm'}$ and the spectrum of $\operatorname{of}$ applied to $\operatorname{Away}$ applied to $x_{3}$ and $x_{5}$.

AlgebraicGeometry.Proj.stalkIsodefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

the stalk isomorphism of x3 and x5 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $x_{5}$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the projection of $x_{3}$. Then the stalk isomorphism of $x_{3}$ and $x_{5}$ is an isomorphism of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the projection of $x_{3}$ and $x_{5}$ and $\operatorname{of}$ applied to $\operatorname{AtPrime}$ applied to $x_{3}$ and the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$ defined as the commutative ring category isomorphism of the stalk isomorphism of $x_{3}$ and $x_{5}$.

AlgebraicGeometry.Proj.toBasicOpenOfGlobalSectionsdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be a ring homomorphism of $A$ and the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the top such that $\EqtMACRoH {f (t)}{x_{5}}$. Assume that $0 < d$. Assume that $\MembershipmemMACRoT {x_{3} (d)}{t}$. Then $\operatorname{toBasicOpenOfGlobalSections}$ applied to $x_{3}$, $f$, $H$, $\mathrm{h0d}$ and $\mathrm{hd}$ is a homomorphism of the scheme of $\operatorname{basicOpen}$ applied to $X$ and $x_{5}$ and the scheme of $\operatorname{basicOpen}$ applied to $x_{3}$ and $t$.

AlgebraicGeometry.Proj.toSpecZerodefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic, function or constant

Wording

the spectrum zero of x3 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then the spectrum zero of $x_{3}$ is a homomorphism of the projection of $x_{3}$ and the spectrum of $\operatorname{of}$ applied to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {x_{3} (0)}{x_{5}})}$ defined as the composition of the inverse of the top isomorphism of the projection of $x_{3}$ and the composition of the inverse of the isomorphism of the projection of $x_{3}$ and $\mathrm{AlgebraicGeometry\_\_Proj\_\_basicOpen\_one}$ applied to $x_{3}$ and the composition of $\operatorname{basicOpenToSpec}$ applied to $x_{3}$ and $1$ and the induced map of the commutative ring category of $\operatorname{fromZeroRingHom}$ applied to $x_{3}$ and the power of $1$.

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

AlgebraicGeometry.Proj.comapStructureSheafdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor, function or constant

Wording

the preimage structure sheaf of U and V (from the name)

English

Let $f$ be a graded ring homomorphism of $x_{6}$ and $x_{7}$ such that $\operatorname{irrelevant}$ applied to $x_{7}$ is less than or equal to the map of $f$ and $\operatorname{irrelevant}$ applied to $x_{6}$. Let $U$ be an open of the set of projective spectra of $x_{6}$. Let $V$ be an open of the set of projective spectra of $x_{7}$ such that the carrier of $V$ is less than or equal to the preimage of $\operatorname{coe}$ applied to the preimage of $f$ and $\mathrm{hf}$ and the carrier of $U$. Then the preimage structure sheaf of $U$ and $V$ is a ring homomorphism of the set of carriers of the action of the object of the structure sheaf of $x_{6}$ and $\operatorname{op}$ applied to $U$ and the set of carriers of the action of the object of the structure sheaf of $x_{7}$ and $\operatorname{op}$ applied to $V$.

AlgebraicGeometry.Proj.comapStructureSheafFundefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor, function or constant

Wording

the underlying function of f (from the docstring)

English

Let $f$ be a graded ring homomorphism of $x_{6}$ and $x_{7}$ such that $\operatorname{irrelevant}$ applied to $x_{7}$ is less than or equal to the map of $f$ and $\operatorname{irrelevant}$ applied to $x_{6}$. Let $U$ be an open of the set of projective spectra of $x_{6}$. Let $V$ be an open of the set of projective spectra of $x_{7}$ such that the carrier of $V$ is less than or equal to the preimage of $\operatorname{coe}$ applied to the preimage of $f$ and $\mathrm{hf}$ and the carrier of $U$. Let $s$ be a function from elements $x_{11}$ of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {U}{x_{12}})}$ to elements of $\operatorname{AtPrime}$ applied to $x_{6}$ and $\operatorname{toSubmodule}$ applied to $\operatorname{asHomogeneousIdeal}$ applied to $x_{11}$. Let $y$ be an element of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {V}{x_{10}})}$. Then the underlying function of $f$ is an element of $\operatorname{AtPrime}$ applied to $x_{7}$ and $\operatorname{toSubmodule}$ applied to $\operatorname{asHomogeneousIdeal}$ applied to $y$.

AlgebraicGeometry.Proj.mapdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor, function or constant

Wording

the map of f and hf (from the name)

English

Let $f$ be a graded ring homomorphism of $x_{6}$ and $x_{7}$ such that $\operatorname{irrelevant}$ applied to $x_{7}$ is less than or equal to the map of $f$ and $\operatorname{irrelevant}$ applied to $x_{6}$. Then the map of $f$ and $\mathrm{hf}$ is a homomorphism of the projection of $x_{7}$ and the projection of $x_{6}$.

AlgebraicGeometry.Proj.mapAffineOpenCoverdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor, function or constant

Wording

the map affine open cover of f and hf (from the name)

English

AlgebraicGeometry.Proj.sheafedSpaceMapdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor, function or constant

Wording

the sheafed space map of f and hf (from the name)

English

Let $f$ be a graded ring homomorphism of $x_{6}$ and $x_{7}$ such that $\operatorname{irrelevant}$ applied to $x_{7}$ is less than or equal to the map of $f$ and $\operatorname{irrelevant}$ applied to $x_{6}$. Then the sheafed space map of $f$ and $\mathrm{hf}$ is a homomorphism of the sheafed space of $x_{7}$ and the sheafed space of $x_{6}$.

AlgebraicGeometry.ProjectiveSpectrum.comapdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor, function or constant

Wording

the preimage of f and hf (from the name)

English

Let $f$ be a graded ring homomorphism of $x_{6}$ and $x_{7}$ such that $\operatorname{irrelevant}$ applied to $x_{7}$ is less than or equal to the map of $f$ and $\operatorname{irrelevant}$ applied to $x_{6}$. Then the preimage of $f$ and $\mathrm{hf}$ is a continuous map of the set of projective spectra of $x_{7}$ and the set of projective spectra of $x_{6}$.

AlgebraicGeometry.ProjectiveSpectrum.comapFundefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor, function or constant

Wording

the underlying function of f (from the docstring)

English

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

AlgebraicGeometry.ProjdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

the projection of x3 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then the projection of $x_{3}$ is a scheme.

AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrierdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

the carrier of f_deg and q (from the name)

English

generation took over the time limit

AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asHomogeneousIdealdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

no wording

English

generation took over the time limit

AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdealdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

no wording

English

generation took over the time limit

AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFundefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

no wording

English

generation took over the time limit

AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrierdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

the carrier of x5 (from the name)

English

generation took over the time limit

AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFundefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

the spectrum of f and x5 (from the name)

English

generation took over the time limit

AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpecdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

no wording

English

generation took over the time limit

AlgebraicGeometry.ProjIsoSpecTopComponent.toSpecdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

the spectrum of x3 and f (from the name)

English

generation took over the time limit

AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSectiondefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

no wording

English

AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

no wording

English

generation took over the time limit

AlgebraicGeometry.ProjectiveSpectrum.Proj.specStalkEquivdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

the spectrum stalk equivalence of f and x5 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $f$ be an element of $A$. Let $x_{5}$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{basicOpen} (x_{3} , f)}{x_{7}})}$. Assume that $\MembershipmemMACRoT {x_{3} (m)}{f}$. Assume that $0 < m$. Then the spectrum stalk equivalence of $f$ and $x_{5}$ is an isomorphism of the stalk of the underlying presheaf of the structure sheaf of $\operatorname{Away}$ applied to $x_{3}$ and $f$ and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to the spectrum of $x_{3}$ and $f$ and $x_{5}$ and $\operatorname{of}$ applied to $\operatorname{AtPrime}$ applied to $x_{3}$ and the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$ defined as the commutative ring category isomorphism of the ring isomorphism of the algebra isomorphism of the complement of $\operatorname{asIdeal}$ applied to $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to the spectrum of $x_{3}$ and $f$ and $x_{5}$.

AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpecdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

the spectrum of x3 and f (from the name)

English

generation took over the time limit

AlgebraicGeometry.projIsoSpecdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

the projection isomorphism spectrum of x3 and f (from the name)

English

generation took over the time limit

AlgebraicGeometry.projIsoSpecTopComponentdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme, function or constant

Wording

the projection isomorphism spectrum top component of f_deg and hm (from the name)

English

generation took over the time limit

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

AlgebraicGeometry.Proj.stalkIso'defMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

the stalk isomorphism of x3 and x5 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $x_{5}$ be a carrier of the underlying topology of $x_{3}$. Then the stalk isomorphism of $x_{3}$ and $x_{5}$ is a ring isomorphism of the set of carriers of the stalk of the underlying presheaf of the structure sheaf of $x_{3}$ and $x_{5}$ and $\operatorname{AtPrime}$ applied to $x_{3}$ and the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$.

AlgebraicGeometry.Proj.toLocallyRingedSpacedefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

the locally ringed space of x3 (from the name)

English

generation took over the time limit

AlgebraicGeometry.Proj.toSheafedSpacedefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

the sheafed space of x3 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then the sheafed space of $x_{3}$ is a sheafed space of the set of categories of commutative rings.

AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheafdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

the structure sheaf of x3 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then the structure sheaf of $x_{3}$ is a sheaf of the set of categories of commutative rings and the underlying topology of $x_{3}$.

AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.IsFractiondefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, predicate

Wording

f is a fraction (from the name)

English

Let $f$ be a function from elements $x_{5}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {U}{x_{6}})}$ to elements of $\operatorname{AtPrime}$ applied to $x_{3}$ and the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$. Then $x_{5}$ is a fraction, if there exists a natural number $i$, such that there exists an element $r$ of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {x_{3} (i)}{x_{10}})}$, such that there exists an element $s$ of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{3} (i)}{x_{9}})}$, such that there exists an element $\mathrm{s\_nin}$ of $\mathrm{forall}$ applied to $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {U}{x_{8}})}$ and the function that maps $x_{7}$ to the proposition that $s$ is not an element of $\operatorname{asHomogeneousIdeal}$ applied to $x_{7}$, such that for all elements $x_{5}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {U}{x_{6}})}$, $\EqtMACRoH {x_{5} (x_{5})}{\operatorname{mk} (\operatorname{mk} (i , r , s , \mathrm{s\_nin} (x_{5})))}$.

AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isFractionPrelocaldefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then $\operatorname{isFractionPrelocal}$ applied to $x_{3}$ is a prelocal predicate of the function that maps $x_{5}$ to $\operatorname{AtPrime}$ applied to $x_{3}$ and the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$.

AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFractiondefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then $\operatorname{isLocallyFraction}$ applied to $x_{3}$ is a local predicate of the function that maps $x_{5}$ to $\operatorname{AtPrime}$ applied to $x_{3}$ and the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$ defined as the sheafification of $\operatorname{isFractionPrelocal}$ applied to $x_{3}$.

AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.sectionsSubringdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

the section subring of U (from the name)

English

Let $U$ be an opposite of the set of opens of the set of carriers of the underlying topology of $x_{3}$. Then the section subring of $U$ is a subring of the set of functions from elements $x_{5}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{unop} (U)}{x_{6}})}$ to elements of $\operatorname{AtPrime}$ applied to $x_{3}$ and the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $f$ to $\operatorname{pred}$ applied to $\operatorname{toPrelocalPredicate}$ applied to $\operatorname{isLocallyFraction}$ applied to $x_{3}$ and $f$ and the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{AlgebraicGeometry\_\_ProjectiveSpectrum\_\_StructureSheaf\_\_SectionSubring\_\_mul\_mem'}$ applied to $U$, $x_{5}$ and $x_{6}$ and $\mathrm{AlgebraicGeometry\_\_ProjectiveSpectrum\_\_StructureSheaf\_\_SectionSubring\_\_one\_mem'}$ applied to $U$, the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{AlgebraicGeometry\_\_ProjectiveSpectrum\_\_StructureSheaf\_\_SectionSubring\_\_add\_mem'}$ applied to $U$, $x_{7}$ and $x_{8}$ and $\mathrm{AlgebraicGeometry\_\_ProjectiveSpectrum\_\_StructureSheaf\_\_SectionSubring\_\_zero\_mem'}$ applied to $U$ and the function that maps $x_{9}$ to $\mathrm{AlgebraicGeometry\_\_ProjectiveSpectrum\_\_StructureSheaf\_\_SectionSubring\_\_neg\_mem'}$ applied to $U$ and $x_{9}$.

AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafCompForgetdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then $\operatorname{structurePresheafCompForget}$ applied to $x_{3}$ is an isomorphism of the composition of the structure presheaf in commutative ring of $x_{3}$ and the forgetful functor of the set of categories of commutative rings and the object of the structure sheaf in type of $x_{3}$.

AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRingdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

the structure presheaf in commutative ring of x3 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then the structure presheaf in commutative ring of $x_{3}$ is a presheaf of the set of categories of commutative rings and the underlying topology of $x_{3}$.

AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInTypedefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

the structure sheaf in type of x3 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then the structure sheaf in type of $x_{3}$ is a sheaf of the set of sets and the underlying topology of $x_{3}$ defined as the subsheaf to type of $\operatorname{isLocallyFraction}$ applied to $x_{3}$.

AlgebraicGeometry.homogeneousLocalizationToStalkdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

the homogeneous localization to stalk of x5 and y (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $x_{5}$ be a carrier of the underlying topology of $x_{3}$. Let $y$ be an element of $\operatorname{AtPrime}$ applied to $x_{3}$ and the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$. Then the homogeneous localization to stalk of $x_{5}$ and $y$ is a carrier of the stalk of the underlying presheaf of the structure sheaf of $x_{3}$ and $x_{5}$.

AlgebraicGeometry.openToLocalizationdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

the open to localization of U and x5 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $U$ be an open of the set of carriers of the underlying topology of $x_{3}$. Let $x_{5}$ be a carrier of the underlying topology of $x_{3}$ such that $x_{5}$ is an element of $U$. Then the open to localization of $U$ and $x_{5}$ is a homomorphism of the action of the object of the structure sheaf of $x_{3}$ and $\operatorname{op}$ applied to $U$ and $\operatorname{of}$ applied to $\operatorname{AtPrime}$ applied to $x_{3}$ and the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$.

AlgebraicGeometry.sectionInBasicOpendefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $x_{5}$ be a carrier of the underlying topology of $x_{3}$. Let $f$ be a numerator denominator same degree of $x_{3}$ and the complement of the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$. Then $\operatorname{sectionInBasicOpen}$ applied to $x_{3}$, $x_{5}$ and $f$ is a carrier of the action of the object of the structure sheaf of $x_{3}$ and $\operatorname{op}$ applied to $\operatorname{basicOpen}$ applied to $x_{3}$ and the denominator of $f$.

AlgebraicGeometry.stalkToFiberRingHomdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf, function or constant

Wording

the stalk to fiber ring homomorphism of x3 and x5 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $x_{5}$ be a carrier of the underlying topology of $x_{3}$. Then the stalk to fiber ring homomorphism of $x_{3}$ and $x_{5}$ is a homomorphism of the stalk of the underlying presheaf of the structure sheaf of $x_{3}$ and $x_{5}$ and $\operatorname{of}$ applied to $\operatorname{AtPrime}$ applied to $x_{3}$ and the ideal of $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$.

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

ProjectiveSpectrumstructureMathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology, type

Wording

projective spectrum of x3 (from the name)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then the projective spectra of $x_{3}$ are a basic type.

ProjectiveSpectrum.asHomogeneousIdealdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a projective spectrum of $x_{3}$. Then $\operatorname{asHomogeneousIdeal}$ applied to $\mathrm{self}$ is a homogeneous ideal of $x_{3}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

ProjectiveSpectrum.basicOpendefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology, function or constant

Wording

no wording

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $r$ be an element of $A$. Then $\operatorname{basicOpen}$ applied to $x_{3}$ and $r$ is an open of the set of projective spectra of $x_{3}$.

ProjectiveSpectrum.topdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology, function or constant

Wording

the underlying topology of x3 (from the docstring)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Then the underlying topology of $x_{3}$ is a topological category defined as $\operatorname{of}$ applied to the set of projective spectra of $x_{3}$.

ProjectiveSpectrum.vanishingIdealdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology, function or constant

Wording

the vanishing ideal of t (from the docstring)

English

Let $t$ be an element of the power set of the set of projective spectra of $x_{3}$. Then the vanishing ideal of $t$ is a homogeneous ideal of $x_{3}$ defined as the infimum of the function that maps $x_{5}$ to the infimum of the function that maps $h_{1}$ to $\operatorname{asHomogeneousIdeal}$ applied to $x_{5}$.

ProjectiveSpectrum.zeroLocusdefMathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology, function or constant

Wording

the zero locus of x3 and s (from the docstring)

English

Let $x_{3}$ be a function from natural numbers to elements of $x$. Let $s$ be an element of $\wp A$. Then the zero locus of $x_{3}$ and $s$ is an element of the power set of the set of projective spectra of $x_{3}$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{5}$ to $\mathrm{Leq} (s , \operatorname{asHomogeneousIdeal} (x_{5}))$.

Mathlib.AlgebraicGeometry.Properties

AlgebraicGeometry.IsIntegralclassMathlib.AlgebraicGeometry.Properties, predicate

Wording

X is integral (from the name)

English

Let $X$ be a scheme. Then we can say that $X$ is integral.

AlgebraicGeometry.IsReducedclassMathlib.AlgebraicGeometry.Properties, predicate

Wording

X is reduced (from the name)

English

Let $X$ be a scheme. Then we can say that $X$ is reduced.

Mathlib.AlgebraicGeometry.PullbackCarrier

AlgebraicGeometry.Scheme.Pullback.SpecOfPointdefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

the spectrum of t (from the name)

English

Let $t$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the pullback of $f$ and $g$. Then the spectrum of $t$ is a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of the tensor of the triplet of $t$ defined as $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the induced map of the pullback of $t$ and the bottom.

AlgebraicGeometry.Scheme.Pullback.TripletstructureMathlib.AlgebraicGeometry.PullbackCarrier, type

Wording

triplet of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $S$. Let $g$ be a homomorphism of $Y$ and $S$. Then the triplets of $f$ and $g$ are a basic type.

AlgebraicGeometry.Scheme.Pullback.Triplet.SpecTensorTodefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

no wording

English

Let $T$ be a triplet of $f$ and $g$. Then $\operatorname{SpecTensorTo}$ applied to $T$ is a homomorphism of the spectrum of the tensor of $T$ and the pullback of $f$ and $g$ defined as the lift of the composition of the induced map of the tensor left injection of $T$ and $\operatorname{fromSpecResidueField}$ applied to $X$ and $\operatorname{x}$ applied to $T$ and the composition of the induced map of the tensor right injection of $T$ and $\operatorname{fromSpecResidueField}$ applied to $Y$ and $\operatorname{y}$ applied to $T$.

AlgebraicGeometry.Scheme.Pullback.Triplet.mk'defMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

no wording

English

Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Let $y$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ such that $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $x$ is equal to $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $g$ and $y$. Then $\operatorname{mk'}$ applied to $x$, $y$ and $h$ is a triplet of $f$ and $g$.

AlgebraicGeometry.Scheme.Pullback.Triplet.ofPointdefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

the triplet of t (from the name)

English

AlgebraicGeometry.Scheme.Pullback.Triplet.sdefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a triplet of $f$ and $g$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $S$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.Pullback.Triplet.tensordefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

the tensor of T (from the name)

English

Let $T$ be a triplet of $f$ and $g$. Then the tensor of $T$ is a category of commutative rings defined as the pushout of the composition of the inverse of the residue field congruence of $\operatorname{hx}$ applied to $T$ and the residue field map of $f$ and $\operatorname{x}$ applied to $T$ and the composition of the inverse of the residue field congruence of $\operatorname{hy}$ applied to $T$ and the residue field map of $g$ and $\operatorname{y}$ applied to $T$.

AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongrdefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

the tensor congruence of e (from the name)

English

Assume that $\EqtMACRoH {x}{x_{1}}$. Then the tensor congruence of $e$ is an isomorphism of the tensor of $x$ and the tensor of $x_{1}$.

AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInldefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

the tensor left injection of T (from the name)

English

Let $T$ be a triplet of $f$ and $g$. Then the tensor left injection of $T$ is a homomorphism of the residue field of $X$ and $\operatorname{x}$ applied to $T$ and the tensor of $T$ defined as the left injection of the composition of the inverse of the residue field congruence of $\operatorname{hx}$ applied to $T$ and the residue field map of $f$ and $\operatorname{x}$ applied to $T$ and the composition of the inverse of the residue field congruence of $\operatorname{hy}$ applied to $T$ and the residue field map of $g$ and $\operatorname{y}$ applied to $T$.

AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInrdefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

the tensor right injection of T (from the name)

English

Let $T$ be a triplet of $f$ and $g$. Then the tensor right injection of $T$ is a homomorphism of the residue field of $Y$ and $\operatorname{y}$ applied to $T$ and the tensor of $T$ defined as the right injection of the composition of the inverse of the residue field congruence of $\operatorname{hx}$ applied to $T$ and the residue field map of $f$ and $\operatorname{x}$ applied to $T$ and the composition of the inverse of the residue field congruence of $\operatorname{hy}$ applied to $T$ and the residue field map of $g$ and $\operatorname{y}$ applied to $T$.

AlgebraicGeometry.Scheme.Pullback.Triplet.xdefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a triplet of $f$ and $g$. Then $\operatorname{x}$ applied to $\mathrm{self}$ is a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.Pullback.Triplet.ydefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a triplet of $f$ and $g$. Then $\operatorname{y}$ applied to $\mathrm{self}$ is a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.Pullback.carrierEquivdefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

the carrier equivalence (from the name)

English

The carrier equivalence is an equivalence from the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the pullback of $f$ and $g$ to $\Sigma$ applied to the function that maps $T$ to the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of the tensor of $T$.

AlgebraicGeometry.Scheme.Pullback.ofPointTensordefMathlib.AlgebraicGeometry.PullbackCarrier, function or constant

Wording

the pullback of t (from the name)

English

Let $t$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the pullback of $f$ and $g$. Then the pullback of $t$ is a homomorphism of the tensor of the triplet of $t$ and the residue field of the pullback of $f$ and $g$ and $t$ defined as $\operatorname{desc}$ applied to the residue field map of the first projection of the pullback of $f$ and $g$ and $t$, the residue field map of the second projection of the pullback of $f$ and $g$ and $t$ and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Pullback\_\_residueFieldCongr\_inv\_residueFieldMap\_ofPoint}$ applied to $t$.

Mathlib.AlgebraicGeometry.Pullbacks

AlgebraicGeometry.Scheme.Pullback.diagonalCoverdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the diagonal cover of x and x1 (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be an open cover of $Y$. Let $x_{1}$ be a function from elements $i$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and $x$ to open covers of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and $x$ and $i$. Then the diagonal cover of $x$ and $i$ is an open cover of the diagonal object of $f$ defined as the function that maps $x_{1}$ to $\operatorname{bind}$ applied to the open cover of $f$ and $f$, the function that maps $i$ to the open cover of the pullback homomorphism of $f$ and $i$ and the pullback homomorphism of $f$ and $i$ and $x_{1}$.

AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRangedefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the diagonal cover diagonal range of x and x1 (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be an open cover of $Y$. Let $x_{1}$ be a function from elements $i$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and $x$ to open covers of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and $x$ and $i$. Then the diagonal cover diagonal range of $x$ and $i$ is an open of the diagonal object of $f$ defined as the function that maps $x_{1}$ to the supremum of the function that maps $i$ to the image of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the diagonal cover of $x$ and $i$ and $\operatorname{mk}$ applied to $\operatorname{fst}$ applied to $i$ and $\ProdmkMACRoU {\operatorname{snd} (i)}{\operatorname{snd} (i)}$.

AlgebraicGeometry.Scheme.Pullback.diagonalRestrictIsoDiagonaldefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be an open cover of $Y$. Let $x_{1}$ be a function from elements $i_{1}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and $x$ to open covers of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and $x$ and $i_{1}$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the open cover of $f$ and $f$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ applied to $i$. Then $\operatorname{diagonalRestrictIsoDiagonal}$ applied to $f$, $x$, $i_{1}$, $x_{1}$, $i$ and $j$ is an isomorphism of $\operatorname{mk}$ applied to the restriction of the diagonal morphism of $f$ and the image of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the diagonal cover of $x$ and $x_{1}$ and $\operatorname{mk}$ applied to $i$ and $\ProdmkMACRoU {j}{j}$ and $\operatorname{mk}$ applied to the diagonal morphism of the composition of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ applied to $i$ and $j$ and the second projection of the pullback of $f$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$.

AlgebraicGeometry.Scheme.Pullback.fVdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

no wording

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $i$ and $j$ be elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$. Then $\operatorname{fV}$ applied to $x$, $f$, $g$, $i$ and $j$ is a homomorphism of $\operatorname{v}$ applied to $x$, $f$, $g$, $i$ and $j$ and the pullback of the composition of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and $f$ and $g$ defined as the first projection of the pullback of the composition of the first projection of the pullback of the composition of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and $f$ and $g$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$.

AlgebraicGeometry.Scheme.Pullback.gluedIsLimitdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

no wording

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{gluedIsLimit}$ applied to $x$, $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{p1}$ applied to $x$, $f$ and $g$, $\operatorname{p2}$ applied to $x$, $f$ and $g$ and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Pullback\_\_p\_comm}$ applied to $x$, $f$ and $g$ defined as $\operatorname{isLimitAux'}$ applied to $\operatorname{mk}$ applied to $\operatorname{p1}$ applied to $x$, $f$ and $g$, $\operatorname{p2}$ applied to $x$, $f$ and $g$ and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Pullback\_\_p\_comm}$ applied to $x$, $f$ and $g$ and the function that maps $s$ to the glued lift of $g$ and $s$.

AlgebraicGeometry.Scheme.Pullback.gluedLiftdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the glued lift of g and s (from the name)

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $s$ be a pullback cone of $f$ and $g$. Then the glued lift of $g$ and $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and the glued scheme of the gluing of $f$ and $g$.

AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMapdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the glued lift pullback map of i and j (from the name)

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $s$ be a pullback cone of $f$ and $g$. Let $i$ and $j$ be elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$. Then the glued lift pullback map of $i$ and $j$ is a homomorphism of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of the first projection of $s$ and $x$ and $i$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of the first projection of $s$ and $x$ and $j$ and $\operatorname{V}$ applied to $\operatorname{toGlueData}$ applied to the gluing of $f$ and $g$ and $\ProdmkMACRoU {i}{j}$.

AlgebraicGeometry.Scheme.Pullback.gluingdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the gluing of f and g (from the name)

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the gluing of $f$ and $g$ is a glue data.

AlgebraicGeometry.Scheme.Pullback.openCoverOfBasedefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the open cover of f and g (from the name)

English

Let $x$ be an open cover of $Z$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the open cover of $f$ and $g$ is an open cover of the pullback of $f$ and $g$.

AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'defMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the open cover of f and g (from the name)

English

AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the open cover of f and g (from the name)

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the open cover of $f$ and $g$ is an open cover of the pullback of $f$ and $g$.

AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRightdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the open cover of f and g (from the name)

English

Let $x$ be an open cover of $X$. Let $x_{1}$ be an open cover of $Y$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the open cover of $f$ and $g$ is an open cover of the pullback of $f$ and $g$.

AlgebraicGeometry.Scheme.Pullback.openCoverOfRightdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the open cover of f and g (from the name)

English

Let $x$ be an open cover of $Y$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the open cover of $f$ and $g$ is an open cover of the pullback of $f$ and $g$.

AlgebraicGeometry.Scheme.Pullback.p1defMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

no wording

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{p1}$ applied to $x$, $f$ and $g$ is a homomorphism of the glued scheme of the gluing of $f$ and $g$ and $X$.

AlgebraicGeometry.Scheme.Pullback.p2defMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

no wording

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{p2}$ applied to $x$, $f$ and $g$ is a homomorphism of the glued scheme of the gluing of $f$ and $g$ and $Y$.

AlgebraicGeometry.Scheme.Pullback.pullbackFstιToVdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

no wording

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $i$ and $j$ be elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$. Then $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Pullback\_\_pullbackFst\_u3b9\_ToV}$ applied to $x$, $f$, $g$, $i$ and $j$ is a homomorphism of the pullback of the first projection of the pullback of $\operatorname{p1}$ applied to $x$, $f$ and $g$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and the inclusion of the gluing of $f$ and $g$ and $j$ and $\operatorname{v}$ applied to $x$, $f$, $g$, $j$ and $i$.

AlgebraicGeometry.Scheme.Pullback.pullbackP1IsodefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the pullback isomorphism of g and i (from the name)

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$. Then the pullback isomorphism of $g$ and $i$ is an isomorphism of the pullback of $\operatorname{p1}$ applied to $x$, $f$ and $g$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and the pullback of the composition of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and $f$ and $g$.

AlgebraicGeometry.Scheme.Pullback.tdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

no wording

English

AlgebraicGeometry.Scheme.Pullback.t'defMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

no wording

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $i$, $j$ and $k$ be elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$. Then $\operatorname{t'}$ applied to $x$, $f$, $g$, $i$, $j$ and $k$ is a homomorphism of the pullback of $\operatorname{fV}$ applied to $x$, $f$, $g$, $i$ and $j$ and $\operatorname{fV}$ applied to $x$, $f$, $g$, $i$ and $k$ and the pullback of $\operatorname{fV}$ applied to $x$, $f$, $g$, $j$ and $k$ and $\operatorname{fV}$ applied to $x$, $f$, $g$, $j$ and $i$.

AlgebraicGeometry.Scheme.Pullback.vdefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

no wording

English

Let $x$ be an open cover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $i$ and $j$ be elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$. Then $\operatorname{v}$ applied to $x$, $f$, $g$, $i$ and $j$ is a scheme defined as the pullback of the composition of the first projection of the pullback of the composition of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and $f$ and $g$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$.

AlgebraicGeometry.pullbackSpecIsodefMathlib.AlgebraicGeometry.Pullbacks, function or constant

Wording

the pullback spectrum isomorphism of S and T (from the name)

English

Let $R$, $S$ and $T$ be sets. Then the pullback spectrum isomorphism of $S$ and $T$ is an isomorphism of the pullback of the induced map of the commutative ring category of the algebra map of $R$ and $S$ and the induced map of the commutative ring category of the algebra map of $R$ and $T$ and the spectrum of $\operatorname{of}$ applied to the set of tensor products of $S$ and $T$.

Mathlib.AlgebraicGeometry.QuasiAffine

AlgebraicGeometry.Scheme.IsQuasiAffineclassMathlib.AlgebraicGeometry.QuasiAffine, predicate

Wording

no wording

English

Let $X$ be a scheme. Then we can say that $\operatorname{IsQuasiAffine}$ holds for $X$.

AlgebraicGeometry.Scheme.openCoverBasicOpenTopdefMathlib.AlgebraicGeometry.QuasiAffine, function or constant

Wording

no wording

English

Let $X$ be a scheme. Then $\operatorname{openCoverBasicOpenTop}$ applied to $X$ is an open cover of $X$.

Mathlib.AlgebraicGeometry.RelativeGluing

AlgebraicGeometry.Scheme.Cover.RelativeGluingDatastructureMathlib.AlgebraicGeometry.RelativeGluing, type

Wording

relative gluing data of x (from the name)

English

Let $x$ be an open cover of $S$. Then the relative gluing data of $x$ are a basic type.

AlgebraicGeometry.Scheme.Cover.RelativeGluingData.coverdefMathlib.AlgebraicGeometry.RelativeGluing, function or constant

Wording

the cover of d (from the name)

English

Let $d$ be a relative gluing data of $x$. Then the cover of $d$ is an open cover of the glued scheme of $d$ defined as the open cover of the colimit of the functor of $d$.

AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functordefMathlib.AlgebraicGeometry.RelativeGluing, function or constant

Wording

the functor of self (from the name)

English

Let $\mathrm{self}$ be a relative gluing data of $x$. Then the functor of $\mathrm{self}$ is a functor of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and the set of schemes defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.Cover.RelativeGluingData.glueddefMathlib.AlgebraicGeometry.RelativeGluing, function or constant

Wording

the glued scheme of d (from the docstring)

English

Let $d$ be a relative gluing data of $x$. Then the glued scheme of $d$ is a scheme defined as the colimit of the functor of $d$.

AlgebraicGeometry.Scheme.Cover.RelativeGluingData.natTransdefMathlib.AlgebraicGeometry.RelativeGluing, function or constant

Wording

the natural transformation of self (from the name)

English

generation took over the time limit

AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBasedefMathlib.AlgebraicGeometry.RelativeGluing, function or constant

Wording

the base of d (from the name)

English

Let $d$ be a relative gluing data of $x$. Then the base of $d$ is a homomorphism of the glued scheme of $d$ and $S$ defined as $\operatorname{desc}$ applied to the functor of $d$ and $\operatorname{mk}$ applied to $S$ and the composition of the natural transformation of $d$ and the functor of $x$.

Mathlib.AlgebraicGeometry.ResidueField

AlgebraicGeometry.Scheme.Hom.residueDegreedefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

the residue degree of f and x (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the residue degree of $f$ and $x$ is a natural number defined as the rank of the set of carriers of the residue field of $Y$ and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $x$ and the set of carriers of the residue field of $X$ and $x$.

AlgebraicGeometry.Scheme.Hom.residueFieldMapdefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

the residue field map of f and x (from the name)

English

AlgebraicGeometry.Scheme.Spec.residueFieldIsodefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

the residue field isomorphism of R and x (from the name)

English

Let $R$ be a category of commutative rings. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$. Then the residue field isomorphism of $R$ and $x$ is an isomorphism of the residue field of the spectrum of $R$ and $x$ and $\operatorname{of}$ applied to the set of residue fields of $\operatorname{asIdeal}$ applied to $x$ defined as the commutative ring category isomorphism of the map equivalence of the commutative ring category isomorphism to ring isomorphism of the stalk isomorphism of $R$ and $x$.

AlgebraicGeometry.Scheme.Spec.residueFieldIsoOfFielddefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

the residue field isomorphism of x1 (from the name)

English

Let $x_{1}$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $\operatorname{of}$ applied to $k$. Then the residue field isomorphism of $x_{1}$ is an isomorphism of the residue field of the spectrum of $\operatorname{of}$ applied to $k$ and $x_{1}$ and $\operatorname{of}$ applied to $k$ defined as the composition of the inverse of $\operatorname{asIso}$ applied to the evaluation of the spectrum of $\operatorname{of}$ applied to $k$ and $x_{1}$ and the spectrum isomorphism of $\operatorname{of}$ applied to $k$.

AlgebraicGeometry.Scheme.SpecToEquivOfFielddefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

the spectrum to equivalence of K and X (from the name)

English

Let $K$ be a set. Let $X$ be a scheme. Then the spectrum to equivalence of $K$ and $X$ is an equivalence from the set of homomorphisms of the spectrum of $\operatorname{of}$ applied to $K$ and $X$ to $\Sigma$ applied to the function that maps $x_{1}$ to the set of homomorphisms of the residue field of $X$ and $x_{1}$ and $\operatorname{of}$ applied to $K$.

AlgebraicGeometry.Scheme.descResidueFielddefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x_{1}$ and $\operatorname{of}$ applied to $K$. Then $\operatorname{descResidueField}$ applied to $f$ is a homomorphism of the residue field of $X$ and $x_{1}$ and $\operatorname{of}$ applied to $K$ defined as the commutative ring category of the lift of the underlying ring hom of $f$.

AlgebraicGeometry.Scheme.evaluationdefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

the evaluation of U and x (from the name)

English

Let $X$ be a scheme. Let $U$ be an open of $X$. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ such that $x$ is an element of $U$. Then the evaluation of $U$ and $x$ is a homomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$ and the residue field of $X$ and $x$ defined as the composition of the germ of $U$ and $x$ and the residue map from the stalk to the residue field of $X$ and $x$.

AlgebraicGeometry.Scheme.fromSpecResidueFielddefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

no wording

English

AlgebraicGeometry.Scheme.residuedefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

the residue map from the stalk to the residue field of X and x (from the docstring)

English

Let $X$ be a scheme. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the residue map from the stalk to the residue field of $X$ and $x$ is a homomorphism of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x$ and the residue field of $X$ and $x$ defined as the commutative ring category of the quotient map of the set of carriers of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x$.

AlgebraicGeometry.Scheme.residueFielddefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

the residue field of X and x (from the name)

English

Let $X$ be a scheme. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the residue field of $X$ and $x$ is a category of commutative rings defined as $\operatorname{of}$ applied to the set of residue fields of the set of carriers of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x$.

AlgebraicGeometry.Scheme.residueFieldCongrdefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

the residue field congruence of h (from the name)

English

Assume that $\EqtMACRoH {x}{y}$. Then the residue field congruence of $h$ is an isomorphism of the residue field of $X$ and $x$ and the residue field of $X$ and $y$.

AlgebraicGeometry.Scheme.ΓevaluationdefMathlib.AlgebraicGeometry.ResidueField, function or constant

Wording

the evaluation of X and x (from the name)

English

Let $X$ be a scheme. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the evaluation of $X$ and $x$ is a homomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the top and the residue field of $X$ and $x$ defined as the evaluation of the top and $x$.