baseChange_nonsingular — Mathlib

English

A base change along an injective f preserves the property of nonsingularity of a pair of affine points: (W.map f).toAffine.Nonsingular (f x) (f y) iff W.Nonsingular x y.

Русский

При базовом переносе по инъективному f сохраняется свойство невырожденности пары точек на аффинной кривой: (W.map f).toAffine.Nonsingular (f x) (f y) эквивалентно W.Nonsingular x y.

LaTeX

$$$(W.map f).toAffine.Nonsingular (f x) (f y) \iff W.Nonsingular x y$$$

Lean4

theorem baseChange_nonsingular (hf : Function.Injective f) :
    (W.baseChange B).toAffine.Nonsingular (f x) (f y) ↔ (W.baseChange A).toAffine.Nonsingular x y := by
  rw [← map_nonsingular _ _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]

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