instLocallyOfFinitePresentationOfIsSmooth

English

Smooth morphisms are locally of finite presentation.

Русский

Гладкие морфизмы локально имеют конечную презентацию.

LaTeX

$$IsSmooth f ⇒ LocallyOfFinitePresentation f$$

Lean4

/-- Smooth morphisms are locally of finite presentation. -/
instance (priority := 100) [hf : IsSmooth f] : LocallyOfFinitePresentation f :=
  by
  rw [HasRingHomProperty.eq_affineLocally @LocallyOfFinitePresentation]
  rw [HasRingHomProperty.eq_affineLocally @IsSmooth] at hf
  refine affineLocally_le (fun hf ↦ ?_) f hf
  apply RingHom.locally_of_locally (Q := RingHom.FinitePresentation)at hf
  ·
    rwa [RingHom.locally_iff_of_localizationSpanTarget finitePresentation_respectsIso
        finitePresentation_ofLocalizationSpanTarget] at hf
  · introv hf
    algebraize [f]
      -- TODO: why is `algebraize` not generating the following instance?

    haveI : Algebra.IsStandardSmooth R S := hf
    exact this.finitePresentation

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