NonsingularLift — Mathlib

English

Equivalence of nonsingularity for lifted and base points in projective Weierstrass curves.

Русский

Эквивалентность несингулярности для лифта и базовой точки в проективной кривой Вейершстраса.

LaTeX

$$$W'.NonsingularLift(\\overline{P}) \\iff W'.Nonsingular P$$$

Lean4

/-- The proposition that a projective point class on a Weierstrass curve `W` is nonsingular.

If `P` is a projective point representative on `W`, then `W.NonsingularLift ⟦P⟧` is definitionally
equivalent to `W.Nonsingular P`.

Note that this definition is only mathematically accurate for fields. -/
def NonsingularLift (P : PointClass R) : Prop :=
  P.lift W'.Nonsingular fun _ _ => propext ∘ nonsingular_of_equiv

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