projective_of_restrictScalars — Mathlib

English

If S is unramified over R and M is R-projective, then M is S-projective after base change.

Русский

Если S неразветвленная над R, а M проектирован над R, то M проектирован над S после базового преобразования.

LaTeX

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

Lean4

/-- If `S` is an unramified `R`-algebra, then `R`-projective implies `S`-projective. -/
theorem projective_of_restrictScalars [Module.Projective R M] : Module.Projective S M :=
  Module.Projective.of_split _ _ (comp_sec R S M)

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