nonsingular_of_equiv — Mathlib

English

Let P and Q be two 3-tuples over a commutative ring R that are projectively equivalent (P ≈ Q). Then the projective Weierstrass curve W′ is nonsingular at P if and only if it is nonsingular at Q.

Русский

Пусть P и Q — тройки из коммутативной кольца R, связанные проектной эквивалентностью (P ≈ Q). Тогда кривая Вейерштрасса W′ в проективной модели не имеет сингулярностей в точке, соответствующей P, тогда и только тогда, когда сингулярность отсутствует в точке, соответствующей Q.

LaTeX

$$$\\forall R [\\text{CommRing }R],\\; W'\\text{ projective}, \\; P,Q: \\mathrm{Fin}(3)\\to R,\\; P \\approx Q \\Rightarrow W'.\\mathrm{Nonsingular} P \\iff W'.\\mathrm{Nonsingular} Q$$$

Lean4

theorem nonsingular_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Nonsingular P ↔ W'.Nonsingular Q :=
  by
  rcases h with ⟨u, rfl⟩
  exact nonsingular_smul Q u.isUnit

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