isStableUnderBaseChange — Mathlib

English

Etale maps are stable under base change: the etale property is preserved by base-changing the base ring. This is deduced from isomorphic combination of FormallyUnramified and Smooth stability under base change.

Русский

Отображения etale сохраняются при базисном изменении: свойство Etale сохраняется после базисного изменения кольца.

LaTeX

$$IsStableUnderBaseChange Etale$$

Lean4

theorem isStableUnderBaseChange : IsStableUnderBaseChange Etale :=
  by
  rw [eq_formallyUnramified_and_smooth]
  exact FormallyUnramified.isStableUnderBaseChange.and Smooth.isStableUnderBaseChange

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