Theorems · Definition · algebraic geometry

WeierstrassCurve.Affine.CoordinateRing.quotientXYIdealEquiv

{R : Type r} →
  [inst : CommRing R] →
    {W' : WeierstrassCurve.Affine R} →
      {x : R} →
        {y : Polynomial R} →
          Polynomial.eval x (Polynomial.eval y W'.polynomial) = 0 →
            (W'.CoordinateRing ⧸ WeierstrassCurve.Affine.CoordinateRing.XYIdeal W' x y) ≃ₐ[R] R

The R-algebra isomorphism from R[W] / ⟨X - x, Y - y(X)⟩ to R obtained by evaluation at some y(X) in R[X] and at some x in R provided that W(x, y(x)) = 0.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

1 results in Mathlib

Foundations

Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing