flat_of_restrictScalars — Mathlib

English

If S is unramified over R and M is R-flat, then M is S-flat via restriction of scalars and a sec construction providing a retract.

Русский

Если S неразветвленная над R, и M является плоским модулем над R, то M плоский над S при ограничении скаляра и секцией, которая образует retract.

LaTeX

$$$[Module.Flat\\, R\\ M] \\Rightarrow [Module.Flat\\, S\\ M]$$$

Lean4

/-- If `S` is an unramified `R`-algebra, then `R`-flat implies `S`-flat. Iversen I.2.7 -/
theorem flat_of_restrictScalars [Module.Flat R M] : Module.Flat S M :=
  Module.Flat.of_retract _ _ (comp_sec R S M)

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