feat(algebraic_geometry/elliptic_curve/point): the group law on the n…

…onsingular rational points of a Weierstrass curve (#18000)

Define a group structure on the nonsingular rational points of a Weierstrass curve by constructing an explicit injective group homomorphism into the class group of its coordinate ring and therefore proving associativity of the addition law.

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

- [x] depends on: #17999 
- [x] depends on: #17194
- [x] depends on: #18038 
- [x] depends on: #18101 
- [x] depends on: #19121 



Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

src/algebraic_geometry/elliptic_curve/point.lean

@@ -5,20 +5,22 @@ Authors: David Kurniadi Angdinata
 -/
 
 import algebraic_geometry.elliptic_curve.weierstrass
+import linear_algebra.free_module.norm
+import ring_theory.class_group
 
 /-!
-# The group of nonsingular rational points on a Weierstrass curve over a field
+# Nonsingular rational points on Weierstrass curves
 
 This file defines the type of nonsingular rational points on a Weierstrass curve over a field and
-(TODO) proves that it forms an abelian group under a geometric secant-and-tangent process.
+proves that it forms an abelian group under a geometric secant-and-tangent process.
 
 ## Mathematical background
 
 Let `W` be a Weierstrass curve over a field `F`. A rational point on `W` is simply a point
-$[A:B:C]$ defined over `F` in the projective plane satisfying the homogeneous cubic equation
-$B^2C + a_1ABC + a_3BC^2 = A^3 + a_2A^2C + a_4AC^2 + a_6C^3$. Any such point either lies in the
-affine chart $C \ne 0$ and satisfies the Weierstrass equation obtained by setting $X := A/C$ and
-$Y := B/C$, or is the unique point at infinity $0 := [0:1:0]$ when $C = 0$. With this new
+$[X:Y:Z]$ defined over `F` in the projective plane satisfying the homogeneous cubic equation
+$Y^2Z + a_1XYZ + a_3YZ^2 = X^3 + a_2X^2Z + a_4XZ^2 + a_6Z^3$. Any such point either lies in the
+affine chart $Z \ne 0$ and satisfies the Weierstrass equation obtained by replacing $X/Z$ with $X$
+and $Y/Z$ with $Y$, or is the unique point at infinity $0 := [0:1:0]$ when $Z = 0$. With this new
 description, a nonsingular rational point on `W` is either $0$ or an affine point $(x, y)$ where
 the partial derivatives $W_X(X, Y)$ and $W_Y(X, Y)$ do not vanish simultaneously. For a field
 extension `K` of `F`, a `K`-rational point is simply a rational point on `W` base changed to `K`.
@@ -50,11 +52,12 @@ The group law on this set is then uniquely determined by these constructions.
 
 ## Main statements
 
- * TODO: the addition of two nonsingular rational points on `W` forms a group.
+ * `weierstrass_curve.point.add_comm_group`: the type of nonsingular rational points on `W` forms an
+    abelian group under addition.
 
 ## Notations
 
- * `W⟮K⟯`: the group of nonsingular rational points on a Weierstrass curve `W` base changed to `K`.
+ * `W⟮K⟯`: the group of nonsingular rational points on `W` base changed to `K`.
 
 ## References
 
@@ -66,7 +69,8 @@ elliptic curve, rational point, group law
 -/
 
 private meta def map_simp : tactic unit :=
-`[simp only [map_one, map_bit0, map_bit1, map_neg, map_add, map_sub, map_mul, map_pow, map_div₀]]
+`[simp only [map_one, map_bit0, map_bit1, map_neg, map_add, map_sub, _root_.map_mul, map_pow,
+             map_div₀]]
 
 private meta def eval_simp : tactic unit :=
 `[simp only [eval_C, eval_X, eval_neg, eval_add, eval_sub, eval_mul, eval_pow]]
@@ -82,9 +86,9 @@ universes u v w
 
 namespace weierstrass_curve
 
-open polynomial
+open coordinate_ring ideal polynomial
 
-open_locale polynomial polynomial_polynomial
+open_locale non_zero_divisors polynomial polynomial_polynomial
 
 section basic
 
@@ -123,14 +127,36 @@ with a slope of $L$ that passes through an affine point $(x_1, y_1)$.
 This does not depend on `W`, and has argument order: $x_1$, $y_1$, $L$. -/
 noncomputable def line_polynomial : R[X] := C L * (X - C x₁) + C y₁
 
-/-- The polynomial obtained by substituting the line $Y = L(X - x_1) + y_1$, with a slope of $L$
+lemma XY_ideal_eq₁ : XY_ideal W x₁ (C y₁) = XY_ideal W x₁ (line_polynomial x₁ y₁ L) :=
+begin
+  simp only [XY_ideal, X_class, Y_class, line_polynomial],
+  rw [← span_pair_add_mul_right $ adjoin_root.mk _ $ C $ C $ -L, ← _root_.map_mul, ← map_add],
+  apply congr_arg (_ ∘ _ ∘ _ ∘ _),
+  C_simp,
+  ring1
+end
+
+/-- The polynomial obtained by substituting the line $Y = L*(X - x_1) + y_1$, with a slope of $L$
 that passes through an affine point $(x_1, y_1)$, into the polynomial $W(X, Y)$ associated to `W`.
 If such a line intersects `W` at another point $(x_2, y_2)$, then the roots of this polynomial are
 precisely $x_1$, $x_2$, and the $X$-coordinate of the addition of $(x_1, y_1)$ and $(x_2, y_2)$.
 
 This depends on `W`, and has argument order: $x_1$, $y_1$, $L$. -/
 noncomputable def add_polynomial : R[X] := W.polynomial.eval $ line_polynomial x₁ y₁ L
 
+lemma C_add_polynomial :
+  C (W.add_polynomial x₁ y₁ L)
+    = (Y - C (line_polynomial x₁ y₁ L)) * (W.neg_polynomial - C (line_polynomial x₁ y₁ L))
+      + W.polynomial :=
+by { rw [add_polynomial, line_polynomial, weierstrass_curve.polynomial, neg_polynomial], eval_simp,
+     C_simp, ring1 }
+
+lemma coordinate_ring.C_add_polynomial :
+  adjoin_root.mk W.polynomial (C (W.add_polynomial x₁ y₁ L))
+    = adjoin_root.mk W.polynomial
+      ((Y - C (line_polynomial x₁ y₁ L)) * (W.neg_polynomial - C (line_polynomial x₁ y₁ L))) :=
+adjoin_root.mk_eq_mk.mpr ⟨1, by rw [C_add_polynomial, add_sub_cancel', mul_one]⟩
+
 lemma add_polynomial_eq : W.add_polynomial x₁ y₁ L = -cubic.to_poly
   ⟨1, -L ^ 2 - W.a₁ * L + W.a₂,
     2 * x₁ * L ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * L + (-W.a₁ * y₁ + W.a₄),
@@ -186,6 +212,20 @@ lemma base_change_add_Y_of_base_change (x₁ x₂ y₁ L : A) :
     (algebra_map A B L) = algebra_map A B ((W.base_change A).add_Y x₁ x₂ y₁ L) :=
 by rw [← base_change_add_Y, base_change_base_change]
 
+lemma XY_ideal_add_eq :
+  XY_ideal W (W.add_X x₁ x₂ L) (C (W.add_Y x₁ x₂ y₁ L))
+    = span {adjoin_root.mk W.polynomial $ W.neg_polynomial - C (line_polynomial x₁ y₁ L)}
+      ⊔ X_ideal W (W.add_X x₁ x₂ L) :=
+begin
+  simp only [XY_ideal, X_ideal, X_class, Y_class, add_Y, add_Y', neg_Y, neg_polynomial,
+             line_polynomial],
+  conv_rhs { rw [sub_sub, ← neg_add', map_neg, span_singleton_neg, sup_comm, ← span_insert] },
+  rw [← span_pair_add_mul_right $ adjoin_root.mk _ $ C $ C $ W.a₁ + L, ← _root_.map_mul, ← map_add],
+  apply congr_arg (_ ∘ _ ∘ _ ∘ _),
+  C_simp,
+  ring1
+end
+
 lemma equation_add_iff :
   W.equation (W.add_X x₁ x₂ L) (W.add_Y' x₁ x₂ y₁ L)
     ↔ (W.add_polynomial x₁ y₁ L).eval (W.add_X x₁ x₂ L) = 0 :=
@@ -359,6 +399,27 @@ end
 lemma Y_eq_of_Y_ne (hx : x₁ = x₂) (hy : y₁ ≠ W.neg_Y x₂ y₂) : y₁ = y₂ :=
 or.resolve_right (Y_eq_of_X_eq h₁' h₂' hx) hy
 
+lemma XY_ideal_eq₂ (hxy : x₁ = x₂ → y₁ ≠ W.neg_Y x₂ y₂) :
+  XY_ideal W x₂ (C y₂) = XY_ideal W x₂ (line_polynomial x₁ y₁ $ W.slope x₁ x₂ y₁ y₂) :=
+begin
+  have hy₂ : y₂ = (line_polynomial x₁ y₁ $ W.slope x₁ x₂ y₁ y₂).eval x₂ :=
+  begin
+    by_cases hx : x₁ = x₂,
+    { rcases ⟨hx, Y_eq_of_Y_ne h₁' h₂' hx $ hxy hx⟩ with ⟨rfl, rfl⟩,
+      field_simp [line_polynomial, sub_ne_zero_of_ne (hxy rfl)] },
+    { field_simp [line_polynomial, slope_of_X_ne hx, sub_ne_zero_of_ne hx],
+      ring1 }
+  end,
+  nth_rewrite_lhs 0 [hy₂],
+  simp only [XY_ideal, X_class, Y_class, line_polynomial],
+  rw [← span_pair_add_mul_right $ adjoin_root.mk W.polynomial $ C $ C $ -W.slope x₁ x₂ y₁ y₂,
+      ← _root_.map_mul, ← map_add],
+  apply congr_arg (_ ∘ _ ∘ _ ∘ _),
+  eval_simp,
+  C_simp,
+  ring1
+end
+
 lemma add_polynomial_slope (hxy : x₁ = x₂ → y₁ ≠ W.neg_Y x₂ y₂) :
   W.add_polynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)
     = -((X - C x₁) * (X - C x₂) * (X - C (W.add_X x₁ x₂ $ W.slope x₁ x₂ y₁ y₂))) :=
@@ -390,6 +451,11 @@ begin
         with { normalization_tactic := `[field_simp [hx], ring1] } } }
 end
 
+lemma coordinate_ring.C_add_polynomial_slope (hxy : x₁ = x₂ → y₁ ≠ W.neg_Y x₂ y₂) :
+  adjoin_root.mk W.polynomial (C $ W.add_polynomial x₁ y₁ $ W.slope x₁ x₂ y₁ y₂)
+    = -(X_class W x₁ * X_class W x₂ * X_class W (W.add_X x₁ x₂ $ W.slope x₁ x₂ y₁ y₂)) :=
+by simpa only [add_polynomial_slope h₁' h₂' hxy, map_neg, neg_inj, _root_.map_mul]
+
 lemma derivative_add_polynomial_slope (hxy : x₁ = x₂ → y₁ ≠ W.neg_Y x₂ y₂) :
   derivative (W.add_polynomial x₁ y₁ $ W.slope x₁ x₂ y₁ y₂)
     = -((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.add_X x₁ x₂ $ W.slope x₁ x₂ y₁ y₂))
@@ -502,15 +568,168 @@ section group
 
 /-! ### The axioms for nonsingular rational points on a Weierstrass curve -/
 
-variables {F : Type u} [field F] {W : weierstrass_curve F}
+variables {F : Type u} [field F] {W : weierstrass_curve F} {x₁ x₂ y₁ y₂ : F}
+  (h₁ : W.nonsingular x₁ y₁) (h₂ : W.nonsingular x₂ y₂)
+  (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂)
+
+include h₁
+
+lemma XY_ideal_neg_mul : XY_ideal W x₁ (C $ W.neg_Y x₁ y₁) * XY_ideal W x₁ (C y₁) = X_ideal W x₁ :=
+begin
+  have Y_rw :
+    (Y - C (C y₁)) * (Y - C (C (W.neg_Y x₁ y₁))) - C (X - C x₁)
+      * (C (X ^ 2 + C (x₁ + W.a₂) * X + C (x₁ ^ 2 + W.a₂ * x₁ + W.a₄)) - C (C W.a₁) * Y)
+      = W.polynomial * 1 :=
+  by linear_combination congr_arg C (congr_arg C ((W.equation_iff _ _).mp h₁.left).symm)
+    with { normalization_tactic := `[rw [neg_Y, weierstrass_curve.polynomial], C_simp, ring1] },
+  simp_rw [XY_ideal, X_class, Y_class, span_pair_mul_span_pair, mul_comm, ← _root_.map_mul,
+           adjoin_root.mk_eq_mk.mpr ⟨1, Y_rw⟩, _root_.map_mul, span_insert,
+           ← span_singleton_mul_span_singleton, ← mul_sup, ← span_insert],
+  convert mul_top _ using 2,
+  simp_rw [← @set.image_singleton _ _ $ adjoin_root.mk _, ← set.image_insert_eq, ← map_span],
+  convert map_top (adjoin_root.mk W.polynomial) using 1,
+  apply congr_arg,
+  simp_rw [eq_top_iff_one, mem_span_insert', mem_span_singleton'],
+  cases ((W.nonsingular_iff' _ _).mp h₁).right with hx hy,
+  { let W_X := W.a₁ * y₁ - (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄),
+    refine ⟨C (C W_X⁻¹ * -(X + C (2 * x₁ + W.a₂))), C (C $ W_X⁻¹ * W.a₁), 0, C (C $ W_X⁻¹ * -1), _⟩,
+    rw [← mul_right_inj' $ C_ne_zero.mpr $ C_ne_zero.mpr hx],
+    simp only [mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel hx],
+    C_simp,
+    ring1 },
+  { let W_Y := 2 * y₁ + W.a₁ * x₁ + W.a₃,
+    refine ⟨0, C (C W_Y⁻¹), C (C $ W_Y⁻¹ * -1), 0, _⟩,
+    rw [neg_Y, ← mul_right_inj' $ C_ne_zero.mpr $ C_ne_zero.mpr hy],
+    simp only [mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel hy],
+    C_simp,
+    ring1 }
+end
+
+private lemma XY_ideal'_mul_inv :
+  (XY_ideal W x₁ (C y₁) : fractional_ideal W.coordinate_ring⁰ W.function_field)
+    * (XY_ideal W x₁ (C $ W.neg_Y x₁ y₁) * (X_ideal W x₁)⁻¹) = 1 :=
+by rw [← mul_assoc, ← fractional_ideal.coe_ideal_mul, mul_comm $ XY_ideal W _ _,
+       XY_ideal_neg_mul h₁, X_ideal,
+       fractional_ideal.coe_ideal_span_singleton_mul_inv W.function_field $ X_class_ne_zero W x₁]
+
+omit h₁
+
+include h₁' h₂'
+
+lemma XY_ideal_mul_XY_ideal (hxy : x₁ = x₂ → y₁ ≠ W.neg_Y x₂ y₂) :
+  X_ideal W (W.add_X x₁ x₂ $ W.slope x₁ x₂ y₁ y₂) * (XY_ideal W x₁ (C y₁) * XY_ideal W x₂ (C y₂))
+    = Y_ideal W (line_polynomial x₁ y₁ $ W.slope x₁ x₂ y₁ y₂)
+      * XY_ideal W (W.add_X x₁ x₂ $ W.slope x₁ x₂ y₁ y₂)
+        (C $ W.add_Y x₁ x₂ y₁ $ W.slope x₁ x₂ y₁ y₂) :=
+begin
+  have sup_rw : ∀ a b c d : ideal W.coordinate_ring, a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c :=
+  λ _ _ c _, by rw [← sup_assoc, @sup_comm _ _ c, sup_sup_sup_comm, ← sup_assoc],
+  rw [XY_ideal_add_eq, X_ideal, mul_comm, W.XY_ideal_eq₁ x₁ y₁ $ W.slope x₁ x₂ y₁ y₂, XY_ideal,
+      XY_ideal_eq₂ h₁' h₂' hxy, XY_ideal, span_pair_mul_span_pair],
+  simp_rw [span_insert, sup_rw, sup_mul, span_singleton_mul_span_singleton],
+  rw [← neg_eq_iff_eq_neg.mpr $ coordinate_ring.C_add_polynomial_slope h₁' h₂' hxy,
+      span_singleton_neg, coordinate_ring.C_add_polynomial, _root_.map_mul, Y_class],
+  simp_rw [mul_comm $ X_class W x₁, mul_assoc, ← span_singleton_mul_span_singleton, ← mul_sup],
+  rw [span_singleton_mul_span_singleton, ← span_insert,
+      ← span_pair_add_mul_right $ -(X_class W $ W.add_X x₁ x₂ $ W.slope x₁ x₂ y₁ y₂), mul_neg,
+      ← sub_eq_add_neg, ← sub_mul, ← map_sub, sub_sub_sub_cancel_right, span_insert,
+      ← span_singleton_mul_span_singleton, ← sup_rw, ← sup_mul, ← sup_mul],
+  apply congr_arg (_ ∘ _),
+  convert top_mul _,
+  simp_rw [X_class, ← @set.image_singleton _ _ $ adjoin_root.mk _, ← map_span, ← ideal.map_sup,
+           eq_top_iff_one, mem_map_iff_of_surjective _ $ adjoin_root.mk_surjective
+             W.monic_polynomial, ← span_insert, mem_span_insert', mem_span_singleton'],
+  by_cases hx : x₁ = x₂,
+  { rcases ⟨hx, Y_eq_of_Y_ne h₁' h₂' hx (hxy hx)⟩ with ⟨rfl, rfl⟩,
+    let y := (y₁ - W.neg_Y x₁ y₁) ^ 2,
+    replace hxy := pow_ne_zero 2 (sub_ne_zero_of_ne $ hxy rfl),
+    refine
+      ⟨1 + C (C $ y⁻¹ * 4) * W.polynomial,
+        ⟨C $ C y⁻¹ * (C 4 * X ^ 2 + C (4 * x₁ + W.b₂) * X + C (4 * x₁ ^ 2 + W.b₂ * x₁ + 2 * W.b₄)),
+        0, C (C y⁻¹) * (Y - W.neg_polynomial), _⟩,
+        by rw [map_add, map_one, _root_.map_mul, adjoin_root.mk_self, mul_zero, add_zero]⟩,
+    rw [weierstrass_curve.polynomial, neg_polynomial,
+        ← mul_right_inj' $ C_ne_zero.mpr $ C_ne_zero.mpr hxy],
+    simp only [mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel hxy],
+    linear_combination -4 * congr_arg C (congr_arg C $ (W.equation_iff _ _).mp h₁')
+      with { normalization_tactic := `[rw [b₂, b₄, neg_Y], C_simp, ring1] } },
+  { replace hx := sub_ne_zero_of_ne hx,
+    refine ⟨_, ⟨⟨C $ C (x₁ - x₂)⁻¹, C $ C $ (x₁ - x₂)⁻¹ * -1, 0, _⟩, map_one _⟩⟩,
+    rw [← mul_right_inj' $ C_ne_zero.mpr $ C_ne_zero.mpr hx],
+    simp only [← mul_assoc, mul_add, ← C_mul, mul_inv_cancel hx],
+    C_simp,
+    ring1 }
+end
+
+omit h₁' h₂'
+
+/-- The non-zero fractional ideal $\langle X - x, Y - y \rangle$ of $F(W)$ for some $x, y \in F$. -/
+@[simp] noncomputable def XY_ideal' : (fractional_ideal W.coordinate_ring⁰ W.function_field)ˣ :=
+units.mk_of_mul_eq_one _ _ $ XY_ideal'_mul_inv h₁
+
+lemma XY_ideal'_eq :
+  (XY_ideal' h₁ : fractional_ideal W.coordinate_ring⁰ W.function_field) = XY_ideal W x₁ (C y₁) :=
+rfl
+
+local attribute [irreducible] coordinate_ring.comm_ring
+
+lemma mk_XY_ideal'_mul_mk_XY_ideal'_of_Y_eq :
+  class_group.mk (XY_ideal' $ nonsingular_neg h₁) * class_group.mk (XY_ideal' h₁) = 1 :=
+begin
+  rw [← _root_.map_mul],
+  exact (class_group.mk_eq_one_of_coe_ideal $
+          by exact (fractional_ideal.coe_ideal_mul _ _).symm.trans
+            (fractional_ideal.coe_ideal_inj.mpr $ XY_ideal_neg_mul h₁)).mpr
+          ⟨_, X_class_ne_zero W _, rfl⟩
+end
+
+lemma mk_XY_ideal'_mul_mk_XY_ideal' (hxy : x₁ = x₂ → y₁ ≠ W.neg_Y x₂ y₂) :
+  class_group.mk (XY_ideal' h₁) * class_group.mk (XY_ideal' h₂)
+    = class_group.mk (XY_ideal' $ nonsingular_add h₁ h₂ hxy) :=
+begin
+  rw [← _root_.map_mul],
+  exact (class_group.mk_eq_mk_of_coe_ideal (by exact (fractional_ideal.coe_ideal_mul _ _).symm) $
+          XY_ideal'_eq _).mpr ⟨_, _, X_class_ne_zero W _, Y_class_ne_zero W _,
+            XY_ideal_mul_XY_ideal h₁.left h₂.left hxy⟩
+end
 
 namespace point
 
+/-- The set function mapping an affine point $(x, y)$ of `W` to the class of the non-zero fractional
+ideal $\langle X - x, Y - y \rangle$ of $F(W)$ in the class group of $F[W]$. -/
+@[simp] noncomputable def to_class_fun : W.point → additive (class_group W.coordinate_ring)
+| 0        := 0
+| (some h) := additive.of_mul $ class_group.mk $ XY_ideal' h
+
+/-- The group homomorphism mapping an affine point $(x, y)$ of `W` to the class of the non-zero
+fractional ideal $\langle X - x, Y - y \rangle$ of $F(W)$ in the class group of $F[W]$. -/
+@[simps] noncomputable def to_class : W.point →+ additive (class_group W.coordinate_ring) :=
+{ to_fun    := to_class_fun,
+  map_zero' := rfl,
+  map_add'  :=
+  begin
+    rintro (_ | @⟨x₁, y₁, h₁⟩) (_ | @⟨x₂, y₂, h₂⟩),
+    any_goals { simp only [zero_def, to_class_fun, _root_.zero_add, _root_.add_zero] },
+    by_cases hx : x₁ = x₂,
+    { by_cases hy : y₁ = W.neg_Y x₂ y₂,
+      { substs hx hy,
+        simpa only [some_add_some_of_Y_eq rfl rfl]
+          using (mk_XY_ideal'_mul_mk_XY_ideal'_of_Y_eq h₂).symm },
+      { simpa only [some_add_some_of_Y_ne hx hy]
+          using (mk_XY_ideal'_mul_mk_XY_ideal' h₁ h₂ $ λ _, hy).symm } },
+    { simpa only [some_add_some_of_X_ne hx]
+        using (mk_XY_ideal'_mul_mk_XY_ideal' h₁ h₂ $ λ h, (hx h).elim).symm }
+  end }
+
+@[simp] lemma to_class_zero : to_class (0 : W.point) = 0 := rfl
+
+lemma to_class_some : to_class (some h₁) = class_group.mk (XY_ideal' h₁) := rfl
+
 @[simp] lemma add_eq_zero (P Q : W.point) : P + Q = 0 ↔ P = -Q :=
 begin
   rcases ⟨P, Q⟩ with ⟨_ | @⟨x₁, y₁, _⟩, _ | @⟨x₂, y₂, _⟩⟩,
   any_goals { refl },
-  { rw [zero_def, zero_add, ← neg_eq_iff_eq_neg, neg_zero, eq_comm], },
+  { rw [zero_def, zero_add, ← neg_eq_iff_eq_neg, neg_zero, eq_comm] },
   { simp only [neg_some],
     split,
     { intro h,
@@ -528,6 +747,42 @@ end
 
 @[simp] lemma neg_add_eq_zero (P Q : W.point) : -P + Q = 0 ↔ P = Q := by rw [add_eq_zero, neg_inj]
 
+lemma to_class_eq_zero (P : W.point) : to_class P = 0 ↔ P = 0 :=
+⟨begin
+  intro hP,
+  rcases P with (_ | @⟨_, _, ⟨h, _⟩⟩),
+  { refl },
+  { rcases (class_group.mk_eq_one_of_coe_ideal $ by refl).mp hP with ⟨p, h0, hp⟩,
+    apply (p.nat_degree_norm_ne_one _).elim,
+    rw [← finrank_quotient_span_eq_nat_degree_norm W^.coordinate_ring.basis h0,
+        ← (quotient_equiv_alg_of_eq F hp).to_linear_equiv.finrank_eq,
+        (quotient_XY_ideal_equiv W h).to_linear_equiv.finrank_eq, finite_dimensional.finrank_self] }
+end, congr_arg to_class⟩
+
+lemma to_class_injective : function.injective $ @to_class _ _ W :=
+begin
+  rintro (_ | h) _ hP,
+  all_goals { rw [← neg_add_eq_zero, ← to_class_eq_zero, map_add, ← hP] },
+  { exact zero_add 0 },
+  { exact mk_XY_ideal'_mul_mk_XY_ideal'_of_Y_eq h }
+end
+
+lemma add_comm (P Q : W.point) : P + Q = Q + P :=
+to_class_injective $ by simp only [map_add, add_comm]
+
+lemma add_assoc (P Q R : W.point) : P + Q + R = P + (Q + R) :=
+to_class_injective $ by simp only [map_add, add_assoc]
+
+noncomputable instance : add_comm_group W.point :=
+{ zero         := zero,
+  neg          := neg,
+  add          := add,
+  zero_add     := zero_add,
+  add_zero     := add_zero,
+  add_left_neg := add_left_neg,
+  add_comm     := add_comm,
+  add_assoc    := add_assoc }
+
 end point
 
 end group