localizedModule — Mathlib

English

Flatness is preserved under localization along AtPrime in flat modules.

Русский

Плоскость сохраняется при локализации вдоль AtPrime в плоских модулях.

LaTeX

$$$Flat(Localization.AtPrime p, Localization.AtPrime P)$$$

Lean4

instance localizedModule [Flat R M] (S : Submonoid R) : Flat (Localization S) (LocalizedModule S M) :=
  by
  apply Flat.isBaseChange (R := R) (S := Localization S) (f := LocalizedModule.mkLinearMap S M)
  rw [← isLocalizedModule_iff_isBaseChange S]
  exact localizedModuleIsLocalizedModule S

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