Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_ReduceHom.lean

definition module

Reduction of points as an additive group homomorphism

Throughout, A is a valuation subring of a field L and W is a Weierstrass curve over A; the two base changes in play are W pushed along the inclusion A \hookrightarrow L (W.map A.subtype) and along the residue map A \to \kappa_A (W.map (residue A)).

A first group of lemmas records how the residue map interacts with division: if a \in A and b is not a non-unit of A then a/b \in A, the residue of such a b is non-zero, the residue of an element of A depends only on its value in L, and residues of quotients are quotients of residues (residue_div, residue_eq_div_of_eq_div). Further, two elements of A have the same residue exactly when their difference lies in the set of non-units, i.e. in the maximal ideal.

A second group transports the Weierstrass formulae: for x,y \in A the quantity \mathrm{negY}(x,y) = -y - a_1x - a_3 computed on the curve over L lies in A and its residue is \mathrm{negY} of the reduced curve at the reduced arguments, and residue_inverse_iff says that, for x_i, y_i \in A, the reduced points satisfy \bar x_1 = \bar x_2 and \bar y_1 = \mathrm{negY}(\bar x_2, \bar y_2) precisely when x_1 - x_2 and y_1 - \mathrm{negY}(x_2,y_2) both lie in the maximal ideal. Building on these, slope_mem_residue_of_not_inverse shows that for two points of the affine equation with x_1, x_2 \in A, whose reductions are not mutually inverse in this sense, the chord-or-tangent slope lies in A and reduces to the slope of the reduced curve at the reduced points; the proof splits according to whether x_1 - x_2 is a non-unit and whether x_1 = x_2, and rewrites the slope over the common denominator y_1 - \mathrm{negY}(x_2,y_2).

Under the hypothesis h\Delta that the reduced curve has non-zero discriminant, the additivity of the reduction map reducePoint hΔ — which sends an affine point with integral x-coordinate to the point with residue coordinates, and every other affine point to zero — is proved in three cases: both x-coordinates in A (reducePoint_add_of_mem, where the sum is again integral unless the two reductions are inverse, in which case the reduced sum is zero by Affine.addX_notMem_of_sub_mem_nonunits); neither in A (reducePoint_add_of_notMem_of_notMem, where the formal-parameter estimate Affine.add_formal_param_estimate shows the x-coordinate of the sum is again non-integral); and one of each (reducePoint_add_of_mem_of_notMem, deduced from the previous two applied to the sum and the negative of a summand). These combine into reducePoint_add_def, additivity for arbitrary points, and reduceHom, the bundled additive monoid homomorphism from the points of the curve over L to the points of the reduced curve whose underlying function is reducePoint hΔ.

Relation to Mathlib

Mathlib supplies the affine Weierstrass point group with negY, slope, addX, addY and their compatibility with base change, together with valuation subrings and their residue fields; the reduction map on points and its additivity are the project's own.

Where it is used

With good reduction at a place, this homomorphism compares the points of the curve over L with those of the special fibre, and is the tool for controlling n-torsion and the action of inertia on it; downstream it is composed with the identification of the special fibre of the Frey curve in the analysis of the attached mod-p Galois representation.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, Chapter VII
  2. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §2

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_WeierstrassCurve_ReduceHom.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_WeierstrassCurve_TorsionIntegral

set_option autoImplicit false

open IsLocalRing

namespace ValuationSubring

variable {L : Type*} [Field L] (A : ValuationSubring L)

theorem div_mem_of_mem_of_notMem_nonunits {a b : L} (ha : a ∈ A) (hb : b ∉ A.nonunits) :
    a / b ∈ A := by
  rw [div_eq_mul_inv]
  exact A.toSubring.mul_mem ha (A.inv_mem_of_notMem_nonunits hb)

theorem residue_ne_zero_of_notMem_nonunits {b : L} (hb : b ∈ A) (hb' : b ∉ A.nonunits) :
    residue A ⟨b, hb⟩ ≠ 0 := fun h =>
  hb' ((A.coe_mem_nonunits_iff_residue_eq_zero ⟨b, hb⟩).mpr h)

theorem residue_eq_of_coe_eq {a : L} (ha : a ∈ A) {v : A} (hav : a = (v : L)) :
    residue A ⟨a, ha⟩ = residue A v :=
  congrArg (residue A) (Subtype.ext hav)

theorem residue_div {a b : L} (ha : a ∈ A) (hb : b ∈ A) (hb' : b ∉ A.nonunits)
    (hq : a / b ∈ A) :
    residue A ⟨a / b, hq⟩ = residue A ⟨a, ha⟩ / residue A ⟨b, hb⟩ := by
  have hb0 : b ≠ 0 := A.ne_zero_of_notMem_nonunits hb'
  have hbres : residue A ⟨b, hb⟩ ≠ 0 := A.residue_ne_zero_of_notMem_nonunits hb hb'
  rw [eq_div_iff hbres, ← map_mul]
  refine congrArg (residue A) (Subtype.ext ?_)
  push_cast
  exact div_mul_cancel₀ a hb0

theorem residue_eq_div_of_eq_div {a c d : L} (ha : a ∈ A) (hc : c ∈ A) (hd : d ∈ A)
    (hd' : d ∉ A.nonunits) (hacd : a = c / d) :
    residue A ⟨a, ha⟩ = residue A ⟨c, hc⟩ / residue A ⟨d, hd⟩ := by
  rw [A.residue_eq_of_coe_eq ha
    (v := ⟨c / d, A.div_mem_of_mem_of_notMem_nonunits hc hd'⟩) hacd]
  exact A.residue_div hc hd hd' _

theorem residue_eq_residue_iff_sub_mem_nonunits {a b : L} (ha : a ∈ A) (hb : b ∈ A) :
    residue A ⟨a, ha⟩ = residue A ⟨b, hb⟩ ↔ a - b ∈ A.nonunits := by
  constructor
  · intro h
    have h0 : residue A (⟨a, ha⟩ - ⟨b, hb⟩) = 0 := by rw [map_sub, h, sub_self]
    have := (A.coe_mem_nonunits_iff_residue_eq_zero _).mpr h0
    simpa using this
  · intro h
    have h0 : residue A (⟨a, ha⟩ - ⟨b, hb⟩) = 0 :=
      (A.coe_mem_nonunits_iff_residue_eq_zero _).mp (by simpa using h)
    rw [map_sub, sub_eq_zero] at h0
    exact h0

end ValuationSubring

namespace WeierstrassCurve

variable {L : Type*} [Field L] {A : ValuationSubring L} (W : WeierstrassCurve A)

private lemma some_congr' {R : Type*} [CommRing R] {V : Affine R} {x₁ x₂ y₁ y₂ : R}
    (hx : x₁ = x₂) (hy : y₁ = y₂) (h₁ : V.Nonsingular x₁ y₁) (h₂ : V.Nonsingular x₂ y₂) :
    Affine.Point.some x₁ y₁ h₁ = Affine.Point.some x₂ y₂ h₂ := by
  subst hx; subst hy; rfl

section Coercion

variable {W}

lemma coe_negY {x y : L} (hx : x ∈ A) (hy : y ∈ A) :
    ((W.toAffine.negY ⟨x, hx⟩ ⟨y, hy⟩ : A) : L) = (W.map A.subtype).toAffine.negY x y :=
  (Affine.map_negY A.subtype (⟨x, hx⟩ : A) (⟨y, hy⟩ : A)).symm

lemma negY_mem {x y : L} (hx : x ∈ A) (hy : y ∈ A) :
    (W.map A.subtype).toAffine.negY x y ∈ A := by
  rw [← coe_negY hx hy]
  exact SetLike.coe_mem _

lemma residue_negY {x y : L} (hx : x ∈ A) (hy : y ∈ A) :
    residue A (W.toAffine.negY ⟨x, hx⟩ ⟨y, hy⟩) =
      (W.map (residue A)).toAffine.negY (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩) :=
  (Affine.map_negY (residue A) (⟨x, hx⟩ : A) (⟨y, hy⟩ : A)).symm

lemma residue_sub_negY {x₂ y₁ y₂ : L} (hy₁ : y₁ ∈ A) (hx₂ : x₂ ∈ A) (hy₂ : y₂ ∈ A)
    (hmem : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A) :
    residue A ⟨y₁ - (W.map A.subtype).toAffine.negY x₂ y₂, hmem⟩ =
      residue A ⟨y₁, hy₁⟩ -
        (W.map (residue A)).toAffine.negY (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩) := by
  rw [A.residue_eq_of_coe_eq hmem (v := ⟨y₁, hy₁⟩ - W.toAffine.negY ⟨x₂, hx₂⟩ ⟨y₂, hy₂⟩)
    (by push_cast; rw [coe_negY hx₂ hy₂]), map_sub, residue_negY hx₂ hy₂]

lemma residue_inverse_iff {x₁ y₁ x₂ y₂ : L} (hx₁ : x₁ ∈ A) (hy₁ : y₁ ∈ A) (hx₂ : x₂ ∈ A)
    (hy₂ : y₂ ∈ A) :
    (residue A ⟨x₁, hx₁⟩ = residue A ⟨x₂, hx₂⟩ ∧
        residue A ⟨y₁, hy₁⟩ =
          (W.map (residue A)).toAffine.negY (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩)) ↔
      (x₁ - x₂ ∈ A.nonunits ∧
        y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits) := by
  have hnegA : (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A := negY_mem hx₂ hy₂
  have h1 := A.residue_eq_residue_iff_sub_mem_nonunits hx₁ hx₂
  have h2 := A.residue_eq_residue_iff_sub_mem_nonunits hy₁ hnegA
  have h3 : residue A ⟨(W.map A.subtype).toAffine.negY x₂ y₂, hnegA⟩ =
      (W.map (residue A)).toAffine.negY (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩) := by
    rw [A.residue_eq_of_coe_eq hnegA (v := W.toAffine.negY ⟨x₂, hx₂⟩ ⟨y₂, hy₂⟩)
      (coe_negY hx₂ hy₂).symm]
    exact residue_negY hx₂ hy₂
  rw [← h3]
  exact and_congr h1 h2

end Coercion

section Slope

variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable {W}

theorem slope_mem_residue_of_not_inverse
    {x₁ y₁ x₂ y₂ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁)
    (h₂ : (W.map A.subtype).toAffine.Equation x₂ y₂) (hx₁ : x₁ ∈ A) (hx₂ : x₂ ∈ A)
    (hred : ¬(x₁ - x₂ ∈ A.nonunits ∧
      y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits)) :
    ∃ hs : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ ∈ A,
      residue A ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hs⟩ =
        (W.map (residue A)).toAffine.slope (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩)
          (residue A ⟨y₁, Affine.Y_mem_of_X_mem W h₁ hx₁⟩)
          (residue A ⟨y₂, Affine.Y_mem_of_X_mem W h₂ hx₂⟩) := by
  have hy₁ : y₁ ∈ A := Affine.Y_mem_of_X_mem W h₁ hx₁
  have hy₂ : y₂ ∈ A := Affine.Y_mem_of_X_mem W h₂ hx₂
  have ha₁ : (W.map A.subtype).toAffine.a₁ ∈ A := SetLike.coe_mem W.a₁
  have ha₂ : (W.map A.subtype).toAffine.a₂ ∈ A := SetLike.coe_mem W.a₂
  have ha₄ : (W.map A.subtype).toAffine.a₄ ∈ A := SetLike.coe_mem W.a₄

  have hk₁ : (W.map (residue A)).toAffine.Equation (residue A ⟨x₁, hx₁⟩) (residue A ⟨y₁, hy₁⟩) :=
    Affine.equation_residue W (x := ⟨x₁, hx₁⟩) (y := ⟨y₁, hy₁⟩) h₁
  have hk₂ : (W.map (residue A)).toAffine.Equation (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩) :=
    Affine.equation_residue W (x := ⟨x₂, hx₂⟩) (y := ⟨y₂, hy₂⟩) h₂

  have ha₁k : (W.map (residue A)).toAffine.a₁ = residue A W.a₁ := rfl
  have ha₂k : (W.map (residue A)).toAffine.a₂ = residue A W.a₂ := rfl
  have ha₄k : (W.map (residue A)).toAffine.a₄ = residue A W.a₄ := rfl
  by_cases hxx : x₁ - x₂ ∈ A.nonunits
  ·

    have hyy : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∉ A.nonunits := fun h => hred ⟨hxx, h⟩
    have hyyA : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A :=
      A.toSubring.sub_mem hy₁ (negY_mem hx₂ hy₂)
    have hyy0 : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ≠ 0 :=
      A.ne_zero_of_notMem_nonunits hyy

    have hxk : residue A ⟨x₁, hx₁⟩ = residue A ⟨x₂, hx₂⟩ :=
      (A.residue_eq_residue_iff_sub_mem_nonunits hx₁ hx₂).mpr hxx
    have hyk : residue A ⟨y₁, hy₁⟩ ≠
        (W.map (residue A)).toAffine.negY (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩) := by
      intro h
      exact hyy (((residue_inverse_iff hx₁ hy₁ hx₂ hy₂).mp ⟨hxk, h⟩).2)

    have hyk' : residue A ⟨y₁, hy₁⟩ = residue A ⟨y₂, hy₂⟩ :=
      Affine.Y_eq_of_Y_ne hk₁ hk₂ hxk hyk
    have hslope_k : (W.map (residue A)).toAffine.slope (residue A ⟨x₁, hx₁⟩)
        (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₁, hy₁⟩) (residue A ⟨y₂, hy₂⟩) =
        (3 * residue A ⟨x₁, hx₁⟩ ^ 2 + 2 * (W.map (residue A)).toAffine.a₂ *
            residue A ⟨x₁, hx₁⟩ + (W.map (residue A)).toAffine.a₄ -
            (W.map (residue A)).toAffine.a₁ * residue A ⟨y₁, hy₁⟩) /
          (residue A ⟨y₁, hy₁⟩ -
            (W.map (residue A)).toAffine.negY (residue A ⟨x₁, hx₁⟩) (residue A ⟨y₁, hy₁⟩)) :=
      Affine.slope_of_Y_ne hxk hyk

    have hden_res : residue A ⟨y₁ - (W.map A.subtype).toAffine.negY x₂ y₂, hyyA⟩ =
        residue A ⟨y₁, hy₁⟩ -
          (W.map (residue A)).toAffine.negY (residue A ⟨x₁, hx₁⟩) (residue A ⟨y₁, hy₁⟩) := by
      rw [residue_sub_negY hy₁ hx₂ hy₂ hyyA, hxk, hyk']

    have hnum_mem : 3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ +
        (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁ ∈ A := by
      refine A.toSubring.sub_mem (A.toSubring.add_mem (A.toSubring.add_mem ?_ ?_) ha₄)
        (A.toSubring.mul_mem ha₁ hy₁)
      · exact A.toSubring.mul_mem (by norm_num : (3 : L) ∈ A) (pow_mem hx₁ 2)
      · exact A.toSubring.mul_mem (A.toSubring.mul_mem (by norm_num : (2 : L) ∈ A) ha₂) hx₁
    have hnum_res : residue A ⟨3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ +
        (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁, hnum_mem⟩ =
        3 * residue A ⟨x₁, hx₁⟩ ^ 2 + 2 * (W.map (residue A)).toAffine.a₂ *
          residue A ⟨x₁, hx₁⟩ + (W.map (residue A)).toAffine.a₄ -
          (W.map (residue A)).toAffine.a₁ * residue A ⟨y₁, hy₁⟩ := by
      rw [A.residue_eq_of_coe_eq hnum_mem
        (v := 3 * ⟨x₁, hx₁⟩ ^ 2 + 2 * W.a₂ * ⟨x₁, hx₁⟩ + W.a₄ - W.a₁ * ⟨y₁, hy₁⟩)
        (by push_cast; rfl)]
      simp only [map_sub, map_add, map_mul, map_pow, map_ofNat]
      rw [ha₁k, ha₂k, ha₄k]
    by_cases hx : x₁ = x₂
    ·
      have hyL : y₁ ≠ (W.map A.subtype).toAffine.negY x₂ y₂ := fun h => hyy0 (by rw [h, sub_self])
      have hyL' : y₁ = y₂ := Affine.Y_eq_of_Y_ne h₁ h₂ hx hyL
      have hslope_L : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ =
          (3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ +
              (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁) /
            (y₁ - (W.map A.subtype).toAffine.negY x₁ y₁) :=
        Affine.slope_of_Y_ne hx hyL
      have hden_eq : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ =
          y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ := by
        rw [hx, hyL']
      have hslope_L' : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ =
          (3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ +
              (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁) /
            (y₁ - (W.map A.subtype).toAffine.negY x₂ y₂) := by
        rw [hslope_L, hden_eq]
      have hsmem : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ ∈ A := by
        rw [hslope_L']
        exact A.div_mem_of_mem_of_notMem_nonunits hnum_mem hyy
      refine ⟨hsmem, ?_⟩
      rw [A.residue_eq_div_of_eq_div hsmem hnum_mem hyyA hyy hslope_L', hslope_k, hnum_res,
        hden_res]
    ·

      have hslope_L : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂) :=
        Affine.slope_of_X_ne hx
      have hN_mem : x₁ ^ 2 + x₁ * x₂ + x₂ ^ 2 + (W.map A.subtype).toAffine.a₂ * (x₁ + x₂) +
          (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁ ∈ A := by
        refine A.toSubring.sub_mem (A.toSubring.add_mem (A.toSubring.add_mem (A.toSubring.add_mem
          (A.toSubring.add_mem (pow_mem hx₁ 2) (A.toSubring.mul_mem hx₁ hx₂)) (pow_mem hx₂ 2))
          (A.toSubring.mul_mem ha₂ (A.toSubring.add_mem hx₁ hx₂))) ha₄)
          (A.toSubring.mul_mem ha₁ hy₁)

      have hslope_N : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ =
          (x₁ ^ 2 + x₁ * x₂ + x₂ ^ 2 + (W.map A.subtype).toAffine.a₂ * (x₁ + x₂) +
              (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁) /
            (y₁ - (W.map A.subtype).toAffine.negY x₂ y₂) := by
        rw [hslope_L, div_eq_div_iff (sub_ne_zero.mpr hx) hyy0]
        linear_combination Affine.sub_mul_sub_negY h₁ h₂
      have hsmem : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ ∈ A := by
        rw [hslope_N]
        exact A.div_mem_of_mem_of_notMem_nonunits hN_mem hyy
      refine ⟨hsmem, ?_⟩

      have hN_res : residue A ⟨x₁ ^ 2 + x₁ * x₂ + x₂ ^ 2 +
          (W.map A.subtype).toAffine.a₂ * (x₁ + x₂) + (W.map A.subtype).toAffine.a₄ -
          (W.map A.subtype).toAffine.a₁ * y₁, hN_mem⟩ =
          3 * residue A ⟨x₁, hx₁⟩ ^ 2 + 2 * (W.map (residue A)).toAffine.a₂ *
            residue A ⟨x₁, hx₁⟩ + (W.map (residue A)).toAffine.a₄ -
            (W.map (residue A)).toAffine.a₁ * residue A ⟨y₁, hy₁⟩ := by
        rw [A.residue_eq_of_coe_eq hN_mem
          (v := ⟨x₁, hx₁⟩ ^ 2 + ⟨x₁, hx₁⟩ * ⟨x₂, hx₂⟩ + ⟨x₂, hx₂⟩ ^ 2 +
            W.a₂ * (⟨x₁, hx₁⟩ + ⟨x₂, hx₂⟩) + W.a₄ - W.a₁ * ⟨y₁, hy₁⟩)
          (by push_cast; rfl)]
        simp only [map_sub, map_add, map_mul, map_pow]
        rw [ha₁k, ha₂k, ha₄k, ← hxk]
        ring
      rw [A.residue_eq_div_of_eq_div hsmem hN_mem hyyA hyy hslope_N, hslope_k, hN_res, hden_res]
  ·
    have hxL : x₁ ≠ x₂ := fun h => hxx (by rw [h, sub_self]; exact A.nonunits.zero_mem)
    have hxxA : x₁ - x₂ ∈ A := A.toSubring.sub_mem hx₁ hx₂
    have hslope_L : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂) :=
      Affine.slope_of_X_ne hxL
    have hyyA : y₁ - y₂ ∈ A := A.toSubring.sub_mem hy₁ hy₂
    have hsmem : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ ∈ A := by
      rw [hslope_L]
      exact A.div_mem_of_mem_of_notMem_nonunits hyyA hxx
    refine ⟨hsmem, ?_⟩

    have hxk : residue A ⟨x₁, hx₁⟩ ≠ residue A ⟨x₂, hx₂⟩ := fun h =>
      hxx ((A.residue_eq_residue_iff_sub_mem_nonunits hx₁ hx₂).mp h)
    have hslope_k : (W.map (residue A)).toAffine.slope (residue A ⟨x₁, hx₁⟩)
        (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₁, hy₁⟩) (residue A ⟨y₂, hy₂⟩) =
        (residue A ⟨y₁, hy₁⟩ - residue A ⟨y₂, hy₂⟩) /
          (residue A ⟨x₁, hx₁⟩ - residue A ⟨x₂, hx₂⟩) := Affine.slope_of_X_ne hxk
    have hnum_eq : residue A ⟨y₁ - y₂, hyyA⟩ = residue A ⟨y₁, hy₁⟩ - residue A ⟨y₂, hy₂⟩ := by
      rw [A.residue_eq_of_coe_eq hyyA (v := ⟨y₁, hy₁⟩ - ⟨y₂, hy₂⟩) (by push_cast; ring), map_sub]
    have hden_eq : residue A ⟨x₁ - x₂, hxxA⟩ = residue A ⟨x₁, hx₁⟩ - residue A ⟨x₂, hx₂⟩ := by
      rw [A.residue_eq_of_coe_eq hxxA (v := ⟨x₁, hx₁⟩ - ⟨x₂, hx₂⟩) (by push_cast; ring), map_sub]
    rw [A.residue_eq_div_of_eq_div hsmem hyyA hxxA hxx hslope_L, hslope_k, hnum_eq, hden_eq]

end Slope

section IntegralCase

variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable {W} (hΔ : (W.map (residue A)).Δ ≠ 0)

set_option maxHeartbeats 1600000 in

theorem reducePoint_add_of_mem {x₁ y₁ x₂ y₂ : L}
    (h₁ : (W.map A.subtype).toAffine.Nonsingular x₁ y₁)
    (h₂ : (W.map A.subtype).toAffine.Nonsingular x₂ y₂) (hx₁ : x₁ ∈ A) (hx₂ : x₂ ∈ A) :
    reducePoint hΔ (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) =
      reducePoint hΔ (.some x₁ y₁ h₁) + reducePoint hΔ (.some x₂ y₂ h₂) := by
  have hy₁ : y₁ ∈ A := Affine.Y_mem_of_X_mem W h₁.1 hx₁
  have hy₂ : y₂ ∈ A := Affine.Y_mem_of_X_mem W h₂.1 hx₂

  rw [reducePoint_some_of_mem _ _ hx₁, reducePoint_some_of_mem _ _ hx₂]
  by_cases hred : x₁ - x₂ ∈ A.nonunits ∧
      y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits
  ·
    obtain ⟨hredx, hredy⟩ := (residue_inverse_iff hx₁ hy₁ hx₂ hy₂).mpr hred
    rw [Affine.Point.add_of_Y_eq hredx hredy]
    by_cases hPQ : x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂
    ·
      rw [Affine.Point.add_of_Y_eq hPQ.1 hPQ.2, reducePoint_zero]
    ·

      rw [Affine.Point.add_some hPQ]
      exact reducePoint_some_of_notMem _ _
        (Affine.addX_notMem_of_sub_mem_nonunits W hΔ h₁.1 h₂.1 hx₁ hx₂ hPQ hred.1 hred.2)
  ·

    obtain ⟨hsmem, hsres⟩ := slope_mem_residue_of_not_inverse h₁.1 h₂.1 hx₁ hx₂ hred

    have hPQ : ¬(x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂) := by
      rintro ⟨hxe, hye⟩
      exact hred ⟨by rw [hxe, sub_self]; exact A.nonunits.zero_mem,
        by rw [hye, sub_self]; exact A.nonunits.zero_mem⟩

    have hredk : ¬(residue A ⟨x₁, hx₁⟩ = residue A ⟨x₂, hx₂⟩ ∧
        residue A ⟨y₁, hy₁⟩ =
          (W.map (residue A)).toAffine.negY (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩)) :=
      fun h => hred ((residue_inverse_iff hx₁ hy₁ hx₂ hy₂).mp h)
    rw [Affine.Point.add_some hPQ, Affine.Point.add_some hredk]

    have hX_coe : (W.map A.subtype).toAffine.addX x₁ x₂
        ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) =
        ((W.toAffine.addX ⟨x₁, hx₁⟩ ⟨x₂, hx₂⟩
          ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩ : A) : L) :=
      Affine.map_addX (W' := W) A.subtype (⟨x₁, hx₁⟩ : A) (⟨x₂, hx₂⟩ : A)
        ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩
    have hY_coe : (W.map A.subtype).toAffine.addY x₁ x₂ y₁
        ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) =
        ((W.toAffine.addY ⟨x₁, hx₁⟩ ⟨x₂, hx₂⟩ ⟨y₁, hy₁⟩
          ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩ : A) : L) :=
      Affine.map_addY (W' := W) A.subtype (⟨x₁, hx₁⟩ : A) (⟨y₁, hy₁⟩ : A) (⟨x₂, hx₂⟩ : A)
        ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩
    have hX_mem : (W.map A.subtype).toAffine.addX x₁ x₂
        ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∈ A := by
      rw [hX_coe]; exact SetLike.coe_mem _
    rw [reducePoint_some_of_mem _ _ hX_mem]
    refine some_congr' ?_ ?_ _ _
    ·
      calc residue A ⟨(W.map A.subtype).toAffine.addX x₁ x₂
              ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂), hX_mem⟩
          = residue A (W.toAffine.addX ⟨x₁, hx₁⟩ ⟨x₂, hx₂⟩
              ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩) :=
            A.residue_eq_of_coe_eq hX_mem hX_coe
        _ = (W.map (residue A)).toAffine.addX (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩)
              (residue A ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩) :=
            (Affine.map_addX (W' := W) (residue A) (⟨x₁, hx₁⟩ : A) (⟨x₂, hx₂⟩ : A)
              ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩).symm
        _ = _ := by rw [hsres]
    ·
      calc residue A ⟨(W.map A.subtype).toAffine.addY x₁ x₂ y₁
              ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂),
              Affine.Y_mem_of_X_mem W (Affine.nonsingular_add h₁ h₂ hPQ).1 hX_mem⟩
          = residue A (W.toAffine.addY ⟨x₁, hx₁⟩ ⟨x₂, hx₂⟩ ⟨y₁, hy₁⟩
              ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩) :=
            A.residue_eq_of_coe_eq _ hY_coe
        _ = (W.map (residue A)).toAffine.addY (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩)
              (residue A ⟨y₁, hy₁⟩)
              (residue A ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩) :=
            (Affine.map_addY (W' := W) (residue A) (⟨x₁, hx₁⟩ : A) (⟨y₁, hy₁⟩ : A)
              (⟨x₂, hx₂⟩ : A)
              ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩).symm
        _ = _ := by rw [hsres]

end IntegralCase

section KernelCase

variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable {W} (hΔ : (W.map (residue A)).Δ ≠ 0)

theorem reducePoint_add_of_notMem_of_notMem {x₁ y₁ x₂ y₂ : L}
    (h₁ : (W.map A.subtype).toAffine.Nonsingular x₁ y₁)
    (h₂ : (W.map A.subtype).toAffine.Nonsingular x₂ y₂) (hx₁ : x₁ ∉ A) (hx₂ : x₂ ∉ A) :
    reducePoint hΔ (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) =
      reducePoint hΔ (.some x₁ y₁ h₁) + reducePoint hΔ (.some x₂ y₂ h₂) := by

  rw [reducePoint_some_of_notMem _ _ hx₁, reducePoint_some_of_notMem _ _ hx₂, add_zero]
  by_cases hPQ : x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂
  · rw [Affine.Point.add_of_Y_eq hPQ.1 hPQ.2, reducePoint_zero]
  ·

    have hy₁0 : y₁ ≠ 0 := Affine.Y_ne_zero_of_X_notMem W h₁.1 hx₁
    have hy₂0 : y₂ ≠ 0 := Affine.Y_ne_zero_of_X_notMem W h₂.1 hx₂
    have hx₁0 : x₁ ≠ 0 := fun h => hx₁ (h ▸ A.zero_mem)
    have hx₂0 : x₂ ≠ 0 := fun h => hx₂ (h ▸ A.zero_mem)
    have ht₁m : x₁ / y₁ ∈ A.nonunits := Affine.X_div_Y_mem_nonunits W h₁.1 hx₁
    have ht₂m : x₂ / y₂ ∈ A.nonunits := Affine.X_div_Y_mem_nonunits W h₂.1 hx₂
    have ht₁0 : x₁ / y₁ ≠ 0 := div_ne_zero hx₁0 hy₁0
    have ht₂0 : x₂ / y₂ ≠ 0 := div_ne_zero hx₂0 hy₂0
    have haddX : (W.map A.subtype).toAffine.addX x₁ x₂
        ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∉ A := by
      rcases A.mem_or_inv_mem ((x₁ / y₁) / (x₂ / y₂)) with hcase | hcase
      ·
        refine (Affine.add_formal_param_estimate h₁.1 h₂.1 hx₁ hx₂ hPQ ht₂m ht₂0 hcase ?_).1
        rw [div_self ht₂0]
        exact A.one_mem
      ·
        rw [show ((x₁ / y₁) / (x₂ / y₂))⁻¹ = (x₂ / y₂) / (x₁ / y₁) by rw [inv_div]] at hcase
        refine (Affine.add_formal_param_estimate h₁.1 h₂.1 hx₁ hx₂ hPQ ht₁m ht₁0 ?_ hcase).1
        rw [div_self ht₁0]
        exact A.one_mem
    rw [Affine.Point.add_some hPQ]
    exact reducePoint_some_of_notMem _ _ haddX

end KernelCase

section MixedCase

variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable {W} (hΔ : (W.map (residue A)).Δ ≠ 0)

theorem reducePoint_add_of_mem_of_notMem {x₁ y₁ x₂ y₂ : L}
    (h₁ : (W.map A.subtype).toAffine.Nonsingular x₁ y₁)
    (h₂ : (W.map A.subtype).toAffine.Nonsingular x₂ y₂) (hx₁ : x₁ ∈ A) (hx₂ : x₂ ∉ A) :
    reducePoint hΔ (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) =
      reducePoint hΔ (.some x₁ y₁ h₁) + reducePoint hΔ (.some x₂ y₂ h₂) := by

  rw [reducePoint_some_of_notMem _ _ hx₂, add_zero]

  have hPn : (W.map A.subtype).toAffine.Nonsingular x₁ ((W.map A.subtype).toAffine.negY x₁ y₁) :=
    (Affine.nonsingular_neg _ _).mpr h₁
  have hQn : (W.map A.subtype).toAffine.Nonsingular x₂ ((W.map A.subtype).toAffine.negY x₂ y₂) :=
    (Affine.nonsingular_neg _ _).mpr h₂
  have hPneg : (.some x₁ ((W.map A.subtype).toAffine.negY x₁ y₁) hPn :
      (W.map A.subtype).toAffine.Point) = -(.some x₁ y₁ h₁) := (Affine.Point.neg_some h₁).symm
  have hQneg : (.some x₂ ((W.map A.subtype).toAffine.negY x₂ y₂) hQn :
      (W.map A.subtype).toAffine.Point) = -(.some x₂ y₂ h₂) := (Affine.Point.neg_some h₂).symm

  cases hadd : (.some x₁ y₁ h₁ + .some x₂ y₂ h₂ : (W.map A.subtype).toAffine.Point) with
  | zero =>

    exfalso
    have hP : (.some x₁ y₁ h₁ : (W.map A.subtype).toAffine.Point) = -(.some x₂ y₂ h₂) :=
      eq_neg_of_add_eq_zero_left hadd
    rw [← hQneg] at hP
    simp only [Affine.Point.some.injEq] at hP
    exact hx₂ (hP.1 ▸ hx₁)
  | some X₃ Y₃ h₃ =>
    by_cases hX₃ : X₃ ∈ A
    ·
      have hint := reducePoint_add_of_mem hΔ h₃ hPn hX₃ hx₁
      have hSnegP : (.some X₃ Y₃ h₃ : (W.map A.subtype).toAffine.Point) +
          .some x₁ ((W.map A.subtype).toAffine.negY x₁ y₁) hPn = .some x₂ y₂ h₂ := by
        rw [hPneg, ← hadd]; abel
      rw [hSnegP, reducePoint_some_of_notMem _ _ hx₂, hPneg, reducePoint_neg,
        ← sub_eq_add_neg] at hint
      exact (sub_eq_zero.mp hint.symm)
    ·
      exfalso
      have hker := reducePoint_add_of_notMem_of_notMem hΔ h₃ hQn hX₃ hx₂
      have hSnegQ : (.some X₃ Y₃ h₃ : (W.map A.subtype).toAffine.Point) +
          .some x₂ ((W.map A.subtype).toAffine.negY x₂ y₂) hQn = .some x₁ y₁ h₁ := by
        rw [hQneg, ← hadd]; abel
      rw [hSnegQ, reducePoint_some_of_mem _ _ hx₁, reducePoint_some_of_notMem _ _ hX₃,
        reducePoint_some_of_notMem _ _ hx₂, add_zero] at hker
      injection hker

end MixedCase

section Homomorphism

variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable {W} (hΔ : (W.map (residue A)).Δ ≠ 0)

theorem reducePoint_add_def (P Q : (W.map A.subtype).toAffine.Point) :
    reducePoint hΔ (P + Q) = reducePoint hΔ P + reducePoint hΔ Q := by
  cases P with
  | zero =>
    show reducePoint hΔ ((0 : (W.map A.subtype).toAffine.Point) + Q) =
      reducePoint hΔ (0 : (W.map A.subtype).toAffine.Point) + reducePoint hΔ Q
    rw [zero_add, reducePoint_zero, zero_add]
  | some x₁ y₁ h₁ =>
    cases Q with
    | zero =>
      show reducePoint hΔ (.some x₁ y₁ h₁ + (0 : (W.map A.subtype).toAffine.Point)) =
        reducePoint hΔ (.some x₁ y₁ h₁) + reducePoint hΔ (0 : (W.map A.subtype).toAffine.Point)
      rw [add_zero, reducePoint_zero, add_zero]
    | some x₂ y₂ h₂ =>
      by_cases hx₁ : x₁ ∈ A <;> by_cases hx₂ : x₂ ∈ A
      · exact reducePoint_add_of_mem hΔ h₁ h₂ hx₁ hx₂
      · exact reducePoint_add_of_mem_of_notMem hΔ h₁ h₂ hx₁ hx₂
      · rw [add_comm, add_comm (reducePoint hΔ (.some x₁ y₁ h₁))]
        exact reducePoint_add_of_mem_of_notMem hΔ h₂ h₁ hx₂ hx₁
      · exact reducePoint_add_of_notMem_of_notMem hΔ h₁ h₂ hx₁ hx₂

noncomputable def reduceHom :
    (W.map A.subtype).toAffine.Point →+ (W.map (residue A)).toAffine.Point where
  toFun := reducePoint hΔ
  map_zero' := reducePoint_zero hΔ
  map_add' := reducePoint_add_def hΔ

end Homomorphism

end WeierstrassCurve

Statements phrased using this module (30)