English
Smoothness holds with respect to localization Span Target; i.e., the localization span argument.
Русский
Гладкость относится к локализации, охватывающей целевой объект.
LaTeX
$$$\mathrm{OfLocalizationSpanTarget}(\mathrm{Smooth})$$$
Lean4
theorem ofLocalizationSpanTarget : OfLocalizationSpanTarget Smooth :=
by
introv R hs hf
have : f.FinitePresentation := finitePresentation_ofLocalizationSpanTarget _ s hs fun r ↦ (hf r).finitePresentation
algebraize [f]
refine ⟨?_, ‹_›⟩
rw [← Algebra.smoothLocus_eq_univ_iff, ← Set.univ_subset_iff, ← TopologicalSpace.Opens.coe_top, ←
PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs]
simp only [TopologicalSpace.Opens.coe_iSup, Set.iUnion_subset_iff, Algebra.basicOpen_subset_smoothLocus_iff,
← formallySmooth_algebraMap]
exact fun r hr ↦ (hf ⟨r, hr⟩).1
