chore(AlgebraicGeometry/EllipticCurve/*): refactor VariableChange (#23217)

Drop certain definitions in `VariableChange` in favor of mathlib's built-in notation:

- `VariableChange.id` -> `(1 : VariableChange R)`
- `VariableChange.comp C C'` -> `C * C'`
- `VariableChange.inv C` -> `C⁻¹`
- `W.variableChange C` -> `C • W`

Author: acmepjz

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

@@ -202,7 +202,7 @@ lemma equation_zero : W'.Equation 0 0 ↔ W'.a₆ = 0 := by
   rw [Equation, evalEval_polynomial_zero, neg_eq_zero]
 
 lemma equation_iff_variableChange (x y : R) :
-    W'.Equation x y ↔ (W'.variableChange ⟨1, x, 0, y⟩).toAffine.Equation 0 0 := by
+    W'.Equation x y ↔ (VariableChange.mk 1 x 0 y • W').toAffine.Equation 0 0 := by
   rw [equation_iff', ← neg_eq_zero, equation_zero, variableChange_a₆, inv_one, Units.val_one]
   congr! 1
   ring1
@@ -271,10 +271,10 @@ lemma nonsingular_zero : W'.Nonsingular 0 0 ↔ W'.a₆ = 0 ∧ (W'.a₃ ≠ 0 
     or_comm]
 
 lemma nonsingular_iff_variableChange (x y : R) :
-    W'.Nonsingular x y ↔ (W'.variableChange ⟨1, x, 0, y⟩).toAffine.Nonsingular 0 0 := by
+    W'.Nonsingular x y ↔ (VariableChange.mk 1 x 0 y • W').toAffine.Nonsingular 0 0 := by
   rw [nonsingular_iff', equation_iff_variableChange, equation_zero, ← neg_ne_zero, or_comm,
     nonsingular_zero, variableChange_a₃, variableChange_a₄, inv_one, Units.val_one]
-  simp only [variableChange]
+  simp only [variableChange_def]
   congr! 3 <;> ring1
 
 private lemma equation_zero_iff_nonsingular_zero_of_Δ_ne_zero (hΔ : W'.Δ ≠ 0) :

Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean

@@ -33,7 +33,7 @@ variable [CharP F 2]
 omit [E.IsElliptic] [E'.IsElliptic] in
 private lemma exists_variableChange_of_char_two_of_j_ne_zero
     [E.IsCharTwoJNeZeroNF] [E'.IsCharTwoJNeZeroNF] (heq : E.a₆ = E'.a₆) :
-    ∃ C : VariableChange F, E.variableChange C = E' := by
+    ∃ C : VariableChange F, C • E = E' := by
   obtain ⟨s, hs⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 2 2
     1 1 (E.a₂ + E'.a₂) (by norm_num) (by norm_num) one_ne_zero
   use ⟨1, 0, s, 0⟩
@@ -51,8 +51,7 @@ private lemma exists_variableChange_of_char_two_of_j_ne_zero
     ring1
 
 private lemma exists_variableChange_of_char_two_of_j_eq_zero
-    [E.IsCharTwoJEqZeroNF] [E'.IsCharTwoJEqZeroNF] :
-    ∃ C : VariableChange F, E.variableChange C = E' := by
+    [E.IsCharTwoJEqZeroNF] [E'.IsCharTwoJEqZeroNF] : ∃ C : VariableChange F, C • E = E' := by
   have ha₃ := E.Δ'.ne_zero
   rw [E.coe_Δ', Δ_of_isCharTwoJEqZeroNF_of_char_two, pow_ne_zero_iff (Nat.succ_ne_zero _)] at ha₃
   have ha₃' := E'.Δ'.ne_zero
@@ -85,29 +84,26 @@ private lemma exists_variableChange_of_char_two_of_j_eq_zero
     linear_combination ht - (t ^ 2 + E.a₃ * t) * CharP.cast_eq_zero F 2
 
 private lemma exists_variableChange_of_char_two (heq : E.j = E'.j) :
-    ∃ C : VariableChange F, E.variableChange C = E' := by
+    ∃ C : VariableChange F, C • E = E' := by
   obtain ⟨C, _ | _⟩ := E.exists_variableChange_isCharTwoNF
   · obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharTwoNF
     · simp_rw [← variableChange_j E C, ← variableChange_j E' C',
         j_of_isCharTwoJNeZeroNF_of_char_two, one_div, inv_inj] at heq
       obtain ⟨C'', hC⟩ := exists_variableChange_of_char_two_of_j_ne_zero _ _ heq
-      use (C'.inv.comp C'').comp C
-      rw [variableChange_comp, variableChange_comp, hC, ← variableChange_comp,
-        VariableChange.comp_left_inv, variableChange_id]
-    · have h := (E.variableChange C).j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
+      use C'⁻¹ * C'' * C
+      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]
+    · have h := (C • E).j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
       rw [variableChange_j, heq, ← variableChange_j E' C',
         j_of_isCharTwoJEqZeroNF_of_char_two] at h
       exact False.elim (h rfl)
   · obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharTwoNF
-    · have h := (E'.variableChange C').j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
+    · have h := (C' • E').j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
       rw [variableChange_j, ← heq, ← variableChange_j E C,
         j_of_isCharTwoJEqZeroNF_of_char_two] at h
       exact False.elim (h rfl)
-    · obtain ⟨C'', hC⟩ := exists_variableChange_of_char_two_of_j_eq_zero
-        (E.variableChange C) (E'.variableChange C')
-      use (C'.inv.comp C'').comp C
-      rw [variableChange_comp, variableChange_comp, hC, ← variableChange_comp,
-        VariableChange.comp_left_inv, variableChange_id]
+    · obtain ⟨C'', hC⟩ := exists_variableChange_of_char_two_of_j_eq_zero (C • E) (C' • E')
+      use C'⁻¹ * C'' * C
+      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]
 
 end CharTwo
 
@@ -117,7 +113,7 @@ variable [CharP F 3]
 
 private lemma exists_variableChange_of_char_three_of_j_ne_zero
     [E.IsCharThreeJNeZeroNF] [E'.IsCharThreeJNeZeroNF] (heq : E.j = E'.j) :
-    ∃ C : VariableChange F, E.variableChange C = E' := by
+    ∃ C : VariableChange F, C • E = E' := by
   have h := E.Δ'.ne_zero
   rw [E.coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three, mul_ne_zero_iff, neg_ne_zero,
     pow_ne_zero_iff three_ne_zero] at h
@@ -153,8 +149,7 @@ private lemma exists_variableChange_of_char_three_of_j_ne_zero
     linear_combination heq
 
 private lemma exists_variableChange_of_char_three_of_j_eq_zero
-    [E.IsShortNF] [E'.IsShortNF] :
-    ∃ C : VariableChange F, E.variableChange C = E' := by
+    [E.IsShortNF] [E'.IsShortNF] : ∃ C : VariableChange F, C • E = E' := by
   have ha₄ := E.Δ'.ne_zero
   rw [E.coe_Δ', Δ_of_isShortNF_of_char_three, neg_ne_zero, pow_ne_zero_iff three_ne_zero] at ha₄
   have ha₄' := E'.Δ'.ne_zero
@@ -187,34 +182,31 @@ private lemma exists_variableChange_of_char_three_of_j_eq_zero
     linear_combination hr
 
 private lemma exists_variableChange_of_char_three (heq : E.j = E'.j) :
-    ∃ C : VariableChange F, E.variableChange C = E' := by
+    ∃ C : VariableChange F, C • E = E' := by
   obtain ⟨C, _ | _⟩ := E.exists_variableChange_isCharThreeNF
   · obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF
     · rw [← variableChange_j E C, ← variableChange_j E' C'] at heq
       obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_ne_zero _ _ heq
-      use (C'.inv.comp C'').comp C
-      rw [variableChange_comp, variableChange_comp, hC, ← variableChange_comp,
-        VariableChange.comp_left_inv, variableChange_id]
-    · have h := (E.variableChange C).j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
+      use C'⁻¹ * C'' * C
+      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]
+    · have h := (C • E).j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
       rw [variableChange_j, heq, ← variableChange_j E' C', j_of_isShortNF_of_char_three] at h
       exact False.elim (h rfl)
   · obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF
-    · have h := (E'.variableChange C').j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
+    · have h := (C' • E').j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
       rw [variableChange_j, ← heq, ← variableChange_j E C, j_of_isShortNF_of_char_three] at h
       exact False.elim (h rfl)
-    · obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_eq_zero
-        (E.variableChange C) (E'.variableChange C')
-      use (C'.inv.comp C'').comp C
-      rw [variableChange_comp, variableChange_comp, hC, ← variableChange_comp,
-        VariableChange.comp_left_inv, variableChange_id]
+    · obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_eq_zero (C • E) (C' • E')
+      use C'⁻¹ * C'' * C
+      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]
 
 end CharThree
 
 section CharNeTwoOrThree
 
 private lemma exists_variableChange_of_char_ne_two_or_three
     {p : ℕ} [CharP F p] (hchar2 : p ≠ 2) (hchar3 : p ≠ 3) (heq : E.j = E'.j) :
-    ∃ C : VariableChange F, E.variableChange C = E' := by
+    ∃ C : VariableChange F, C • E = E' := by
   replace hchar2 : (2 : F) ≠ 0 := CharP.cast_ne_zero_of_ne_of_prime F Nat.prime_two hchar2
   replace hchar3 : (3 : F) ≠ 0 := CharP.cast_ne_zero_of_ne_of_prime F Nat.prime_three hchar3
   haveI := NeZero.mk hchar2
@@ -232,13 +224,12 @@ private lemma exists_variableChange_of_char_ne_two_or_three
   · obtain ⟨C, hE⟩ := E.exists_variableChange_isShortNF
     rw [← variableChange_j E C] at heq
     obtain ⟨C', hC⟩ := this _ heq hE
-    exact ⟨C'.comp C, by rwa [variableChange_comp]⟩
+    exact ⟨C' * C, by rwa [mul_smul]⟩
   wlog _ : E'.IsShortNF generalizing E'
   · obtain ⟨C, hE'⟩ := E'.exists_variableChange_isShortNF
     rw [← variableChange_j E' C] at heq
     obtain ⟨C', hC⟩ := this _ heq hE'
-    exact ⟨C.inv.comp C', by rw [variableChange_comp, hC, ← variableChange_comp,
-      VariableChange.comp_left_inv, variableChange_id]⟩
+    exact ⟨C⁻¹ * C', by rw [mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]⟩
   simp_rw [j, Units.val_inv_eq_inv_val, inv_mul_eq_div,
     div_eq_div_iff E.Δ'.ne_zero E'.Δ'.ne_zero, coe_Δ', Δ_of_isShortNF, c₄_of_isShortNF] at heq
   replace heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2 := by
@@ -335,8 +326,7 @@ end CharNeTwoOrThree
 /-- If there are two elliptic curves with the same `j`-invariants defined over a
 separably closed field, then there exists a change of variables over that field which change
 one curve into another. -/
-theorem exists_variableChange_of_j_eq (heq : E.j = E'.j) :
-    ∃ C : VariableChange F, E.variableChange C = E' := by
+theorem exists_variableChange_of_j_eq (heq : E.j = E'.j) : ∃ C : VariableChange F, C • E = E' := by
   obtain ⟨p, _⟩ := CharP.exists F
   by_cases hchar2 : p = 2
   · subst hchar2

Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean

@@ -162,11 +162,10 @@ a normal form of characteristic ≠ 2, provided that 2 is invertible in the ring
 @[simps]
 def toCharNeTwoNF : VariableChange R := ⟨1, 0, ⅟2 * -W.a₁, ⅟2 * -W.a₃⟩
 
-instance toCharNeTwoNF_spec : (W.variableChange W.toCharNeTwoNF).IsCharNeTwoNF := by
+instance toCharNeTwoNF_spec : (W.toCharNeTwoNF • W).IsCharNeTwoNF := by
   constructor <;> simp
 
-theorem exists_variableChange_isCharNeTwoNF :
-    ∃ C : VariableChange R, (W.variableChange C).IsCharNeTwoNF :=
+theorem exists_variableChange_isCharNeTwoNF : ∃ C : VariableChange R, (C • W).IsCharNeTwoNF :=
   ⟨_, W.toCharNeTwoNF_spec⟩
 
 end VariableChange
@@ -262,14 +261,13 @@ variable [Invertible (2 : R)] [Invertible (3 : R)]
 a short normal form, provided that 2 and 3 are invertible in the ring.
 It is the composition of an explicit change of variables with `WeierstrassCurve.toCharNeTwoNF`. -/
 def toShortNF : VariableChange R :=
-  .comp ⟨1, ⅟3 * -(W.variableChange W.toCharNeTwoNF).a₂, 0, 0⟩ W.toCharNeTwoNF
+  ⟨1, ⅟3 * -(W.toCharNeTwoNF • W).a₂, 0, 0⟩ * W.toCharNeTwoNF
 
-instance toShortNF_spec : (W.variableChange W.toShortNF).IsShortNF := by
-  rw [toShortNF, variableChange_comp]
+instance toShortNF_spec : (W.toShortNF • W).IsShortNF := by
+  rw [toShortNF, mul_smul]
   constructor <;> simp
 
-theorem exists_variableChange_isShortNF :
-    ∃ C : VariableChange R, (W.variableChange C).IsShortNF :=
+theorem exists_variableChange_isShortNF : ∃ C : VariableChange R, (C • W).IsShortNF :=
   ⟨_, W.toShortNF_spec⟩
 
 end VariableChange
@@ -392,12 +390,11 @@ def toShortNFOfCharThree : VariableChange R :=
   letI : Invertible (2 : R) := ⟨2, h, h⟩
   W.toCharNeTwoNF
 
-lemma toShortNFOfCharThree_a₂ : (W.variableChange W.toShortNFOfCharThree).a₂ = W.b₂ := by
+lemma toShortNFOfCharThree_a₂ : (W.toShortNFOfCharThree • W).a₂ = W.b₂ := by
   simp_rw [toShortNFOfCharThree, toCharNeTwoNF, variableChange_a₂, inv_one, Units.val_one, b₂]
   linear_combination (-W.a₂ - W.a₁ ^ 2) * CharP.cast_eq_zero R 3
 
-theorem toShortNFOfCharThree_spec (hb₂ : W.b₂ = 0) :
-    (W.variableChange W.toShortNFOfCharThree).IsShortNF := by
+theorem toShortNFOfCharThree_spec (hb₂ : W.b₂ = 0) : (W.toShortNFOfCharThree • W).IsShortNF := by
   have h : (2 : R) * 2 = 1 := by linear_combination CharP.cast_eq_zero R 3
   letI : Invertible (2 : R) := ⟨2, h, h⟩
   have H := W.toCharNeTwoNF_spec
@@ -412,15 +409,15 @@ there is an explicit change of variables of it to `WeierstrassCurve.IsCharThreeN
 It is the composition of an explicit change of variables with
 `WeierstrassCurve.toShortNFOfCharThree`. -/
 def toCharThreeNF : VariableChange F :=
-  .comp ⟨1, (W.variableChange W.toShortNFOfCharThree).a₄ /
-    (W.variableChange W.toShortNFOfCharThree).a₂, 0, 0⟩ W.toShortNFOfCharThree
+  ⟨1, (W.toShortNFOfCharThree • W).a₄ /
+    (W.toShortNFOfCharThree • W).a₂, 0, 0⟩ * W.toShortNFOfCharThree
 
 theorem toCharThreeNF_spec_of_b₂_ne_zero (hb₂ : W.b₂ ≠ 0) :
-    (W.variableChange W.toCharThreeNF).IsCharThreeJNeZeroNF := by
+    (W.toCharThreeNF • W).IsCharThreeJNeZeroNF := by
   have h : (2 : F) * 2 = 1 := by linear_combination CharP.cast_eq_zero F 3
   letI : Invertible (2 : F) := ⟨2, h, h⟩
-  rw [toCharThreeNF, variableChange_comp]
-  set W' := W.variableChange W.toShortNFOfCharThree
+  rw [toCharThreeNF, mul_smul]
+  set W' := W.toShortNFOfCharThree • W
   haveI : W'.IsCharNeTwoNF := W.toCharNeTwoNF_spec
   constructor
   · simp
@@ -429,21 +426,18 @@ theorem toCharThreeNF_spec_of_b₂_ne_zero (hb₂ : W.b₂ ≠ 0) :
     field_simp [ha₂]
     linear_combination (W'.a₄ * W'.a₂ ^ 2 + W'.a₄ ^ 2) * CharP.cast_eq_zero F 3
 
-theorem toCharThreeNF_spec_of_b₂_eq_zero (hb₂ : W.b₂ = 0) :
-    (W.variableChange W.toCharThreeNF).IsShortNF := by
-  rw [toCharThreeNF, toShortNFOfCharThree_a₂, hb₂, div_zero, ← VariableChange.id,
-    VariableChange.id_comp]
+theorem toCharThreeNF_spec_of_b₂_eq_zero (hb₂ : W.b₂ = 0) : (W.toCharThreeNF • W).IsShortNF := by
+  rw [toCharThreeNF, toShortNFOfCharThree_a₂, hb₂, div_zero, ← VariableChange.one_def, one_mul]
   exact W.toShortNFOfCharThree_spec hb₂
 
-instance toCharThreeNF_spec : (W.variableChange W.toCharThreeNF).IsCharThreeNF := by
+instance toCharThreeNF_spec : (W.toCharThreeNF • W).IsCharThreeNF := by
   by_cases hb₂ : W.b₂ = 0
   · haveI := W.toCharThreeNF_spec_of_b₂_eq_zero hb₂
     infer_instance
   · haveI := W.toCharThreeNF_spec_of_b₂_ne_zero hb₂
     infer_instance
 
-theorem exists_variableChange_isCharThreeNF :
-    ∃ C : VariableChange F, (W.variableChange C).IsCharThreeNF :=
+theorem exists_variableChange_isCharThreeNF : ∃ C : VariableChange F, (C • W).IsCharThreeNF :=
   ⟨_, W.toCharThreeNF_spec⟩
 
 end VariableChange
@@ -655,7 +649,7 @@ there is an explicit change of variables of it to `Y² + a₃Y = X³ + a₄X + a
 def toCharTwoJEqZeroNF : VariableChange R := ⟨1, W.a₂, 0, 0⟩
 
 theorem toCharTwoJEqZeroNF_spec (ha₁ : W.a₁ = 0) :
-    (W.variableChange W.toCharTwoJEqZeroNF).IsCharTwoJEqZeroNF := by
+    (W.toCharTwoJEqZeroNF • W).IsCharTwoJEqZeroNF := by
   constructor
   · simp [toCharTwoJEqZeroNF, ha₁]
   · simp_rw [toCharTwoJEqZeroNF, variableChange_a₂, inv_one, Units.val_one]
@@ -670,7 +664,7 @@ def toCharTwoJNeZeroNF (W : WeierstrassCurve F) (ha₁ : W.a₁ ≠ 0) : Variabl
   ⟨Units.mk0 _ ha₁, W.a₃ / W.a₁, 0, (W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) / W.a₁ ^ 3⟩
 
 theorem toCharTwoJNeZeroNF_spec (ha₁ : W.a₁ ≠ 0) :
-    (W.variableChange (W.toCharTwoJNeZeroNF ha₁)).IsCharTwoJNeZeroNF := by
+    (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF := by
   constructor
   · simp [toCharTwoJNeZeroNF, ha₁]
   · field_simp [toCharTwoJNeZeroNF]
@@ -685,7 +679,7 @@ there is an explicit change of variables of it to `WeierstrassCurve.IsCharTwoNF`
 def toCharTwoNF [DecidableEq F] : VariableChange F :=
   if ha₁ : W.a₁ = 0 then W.toCharTwoJEqZeroNF else W.toCharTwoJNeZeroNF ha₁
 
-instance toCharTwoNF_spec [DecidableEq F] : (W.variableChange W.toCharTwoNF).IsCharTwoNF := by
+instance toCharTwoNF_spec [DecidableEq F] : (W.toCharTwoNF • W).IsCharTwoNF := by
   by_cases ha₁ : W.a₁ = 0
   · rw [toCharTwoNF, dif_pos ha₁]
     haveI := W.toCharTwoJEqZeroNF_spec ha₁
@@ -694,8 +688,7 @@ instance toCharTwoNF_spec [DecidableEq F] : (W.variableChange W.toCharTwoNF).IsC
     haveI := W.toCharTwoJNeZeroNF_spec ha₁
     infer_instance
 
-theorem exists_variableChange_isCharTwoNF :
-    ∃ C : VariableChange F, (W.variableChange C).IsCharTwoNF := by
+theorem exists_variableChange_isCharTwoNF : ∃ C : VariableChange F, (C • W).IsCharTwoNF := by
   classical
   exact ⟨_, W.toCharTwoNF_spec⟩