English
The Weierstrass curve over R induced by a minimal equation yields a Weierstrass curve over the residue field, describing reduction modulo the maximal ideal.
Русский
Кривая Вейерштрасса над R, полученная из минимального уравнения, даёт кривую Вейерштрасса над остаточным полем, описывая редукцию по максимальной идеали.
LaTeX
$$$ (W : WeierstrassCurve K)\\; [IsMinimal\\ R\\ W] \\; \\Rightarrow\\; (W.reduction\\ R) \\text{ is a WeierstrassCurve over } \\mathrm{ResidueField}(R).$$$
Lean4
/-- The Weierstrass curve over `R` induced by an admissible linear change of variables
`(X, Y) ↦ (u²X + r, u³Y + u²sX + t)` for some `u` in `Rˣ` and some `r, s, t` in `R`. -/
theorem variableChange_def :
C • W =
{ a₁ := C.u⁻¹ * (W.a₁ + 2 * C.s)
a₂ := C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)
a₃ := C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)
a₄ := C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)
a₆ := C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁) } :=
rfl
