reduction — Mathlib

English

The reduction of a Weierstrass curve W over K, given by a minimal Weierstrass equation, is a Weierstrass curve over the residue field of R.

Русский

Редукция кривой Вейерштрасса W над K, заданной минимальным уравнением, является кривой Вейершстра над остаточным полем R.

LaTeX

$$$\\mathrm{reduction}(R,W) = (\\mathrm{integralModel}(R,W)).map(\\mathrm{residue}(R)).$$$

Lean4

/-- The reduction of a Weierstrass curve over `K` given by a minimal Weierstrass equation,
which is a Weierstrass curve over the residue field of `R`. -/
noncomputable def reduction (W : WeierstrassCurve K) [IsMinimal R W] : WeierstrassCurve (ResidueField R) :=
  (integralModel R W).map (residue R)

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