English
A Weierstrass curve W has good reduction over R if and only if its reduction is an elliptic curve over the residue field.
Русский
Кривая Вейерштрасса W имеет хорошую редукцию над R тогда и только тогда, когда её редукция является эллиптической кривой над остаточным полем.
LaTeX
$$$\\mathrm{IsGoodReduction}(R,W) \\;\\iff\\; (\\mathrm{reduction}(R,W)).IsElliptic.$$$
Lean4
theorem isGoodReduction_iff_isElliptic_reduction {W : WeierstrassCurve K} [IsMinimal R W] :
IsGoodReduction R W ↔ (W.reduction R).IsElliptic :=
by
refine Iff.trans ?_ (W.reduction R).isElliptic_iff.symm
simp only [reduction, map_Δ, isUnit_iff_ne_zero, ne_eq, residue_eq_zero_iff]
have h :
¬(valuation K (maximalIdeal R) (algebraMap R K (integralModel R W).Δ) < 1) ↔
(integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R :=
not_iff_not.mpr <| valuation_lt_one_iff_mem _ _
refine ((integralModel_Δ_eq R W ▸ isGoodReduction_iff _ _).trans ?_).trans h
simpa using (valuation_le_one _ _).ge_iff_eq.symm
