English
The property IsStableUnderBaseChange and related locality results show that FormallyUnramified is a local property on the base; it can be checked after suitable localizations.
Русский
Свойство FormallyUnramified локально по основанию; проверяется после соответствующих локализаций.
LaTeX
$$$\\text{IsStableUnderBaseChange(FormallyUnramified)}\\ \\text{локально по основанию}$$$
Lean4
theorem propertyIsLocal : PropertyIsLocal FormallyUnramified :=
by
constructor
· intro R S _ _ f r R' S' _ _ _ _ _ _ H
algebraize [f, (algebraMap S S').comp f, IsLocalization.Away.map R' S' f r]
have := Algebra.FormallyUnramified.of_isLocalization (Rₘ := S') (.powers (f r))
have := Algebra.FormallyUnramified.comp R S S'
have H : Submonoid.powers r ≤ (Submonoid.powers (f r)).comap f := by rintro x ⟨n, rfl⟩; exact ⟨n, by simp⟩
have : IsScalarTower R R' S' := .of_algebraMap_eq' (IsLocalization.map_comp H).symm
exact Algebra.FormallyUnramified.of_comp R R' S'
· exact ofLocalizationSpanTarget
·
exact
ofLocalizationSpanTarget.ofLocalizationSpan
(stableUnderComposition.stableUnderCompositionWithLocalizationAway holdsForLocalizationAway).1
· exact (stableUnderComposition.stableUnderCompositionWithLocalizationAway holdsForLocalizationAway).2
