instIsStableUnderBaseChangeScheme

English

Formally unramified morphisms are stable under base change: if f: X → Y is formally unramified and h: Y' → Y is any morphism, then the base-changed morphism X' → Y' is formally unramified.

Русский

Формально неразрывные морфизмы устойчивы к базовым изменениям: если f: X → Y формально неразрывна и есть произвольный морфизм h: Y' → Y, то основанная на базисе морфизма X' → Y' формально неразрывна.

LaTeX

$$$\\forall h: Y' \\to Y,\\ \\text{FormallyUnramified}(X' \\to Y')$ where $X' = X \\times_Y Y'.$$$

Lean4

instance : MorphismProperty.IsStableUnderBaseChange @FormallyUnramified :=
  HasRingHomProperty.isStableUnderBaseChange RingHom.FormallyUnramified.isStableUnderBaseChange

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