baseChange_nonsingular — Mathlib

English

Nonsingularity is preserved under a compatible base change: a point P yields a nonsingular base-change point iff the original P is nonsingular after the corresponding base-change.

Русский

Свойство невырожденности сохраняется при совместимом базовом изменении: точка P даёт невырожденную точку после изменения база-из A на B тогда и только тогда, когда исходная точка P невырождена после соответствующего изменения.

LaTeX

$$$ (W'.baseChange B).toProjective.Nonsingular (f \\circ P) \\;\\iff\\; (W'.baseChange A).toProjective.Nonsingular P $$$

Lean4

theorem baseChange_nonsingular (hf : Function.Injective f) :
    (W'.baseChange B).toProjective.Nonsingular (f ∘ P) ↔ (W'.baseChange A).toProjective.Nonsingular P := by
  rw [← RingHom.coe_coe, ← map_nonsingular P hf, AlgHom.toRingHom_eq_coe, map_baseChange]

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