flat_of_isLocalized_span — Mathlib

English

If R-S-M setup has localization data, then flatness transfers under base change via LocalizedModule.

Русский

Если имеется локализационная структура модуля, то плоскость передается при базовом изменении через LocalizedModule.

LaTeX

$$$\\text{Flat}_R(M) \\Rightarrow \\text{Flat}_{\\mathrm{Localization}(p)}(M)$$$

Lean4

theorem flat_of_isLocalized_span (H : ∀ r : s, Module.Flat R (Mₛ r)) : Module.Flat R M :=
  by
  simp_rw [Flat.iff_lTensor_injectiveₛ] at H ⊢
  simp_rw [← AlgebraTensorModule.coe_lTensor (A := S)]
  refine fun _ _ _ N ↦
    injective_of_isLocalized_span s spn _ (fun r ↦ AlgebraTensorModule.rTensor R _ (g r)) _
      (fun r ↦ AlgebraTensorModule.rTensor R _ (g r)) _ fun r ↦ ?_
  simpa [IsLocalizedModule.map_lTensor] using H r N

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