isStableUnderBaseChange — Mathlib

English

The property of being formally unramified is stable under base change: if f: R → S has the property, then for any base change R' ← R, S' with appropriate algebra structures, the induced map R' → S' also has the property.

Русский

Свойство формально немрамированного гомоморфизма стабильно при базовом изменении: если f:R→S имеет свойство, то при базовом измененииR'←R, S' образуется соответствующий гомоморфизм R'→S', сохраняющий это свойство.

LaTeX

$$$\\mathrm{IsStableUnderBaseChange}(\\mathrm{FrmUnramified})$$$

Lean4

theorem isStableUnderBaseChange : IsStableUnderBaseChange FormallyUnramified :=
  by
  refine .mk respectsIso ?_
  introv H
  rw [formallyUnramified_algebraMap] at H ⊢
  infer_instance

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