feat(AlgebraicGeometry/EllipticCurve/Affine/Point): add equivalences between points and explicit WithZero types (#25984)

This PR continues the work from #14627.

Original PR: #14627

Author: Multramate

Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

@@ -481,20 +481,143 @@ inductive Point
 
 /-- For an algebraic extension `S` of a ring `R`, the type of nonsingular `S`-points on a
 Weierstrass curve `W` over `R` in affine coordinates. -/
-scoped notation3:max W' "⟮" S "⟯" => Affine.Point <| baseChange W' S
+scoped notation3:max W' "⟮" S "⟯" => Point <| baseChange W' S
+
+/-- The equivalence between the nonsingular points on a Weierstrass curve `W` in affine coordinates
+satisfying a predicate and the set of pairs `⟨x, y⟩` satisfying `W.Nonsingular x y` with zero. -/
+def nonsingularPointEquivSubtype {p : W'.Point → Prop} (p0 : p .zero) : {P : W'.Point // p P} ≃
+    WithZero {xy : R × R // ∃ h : W'.Nonsingular xy.fst xy.snd, p <| .some h} where
+  toFun
+    | ⟨.zero, _⟩ => none
+    | ⟨.some h, ph⟩ => .some ⟨⟨_, _⟩, h, ph⟩
+  invFun P := P.casesOn ⟨.zero, p0⟩ fun xy => ⟨.some xy.prop.choose, xy.prop.choose_spec⟩
+  left_inv := by rintro (_ | _) <;> rfl
+  right_inv := by rintro (_ | _) <;> rfl
+
+@[simp]
+lemma nonsingularPointEquivSubtype_zero {p : W'.Point → Prop} (p0 : p .zero) :
+    nonsingularPointEquivSubtype p0 ⟨.zero, p0⟩ = none :=
+  rfl
+
+@[simp]
+lemma nonsingularPointEquivSubtype_some {x y : R} {h : W'.Nonsingular x y} {p : W'.Point → Prop}
+    (p0 : p .zero) (ph : p <| .some h) :
+    nonsingularPointEquivSubtype p0 ⟨.some h, ph⟩ = .some ⟨⟨x, y⟩, h, ph⟩ :=
+  rfl
+
+@[simp]
+lemma nonsingularPointEquivSubtype_symm_none {p : W'.Point → Prop} (p0 : p .zero) :
+    (nonsingularPointEquivSubtype p0).symm none = ⟨.zero, p0⟩ :=
+  rfl
+
+@[simp]
+lemma nonsingularPointEquivSubtype_symm_some {x y : R} {h : W'.Nonsingular x y}
+    {p : W'.Point → Prop} (p0 : p .zero) (ph : p <| .some h) :
+    (nonsingularPointEquivSubtype p0).symm (.some ⟨⟨x, y⟩, h, ph⟩) = ⟨.some h, ph⟩ :=
+  rfl
+
+variable (W') in
+/-- The equivalence between the nonsingular points on a Weierstrass curve `W` in affine coordinates
+and the set of pairs `⟨x, y⟩` satisfying `W.Nonsingular x y` with zero. -/
+def nonsingularPointEquiv : W'.Point ≃ WithZero {xy : R × R // W'.Nonsingular xy.fst xy.snd} :=
+  (Equiv.Set.univ W'.Point).symm.trans <| (nonsingularPointEquivSubtype trivial).trans
+    (Equiv.setCongr <| Set.ext fun _ => exists_iff_of_forall fun _ => trivial).optionCongr
+
+@[simp]
+lemma nonsingularPointEquiv_zero : nonsingularPointEquiv W' .zero = none :=
+  rfl
+
+@[simp]
+lemma nonsingularPointEquiv_some {x y : R} (h : W'.Nonsingular x y) :
+    W'.nonsingularPointEquiv (.some h) = .some ⟨⟨x, y⟩, h⟩ := by
+  rfl
+
+@[simp]
+lemma nonsingularPointEquiv_symm_none : W'.nonsingularPointEquiv.symm none = .zero :=
+  rfl
+
+@[simp]
+lemma nonsingularPointEquiv_symm_some {x y : R} (h : W'.Nonsingular x y) :
+    W'.nonsingularPointEquiv.symm (.some ⟨⟨x, y⟩, h⟩) = .some h :=
+  rfl
+
+section IsElliptic
+
+variable [Nontrivial R] [W'.IsElliptic]
+
+/-- A point on an elliptic curve `W` over `R`. -/
+def Point.mk {x y : R} (h : W'.Equation x y) : W'.Point :=
+  .some <| equation_iff_nonsingular.mp h
+
+/-- The equivalence between the points on an elliptic curve `W` in affine coordinates satisfying a
+predicate and the set of pairs `⟨x, y⟩` satisfying `W.Equation x y` with zero. -/
+def pointEquivSubtype {p : W'.Point → Prop} (p0 : p .zero) :
+    {P : W'.Point // p P} ≃ WithZero {xy : R × R // ∃ h : W'.Equation xy.fst xy.snd, p <| .mk h} :=
+  (nonsingularPointEquivSubtype p0).trans
+    (Equiv.setCongr <| by simpa only [equation_iff_nonsingular] using by rfl).optionCongr
+
+@[simp]
+lemma pointEquivSubtype_zero {p : W'.Point → Prop} (p0 : p .zero) :
+    pointEquivSubtype p0 ⟨.zero, p0⟩ = none :=
+  rfl
+
+@[simp]
+lemma pointEquivSubtype_some {x y : R} {h : W'.Equation x y} {p : W'.Point → Prop} (p0 : p .zero)
+    (ph : p <| .mk h) : pointEquivSubtype p0 ⟨.mk h, ph⟩ = .some ⟨⟨x, y⟩, h, ph⟩ :=
+  rfl
+
+@[simp]
+lemma pointEquivSubtype_symm_none {p : W'.Point → Prop} (p0 : p .zero) :
+    (pointEquivSubtype p0).symm none = ⟨.zero, p0⟩ :=
+  rfl
+
+@[simp]
+lemma pointEquivSubtype_symm_some {x y : R} {h : W'.Equation x y} {p : W'.Point → Prop}
+    (p0 : p .zero) (ph : p <| .mk h) :
+    (pointEquivSubtype p0).symm (.some ⟨⟨x, y⟩, h, ph⟩) = ⟨.mk h, ph⟩ :=
+  rfl
+
+variable (W') in
+/-- The equivalence between the rational points on an elliptic curve `E` and the set of pairs
+`⟨x, y⟩` satisfying `E.Equation x y` with zero. -/
+def pointEquiv : W'.Point ≃ WithZero {xy : R × R // W'.Equation xy.fst xy.snd} :=
+  (Equiv.Set.univ W'.Point).symm.trans <| (pointEquivSubtype trivial).trans
+    (Equiv.setCongr <| Set.ext fun _ => exists_iff_of_forall fun _ => trivial).optionCongr
+
+@[simp]
+lemma pointEquiv_zero : W'.pointEquiv .zero = none :=
+  rfl
+
+@[simp]
+lemma pointEquiv_some {x y : R} (h : W'.Equation x y) :
+    pointEquiv W' (.mk h) = .some ⟨⟨x, y⟩, h⟩ := by
+  rfl
+
+@[simp]
+lemma pointEquiv_symm_none : (pointEquiv W').symm none = .zero :=
+  rfl
+
+@[simp]
+lemma pointEquiv_symm_some {x y : R} (h : W'.Equation x y) :
+    (pointEquiv W').symm (.some ⟨⟨x, y⟩, h⟩) = .mk h :=
+  rfl
+
+end IsElliptic
 
 namespace Point
 
+/-! ## Group law in affine coordinates -/
+
 instance : Inhabited W'.Point :=
-  ⟨.zero⟩
+  ⟨zero⟩
 
 instance : Zero W'.Point :=
-  ⟨.zero⟩
+  ⟨zero⟩
 
-lemma zero_def : 0 = (.zero : W'.Point) :=
+lemma zero_def : 0 = (zero : W'.Point) :=
   rfl
 
-lemma some_ne_zero {x y : R} (h : W'.Nonsingular x y) : Point.some h ≠ 0 := by
+lemma some_ne_zero {x y : R} (h : W'.Nonsingular x y) : some h ≠ 0 := by
   rintro (_ | _)
 
 /-- The negation of a nonsingular point on a Weierstrass curve in affine coordinates.
@@ -524,6 +647,8 @@ instance : InvolutiveNeg W'.Point where
     · rfl
     · simp only [neg_some, negY_negY]
 
+variable [DecidableEq F] [DecidableEq K] [DecidableEq L]
+
 /-- The addition of two nonsingular points on a Weierstrass curve in affine coordinates.
 
 Given two nonsingular points `P` and `Q` in affine coordinates, use `P + Q` instead of `add P Q`. -/
@@ -533,10 +658,6 @@ def add [DecidableEq F] : W.Point → W.Point → W.Point
   | @some _ _ _ x₁ y₁ h₁, @some _ _ _ x₂ y₂ h₂ =>
     if hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ then 0 else some <| nonsingular_add h₁ h₂ hxy
 
-section add
-
-variable [DecidableEq F]
-
 instance : Add W.Point :=
   ⟨add⟩
 
@@ -590,10 +711,6 @@ lemma add_of_X_ne' {x₁ x₂ y₁ y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h
     (hx : x₁ ≠ x₂) : some h₁ + some h₂ = -some (nonsingular_negAdd h₁ h₂ fun hxy => hx hxy.left) :=
   add_of_X_ne hx
 
-variable [DecidableEq K] [DecidableEq L]
-
-/-! ## Group law in affine coordinates -/
-
 /-- The group homomorphism mapping a nonsingular affine point `(x, y)` of a Weierstrass curve `W` to
 the class of the non-zero fractional ideal `⟨X - x, Y - y⟩` in the ideal class group of `F[W]`. -/
 @[simps]
@@ -711,8 +828,6 @@ lemma map_baseChange [Algebra F K] [IsScalarTower R F K] [Algebra F L] [IsScalar
   have : Subsingleton (F →ₐ[F] L) := inferInstance
   convert map_map (Algebra.ofId F K) f P
 
-end add
-
 end Point
 
 end Affine