Definitions: Mathlib.AlgebraicGeometry, part 1 of 3

AlgebraicGeometry.AffineScheme.SpecdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the spectrum (from the name)

English

The spectrum is a functor of the set of opposites of the set of categories of commutative rings and the set of affine schemes defined as the essential image of the spectrum.

AlgebraicGeometry.AffineScheme.equivCommRingCatdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the equivalence commutative ring category (from the name)

English

The equivalence commutative ring category is an equivalence of the set of affine schemes and the set of opposites of the set of categories of commutative rings defined as the inverse of the equivalence essential image.

AlgebraicGeometry.AffineScheme.forgetToSchemedefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the forgetful functor (from the docstring)

English

The forgetful functor is a functor of the set of affine schemes and the set of schemes defined as the inclusion of the essential image of the spectrum.

AlgebraicGeometry.AffineScheme.mkdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

no wording

English

Let $X$ be an affine scheme. Then $\operatorname{mk}$ applied to $X$ and $h$ is an affine scheme.

AlgebraicGeometry.AffineScheme.ofdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

no wording

English

Let $X$ be a scheme. Then $\operatorname{of}$ applied to $X$ is an affine scheme defined as $\operatorname{mk}$ applied to $X$ and $h$.

AlgebraicGeometry.AffineScheme.ofHomdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the affine scheme of f (from the name)

English

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

AlgebraicGeometry.AffineScheme.ΓdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

no wording

English

$\mathrm{AlgebraicGeometry\_\_AffineScheme\_\_\_u393\_}$ is a functor of the set of opposites of the set of affine schemes and the set of categories of commutative rings defined as the composition of the opposite of the forgetful functor and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_\_u393\_}$.

AlgebraicGeometry.IsAffineclassMathlib.AlgebraicGeometry.AffineScheme, predicate

Wording

X is affine (from the docstring)

English

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

AlgebraicGeometry.IsAffineOpendefMathlib.AlgebraicGeometry.AffineScheme, predicate

Wording

U is affine (from the docstring)

English

Let $U$ be an open of $X$. Then $U$ is affine, if the scheme of $U$ is affine.

AlgebraicGeometry.IsAffineOpen.appBasicOpenIsoAwayMapdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Assume that $U$ is affine. Assume that the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$ is affine. Let $r$ be a carrier 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 $U$. Then $\operatorname{appBasicOpenIsoAwayMap}$ applied to $f$, $\mathrm{hU}$, $h$ and $r$ is an isomorphism of $\operatorname{mk}$ applied to the homomorphism of $f$ and $\operatorname{basicOpen}$ applied to $Y$ and $r$ and $\operatorname{mk}$ applied to the commutative ring category of the map of the underlying ring hom of the homomorphism of $f$ and $U$ and $r$.

AlgebraicGeometry.IsAffineOpen.arrowStalkMapIsodefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the arrow stalk map isomorphism of U and V (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an affine open of $Y$. Let $V$ be an open of $X$ such that $V$ is affine, $V$ 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 $U$ and $x$ is an element of $V$. Then the arrow stalk map isomorphism of $U$ and $V$ is an isomorphism of $\operatorname{mk}$ applied to the stalk map of $f$ and $x$ and $\operatorname{mk}$ applied to the commutative ring category of the local ring homomorphism of $\operatorname{asIdeal}$ applied to the prime ideal of $\mathrm{hV}$ and $x$ and the underlying ring hom of $\operatorname{appLE}$ applied to $f$, $U$, $V$ and $\mathrm{hVU}$.

AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffinedefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

no wording

English

Assume that $U$ is affine. Let $f$ be a carrier 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 $\operatorname{basicOpenSectionsToAffine}$ applied to $\mathrm{hU}$ and $f$ 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 $\operatorname{basicOpen}$ applied to $X$ and $f$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to 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 $U$ and $\operatorname{op}$ applied to $\operatorname{basicOpen}$ applied to $f$.

AlgebraicGeometry.IsAffineOpen.fromSpecdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

no wording

English

Assume that $U$ is affine. Then $\operatorname{fromSpec}$ applied to $\mathrm{hU}$ is a homomorphism of 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 $U$ and $X$ defined as the composition of the inverse of the isomorphism of $\mathrm{hU}$ and the inclusion of $U$.

AlgebraicGeometry.IsAffineOpen.isoSpecdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the isomorphism of hU (from the docstring)

English

Assume that $U$ is affine. Then the isomorphism of $\mathrm{hU}$ is an isomorphism of the scheme of $U$ 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 $U$ defined as the composition of the canonical isomorphism of the scheme of $U$ and the map isomorphism of the spectrum and the opposite isomorphism of the inverse of the top isomorphism of $U$.

AlgebraicGeometry.IsAffineOpen.primeIdealOfdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the prime ideal of hU and x (from the name)

English

Assume that $U$ is affine. Let $x$ be an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {U}{x_{1}})}$. Then the prime ideal of $\mathrm{hU}$ and $x$ is a prime spectrum 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{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the homomorphism of the isomorphism of $\mathrm{hU}$ and $x$.

AlgebraicGeometry.IsOpenImmersion.affineOpensEquivdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the affine open equivalence of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the affine open equivalence of $f$ is an order isomorphism of the set of elements of the affine open of $X$ and $\SubtypeSet {U}{\mathrm{Leq} (U , \operatorname{opensRange} (f))}$.

AlgebraicGeometry.Scheme.AffineOpenCover.ofIsOpenCoverdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the affine open cover of U (from the name)

English

Let $U$ be a function from elements of $x$ to opens of $X$ such that $U$ is an open cover and for all elements $i$ of $x$, $U$ applied to $i$ is affine. Then the affine open cover of $U$ is an affine open cover of $X$.

AlgebraicGeometry.Scheme.Hom.liftQuotientdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the lift quotient of f and I (from the name)

English

Let $f$ be a homomorphism of $X$ and the spectrum of $A$. Let $I$ be an ideal of the set of carriers of $A$ such that $I$ is less than or equal to the kernel of the underlying ring hom of the composition of the inverse of the spectrum isomorphism of $A$ and the application top of $f$. Then the lift quotient of $f$ and $I$ is a homomorphism of $X$ and the spectrum of $\operatorname{of}$ applied to the set of quotients of the set of carriers of $A$ and $I$ defined as the composition of the spectrum of $X$ and the induced map of the commutative ring category of the lift of $I$ and the underlying ring hom of the composition of the inverse of the spectrum isomorphism of $A$ and the application top of $f$.

AlgebraicGeometry.Scheme.Opens.toSpecΓdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the spectrum of U (from the name)

English

Let $U$ be an open of $X$. Then the spectrum of $U$ is a homomorphism of the scheme of $U$ 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 $U$ defined as the composition of the spectrum of the scheme of $U$ and the induced map of the inverse of the top isomorphism of $U$.

AlgebraicGeometry.Scheme.affineBasicOpendefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

no wording

English

Let $X$ be a scheme. Let $f$ be a carrier 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 $\operatorname{affineBasicOpen}$ applied to $X$ and $f$ is an element of the affine open of $X$ defined as $\operatorname{basicOpen}$ applied to $X$ and $f$.

AlgebraicGeometry.Scheme.affineOpensdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the affine open of X (from the name)

English

Let $X$ be a scheme. Then the affine open of $X$ is an element of the power set of the set of opens of $X$ defined as $\operatorname{ofPred}$ applied to the function that maps $U$ to the proposition that $U$ is affine.

AlgebraicGeometry.Scheme.arrowStalkMapSpecIsodefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the arrow stalk map spectrum isomorphism of f and p (from the name)

English

Let $f$ be a homomorphism of $R$ and $S$. Let $p$ be a prime spectrum of the set of carriers of $S$. Then the arrow stalk map spectrum isomorphism of $f$ and $p$ is an isomorphism of $\operatorname{mk}$ applied to the stalk map of the induced map of $f$ and $p$ and $\operatorname{mk}$ applied to the commutative ring category of the local ring homomorphism of $\operatorname{asIdeal}$ applied to $p$ and the underlying ring hom of $f$.

AlgebraicGeometry.Scheme.isoSpecdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the canonical isomorphism of X (from the docstring)

English

Let $X$ be a scheme. Then the canonical isomorphism of $X$ is an isomorphism 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 $\operatorname{asIso}$ applied to the spectrum of $X$.

AlgebraicGeometry.Spec.stalkIsodefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the stalk isomorphism of R and x (from the name)

English

Let $R$ be a category of commutative rings. Let $x$ be a prime spectrum of the set of carriers of $R$. Then the stalk isomorphism of $R$ and $x$ is an isomorphism of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and $x$ and $\operatorname{of}$ applied to $\operatorname{AtPrime}$ applied to $\operatorname{asIdeal}$ applied to $x$ defined as the inverse of the commutative ring category isomorphism of the ring isomorphism of the stalk isomorphism of the set of carriers of $R$ and $x$.

AlgebraicGeometry.SpecMapRestrictBasicOpenIsodefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $R$ and $S$. Let $r$ be a carrier of $R$. Then $\operatorname{SpecMapRestrictBasicOpenIso}$ applied to $f$ and $r$ is an isomorphism of $\operatorname{mk}$ applied to the restriction of the induced map of $f$ and $\operatorname{basicOpen}$ applied to $r$ and $\operatorname{mk}$ applied to the induced map of the commutative ring category of $\operatorname{awayMap}$ applied to the underlying ring hom of $f$ and $r$.

AlgebraicGeometry.affineOpensRestrictdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

no wording

English

Let $U$ be an open of $X$. Then $\operatorname{affineOpensRestrict}$ applied to $U$ is an equivalence from the set of elements of the affine open of the scheme of $U$ to $\SubtypeSet {V}{\mathrm{Leq} (V , U)}$.

AlgebraicGeometry.arrowIsoSpecΓOfIsAffinedefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the arrow isomorphism spectrum of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the arrow isomorphism spectrum of $f$ is an isomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to the induced map of the application top of $f$.

AlgebraicGeometry.arrowIsoΓSpecOfIsAffinedefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the arrow isomorphism spectrum of f (from the name)

English

Let $f$ be a homomorphism of $A$ and $B$. Then the arrow isomorphism spectrum of $f$ is an isomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to the application top of the induced map of $f$.

AlgebraicGeometry.specTargetImagedefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the spectrum target image of f (from the name)

English

Let $f$ be a homomorphism of $X$ and the spectrum of $A$. Then the spectrum target image of $f$ is a category of commutative rings defined as $\operatorname{of}$ applied to the set of quotients of the set of carriers of $A$ and the spectrum target image ideal of $f$.

AlgebraicGeometry.specTargetImageFactorizationdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the spectrum target image factorization of f (from the name)

English

Let $f$ be a homomorphism of $X$ and the spectrum of $A$. Then the spectrum target image factorization of $f$ is a homomorphism of $X$ and the spectrum of the spectrum target image of $f$.

AlgebraicGeometry.specTargetImageIdealdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the spectrum target image ideal of f (from the name)

English

Let $f$ be a homomorphism of $X$ and the spectrum of $A$. Then the spectrum target image ideal of $f$ is an ideal of the set of carriers of $A$ defined as the kernel of the underlying ring hom of the opposite of $\operatorname{symm}$ applied to the homomorphism equivalence of $X$ and $\operatorname{op}$ applied to $A$ and $f$.

AlgebraicGeometry.specTargetImageRingHomdefMathlib.AlgebraicGeometry.AffineScheme, function or constant

Wording

the spectrum target image ring homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and the spectrum of $A$. Then the spectrum target image ring homomorphism of $f$ is a homomorphism of $A$ and the spectrum target image of $f$ defined as the commutative ring category of $\operatorname{mk}$ applied to the spectrum target image ideal of $f$.

Mathlib.AlgebraicGeometry.AffineSpace

AlgebraicGeometry.AffineSpacedefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the affine space of n and S (from the name)

English

Let $n$ be a set. Let $S$ be a scheme. Then the affine space of $n$ and $S$ is a scheme defined as the pullback of the map of $S$ and the map of the spectrum of $\operatorname{of}$ applied to the set of multivariate polynomials of $n$ and $\mathrm{ULift}$ applied to $\Integer$.

AlgebraicGeometry.AffineSpace.SpecIsodefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the spectrum isomorphism of n and R (from the name)

English

Let $n$ be a set. Let $R$ be a category of commutative rings. Then the spectrum isomorphism of $n$ and $R$ is an isomorphism of the affine space of $n$ and the spectrum of $R$ and the spectrum of $\operatorname{of}$ applied to the set of multivariate polynomials of $n$ and the set of carriers of $R$ defined as the composition of the affine space of $n$ and the spectrum of $R$ and the map isomorphism of the spectrum and the opposite isomorphism of the commutative ring category isomorphism of the map equivalence of $n$ and the commutative ring category isomorphism to ring isomorphism of the inverse of the spectrum isomorphism of $R$.

AlgebraicGeometry.AffineSpace.coorddefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the coordinate of S and i (from the name)

English

Let $S$ be a scheme. Let $i$ be an element of $n$. Then the coordinate of $S$ and $i$ is a carrier of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the affine space of $n$ and $S$ and $\operatorname{op}$ applied to the top defined as $\operatorname{toSpecMvPolyIntEquiv}$ applied to $n$, the spectrum multivariate polynomial of $n$ and $S$ and $i$.

AlgebraicGeometry.AffineSpace.functordefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the affine space as a functor (from the docstring)

English

The affine space as a functor is a functor of the set of opposites of the set of sets and the set of functors of the set of schemes and the set of schemes.

AlgebraicGeometry.AffineSpace.homOfVectordefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the homomorphism of f and v (from the name)

English

Let $f$ be a homomorphism of $X$ and $S$. Let $v$ be a function from elements of $n$ to 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 homomorphism of $f$ and $v$ is a homomorphism of $X$ and the affine space of $n$ and $S$.

AlgebraicGeometry.AffineSpace.homOverEquivdefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the homomorphism over equivalence of S (from the name)

English

Let $S$ be a scheme. Then the homomorphism over equivalence of $S$ is an equivalence from $\SubtypeSet {f}{\operatorname{IsOver} (f , S)}$ to the set of functions from elements of $n$ to 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.AffineSpace.isoOfIsAffinedefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the affine space of n and S (from the docstring)

English

Let $n$ be a set. Let $S$ be a scheme. Then the affine space of $n$ and $S$ is an isomorphism of the affine space of $n$ and $S$ and the spectrum of $\operatorname{of}$ applied to the set of multivariate polynomials of $n$ and the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $S$ and $\operatorname{op}$ applied to the top.

AlgebraicGeometry.AffineSpace.mapdefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the map of n and f (from the name)

English

Let $n$ be a set. Let $f$ be a homomorphism of $S$ and $T$. Then the map of $n$ and $f$ is a homomorphism of the affine space of $n$ and $S$ and the affine space of $n$ and $T$ defined as the homomorphism of the composition of $\operatorname{over}$ applied to the affine space of $n$ and $S$, $S$ and $\mathrm{inferInstance}$ and $f$ and $\operatorname{coord}$ applied to $S$.

AlgebraicGeometry.AffineSpace.mapSpecMapdefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the map spectrum map of x (from the name)

English

Let $x$ be a homomorphism of $R$ and $S$. Then the map spectrum map of $x$ is an isomorphism of $\operatorname{mk}$ applied to the map of $n$ and the induced map of $x$ and $\operatorname{mk}$ applied to the induced map of the commutative ring category of the map of the underlying ring hom of $x$.

AlgebraicGeometry.AffineSpace.reindexdefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the reindexing of i and S (from the name)

English

Let $i$ be a function from elements of $m$ to elements of $n$. Let $S$ be a scheme. Then the reindexing of $i$ and $S$ is a homomorphism of the affine space of $n$ and $S$ and the affine space of $m$ and $S$ defined as the homomorphism of $\operatorname{over}$ applied to the affine space of $n$ and $S$, $S$ and $\mathrm{inferInstance}$ and $\operatorname{comp}$ applied to $\operatorname{coord}$ applied to $S$ and $i$.

AlgebraicGeometry.AffineSpace.toSpecMvPolydefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the spectrum multivariate polynomial of n and S (from the name)

English

Let $n$ be a set. Let $S$ be a scheme. Then the spectrum multivariate polynomial of $n$ and $S$ is a homomorphism of the affine space of $n$ and $S$ and the spectrum of $\operatorname{of}$ applied to the set of multivariate polynomials of $n$ and $\mathrm{ULift}$ applied to $\Integer$ defined as the second projection of the pullback of the map of $S$ and the map of the spectrum of $\operatorname{of}$ applied to the set of multivariate polynomials of $n$ and $\mathrm{ULift}$ applied to $\Integer$.

AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquivdefMathlib.AlgebraicGeometry.AffineSpace, function or constant

Wording

the spectrum multivariate polynomial integer equivalence of n (from the name)

English

Let $n$ be a set. Then the spectrum multivariate polynomial integer equivalence of $n$ is an equivalence from the set of homomorphisms of $X$ and the spectrum of $\operatorname{of}$ applied to the set of multivariate polynomials of $n$ and $\mathrm{ULift}$ applied to $\Integer$ to the set of functions from elements of $n$ to 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.

Mathlib.AlgebraicGeometry.AffineTransitionLimit

AlgebraicGeometry.ExistsHomHomCompEqCompAux.D'defMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $A$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D}$ applied to $A$. Then $\operatorname{D'}$ applied to $A$ and $j$ is a functor of $\operatorname{Over}$ applied to $\operatorname{i'}$ applied to $A$ and the set of schemes defined as the composition of the post of $D$ and the composition of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D}$ applied to $A$ and $j$ and $\operatorname{forget}$ applied to $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D}$ applied to $A$ and $j$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.adefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Then $\operatorname{a}$ applied to $\mathrm{self}$ is a homomorphism of the action of $D$ and $\operatorname{i}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.bdefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Then $\operatorname{b}$ applied to $\mathrm{self}$ is a homomorphism of the action of $D$ and $\operatorname{i}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.cdefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Then $\operatorname{c}$ applied to $\mathrm{self}$ is a cone of $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.c'defMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $A$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D}$ applied to $A$. Then $\operatorname{c'}$ applied to $A$ and $j$ is a cone of $\operatorname{D'}$ applied to $A$ and $j$ defined as the map cone of the composition of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D}$ applied to $A$ and $j$ and $\operatorname{forget}$ applied to $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D}$ applied to $A$ and $j$ and the action of the cone post of $D$ and $\operatorname{i'}$ applied to $A$ and $\operatorname{c}$ applied to $A$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.gdefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $A$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Then $\operatorname{g}$ applied to $A$ is a homomorphism of the action of $D$ and $\operatorname{i'}$ applied to $A$ and the pullback of $f$ and $f$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.hcdefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Then $\operatorname{hc}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{c}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.hc'defMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $A$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D}$ applied to $A$. Then $\operatorname{hc'}$ applied to $A$ and $j$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{c'}$ applied to $A$ and $j$ defined as $\operatorname{isLimitOfPreserves}$ applied to the composition of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D}$ applied to $A$ and $j$ and $\operatorname{forget}$ applied to $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D}$ applied to $A$ and $j$ and $\operatorname{isLimitConePost}$ applied to $\operatorname{i'}$ applied to $A$ and $\operatorname{hc}$ applied to $A$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.hii'defMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $A$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Then $\operatorname{hii'}$ applied to $A$ is a homomorphism of $\operatorname{i'}$ applied to $A$ and $\operatorname{i}$ applied to $A$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.idefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Then $\operatorname{i}$ applied to $\mathrm{self}$ is an element of $I$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.i'defMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $A$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Then $\operatorname{i'}$ applied to $A$ is an element of $I$ defined as $\operatorname{choose}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_exists\_index}$ applied to $A$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰DdefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $A$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Then $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D}$ applied to $A$ is an open cover of the action of $D$ and $\operatorname{i'}$ applied to $A$ defined as $\operatorname{bind}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D\_u2080\_}$ applied to $A$ and the function that maps $x_{1}$ to the affine cover of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_D\_u2080\_}$ applied to $A$ and $x_{1}$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D₀defMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰SdefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Then $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_S}$ applied to $\mathrm{self}$ is an open cover of $S$ defined as $\operatorname{proj8}$ applied to $\mathrm{self}$.

AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰XdefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{ExistsHomHomCompEqCompAux}$ applied to $D$, $t$ and $f$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_S}$ applied to $\mathrm{self}$. Then $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_X}$ applied to $\mathrm{self}$ and $i$ is an open cover of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and $\mathrm{AlgebraicGeometry\_\_ExistsHomHomCompEqCompAux\_\_\_u1d4b0\_S}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj10}$ applied to $\mathrm{self}$ and $i$.

AlgebraicGeometry.isLimitOpensConedefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

no wording

English

Let $D$ be a functor of $I$ and the set of schemes. Let $c$ be a cone of $D$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $i$ be an element of $I$. Let $U$ be an open of the action of $D$ and $i$. Then $\operatorname{isLimitOpensCone}$ applied to $D$, $c$, $\mathrm{hc}$, $i$ and $U$ is an element of $\operatorname{IsLimit}$ applied to the open cone of $i$ and $U$.

AlgebraicGeometry.opensConedefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

the open cone of i and U (from the name)

English

Let $D$ be a functor of $I$ and the set of schemes. Let $c$ be a cone of $D$. Let $i$ be an element of $I$. Let $U$ be an open of the action of $D$ and $i$. Then the open cone of $i$ and $U$ is a cone of the open diagram of $i$ and $U$.

AlgebraicGeometry.opensDiagramdefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

the open diagram of i and U (from the name)

English

Let $D$ be a functor of $I$ and the set of schemes. Let $i$ be an element of $I$. Let $U$ be an open of the action of $D$ and $i$. Then the open diagram of $i$ and $U$ is a functor of $\operatorname{Over}$ applied to $i$ and the set of schemes.

AlgebraicGeometry.opensDiagramιdefMathlib.AlgebraicGeometry.AffineTransitionLimit, function or constant

Wording

the open diagram inclusion of i and U (from the name)

English

Let $D$ be a functor of $I$ and the set of schemes. Let $i$ be an element of $I$. Let $U$ be an open of the action of $D$ and $i$. Then the open diagram inclusion of $i$ and $U$ is a homomorphism of the open diagram of $i$ and $U$ and the composition of $\operatorname{forget}$ applied to $i$ and $D$.

Mathlib.AlgebraicGeometry.AlgClosed.Basic

AlgebraicGeometry.pointEquivClosedPointdefMathlib.AlgebraicGeometry.AlgClosed.Basic, function or constant

Wording

the point equivalence closed point of f (from the name)

English

Let $f$ be a homomorphism of $X$ and the spectrum of $\operatorname{of}$ applied to $K$. Then the point equivalence closed point of $f$ is an element of $\EquivMACRoAE {(\SubtypeSet {p}{(\EqtMACRoH {\operatorname{comp} (p , f)}{\operatorname{id} (\operatorname{Spec} (\operatorname{of} (K)))})})}{\operatorname{Elem} (\mathrm{closedPoints} (\operatorname{carrier} (\operatorname{carrier} (\operatorname{toPresheafedSpace} (\operatorname{toSheafedSpace} (\operatorname{toLocallyRingedSpace} (X)))))))}$.

AlgebraicGeometry.pointOfClosedPointdefMathlib.AlgebraicGeometry.AlgClosed.Basic, function or constant

Wording

the point of f and x1 (from the name)

English

Let $f$ be a homomorphism of $X$ and the spectrum of $\operatorname{of}$ applied to $K$. Let $x_{1}$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ such that $\operatorname{singleton}$ applied to $x_{1}$ is closed. Then the point of $f$ and $x_{1}$ is a homomorphism of the spectrum of $\operatorname{of}$ applied to $K$ and $X$ defined as the composition of the induced map of the homomorphism of the residue field isomorphism base of $f$ and $x_{1}$ and $\operatorname{fromSpecResidueField}$ applied to $X$ and $x_{1}$.

AlgebraicGeometry.residueFieldIsoBasedefMathlib.AlgebraicGeometry.AlgClosed.Basic, function or constant

Wording

the residue field isomorphism base of f and x1 (from the name)

English

Let $f$ be a homomorphism of $X$ and the spectrum of $\operatorname{of}$ applied to $K$. Let $x_{1}$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ such that $\operatorname{singleton}$ applied to $x_{1}$ is closed. Then the residue field isomorphism base of $f$ and $x_{1}$ is an isomorphism of the residue field of $X$ and $x_{1}$ and $\operatorname{of}$ applied to $K$ defined as the inverse of $\operatorname{asIso}$ applied to the preimage of the composition of $\operatorname{fromSpecResidueField}$ applied to $X$ and $x_{1}$ and $f$.

Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic

AlgebraicGeometry.AlgebraicCycledefMathlib.AlgebraicGeometry.AlgebraicCycle.Basic, type

Wording

algebraic cycle of X and R (from the name)

English

generation took over the time limit

AlgebraicGeometry.AlgebraicCycle.IsWeilDivisordefMathlib.AlgebraicGeometry.AlgebraicCycle.Basic, predicate

Wording

D is a Weil divisor (from the name)

English

Let $D$ be an algebraic cycle of $X$ and $R$. Then $D$ is a Weil divisor, if the support of $D$ is less than or equal to $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\EqtMACRoH {\operatorname{coheight} (x_{1})}{1}$.

AlgebraicGeometry.AlgebraicCycle.degreedefMathlib.AlgebraicGeometry.AlgebraicCycle.Basic, function or constant

Wording

the degree of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the degree of $f$ is an additive monoid homomorphism of the set of algebraic cycles of $X$ and $R$ and $R$.

AlgebraicGeometry.AlgebraicCycle.mapdefMathlib.AlgebraicGeometry.AlgebraicCycle.Basic, function or constant

Wording

the map of wy and c (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $\mathrm{wx}$ be a function from carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ to elements of $N$. Let $\mathrm{wy}$ be a function from carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ to elements of $N$. Let $c$ be an algebraic cycle of $X$ and $R$. Then the map of $\mathrm{wy}$ and $c$ is an algebraic cycle of $Y$ and $R$ defined as the map of the function that maps $x_{2}$ to $\operatorname{mapCoeff}$ applied to $f$, $\mathrm{wx}$, $\mathrm{wy}$ and $x_{2}$ and $c$.

AlgebraicGeometry.AlgebraicCycle.weilDivisorsdefMathlib.AlgebraicGeometry.AlgebraicCycle.Basic, function or constant

Wording

the Weil divisor of X and R (from the name)

English

Let $X$ be a scheme. Let $R$ be a set. Then the Weil divisor of $X$ and $R$ is an additive subgroup of the set of algebraic cycles of $X$ and $R$ defined as $\operatorname{supported}$ applied to $R$, the universal set and $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\EqtMACRoH {\operatorname{coheight} (x_{1})}{1}$.

Mathlib.AlgebraicGeometry.Artinian

AlgebraicGeometry.IsArtinianSchemeclassMathlib.AlgebraicGeometry.Artinian, predicate

Wording

X is a Artinian scheme (from the name)

English

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

AlgebraicGeometry.IsLocallyArtinianclassMathlib.AlgebraicGeometry.Artinian, predicate

Wording

no wording

English

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

Mathlib.AlgebraicGeometry.Birational.Birational

AlgebraicGeometry.Scheme.BirationaldefMathlib.AlgebraicGeometry.Birational.Birational, predicate

Wording

no wording

English

Let $X$ and $Y$ be schemes. Then $\operatorname{Birational}$ holds for $X$ and $Y$, if $\mathrm{Nonempty}$ holds for the set of partial isomorphisms of $X$ and $Y$.

AlgebraicGeometry.Scheme.Birational.partialIsodefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the partial isomorphism of h (from the name)

English

Assume that $\operatorname{Birational}$ holds for $X$ and $Y$. Then the partial isomorphism of $h$ is a partial isomorphism of $X$ and $Y$ defined as $\operatorname{choice}$ applied to $h$.

AlgebraicGeometry.Scheme.BirationalOverdefMathlib.AlgebraicGeometry.Birational.Birational, predicate

Wording

no wording

English

Let $\mathrm{sX}$ be a homomorphism of $X$ and $S$. Let $\mathrm{sY}$ be a homomorphism of $Y$ and $S$. Then $\operatorname{BirationalOver}$ holds for $\mathrm{sX}$ and $\mathrm{sY}$, if there exists a partial isomorphism $f$ of $X$ and $Y$, such that $\operatorname{IsOver}$ holds for $\mathrm{sX}$, $\mathrm{sY}$ and $f$.

AlgebraicGeometry.Scheme.BirationalOver.partialIsodefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the partial isomorphism of sX and sY (from the name)

English

Let $\mathrm{sX}$ be a homomorphism of $X$ and $S$. Let $\mathrm{sY}$ be a homomorphism of $Y$ and $S$ such that $\operatorname{BirationalOver}$ holds for $\mathrm{sX}$ and $\mathrm{sY}$. Then the partial isomorphism of $\mathrm{sX}$ and $\mathrm{sY}$ is a partial isomorphism of $X$ and $Y$ defined as $\operatorname{choose}$ applied to $h$.

AlgebraicGeometry.Scheme.Hom.partialIsodefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the partial isomorphism of f (from the name)

English

Let $f$ be a homomorphism of $U$ and $X$. Then the partial isomorphism of $f$ is a partial isomorphism of $U$ and $X$.

AlgebraicGeometry.Scheme.IsRationalOverclassMathlib.AlgebraicGeometry.Birational.Birational, predicate

Wording

no wording

English

Let $\mathrm{sX}$ be a homomorphism of $X$ and $S$. Then we can say that $\operatorname{IsRationalOver}$ holds for $\mathrm{sX}$.

AlgebraicGeometry.Scheme.Opens.partialIsoOfDensedefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the partial isomorphism of U and hU (from the name)

English

Let $U$ be a dense open of $X$. Then the partial isomorphism of $U$ and $\mathrm{hU}$ is a partial isomorphism of the scheme of $U$ and $X$.

AlgebraicGeometry.Scheme.PartialIsostructureMathlib.AlgebraicGeometry.Birational.Birational, type

Wording

partial isomorphism of X and Y (from the name)

English

Let $X$ and $Y$ be schemes. Then the partial isomorphisms of $X$ and $Y$ are a basic type.

AlgebraicGeometry.Scheme.PartialIso.IsOverdefMathlib.AlgebraicGeometry.Birational.Birational, predicate

Wording

no wording

English

Let $\mathrm{sX}$ be a homomorphism of $X$ and $S$. Let $\mathrm{sY}$ be a homomorphism of $Y$ and $S$. Let $f$ be a partial isomorphism of $X$ and $Y$. Then $\operatorname{IsOver}$ holds for $\mathrm{sX}$, $\mathrm{sY}$ and $f$, if the composition of the homomorphism of the underlying isomorphism of $f$ and the composition of the inclusion of the target open subscheme of $f$ and $\mathrm{sY}$ is equal to the composition of the inclusion of the source open subscheme of $f$ and $\mathrm{sX}$.

AlgebraicGeometry.Scheme.PartialIso.isodefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the underlying isomorphism of self (from the docstring)

English

Let $\mathrm{self}$ be a partial isomorphism of $X$ and $Y$. Then the underlying isomorphism of $\mathrm{self}$ is an isomorphism of the scheme of the source open subscheme of $\mathrm{self}$ and the scheme of the target open subscheme of $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.PartialIso.ofIsodefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the partial isomorphism of f (from the name)

English

Let $f$ be an isomorphism of $X$ and $Y$. Then the partial isomorphism of $f$ is a partial isomorphism of $X$ and $Y$.

AlgebraicGeometry.Scheme.PartialIso.refldefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the identity of X (from the name)

English

Let $X$ be a scheme. Then the identity of $X$ is a partial isomorphism of $X$ and $X$.

AlgebraicGeometry.Scheme.PartialIso.restrictSourcedefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

no wording

English

Let $f$ be a partial isomorphism of $X$ and $Y$. Let $U$ be an open of $X$ such that $U$ is dense and $U$ is less than or equal to the source open subscheme of $f$. Then $\operatorname{restrictSource}$ applied to $f$, $U$, $\mathrm{hU}$ and $\mathrm{hU'}$ is a partial isomorphism of $X$ and $Y$.

AlgebraicGeometry.Scheme.PartialIso.restrictTargetdefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

no wording

English

Let $f$ be a partial isomorphism of $X$ and $Y$. Let $U$ be an open of $Y$ such that $U$ is dense and $U$ is less than or equal to the target open subscheme of $f$. Then $\operatorname{restrictTarget}$ applied to $f$, $U$, $\mathrm{hU}$ and $\mathrm{hU'}$ is a partial isomorphism of $X$ and $Y$ defined as the inverse of $\operatorname{restrictSource}$ applied to the inverse of $f$, $U$, $\mathrm{hU}$ and $\mathrm{hU'}$.

AlgebraicGeometry.Scheme.PartialIso.sourcedefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the source open subscheme of self (from the docstring)

English

Let $\mathrm{self}$ be a partial isomorphism of $X$ and $Y$. Then the source open subscheme of $\mathrm{self}$ is an open of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.PartialIso.symmdefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the inverse of f (from the docstring)

English

Let $f$ be a partial isomorphism of $X$ and $Y$. Then the inverse of $f$ is a partial isomorphism of $Y$ and $X$ defined as $\operatorname{mk}$ applied to the target open subscheme of $f$, $\mathrm{AlgebraicGeometry\_\_Scheme\_\_PartialIso\_\_dense\_target}$ applied to $f$, the source open subscheme of $f$, $\mathrm{AlgebraicGeometry\_\_Scheme\_\_PartialIso\_\_dense\_source}$ applied to $f$ and the inverse of the underlying isomorphism of $f$.

AlgebraicGeometry.Scheme.PartialIso.targetdefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the target open subscheme of self (from the docstring)

English

Let $\mathrm{self}$ be a partial isomorphism of $X$ and $Y$. Then the target open subscheme of $\mathrm{self}$ is an open of $Y$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.PartialIso.toPartialMapdefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the underlying partial map of f (from the docstring)

English

Let $f$ be a partial isomorphism of $X$ and $Y$. Then the underlying partial map of $f$ is a partial map of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the source open subscheme of $f$, $\mathrm{AlgebraicGeometry\_\_Scheme\_\_PartialIso\_\_dense\_source}$ applied to $f$ and the composition of the homomorphism of the underlying isomorphism of $f$ and the inclusion of the target open subscheme of $f$.

AlgebraicGeometry.Scheme.PartialIso.toRationalMapdefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the underlying rational map of f (from the docstring)

English

Let $f$ be a partial isomorphism of $X$ and $Y$. Then the underlying rational map of $f$ is a rational map of $X$ and $Y$ defined as the rational map of the underlying partial map of $f$.

AlgebraicGeometry.Scheme.PartialIso.transdefMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a partial isomorphism of $X$ and $Y$. Let $g$ be a partial isomorphism of $Y$ and $Z$. Then the composition of $f$ and $g$ is a partial isomorphism of $X$ and $Z$.

AlgebraicGeometry.Scheme.PartialIso.trans'defMathlib.AlgebraicGeometry.Birational.Birational, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a partial isomorphism of $X$ and $Y$. Let $g$ be a partial isomorphism of $Y$ and $Z$ such that the target open subscheme of $f$ is equal to the source open subscheme of $g$. Then the composition of $f$ and $g$ is a partial isomorphism of $X$ and $Z$ defined as $\operatorname{mk}$ applied to the source open subscheme of $f$, $\mathrm{AlgebraicGeometry\_\_Scheme\_\_PartialIso\_\_dense\_source}$ applied to $f$, the target open subscheme of $g$, $\mathrm{AlgebraicGeometry\_\_Scheme\_\_PartialIso\_\_dense\_target}$ applied to $g$ and the composition of the underlying isomorphism of $f$ and the composition of the isomorphism of $Y$ and $e$ and the underlying isomorphism of $g$.

Mathlib.AlgebraicGeometry.Birational.Composition

AlgebraicGeometry.Scheme.PartialMap.compdefMathlib.AlgebraicGeometry.Birational.Composition, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a partial map of $X$ and $Y$. Let $g$ be a partial map of $Y$ and $Z$. Then the composition of $f$ and $g$ is a partial map of $X$ and $Z$.

AlgebraicGeometry.Scheme.RationalMap.compdefMathlib.AlgebraicGeometry.Birational.Composition, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a rational map of $X$ and $Y$. Let $g$ be a rational map of $Y$ and $Z$. Then the composition of $f$ and $g$ is a rational map of $X$ and $Z$.

Mathlib.AlgebraicGeometry.Birational.Dominant

AlgebraicGeometry.Scheme.RationalMap.IsDominantclassMathlib.AlgebraicGeometry.Birational.Dominant, predicate

Wording

f is dominant (from the docstring)

English

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

Mathlib.AlgebraicGeometry.Birational.RationalMap

AlgebraicGeometry.Scheme.Hom.toPartialMapdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the partial map of f (from the name)

English

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

AlgebraicGeometry.Scheme.Hom.toRationalMapdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the rational map of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the rational map of $f$ is a rational map of $X$ and $Y$ defined as the rational map of the partial map of $f$.

AlgebraicGeometry.Scheme.PartialMapstructureMathlib.AlgebraicGeometry.Birational.RationalMap, type

Wording

partial map of X and Y (from the name)

English

Let $X$ and $Y$ be schemes. Then the partial maps of $X$ and $Y$ are a basic type.

AlgebraicGeometry.Scheme.PartialMap.IsOverdefMathlib.AlgebraicGeometry.Birational.RationalMap, predicate

Wording

no wording

English

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

AlgebraicGeometry.Scheme.PartialMap.compHomdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the composition of f and g (from the docstring)

English

Let $f$ be a partial map of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the composition of $f$ and $g$ is a partial map of $X$ and $Z$ defined as $\operatorname{mk}$ applied to the domain of definition of $f$, $\mathrm{AlgebraicGeometry\_\_Scheme\_\_PartialMap\_\_dense\_domain}$ applied to $f$ and the composition of the homomorphism of $f$ and $g$.

AlgebraicGeometry.Scheme.PartialMap.domaindefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the domain of definition of self (from the docstring)

English

Let $\mathrm{self}$ be a partial map of $X$ and $Y$. Then the domain of definition of $\mathrm{self}$ is an open of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.PartialMap.equivdefMathlib.AlgebraicGeometry.Birational.RationalMap, predicate

Wording

no wording

English

Let $f$ and $g$ be partial maps of $X$ and $Y$. Then $\operatorname{equiv}$ holds for $f$ and $g$, if there exists an open $W$ of $X$, such that there exists an element $\mathrm{hW}$ of $\mathrm{Dense}$ applied to $W$, such that there exists an element $\mathrm{hWl}$ of $\mathrm{Leq}$ applied to $W$ and the domain of definition of $f$, such that there exists an element $\mathrm{hWr}$ of $\mathrm{Leq}$ applied to $W$ and the domain of definition of $g$, such that the homomorphism of $\operatorname{restrict}$ applied to $f$, $W$, $\mathrm{hW}$ and $\mathrm{hWl}$ is equal to the homomorphism of $\operatorname{restrict}$ applied to $g$, $W$, $\mathrm{hW}$ and $\mathrm{hWr}$.

AlgebraicGeometry.Scheme.PartialMap.fromFunctionFielddefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

no wording

English

Let $f$ be a partial map of $X$ and $Y$. Then $\operatorname{fromFunctionField}$ applied to $f$ is a homomorphism of the spectrum of the function field of $X$ and $Y$.

AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMemdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

no wording

English

Let $f$ be a partial map of $X$ and $Y$ such that $x$ is an element of the domain of definition of $f$. Then $\operatorname{fromSpecStalkOfMem}$ applied to $f$ and $\mathrm{hx}$ is a homomorphism of the spectrum of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x$ and $Y$ defined as the composition of $\operatorname{fromSpecStalkOfMem}$ applied to the domain of definition of $f$, $x$ and $\mathrm{hx}$ and the homomorphism of $f$.

AlgebraicGeometry.Scheme.PartialMap.homdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a partial map of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the scheme of the domain of definition of $\mathrm{self}$ and $Y$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.PartialMap.iddefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the identity partial map of X (from the docstring)

English

Let $X$ be a scheme. Then the identity partial map of $X$ is a partial map of $X$ and $X$ defined as the partial map of the identity morphism of $X$.

AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalkdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the partial map of sY and x1 (from the name)

English

Let $\mathrm{sX}$ be a homomorphism of $X$ and $S$. Let $\mathrm{sY}$ be a homomorphism of $Y$ and $S$. Let $x_{1}$ be a homomorphism of the spectrum of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x$ and $Y$ such that the composition of $x_{1}$ and $\mathrm{sY}$ is equal to the composition of $\operatorname{fromSpecStalk}$ applied to $X$ and $x$ and $\mathrm{sX}$. Then the partial map of $\mathrm{sY}$ and $x_{1}$ is a partial map of $X$ and $Y$.

AlgebraicGeometry.Scheme.PartialMap.restrictdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

no wording

English

Let $f$ be a partial map of $X$ and $Y$. Let $U$ be an open of $X$ such that $U$ is dense and $U$ is less than or equal to the domain of definition of $f$. Then $\operatorname{restrict}$ applied to $f$, $U$, $\mathrm{hU}$ and $\mathrm{hU'}$ is a partial map of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $U$, $\mathrm{hU}$ and the composition of the homomorphism of $X$ and $\mathrm{hU'}$ and the homomorphism of $f$.

AlgebraicGeometry.Scheme.PartialMap.toRationalMapdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the rational map of f (from the name)

English

Let $f$ be a partial map of $X$ and $Y$. Then the rational map of $f$ is a rational map of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{inferInstance}$ and $f$.

AlgebraicGeometry.Scheme.RationalMapdefMathlib.AlgebraicGeometry.Birational.RationalMap, type

Wording

rational map of X and Y (from the name)

English

Let $X$ and $Y$ be schemes. Then a rational map of $X$ and $Y$ is an element of the function that maps $X$ and $Y$ to $\mathrm{Quotient}$ applied to $\mathrm{inferInstance}$.

AlgebraicGeometry.Scheme.RationalMap.IsOverclassMathlib.AlgebraicGeometry.Birational.RationalMap, predicate

Wording

no wording

English

Let $S$ be a scheme. Let $f$ be a rational map of $X$ and $Y$. Then we can say that $\operatorname{IsOver}$ holds for $S$ and $f$.

AlgebraicGeometry.Scheme.RationalMap.compHomdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the composition of f and g (from the docstring)

English

Let $f$ be a rational map of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the composition of $f$ and $g$ is a rational map of $X$ and $Z$.

AlgebraicGeometry.Scheme.RationalMap.domaindefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the domain of definition of f (from the docstring)

English

Let $f$ be a rational map of $X$ and $Y$. Then the domain of definition of $f$ is an open of $X$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $x$ to the proposition that there exists a partial map $g$ of $X$ and $Y$, such that there exists an element $h$ of $\mathrm{Eqt}$ applied to the rational map of $g$ and $f$, such that the domain of definition of $g$ is equal to $x$.

AlgebraicGeometry.Scheme.RationalMap.equivFunctionFielddefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the equivalence function field of sX and sY (from the name)

English

Let $\mathrm{sX}$ be a homomorphism of $X$ and $S$. Let $\mathrm{sY}$ be a homomorphism of $Y$ and $S$. Then the equivalence function field of $\mathrm{sX}$ and $\mathrm{sY}$ is an element of $\EquivMACRoAE {(\SubtypeSet {f}{(\EqtMACRoH {\operatorname{comp} (f , \mathrm{sY})}{\operatorname{comp} (\operatorname{fromSpecStalk} (X , \mathrm{genericPoint} (\operatorname{carrier} (\operatorname{carrier} (\operatorname{toPresheafedSpace} (\operatorname{toSheafedSpace} (\operatorname{toLocallyRingedSpace} (X))))))), \mathrm{sX})})})}{(\SubtypeSet {f_{1}}{(\EqtMACRoH {\operatorname{compHom} (f_{1} , \mathrm{sY})}{\operatorname{toRationalMap} (\mathrm{sX})})})}$.

AlgebraicGeometry.Scheme.RationalMap.equivFunctionFieldOverdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

no wording

English

$\operatorname{equivFunctionFieldOver}$ is an equivalence from $\SubtypeSet {f}{\operatorname{IsOver} (f , S)}$ to $\SubtypeSet {f_{1}}{\operatorname{IsOver} (S , f_{1})}$.

AlgebraicGeometry.Scheme.RationalMap.fromFunctionFielddefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

no wording

English

Let $f$ be a rational map of $X$ and $Y$. Then $\operatorname{fromFunctionField}$ applied to $f$ is a homomorphism of the spectrum of the function field of $X$ and $Y$.

AlgebraicGeometry.Scheme.RationalMap.iddefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the identity rational map of X (from the docstring)

English

Let $X$ be a scheme. Then the identity rational map of $X$ is a rational map of $X$ and $X$ defined as the rational map of the identity partial map of $X$.

AlgebraicGeometry.Scheme.RationalMap.ofFunctionFielddefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the rational map of sY and f (from the name)

English

Let $\mathrm{sX}$ be a homomorphism of $X$ and $S$. Let $\mathrm{sY}$ be a homomorphism of $Y$ and $S$. Let $f$ be a homomorphism of the spectrum of the function field of $X$ and $Y$ such that the composition of $f$ and $\mathrm{sY}$ is equal to the composition of $\operatorname{fromSpecStalk}$ applied to $X$ and the generic point of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\mathrm{sX}$. Then the rational map of $\mathrm{sY}$ and $f$ is a rational map of $X$ and $Y$ defined as the rational map of the partial map of $\mathrm{sY}$ and $f$.

AlgebraicGeometry.Scheme.RationalMap.openCoverDomaindefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the open cover of the domain of f (from the docstring)

English

Let $f$ be a rational map of $X$ and $Y$. Then the open cover of the domain of $f$ is an open cover of the scheme of the domain of definition of $f$.

AlgebraicGeometry.Scheme.RationalMap.representativedefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the representative of f (from the name)

English

Let $f$ be a rational map of $X$ and $Y$. Then the representative of $f$ is a partial map of $X$ and $Y$ defined as $\operatorname{choose}$ applied to $\mathrm{AlgebraicGeometry\_\_Scheme\_\_RationalMap\_\_exists\_rep}$ applied to $f$.

AlgebraicGeometry.Scheme.RationalMap.toPartialMapdefMathlib.AlgebraicGeometry.Birational.RationalMap, function or constant

Wording

the partial map of f (from the name)

English

Let $f$ be a rational map of $X$ and $Y$. Then the partial map of $f$ is a partial map of $X$ and $Y$.

Mathlib.AlgebraicGeometry.ColimitsOver

AlgebraicGeometry.Scheme.Cover.ColimitGluingDatastructureMathlib.AlgebraicGeometry.ColimitsOver, type

Wording

colimit gluing data of D and x1 (from the name)

English

Let $D$ be a functor of $J$ and $\operatorname{Over}$ applied to $P$, the top and $S$. Let $x_{1}$ be an open cover of $S$. Then the colimit gluing data of $D$ and $x_{1}$ are a basic type.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.coconedefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

the cocone of self and i (from the name)

English

Let $\mathrm{self}$ be a colimit gluing data of $D$ and $x_{1}$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$. Then the cocone of $\mathrm{self}$ and $i$ is a cocone of the composition of $D$ and the pullback of the top and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functordefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

the functor of d (from the name)

English

Let $d$ be a colimit gluing data of $D$ and $x_{1}$. Then the functor of $d$ is a functor of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and the set of schemes.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.glueddefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

no wording

English

Let $d$ be a colimit gluing data of $D$ and $x_{1}$. Then $\operatorname{glued}$ applied to $d$ is an element of $\operatorname{Over}$ applied to $P$, the top and $S$.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCoconedefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

the glued cocone of d (from the name)

English

Let $d$ be a colimit gluing data of $D$ and $x_{1}$. Then the glued cocone of $d$ is a cocone of $D$.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimitdefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a colimit gluing data of $D$ and $x_{1}$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$. Then $\operatorname{isColimit}$ applied to $\mathrm{self}$ and $i$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $\mathrm{self}$ and $i$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimitGluedCoconedefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

the glued cocone of d (from the docstring)

English

Let $d$ be a colimit gluing data of $D$ and $x_{1}$. Then the glued cocone of $d$ is an element of $\operatorname{IsColimit}$ applied to the glued cocone of $d$.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIsodefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

the pullback glued isomorphism of d and i (from the name)

English

Let $d$ be a colimit gluing data of $D$ and $x_{1}$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$. Then the pullback glued isomorphism of $d$ and $i$ is an isomorphism of the action of the pullback of the top and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $i$ and $\operatorname{glued}$ applied to $d$ and $\operatorname{pt}$ applied to the cocone of $d$ and $i$.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingDatadefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

the relative gluing data of d (from the name)

English

Let $d$ be a colimit gluing data of $D$ and $x_{1}$. Then the relative gluing data of $d$ is a relative gluing data of $x_{1}$.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transdefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

the composition of d and hij (from the name)

English

Let $d$ be a colimit gluing data of $D$ and $x_{1}$. Let $\mathrm{hij}$ be a homomorphism of $i$ and $j$. Then the composition of $d$ and $\mathrm{hij}$ is a homomorphism of the composition of $D$ and the composition of the pullback of the top and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $i$ and the map of the top and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Cover\_\_ColimitGluingData\_\_prop\_trans}$ applied to $d$ and $\mathrm{hij}$ and the composition of $D$ and the pullback of the top and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $j$.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCoconedefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

the transition cocone of d and hij (from the name)

English

Let $d$ be a colimit gluing data of $D$ and $x_{1}$. Let $\mathrm{hij}$ be a homomorphism of $i$ and $j$. Then the transition cocone of $d$ and $\mathrm{hij}$ is a cocone of the composition of $D$ and the composition of the pullback of the top and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $i$ and the map of the top and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Cover\_\_ColimitGluingData\_\_prop\_trans}$ applied to $d$ and $\mathrm{hij}$ defined as the action of the precomposition of the composition of $d$ and $\mathrm{hij}$ and the cocone of $d$ and $j$.

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMapdefMathlib.AlgebraicGeometry.ColimitsOver, function or constant

Wording

the transition map of d and hij (from the name)

English

Let $d$ be a colimit gluing data of $D$ and $x_{1}$. Let $\mathrm{hij}$ be a homomorphism of $i$ and $j$. Then the transition map of $d$ and $\mathrm{hij}$ is a homomorphism of the action of the map of the top and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Cover\_\_ColimitGluingData\_\_prop\_trans}$ applied to $d$ and $\mathrm{hij}$ and $\operatorname{pt}$ applied to the cocone of $d$ and $i$ and $\operatorname{pt}$ applied to the cocone of $d$ and $j$ defined as $\operatorname{desc}$ applied to $\operatorname{isColimitOfPreserves}$ applied to the map of the top and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Cover\_\_ColimitGluingData\_\_prop\_trans}$ applied to $d$ and $\mathrm{hij}$ and $\operatorname{isColimit}$ applied to $d$ and $i$ and the transition cocone of $d$ and $\mathrm{hij}$.

Mathlib.AlgebraicGeometry.Cover.Directed

AlgebraicGeometry.Scheme.Cover.LocallyDirectedclassMathlib.AlgebraicGeometry.Cover.Directed, predicate

Wording

x is locally directed (from the name)

English

generation took over the time limit

AlgebraicGeometry.Scheme.Cover.LocallyDirected.transdefMathlib.AlgebraicGeometry.Cover.Directed, function or constant

Wording

the composition of hij (from the name)

English

Let $\mathrm{hij}$ be a homomorphism of $i$ and $j$. Then the composition of $\mathrm{hij}$ is a homomorphism of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $\mathrm{hij}$.

AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirecteddefMathlib.AlgebraicGeometry.Cover.Directed, function or constant

Wording

the canonical cocone with point of x (from the docstring)

English

generation took over the time limit

AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirecteddefMathlib.AlgebraicGeometry.Cover.Directed, function or constant

Wording

the canonical diagram induced by a locally directed cover of x (from the docstring)

English

generation took over the time limit

AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirectedHomBasedefMathlib.AlgebraicGeometry.Cover.Directed, function or constant

Wording

the functor of x (from the name)

English

generation took over the time limit

AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirecteddefMathlib.AlgebraicGeometry.Cover.Directed, function or constant

Wording

the intersection of i and j (from the name)

English

Let $x$ be a cover of the precoverage of $P$ and $X$. Let $i$ and $j$ be elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$. Then the intersection of $i$ and $j$ is a cover of the precoverage of $P$ and the pullback of $\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.Cover.transdefMathlib.AlgebraicGeometry.Cover.Directed, function or constant

Wording

the composition of x and hij (from the name)

English

Let $x$ be a cover of the precoverage of $P$ and $X$. Let $\mathrm{hij}$ be a homomorphism of $i$ and $j$. Then the composition of $x$ and $\mathrm{hij}$ is a homomorphism of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$ defined as the composition of $\mathrm{hij}$.

AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirecteddefMathlib.AlgebraicGeometry.Cover.Directed, function or constant

Wording

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

English

Let $x$ be an open cover of $X$. Let $g$ be a function from elements $i_{1}$ 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 $i_{1}$ and $Y$ such that for all elements $i$ and $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$, for all homomorphisms $\mathrm{hij}$ of $i$ and $j$, the composition of the composition of $x$ and $\mathrm{hij}$ and $g$ applied to $j$ is equal to $g$ applied to $i$. Then the glue morphism of $x$ and $i_{1}$ is a homomorphism of $X$ and $Y$.

AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirecteddefMathlib.AlgebraicGeometry.Cover.Directed, function or constant

Wording

no wording

English

Let $x$ be an open cover of the left of $X$. Let $g$ be a function from elements $i_{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 $i_{2}$ and the left of $Y$ such that for all elements $i_{1}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$, for all elements $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$, for all homomorphisms $\mathrm{hij}$ of $i_{1}$ and $j$, the composition of the composition of $x$ and $\mathrm{hij}$ and $g$ applied to $j$ is equal to $g$ applied to $i_{1}$ and for all elements $i$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$, the composition of $g$ applied to $i$ and the homomorphism of $Y$ is equal to the composition of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ and the homomorphism of $X$. Then $\operatorname{glueMorphismsOverOfLocallyDirected}$ applied to $x$, $i_{2}$, $g$, $h$ and $w$ is a homomorphism of $X$ and $Y$.

AlgebraicGeometry.Scheme.OpenCover.isColimitCoconeOfLocallyDirecteddefMathlib.AlgebraicGeometry.Cover.Directed, function or constant

Wording

no wording

English

Let $x$ be an open cover of $X$. Then $\operatorname{isColimitCoconeOfLocallyDirected}$ applied to $x$ is an element of $\operatorname{IsColimit}$ applied to the canonical cocone with point of $x$.

AlgebraicGeometry.Scheme.directedAffineCoverdefMathlib.AlgebraicGeometry.Cover.Directed, function or constant

Wording

the directed affine cover of X (from the name)

English

Let $X$ be a scheme. Then the directed affine cover of $X$ is an open cover of $X$.

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

AlgebraicGeometry.Scheme.AffineCoverstructureMathlib.AlgebraicGeometry.Cover.MorphismProperty, type

Wording

affine cover of P and S (from the name)

English

Let $P$ be a morphism property of the set of schemes. Let $S$ be a scheme. Then the affine covers of $P$ and $S$ are a basic type.

AlgebraicGeometry.Scheme.AffineCover.I₀defMathlib.AlgebraicGeometry.Cover.MorphismProperty, type

Wording

no wording

English

Let $\mathrm{self}$ be an affine cover of $P$ and $S$. Then an element of $\mathrm{AlgebraicGeometry\_\_Scheme\_\_AffineCover\_\_I\_u2080\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

AlgebraicGeometry.Scheme.AffineCover.XdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an affine cover of $P$ and $S$. Let $j$ be an element of $\mathrm{AlgebraicGeometry\_\_Scheme\_\_AffineCover\_\_I\_u2080\_}$ applied to $\mathrm{self}$. Then $\operatorname{X}$ applied to $\mathrm{self}$ and $j$ is a category of commutative rings defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $j$.

AlgebraicGeometry.Scheme.AffineCover.coverdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

the cover of x (from the name)

English

Let $x$ be an affine cover of $P$ and $X$. Then the cover of $x$ is a cover of the precoverage of $P$ and $X$.

AlgebraicGeometry.Scheme.AffineCover.fdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an affine cover of $P$ and $S$. Let $j$ be an element of $\mathrm{AlgebraicGeometry\_\_Scheme\_\_AffineCover\_\_I\_u2080\_}$ applied to $\mathrm{self}$. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $j$ is a homomorphism of the spectrum of $\operatorname{X}$ applied to $\mathrm{self}$ and $j$ and $S$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $j$.

AlgebraicGeometry.Scheme.AffineCover.idxdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

the index of self and x (from the name)

English

Let $\mathrm{self}$ be an affine cover of $P$ and $S$. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $S$. Then the index of $\mathrm{self}$ and $x$ is an element of $\mathrm{AlgebraicGeometry\_\_Scheme\_\_AffineCover\_\_I\_u2080\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x$.

AlgebraicGeometry.Scheme.CoverdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, type

Wording

cover of K and S (from the name)

English

Let $K$ be a precoverage of the set of schemes. Let $S$ be a scheme. Then a cover of $K$ and $S$ is an element of the function that maps $K$ and $S$ to the set of zero hypercovers of $K$ and $S$.

AlgebraicGeometry.Scheme.Cover.HomdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, type

Wording

homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be covers of $K$ and $X$. Then a homomorphism of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of homomorphisms of $x$ and $x_{1}$.

AlgebraicGeometry.Scheme.Cover.adddefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

the sum of x and f (from the name)

English

Let $x$ be a cover of the precoverage of $P$ and $X$. Let $f$ be a homomorphism of $Y$ and $X$ such that $\mathrm{autoParam}$ holds for $P$ applied to $Y$, $X$ and $f$ and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Cover\_\_add\_\_\_auto\_1}$. Then the sum of $x$ and $f$ is a cover of the precoverage of $P$ and $X$.

AlgebraicGeometry.Scheme.Cover.changePropdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

no wording

English

Let $x$ be a cover of $K$ and $X$ such that for all elements $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$, $Q$ holds for $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$, $X$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$. Then $\operatorname{changeProp}$ applied to $x$ and $h_{1}$ is a cover of the precoverage of $Q$ and $X$.

AlgebraicGeometry.Scheme.Cover.copydefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

the copy of i2 and x1 (from the name)

English

Let $x$ be a cover of the precoverage of $P$ and $X$. Let $J$ be a set. Let $\mathrm{obj}$ be a function from elements of $J$ to schemes. Let $\mathrm{map}$ be a function from elements $i_{2}$ of $J$ to homomorphisms of $\mathrm{obj}$ applied to $i_{2}$ and $X$. Let $x_{1}$ be an element of $\EquivMACRoAE {J}{\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_} (\operatorname{toPreZeroHypercover} (x))}$. Let $x_{2}$ be a function from elements $i_{1}$ of $J$ to isomorphisms of $\mathrm{obj}$ applied to $i_{1}$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $x_{1}$ applied to $i_{1}$ such that for all elements $i$ of $J$, $\mathrm{map}$ applied to $i$ is equal to the composition of the homomorphism of $x_{2}$ applied to $i$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $x_{1}$ applied to $i$. Then the copy of $\mathrm{map}$ and $x_{1}$ is a cover of the precoverage of $P$ and $X$.

AlgebraicGeometry.Scheme.Cover.idxdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

the index of x and x1 (from the name)

English

Let $x$ be a cover of $K$ and $X$. Let $x_{1}$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the index of $x$ and $x_{1}$ is an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ defined as $\operatorname{choose}$ applied to $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Cover\_\_exists\_eq}$ applied to $x$ and $x_{1}$.

AlgebraicGeometry.Scheme.Cover.mkOfCoversdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

no wording

English

Let $J$ be a set. Let $\mathrm{obj}$ be a function from elements of $J$ to schemes. Let $\mathrm{map}$ be a function from elements $j_{2}$ of $J$ to homomorphisms of $\mathrm{obj}$ applied to $j_{2}$ and $X$ such that for all carriers $x$ of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$, there exists an element $j_{1}$ of $J$ such that there exists a carrier $y$ of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $\mathrm{obj}$ applied to $j_{1}$ such that $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $\mathrm{map}$ applied to $j_{1}$ and $y$ is equal to $x$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $j$ of $J$, $P$ holds for $\mathrm{obj}$ applied to $j$, $X$ and $\mathrm{map}$ applied to $j$ and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Cover\_\_mkOfCovers\_\_\_auto\_1}$. Then $\operatorname{mkOfCovers}$ applied to $J$, $\mathrm{obj}$, $j_{2}$, $\mathrm{map}$, $\mathrm{covers}$ and $\mathrm{map\_prop}$ is a cover of the precoverage of $P$ and $X$.

AlgebraicGeometry.Scheme.Cover.pullbackHomdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

the pullback homomorphism of f and i (from the name)

English

Let $x$ be a cover of the precoverage of $P$ and $X$. Let $f$ be a homomorphism of $W$ and $X$. Let $i$ be an element of $\operatorname{proj0}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$. Then the pullback homomorphism of $f$ and $i$ is a homomorphism of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and $x$ and $i$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$ defined as the second projection of the pullback of $f$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $i$.

AlgebraicGeometry.Scheme.Cover.pushforwardIsodefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

the pushforward isomorphism of x and f (from the name)

English

Let $x$ be a cover of the precoverage of $P$ and $X$. Let $f$ be a homomorphism of $X$ and $Y$. Then the pushforward isomorphism of $x$ and $f$ is a cover of the precoverage of $P$ and $Y$.

AlgebraicGeometry.Scheme.Cover.uliftdefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

the lift of x (from the name)

English

Let $x$ be a cover of the precoverage of $P$ and $X$. Then the lift of $x$ is a cover of the precoverage of $P$ and $X$.

AlgebraicGeometry.Scheme.JointlySurjectiveclassMathlib.AlgebraicGeometry.Cover.MorphismProperty, predicate

Wording

K is jointly surjective (from the name)

English

generation took over the time limit

AlgebraicGeometry.Scheme.coverOfIsIsodefMathlib.AlgebraicGeometry.Cover.MorphismProperty, function or constant

Wording

the cover of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the cover of $f$ is a cover of the precoverage of $P$ and $Y$.

Mathlib.AlgebraicGeometry.Cover.Open

AlgebraicGeometry.Scheme.AffineOpenCoverdefMathlib.AlgebraicGeometry.Cover.Open, type

Wording

affine open cover of X (from the name)

English

Let $X$ be a scheme. Then an affine open cover of $X$ is an element of the function that maps $X$ to the set of affine covers of $\operatorname{IsOpenImmersion}$ and $X$.

AlgebraicGeometry.Scheme.AffineOpenCover.openCoverdefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

the open cover of x (from the name)

English

Let $x$ be an affine open cover of $X$. Then the open cover of $x$ is an open cover of $X$ defined as the cover of $x$.

AlgebraicGeometry.Scheme.OpenCoverdefMathlib.AlgebraicGeometry.Cover.Open, type

Wording

open cover of X (from the name)

English

Let $X$ be a scheme. Then an open cover of $X$ is an element of the function that maps $X$ to the set of covers of the precoverage of $\operatorname{IsOpenImmersion}$ and $X$.

AlgebraicGeometry.Scheme.OpenCover.affineRefinementdefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

the affine refinement of x (from the name)

English

Let $x$ be an open cover of $X$. Then the affine refinement of $x$ is an affine open cover of $X$.

AlgebraicGeometry.Scheme.OpenCover.finiteSubcoverdefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

no wording

English

Let $x$ be an open cover of $X$. Then $\operatorname{finiteSubcover}$ applied to $x$ is an open cover of $X$.

AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinementdefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

no wording

English

Let $x$ be an open cover of $X$. Then $\operatorname{fromAffineRefinement}$ applied to $x$ is a homomorphism of the open cover of the affine refinement of $x$ and $x$.

AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIsodefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

the pullback cover affine refinement object isomorphism of x and i (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be an open cover of $Y$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and the open cover of the affine refinement of $x$. Then the pullback cover affine refinement object isomorphism of $x$ and $i$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of $f$ and the open cover of the affine refinement of $x$ and $i$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the pullback of the pullback homomorphism of $f$ and $\operatorname{fst}$ applied to $i$ and the affine cover of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$.

AlgebraicGeometry.Scheme.affineBasisCoverdefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

the affine basis cover of X (from the name)

English

Let $X$ be a scheme. Then the affine basis cover of $X$ is an open cover of $X$.

AlgebraicGeometry.Scheme.affineBasisCoverOfAffinedefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

the affine basis cover of R (from the name)

English

Let $R$ be a category of commutative rings. Then the affine basis cover of $R$ is an open cover of the spectrum of $R$.

AlgebraicGeometry.Scheme.affineBasisCoverRingdefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

the coordinate ring of X and i (from the docstring)

English

Let $X$ be a scheme. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to the affine basis cover of $X$. Then the coordinate ring of $X$ and $i$ is a category of commutative rings defined as $\operatorname{of}$ applied to $\operatorname{Away}$ applied to $\operatorname{snd}$ applied to $i$.

AlgebraicGeometry.Scheme.affineCoverdefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

the affine cover of X (from the docstring)

English

Let $X$ be a scheme. Then the affine cover of $X$ is an open cover of $X$.

AlgebraicGeometry.Scheme.affineOpenCoverdefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

the affine open cover of X (from the name)

English

Let $X$ be a scheme. Then the affine open cover of $X$ is an affine open cover of $X$.

AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTopdefMathlib.AlgebraicGeometry.Cover.Open, function or constant

Wording

the affine open cover of s and hs (from the name)

English

Let $s$ be a function from elements of $x$ to carriers of $R$ such that the span of the range of $s$ is equal to the top. Then the affine open cover of $s$ and $\mathrm{hs}$ is an affine open cover of the spectrum of $R$.

Mathlib.AlgebraicGeometry.Cover.Over

AlgebraicGeometry.Scheme.Cover.OverclassMathlib.AlgebraicGeometry.Cover.Over, predicate

Wording

no wording

English

Let $S$ be a scheme. Let $x_{1}$ be a cover of the precoverage of $P$ and $X$. Then we can say that $\operatorname{Over}$ holds for $S$ and $x_{1}$.

AlgebraicGeometry.Scheme.Cover.pullbackCoverOverdefMathlib.AlgebraicGeometry.Cover.Over, function or constant

Wording

no wording

English

Let $S$ be a scheme. Let $x$ be a cover of the precoverage of $P$ and $X$. Let $f$ be a homomorphism of $W$ and $X$. Then $\operatorname{pullbackCoverOver}$ applied to $S$, $x$ and $f$ is a cover of the precoverage of $P$ and $W$.

AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'defMathlib.AlgebraicGeometry.Cover.Over, function or constant

Wording

no wording

English

Let $S$ be a scheme. Let $x$ be a cover of the precoverage of $P$ and $X$. Let $f$ be a homomorphism of $W$ and $X$. Then $\operatorname{pullbackCoverOver'}$ applied to $S$, $x$ and $f$ is a cover of the precoverage of $P$ and $W$.

AlgebraicGeometry.Scheme.Cover.pullbackCoverOverPropdefMathlib.AlgebraicGeometry.Cover.Over, function or constant

Wording

no wording

English

Let $S$ be a scheme. Let $x$ be a cover of the precoverage of $P$ and $X$. Let $f$ be a homomorphism of $W$ and $X$. Assume that $Q$ holds for $X$, $S$ and $\operatorname{over}$ applied to $X$, $S$ and $\mathrm{inferInstance}$. Assume that $Q$ holds for $W$, $S$ and $\operatorname{over}$ applied to $W$, $S$ and $\mathrm{inferInstance}$. Assume that for all elements $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$, $Q$ holds for $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$, $S$ and $\operatorname{over}$ applied to $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$, $S$ and $\mathrm{inferInstance}$. Then $\operatorname{pullbackCoverOverProp}$ applied to $S$, $x$, $f$, $\mathrm{hX}$, $\mathrm{hW}$ and $\mathrm{hQ}$ is a cover of the precoverage of $P$ and $W$.

AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'defMathlib.AlgebraicGeometry.Cover.Over, function or constant

Wording

no wording

English

Let $S$ be a scheme. Let $x$ be a cover of the precoverage of $P$ and $X$. Let $f$ be a homomorphism of $W$ and $X$. Assume that $Q$ holds for $X$, $S$ and $\operatorname{over}$ applied to $X$, $S$ and $\mathrm{inferInstance}$. Assume that $Q$ holds for $W$, $S$ and $\operatorname{over}$ applied to $W$, $S$ and $\mathrm{inferInstance}$. Assume that for all elements $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$, $Q$ holds for $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$, $S$ and $\operatorname{over}$ applied to $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$, $S$ and $\mathrm{inferInstance}$. Then $\operatorname{pullbackCoverOverProp'}$ applied to $S$, $x$, $f$, $\mathrm{hX}$, $\mathrm{hW}$ and $\mathrm{hQ}$ is a cover of the precoverage of $P$ and $W$.

AlgebraicGeometry.Scheme.Hom.asOverPropdefMathlib.AlgebraicGeometry.Cover.Over, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $S$ be a scheme. Then $\operatorname{asOverProp}$ applied to $f$ and $S$ is a homomorphism of $\operatorname{asOverProp}$ applied to $X$, $S$ and $\mathrm{hX}$ and $\operatorname{asOverProp}$ applied to $Y$, $S$ and $\mathrm{hY}$ defined as $\operatorname{mk}$ applied to $\operatorname{asOver}$ applied to $f$ and $S$, $\mathrm{trivial}$ and $\mathrm{trivial}$.

AlgebraicGeometry.Scheme.asOverPropdefMathlib.AlgebraicGeometry.Cover.Over, function or constant

Wording

no wording

English

Let $X$ and $S$ be schemes such that $P$ holds for $X$, $S$ and $\operatorname{over}$ applied to $X$, $S$ and $\mathrm{inferInstance}$. Then $\operatorname{asOverProp}$ applied to $X$, $S$ and $h$ is an element of $\operatorname{Over}$ applied to $P$, the top and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{asOver}$ applied to $X$ and $S$ and $h$.

Mathlib.AlgebraicGeometry.Cover.QuasiCompact

AlgebraicGeometry.QuasiCompactCoverclassMathlib.AlgebraicGeometry.Cover.QuasiCompact, predicate

Wording

no wording

English

Let $x$ be a zero hypercover of $S$. Then we can say that $\operatorname{QuasiCompactCover}$ holds for $x$.

AlgebraicGeometry.QuasiCompactCover.uliftdefMathlib.AlgebraicGeometry.Cover.QuasiCompact, function or constant

Wording

the lift of x (from the name)

English

Let $x$ be a zero hypercover of $S$. Then the lift of $x$ is a zero hypercover of $S$.

AlgebraicGeometry.QuasiCompactCover.uliftHomdefMathlib.AlgebraicGeometry.Cover.QuasiCompact, function or constant

Wording

the refinement morphism of the lifted cover of x (from the docstring)

English

Let $x$ be a zero hypercover of $S$. Then the refinement morphism of the lifted cover of $x$ is a homomorphism of the lift of $x$ and $x$.

AlgebraicGeometry.Scheme.quasiCompactCoverdefMathlib.AlgebraicGeometry.Cover.QuasiCompact, function or constant

Wording

no wording

English

Let $S$ be a scheme. Then there is an object property of the set of zero hypercovers of $S$. Proof. Let $S$ be arbitrary. By AlgebraicGeometry__QuasiCompactCover.

Mathlib.AlgebraicGeometry.Cover.Sigma

AlgebraicGeometry.Scheme.Cover.Hom.sigmadefMathlib.AlgebraicGeometry.Cover.Sigma, function or constant

Wording

the sigma of f (from the name)

English

Let $f$ be a homomorphism of $x$ and $x_{1}$. Then the sigma of $f$ is a homomorphism of the sigma of $x$ and the sigma of $x_{1}$.

AlgebraicGeometry.Scheme.Cover.sigmadefMathlib.AlgebraicGeometry.Cover.Sigma, function or constant

Wording

the sigma of x (from the name)

English

Let $x$ be a cover of the precoverage of $P$ and $S$. Then the sigma of $x$ is a cover of the precoverage of $P$ and $S$.

AlgebraicGeometry.Scheme.Cover.sigmaFunctordefMathlib.AlgebraicGeometry.Cover.Sigma, function or constant

Wording

the sigma functor (from the name)

English

The sigma functor is a functor of the set of covers of the precoverage of $P$ and $S$ and the set of covers of the precoverage of $P$ and $S$.

AlgebraicGeometry.Scheme.Cover.toSigmadefMathlib.AlgebraicGeometry.Cover.Sigma, function or constant

Wording

the sigma of x (from the name)

English

Let $x$ be a cover of the precoverage of $P$ and $S$. Then the sigma of $x$ is a homomorphism of $x$ and the sigma of $x$.

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

WeierstrassCurve.Affine.Point.sym2xdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap, function or constant

Wording

the symmetric power of Q and x1 (from the name)

English

Let $P$ and $Q$ be points of $\mathrm{W'}$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $3$. Then the symmetric power of $Q$ and $x_{1}$ is an element of $R$ defined as $\operatorname{vecCons}$ applied to the product of the representation of $P$ and $0$ and the representation of $Q$ and $0$, $\operatorname{vecCons}$ applied to the sum of the product of the representation of $P$ and $0$ and the representation of $Q$ and $1$ and the product of the representation of $P$ and $1$ and the representation of $Q$ and $0$ and $\operatorname{vecCons}$ applied to the product of the representation of $P$ and $1$ and the representation of $Q$ and $1$ and $\operatorname{vecEmpty}$ and $x_{1}$.

WeierstrassCurve.addSubMapdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap, function or constant

Wording

the additive difference map of W and x1 (from the name)

English

Let $W$ be a Weierstrass curve of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $3$. Then the additive difference map of $W$ and $x_{1}$ is a multivariate polynomial of $\mathrm{Fin}$ applied to $3$ and $R$ defined as $\operatorname{vecCons}$ applied to $\operatorname{X} (0)^ {2}- \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2084\_} (W))\times \operatorname{X} (0)\times \operatorname{X} (2)- \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2086\_} (W))\times \operatorname{X} (1)\times \operatorname{X} (2)- \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2088\_} (W))\times \operatorname{X} (2)^ {2}$, $\operatorname{vecCons}$ applied to $\operatorname{C} (2)\times \operatorname{X} (1)\times \operatorname{X} (0)+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2082\_} (W))\times \operatorname{X} (0)\times \operatorname{X} (2)+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2084\_} (W))\times \operatorname{X} (1)\times \operatorname{X} (2)+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2086\_} (W))\times \operatorname{X} (2)^ {2}$ and $\operatorname{vecCons}$ applied to $\operatorname{X} (1)^ {2}- \operatorname{C} (4)\times \operatorname{X} (0)\times \operatorname{X} (2)$ and $\operatorname{vecEmpty}$ and $x_{1}$.

WeierstrassCurve.addSubMapCoeffdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap, function or constant

Wording

the additive difference map coefficient of W and x1 (from the name)

English

Let $W$ be a Weierstrass curve of $R$. Let $x_{1}$ be an element of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $3$ and $\mathrm{Fin}$ applied to $3$. Then the additive difference map coefficient of $W$ and $x_{1}$ is a multivariate polynomial of $\mathrm{Fin}$ applied to $3$ and $R$.

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

WeierstrassCurve.AffinedefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic, type

Wording

affine of R (from the name)

English

Let $R$ be a set. Then an affine of $R$ is an element of the function that maps $R$ to the set of Weierstrass curves of $R$.

WeierstrassCurve.Affine.EquationdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic, predicate

Wording

no wording

English

Let $W$ be an affine of $R$. Let $x_{1}$ and $y$ be elements of $R$. Then $\operatorname{Equation}$ holds for $W$, $x_{1}$ and $y$, if the evaluation evaluation of $y$ and the polynomial of $W$ is equal to $0$.

WeierstrassCurve.Affine.NonsingulardefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic, predicate

Wording

no wording

English

Let $W$ be an affine of $R$. Let $x_{1}$ and $y$ be elements of $R$. Then $\operatorname{Nonsingular}$ holds for $W$, $x_{1}$ and $y$, if $\operatorname{Equation}$ holds for $W$, $x_{1}$ and $y$ and the evaluation evaluation of $y$ and the polynomial of $W$ is distinct from $0$ or the evaluation evaluation of $y$ and the polynomial of $W$ is distinct from $0$.

WeierstrassCurve.Affine.baseChangedefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic, function or constant

Wording

the base change of W and S (from the name)

English

Let $W$ be an affine of $R$. Let $S$ be a set. Then the base change of $W$ and $S$ is an affine of $S$ defined as the base change of $W$ and $S$.

WeierstrassCurve.Affine.mapdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic, function or constant

Wording

the map of W and f (from the name)

English

Let $W$ be an affine of $R$. Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $W$ and $f$ is an affine of $S$ defined as the map of $W$ and $f$.

WeierstrassCurve.Affine.polynomialdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic, function or constant

Wording

the polynomial of W (from the docstring)

English

Let $W$ be an affine of $R$. Then the polynomial of $W$ is a polynomial of the set of polynomials of $R$ defined as $\operatorname{X} ^ {2}+ \operatorname{C} (\operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2081\_} (W))\times \operatorname{X} + \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2083\_} (W)))\times \operatorname{X} - \operatorname{C} (\operatorname{X} ^ {3}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2082\_} (W))\times \operatorname{X} ^ {2}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2084\_} (W))\times \operatorname{X} + \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2086\_} (W)))$.

WeierstrassCurve.Affine.polynomialXdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic, function or constant

Wording

the polynomial of W (from the name)

English

Let $W$ be an affine of $R$. Then the polynomial of $W$ is a polynomial of the set of polynomials of $R$ defined as $\operatorname{C} (\operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)))\times \operatorname{X} - \operatorname{C} (\operatorname{C} (3)\times \operatorname{X} ^ {2}+ \operatorname{C} (2 \times \mathrm{WeierstrassCurve\_\_a\_u2082\_} (W))\times \operatorname{X} + \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2084\_} (W)))$.

WeierstrassCurve.Affine.polynomialYdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic, function or constant

Wording

the polynomial of W (from the name)

English

Let $W$ be an affine of $R$. Then the polynomial of $W$ is a polynomial of the set of polynomials of $R$ defined as $\operatorname{C} (\operatorname{C} (2))\times \operatorname{X} + \operatorname{C} (\operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2081\_} (W))\times \operatorname{X} + \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2083\_} (W)))$.

WeierstrassCurve.toAffinedefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic, function or constant

Wording

the conversion from a Weierstrass curve to affine coordinates of W (from the docstring)

English

Let $W$ be a Weierstrass curve of $R$. Then the conversion from a Weierstrass curve to affine coordinates of $W$ is an affine of $R$ defined as $W$.

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

WeierstrassCurve.Affine.addPolynomialdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula, function or constant

Wording

the additive polynomial of x2 and #4 (from the name)

English

Let $\mathrm{W'}$ be an affine of $R$. Let $x_{1}$, $y$ and $x_{2}$ be elements of $R$. Then the additive polynomial of $y$ and $x_{2}$ is a polynomial of $R$ defined as the evaluation of the line polynomial of $y$ and $x_{2}$ and the polynomial of $\mathrm{W'}$.

WeierstrassCurve.Affine.addXdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an affine of $R$. Let $x_{1}$, $x_{2}$ and $x_{3}$ be elements of $R$. Then $\operatorname{addX}$ applied to $\mathrm{W'}$, $x_{1}$, $x_{2}$ and $x_{3}$ is an element of $R$ defined as $x_{3} ^ {2}+ \mathrm{WeierstrassCurve\_\_a\_u2081\_} (\mathrm{W'})\times x_{3} - \mathrm{WeierstrassCurve\_\_a\_u2082\_} (\mathrm{W'})- x_{1} - x_{2}$.

WeierstrassCurve.Affine.addYdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an affine of $R$. Let $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$ be elements of $R$. Then $\operatorname{addY}$ applied to $\mathrm{W'}$, $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$ is an element of $R$ defined as the negation of $\operatorname{addX}$ applied to $\mathrm{W'}$, $x_{1}$, $x_{2}$ and $x_{4}$ and $\operatorname{negAddY}$ applied to $\mathrm{W'}$, $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$.

WeierstrassCurve.Affine.linePolynomialdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula, function or constant

Wording

the line polynomial of y and x2 (from the name)

English

Let $x_{1}$, $y$ and $x_{2}$ be elements of $R$. Then the line polynomial of $y$ and $x_{2}$ is a polynomial of $R$ defined as $\operatorname{C} (x_{2})\times (\operatorname{X} - \operatorname{C} (x_{1}))+ \operatorname{C} (y)$.

WeierstrassCurve.Affine.negAddYdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an affine of $R$. Let $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$ be elements of $R$. Then $\operatorname{negAddY}$ applied to $\mathrm{W'}$, $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$ is an element of $R$ defined as $x_{4} \times (\operatorname{addX} (\mathrm{W'} , x_{1} , x_{2} , x_{4})- x_{1})+ x_{3}$.

WeierstrassCurve.Affine.negPolynomialdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula, function or constant

Wording

the negation polynomial of #1 (from the docstring)

English

Let $\mathrm{W'}$ be an affine of $R$. Then the negation polynomial of $\mathrm{W'}$ is a polynomial of the set of polynomials of $R$ defined as $\operatorname{neg} (\operatorname{X})- \operatorname{C} (\operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2081\_} (\mathrm{W'}))\times \operatorname{X} + \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2083\_} (\mathrm{W'})))$.

WeierstrassCurve.Affine.negYdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula, function or constant

Wording

the negation of y and #3 (from the name)

English

Let $\mathrm{W'}$ be an affine of $R$. Let $x_{1}$ and $y$ be elements of $R$. Then the negation of $x_{1}$ and $y$ is an element of $R$ defined as $\operatorname{neg} (y)- \mathrm{WeierstrassCurve\_\_a\_u2081\_} (\mathrm{W'})\times x_{1} - \mathrm{WeierstrassCurve\_\_a\_u2083\_} (\mathrm{W'})$.

WeierstrassCurve.Affine.slopedefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula, function or constant

Wording

the slope of x4 and x5 (from the name)

English

Let $W$ be an affine of $F$. Let $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ be elements of $F$. Then the slope of $x_{4}$ and $x_{5}$ is an element of $F$ defined as $\iteMACRoG {(\EqtMACRoH {x_{2}}{x_{3}})}{(\iteMACRoG {(\EqtMACRoH {x_{4}}{\operatorname{negY} (x_{3} , x_{5})})}{0}{(\frac{ 3 \times x_{2} ^ {2}+ 2 \times \mathrm{WeierstrassCurve\_\_a\_u2082\_} (W)\times x_{2} + \mathrm{WeierstrassCurve\_\_a\_u2084\_} (W)- \mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)\times x_{4}}{x_{4} - \operatorname{negY} (x_{2} , x_{4})})})}{(\frac{ x_{4} - x_{5}}{x_{2} - x_{3}})}$.

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

WeierstrassCurve.Affine.CoordinateRingdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, type

Wording

coordinate ring of #1 (from the name)

English

Let $\mathrm{W'}$ be an affine of $R$. Then a coordinate ring of $\mathrm{W'}$ is an element of the function that maps $\mathrm{W'}$ to $\mathrm{AdjoinRoot}$ applied to the polynomial of $\mathrm{W'}$.

WeierstrassCurve.Affine.CoordinateRing.XClassdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the class of the element of x1 and #2 (from the docstring)

English

Let $\mathrm{W'}$ be an affine of $R$. Let $x_{1}$ be an element of $R$. Then the class of the element of $\mathrm{W'}$ and $x_{1}$ is a coordinate ring of $\mathrm{W'}$ defined as $\operatorname{mk}$ applied to $\mathrm{W'}$ and $\operatorname{C}$ applied to $\operatorname{X} - \operatorname{C} (x_{1})$.

WeierstrassCurve.Affine.CoordinateRing.XIdealdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the ideal of x1 and #2 (from the docstring)

English

Let $\mathrm{W'}$ be an affine of $R$. Let $x_{1}$ be an element of $R$. Then the ideal of $\mathrm{W'}$ and $x_{1}$ is an ideal of the set of coordinate rings of $\mathrm{W'}$ defined as the span of $\operatorname{singleton}$ applied to the class of the element of $\mathrm{W'}$ and $x_{1}$.

WeierstrassCurve.Affine.CoordinateRing.XYIdealdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an affine of $R$. Let $x_{1}$ be an element of $R$. Let $y$ be a polynomial of $R$. Then $\operatorname{XYIdeal}$ applied to $\mathrm{W'}$, $x_{1}$ and $y$ is an ideal of the set of coordinate rings of $\mathrm{W'}$ defined as the span of $\operatorname{insert}$ applied to the class of the element of $\mathrm{W'}$ and $x_{1}$ and $\operatorname{singleton}$ applied to the class of the element of $\mathrm{W'}$ and $y$.

WeierstrassCurve.Affine.CoordinateRing.XYIdeal'defMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the non-zero fractional ideal of h (from the docstring)

English

Assume that $\operatorname{Nonsingular}$ holds for $W$, $x_{1}$ and $y$. Then the non-zero fractional ideal of $h$ is a unit of the set of fractional ideals of the non zero divisor of the set of coordinate rings of $W$ and the set of function fields of $W$.

WeierstrassCurve.Affine.CoordinateRing.YClassdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the class of the element of y and #2 (from the docstring)

English

Let $\mathrm{W'}$ be an affine of $R$. Let $y$ be a polynomial of $R$. Then the class of the element of $\mathrm{W'}$ and $y$ is a coordinate ring of $\mathrm{W'}$ defined as $\operatorname{mk}$ applied to $\mathrm{W'}$ and $\operatorname{X} - \operatorname{C} (y)$.

WeierstrassCurve.Affine.CoordinateRing.YIdealdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the ideal of y and #2 (from the docstring)

English

Let $\mathrm{W'}$ be an affine of $R$. Let $y$ be a polynomial of $R$. Then the ideal of $\mathrm{W'}$ and $y$ is an ideal of the set of coordinate rings of $\mathrm{W'}$ defined as the span of $\operatorname{singleton}$ applied to the class of the element of $\mathrm{W'}$ and $y$.

WeierstrassCurve.Affine.CoordinateRing.basisdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the power basis of #1 (from the docstring)

English

Let $\mathrm{W'}$ be an affine of $R$. Then the power basis of $\mathrm{W'}$ is a basis of the set of polynomials of $R$ and the set of coordinate rings of $\mathrm{W'}$.

WeierstrassCurve.Affine.CoordinateRing.mapdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

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

English

Let $\mathrm{W'}$ be an affine of $R$. Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $\mathrm{W'}$ and $f$ is a ring homomorphism of the set of coordinate rings of $\mathrm{W'}$ and the set of coordinate rings of the map of $\mathrm{W'}$ and $f$.

WeierstrassCurve.Affine.CoordinateRing.mkdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an affine of $R$. Then $\operatorname{mk}$ applied to $\mathrm{W'}$ is a ring homomorphism of the set of polynomials of the set of polynomials of $R$ and the set of coordinate rings of $\mathrm{W'}$ defined as $\operatorname{mk}$ applied to the polynomial of $\mathrm{W'}$.

WeierstrassCurve.Affine.CoordinateRing.quotientXYIdealEquivdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

no wording

English

Assume that the evaluation of $x_{1}$ and the evaluation of $y$ and the polynomial of $\mathrm{W'}$ is equal to $0$. Then $\operatorname{quotientXYIdealEquiv}$ applied to $h$ is an algebra isomorphism of the set of quotients of the set of coordinate rings of $\mathrm{W'}$ and $\operatorname{XYIdeal}$ applied to $\mathrm{W'}$, $x_{1}$ and $y$ and $R$.

WeierstrassCurve.Affine.FunctionFielddefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, type

Wording

function field of #1 (from the name)

English

Let $\mathrm{W'}$ be an affine of $R$. Then a function field of $\mathrm{W'}$ is an element of the function that maps $\mathrm{W'}$ to the set of fraction rings of the set of coordinate rings of $\mathrm{W'}$.

WeierstrassCurve.Affine.PointinductiveMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, type

Wording

point of #1 (from the name)

English

Let $\mathrm{W'}$ be an affine of $R$. Then the points of $\mathrm{W'}$ are a basic type.

WeierstrassCurve.Affine.Point.adddefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the sum of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be points of $W$. Then the sum of $x_{2}$ and $x_{3}$ is a point of $W$.

WeierstrassCurve.Affine.Point.baseChangedefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the base change of F and K (from the name)

English

Let $F$ and $K$ be sets. Then the base change of $F$ and $K$ is an additive monoid homomorphism of the set of points of the base change of $\mathrm{W'}$ and $F$ and the set of points of the base change of $\mathrm{W'}$ and $K$ defined as the map of the algebra of $F$ and $K$.

WeierstrassCurve.Affine.Point.ctorElimTypedefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, type

Wording

no wording

English

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $R$ and elements $y$ of $R$ and elements $h$ of $\mathrm{Proof}$ applied to $\operatorname{Nonsingular}$ applied to $\mathrm{W'}$, $x_{1}$ and $y$ to elements of $\mathrm{motive}$ applied to $\operatorname{some}$ applied to $x_{1}$, $y$ and $h$.

WeierstrassCurve.Affine.Point.mapdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the map of f (from the name)

English

Let $f$ be an algebra homomorphism of $F$ and $K$. Then the map of $f$ is an additive monoid homomorphism of the set of points of the base change of $\mathrm{W'}$ and $F$ and the set of points of the base change of $\mathrm{W'}$ and $K$.

WeierstrassCurve.Affine.Point.mkdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

no wording

English

Assume that $\operatorname{Equation}$ holds for $\mathrm{W'}$, $x_{1}$ and $y$. Then $\operatorname{mk}$ applied to $h_{2}$ is a point of $\mathrm{W'}$.

WeierstrassCurve.Affine.Point.negdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the negation of x1 (from the docstring)

English

Let $x_{1}$ be a point of $\mathrm{W'}$. Then the negation of $x_{1}$ is a point of $\mathrm{W'}$.

WeierstrassCurve.Affine.Point.someconstructorMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

no wording

English

Let $x_{1}$ and $y$ be elements of $R$ such that $\operatorname{Nonsingular}$ holds for $\mathrm{W'}$, $x_{1}$ and $y$. Then $\operatorname{some}$ applied to $x_{1}$, $y$ and $h$ is a point of $\mathrm{W'}$.

WeierstrassCurve.Affine.Point.toClassdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the class (from the name)

English

The class is an additive monoid homomorphism of the set of points of $W$ and $\mathrm{Additive}$ applied to the set of ideal class groups of the set of coordinate rings of $W$.

WeierstrassCurve.Affine.Point.xRepdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the representation of x1 and x2 (from the name)

English

Let $x_{1}$ be a point of $\mathrm{W'}$. Let $x_{2}$ be an element of $\mathrm{Fin}$ applied to $2$. Then the representation of $x_{1}$ and $x_{2}$ is an element of $R$.

WeierstrassCurve.Affine.Point.zeroconstructorMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the zero (from the name)

English

The zero is a point of $\mathrm{W'}$.

WeierstrassCurve.Affine.nonsingularPointEquivdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the equivalence between the nonsingular points on a Weierstrass curve of #1 (from the docstring)

English

Let $\mathrm{W'}$ be an affine of $R$. Then the equivalence between the nonsingular points on a Weierstrass curve of $\mathrm{W'}$ is an equivalence from the set of points of $\mathrm{W'}$ to $\mathrm{WithZero}$ applied to $\SubtypeSet {\mathrm{xy}}{\operatorname{Nonsingular} (\mathrm{W'} , \ProdfstMACRoZ {\mathrm{xy}}, \ProdsndMACRoAA {\mathrm{xy}})}$.

WeierstrassCurve.Affine.nonsingularPointEquivSubtypedefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the equivalence between the nonsingular points on a Weierstrass curve of p0 (from the docstring)

English

Assume that $p$ holds for the zero. Then the equivalence between the nonsingular points on a Weierstrass curve of $p_{0}$ is an element of $\EquivMACRoAE {(\SubtypeSet {P}{p (P)})}{\mathrm{WithZero} (\SubtypeSet {\mathrm{xy}}{\mathrm{exists} (\operatorname{Nonsingular} (\mathrm{W'} , \ProdfstMACRoZ {\mathrm{xy}}, \ProdsndMACRoAA {\mathrm{xy}}), \lambda h . p (\operatorname{some} (\ProdfstMACRoZ {\mathrm{xy}}, \ProdsndMACRoAA {\mathrm{xy}}, h)))})}$.

WeierstrassCurve.Affine.pointEquivdefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the equivalence between the rational points of #1 (from the docstring)

English

Let $\mathrm{W'}$ be an affine of $R$. Then the equivalence between the rational points of $\mathrm{W'}$ is an equivalence from the set of points of $\mathrm{W'}$ to $\mathrm{WithZero}$ applied to $\SubtypeSet {\mathrm{xy}}{\operatorname{Equation} (\mathrm{W'} , \ProdfstMACRoZ {\mathrm{xy}}, \ProdsndMACRoAA {\mathrm{xy}})}$.

WeierstrassCurve.Affine.pointEquivSubtypedefMathlib.AlgebraicGeometry.EllipticCurve.Affine.Point, function or constant

Wording

the equivalence between the points of p0 (from the docstring)

English

Assume that $p$ holds for the zero. Then the equivalence between the points of $p_{0}$ is an element of $\EquivMACRoAE {(\SubtypeSet {P}{p (P)})}{\mathrm{WithZero} (\SubtypeSet {\mathrm{xy}}{\mathrm{exists} (\operatorname{Equation} (\mathrm{W'} , \ProdfstMACRoZ {\mathrm{xy}}, \ProdsndMACRoAA {\mathrm{xy}}), \lambda h_{2} . p (\operatorname{mk} (h_{2})))})}$.

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

WeierstrassCurve.preΨdefMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Let $n$ be an integer. Then $\mathrm{WeierstrassCurve\_\_pre\_u3a8\_}$ applied to $W$ and $n$ is a polynomial of $R$ defined as $\mathrm{preNormEDS}$ applied to the exponentiation of the square of $W$ to $2$, $\mathrm{WeierstrassCurve\_\_\_u3a8\_\_u2083\_}$ applied to $W$, $\mathrm{WeierstrassCurve\_\_pre\_u3a8\_\_u2084\_}$ applied to $W$ and $n$.

WeierstrassCurve.preΨ'defMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Let $n$ be a natural number. Then $\mathrm{WeierstrassCurve\_\_pre\_u3a8\_'}$ applied to $W$ and $n$ is a polynomial of $R$ defined as $\mathrm{preNormEDS'}$ applied to the exponentiation of the square of $W$ to $2$, $\mathrm{WeierstrassCurve\_\_\_u3a8\_\_u2083\_}$ applied to $W$, $\mathrm{WeierstrassCurve\_\_pre\_u3a8\_\_u2084\_}$ applied to $W$ and $n$.

WeierstrassCurve.preΨ₄defMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_pre\_u3a8\_\_u2084\_}$ applied to $W$ is a polynomial of $R$ defined as $2 \times \operatorname{X} ^ {6}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2082\_} (W))\times \operatorname{X} ^ {5}+ 5 \times \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2084\_} (W))\times \operatorname{X} ^ {4}+ 10 \times \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2086\_} (W))\times \operatorname{X} ^ {3}+ 10 \times \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2088\_} (W))\times \operatorname{X} ^ {2}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2082\_} (W)\times \mathrm{WeierstrassCurve\_\_b\_u2088\_} (W)- \mathrm{WeierstrassCurve\_\_b\_u2084\_} (W)\times \mathrm{WeierstrassCurve\_\_b\_u2086\_} (W))\times \operatorname{X} + \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2084\_} (W)\times \mathrm{WeierstrassCurve\_\_b\_u2088\_} (W)- \mathrm{WeierstrassCurve\_\_b\_u2086\_} (W)^ {2})$.

WeierstrassCurve.ΦdefMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Let $n$ be an element of $\Integer$. Then $\mathrm{WeierstrassCurve\_\_\_u3a6\_}$ applied to $W$ and $n$ is a polynomial of $R$ defined as $\operatorname{X} \times \mathrm{WeierstrassCurve\_\_\_u3a8\_Sq} (W , n)- \mathrm{WeierstrassCurve\_\_pre\_u3a8\_} (W , n + 1)\times \mathrm{WeierstrassCurve\_\_pre\_u3a8\_} (W , n - 1)\times \iteMACRoG {\mathrm{even} (n)}{1}{\mathrm{WeierstrassCurve\_\_\_u3a8\_\_u2082\_Sq} (W)}$.

WeierstrassCurve.ΨdefMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Let $n$ be an element of $\Integer$. Then $\mathrm{WeierstrassCurve\_\_\_u3a8\_}$ applied to $W$ and $n$ is a polynomial of the set of polynomials of $R$ defined as $\operatorname{C} (\mathrm{WeierstrassCurve\_\_pre\_u3a8\_} (W , n))\times \iteMACRoG {\mathrm{even} (n)}{\mathrm{WeierstrassCurve\_\_\_u3c8\_\_u2082\_} (W)}{1}$.

WeierstrassCurve.ΨSqdefMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

the square of W and n (from the name)

English

Let $W$ be a Weierstrass curve of $R$. Let $n$ be an element of $\Integer$. Then the square of $W$ and $n$ is a polynomial of $R$ defined as $\mathrm{WeierstrassCurve\_\_pre\_u3a8\_} (W , n)^ {2}\times \iteMACRoG {\mathrm{even} (n)}{\mathrm{WeierstrassCurve\_\_\_u3a8\_\_u2082\_Sq} (W)}{1}$.

WeierstrassCurve.Ψ₂SqdefMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

the square of W (from the name)

English

Let $W$ be a Weierstrass curve of $R$. Then the square of $W$ is a polynomial of $R$ defined as $\operatorname{C} (4)\times \operatorname{X} ^ {3}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2082\_} (W))\times \operatorname{X} ^ {2}+ \operatorname{C} (2 \times \mathrm{WeierstrassCurve\_\_b\_u2084\_} (W))\times \operatorname{X} + \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2086\_} (W))$.

WeierstrassCurve.Ψ₃defMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_\_u3a8\_\_u2083\_}$ applied to $W$ is a polynomial of $R$ defined as $3 \times \operatorname{X} ^ {4}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2082\_} (W))\times \operatorname{X} ^ {3}+ 3 \times \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2084\_} (W))\times \operatorname{X} ^ {2}+ 3 \times \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2086\_} (W))\times \operatorname{X} + \operatorname{C} (\mathrm{WeierstrassCurve\_\_b\_u2088\_} (W))$.

WeierstrassCurve.φdefMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Let $n$ be an integer. Then $\mathrm{WeierstrassCurve\_\_\_u3c6\_}$ applied to $W$ and $n$ is a polynomial of the set of polynomials of $R$ defined as $\operatorname{C} (\operatorname{X})\times \mathrm{WeierstrassCurve\_\_\_u3c8\_} (W , n)^ {2}- \mathrm{WeierstrassCurve\_\_\_u3c8\_} (W , n + 1)\times \mathrm{WeierstrassCurve\_\_\_u3c8\_} (W , n - 1)$.

WeierstrassCurve.ψdefMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Let $n$ be an integer. Then $\mathrm{WeierstrassCurve\_\_\_u3c8\_}$ applied to $W$ and $n$ is a polynomial of the set of polynomials of $R$ defined as $\mathrm{normEDS}$ applied to $\mathrm{WeierstrassCurve\_\_\_u3c8\_\_u2082\_}$ applied to $W$, $\operatorname{C}$ applied to $\mathrm{WeierstrassCurve\_\_\_u3a8\_\_u2083\_}$ applied to $W$, $\operatorname{C}$ applied to $\mathrm{WeierstrassCurve\_\_pre\_u3a8\_\_u2084\_}$ applied to $W$ and $n$.

WeierstrassCurve.ψ₂defMathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_\_u3c8\_\_u2082\_}$ applied to $W$ is a polynomial of the set of polynomials of $R$ defined as the polynomial of the conversion from a Weierstrass curve to affine coordinates of $W$.

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

WeierstrassCurve.JacobiandefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, type

Wording

no wording

English

Let $R$ be a set. Then an element of $\operatorname{Jacobian}$ applied to $R$ is an element of the function that maps $R$ to the set of Weierstrass curves of $R$.

WeierstrassCurve.Jacobian.EquationdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, predicate

Wording

no wording

English

WeierstrassCurve.Jacobian.NonsingulardefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, predicate

Wording

no wording

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then $\operatorname{Nonsingular}$ holds for $\mathrm{W'}$ and $P$, if $\operatorname{Equation}$ holds for $\mathrm{W'}$ and $P$ and $\operatorname{eval}$ applied to $P$ and the polynomial of $\mathrm{W'}$ is distinct from $0$ or $\operatorname{eval}$ applied to $P$ and the polynomial of $\mathrm{W'}$ is distinct from $0$ or $\operatorname{eval}$ applied to $P$ and the polynomial of $\mathrm{W'}$ is distinct from $0$.

WeierstrassCurve.Jacobian.NonsingularLiftdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, predicate

Wording

no wording

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ be a point class of $R$. Then we can say that $\operatorname{NonsingularLift}$ holds for $\mathrm{W'}$ and $P$.

WeierstrassCurve.Jacobian.PointClassdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, type

Wording

point class of R (from the name)

English

Let $R$ be a set. Then a point class of $R$ is an element of the function that maps $R$ to the set of quotients of $\UnitsMACRoAO {R}$ and the set of functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$.

WeierstrassCurve.Jacobian.baseChangedefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, function or constant

Wording

the base change of S and #2 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $S$ be a set. Then the base change of $\mathrm{W'}$ and $S$ is an element of $\operatorname{Jacobian}$ applied to $S$ defined as the base change of $\mathrm{W'}$ and $S$.

WeierstrassCurve.Jacobian.mapdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, function or constant

Wording

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

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $\mathrm{W'}$ and $f$ is an element of $\operatorname{Jacobian}$ applied to $S$ defined as the map of $\mathrm{W'}$ and $f$.

WeierstrassCurve.Jacobian.polynomialdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, function or constant

Wording

the polynomial of #1 (from the docstring)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Then the polynomial of $\mathrm{W'}$ is a multivariate polynomial of $\mathrm{Fin}$ applied to $3$ and $R$ defined as $\operatorname{X} (1)^ {2}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2081\_} (\mathrm{W'}))\times \operatorname{X} (0)\times \operatorname{X} (1)\times \operatorname{X} (2)+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2083\_} (\mathrm{W'}))\times \operatorname{X} (1)\times \operatorname{X} (2)^ {3}- (\operatorname{X} (0)^ {3}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2082\_} (\mathrm{W'}))\times \operatorname{X} (0)^ {2}\times \operatorname{X} (2)^ {2}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2084\_} (\mathrm{W'}))\times \operatorname{X} (0)\times \operatorname{X} (2)^ {4}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2086\_} (\mathrm{W'}))\times \operatorname{X} (2)^ {6})$.

WeierstrassCurve.Jacobian.polynomialXdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, function or constant

Wording

the polynomial of #1 (from the name)

English

WeierstrassCurve.Jacobian.polynomialYdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, function or constant

Wording

the polynomial of #1 (from the name)

English

WeierstrassCurve.Jacobian.polynomialZdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, function or constant

Wording

the polynomial of #1 (from the name)

English

WeierstrassCurve.Jacobian.toAffinedefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, function or constant

Wording

the affine of #1 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Then the affine of $\mathrm{W'}$ is an affine of $R$ defined as $\mathrm{W'}$.

WeierstrassCurve.toJacobiandefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic, function or constant

Wording

the conversion from a Weierstrass curve to Jacobian coordinates of W (from the docstring)

English

Let $W$ be a Weierstrass curve of $R$. Then the conversion from a Weierstrass curve to Jacobian coordinates of $W$ is an element of $\operatorname{Jacobian}$ applied to $R$ defined as $W$.

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

WeierstrassCurve.Jacobian.addUdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

no wording

English

Let $P$ and $Q$ be functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $F$. Then $\operatorname{addU}$ applied to $P$ and $Q$ is an element of $F$ defined as $\operatorname{neg}$ applied to $\frac{ P (1)\times Q (2)^ {3}- Q (1)\times P (2)^ {3}}{P (2)\times Q (2)}$.

WeierstrassCurve.Jacobian.addXdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

no wording

English

generation took over the time limit

WeierstrassCurve.Jacobian.addXYZdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ and $Q$ be functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $3$. Then $\operatorname{addXYZ}$ applied to $\mathrm{W'}$, $P$, $Q$ and $x_{1}$ is an element of $R$ defined as $\operatorname{vecCons}$ applied to $\operatorname{addX}$ applied to $\mathrm{W'}$, $P$ and $Q$, $\operatorname{vecCons}$ applied to $\operatorname{addY}$ applied to $\mathrm{W'}$, $P$ and $Q$ and $\operatorname{vecCons}$ applied to $\operatorname{addZ}$ applied to $P$ and $Q$ and $\operatorname{vecEmpty}$ and $x_{1}$.

WeierstrassCurve.Jacobian.addYdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ and $Q$ be functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then $\operatorname{addY}$ applied to $\mathrm{W'}$, $P$ and $Q$ is an element of $R$ defined as the negation of $\mathrm{W'}$ and $\operatorname{vecCons}$ applied to $\operatorname{addX}$ applied to $\mathrm{W'}$, $P$ and $Q$ and $\operatorname{vecCons}$ applied to $\operatorname{negAddY}$ applied to $\mathrm{W'}$, $P$ and $Q$ and $\operatorname{vecCons}$ applied to $\operatorname{addZ}$ applied to $P$ and $Q$ and $\operatorname{vecEmpty}$.

WeierstrassCurve.Jacobian.addZdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

no wording

English

Let $P$ and $Q$ be functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then $\operatorname{addZ}$ applied to $P$ and $Q$ is an element of $R$ defined as $P (0)\times Q (2)^ {2}- Q (0)\times P (2)^ {2}$.

WeierstrassCurve.Jacobian.dblUdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

the double of P and #2 (from the name)

English

WeierstrassCurve.Jacobian.dblXdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

the double of P and #2 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then the double of $\mathrm{W'}$ and $P$ is an element of $R$ defined as the difference between the difference between the difference between the exponentiation of the double of $\mathrm{W'}$ and $P$ to $2$ and the product of $\mathrm{WeierstrassCurve\_\_a\_u2081\_}$ applied to $\mathrm{W'}$, the double of $\mathrm{W'}$ and $P$, $P$ applied to $2$ and the difference between $P$ applied to $1$ and the negation of $\mathrm{W'}$ and $P$ and the product of $\mathrm{WeierstrassCurve\_\_a\_u2082\_} (\mathrm{W'})\times P (2)^ {2}$ and the exponentiation of the difference between $P$ applied to $1$ and the negation of $\mathrm{W'}$ and $P$ to $2$ and the product of $2 \times P (0)$ and the exponentiation of the difference between $P$ applied to $1$ and the negation of $\mathrm{W'}$ and $P$ to $2$.

WeierstrassCurve.Jacobian.dblXYZdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $3$. Then $\operatorname{dblXYZ}$ applied to $\mathrm{W'}$, $P$ and $x_{1}$ is an element of $R$ defined as $\operatorname{vecCons}$ applied to the double of $\mathrm{W'}$ and $P$, $\operatorname{vecCons}$ applied to the double of $\mathrm{W'}$ and $P$ and $\operatorname{vecCons}$ applied to the double of $\mathrm{W'}$ and $P$ and $\operatorname{vecEmpty}$ and $x_{1}$.

WeierstrassCurve.Jacobian.dblYdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

the double of P and #2 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then the double of $\mathrm{W'}$ and $P$ is an element of $R$ defined as the negation of $\mathrm{W'}$ and $\operatorname{vecCons}$ applied to the double of $\mathrm{W'}$ and $P$ and $\operatorname{vecCons}$ applied to the negation double of $\mathrm{W'}$ and $P$ and $\operatorname{vecCons}$ applied to the double of $\mathrm{W'}$ and $P$ and $\operatorname{vecEmpty}$.

WeierstrassCurve.Jacobian.dblZdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

the double of P and #2 (from the name)

English

WeierstrassCurve.Jacobian.negAddYdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

no wording

English

generation took over the time limit

WeierstrassCurve.Jacobian.negDblYdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

the negation double of P and #2 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then the negation double of $\mathrm{W'}$ and $P$ is an element of $R$ defined as the sum of the product of $\operatorname{neg}$ applied to the double of $\mathrm{W'}$ and $P$ and the difference between the double of $\mathrm{W'}$ and $P$ and the product of $P$ applied to $0$ and the exponentiation of the difference between $P$ applied to $1$ and the negation of $\mathrm{W'}$ and $P$ to $2$ and the product of $P$ applied to $1$ and the exponentiation of the difference between $P$ applied to $1$ and the negation of $\mathrm{W'}$ and $P$ to $3$.

WeierstrassCurve.Jacobian.negYdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula, function or constant

Wording

the negation of P and #2 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then the negation of $\mathrm{W'}$ and $P$ is an element of $R$ defined as $\operatorname{neg} (P (1))- \mathrm{WeierstrassCurve\_\_a\_u2081\_} (\mathrm{W'})\times P (0)\times P (2)- \mathrm{WeierstrassCurve\_\_a\_u2083\_} (\mathrm{W'})\times P (2)^ {3}$.

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

WeierstrassCurve.Affine.Point.toJacobiandefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

no wording

English

Let $P$ be a point of $W$. Then $\operatorname{toJacobian}$ applied to $P$ is a point of the conversion from a Weierstrass curve to Jacobian coordinates of $W$ defined as $\operatorname{fromAffine}$ applied to $P$.

WeierstrassCurve.Jacobian.PointstructureMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, type

Wording

point of #1 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Then the points of $\mathrm{W'}$ are a basic type.

WeierstrassCurve.Jacobian.Point.adddefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

the sum of P and Q (from the name)

English

Let $P$ and $Q$ be points of $W$. Then the sum of $P$ and $Q$ is a point of $W$.

WeierstrassCurve.Jacobian.Point.fromAffinedefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

no wording

English

Let $x_{1}$ be a point of the affine of $\mathrm{W'}$. Then $\operatorname{fromAffine}$ applied to $x_{1}$ is a point of $\mathrm{W'}$.

WeierstrassCurve.Jacobian.Point.negdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

the negation of P (from the docstring)

English

Let $P$ be a point of $W$. Then the negation of $P$ is a point of $W$.

WeierstrassCurve.Jacobian.Point.pointdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

the point of self (from the name)

English

Let $\mathrm{self}$ be a point of $\mathrm{W'}$. Then the point of $\mathrm{self}$ is a point class of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

WeierstrassCurve.Jacobian.Point.toAffinedefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

the affine of W and P (from the name)

English

Let $W$ be an element of $\operatorname{Jacobian}$ applied to $F$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $F$. Then the affine of $W$ and $P$ is a point of the affine of $W$.

WeierstrassCurve.Jacobian.Point.toAffineAddEquivdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

the affine additive equivalence of W (from the name)

English

Let $W$ be an element of $\operatorname{Jacobian}$ applied to $F$. Then the affine additive equivalence of $W$ is an additive equivalence of the set of points of $W$ and the set of points of the affine of $W$.

WeierstrassCurve.Jacobian.Point.toAffineLiftdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

the affine lift of P (from the name)

English

Let $P$ be a point of $W$. Then the affine lift of $P$ is a point of the affine of $W$ defined as $\operatorname{lift}$ applied to the function that maps $x_{1}$ to the affine of $W$ and $x_{1}$, the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{WeierstrassCurve\_\_Jacobian\_\_Point\_\_toAffine\_of\_equiv}$ and the point of $P$.

WeierstrassCurve.Jacobian.adddefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

the sum of x1 and #4 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ and $Q$ be functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $3$. Then the sum of $Q$ and $x_{1}$ is an element of $R$ defined as $\iteMACRoG {\operatorname{Equiv} (P , Q)}{\operatorname{dblXYZ} (\mathrm{W'} , P)}{\operatorname{addXYZ} (\mathrm{W'} , P , Q)}$.

WeierstrassCurve.Jacobian.addMapdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

the additive map of Q and #3 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ and $Q$ be point classes of $R$. Then the additive map of $P$ and $Q$ is a point class of $R$ defined as the map of $P$ and $Q$.

WeierstrassCurve.Jacobian.negdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

the negation of x1 and #3 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $3$. Then the negation of $P$ and $x_{1}$ is an element of $R$ defined as $\operatorname{vecCons}$ applied to $P$ applied to $0$, $\operatorname{vecCons}$ applied to the negation of $\mathrm{W'}$ and $P$ and $\operatorname{vecCons}$ applied to $P$ applied to $2$ and $\operatorname{vecEmpty}$ and $x_{1}$.

WeierstrassCurve.Jacobian.negMapdefMathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point, function or constant

Wording

the negation of P and #2 (from the docstring)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Jacobian}$ applied to $R$. Let $P$ be a point class of $R$. Then the negation of $\mathrm{W'}$ and $P$ is a point class of $R$ defined as the map of $\operatorname{neg}$ and $P$.

Mathlib.AlgebraicGeometry.EllipticCurve.LFunction

WeierstrassCurve.LFunctiondefMathlib.AlgebraicGeometry.EllipticCurve.LFunction, function or constant

Wording

the function of W (from the name)

English

Let $W$ be a Weierstrass curve of $K$. Then the function of $W$ is an arithmetic function of $\Integer$ defined as the Euler product of the function that maps $p$ to the local Euler factor of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{adicCompletionIntegers} (K , p)}{x_{1}})}$ and the base change of $W$ and the set of adic completions of $K$ and $p$.

WeierstrassCurve.LSeriesdefMathlib.AlgebraicGeometry.EllipticCurve.LFunction, function or constant

Wording

the series of W and s (from the name)

English

Let $W$ be a Weierstrass curve of $K$. Let $s$ be a complex. Then the series of $W$ and $s$ is a complex defined as the series of $\operatorname{comp}$ applied to $\operatorname{instIntCast}$ and $\operatorname{coe}$ applied to the function of $W$ and $s$.

WeierstrassCurve.localEulerFactordefMathlib.AlgebraicGeometry.EllipticCurve.LFunction, function or constant

Wording

the local Euler factor of R and W (from the name)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then the local Euler factor of $R$ and $W$ is an arithmetic function of $\Integer$ defined as $\operatorname{ofPowerSeries}$ applied to the cardinality of the set of residue fields of $R$ and the local power series of $R$ and $W$.

WeierstrassCurve.localPolynomialdefMathlib.AlgebraicGeometry.EllipticCurve.LFunction, function or constant

Wording

the local polynomial of R and W (from the name)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then the local polynomial of $R$ and $W$ is a polynomial of $\Integer$ defined as $\iteMACRoG {\operatorname{HasGoodReduction} (\operatorname{minimal} (R , W))}{(1 - \operatorname{C} (\operatorname{card} (\operatorname{ResidueField} (R))+ 1 - \operatorname{card} (\operatorname{Point} (\operatorname{toAffine} (\operatorname{reduction} (R , \operatorname{minimal} (R , W))))))\times \operatorname{X} + \operatorname{C} (\operatorname{card} (\operatorname{ResidueField} (R)))\times \operatorname{X} ^ {2})}{(\iteMACRoG {\operatorname{HasSplitMultiplicativeReduction} (\operatorname{minimal} (R , W))}{(1 - \operatorname{X})}{(\iteMACRoG {\operatorname{HasMultiplicativeReduction} (\operatorname{minimal} (R , W))}{(1 + \operatorname{X})}{1})})}$.

WeierstrassCurve.localPowerSeriesdefMathlib.AlgebraicGeometry.EllipticCurve.LFunction, function or constant

Wording

the local power series of R and W (from the name)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then the local power series of $R$ and $W$ is a power series of $\Integer$ defined as the inverse of the power series of the local polynomial of $R$ and $W$ and $1$.

Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

WeierstrassCurve.ofJdefMathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ, function or constant

Wording

the Weierstrass curve of j (from the name)

English

Let $j$ be an element of $F$. Then the Weierstrass curve of $j$ is a Weierstrass curve of $F$ defined as $\iteMACRoG {(\EqtMACRoH {j}{0})}{(\iteMACRoG {(\EqtMACRoH {3}{0})}{\operatorname{ofJ1728} (F)}{\operatorname{ofJ0} (F)})}{(\iteMACRoG {(\EqtMACRoH {j}{1728})}{\operatorname{ofJ1728} (F)}{\operatorname{ofJNe0Or1728} (j)})}$.

WeierstrassCurve.ofJ0defMathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ, function or constant

Wording

the Weierstrass curve of R (from the docstring)

English

Let $R$ be a set. Then the Weierstrass curve of $R$ is a Weierstrass curve of $R$ defined as $\operatorname{mk}$ applied to $0$, $0$, $1$, $0$ and $0$.

WeierstrassCurve.ofJ1728defMathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ, function or constant

Wording

the Weierstrass curve of R (from the docstring)

English

Let $R$ be a set. Then the Weierstrass curve of $R$ is a Weierstrass curve of $R$ defined as $\operatorname{mk}$ applied to $0$, $0$, $0$, $1$ and $0$.

WeierstrassCurve.ofJNe0Or1728defMathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ, function or constant

Wording

the Weierstrass curve of j (from the docstring)

English

Let $j$ be an element of $R$. Then the Weierstrass curve of $j$ is a Weierstrass curve of $R$ defined as $\operatorname{mk}$ applied to $j - 1728$, $0$, $0$, $\operatorname{neg} (36)\times (j - 1728)^ {3}$ and $\operatorname{neg}$ applied to $(j - 1728)^ {5}$.

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

WeierstrassCurve.IsCharNeTwoNFclassMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, predicate

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then we can say that $\operatorname{IsCharNeTwoNF}$ holds for $W$.

WeierstrassCurve.IsCharThreeJNeZeroNFclassMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, predicate

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then we can say that $\operatorname{IsCharThreeJNeZeroNF}$ holds for $W$.

WeierstrassCurve.IsCharThreeNFclassMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, predicate

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then we can say that $\operatorname{IsCharThreeNF}$ holds for $W$.

WeierstrassCurve.IsCharTwoJEqZeroNFclassMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, predicate

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then we can say that $\operatorname{IsCharTwoJEqZeroNF}$ holds for $W$.

WeierstrassCurve.IsCharTwoJNeZeroNFclassMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, predicate

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then we can say that $\operatorname{IsCharTwoJNeZeroNF}$ holds for $W$.

WeierstrassCurve.IsCharTwoNFclassMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, predicate

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then we can say that $\operatorname{IsCharTwoNF}$ holds for $W$.

WeierstrassCurve.IsShortNFclassMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, predicate

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then we can say that $\operatorname{IsShortNF}$ holds for $W$.

WeierstrassCurve.toCharNeTwoNFdefMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\operatorname{toCharNeTwoNF}$ applied to $W$ is a variable change of $R$ defined as $\operatorname{mk}$ applied to $1$, $0$, the product of the inverse of $2$ and $\operatorname{neg}$ applied to $\mathrm{WeierstrassCurve\_\_a\_u2081\_}$ applied to $W$ and the product of the inverse of $2$ and $\operatorname{neg}$ applied to $\mathrm{WeierstrassCurve\_\_a\_u2083\_}$ applied to $W$.

WeierstrassCurve.toCharThreeNFdefMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $F$. Then $\operatorname{toCharThreeNF}$ applied to $W$ is a variable change of $F$ defined as $\operatorname{mk} (1 , \frac{ \mathrm{WeierstrassCurve\_\_a\_u2084\_} (\HSMulhSMulMACRoAL {\operatorname{toShortNFOfCharThree} (W)}{W})}{\mathrm{WeierstrassCurve\_\_a\_u2082\_} (\HSMulhSMulMACRoAL {\operatorname{toShortNFOfCharThree} (W)}{W})}, 0 , 0)\times \operatorname{toShortNFOfCharThree} (W)$.

WeierstrassCurve.toCharTwoJEqZeroNFdefMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\operatorname{toCharTwoJEqZeroNF}$ applied to $W$ is a variable change of $R$ defined as $\operatorname{mk}$ applied to $1$, $\mathrm{WeierstrassCurve\_\_a\_u2082\_}$ applied to $W$, $0$ and $0$.

WeierstrassCurve.toCharTwoJNeZeroNFdefMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $F$ such that $\mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)\neq 0$. Then $\operatorname{toCharTwoJNeZeroNF}$ applied to $W$ and $h$ is a variable change of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{mk0}$ applied to $\mathrm{WeierstrassCurve\_\_a\_u2081\_}$ applied to $W$ and $h$, $\frac{ \mathrm{WeierstrassCurve\_\_a\_u2083\_} (W)}{\mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)}$, $0$ and $\frac{ \mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)^ {2}\times \mathrm{WeierstrassCurve\_\_a\_u2084\_} (W)+ \mathrm{WeierstrassCurve\_\_a\_u2083\_} (W)^ {2}}{\mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)^ {3}}$.

WeierstrassCurve.toCharTwoNFdefMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $F$. Then $\operatorname{toCharTwoNF}$ applied to $W$ is a variable change of $F$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {\mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)}{0}$, the function that maps $h$ to $\operatorname{toCharTwoJEqZeroNF}$ applied to $W$ and the function that maps $h_{1}$ to $\operatorname{toCharTwoJNeZeroNF}$ applied to $W$ and $h_{1}$.

WeierstrassCurve.toShortNFdefMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\operatorname{toShortNF}$ applied to $W$ is a variable change of $R$ defined as the product of $\operatorname{mk}$ applied to $1$, the product of the inverse of $3$ and $\operatorname{neg}$ applied to $\mathrm{WeierstrassCurve\_\_a\_u2082\_}$ applied to $\HSMulhSMulMACRoAL {\operatorname{toCharNeTwoNF} (W)}{W}$, $0$ and $0$ and $\operatorname{toCharNeTwoNF}$ applied to $W$.

WeierstrassCurve.toShortNFOfCharThreedefMathlib.AlgebraicGeometry.EllipticCurve.NormalForms, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\operatorname{toShortNFOfCharThree}$ applied to $W$ is a variable change of $R$ defined as $\operatorname{toCharNeTwoNF}$ applied to $W$.

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

WeierstrassCurve.ProjectivedefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, type

Wording

no wording

English

Let $R$ be a set. Then an element of $\operatorname{Projective}$ applied to $R$ is an element of the function that maps $R$ to the set of Weierstrass curves of $R$.

WeierstrassCurve.Projective.EquationdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, predicate

Wording

no wording

English

WeierstrassCurve.Projective.NonsingulardefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, predicate

Wording

no wording

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then $\operatorname{Nonsingular}$ holds for $\mathrm{W'}$ and $P$, if $\operatorname{Equation}$ holds for $\mathrm{W'}$ and $P$ and $\operatorname{eval}$ applied to $P$ and the polynomial of $\mathrm{W'}$ is distinct from $0$ or $\operatorname{eval}$ applied to $P$ and the polynomial of $\mathrm{W'}$ is distinct from $0$ or $\operatorname{eval}$ applied to $P$ and the polynomial of $\mathrm{W'}$ is distinct from $0$.

WeierstrassCurve.Projective.NonsingularLiftdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, predicate

Wording

no wording

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ be a point class of $R$. Then we can say that $\operatorname{NonsingularLift}$ holds for $\mathrm{W'}$ and $P$.

WeierstrassCurve.Projective.PointClassdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, type

Wording

point class of R (from the name)

English

WeierstrassCurve.Projective.baseChangedefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, function or constant

Wording

the base change of S and #2 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $S$ be a set. Then the base change of $\mathrm{W'}$ and $S$ is an element of $\operatorname{Projective}$ applied to $S$ defined as the base change of $\mathrm{W'}$ and $S$.

WeierstrassCurve.Projective.mapdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, function or constant

Wording

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

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $\mathrm{W'}$ and $f$ is an element of $\operatorname{Projective}$ applied to $S$ defined as the map of $\mathrm{W'}$ and $f$.

WeierstrassCurve.Projective.polynomialdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, function or constant

Wording

the polynomial of #1 (from the docstring)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Then the polynomial of $\mathrm{W'}$ is a multivariate polynomial of $\mathrm{Fin}$ applied to $3$ and $R$ defined as $\operatorname{X} (1)^ {2}\times \operatorname{X} (2)+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2081\_} (\mathrm{W'}))\times \operatorname{X} (0)\times \operatorname{X} (1)\times \operatorname{X} (2)+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2083\_} (\mathrm{W'}))\times \operatorname{X} (1)\times \operatorname{X} (2)^ {2}- (\operatorname{X} (0)^ {3}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2082\_} (\mathrm{W'}))\times \operatorname{X} (0)^ {2}\times \operatorname{X} (2)+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2084\_} (\mathrm{W'}))\times \operatorname{X} (0)\times \operatorname{X} (2)^ {2}+ \operatorname{C} (\mathrm{WeierstrassCurve\_\_a\_u2086\_} (\mathrm{W'}))\times \operatorname{X} (2)^ {3})$.

WeierstrassCurve.Projective.polynomialXdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, function or constant

Wording

the polynomial of #1 (from the name)

English

WeierstrassCurve.Projective.polynomialYdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, function or constant

Wording

the polynomial of #1 (from the name)

English

WeierstrassCurve.Projective.polynomialZdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, function or constant

Wording

the polynomial of #1 (from the name)

English

WeierstrassCurve.Projective.toAffinedefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, function or constant

Wording

the affine of #1 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Then the affine of $\mathrm{W'}$ is an affine of $R$ defined as $\mathrm{W'}$.

WeierstrassCurve.toProjectivedefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic, function or constant

Wording

the conversion from a Weierstrass curve to projective coordinates of W (from the docstring)

English

Let $W$ be a Weierstrass curve of $R$. Then the conversion from a Weierstrass curve to projective coordinates of $W$ is an element of $\operatorname{Projective}$ applied to $R$ defined as $W$.

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

WeierstrassCurve.Projective.addUdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

no wording

English

Let $P$ and $Q$ be functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $F$. Then $\operatorname{addU}$ applied to $P$ and $Q$ is an element of $F$ defined as $\frac{ \operatorname{neg} ((P (1)\times Q (2)- Q (1)\times P (2))^ {3})}{P (2)\times Q (2)}$.

WeierstrassCurve.Projective.addXdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

no wording

English

generation took over the time limit

WeierstrassCurve.Projective.addXYZdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ and $Q$ be functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $3$. Then $\operatorname{addXYZ}$ applied to $\mathrm{W'}$, $P$, $Q$ and $x_{1}$ is an element of $R$ defined as $\operatorname{vecCons}$ applied to $\operatorname{addX}$ applied to $\mathrm{W'}$, $P$ and $Q$, $\operatorname{vecCons}$ applied to $\operatorname{addY}$ applied to $\mathrm{W'}$, $P$ and $Q$ and $\operatorname{vecCons}$ applied to $\operatorname{addZ}$ applied to $\mathrm{W'}$, $P$ and $Q$ and $\operatorname{vecEmpty}$ and $x_{1}$.

WeierstrassCurve.Projective.addYdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ and $Q$ be functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then $\operatorname{addY}$ applied to $\mathrm{W'}$, $P$ and $Q$ is an element of $R$ defined as the negation of $\mathrm{W'}$ and $\operatorname{vecCons}$ applied to $\operatorname{addX}$ applied to $\mathrm{W'}$, $P$ and $Q$ and $\operatorname{vecCons}$ applied to $\operatorname{negAddY}$ applied to $\mathrm{W'}$, $P$ and $Q$ and $\operatorname{vecCons}$ applied to $\operatorname{addZ}$ applied to $\mathrm{W'}$, $P$ and $Q$ and $\operatorname{vecEmpty}$.

WeierstrassCurve.Projective.addZdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

no wording

English

generation took over the time limit

WeierstrassCurve.Projective.dblUdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

the double of W and P (from the name)

English

Let $W$ be an element of $\operatorname{Projective}$ applied to $F$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $F$. Then the double of $W$ and $P$ is an element of $F$ defined as the quotient of the exponentiation of $\operatorname{eval}$ applied to $P$ and the polynomial of $W$ to $3$ and $P (2)^ {2}$.

WeierstrassCurve.Projective.dblXdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

the double of P and #2 (from the name)

English

WeierstrassCurve.Projective.dblXYZdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

no wording

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $3$. Then $\operatorname{dblXYZ}$ applied to $\mathrm{W'}$, $P$ and $x_{1}$ is an element of $R$ defined as $\operatorname{vecCons}$ applied to the double of $\mathrm{W'}$ and $P$, $\operatorname{vecCons}$ applied to the double of $\mathrm{W'}$ and $P$ and $\operatorname{vecCons}$ applied to the double of $\mathrm{W'}$ and $P$ and $\operatorname{vecEmpty}$ and $x_{1}$.

WeierstrassCurve.Projective.dblYdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

the double of P and #2 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then the double of $\mathrm{W'}$ and $P$ is an element of $R$ defined as the negation of $\mathrm{W'}$ and $\operatorname{vecCons}$ applied to the double of $\mathrm{W'}$ and $P$ and $\operatorname{vecCons}$ applied to the negation double of $\mathrm{W'}$ and $P$ and $\operatorname{vecCons}$ applied to the double of $\mathrm{W'}$ and $P$ and $\operatorname{vecEmpty}$.

WeierstrassCurve.Projective.dblZdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

the double of P and #2 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then the double of $\mathrm{W'}$ and $P$ is an element of $R$ defined as the product of $P$ applied to $2$ and the exponentiation of the difference between $P$ applied to $1$ and the negation of $\mathrm{W'}$ and $P$ to $3$.

WeierstrassCurve.Projective.negAddYdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

no wording

English

generation took over the time limit

WeierstrassCurve.Projective.negDblYdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

the negation double of P and #2 (from the name)

English

WeierstrassCurve.Projective.negYdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula, function or constant

Wording

the negation of P and #2 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Then the negation of $\mathrm{W'}$ and $P$ is an element of $R$ defined as $\operatorname{neg} (P (1))- \mathrm{WeierstrassCurve\_\_a\_u2081\_} (\mathrm{W'})\times P (0)- \mathrm{WeierstrassCurve\_\_a\_u2083\_} (\mathrm{W'})\times P (2)$.

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

WeierstrassCurve.Affine.Point.toProjectivedefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

no wording

English

Let $P$ be a point of $W$. Then $\operatorname{toProjective}$ applied to $P$ is a point of the conversion from a Weierstrass curve to projective coordinates of $W$ defined as $\operatorname{fromAffine}$ applied to $P$.

WeierstrassCurve.Projective.PointstructureMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, type

Wording

point of #1 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Then the points of $\mathrm{W'}$ are a basic type.

WeierstrassCurve.Projective.Point.adddefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

the sum of P and Q (from the name)

English

Let $P$ and $Q$ be points of $W$. Then the sum of $P$ and $Q$ is a point of $W$.

WeierstrassCurve.Projective.Point.fromAffinedefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

no wording

English

Let $x_{1}$ be a point of the affine of $\mathrm{W'}$. Then $\operatorname{fromAffine}$ applied to $x_{1}$ is a point of $\mathrm{W'}$.

WeierstrassCurve.Projective.Point.negdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

the negation of P (from the docstring)

English

Let $P$ be a point of $W$. Then the negation of $P$ is a point of $W$.

WeierstrassCurve.Projective.Point.pointdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

the point of self (from the name)

English

Let $\mathrm{self}$ be a point of $\mathrm{W'}$. Then the point of $\mathrm{self}$ is a point class of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

WeierstrassCurve.Projective.Point.toAffinedefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

the affine of W and P (from the name)

English

Let $W$ be an element of $\operatorname{Projective}$ applied to $F$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $F$. Then the affine of $W$ and $P$ is a point of the affine of $W$.

WeierstrassCurve.Projective.Point.toAffineAddEquivdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

the affine additive equivalence of W (from the name)

English

Let $W$ be an element of $\operatorname{Projective}$ applied to $F$. Then the affine additive equivalence of $W$ is an additive equivalence of the set of points of $W$ and the set of points of the affine of $W$.

WeierstrassCurve.Projective.Point.toAffineLiftdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

the affine lift of P (from the name)

English

Let $P$ be a point of $W$. Then the affine lift of $P$ is a point of the affine of $W$ defined as $\operatorname{lift}$ applied to the function that maps $x_{1}$ to the affine of $W$ and $x_{1}$, the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{WeierstrassCurve\_\_Projective\_\_Point\_\_toAffine\_of\_equiv}$ and the point of $P$.

WeierstrassCurve.Projective.adddefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

the sum of x1 and #4 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ and $Q$ be functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $3$. Then the sum of $Q$ and $x_{1}$ is an element of $R$ defined as $\iteMACRoG {\operatorname{Equiv} (P , Q)}{\operatorname{dblXYZ} (\mathrm{W'} , P)}{\operatorname{addXYZ} (\mathrm{W'} , P , Q)}$.

WeierstrassCurve.Projective.addMapdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

the additive map of Q and #3 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ and $Q$ be point classes of $R$. Then the additive map of $P$ and $Q$ is a point class of $R$ defined as the map of $P$ and $Q$.

WeierstrassCurve.Projective.negdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

the negation of x1 and #3 (from the name)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ be a function from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $3$. Then the negation of $P$ and $x_{1}$ is an element of $R$ defined as $\operatorname{vecCons}$ applied to $P$ applied to $0$, $\operatorname{vecCons}$ applied to the negation of $\mathrm{W'}$ and $P$ and $\operatorname{vecCons}$ applied to $P$ applied to $2$ and $\operatorname{vecEmpty}$ and $x_{1}$.

WeierstrassCurve.Projective.negMapdefMathlib.AlgebraicGeometry.EllipticCurve.Projective.Point, function or constant

Wording

the negation of P and #2 (from the docstring)

English

Let $\mathrm{W'}$ be an element of $\operatorname{Projective}$ applied to $R$. Let $P$ be a point class of $R$. Then the negation of $\mathrm{W'}$ and $P$ is a point class of $R$ defined as the map of $\operatorname{neg}$ and $P$.

Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

WeierstrassCurve.HasAdditiveReductionclassMathlib.AlgebraicGeometry.EllipticCurve.Reduction, predicate

Wording

W has additive reductions (from the name)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then we can say that $W$ has additive reductions.

WeierstrassCurve.HasGoodReductionclassMathlib.AlgebraicGeometry.EllipticCurve.Reduction, predicate

Wording

W has good reductions (from the name)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then we can say that $W$ has good reductions.

WeierstrassCurve.HasMultiplicativeReductionclassMathlib.AlgebraicGeometry.EllipticCurve.Reduction, predicate

Wording

W has multiplicative reductions (from the name)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then we can say that $W$ has multiplicative reductions.

WeierstrassCurve.HasSplitMultiplicativeReductionclassMathlib.AlgebraicGeometry.EllipticCurve.Reduction, predicate

Wording

W has split multiplicative reductions (from the name)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then we can say that $W$ has split multiplicative reductions.

WeierstrassCurve.IsIntegralclassMathlib.AlgebraicGeometry.EllipticCurve.Reduction, predicate

Wording

W is integral (from the name)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then we can say that $W$ is integral.

WeierstrassCurve.IsMinimalclassMathlib.AlgebraicGeometry.EllipticCurve.Reduction, predicate

Wording

W is minimal (from the name)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then we can say that $W$ is minimal.

WeierstrassCurve.integralModeldefMathlib.AlgebraicGeometry.EllipticCurve.Reduction, function or constant

Wording

the integral model of R and W (from the name)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then the integral model of $R$ and $W$ is a Weierstrass curve of $R$ defined as $\operatorname{choose}$ applied to $\operatorname{integral}$.

WeierstrassCurve.minimaldefMathlib.AlgebraicGeometry.EllipticCurve.Reduction, function or constant

Wording

no wording

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then $\operatorname{minimal}$ applied to $R$ and $W$ is a Weierstrass curve of $K$ defined as $\HSMulhSMulMACRoAL {\operatorname{choose} (\mathrm{WeierstrassCurve\_\_exists\_isMinimal} (R , W))}{W}$.

WeierstrassCurve.reductiondefMathlib.AlgebraicGeometry.EllipticCurve.Reduction, function or constant

Wording

the reduction of R and W (from the docstring)

English

Let $R$ be a set. Let $W$ be a Weierstrass curve of $K$. Then the reduction of $R$ and $W$ is a Weierstrass curve of the set of residue fields of $R$ defined as the map of the integral model of $R$ and $W$ and the quotient map of $R$.

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

WeierstrassCurve.VariableChangestructureMathlib.AlgebraicGeometry.EllipticCurve.VariableChange, type

Wording

variable change of R (from the name)

English

Let $R$ be a set. Then the variable changes of $R$ are a basic type.

WeierstrassCurve.VariableChange.baseChangedefMathlib.AlgebraicGeometry.EllipticCurve.VariableChange, function or constant

Wording

the base change of C and A (from the name)

English

Let $C$ be a variable change of $R$. Let $A$ be a set. Then the base change of $C$ and $A$ is a variable change of $A$ defined as the map of $C$ and the algebra map of $R$ and $A$.

WeierstrassCurve.VariableChange.mapdefMathlib.AlgebraicGeometry.EllipticCurve.VariableChange, function or constant

Wording

the map of C and x2 (from the name)

English

Let $C$ be a variable change of $R$. Let $x_{2}$ be a ring homomorphism of $R$ and $A$. Then the map of $C$ and $x_{2}$ is a variable change of $A$ defined as $\operatorname{mk}$ applied to $\operatorname{map}$ applied to the monoid homomorphism of $x_{2}$ and $\operatorname{u}$ applied to $C$, $x_{2}$ applied to $\operatorname{r}$ applied to $C$, $x_{2}$ applied to $\operatorname{s}$ applied to $C$ and $x_{2}$ applied to $\operatorname{t}$ applied to $C$.

WeierstrassCurve.VariableChange.mapHomdefMathlib.AlgebraicGeometry.EllipticCurve.VariableChange, function or constant

Wording

the map of x2 (from the docstring)

English

Let $x_{2}$ be a ring homomorphism of $R$ and $A$. Then the map of $x_{2}$ is a monoid homomorphism of the set of variable changes of $R$ and the set of variable changes of $A$.

WeierstrassCurve.VariableChange.rdefMathlib.AlgebraicGeometry.EllipticCurve.VariableChange, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a variable change of $R$. Then $\operatorname{r}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

WeierstrassCurve.VariableChange.sdefMathlib.AlgebraicGeometry.EllipticCurve.VariableChange, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a variable change of $R$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

WeierstrassCurve.VariableChange.tdefMathlib.AlgebraicGeometry.EllipticCurve.VariableChange, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a variable change of $R$. Then $\operatorname{t}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

WeierstrassCurve.VariableChange.udefMathlib.AlgebraicGeometry.EllipticCurve.VariableChange, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a variable change of $R$. Then $\operatorname{u}$ applied to $\mathrm{self}$ is a unit of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

WeierstrassCurvestructureMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, type

Wording

Weierstrass curve of R (from the name)

English

Let $R$ be a set. Then the Weierstrass curves of $R$ are a basic type.

WeierstrassCurve.IsEllipticclassMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, predicate

Wording

W is elliptic (from the name)

English

Let $W$ be a Weierstrass curve of $R$. Then we can say that $W$ is elliptic.

WeierstrassCurve.a₁defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_a\_u2081\_}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

WeierstrassCurve.a₂defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_a\_u2082\_}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

WeierstrassCurve.a₃defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_a\_u2083\_}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

WeierstrassCurve.a₄defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_a\_u2084\_}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

WeierstrassCurve.a₆defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_a\_u2086\_}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

WeierstrassCurve.baseChangedefMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

the base change of W and A (from the name)

English

Let $W$ be a Weierstrass curve of $R$. Let $A$ be a set. Then the base change of $W$ and $A$ is a Weierstrass curve of $A$ defined as the map of $W$ and the algebra map of $R$ and $A$.

WeierstrassCurve.b₂defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_b\_u2082\_}$ applied to $W$ is an element of $R$ defined as $\mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)^ {2}+ 4 \times \mathrm{WeierstrassCurve\_\_a\_u2082\_} (W)$.

WeierstrassCurve.b₄defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_b\_u2084\_}$ applied to $W$ is an element of $R$ defined as $2 \times \mathrm{WeierstrassCurve\_\_a\_u2084\_} (W)+ \mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)\times \mathrm{WeierstrassCurve\_\_a\_u2083\_} (W)$.

WeierstrassCurve.b₆defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_b\_u2086\_}$ applied to $W$ is an element of $R$ defined as $\mathrm{WeierstrassCurve\_\_a\_u2083\_} (W)^ {2}+ 4 \times \mathrm{WeierstrassCurve\_\_a\_u2086\_} (W)$.

WeierstrassCurve.b₈defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_b\_u2088\_}$ applied to $W$ is an element of $R$ defined as $\mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)^ {2}\times \mathrm{WeierstrassCurve\_\_a\_u2086\_} (W)+ 4 \times \mathrm{WeierstrassCurve\_\_a\_u2082\_} (W)\times \mathrm{WeierstrassCurve\_\_a\_u2086\_} (W)- \mathrm{WeierstrassCurve\_\_a\_u2081\_} (W)\times \mathrm{WeierstrassCurve\_\_a\_u2083\_} (W)\times \mathrm{WeierstrassCurve\_\_a\_u2084\_} (W)+ \mathrm{WeierstrassCurve\_\_a\_u2082\_} (W)\times \mathrm{WeierstrassCurve\_\_a\_u2083\_} (W)^ {2}- \mathrm{WeierstrassCurve\_\_a\_u2084\_} (W)^ {2}$.

WeierstrassCurve.c₄defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_c\_u2084\_}$ applied to $W$ is an element of $R$ defined as $\mathrm{WeierstrassCurve\_\_b\_u2082\_} (W)^ {2}- 24 \times \mathrm{WeierstrassCurve\_\_b\_u2084\_} (W)$.

WeierstrassCurve.c₆defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_c\_u2086\_}$ applied to $W$ is an element of $R$ defined as $\operatorname{neg} (\mathrm{WeierstrassCurve\_\_b\_u2082\_} (W)^ {3})+ 36 \times \mathrm{WeierstrassCurve\_\_b\_u2082\_} (W)\times \mathrm{WeierstrassCurve\_\_b\_u2084\_} (W)- 216 \times \mathrm{WeierstrassCurve\_\_b\_u2086\_} (W)$.

WeierstrassCurve.jdefMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\operatorname{j}$ applied to $W$ is an element of $R$ defined as the product of the underlying value in the base of $\operatorname{inv}$ applied to $\mathrm{WeierstrassCurve\_\_\_u394\_'}$ applied to $W$ and $\mathrm{WeierstrassCurve\_\_c\_u2084\_} (W)^ {3}$.

WeierstrassCurve.mapdefMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

the map of W and f (from the name)

English

Let $W$ be a Weierstrass curve of $R$. Let $f$ be a ring homomorphism of $R$ and $A$. Then the map of $W$ and $f$ is a Weierstrass curve of $A$ defined as $\operatorname{mk}$ applied to $f$ applied to $\mathrm{WeierstrassCurve\_\_a\_u2081\_}$ applied to $W$, $f$ applied to $\mathrm{WeierstrassCurve\_\_a\_u2082\_}$ applied to $W$, $f$ applied to $\mathrm{WeierstrassCurve\_\_a\_u2083\_}$ applied to $W$, $f$ applied to $\mathrm{WeierstrassCurve\_\_a\_u2084\_}$ applied to $W$ and $f$ applied to $\mathrm{WeierstrassCurve\_\_a\_u2086\_}$ applied to $W$.

WeierstrassCurve.twoTorsionPolynomialdefMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\operatorname{twoTorsionPolynomial}$ applied to $W$ is an element of $\mathrm{Cubic}$ applied to $R$ defined as $\operatorname{mk}$ applied to $4$, $\mathrm{WeierstrassCurve\_\_b\_u2082\_}$ applied to $W$, $2 \times \mathrm{WeierstrassCurve\_\_b\_u2084\_} (W)$ and $\mathrm{WeierstrassCurve\_\_b\_u2086\_}$ applied to $W$.

WeierstrassCurve.ΔdefMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_\_u394\_}$ applied to $W$ is an element of $R$ defined as $\operatorname{neg} (\mathrm{WeierstrassCurve\_\_b\_u2082\_} (W)^ {2})\times \mathrm{WeierstrassCurve\_\_b\_u2088\_} (W)- 8 \times \mathrm{WeierstrassCurve\_\_b\_u2084\_} (W)^ {3}- 27 \times \mathrm{WeierstrassCurve\_\_b\_u2086\_} (W)^ {2}+ 9 \times \mathrm{WeierstrassCurve\_\_b\_u2082\_} (W)\times \mathrm{WeierstrassCurve\_\_b\_u2084\_} (W)\times \mathrm{WeierstrassCurve\_\_b\_u2086\_} (W)$.

WeierstrassCurve.Δ'defMathlib.AlgebraicGeometry.EllipticCurve.Weierstrass, function or constant

Wording

no wording

English

Let $W$ be a Weierstrass curve of $R$. Then $\mathrm{WeierstrassCurve\_\_\_u394\_'}$ applied to $W$ is a unit of $R$ defined as the unit of $\mathrm{WeierstrassCurve\_\_isUnit\_\_u394\_}$ applied to $W$.

Mathlib.AlgebraicGeometry.Fiber

AlgebraicGeometry.Scheme.Hom.asFiberdefMathlib.AlgebraicGeometry.Fiber, 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{asFiber}$ applied to $f$ and $x$ is a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the fiber of $f$ and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $x$ defined as $\operatorname{symm}$ applied to the fiber homeomorphism of $f$ and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $x$ and $x$.

AlgebraicGeometry.Scheme.Hom.asFiberHomdefMathlib.AlgebraicGeometry.Fiber, function or constant

Wording

no wording

English

AlgebraicGeometry.Scheme.Hom.fiberdefMathlib.AlgebraicGeometry.Fiber, function or constant

Wording

the fiber of f and y (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $y$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$. Then the fiber of $f$ and $y$ is a scheme defined as the pullback of $f$ and $\operatorname{fromSpecResidueField}$ applied to $Y$ and $y$.

AlgebraicGeometry.Scheme.Hom.fiberHomeodefMathlib.AlgebraicGeometry.Fiber, function or constant

Wording

the fiber homeomorphism of f and y (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $y$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$. Then the fiber homeomorphism of $f$ and $y$ 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 fiber of $f$ and $y$ and the set of elements of the preimage of $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $\operatorname{singleton}$ applied to $y$.

AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueFielddefMathlib.AlgebraicGeometry.Fiber, function or constant

Wording

the fiber to spectrum residue field of f and y (from the name)

English

AlgebraicGeometry.Scheme.Hom.fiberιdefMathlib.AlgebraicGeometry.Fiber, function or constant

Wording

the fiber inclusion of f and y (from the name)

English

AlgebraicGeometry.Spec.fiberToSpecResidueFieldIsodefMathlib.AlgebraicGeometry.Fiber, function or constant

Wording

the morphism from the fiber of R (from the docstring)

English

Let $R$ and $S$ be sets. Let $p$ be a prime spectrum of $R$. Then the morphism from the fiber of $R$ is an isomorphism of $\operatorname{mk}$ applied to the fiber to spectrum residue field of the induced map of the commutative ring category of the algebra map of $R$ and $S$ and $p$ and $\operatorname{mk}$ applied to the induced map of the commutative ring category of the algebra map of the set of residue fields of $\operatorname{asIdeal}$ applied to $p$ and the set of fibers of $\operatorname{asIdeal}$ applied to $p$ and $S$.

Mathlib.AlgebraicGeometry.FunctionField

AlgebraicGeometry.Scheme.functionFielddefMathlib.AlgebraicGeometry.FunctionField, function or constant

Wording

the function field of X (from the docstring)

English

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

AlgebraicGeometry.Scheme.germToFunctionFielddefMathlib.AlgebraicGeometry.FunctionField, function or constant

Wording

the restriction map of X and U (from the docstring)

English

Let $X$ be a scheme. Let $U$ be an open of $X$. Then the restriction map of $X$ and $U$ 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 function field of $X$.