@[reducible, inline]

noncomputable abbrev ProjectiveCurve.CoordinateRing {k : Type u} [CommRing k] (f₀ : Polynomial (Polynomial k)) : Type u

The (affine) coordinate ring of a plane curve cut out by a bivariate polynomial f₀ ∈ k[X][Y], defined as the quotient k[X][Y]/(f₀) via AdjoinRoot.

@[reducible, inline]

noncomputable abbrev ProjectiveCurve.FunctionField {k : Type u} [CommRing k] (f₀ : Polynomial (Polynomial k)) : Type u

The function field of a plane curve, defined as the field of fractions of its coordinate ring k[X][Y]/(f₀).

instance ProjectiveCurve.CoordinateRing.isDomain {k : Type u} [CommRing k] (f₀ : Polynomial (Polynomial k)) (hf : Prime f₀) : IsDomain (CoordinateRing f₀)

If the defining polynomial f₀ of the curve is prime, then the coordinate ring k[X][Y]/(f₀) is an integral domain.

@[implicit_reducible]

noncomputable instance ProjectiveCurve.FunctionField.instField {k : Type u} [CommRing k] (f₀ : Polynomial (Polynomial k)) [h : Fact (Prime f₀)] : Field (FunctionField f₀)

When f₀ is prime, the function field of the curve is a genuine field, obtained as the fraction field of the integral coordinate ring.

noncomputable def ProjectiveCurve.dehomogenizeHom (k : Type u) [CommRing k] : MvPolynomial (Fin 3) k →+* Polynomial (Polynomial k)

The ring homomorphism that dehomogenizes a polynomial in three projective variables by setting the third coordinate to 1, sending X₀ ↦ X, X₁ ↦ Y, X₂ ↦ 1.

noncomputable def ProjectiveCurve.dehomogenize {k : Type u} [CommRing k] (f : MvPolynomial (Fin 3) k) : Polynomial (Polynomial k)

Dehomogenize a homogeneous polynomial in MvPolynomial (Fin 3) k to a bivariate polynomial in k[X][Y] by substituting Z = 1.

@[simp]

theorem ProjectiveCurve.dehomogenize_X_zero {k : Type u} [CommRing k] : dehomogenize (MvPolynomial.X 0) = Polynomial.C Polynomial.X

Dehomogenization sends the projective coordinate X₀ to the bivariate polynomial X.

@[simp]

theorem ProjectiveCurve.dehomogenize_X_one {k : Type u} [CommRing k] : dehomogenize (MvPolynomial.X 1) = Polynomial.X

Dehomogenization sends the projective coordinate X₁ to the bivariate polynomial Y.

@[simp]

theorem ProjectiveCurve.dehomogenize_X_two {k : Type u} [CommRing k] : dehomogenize (MvPolynomial.X 2) = 1

Dehomogenization sends the projective coordinate X₂ (the homogenizing variable) to 1.

@[simp]

theorem ProjectiveCurve.dehomogenize_C {k : Type u} [CommRing k] (a : k) : dehomogenize (MvPolynomial.C a) = Polynomial.C (Polynomial.C a)

Dehomogenization sends the constant a ∈ k to itself viewed as a constant in k[X][Y].

@[reducible, inline]

noncomputable abbrev ProjectiveCurve.CoordinateRingOfHomog {k : Type u} [CommRing k] (f : MvPolynomial (Fin 3) k) : Type u

The coordinate ring of the affine chart {Z = 1} of a projective plane curve defined by a homogeneous polynomial f ∈ k[X₀, X₁, X₂].

@[reducible, inline]

noncomputable abbrev ProjectiveCurve.FunctionFieldOfHomog {k : Type u} [CommRing k] (f : MvPolynomial (Fin 3) k) : Type u

The function field of a projective plane curve obtained as the fraction field of the affine coordinate ring of its {Z = 1} chart.

structure ProjectiveCurve.AffinePointOver {k : Type u} [CommRing k] (f₀ : Polynomial (Polynomial k)) (L : Type v) [CommRing L] [Algebra k L] : Type v

An affine point of the curve f₀ = 0 over an extension algebra L of k, consisting of coordinates x, y ∈ L satisfying the defining equation.

• x : L
• y : L
• on_curve : Polynomial.eval₂ (Polynomial.eval₂RingHom (algebraMap k L) self.x) self.y f₀ = 0

noncomputable def ProjectiveCurve.AffinePointOver.evalRingHom {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} {L : Type v} [CommRing L] [Algebra k L] (P : AffinePointOver f₀ L) : CoordinateRing f₀ →+* L

Evaluation ring homomorphism from the coordinate ring k[X][Y]/(f₀) to L induced by a point P = (x, y) of the curve over L.

@[simp]

theorem ProjectiveCurve.AffinePointOver.evalRingHom_mk {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} {L : Type v} [CommRing L] [Algebra k L] (P : AffinePointOver f₀ L) (p : Polynomial (Polynomial k)) : P.evalRingHom ((AdjoinRoot.mk f₀) p) = Polynomial.eval₂ (Polynomial.eval₂RingHom (algebraMap k L) P.x) P.y p

Evaluating a class [p] ∈ k[X][Y]/(f₀) at a point P of the curve agrees with substituting P.x, P.y into the representative p.

structure ProjectiveCurve.AffinePoint {k : Type u} [CommRing k] (f₀ : Polynomial (Polynomial k)) : Type u

An affine point of f₀ = 0 with coordinates in the base ring k.

• x : k
• y : k
• on_curve : Polynomial.eval₂ (Polynomial.evalRingHom self.x) self.y f₀ = 0

noncomputable def ProjectiveCurve.AffinePoint.evalRingHom {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} (P : AffinePoint f₀) : CoordinateRing f₀ →+* k

Evaluation ring homomorphism from the coordinate ring k[X][Y]/(f₀) to the base ring k induced by an affine point P.

@[simp]

theorem ProjectiveCurve.AffinePoint.evalRingHom_mk {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} (P : AffinePoint f₀) (p : Polynomial (Polynomial k)) : P.evalRingHom ((AdjoinRoot.mk f₀) p) = Polynomial.eval₂ (Polynomial.evalRingHom P.x) P.y p

Evaluating a class [p] ∈ k[X][Y]/(f₀) at an affine k-point P agrees with substituting P.x, P.y into the representative p.

theorem ProjectiveCurve.eval₂RingHom_algebraMap_self {k : Type u} [CommRing k] (a : k) : Polynomial.eval₂RingHom (algebraMap k k) a = Polynomial.evalRingHom a

The two-variable evaluation map eval₂RingHom (algebraMap k k) a coincides with Polynomial.evalRingHom a, since algebraMap k k = id.

def ProjectiveCurve.AffinePoint.toOver {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} (P : AffinePoint f₀) : AffinePointOver f₀ k

Coerce a k-rational affine point into an affine point over k viewed as a k-algebra.

def ProjectiveCurve.FunctionField.IsRegularAtOver {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} {L : Type v} [CommRing L] [Algebra k L] (φ : FunctionField f₀) (P : AffinePointOver f₀ L) : Prop

A function φ on the curve is regular at an L-point P if it can be written as g/h with h not vanishing at P.

def ProjectiveCurve.FunctionField.IsRegularAt {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} (φ : FunctionField f₀) (P : AffinePoint f₀) : Prop

A function on the curve is regular at a k-rational affine point P if it admits a representation g/h with h(P) ≠ 0.

def ProjectiveCurve.FunctionField.IsRegularNonzeroAt {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} (φ : FunctionField f₀) (P : AffinePoint f₀) : Prop

A function φ is regular and nonzero at a k-rational affine point P if it has a representation g/h with h(P) ≠ 0 and g(P) ≠ 0.

noncomputable def ProjectiveCurve.evalBivariate {k : Type u} [CommRing k] {R : Type u} [CommRing R] [Algebra k R] (f : Polynomial (Polynomial k)) (a b : R) : R

Bivariate evaluation: evaluate f ∈ k[X][Y] at scalars (a, b) ∈ R × R for a k-algebra R, by mapping coefficients via algebraMap k R.

structure ProjectiveCurve.RationalMap {k : Type u} [CommRing k] (f₁ f₂ : Polynomial (Polynomial k)) [IsDomain (CoordinateRing f₁)] : Type u

A rational map from the curve f₁ = 0 to the curve f₂ = 0, represented by a triple of elements (φ₁ : φ₂ : φ₃) in the function field of f₁, not all zero, such that whenever (φ₁ : φ₂ : φ₃) is defined at a point with φ₃ ≠ 0, the image lies on f₂.

• φ₁ : FunctionField f₁
• φ₂ : FunctionField f₁
• φ₃ : FunctionField f₁
• not_all_zero : self.φ₁ ≠ 0 ∨ self.φ₂ ≠ 0 ∨ self.φ₃ ≠ 0
• image_on_curve (K : Type u) [Field K] [Algebra k K] [IsAlgClosed K] (P : AffinePointOver f₁ K) (g₁ g₂ g₃ : CoordinateRing f₁) (h : ↥(nonZeroDivisors (CoordinateRing f₁))) : self.φ₁ = IsLocalization.mk' (FunctionField f₁) g₁ h → self.φ₂ = IsLocalization.mk' (FunctionField f₁) g₂ h → self.φ₃ = IsLocalization.mk' (FunctionField f₁) g₃ h → P.evalRingHom ↑h ≠ 0 → P.evalRingHom g₁ ≠ 0 ∨ P.evalRingHom g₂ ≠ 0 ∨ P.evalRingHom g₃ ≠ 0 → P.evalRingHom g₃ ≠ 0 → evalBivariate f₂ (P.evalRingHom g₁ / P.evalRingHom g₃) (P.evalRingHom g₂ / P.evalRingHom g₃) = 0

def ProjectiveCurve.RationalMap.IsRegularAt {k : Type u} [CommRing k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (φ : RationalMap f₁ f₂) (P : AffinePoint f₁) : Prop

A rational map φ is regular at an affine k-point P if there is a nonzero scalar μ in the function field such that all three coordinates μ·φᵢ are regular at P and at least one is regular and nonzero there.

def ProjectiveCurve.FunctionField.IsRegularNonzeroAtOver {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} {K : Type u} [Field K] [Algebra k K] (φ : FunctionField f₀) (P : AffinePointOver f₀ K) : Prop

Field-valued version of IsRegularNonzeroAt: a function is regular and nonzero at an L-point P if it equals g/h for h(P) ≠ 0 and g(P) ≠ 0.

def ProjectiveCurve.RationalMap.IsRegularAtOver {k : Type u} [CommRing k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (φ : RationalMap f₁ f₂) {K : Type u} [Field K] [Algebra k K] (P : AffinePointOver f₁ K) : Prop

Field-valued regularity for rational maps: there exists a rescaling μ so that each coordinate is regular at P and at least one is regular and nonzero.

inductive ProjectiveCurve.ProjectiveCurvePointOver {k : Type u} [CommRing k] (f₀ : Polynomial (Polynomial k)) (K : Type u) [Field K] [Algebra k K] : Type u

A projective point on the curve f₀ = 0 over an extension field K, either an affine point or a point at infinity given by a nonzero direction (a, b).

• affine {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} {K : Type u} [Field K] [Algebra k K] : AffinePointOver f₀ K → ProjectiveCurvePointOver f₀ K
• atInfinity {k : Type u} [CommRing k] {f₀ : Polynomial (Polynomial k)} {K : Type u} [Field K] [Algebra k K] (a b : K) : a ≠ 0 ∨ b ≠ 0 → ProjectiveCurvePointOver f₀ K

def ProjectiveCurve.RationalMap.IsRegularAtProjectivePoint {k : Type u} [CommRing k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (φ : RationalMap f₁ f₂) {K : Type u} [Field K] [Algebra k K] (P : ProjectiveCurvePointOver f₁ K) : Prop

Regularity of a rational map at a projective point: in the affine case use IsRegularAtOver; at infinity, require that some scaling makes all coordinates into a common ratio whose numerators are not all zero.

def ProjectiveCurve.RationalMap.IsMorphism {k : Type u} [CommRing k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (φ : RationalMap f₁ f₂) : Prop

A rational map is a morphism if it is regular at every projective point of the source curve over every algebraically closed extension.

structure ProjectiveCurve.Morphism {k : Type u} [CommRing k] (f₁ f₂ : Polynomial (Polynomial k)) [IsDomain (CoordinateRing f₁)] extends ProjectiveCurve.RationalMap f₁ f₂ : Type u

A morphism of plane curves is a rational map together with a proof that it is regular everywhere.

• φ₁ : FunctionField f₁
• φ₂ : FunctionField f₁
• φ₃ : FunctionField f₁
• not_all_zero : self.φ₁ ≠ 0 ∨ self.φ₂ ≠ 0 ∨ self.φ₃ ≠ 0
• image_on_curve (K : Type u) [Field K] [Algebra k K] [IsAlgClosed K] (P : AffinePointOver f₁ K) (g₁ g₂ g₃ : CoordinateRing f₁) (h : ↥(nonZeroDivisors (CoordinateRing f₁))) : self.φ₁ = IsLocalization.mk' (FunctionField f₁) g₁ h → self.φ₂ = IsLocalization.mk' (FunctionField f₁) g₂ h → self.φ₃ = IsLocalization.mk' (FunctionField f₁) g₃ h → P.evalRingHom ↑h ≠ 0 → P.evalRingHom g₁ ≠ 0 ∨ P.evalRingHom g₂ ≠ 0 ∨ P.evalRingHom g₃ ≠ 0 → P.evalRingHom g₃ ≠ 0 → evalBivariate f₂ (P.evalRingHom g₁ / P.evalRingHom g₃) (P.evalRingHom g₂ / P.evalRingHom g₃) = 0
• regular_everywhere : self.IsMorphism

theorem ProjectiveCurve.Morphism.isMorphism {k : Type u} [CommRing k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (φ : Morphism f₁ f₂) : φ.IsMorphism

The underlying rational map of a Morphism is, by construction, a morphism.

noncomputable def ProjectiveCurve.partialDerivY {k : Type u} [CommRing k] (f₀ : Polynomial (Polynomial k)) : Polynomial (Polynomial k)

Partial derivative with respect to Y of a bivariate polynomial in k[X][Y], implemented as the formal derivative in the outer (Y) variable.

noncomputable def ProjectiveCurve.partialDerivX {k : Type u} [CommRing k] (f₀ : Polynomial (Polynomial k)) : Polynomial (Polynomial k)

Partial derivative with respect to X of a bivariate polynomial in k[X][Y], obtained by differentiating each coefficient.

def ProjectiveCurve.IsSmooth {k : Type u} [CommRing k] (f₀ : Polynomial (Polynomial k)) : Prop

A plane curve f₀ = 0 is smooth if at every affine k-point at least one of the two partial derivatives is nonzero.

theorem ProjectiveCurve.rational_map_from_smooth_is_morphism {k : Type u} [CommRing k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (hsmooth : IsSmooth f₁) (φ : RationalMap f₁ f₂) : φ.IsMorphism

Every rational map out of a smooth plane curve extends to a morphism: this is the curve-theoretic fact that a rational map from a smooth curve is automatically regular at every point.

def ProjectiveCurve.Morphism.MapsTo {k : Type u} [Field k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (φ : Morphism f₁ f₂) (P : AffinePoint f₁) (Q : AffinePoint f₂) : Prop

A morphism φ maps an affine point P of the source to an affine point Q of the target if the three coordinate ratios can be rescaled to send P to Q.

def ProjectiveCurve.Morphism.IsSurjective {k : Type u} [Field k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (φ : Morphism f₁ f₂) : Prop

A morphism is surjective on affine k-points if every target affine point has at least one preimage.

def ProjectiveCurve.Morphism.IsConstant {k : Type u} [Field k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (φ : Morphism f₁ f₂) : Prop

A morphism is constant if there is a single target point that every source point is mapped to.

theorem ProjectiveCurve.morphism_surjective_or_constant {k : Type u} [Field k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (φ : Morphism f₁ f₂) : φ.IsSurjective ∨ φ.IsConstant

Dichotomy for morphisms between plane curves over a field: a morphism is either surjective on affine k-points or constant.

def ProjectiveCurve.RationalMap.IsNonConstant {k : Type u} [Field k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (CoordinateRing f₁)] (φ : RationalMap f₁ f₂) : Prop

A rational map φ is non-constant if the affine ratios φ₁/φ₃ and φ₂/φ₃ do not both lie in the image of the constant map k → k(f₁).

@[reducible, inline]

abbrev ProjectiveCurve.ProjectivePlane (L : Type u_1) [Field L] : Type u_1

The projective plane ℙ²(L) over a field L, modeled as the projectivization of Fin 3 → L.

def ProjectiveCurve.ProjectivePointOnCurve {k : Type u} [CommRing k] (f : MvPolynomial (Fin 3) k) (L : Type u_1) [Field L] [Algebra k L] (P : ProjectivePlane L) : Prop

A point P of the projective plane ℙ²(L) lies on the projective curve cut out by a homogeneous polynomial f ∈ k[X₀, X₁, X₂] if f vanishes on any representative of P.

def ProjectiveCurve.ProjectiveCurvePoints {k : Type u} [CommRing k] (f : MvPolynomial (Fin 3) k) (L : Type u_1) [Field L] [Algebra k L] : Set (ProjectivePlane L)

The set of L-points of the projective curve f = 0.

noncomputable def ProjectiveCurve.AlgClosurePoints {k : Type u} [Field k] (f : MvPolynomial (Fin 3) k) : Set (ProjectivePlane (AlgebraicClosure k))

Points of the projective curve f = 0 over the algebraic closure of k.

@[simp]

theorem ProjectiveCurve.mem_projectiveCurvePoints_iff {k : Type u} [CommRing k] {f : MvPolynomial (Fin 3) k} {L : Type u_1} [Field L] [Algebra k L] {P : ProjectivePlane L} : P ∈ ProjectiveCurvePoints f L ↔ (MvPolynomial.aeval (Projectivization.rep P)) f = 0

Unfolding lemma for membership in ProjectiveCurvePoints: a projective point P lies on f = 0 iff f evaluates to zero on its representative.

def ProjectiveCurve.FunctionFieldOfHomog.IsRegularAt {k : Type u} [CommRing k] {f : MvPolynomial (Fin 3) k} {L : Type v} [Field L] [Algebra k L] (α : FunctionFieldOfHomog f) (P : ProjectivePlane L) (_hP : P ∈ ProjectiveCurvePoints f L) : Prop

An element of the function field of the projective curve f = 0 is regular at a projective point P if it can be expressed as a ratio g/h of homogeneous polynomials of equal degree with h not vanishing on P.

noncomputable def ProjectiveCurve.affineToProjective {L : Type u_1} [Field L] (a b : L) : ProjectivePlane L

Embed an affine point (a, b) ∈ L² into the projective plane ℙ²(L) as the point [a : b : 1].

@[reducible, inline]

noncomputable abbrev ProjectiveCurve.ProjectivePlaneOfFunctionField {k : Type u} [Field k] (f₁ : Polynomial (Polynomial k)) [IsDomain (CoordinateRing f₁)] [Fact (Prime f₁)] : Type u

The projective plane over the function field of a plane curve f₁.

structure IsogenyStandardForm (F : Type u) [Field F] : Type u

Data for an isogeny α : E₁ → E₂ in standard form: rational functions u, v, s, t ∈ F[X] such that the x-coordinate transforms as u/v and the y-coordinate transforms as (s/t)·y, with the coprimality and nonvanishing conditions required for this to be in lowest terms.

• u : Polynomial F
• v : Polynomial F
• s : Polynomial F
• t : Polynomial F
• v_ne_zero : self.v ≠ 0
• t_ne_zero : self.t ≠ 0
• coprime_uv : IsCoprime self.u self.v
• coprime_st : IsCoprime self.s self.t

noncomputable def IsogenyStandardForm.degree {F : Type u} [Field F] (α : IsogenyStandardForm F) : ℕ

The degree of an isogeny in standard form: deg α := max (deg u) (deg v) (see Definition for Theorem 5.22 / standard-form degree).

def IsogenyStandardForm.IsSeparable {F : Type u} [Field F] (α : IsogenyStandardForm F) : Prop

An isogeny in standard form is separable if u'v - uv' ≠ 0.

def IsogenyStandardForm.IsInseparable {F : Type u} [Field F] (α : IsogenyStandardForm F) : Prop

An isogeny is inseparable if it is not separable.

theorem WeierstrassCurve.Affine.coordinateRing_eq {F : Type u} [Field F] (W : Affine F) : W.CoordinateRing = ProjectiveCurve.CoordinateRing W.polynomial

The coordinate ring of a Weierstrass curve W (in the sense of Mathlib's WeierstrassCurve.Affine.CoordinateRing) agrees definitionally with the ProjectiveCurve.CoordinateRing of its defining bivariate polynomial.

@[implicit_reducible]

noncomputable instance WeierstrassCurve.Affine.instFieldFunctionField_atlas {F : Type u} [Field F] (W : Affine F) : Field W.FunctionField

The function field of a Weierstrass curve is a field.

instance WeierstrassCurve.Affine.instIsFractionRingCoordinateRingFunctionField_atlas {F : Type u} [Field F] (W : Affine F) : IsFractionRing W.CoordinateRing W.FunctionField

The function field of a Weierstrass curve is the fraction field of its coordinate ring.

@[reducible, inline]

noncomputable abbrev Field.transcendenceDegree (K : Type u) (L : Type u_1) [Field K] [Field L] [Algebra K L] : Cardinal.{u_1}

The transcendence degree of a field extension L/K, as a cardinal.

structure Isogeny {F : Type u} [Field F] [DecidableEq F] (E₁ E₂ : WeierstrassCurve.Affine F) : Type u

An isogeny E₁ → E₂ between Weierstrass curves: a surjective group homomorphism between their group-of-points along with a positive integer "degree" attribute. (See Sutherland, definitions surrounding §5.1 — an isogeny is a surjective morphism of elliptic curves that sends the identity to the identity.)

• toAddMonoidHom : E₁.Point →+ E₂.Point
• surjective : Function.Surjective ⇑self.toAddMonoidHom
• degree : ℕ
• degree_pos : 0 < self.degree

@[implicit_reducible]

instance Isogeny.instCoeFunForallPoint {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} : CoeFun (Isogeny E₁ E₂) fun (x : Isogeny E₁ E₂) => E₁.Point → E₂.Point

An isogeny may be applied to points like a function.

theorem Isogeny.map_add {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (φ : Isogeny E₁ E₂) (P Q : E₁.Point) : φ.toAddMonoidHom (P + Q) = φ.toAddMonoidHom P + φ.toAddMonoidHom Q

Isogenies are group homomorphisms: φ (P + Q) = φ P + φ Q.

@[simp]

theorem Isogeny.map_zero {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (φ : Isogeny E₁ E₂) : φ.toAddMonoidHom 0 = 0

Isogenies send the identity to the identity.

@[simp]

theorem Isogeny.map_neg {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (φ : Isogeny E₁ E₂) (P : E₁.Point) : φ.toAddMonoidHom (-P) = -φ.toAddMonoidHom P

Isogenies commute with negation.

def Isogeny.IsIsogenous {F : Type u} [Field F] [DecidableEq F] (E₁ E₂ : WeierstrassCurve.Affine F) : Prop

Two elliptic curves are isogenous if there is at least one isogeny from the first to the second.

def Isogeny.comp {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ E₃ : WeierstrassCurve.Affine F} (ψ : Isogeny E₂ E₃) (φ : Isogeny E₁ E₂) : Isogeny E₁ E₃

Composition of isogenies: comp ψ φ applies φ then ψ and multiplies the recorded degrees.

@[simp]

theorem Isogeny.comp_apply {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ E₃ : WeierstrassCurve.Affine F} (ψ : Isogeny E₂ E₃) (φ : Isogeny E₁ E₂) (P : E₁.Point) : (ψ.comp φ).toAddMonoidHom P = ψ.toAddMonoidHom (φ.toAddMonoidHom P)

The composition of isogenies acts pointwise as the composition of functions.

def Isogeny.id {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) : Isogeny E E

The identity isogeny on a Weierstrass curve, of degree 1.

@[simp]

theorem Isogeny.id_apply {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (P : E.Point) : (id E).toAddMonoidHom P = P

The identity isogeny acts as the identity function on points.

def Isogeny.IsIsomorphism {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (φ : Isogeny E₁ E₂) : Prop

An isogeny is an isomorphism if it admits a two-sided inverse isogeny.

def Isogeny.IsIsomorphic {F : Type u} [Field F] [DecidableEq F] (E₁ E₂ : WeierstrassCurve.Affine F) : Prop

Two elliptic curves are isomorphic if there is a pair of mutually-inverse isogenies between them.

noncomputable def Isogeny.extensionDegree {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (_φ : Isogeny E₁ E₂) [Algebra E₂.FunctionField E₁.FunctionField] : ℕ

The extension degree [k(E₁) : k(E₂)] of function fields associated to an isogeny φ : E₁ → E₂, computed via Module.finrank.

def ProjectiveCurve.RationalMap.SendsBasePointToBasePoint {F : Type u} [Field F] {E₁ E₂ : WeierstrassCurve.Affine F} [IsDomain (CoordinateRing E₁.polynomial)] (φ : RationalMap E₁.polynomial E₂.polynomial) : Prop

A rational map between the Weierstrass curves underlying E₁ and E₂ sends the base point (the point at infinity) of E₁ to the base point of E₂ if the second coordinate φ₂ is nonzero and the ratios φ₁/φ₂, φ₃/φ₂ come from the coordinate ring (so the rational map is regular at infinity, where the third coordinate vanishes).

structure IsogenyAlt {F : Type u} [Field F] [DecidableEq F] (E₁ E₂ : WeierstrassCurve.Affine F) : Type u

Alternative geometric definition of an isogeny: a non-constant rational map between Weierstrass curves which sends the base point to the base point.

• toRationalMap : ProjectiveCurve.RationalMap E₁.polynomial E₂.polynomial
• nonConstant : self.toRationalMap.IsNonConstant
• sendsBasePointToBasePoint : self.toRationalMap.SendsBasePointToBasePoint

theorem isogeny_iff_isogenyAlt {F : Type u} [Field F] [DecidableEq F] (E₁ E₂ : WeierstrassCurve.Affine F) : Nonempty (Isogeny E₁ E₂) ↔ Nonempty (IsogenyAlt E₁ E₂)

The group-theoretic definition (Isogeny) and the geometric definition (IsogenyAlt) of an isogeny agree: there exists an Isogeny E₁ E₂ if and only if there exists an IsogenyAlt E₁ E₂.

structure IsogenyStandardForm.WithCurveData (F : Type u) [Field F] extends IsogenyStandardForm F : Type u

An isogeny in standard form together with curve data: the polynomial `f₁ = x³

• ax + bof the source curve, an auxiliary polynomialw, and the identity v³ · (s²f₁) = t² · w(along withIsCoprime v wandSquarefree f₁). This packages the algebraic conditions needed to prove the divisibility lemma v³ ∣ t²`.

• u : Polynomial F
• v : Polynomial F
• s : Polynomial F
• t : Polynomial F
• v_ne_zero : self.v ≠ 0
• t_ne_zero : self.t ≠ 0
• coprime_uv : IsCoprime self.u self.v
• coprime_st : IsCoprime self.s self.t
• f₁ : Polynomial F
• w : Polynomial F
• identity : self.v ^ 3 * (self.s ^ 2 * self.f₁) = self.t ^ 2 * self.w
• coprime_vw : IsCoprime self.v self.w
• squarefree_f₁ : Squarefree self.f₁

theorem IsogenyStandardForm.WithCurveData.v_cube_dvd_t_sq {F : Type u} [Field F] (α : WithCurveData F) : α.v ^ 3 ∣ α.t ^ 2

From the identity v³(s²f₁) = t²w with gcd(v, w) = 1 we deduce v³ ∣ t².

theorem IsogenyStandardForm.WithCurveData.t_sq_dvd_v_cube_f₁ {F : Type u} [Field F] (α : WithCurveData F) : α.t ^ 2 ∣ α.v ^ 3 * α.f₁

Dually, from the same identity together with gcd(s, t) = 1 we deduce t² ∣ v³·f₁.

theorem IsogenyStandardForm.WithCurveData.isRoot_t_of_isRoot_v {F : Type u} [Field F] (α : WithCurveData F) {x₀ : F} (hv : α.v.IsRoot x₀) : α.t.IsRoot x₀

Every root of v is a root of t.

theorem IsogenyStandardForm.WithCurveData.isRoot_v_of_isRoot_t {F : Type u} [Field F] (α : WithCurveData F) {x₀ : F} (ht : α.t.IsRoot x₀) : α.v.IsRoot x₀

Every root of t is a root of v (using that f₁ is squarefree).

theorem IsogenyStandardForm.WithCurveData.isRoot_v_iff_isRoot_t {F : Type u} [Field F] (α : WithCurveData F) {x₀ : F} : α.v.IsRoot x₀ ↔ α.t.IsRoot x₀

v and t share exactly the same roots.

structure ProjectiveCurve.HomogeneousTriple (k : Type u) [CommRing k] : Type u

A triple of homogeneous polynomials of common degree deg in three variables, used to represent a candidate rational map between projective plane curves.

• ψ_x : MvPolynomial (Fin 3) k
• ψ_y : MvPolynomial (Fin 3) k
• ψ_z : MvPolynomial (Fin 3) k
• deg : ℕ
• hom_x : self.ψ_x.IsHomogeneous self.deg
• hom_y : self.ψ_y.IsHomogeneous self.deg
• hom_z : self.ψ_z.IsHomogeneous self.deg

def ProjectiveCurve.HomogeneousTriple.toFun {k : Type u} [CommRing k] (t : HomogeneousTriple k) : Fin 3 → MvPolynomial (Fin 3) k

Convert a HomogeneousTriple into the Fin 3 → MvPolynomial _ k function suitable for MvPolynomial.bind₁.

noncomputable def ProjectiveCurve.HomogeneousTriple.substIn {k : Type u} [CommRing k] (t : HomogeneousTriple k) (f : MvPolynomial (Fin 3) k) : MvPolynomial (Fin 3) k

Substitute the components of a homogeneous triple into a polynomial f, i.e. compute f(ψ_x, ψ_y, ψ_z).

structure ProjectiveCurve.RationalMapTriple {k : Type u} [CommRing k] (f₁ f₂ : MvPolynomial (Fin 3) k) extends ProjectiveCurve.HomogeneousTriple k : Type u

A rational map from the projective curve f₁ = 0 to f₂ = 0, represented by a homogeneous triple whose components are not all in the ideal (f₁), and which satisfies f₂(ψ_x, ψ_y, ψ_z) ∈ (f₁) (so the image lies on f₂).

• ψ_x : MvPolynomial (Fin 3) k
• ψ_y : MvPolynomial (Fin 3) k
• ψ_z : MvPolynomial (Fin 3) k
• deg : ℕ
• hom_x : self.ψ_x.IsHomogeneous self.deg
• hom_y : self.ψ_y.IsHomogeneous self.deg
• hom_z : self.ψ_z.IsHomogeneous self.deg
• not_all_in_ideal : self.ψ_x ∉ Ideal.span {f₁} ∨ self.ψ_y ∉ Ideal.span {f₁} ∨ self.ψ_z ∉ Ideal.span {f₁}
• image_in_ideal : self.substIn f₂ ∈ Ideal.span {f₁}

def ProjectiveCurve.RationalMapTriple.IsEquiv {k : Type u} [CommRing k] {f₁ f₂ : MvPolynomial (Fin 3) k} (t₁ t₂ : RationalMapTriple f₁ f₂) : Prop

Two rational-map triples are equivalent if all pairwise cross-products ψ_i^(1) ψ_j^(2) - ψ_j^(1) ψ_i^(2) lie in the ideal (f₁).

theorem ProjectiveCurve.RationalMapTriple.isEquiv_refl {k : Type u} [CommRing k] {f₁ f₂ : MvPolynomial (Fin 3) k} (t : RationalMapTriple f₁ f₂) : t.IsEquiv t

Reflexivity of triple equivalence: every rational map triple is equivalent to itself.

theorem ProjectiveCurve.RationalMapTriple.isEquiv_symm {k : Type u} [CommRing k] {f₁ f₂ : MvPolynomial (Fin 3) k} {t₁ t₂ : RationalMapTriple f₁ f₂} (h : t₁.IsEquiv t₂) : t₂.IsEquiv t₁

Symmetry of triple equivalence.

theorem ProjectiveCurve.RationalMapTriple.isEquiv_trans_of_prime {k : Type u} [CommRing k] {f₁ f₂ : MvPolynomial (Fin 3) k} (hprime : (Ideal.span {f₁}).IsPrime) {t₁ t₂ t₃ : RationalMapTriple f₁ f₂} (h12 : t₁.IsEquiv t₂) (h23 : t₂.IsEquiv t₃) : t₁.IsEquiv t₃

Transitivity of triple equivalence, assuming the ideal (f₁) is prime so we can cancel a non-vanishing component of the middle triple.

@[implicit_reducible]

instance ProjectiveCurve.RationalMapTriple.setoid {k : Type u} [CommRing k] (f₁ f₂ : MvPolynomial (Fin 3) k) [hprime : Fact (Ideal.span {f₁}).IsPrime] : Setoid (RationalMapTriple f₁ f₂)

RationalMapTriple modulo equivalence is a Setoid, provided (f₁) is prime so that transitivity holds.

def ProjectiveCurve.RationalMapAlt {k : Type u} [CommRing k] (f₁ f₂ : MvPolynomial (Fin 3) k) [Fact (Ideal.span {f₁}).IsPrime] : Type u

Alternative definition of a rational map from f₁ = 0 to f₂ = 0, as a quotient of the type of RationalMapTriples by the equivalence relation.

def ProjectiveCurve.RationalMapTriple.IsDefinedAt {k : Type u} [CommRing k] {f₁ f₂ : MvPolynomial (Fin 3) k} (t : RationalMapTriple f₁ f₂) (P : Fin 3 → k) : Prop

A rational-map triple t is defined at a point P if at least one of its homogeneous components is nonzero on P.

def EllipticCurve.IsAlgebraicEndomorphism {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (φ : AddMonoid.End E.Point) : Prop

An additive group endomorphism of E(F) is algebraic if it is either the zero map or comes from some Isogeny E E.

def EllipticCurve.EndomorphismRing {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) : Type u

The endomorphism ring End(E) of E, defined as the subtype of additive endomorphisms of E.Point which are algebraic.

def EllipticCurve.IsAlgebraicAutomorphism {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (f : AddAut E.Point) : Prop

An additive automorphism of E.Point is algebraic if it comes from a pair of mutually-inverse isogenies.

def EllipticCurve.AutomorphismGroup {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) : Type u

The automorphism group Aut(E) of E, the subtype of additive automorphisms of E.Point arising from isogenies.

def EllipticCurve.EndomorphismRing.val {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (φ : EndomorphismRing E) : AddMonoid.End E.Point

Extract the underlying additive endomorphism from an element of EndomorphismRing E.

def EllipticCurve.Isogeny.toEndomorphism {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (φ : Isogeny E E) : EndomorphismRing E

Every isogeny E → E is an algebraic endomorphism of E.Point.

def EllipticCurve.EndomorphismRing.zero {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} : EndomorphismRing E

The zero endomorphism in EndomorphismRing E.

def EllipticCurve.EndomorphismRing.one {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} : EndomorphismRing E

The identity endomorphism in EndomorphismRing E.

def EllipticCurve.EndomorphismRing.apply {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α : EndomorphismRing E) (P : E.Point) : E.Point

Apply an algebraic endomorphism to a point of E.

@[implicit_reducible]

noncomputable instance EllipticCurve.instRingEndomorphismRing {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) : Ring (EndomorphismRing E)

The endomorphism ring End(E) of an elliptic curve is a (noncommutative) ring; the proof requires geometric content and is left as sorry.

def WeierstrassCurve.Affine.IsShortWeierstrass {R : Type u} [CommRing R] (W : Affine R) : Prop

A Weierstrass curve is in short Weierstrass form if a₁ = a₂ = a₃ = 0, i.e. its equation is y² = x³ + a₄ x + a₆.

structure Isogeny.IsogenyRepresentation {F : Type u} [Field F] [DecidableEq F] (E₁ E₂ : WeierstrassCurve.Affine F) (α : Isogeny E₁ E₂) extends IsogenyStandardForm F : Type u

A representation of an isogeny α : E₁ → E₂ in standard form: it records (u, v, s, t) ∈ F[X] and the fact that on a nonsingular point (x₀, y₀) with v(x₀) ≠ 0, α sends (x₀, y₀) ↦ (u(x₀)/v(x₀), (s(x₀)/t(x₀))·y₀); in the "pole" case v(x₀) = 0 and u(x₀) ≠ 0, the image is the identity.

• u : Polynomial F
• v : Polynomial F
• s : Polynomial F
• t : Polynomial F
• v_ne_zero : self.v ≠ 0
• t_ne_zero : self.t ≠ 0
• coprime_uv : IsCoprime self.u self.v
• coprime_st : IsCoprime self.s self.t
• represents (x₀ y₀ : F) (h₁ : E₁.Nonsingular x₀ y₀) (_hv : Polynomial.eval x₀ self.v ≠ 0) : ∃ (h₂ : E₂.Nonsingular (Polynomial.eval x₀ self.u / Polynomial.eval x₀ self.v) (Polynomial.eval x₀ self.s / Polynomial.eval x₀ self.t * y₀)), α.toAddMonoidHom (WeierstrassCurve.Affine.Point.some x₀ y₀ h₁) = WeierstrassCurve.Affine.Point.some (Polynomial.eval x₀ self.u / Polynomial.eval x₀ self.v) (Polynomial.eval x₀ self.s / Polynomial.eval x₀ self.t * y₀) h₂
• maps_poles_to_zero (x₀ y₀ : F) (h₁ : E₁.Nonsingular x₀ y₀) (_hv : Polynomial.eval x₀ self.v = 0) (_hu : Polynomial.eval x₀ self.u ≠ 0) : α.toAddMonoidHom (WeierstrassCurve.Affine.Point.some x₀ y₀ h₁) = 0

noncomputable def Isogeny.isogeny_standard_form {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (hE₁ : E₁.IsShortWeierstrass) (hE₂ : E₂.IsShortWeierstrass) (α : Isogeny E₁ E₂) : IsogenyRepresentation E₁ E₂ α

For curves in short Weierstrass form, every isogeny α : E₁ → E₂ admits an IsogenyRepresentation in standard form (proved geometrically; left as sorry).

theorem Isogeny.not_in_kernel_of_v_ne_zero {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (_hE₁ : E₁.IsShortWeierstrass) (_hE₂ : E₂.IsShortWeierstrass) (α : Isogeny E₁ E₂) (rep : IsogenyRepresentation E₁ E₂ α) (x₀ y₀ : F) (h₁ : E₁.Nonsingular x₀ y₀) (hv : Polynomial.eval x₀ rep.v ≠ 0) : α.toAddMonoidHom (WeierstrassCurve.Affine.Point.some x₀ y₀ h₁) ≠ 0

If the denominator polynomial v of the standard form does not vanish at x₀, then the point (x₀, y₀) is not in the kernel of α.

theorem Isogeny.in_kernel_of_v_eq_zero {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (_hE₁ : E₁.IsShortWeierstrass) (_hE₂ : E₂.IsShortWeierstrass) (α : Isogeny E₁ E₂) (rep : IsogenyRepresentation E₁ E₂ α) (x₀ y₀ : F) (h₁ : E₁.Nonsingular x₀ y₀) (hv : Polynomial.eval x₀ rep.v = 0) : α.toAddMonoidHom (WeierstrassCurve.Affine.Point.some x₀ y₀ h₁) = 0

Conversely, if v(x₀) = 0 then u(x₀) ≠ 0 (using IsCoprime u v), so the "pole" case of the representation forces (x₀, y₀) to be in the kernel.

theorem Isogeny.kernel_iff_v_eq_zero {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (hE₁ : E₁.IsShortWeierstrass) (hE₂ : E₂.IsShortWeierstrass) (α : Isogeny E₁ E₂) (rep : IsogenyRepresentation E₁ E₂ α) (x₀ y₀ : F) (h₁ : E₁.Nonsingular x₀ y₀) : α.toAddMonoidHom (WeierstrassCurve.Affine.Point.some x₀ y₀ h₁) = 0 ↔ Polynomial.eval x₀ rep.v = 0

Combining the previous two: (x₀, y₀) lies in the kernel of α iff v(x₀) = 0. This characterizes affine points of the kernel via the standard form.

theorem Isogeny.finite_nonsingular_fibers {F : Type u} [Field F] {E₁ : WeierstrassCurve.Affine F} (x₀ : F) : {y : F | E₁.Nonsingular x₀ y}.Finite

For a fixed x₀ ∈ F, only finitely many y₀ make (x₀, y₀) a nonsingular point of E₁, because such y₀ are roots of the (nonzero) specialization of the Weierstrass polynomial at x₀.

noncomputable def Isogeny.pointToCoords {F : Type u} [Field F] {E₁ : WeierstrassCurve.Affine F} : E₁.Point → Option (F × F)

Extract the affine coordinates (x, y) of a point of E₁, mapping the identity to none.

theorem Isogeny.pointToCoords_injective {F : Type u} [Field F] {E₁ : WeierstrassCurve.Affine F} : Function.Injective pointToCoords

The coordinate-extraction function is injective.

theorem Isogeny.isogeny_kernel_finite_of_rep {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (hE₁ : E₁.IsShortWeierstrass) (hE₂ : E₂.IsShortWeierstrass) (α : Isogeny E₁ E₂) (rep : IsogenyRepresentation E₁ E₂ α) : {P : E₁.Point | α.toAddMonoidHom P = 0}.Finite

Given a standard-form representation of α, the kernel of α is finite: its image under pointToCoords is contained in {none} ∪ {(x₀,y₀) : v(x₀) = 0 ∧ E₁.Nonsingular x₀ y₀}, which is finite by the previous lemmas.

theorem Isogeny.isogeny_kernel_finite {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (hE₁ : E₁.IsShortWeierstrass) (hE₂ : E₂.IsShortWeierstrass) (α : Isogeny E₁ E₂) : {P : E₁.Point | α.toAddMonoidHom P = 0}.Finite

Corollary: the kernel of any isogeny between short Weierstrass curves is a finite set of points. Combined with isogeny_standard_form, this is a key finiteness statement underlying the degree theory of isogenies.

theorem Isogeny.isogeny_kernel_card_eq_sep_degree {F : Type u} [Field F] [DecidableEq F] [IsAlgClosed F] {E₁ E₂ : WeierstrassCurve.Affine F} {p : ℕ} [CharP F p] (hE₁ : E₁.IsShortWeierstrass) (hE₂ : E₂.IsShortWeierstrass) (α : Isogeny E₁ E₂) (rep : IsogenyRepresentation E₁ E₂ α) (α_sep : IsogenyStandardForm F) (n : ℕ) (hsep : α_sep.IsSeparable) (hu : rep.u = (Polynomial.expand F (p ^ n)) α_sep.u) (hv : rep.v = (Polynomial.expand F (p ^ n)) α_sep.v) : {P : E₁.Point | α.toAddMonoidHom P = 0}.ncard = α_sep.degree

Over an algebraically closed field of characteristic p, if α decomposes as a separable isogeny α_sep precomposed with the p^n-th power Frobenius (i.e. u = α_sep.u ∘ X^{p^n} and similarly for v), then the cardinality of the kernel of α equals the degree of its separable part α_sep. (This is the key relation between the kernel size and the separable degree of an isogeny.)