instMulActionVariableChange — Mathlib

English

A linear change of variables acts on Weierstrass curves, turning W into C • W, and this action makes Weierstrass curves transform coherently under changes of coordinates.

Русский

Линейное преобразование переменных действует на кривые Вейерштрасса, переводя W в C • W, и это действие сохраняет согласованность преобразований координат.

LaTeX

$$$\\text{There is a canonical }\\mathrm{MulAction}(\\mathrm{VariableChange}(R),\\mathrm{WeierstrassCurve}(R)).$$$

Lean4

instance : MulAction (VariableChange R) (WeierstrassCurve R)
    where
  one_smul
    W := by
    rw [VariableChange.one_def, variableChange_def, inv_one, Units.val_one]
    ext <;> dsimp only <;> ring1
  mul_smul C C'
    W := by
    simp only [VariableChange.mul_def, variableChange_def]
    ext <;> simp only [mul_inv, Units.val_mul]
    · linear_combination ↑C.u⁻¹ * C.s * 2 * C'.u.inv_mul
    ·
      linear_combination
        C.s * (-C'.s * 2 - W.a₁) * C.u⁻¹ ^ 2 * ↑C'.u⁻¹ * C'.u.inv_mul +
          (C.r * 3 - C.s ^ 2) * C.u⁻¹ ^ 2 * pow_mul_pow_eq_one 2 C'.u.inv_mul
    ·
      linear_combination
        C.r * (C'.s * 2 + W.a₁) * C.u⁻¹ ^ 3 * ↑C'.u⁻¹ * pow_mul_pow_eq_one 2 C'.u.inv_mul +
          C.t * 2 * C.u⁻¹ ^ 3 * pow_mul_pow_eq_one 3 C'.u.inv_mul
    ·
      linear_combination
        C.s * (-W.a₃ - C'.r * W.a₁ - C'.t * 2) * C.u⁻¹ ^ 4 * C'.u⁻¹ ^ 3 * C'.u.inv_mul +
              C.u⁻¹ ^ 4 * C'.u⁻¹ ^ 2 * (C.r * C'.r * 6 + C.r * W.a₂ * 2 - C'.s * C.r * W.a₁ * 2 - C'.s ^ 2 * C.r * 2) *
                pow_mul_pow_eq_one 2 C'.u.inv_mul -
            C.u⁻¹ ^ 4 * ↑C'.u⁻¹ * (C.s * C'.s * C.r * 2 + C.s * C.r * W.a₁ + C'.s * C.t * 2 + C.t * W.a₁) *
              pow_mul_pow_eq_one 3 C'.u.inv_mul +
          C.u⁻¹ ^ 4 * (C.r ^ 2 * 3 - C.s * C.t * 2) * pow_mul_pow_eq_one 4 C'.u.inv_mul
    ·
      linear_combination
        C.r * C.u⁻¹ ^ 6 * C'.u⁻¹ ^ 4 *
                    (C'.r * W.a₂ * 2 - C'.r * C'.s * W.a₁ + C'.r ^ 2 * 3 + W.a₄ - C'.s * C'.t * 2 - C'.s * W.a₃ -
                      C'.t * W.a₁) *
                  pow_mul_pow_eq_one 2 C'.u.inv_mul -
                C.u⁻¹ ^ 6 * C'.u⁻¹ ^ 3 * C.t * (C'.r * W.a₁ + C'.t * 2 + W.a₃) * pow_mul_pow_eq_one 3 C'.u.inv_mul +
              C.r ^ 2 * C.u⁻¹ ^ 6 * C'.u⁻¹ ^ 2 * (C'.r * 3 + W.a₂ - C'.s * W.a₁ - C'.s ^ 2) *
                pow_mul_pow_eq_one 4 C'.u.inv_mul -
            C.r * C.t * C.u⁻¹ ^ 6 * ↑C'.u⁻¹ * (C'.s * 2 + W.a₁) * pow_mul_pow_eq_one 5 C'.u.inv_mul +
          C.u⁻¹ ^ 6 * (C.r ^ 3 - C.t ^ 2) * pow_mul_pow_eq_one 6 C'.u.inv_mul

Похожие утверждения