feat(algebraic_geometry/elliptic_curve/point): define homomorphism in…

…duced by base change (#18493)

src/algebraic_geometry/elliptic_curve/point.lean

@@ -67,6 +67,9 @@ The group law on this set is then uniquely determined by these constructions.
 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₀]]
+
 private meta def eval_simp : tactic unit :=
 `[simp only [eval_C, eval_X, eval_neg, eval_add, eval_sub, eval_mul, eval_pow]]
 
@@ -77,7 +80,7 @@ private meta def derivative_simp : tactic unit :=
 `[simp only [derivative_C, derivative_X, derivative_X_pow, derivative_neg, derivative_add,
              derivative_sub, derivative_mul, derivative_sq]]
 
-universe u
+universes u v w
 
 namespace weierstrass_curve
 
@@ -89,7 +92,9 @@ section basic
 
 /-! ### Polynomials associated to nonsingular rational points on a Weierstrass curve -/
 
-variables {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x₁ x₂ y₁ y₂ L : R)
+variables {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A]
+  [algebra R A] (B : Type w) [comm_ring B] [algebra R B] [algebra A B] [is_scalar_tower R A B]
+  (x₁ x₂ y₁ y₂ L : R)
 
 /-- The polynomial $-Y - a_1X - a_3$ associated to negation. -/
 noncomputable def neg_polynomial : R[X][Y] := -Y - C (C W.a₁ * X + C W.a₃)
@@ -101,16 +106,26 @@ This depends on `W`, and has argument order: $x_1$, $y_1$. -/
 
 lemma neg_Y_neg_Y : W.neg_Y x₁ (W.neg_Y x₁ y₁) = y₁ := by { simp only [neg_Y], ring1 }
 
+lemma base_change_neg_Y :
+  (W.base_change A).neg_Y (algebra_map R A x₁) (algebra_map R A y₁)
+    = algebra_map R A (W.neg_Y x₁ y₁) :=
+by { simp only [neg_Y], map_simp, refl }
+
+lemma base_change_neg_Y_of_base_change (x₁ y₁ : A) :
+  (W.base_change B).neg_Y (algebra_map A B x₁) (algebra_map A B y₁)
+    = algebra_map A B ((W.base_change A).neg_Y x₁ y₁) :=
+by rw [← base_change_neg_Y, base_change_base_change]
+
 @[simp] lemma eval_neg_polynomial : (W.neg_polynomial.eval $ C y₁).eval x₁ = W.neg_Y x₁ y₁ :=
 by { rw [neg_Y, sub_sub, neg_polynomial], eval_simp }
 
-/-- The polynomial $L*(X - x_1) + y_1$ associated to the line $Y = L*(X - x_1) + y_1$,
+/-- The polynomial $L(X - x_1) + y_1$ associated to the line $Y = L(X - x_1) + y_1$,
 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$
+/-- 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)$.
@@ -131,18 +146,48 @@ where the line through them is not vertical and has a slope of $L$.
 This depends on `W`, and has argument order: $x_1$, $x_2$, $L$. -/
 @[simp] def add_X : R := L ^ 2 + W.a₁ * L - W.a₂ - x₁ - x₂
 
+lemma base_change_add_X :
+  (W.base_change A).add_X (algebra_map R A x₁) (algebra_map R A x₂) (algebra_map R A L)
+    = algebra_map R A (W.add_X x₁ x₂ L) :=
+by { simp only [add_X], map_simp, refl }
+
+lemma base_change_add_X_of_base_change (x₁ x₂ L : A) :
+  (W.base_change B).add_X (algebra_map A B x₁) (algebra_map A B x₂) (algebra_map A B L)
+    = algebra_map A B ((W.base_change A).add_X x₁ x₂ L) :=
+by rw [← base_change_add_X, base_change_base_change]
+
 /-- The $Y$-coordinate, before applying the final negation, of the addition of two affine points
 $(x_1, y_1)$ and $(x_2, y_2)$, where the line through them is not vertical and has a slope of $L$.
 
 This depends on `W`, and has argument order: $x_1$, $x_2$, $y_1$, $L$. -/
 @[simp] def add_Y' : R := L * (W.add_X x₁ x₂ L - x₁) + y₁
 
+lemma base_change_add_Y' :
+  (W.base_change A).add_Y' (algebra_map R A x₁) (algebra_map R A x₂) (algebra_map R A y₁)
+    (algebra_map R A L) = algebra_map R A (W.add_Y' x₁ x₂ y₁ L) :=
+by { simp only [add_Y', base_change_add_X], map_simp }
+
+lemma base_change_add_Y'_of_base_change (x₁ x₂ y₁ L : A) :
+  (W.base_change B).add_Y' (algebra_map A B x₁) (algebra_map A B x₂) (algebra_map A B y₁)
+    (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]
+
 /-- The $Y$-coordinate of the addition of two affine points $(x_1, y_1)$ and $(x_2, y_2)$ in `W`,
 where the line through them is not vertical and has a slope of $L$.
 
 This depends on `W`, and has argument order: $x_1$, $x_2$, $y_1$, $L$. -/
 @[simp] def add_Y : R := W.neg_Y (W.add_X x₁ x₂ L) (W.add_Y' x₁ x₂ y₁ L)
 
+lemma base_change_add_Y :
+  (W.base_change A).add_Y (algebra_map R A x₁) (algebra_map R A x₂) (algebra_map R A y₁)
+    (algebra_map R A L) = algebra_map R A (W.add_Y x₁ x₂ y₁ L) :=
+by simp only [add_Y, base_change_add_Y', base_change_add_X, base_change_neg_Y]
+
+lemma base_change_add_Y_of_base_change (x₁ x₂ y₁ L : A) :
+  (W.base_change B).add_Y (algebra_map A B x₁) (algebra_map A B x₂) (algebra_map A B y₁)
+    (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 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 :=
@@ -241,7 +286,8 @@ section addition
 
 open_locale classical
 
-variables {F : Type u} [field F] (W : weierstrass_curve F) (x₁ x₂ y₁ y₂ : F)
+variables {F : Type u} [field F] (W : weierstrass_curve F) (K : Type v) [field K] [algebra F K]
+  (x₁ x₂ y₁ y₂ : F)
 
 /-- The slope of the line through two affine points $(x_1, y_1)$ and $(x_2, y_2)$ in `W`.
 If $x_1 \ne x_2$, then this line is the secant of `W` through $(x_1, y_1)$ and $(x_2, y_2)$,
@@ -259,6 +305,10 @@ else (y₁ - y₂) / (x₁ - x₂)
 variables {W x₁ x₂ y₁ y₂} (h₁ : W.nonsingular x₁ y₁) (h₂ : W.nonsingular x₂ y₂)
   (h₁' : W.equation x₁ y₁) (h₂' : W.equation x₂ y₂)
 
+@[simp] lemma slope_of_Y_eq (hx : x₁ = x₂) (hy : y₁ = W.neg_Y x₂ y₂) :
+  W.slope x₁ x₂ y₁ y₂ = 0 :=
+by rw [slope, dif_pos hx, dif_pos hy]
+
 @[simp] lemma slope_of_Y_ne (hx : x₁ = x₂) (hy : y₁ ≠ W.neg_Y x₂ y₂) :
   W.slope x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.neg_Y x₁ y₁) :=
 by rw [slope, dif_pos hx, dif_neg hy]
@@ -272,6 +322,33 @@ lemma slope_of_Y_ne_eq_eval (hx : x₁ = x₂) (hy : y₁ ≠ W.neg_Y x₂ y₂)
 by { rw [slope_of_Y_ne hx hy, eval_polynomial_X, neg_sub], congr' 1, rw [neg_Y, eval_polynomial_Y],
      ring1 }
 
+lemma base_change_slope :
+  (W.base_change K).slope (algebra_map F K x₁) (algebra_map F K x₂) (algebra_map F K y₁)
+    (algebra_map F K y₂) = algebra_map F K (W.slope x₁ x₂ y₁ y₂) :=
+begin
+  by_cases hx : x₁ = x₂,
+  { by_cases hy : y₁ = W.neg_Y x₂ y₂,
+    { rw [slope_of_Y_eq hx hy, slope_of_Y_eq $ congr_arg _ hx, map_zero],
+      { rw [hy, base_change_neg_Y] } },
+    { rw [slope_of_Y_ne hx hy, slope_of_Y_ne $ congr_arg _ hx],
+      { map_simp,
+        simpa only [base_change_neg_Y] },
+      { rw [base_change_neg_Y],
+        contrapose! hy,
+        exact no_zero_smul_divisors.algebra_map_injective F K hy } } },
+  { rw [slope_of_X_ne hx, slope_of_X_ne],
+    { map_simp },
+    { contrapose! hx,
+      exact no_zero_smul_divisors.algebra_map_injective F K hx } }
+end
+
+lemma base_change_slope_of_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R)
+  (F : Type v) [field F] [algebra R F] (K : Type w) [field K] [algebra R K] [algebra F K]
+  [is_scalar_tower R F K] (x₁ x₂ y₁ y₂ : F) :
+  (W.base_change K).slope (algebra_map F K x₁) (algebra_map F K x₂) (algebra_map F K y₁)
+    (algebra_map F K y₂) = algebra_map F K ((W.base_change F).slope x₁ x₂ y₁ y₂) :=
+by rw [← base_change_slope, base_change_base_change]
+
 include h₁' h₂'
 
 lemma Y_eq_of_X_eq (hx : x₁ = x₂) : y₁ = y₂ ∨ y₁ = W.neg_Y x₂ y₂ :=
@@ -368,6 +445,8 @@ omit h₁ h₂
 
 namespace point
 
+variables {h₁ h₂}
+
 /-- The addition of two nonsingular rational points.
 
 Given two nonsingular rational points `P` and `Q`, use `P + Q` instead of `add P Q`. -/
@@ -391,31 +470,31 @@ noncomputable instance : add_zero_class W.point :=
 by rw [← add_def, add, dif_pos hx, dif_pos hy]
 
 @[simp] lemma some_add_self_of_Y_eq (hy : y₁ = W.neg_Y x₁ y₁) : some h₁ + some h₁ = 0 :=
-some_add_some_of_Y_eq h₁ h₁ rfl hy
+some_add_some_of_Y_eq rfl hy
 
 @[simp] lemma some_add_some_of_Y_ne (hx : x₁ = x₂) (hy : y₁ ≠ W.neg_Y x₂ y₂) :
   some h₁ + some h₂ = some (nonsingular_add h₁ h₂ $ λ _, hy) :=
 by rw [← add_def, add, dif_pos hx, dif_neg hy]
 
 lemma some_add_some_of_Y_ne' (hx : x₁ = x₂) (hy : y₁ ≠ W.neg_Y x₂ y₂) :
   some h₁ + some h₂ = -some (nonsingular_add' h₁ h₂ $ λ _, hy) :=
-some_add_some_of_Y_ne h₁ h₂ hx hy
+some_add_some_of_Y_ne hx hy
 
 @[simp] lemma some_add_self_of_Y_ne (hy : y₁ ≠ W.neg_Y x₁ y₁) :
   some h₁ + some h₁ = some (nonsingular_add h₁ h₁ $ λ _, hy) :=
-some_add_some_of_Y_ne h₁ h₁ rfl hy
+some_add_some_of_Y_ne rfl hy
 
 lemma some_add_self_of_Y_ne' (hy : y₁ ≠ W.neg_Y x₁ y₁) :
   some h₁ + some h₁ = -some (nonsingular_add' h₁ h₁ $ λ _, hy) :=
-some_add_some_of_Y_ne h₁ h₁ rfl hy
+some_add_some_of_Y_ne rfl hy
 
 @[simp] lemma some_add_some_of_X_ne (hx : x₁ ≠ x₂) :
   some h₁ + some h₂ = some (nonsingular_add h₁ h₂ $ λ h, (hx h).elim) :=
 by rw [← add_def, add, dif_neg hx]
 
 lemma some_add_some_of_X_ne' (hx : x₁ ≠ x₂) :
   some h₁ + some h₂ = -some (nonsingular_add' h₁ h₂ $ λ h, (hx h).elim) :=
-some_add_some_of_X_ne h₁ h₂ hx
+some_add_some_of_X_ne hx
 
 end point
 
@@ -431,7 +510,7 @@ namespace point
 
 @[simp] lemma add_eq_zero (P Q : W.point) : P + Q = 0 ↔ P = -Q :=
 begin
-  rcases ⟨P, Q⟩ with ⟨_ | @⟨x₁, y₁, h₁⟩, _ | @⟨x₂, y₂, h₂⟩⟩,
+  rcases ⟨P, Q⟩ with ⟨_ | @⟨x₁, y₁, _⟩, _ | @⟨x₂, y₂, _⟩⟩,
   any_goals { refl },
   { rw [zero_def, zero_add, eq_neg_iff_eq_neg, neg_zero] },
   { simp only [neg_some],
@@ -440,11 +519,11 @@ begin
       by_cases hx : x₁ = x₂,
       { by_cases hy : y₁ = W.neg_Y x₂ y₂,
         { exact ⟨hx, hy⟩ },
-        { rw [some_add_some_of_Y_ne h₁ h₂ hx hy] at h,
+        { rw [some_add_some_of_Y_ne hx hy] at h,
           contradiction } },
-      { rw [some_add_some_of_X_ne h₁ h₂ hx] at h,
+      { rw [some_add_some_of_X_ne hx] at h,
         contradiction } },
-    { exact λ ⟨hx, hy⟩, some_add_some_of_Y_eq h₁ h₂ hx hy } }
+    { exact λ ⟨hx, hy⟩, some_add_some_of_Y_eq hx hy } }
 end
 
 @[simp] lemma add_left_neg (P : W.point) : -P + P = 0 := by rw [add_eq_zero]
@@ -455,6 +534,66 @@ end point
 
 end group
 
+section base_change
+
+/-! ### Nonsingular rational points on a base changed Weierstrass curve -/
+
+variables {R : Type u} [comm_ring R] (W : weierstrass_curve R) (F : Type v) [field F] [algebra R F]
+  (K : Type w) [field K] [algebra R K] [algebra F K] [is_scalar_tower R F K]
+
+namespace point
+
+open_locale weierstrass_curve
+
+/-- The function from `W⟮F⟯` to `W⟮K⟯` induced by a base change from `F` to `K`. -/
+def of_base_change_fun : W⟮F⟯ → W⟮K⟯
+| 0        := 0
+| (some h) := some $ (nonsingular_iff_base_change_of_base_change W F K _ _).mp h
+
+/-- The group homomorphism from `W⟮F⟯` to `W⟮K⟯` induced by a base change from `F` to `K`. -/
+@[simps] def of_base_change : W⟮F⟯ →+ W⟮K⟯ :=
+{ to_fun    := of_base_change_fun W F K,
+  map_zero' := rfl,
+  map_add'  :=
+  begin
+    rintro (_ | @⟨x₁, y₁, _⟩) (_ | @⟨x₂, y₂, _⟩),
+    any_goals { refl },
+    by_cases hx : x₁ = x₂,
+    { by_cases hy : y₁ = (W.base_change F).neg_Y x₂ y₂,
+      { simp only [some_add_some_of_Y_eq hx hy, of_base_change_fun],
+        rw [some_add_some_of_Y_eq $ congr_arg _ hx],
+        { rw [hy, base_change_neg_Y_of_base_change] } },
+      { simp only [some_add_some_of_Y_ne hx hy, of_base_change_fun],
+        rw [some_add_some_of_Y_ne $ congr_arg _ hx],
+        { simp only [base_change_add_X_of_base_change, base_change_add_Y_of_base_change,
+                     base_change_slope_of_base_change],
+          exact ⟨rfl, rfl⟩ },
+        { rw [base_change_neg_Y_of_base_change],
+          contrapose! hy,
+          exact no_zero_smul_divisors.algebra_map_injective F K hy } } },
+    { simp only [some_add_some_of_X_ne hx, of_base_change_fun],
+      rw [some_add_some_of_X_ne],
+      { simp only [base_change_add_X_of_base_change, base_change_add_Y_of_base_change,
+                   base_change_slope_of_base_change],
+        exact ⟨rfl, rfl⟩ },
+      { contrapose! hx,
+        exact no_zero_smul_divisors.algebra_map_injective F K hx } }
+  end }
+
+lemma of_base_change_injective : function.injective $ of_base_change W F K :=
+begin
+  rintro (_ | _) (_ | _) h,
+  { refl },
+  any_goals { contradiction },
+  simp only,
+  exact ⟨no_zero_smul_divisors.algebra_map_injective F K (some.inj h).left,
+    no_zero_smul_divisors.algebra_map_injective F K (some.inj h).right⟩
+end
+
+end point
+
+end base_change
+
 end weierstrass_curve
 
 namespace elliptic_curve

src/algebraic_geometry/elliptic_curve/weierstrass.lean

@@ -85,7 +85,7 @@ private meta def eval_simp : tactic unit :=
 
 private meta def C_simp : tactic unit := `[simp only [C_0, C_1, C_neg, C_add, C_sub, C_mul, C_pow]]
 
-universes u v
+universes u v w
 
 variable {R : Type u}
 
@@ -180,12 +180,13 @@ by { dsimp, ring1 }
 
 end variable_change
 
+variables (A : Type v) [comm_ring A] [algebra R A] (B : Type w) [comm_ring B] [algebra R B]
+  [algebra A B] [is_scalar_tower R A B]
+
 section base_change
 
 /-! ### Base changes -/
 
-variables (A : Type v) [comm_ring A] [algebra R A]
-
 /-- The Weierstrass curve over `R` base changed to `A`. -/
 @[simps] def base_change : weierstrass_curve A :=
 ⟨algebra_map R A W.a₁, algebra_map R A W.a₂, algebra_map R A W.a₃, algebra_map R A W.a₄,
@@ -213,6 +214,11 @@ by { simp only [c₆, base_change_b₂, base_change_b₄, base_change_b₆], map
 @[simp, nolint simp_nf] lemma base_change_Δ : (W.base_change A).Δ = algebra_map R A W.Δ :=
 by { simp only [Δ, base_change_b₂, base_change_b₄, base_change_b₆, base_change_b₈], map_simp }
 
+lemma base_change_self : W.base_change R = W := by ext; refl
+
+lemma base_change_base_change : (W.base_change A).base_change B = W.base_change B :=
+by ext; exact (is_scalar_tower.algebra_map_apply R A B _).symm
+
 end base_change
 
 section torsion_polynomial
@@ -321,6 +327,20 @@ begin
   ring1
 end
 
+lemma equation_iff_base_change [nontrivial A] [no_zero_smul_divisors R A] (x y : R) :
+  W.equation x y ↔ (W.base_change A).equation (algebra_map R A x) (algebra_map R A y) :=
+begin
+  simp only [equation_iff],
+  refine ⟨λ h, _, λ h, _⟩,
+  { convert congr_arg (algebra_map R A) h; { map_simp, refl } },
+  { apply no_zero_smul_divisors.algebra_map_injective R A, map_simp, exact h }
+end
+
+lemma equation_iff_base_change_of_base_change [nontrivial B] [no_zero_smul_divisors A B] (x y : A) :
+  (W.base_change A).equation x y
+    ↔ (W.base_change B).equation (algebra_map A B x) (algebra_map A B y) :=
+by rw [equation_iff_base_change (W.base_change A) B, base_change_base_change]
+
 /-! ### Nonsingularity of Weierstrass curves -/
 
 /-- The partial derivative $W_X(X, Y)$ of $W(X, Y)$ with respect to $X$.
@@ -376,6 +396,21 @@ begin
   congr' 4; ring1
 end
 
+lemma nonsingular_iff_base_change [nontrivial A] [no_zero_smul_divisors R A] (x y : R) :
+  W.nonsingular x y ↔ (W.base_change A).nonsingular (algebra_map R A x) (algebra_map R A y) :=
+begin
+  rw [nonsingular_iff, nonsingular_iff, and_congr $ W.equation_iff_base_change A x y],
+  refine ⟨or.imp (not_imp_not.mpr $ λ h, _) (not_imp_not.mpr $ λ h, _),
+    or.imp (not_imp_not.mpr $ λ h, _) (not_imp_not.mpr $ λ h, _)⟩,
+  any_goals { apply no_zero_smul_divisors.algebra_map_injective R A, map_simp, exact h },
+  any_goals { convert congr_arg (algebra_map R A) h; { map_simp, refl } }
+end
+
+lemma nonsingular_iff_base_change_of_base_change [nontrivial B] [no_zero_smul_divisors A B]
+  (x y : A) : (W.base_change A).nonsingular x y
+    ↔ (W.base_change B).nonsingular (algebra_map A B x) (algebra_map A B y) :=
+by rw [nonsingular_iff_base_change (W.base_change A) B, base_change_base_change]
+
 lemma nonsingular_zero_of_Δ_ne_zero (h : W.equation 0 0) (hΔ : W.Δ ≠ 0) : W.nonsingular 0 0 :=
 by { simp only [equation_zero, nonsingular_zero] at *, contrapose! hΔ, simp [h, hΔ] }