import Mathlib import Definitions.Def_WeierstrassCurve_ReduceHom set_option autoImplicit false open IsLocalRing Finset namespace ValuationSubring variable {L : Type*} [Field L] (A : ValuationSubring L) theorem valuation_eq_one_of_notMem_nonunits {a : L} (haA : a ∈ A) (ha : a ∉ A.nonunits) : A.valuation a = 1 := le_antisymm ((A.valuation_le_one_iff a).mpr haA) (not_lt.mp fun h => ha (A.mem_nonunits_iff.mpr h)) theorem natCast_mem (n : ℕ) : (n : L) ∈ A := by simp theorem valuation_natCast_eq_one {n : ℕ} (hn : (n : L) ∉ A.nonunits) : A.valuation (n : L) = 1 := A.valuation_eq_one_of_notMem_nonunits (A.natCast_mem n) hn end ValuationSubring variable {L : Type*} [Field L] structure FormalCoordinates (A : ValuationSubring L) (G : Type*) [AddCommGroup G] (d : ℕ) where disc : AddSubgroup G coord : G → Fin d → L coord_mem_nonunits : ∀ P ∈ disc, ∀ i, coord P i ∈ A.nonunits eq_zero_of_coord_eq_zero : ∀ P ∈ disc, (∀ i, coord P i = 0) → P = 0 coord_zero : ∀ i, coord 0 i = 0 coord_nsmul_sub : ∀ P ∈ disc, ∀ (n : ℕ) (i : Fin d), ∃ c : Fin d → L, (∀ j, c j ∈ A.nonunits) ∧ coord (n • P) i - n * coord P i = ∑ j, c j * coord P j namespace FormalCoordinates variable {A : ValuationSubring L} {G : Type*} [AddCommGroup G] {d : ℕ} theorem exists_dominant_coord (F : FormalCoordinates A G d) {P : G} {i₁ : Fin d} (hi₁ : F.coord P i₁ ≠ 0) : ∃ i₀, F.coord P i₀ ≠ 0 ∧ ∀ j, A.valuation (F.coord P j) ≤ A.valuation (F.coord P i₀) := by obtain ⟨i₀, -, hi₀⟩ := Finset.exists_max_image Finset.univ (fun i => A.valuation (F.coord P i)) ⟨i₁, Finset.mem_univ _⟩ refine ⟨i₀, fun h0 => hi₁ ?_, fun j => hi₀ j (Finset.mem_univ _)⟩ have h := hi₀ i₁ (Finset.mem_univ _) rw [h0, map_zero, le_zero_iff] at h exact (Valuation.zero_iff _).mp h theorem eq_zero_of_nsmul_eq_zero (F : FormalCoordinates A G d) {n : ℕ} (hn : (n : L) ∉ A.nonunits) {P : G} (hP : P ∈ F.disc) (h : n • P = 0) : P = 0 := by by_contra hP0 obtain ⟨i₁, hi₁⟩ : ∃ i, F.coord P i ≠ 0 := by by_contra hall push Not at hall exact hP0 (F.eq_zero_of_coord_eq_zero P hP hall) obtain ⟨i₀, hi₀ne, hi₀⟩ := F.exists_dominant_coord hi₁ have hv₀ : A.valuation (F.coord P i₀) ≠ 0 := (Valuation.ne_zero_iff _).mpr hi₀ne obtain ⟨c, hc, hest⟩ := F.coord_nsmul_sub P hP n i₀ have hcorr : A.valuation (∑ j, c j * F.coord P j) < A.valuation (F.coord P i₀) := by refine Valuation.map_sum_lt _ hv₀ fun j _ => ?_ rw [map_mul] calc A.valuation (c j) * A.valuation (F.coord P j) ≤ A.valuation (c j) * A.valuation (F.coord P i₀) := by gcongr exact hi₀ j _ = A.valuation (F.coord P i₀) * A.valuation (c j) := mul_comm _ _ _ < A.valuation (F.coord P i₀) * 1 := by have hk : A.valuation (c j) < 1 := A.mem_nonunits_iff.mp (hc j) exact lt_of_le_of_ne (mul_le_mul_right hk.le _) fun heq => (ne_of_lt hk) (mul_left_cancel₀ hv₀ heq) _ = A.valuation (F.coord P i₀) := mul_one _ have hlead : A.valuation ((n : L) * F.coord P i₀) = A.valuation (F.coord P i₀) := by rw [map_mul, A.valuation_natCast_eq_one hn, one_mul] have hkey : A.valuation (F.coord (n • P) i₀) = A.valuation (F.coord P i₀) := by have hsum : F.coord (n • P) i₀ = (n : L) * F.coord P i₀ + ∑ j, c j * F.coord P j := by rw [← hest]; ring rw [hsum, Valuation.map_add_eq_of_lt_left _ (hlead.symm ▸ hcorr), hlead] rw [h, F.coord_zero i₀, map_zero] at hkey exact hv₀ hkey.symm def additive (A : ValuationSubring L) (d : ℕ) : FormalCoordinates A (Fin d → L) d where disc := AddSubgroup.pi Set.univ fun _ => A.nonunits.toAddSubgroup coord f := f coord_mem_nonunits f hf i := hf i (Set.mem_univ i) eq_zero_of_coord_eq_zero f _ hf := funext hf coord_zero _ := rfl coord_nsmul_sub f _ n i := by refine ⟨fun _ => 0, fun _ => A.nonunits.zero_mem, ?_⟩ simp [Pi.smul_apply, nsmul_eq_mul] end FormalCoordinates set_option autoImplicit false namespace ModularCurve namespace ElevenA1 open WeierstrassCurve Affine section Count variable {K : Type*} [CommRing K] (W : WeierstrassCurve.Affine K) instance instDecidableEquation [DecidableEq K] (x y : K) : Decidable (W.Equation x y) := decidable_of_iff _ (W.equation_iff x y).symm instance instDecidableNonsingular [DecidableEq K] (x y : K) : Decidable (W.Nonsingular x y) := decidable_of_iff _ (W.nonsingular_iff x y).symm end Count end ElevenA1 end ModularCurve set_option autoImplicit false open IsLocalRing ValuationSubring WeierstrassCurve.Affine WeierstrassCurve.Affine.Point namespace WeierstrassCurve variable {L : Type*} [Field L] {A : ValuationSubring L} (W : WeierstrassCurve A) def formalParam : (W.map A.subtype).toAffine.Point → L | .zero => 0 | .some x y _ => -(x / y) @[simp] theorem formalParam_zero : W.formalParam 0 = 0 := rfl @[simp] theorem formalParam_some {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) : W.formalParam (some x y h) = -(x / y) := rfl def IsNonIntegral (P : (W.map A.subtype).toAffine.Point) : Prop := ∀ x y (h : (W.map A.subtype).toAffine.Nonsingular x y), P = some x y h → x ∉ A theorem isNonIntegral_zero : W.IsNonIntegral 0 := fun _ _ h heq => absurd heq (Ne.symm (some_ne_zero h)) theorem isNonIntegral_some_iff {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) : W.IsNonIntegral (some x y h) ↔ x ∉ A := by refine ⟨fun hP => hP x y h rfl, fun hx x' y' h' heq => ?_⟩ obtain ⟨rfl, rfl⟩ : x = x' ∧ y = y' := by rwa [Affine.Point.some.injEq] at heq exact hx theorem exists_common_depth {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) : ∃ τ : L, τ ∈ A.nonunits ∧ τ ≠ 0 ∧ (x₁ / y₁) / τ ∈ A ∧ (x₂ / y₂) / τ ∈ A := by have hy₁0 : y₁ ≠ 0 := Y_ne_zero_of_X_notMem W h₁ hx₁ have hy₂0 : y₂ ≠ 0 := Y_ne_zero_of_X_notMem W h₂ hx₂ have hx₁0 : x₁ ≠ 0 := fun h0 => hx₁ (h0 ▸ A.zero_mem) have hx₂0 : x₂ ≠ 0 := fun h0 => hx₂ (h0 ▸ A.zero_mem) 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 rcases A.mem_or_inv_mem ((x₁ / y₁) / (x₂ / y₂)) with hd | hd · exact ⟨x₂ / y₂, X_div_Y_mem_nonunits W h₂ hx₂, ht₂0, hd, by rw [div_self ht₂0]; exact A.one_mem⟩ · rw [show ((x₁ / y₁) / (x₂ / y₂))⁻¹ = (x₂ / y₂) / (x₁ / y₁) by rw [inv_div]] at hd exact ⟨x₁ / y₁, X_div_Y_mem_nonunits W h₁ hx₁, ht₁0, by rw [div_self ht₁0]; exact A.one_mem, hd⟩ variable [DecidableEq L] def nonIntegralLocus : AddSubgroup (W.map A.subtype).toAffine.Point where carrier := {P | W.IsNonIntegral P} zero_mem' := W.isNonIntegral_zero neg_mem' := by rintro (_ | @⟨a, b, hab⟩) hP · exact W.isNonIntegral_zero · rw [neg_some] exact (W.isNonIntegral_some_iff _).mpr ((W.isNonIntegral_some_iff hab).mp hP) add_mem' := by rintro (_ | @⟨x₁, y₁, h₁⟩) (_ | @⟨x₂, y₂, h₂⟩) hP hQ · simpa [← Affine.Point.zero_def] using W.isNonIntegral_zero · simpa [← Affine.Point.zero_def] using hQ · simpa [← Affine.Point.zero_def] using hP · have hx₁ : x₁ ∉ A := (W.isNonIntegral_some_iff h₁).mp hP have hx₂ : x₂ ∉ A := (W.isNonIntegral_some_iff h₂).mp hQ by_cases hxy : x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂ · rw [add_of_Y_eq hxy.1 hxy.2] exact W.isNonIntegral_zero · rw [add_some hxy] obtain ⟨τ, hτ, hτ0, ht₁, ht₂⟩ := W.exists_common_depth h₁.1 h₂.1 hx₁ hx₂ exact (W.isNonIntegral_some_iff _).mpr (add_formal_param_estimate (W := W) h₁.1 h₂.1 hx₁ hx₂ hxy hτ hτ0 ht₁ ht₂).1 theorem mem_nonIntegralLocus_some_iff {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) : some x y h ∈ W.nonIntegralLocus ↔ x ∉ A := W.isNonIntegral_some_iff h def formalCoordinates : FormalCoordinates A (W.map A.subtype).toAffine.Point 1 where disc := W.nonIntegralLocus coord P _ := W.formalParam P coord_mem_nonunits := by rintro (_ | @⟨x, y, h⟩) hP i · exact A.nonunits.zero_mem · exact A.nonunits.neg_mem (X_div_Y_mem_nonunits W h.1 ((W.mem_nonIntegralLocus_some_iff h).mp hP)) eq_zero_of_coord_eq_zero := by rintro (_ | @⟨x, y, h⟩) hP hcoord · rfl · exfalso have hx : x ∉ A := (W.mem_nonIntegralLocus_some_iff h).mp hP have hy0 : y ≠ 0 := Y_ne_zero_of_X_notMem W h.1 hx have h0 := hcoord 0 rw [formalParam_some, neg_eq_zero, div_eq_zero_iff] at h0 exact hx ((h0.resolve_right hy0) ▸ A.zero_mem) coord_zero _ := rfl coord_nsmul_sub := by rintro (_ | @⟨x, y, h⟩) hP n i · exact ⟨fun _ => 0, fun _ => A.nonunits.zero_mem, by simp [← Affine.Point.zero_def]⟩ · have hx : x ∉ A := (W.mem_nonIntegralLocus_some_iff h).mp hP have hy0 : y ≠ 0 := Y_ne_zero_of_X_notMem W h.1 hx have hx0 : x ≠ 0 := fun h0 => hx (h0 ▸ A.zero_mem) have hτ0 : -(x / y) ≠ 0 := neg_ne_zero.mpr (div_ne_zero hx0 hy0) obtain ⟨hzero, haffine⟩ := formal_param_nsmul (W := W) h hx n rcases hnP : (n • (some x y h : (W.map A.subtype).toAffine.Point)) with _ | @⟨x', y', h'⟩ · refine ⟨fun _ => -(n : L), fun _ => A.nonunits.neg_mem (hzero hnP), ?_⟩ simp only [Fin.sum_univ_one, ← Affine.Point.zero_def, formalParam_zero, formalParam_some] ring · obtain ⟨-, hcong⟩ := haffine x' y' h' hnP refine ⟨fun _ => -(x' / y') / -(x / y) - (n : L), fun _ => hcong, ?_⟩ simp only [Fin.sum_univ_one, formalParam_some] rw [sub_mul, div_mul_cancel₀ _ hτ0] theorem X_mem_of_nsmul_eq_zero_of_formalCoordinates {n : ℕ} (hn : (n : ResidueField A) ≠ 0) {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) (hP : n • (some x y h : (W.map A.subtype).toAffine.Point) = 0) : x ∈ A := by by_contra hx refine some_ne_zero h (W.formalCoordinates.eq_zero_of_nsmul_eq_zero ?_ ((W.mem_nonIntegralLocus_some_iff h).mpr hx) hP) rw [A.natCast_mem_nonunits_iff_residue_eq_zero] exact hn end WeierstrassCurve set_option autoImplicit false open IsLocalRing namespace WeierstrassCurve section General variable {L : Type*} [Field L] {A : ValuationSubring L} (W : WeierstrassCurve A) def HasNonsingularReduction (P : (W.map A.subtype).toAffine.Point) : Prop := ∀ x y (h : (W.map A.subtype).toAffine.Nonsingular x y), P = .some x y h → ∀ (hx : x ∈ A) (hy : y ∈ A), (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩) theorem hasNonsingularReduction_zero : W.HasNonsingularReduction 0 := fun _ _ h heq => absurd heq (Ne.symm (Affine.Point.some_ne_zero h)) theorem hasNonsingularReduction_some_iff {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) : W.HasNonsingularReduction (.some x y h) ↔ ∀ (hx : x ∈ A) (hy : y ∈ A), (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩) := by refine ⟨fun hP hx hy => hP x y h rfl hx hy, fun hns x' y' h' heq hx' hy' => ?_⟩ obtain ⟨rfl, rfl⟩ : x = x' ∧ y = y' := by rwa [Affine.Point.some.injEq] at heq exact hns hx' hy' theorem hasNonsingularReduction_some_of_notMem {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) (hx : x ∉ A) : W.HasNonsingularReduction (.some x y h) := (W.hasNonsingularReduction_some_iff h).mpr fun hx' _ => absurd hx' hx theorem hasNonsingularReduction_of_good (hΔ : (W.map (residue A)).Δ ≠ 0) (P : (W.map A.subtype).toAffine.Point) : W.HasNonsingularReduction P := fun _ _ h _ _ _ => Affine.nonsingular_residue W hΔ h.1 theorem hasNonsingularReduction_of_isNonIntegral {P : (W.map A.subtype).toAffine.Point} (hP : W.IsNonIntegral P) : W.HasNonsingularReduction P := fun x y h heq hx _ => absurd hx (hP x y h heq) theorem hasNonsingularReduction_neg {P : (W.map A.subtype).toAffine.Point} (hP : W.HasNonsingularReduction P) : W.HasNonsingularReduction (-P) := by cases P with | zero => show W.HasNonsingularReduction (-(0 : (W.map A.subtype).toAffine.Point)) rw [Affine.Point.neg_zero] exact W.hasNonsingularReduction_zero | some x y h => rw [Affine.Point.neg_some] rw [W.hasNonsingularReduction_some_iff] at hP rw [W.hasNonsingularReduction_some_iff] intro hx hy' have hy : y ∈ A := Affine.Y_mem_of_X_mem W h.1 hx have hns := hP hx hy have hkey : residue A (⟨(W.map A.subtype).toAffine.negY x y, hy'⟩ : A) = (W.map (residue A)).toAffine.negY (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩) := by rw [A.residue_eq_of_coe_eq hy' (v := W.toAffine.negY ⟨x, hx⟩ ⟨y, hy⟩) (coe_negY hx hy).symm] exact residue_negY hx hy rw [hkey] exact (Affine.nonsingular_neg ..).mpr hns section NonIntegralLocus variable [DecidableEq L] theorem isNonIntegral_of_mem_nonIntegralLocus {P : (W.map A.subtype).toAffine.Point} (hP : P ∈ W.nonIntegralLocus) : W.IsNonIntegral P := fun _ _ h heq => (W.mem_nonIntegralLocus_some_iff h).mp (heq ▸ hP) theorem hasNonsingularReduction_of_mem_nonIntegralLocus {P : (W.map A.subtype).toAffine.Point} (hP : P ∈ W.nonIntegralLocus) : W.HasNonsingularReduction P := W.hasNonsingularReduction_of_isNonIntegral (W.isNonIntegral_of_mem_nonIntegralLocus hP) end NonIntegralLocus private lemma some_smoothLocus_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 open Classical in noncomputable def reducePointSmooth : (W.map A.subtype).toAffine.Point → (W.map (residue A)).toAffine.Point | .zero => .zero | .some x y h => if hx : x ∈ A then if hns : (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x, hx⟩) (residue A ⟨y, Affine.Y_mem_of_X_mem W h.1 hx⟩) then .some _ _ hns else .zero else .zero @[simp] theorem reducePointSmooth_zero : W.reducePointSmooth 0 = 0 := rfl theorem reducePointSmooth_some_of_mem {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) (hx : x ∈ A) {hy : y ∈ A} (hns : (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩)) : W.reducePointSmooth (.some x y h) = .some (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩) hns := by simp only [reducePointSmooth] rw [dif_pos hx] exact dif_pos hns theorem reducePointSmooth_some_of_notMem {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) (hx : x ∉ A) : W.reducePointSmooth (.some x y h) = 0 := by simp only [reducePointSmooth] exact dif_neg hx theorem reducePointSmooth_some_of_singular {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) (hx : x ∈ A) {hy : y ∈ A} (hsing : ¬ (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩)) : W.reducePointSmooth (.some x y h) = 0 := by simp only [reducePointSmooth] rw [dif_pos hx] exact dif_neg fun hcon => hsing hcon theorem reducePointSmooth_eq_reducePoint (hΔ : (W.map (residue A)).Δ ≠ 0) (P : (W.map A.subtype).toAffine.Point) : W.reducePointSmooth P = reducePoint hΔ P := by cases P with | zero => rfl | some x y h => by_cases hx : x ∈ A · rw [W.reducePointSmooth_some_of_mem h hx (Affine.nonsingular_residue W hΔ (x := ⟨x, hx⟩) (y := ⟨y, Affine.Y_mem_of_X_mem W h.1 hx⟩) h.1), reducePoint_some_of_mem _ _ hx] · rw [W.reducePointSmooth_some_of_notMem h hx, reducePoint_some_of_notMem _ _ hx] theorem reducePointSmooth_neg (P : (W.map A.subtype).toAffine.Point) : W.reducePointSmooth (-P) = -W.reducePointSmooth P := by cases P with | zero => show W.reducePointSmooth (-(0 : (W.map A.subtype).toAffine.Point)) = -W.reducePointSmooth (0 : (W.map A.subtype).toAffine.Point) rw [Affine.Point.neg_zero, reducePointSmooth_zero, Affine.Point.neg_zero] | some x y h => rw [Affine.Point.neg_some] by_cases hx : x ∈ A · have hy : y ∈ A := Affine.Y_mem_of_X_mem W h.1 hx have hy' : (W.map A.subtype).toAffine.negY x y ∈ A := negY_mem hx hy have hkey : residue A (⟨(W.map A.subtype).toAffine.negY x y, hy'⟩ : A) = (W.map (residue A)).toAffine.negY (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩) := by rw [A.residue_eq_of_coe_eq hy' (v := W.toAffine.negY ⟨x, hx⟩ ⟨y, hy⟩) (coe_negY hx hy).symm] exact residue_negY hx hy by_cases hns : (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩) · have hns' : (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x, hx⟩) (residue A ⟨(W.map A.subtype).toAffine.negY x y, hy'⟩) := by rw [hkey] exact (Affine.nonsingular_neg ..).mpr hns rw [W.reducePointSmooth_some_of_mem _ hx hns', W.reducePointSmooth_some_of_mem h hx hns, Affine.Point.neg_some] exact some_smoothLocus_congr rfl hkey _ _ · have hns' : ¬ (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x, hx⟩) (residue A ⟨(W.map A.subtype).toAffine.negY x y, hy'⟩) := by rw [hkey] intro hcon exact hns ((Affine.nonsingular_neg ..).mp hcon) rw [W.reducePointSmooth_some_of_singular _ hx hns', W.reducePointSmooth_some_of_singular h hx hns] exact (Affine.Point.neg_zero).symm · rw [W.reducePointSmooth_some_of_notMem _ hx, W.reducePointSmooth_some_of_notMem h hx] exact (Affine.Point.neg_zero).symm section Kernel variable [DecidableEq L] theorem reducePointSmooth_eq_zero_of_mem_nonIntegralLocus {P : (W.map A.subtype).toAffine.Point} (hP : P ∈ W.nonIntegralLocus) : W.reducePointSmooth P = 0 := by cases P with | zero => exact W.reducePointSmooth_zero | some x y h => exact W.reducePointSmooth_some_of_notMem h ((W.mem_nonIntegralLocus_some_iff h).mp hP) theorem mem_nonIntegralLocus_of_reducePointSmooth_eq_zero {P : (W.map A.subtype).toAffine.Point} (hP : W.HasNonsingularReduction P) (h0 : W.reducePointSmooth P = 0) : P ∈ W.nonIntegralLocus := by cases P with | zero => exact zero_mem _ | some x y h => by_cases hx : x ∈ A · exfalso have hy : y ∈ A := Affine.Y_mem_of_X_mem W h.1 hx have hns := (W.hasNonsingularReduction_some_iff h).mp hP hx hy rw [W.reducePointSmooth_some_of_mem h hx hns] at h0 exact Affine.Point.some_ne_zero hns h0 · exact (W.mem_nonIntegralLocus_some_iff h).mpr hx end Kernel theorem Affine.notMem_nonunits_of_sub_negY_mem_nonunits_of_nonsingular_residue {x y : L} (hx : x ∈ A) (hy : y ∈ A) (hns : (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩)) (hY : y - (W.map A.subtype).toAffine.negY x y ∈ A.nonunits) : 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.nonunits := by set eX : A := 3 * ⟨x, hx⟩ ^ 2 + 2 * W.a₂ * ⟨x, hx⟩ + W.a₄ - W.a₁ * ⟨y, hy⟩ with heX set eY : A := ⟨y, hy⟩ - W.toAffine.negY ⟨x, hx⟩ ⟨y, hy⟩ with heY have hcoeX : (eX : L) = 3 * x ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y := by push_cast [heX] rfl have hcoeY : (eY : L) = y - (W.map A.subtype).toAffine.negY x y := by have h1 : ((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 rw [heY] push_cast rw [h1] rw [Affine.nonsingular_iff] at hns have hY0 : residue A eY = 0 := by rw [← A.coe_mem_nonunits_iff_residue_eq_zero, hcoeY] exact hY have hX0 : residue A eX ≠ 0 := by rcases hns.2 with hX | hY' · intro h0 apply hX rw [heX] at h0 simp only [map_sub, map_add, map_mul, map_pow, map_ofNat] at h0 show residue A W.a₁ * residue A ⟨y, hy⟩ = 3 * residue A ⟨x, hx⟩ ^ 2 + 2 * residue A W.a₂ * residue A ⟨x, hx⟩ + residue A W.a₄ linear_combination -h0 · exact absurd (by show residue A ⟨y, hy⟩ = -residue A ⟨y, hy⟩ - residue A W.a₁ * residue A ⟨x, hx⟩ - residue A W.a₃ rw [heY] at hY0 simp only [Affine.negY, map_sub, map_neg, map_mul] at hY0 linear_combination hY0) hY' rw [← hcoeX, A.coe_mem_nonunits_iff_residue_eq_zero] exact hX0 section Slope variable [DecidableEq L] theorem Affine.slope_notMem_of_sub_mem_nonunits_of_nonsingular_residue {x₁ x₂ y₁ 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) (hy₁ : y₁ ∈ A) (hns₁ : (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x₁, hx₁⟩) (residue A ⟨y₁, hy₁⟩)) (hPQ : ¬(x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂)) (hxx : x₁ - x₂ ∈ A.nonunits) (hyy : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits) : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ ∉ A := by 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 ha₄ : (W.map A.subtype).toAffine.a₄ ∈ A := SetLike.coe_mem W.a₄ have hnegY : (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A := by rw [Affine.negY] exact A.toSubring.sub_mem (A.toSubring.sub_mem (A.toSubring.neg_mem hy₂) (A.toSubring.mul_mem ha₁ hx₂)) ha₃ by_cases hx : x₁ = x₂ · have hy : y₁ ≠ (W.map A.subtype).toAffine.negY x₂ y₂ := fun h => hPQ ⟨hx, h⟩ have hy12 : y₁ = y₂ := (Affine.Y_eq_of_X_eq h₁ h₂ hx).resolve_right hy rw [Affine.slope_of_Y_ne hx hy] have hden : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ ∈ A.nonunits := by rwa [← hx, ← hy12] at hyy have hden0 : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ ≠ 0 := by rw [sub_ne_zero] intro hcon exact hy (by rw [← hx, ← hy12]; exact hcon) have hnum := Affine.notMem_nonunits_of_sub_negY_mem_nonunits_of_nonsingular_residue W hx₁ hy₁ hns₁ hden exact A.div_notMem hnum hden hden0 · by_cases hyy' : y₁ - y₂ ∈ A.nonunits · rw [Affine.slope_of_X_ne hx] have hden : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ ∈ A.nonunits := by have key : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ = (y₁ - (W.map A.subtype).toAffine.negY x₂ y₂) + (y₁ - y₂) + (W.map A.subtype).toAffine.a₁ * (x₁ - x₂) := by simp only [Affine.negY] ring rw [key] exact add_mem (add_mem hyy hyy') (A.mul_mem_nonunits ha₁ hxx) have hnum := Affine.notMem_nonunits_of_sub_negY_mem_nonunits_of_nonsingular_residue W hx₁ hy₁ hns₁ hden set N : L := 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₁ with hN have hNunit : N ∉ A.nonunits := by intro hmem apply hnum have key : 3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁ = N - (x₁ + x₁ + x₂ + (W.map A.subtype).toAffine.a₂) * -(x₁ - x₂) := by rw [hN]; ring rw [key] exact sub_mem hmem (A.mul_mem_nonunits (add_mem (add_mem (add_mem hx₁ hx₁) hx₂) ha₂) (neg_mem hxx)) have hd0 : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ≠ 0 := by intro hd apply hNunit rw [hN] have hid := Affine.sub_mul_sub_negY h₁ h₂ rw [hd, mul_zero] at hid rcases mul_eq_zero.mp hid.symm with h | h · exact absurd (sub_eq_zero.mp h) hx · rw [h] exact zero_mem _ have hslope : (y₁ - y₂) / (x₁ - x₂) = N / (y₁ - (W.map A.subtype).toAffine.negY x₂ y₂) := by rw [div_eq_div_iff (sub_ne_zero.mpr hx) hd0, hN] linear_combination Affine.sub_mul_sub_negY h₁ h₂ rw [hslope] exact A.div_notMem hNunit hyy hd0 · rw [Affine.slope_of_X_ne hx] exact A.div_notMem hyy' hxx (sub_ne_zero.mpr hx) theorem Affine.addX_notMem_of_sub_mem_nonunits_of_nonsingular_residue {x₁ x₂ y₁ 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) (hy₁ : y₁ ∈ A) (hns₁ : (W.map (residue A)).toAffine.Nonsingular (residue A ⟨x₁, hx₁⟩) (residue A ⟨y₁, hy₁⟩)) (hPQ : ¬(x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂)) (hxx : x₁ - x₂ ∈ A.nonunits) (hyy : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits) : (W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∉ A := by have hℓ := Affine.slope_notMem_of_sub_mem_nonunits_of_nonsingular_residue W h₁ h₂ hx₁ hx₂ hy₁ hns₁ hPQ hxx hyy set ℓ : L := (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ 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₂ rw [show (W.map A.subtype).toAffine.addX x₁ x₂ ℓ = ℓ * (ℓ + (W.map A.subtype).toAffine.a₁) + (-(W.map A.subtype).toAffine.a₂ - x₁ - x₂) from by rw [Affine.addX]; ring] exact A.add_notMem (A.mul_notMem hℓ (by simpa [add_comm] using A.add_notMem hℓ ha₁)) (A.toSubring.sub_mem (A.toSubring.sub_mem (A.toSubring.neg_mem ha₂) hx₁) hx₂) end Slope section Carrier variable [DecidableEq L] [DecidableEq (ResidueField A)] structure SmoothLocusReductionData : Type _ where zeroComponent : AddSubgroup (W.map A.subtype).toAffine.Point mem_iff : ∀ P : (W.map A.subtype).toAffine.Point, P ∈ zeroComponent ↔ W.HasNonsingularReduction P reducePointSmooth_add : ∀ P Q : (W.map A.subtype).toAffine.Point, P ∈ zeroComponent → Q ∈ zeroComponent → W.reducePointSmooth (P + Q) = W.reducePointSmooth P + W.reducePointSmooth Q namespace SmoothLocusReductionData variable {W} theorem nonIntegralLocus_le (D : W.SmoothLocusReductionData) : W.nonIntegralLocus ≤ D.zeroComponent := fun P hP => (D.mem_iff P).mpr (W.hasNonsingularReduction_of_mem_nonIntegralLocus hP) theorem zero_mem (D : W.SmoothLocusReductionData) : (0 : (W.map A.subtype).toAffine.Point) ∈ D.zeroComponent := (D.mem_iff 0).mpr (W.hasNonsingularReduction_zero) noncomputable def reduceHom₀ (D : W.SmoothLocusReductionData) : D.zeroComponent →+ (W.map (residue A)).toAffine.Point where toFun P := W.reducePointSmooth (P : (W.map A.subtype).toAffine.Point) map_zero' := by simp map_add' P Q := by simpa using D.reducePointSmooth_add (P : (W.map A.subtype).toAffine.Point) (Q : (W.map A.subtype).toAffine.Point) P.2 Q.2 @[simp] theorem reduceHom₀_apply (D : W.SmoothLocusReductionData) (P : D.zeroComponent) : D.reduceHom₀ P = W.reducePointSmooth (P : (W.map A.subtype).toAffine.Point) := rfl theorem reduceHom₀_eq_zero_iff (D : W.SmoothLocusReductionData) (P : D.zeroComponent) : D.reduceHom₀ P = 0 ↔ (P : (W.map A.subtype).toAffine.Point) ∈ W.nonIntegralLocus := by constructor · intro h0 exact W.mem_nonIntegralLocus_of_reducePointSmooth_eq_zero ((D.mem_iff _).mp P.2) h0 · intro hmem exact W.reducePointSmooth_eq_zero_of_mem_nonIntegralLocus hmem end SmoothLocusReductionData end Carrier end General section ConsumerEngine variable {L : Type} [Field L] {A : ValuationSubring L} {W : WeierstrassCurve A} [DecidableEq L] [DecidableEq (ResidueField A)] end ConsumerEngine end WeierstrassCurve set_option autoImplicit false open IsLocalRing namespace WeierstrassCurve variable {L : Type*} [Field L] {A : ValuationSubring L} {W : WeierstrassCurve A} private lemma some_smoothClosure_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 CoordinatewiseEngine variable [DecidableEq L] [DecidableEq (ResidueField A)] theorem addX_mem_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)) : (W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∈ A := by obtain ⟨hsmem, -⟩ := slope_mem_residue_of_not_inverse h₁ h₂ hx₁ hx₂ hred 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⟩ rw [hX_coe] exact SetLike.coe_mem _ theorem addY_mem_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)) : (W.map A.subtype).toAffine.addY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∈ A := by obtain ⟨hsmem, -⟩ := slope_mem_residue_of_not_inverse h₁ h₂ hx₁ hx₂ hred have hy₁ : y₁ ∈ A := Affine.Y_mem_of_X_mem W h₁ hx₁ 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⟩ rw [hY_coe] exact SetLike.coe_mem _ set_option maxHeartbeats 800000 in theorem residue_addX_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) (hy₁ : y₁ ∈ A) (hy₂ : y₂ ∈ A) (hred : ¬(x₁ - x₂ ∈ A.nonunits ∧ y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits)) (hmem : (W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∈ A) : residue A ⟨(W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂), hmem⟩ = (W.map (residue A)).toAffine.addX (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩) ((W.map (residue A)).toAffine.slope (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₁, hy₁⟩) (residue A ⟨y₂, hy₂⟩)) := by obtain ⟨hsmem, hsres⟩ := slope_mem_residue_of_not_inverse h₁ h₂ hx₁ hx₂ hred have hsres' : residue A ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩ = (W.map (residue A)).toAffine.slope (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₁, hy₁⟩) (residue A ⟨y₂, hy₂⟩) := hsres 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⟩ calc residue A ⟨(W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂), hmem⟩ = 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 hmem 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'] set_option maxHeartbeats 800000 in theorem residue_addY_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) (hy₁ : y₁ ∈ A) (hy₂ : y₂ ∈ A) (hred : ¬(x₁ - x₂ ∈ A.nonunits ∧ y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits)) (hmem : (W.map A.subtype).toAffine.addY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∈ A) : residue A ⟨(W.map A.subtype).toAffine.addY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂), hmem⟩ = (W.map (residue A)).toAffine.addY (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₁, hy₁⟩) ((W.map (residue A)).toAffine.slope (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₁, hy₁⟩) (residue A ⟨y₂, hy₂⟩)) := by obtain ⟨hsmem, hsres⟩ := slope_mem_residue_of_not_inverse h₁ h₂ hx₁ hx₂ hred have hsres' : residue A ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩ = (W.map (residue A)).toAffine.slope (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₁, hy₁⟩) (residue A ⟨y₂, hy₂⟩) := hsres 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⟩ calc residue A ⟨(W.map A.subtype).toAffine.addY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂), hmem⟩ = 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 hmem 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 CoordinatewiseEngine section CaseAnalysis variable [DecidableEq L] [DecidableEq (ResidueField A)] set_option maxHeartbeats 1600000 in private lemma addAux_of_mem_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) (hP : W.HasNonsingularReduction (.some x₁ y₁ h₁)) (hQ : W.HasNonsingularReduction (.some x₂ y₂ h₂)) : W.HasNonsingularReduction (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) ∧ W.reducePointSmooth (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) = W.reducePointSmooth (.some x₁ y₁ h₁) + W.reducePointSmooth (.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₂ have hns₁ := (W.hasNonsingularReduction_some_iff h₁).mp hP hx₁ hy₁ have hns₂ := (W.hasNonsingularReduction_some_iff h₂).mp hQ hx₂ hy₂ 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 by_cases hPQ : x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂ · constructor · rw [Affine.Point.add_of_Y_eq hPQ.1 hPQ.2] exact W.hasNonsingularReduction_zero · rw [Affine.Point.add_of_Y_eq hPQ.1 hPQ.2, W.reducePointSmooth_zero, W.reducePointSmooth_some_of_mem h₁ hx₁ hns₁, W.reducePointSmooth_some_of_mem h₂ hx₂ hns₂, Affine.Point.add_of_Y_eq hredx hredy] · have haddX := Affine.addX_notMem_of_sub_mem_nonunits_of_nonsingular_residue W h₁.1 h₂.1 hx₁ hx₂ hy₁ hns₁ hPQ hred.1 hred.2 constructor · rw [Affine.Point.add_some hPQ] exact W.hasNonsingularReduction_some_of_notMem _ haddX · rw [Affine.Point.add_some hPQ, W.reducePointSmooth_some_of_notMem _ haddX, W.reducePointSmooth_some_of_mem h₁ hx₁ hns₁, W.reducePointSmooth_some_of_mem h₂ hx₂ hns₂, Affine.Point.add_of_Y_eq hredx hredy] · 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) have hXmem : (W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∈ A := addX_mem_of_not_inverse h₁.1 h₂.1 hx₁ hx₂ hred have hYmem : (W.map A.subtype).toAffine.addY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∈ A := addY_mem_of_not_inverse h₁.1 h₂.1 hx₁ hx₂ hred have hXres := residue_addX_of_not_inverse h₁.1 h₂.1 hx₁ hx₂ hy₁ hy₂ hred hXmem have hYres := residue_addY_of_not_inverse h₁.1 h₂.1 hx₁ hx₂ hy₁ hy₂ hred hYmem have hns₃ : (W.map (residue A)).toAffine.Nonsingular (residue A ⟨(W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂), hXmem⟩) (residue A ⟨(W.map A.subtype).toAffine.addY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂), hYmem⟩) := by rw [hXres, hYres] exact Affine.nonsingular_add hns₁ hns₂ hredk constructor · rw [Affine.Point.add_some hPQ, W.hasNonsingularReduction_some_iff] intro hx hy exact hns₃ · rw [Affine.Point.add_some hPQ, W.reducePointSmooth_some_of_mem _ hXmem hns₃, W.reducePointSmooth_some_of_mem h₁ hx₁ hns₁, W.reducePointSmooth_some_of_mem h₂ hx₂ hns₂, Affine.Point.add_some hredk] exact some_smoothClosure_congr hXres hYres _ _ private lemma addAux_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) : W.HasNonsingularReduction (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) ∧ W.reducePointSmooth (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) = W.reducePointSmooth (.some x₁ y₁ h₁) + W.reducePointSmooth (.some x₂ y₂ h₂) := by have hPmem : (.some x₁ y₁ h₁ : (W.map A.subtype).toAffine.Point) ∈ W.nonIntegralLocus := (W.mem_nonIntegralLocus_some_iff h₁).mpr hx₁ have hQmem : (.some x₂ y₂ h₂ : (W.map A.subtype).toAffine.Point) ∈ W.nonIntegralLocus := (W.mem_nonIntegralLocus_some_iff h₂).mpr hx₂ have hSmem : (.some x₁ y₁ h₁ + .some x₂ y₂ h₂ : (W.map A.subtype).toAffine.Point) ∈ W.nonIntegralLocus := add_mem hPmem hQmem refine ⟨W.hasNonsingularReduction_of_mem_nonIntegralLocus hSmem, ?_⟩ rw [W.reducePointSmooth_eq_zero_of_mem_nonIntegralLocus hSmem, W.reducePointSmooth_some_of_notMem h₁ hx₁, W.reducePointSmooth_some_of_notMem h₂ hx₂, add_zero] set_option maxHeartbeats 800000 in private lemma addAux_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₂) (hP : W.HasNonsingularReduction (.some x₁ y₁ h₁)) (hx₁ : x₁ ∈ A) (hx₂ : x₂ ∉ A) : W.HasNonsingularReduction (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) ∧ W.reducePointSmooth (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) = W.reducePointSmooth (.some x₁ y₁ h₁) + W.reducePointSmooth (.some x₂ y₂ h₂) := by have hy₁ : y₁ ∈ A := Affine.Y_mem_of_X_mem W h₁.1 hx₁ have hns₁ := (W.hasNonsingularReduction_some_iff h₁).mp hP hx₁ hy₁ have hPn : (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 cases hadd : (.some x₁ y₁ h₁ + .some x₂ y₂ h₂ : (W.map A.subtype).toAffine.Point) with | zero => exfalso have hPQ : (.some x₁ y₁ h₁ : (W.map A.subtype).toAffine.Point) = -(.some x₂ y₂ h₂) := eq_neg_of_add_eq_zero_left hadd rw [Affine.Point.neg_some] at hPQ simp only [Affine.Point.some.injEq] at hPQ exact hx₂ (hPQ.1 ▸ hx₁) | some X₃ Y₃ h₃ => by_cases hX₃ : X₃ ∈ A · have hY₃ : Y₃ ∈ A := Affine.Y_mem_of_X_mem W h₃.1 hX₃ have hkey : X₃ - x₁ ∈ A.nonunits ∧ Y₃ - (W.map A.subtype).toAffine.negY x₁ ((W.map A.subtype).toAffine.negY x₁ y₁) ∈ A.nonunits := by by_contra hcon 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 have hSP : ¬(X₃ = x₁ ∧ Y₃ = (W.map A.subtype).toAffine.negY x₁ ((W.map A.subtype).toAffine.negY x₁ y₁)) := by rintro ⟨hX, hY⟩ have h0 : (.some X₃ Y₃ h₃ : (W.map A.subtype).toAffine.Point) + .some x₁ ((W.map A.subtype).toAffine.negY x₁ y₁) hPn = 0 := Affine.Point.add_of_Y_eq hX hY rw [hSnegP] at h0 exact Affine.Point.some_ne_zero h₂ h0 have haddX : (W.map A.subtype).toAffine.addX X₃ x₁ ((W.map A.subtype).toAffine.slope X₃ x₁ Y₃ ((W.map A.subtype).toAffine.negY x₁ y₁)) ∈ A := addX_mem_of_not_inverse h₃.1 hPn.1 hX₃ hx₁ hcon rw [Affine.Point.add_some hSP] at hSnegP simp only [Affine.Point.some.injEq] at hSnegP exact hx₂ (hSnegP.1 ▸ haddX) rw [Affine.negY_negY] at hkey have hXres : residue A ⟨X₃, hX₃⟩ = residue A ⟨x₁, hx₁⟩ := (A.residue_eq_residue_iff_sub_mem_nonunits hX₃ hx₁).mpr hkey.1 have hYres : residue A ⟨Y₃, hY₃⟩ = residue A ⟨y₁, hy₁⟩ := (A.residue_eq_residue_iff_sub_mem_nonunits hY₃ hy₁).mpr hkey.2 have hnsS : (W.map (residue A)).toAffine.Nonsingular (residue A ⟨X₃, hX₃⟩) (residue A ⟨Y₃, hY₃⟩) := by rw [hXres, hYres] exact hns₁ constructor · rw [W.hasNonsingularReduction_some_iff] intro hx hy exact hnsS · rw [W.reducePointSmooth_some_of_mem h₃ hX₃ hnsS, W.reducePointSmooth_some_of_notMem h₂ hx₂, W.reducePointSmooth_some_of_mem h₁ hx₁ hns₁, add_zero] exact some_smoothClosure_congr hXres hYres _ _ · exfalso have hS : (.some X₃ Y₃ h₃ : (W.map A.subtype).toAffine.Point) ∈ W.nonIntegralLocus := (W.mem_nonIntegralLocus_some_iff h₃).mpr hX₃ have hQmem : (.some x₂ y₂ h₂ : (W.map A.subtype).toAffine.Point) ∈ W.nonIntegralLocus := (W.mem_nonIntegralLocus_some_iff h₂).mpr hx₂ have hPmem : (.some x₁ y₁ h₁ : (W.map A.subtype).toAffine.Point) ∈ W.nonIntegralLocus := by have hPeq : (.some x₁ y₁ h₁ : (W.map A.subtype).toAffine.Point) = .some X₃ Y₃ h₃ - .some x₂ y₂ h₂ := by rw [← hadd]; abel rw [hPeq] exact sub_mem hS hQmem exact ((W.mem_nonIntegralLocus_some_iff h₁).mp hPmem) hx₁ end CaseAnalysis section Closure variable [DecidableEq L] [DecidableEq (ResidueField A)] theorem hasNonsingularReduction_add {P Q : (W.map A.subtype).toAffine.Point} (hP : W.HasNonsingularReduction P) (hQ : W.HasNonsingularReduction Q) : W.HasNonsingularReduction (P + Q) := by cases P with | zero => show W.HasNonsingularReduction ((0 : (W.map A.subtype).toAffine.Point) + Q) rw [zero_add] exact hQ | some x₁ y₁ h₁ => cases Q with | zero => show W.HasNonsingularReduction (.some x₁ y₁ h₁ + (0 : (W.map A.subtype).toAffine.Point)) rw [add_zero] exact hP | some x₂ y₂ h₂ => by_cases hx₁ : x₁ ∈ A <;> by_cases hx₂ : x₂ ∈ A · exact (addAux_of_mem_of_mem h₁ h₂ hx₁ hx₂ hP hQ).1 · exact (addAux_of_mem_of_notMem h₁ h₂ hP hx₁ hx₂).1 · rw [add_comm (Affine.Point.some x₁ y₁ h₁) (Affine.Point.some x₂ y₂ h₂)] exact (addAux_of_mem_of_notMem h₂ h₁ hQ hx₂ hx₁).1 · exact (addAux_of_notMem_of_notMem h₁ h₂ hx₁ hx₂).1 theorem reducePointSmooth_add_of_hasNonsingularReduction {P Q : (W.map A.subtype).toAffine.Point} (hP : W.HasNonsingularReduction P) (hQ : W.HasNonsingularReduction Q) : W.reducePointSmooth (P + Q) = W.reducePointSmooth P + W.reducePointSmooth Q := by cases P with | zero => show W.reducePointSmooth ((0 : (W.map A.subtype).toAffine.Point) + Q) = W.reducePointSmooth (0 : (W.map A.subtype).toAffine.Point) + W.reducePointSmooth Q rw [zero_add, W.reducePointSmooth_zero, zero_add] | some x₁ y₁ h₁ => cases Q with | zero => show W.reducePointSmooth (.some x₁ y₁ h₁ + (0 : (W.map A.subtype).toAffine.Point)) = W.reducePointSmooth (.some x₁ y₁ h₁) + W.reducePointSmooth (0 : (W.map A.subtype).toAffine.Point) rw [add_zero, W.reducePointSmooth_zero, add_zero] | some x₂ y₂ h₂ => by_cases hx₁ : x₁ ∈ A <;> by_cases hx₂ : x₂ ∈ A · exact (addAux_of_mem_of_mem h₁ h₂ hx₁ hx₂ hP hQ).2 · exact (addAux_of_mem_of_notMem h₁ h₂ hP hx₁ hx₂).2 · rw [add_comm (Affine.Point.some x₁ y₁ h₁) (Affine.Point.some x₂ y₂ h₂), (addAux_of_mem_of_notMem h₂ h₁ hQ hx₂ hx₁).2] exact add_comm _ _ · exact (addAux_of_notMem_of_notMem h₁ h₂ hx₁ hx₂).2 end Closure section Carrier variable [DecidableEq L] [DecidableEq (ResidueField A)] variable (W) in def zeroComponentSubgroup : AddSubgroup (W.map A.subtype).toAffine.Point where carrier := {P | W.HasNonsingularReduction P} zero_mem' := W.hasNonsingularReduction_zero neg_mem' := fun {_P} hP => W.hasNonsingularReduction_neg hP add_mem' := fun {_P _Q} hP hQ => W.hasNonsingularReduction_add hP hQ variable (W) in @[simp] theorem mem_zeroComponentSubgroup_iff {P : (W.map A.subtype).toAffine.Point} : P ∈ W.zeroComponentSubgroup ↔ W.HasNonsingularReduction P := Iff.rfl variable (W) in noncomputable def smoothLocusReductionData : W.SmoothLocusReductionData where zeroComponent := W.zeroComponentSubgroup mem_iff := fun _ => Iff.rfl reducePointSmooth_add := fun _ _ hP hQ => W.reducePointSmooth_add_of_hasNonsingularReduction hP hQ variable (W) in theorem smoothLocusReductionData_zeroComponent : (W.smoothLocusReductionData).zeroComponent = W.zeroComponentSubgroup := rfl variable (W) in theorem nonempty_smoothLocusReductionData : Nonempty (W.SmoothLocusReductionData) := ⟨W.smoothLocusReductionData⟩ theorem SmoothLocusReductionData.zeroComponent_eq (D : W.SmoothLocusReductionData) : D.zeroComponent = W.zeroComponentSubgroup := AddSubgroup.ext fun P => D.mem_iff P variable (W) in theorem zeroComponentSubgroup_eq_top_of_good (hΔ : (W.map (residue A)).Δ ≠ 0) : W.zeroComponentSubgroup = ⊤ := by refine AddSubgroup.ext fun P => ?_ simp only [AddSubgroup.mem_top, iff_true] exact W.hasNonsingularReduction_of_good hΔ P variable (W) in theorem nonIntegralLocus_le_zeroComponentSubgroup : W.nonIntegralLocus ≤ W.zeroComponentSubgroup := fun _ hP => W.hasNonsingularReduction_of_mem_nonIntegralLocus hP end Carrier end WeierstrassCurve