English
A localization-span property asserts that FormallyUnramified can be checked over a target covering by localizations; if each localization in a cover satisfies the property and a compatibility condition holds, then the original morphism is formally unramified.
Русский
Свойство локализации по покрытию признаков: проверка FormallyUnramified на локализациях покрытия даёт формально немрамированное для исходного гомоморфизма.
LaTeX
$$$\\text{OfLocalizationSpanTarget}(\\mathrm{FrmUnramified})$$$
Lean4
theorem ofLocalizationSpanTarget : OfLocalizationSpanTarget FormallyUnramified :=
by
intro R S _ _ f s hs H
algebraize [f]
rw [FormallyUnramified, ← Algebra.unramifiedLocus_eq_univ_iff, Set.eq_univ_iff_forall]
intro x
obtain ⟨r, hr, hrx⟩ : ∃ r ∈ s, x ∈ PrimeSpectrum.basicOpen r := by
simpa using (PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs).ge (TopologicalSpace.Opens.mem_top x)
refine Algebra.basicOpen_subset_unramifiedLocus_iff.mpr ?_ hrx
convert H ⟨r, hr⟩
dsimp
rw [← algebraMap_toAlgebra f, ← IsScalarTower.algebraMap_eq, formallyUnramified_algebraMap]
