ofLocalizationPrime — Mathlib

English

Localization at a prime preserves flatness: a flat map remains flat after localizing at a prime ideal.

Русский

Локализация поprime сохраняет плоскость: плоский переход сохраняется после локализации по prime-идеалу.

LaTeX

$$$$\text{OfLocalizationPrime}(Flat).$$$$

Lean4

theorem ofLocalizationPrime : OfLocalizationPrime Flat :=
  by
  introv R h
  algebraize_only  [f]
  rw [RingHom.Flat]
  apply Module.flat_of_isLocalized_maximal S S (fun P ↦ Localization.AtPrime P) (fun P ↦ Algebra.linearMap S _)
  intro P _
  algebraize_only  [Localization.localRingHom (Ideal.comap f P) P f rfl]
  have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
    .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
  replace h : Module.Flat (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) := h ..
  exact Module.Flat.trans R (Localization.AtPrime <| Ideal.comap f P) (Localization.AtPrime P)

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