Theorems · Definition · algebraic geometry

WeierstrassCurve.Affine.Point.toClass

{F : Type u} →
  [inst : Field F] →
    {W : WeierstrassCurve.Affine F} → [inst_1 : DecidableEq F] → W.Point →+ Additive (ClassGroup W.CoordinateRing)

The group homomorphism mapping a nonsingular affine point (x, y) of a Weierstrass curve W to the class of the non-zero fractional ideal ⟨X - x, Y - y⟩ in the ideal class group of F[W].

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldDecidableEq