isBaseChange — Mathlib

English

If N has flat structure as R-module and h is an IsBaseChange data, then N is flat over S.

Русский

Если N как R-модуль плосок и существует структура IsBaseChange, то N плосок над S.

LaTeX

$$$Flat_S(N) \\leftarrow IsBaseChange(S,f) \\Rightarrow Flat_S N$$$

Lean4

/-- A base change of a flat module is flat. -/
theorem isBaseChange [Flat R M] (N : Type t) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N]
    {f : M →ₗ[R] N} (h : IsBaseChange S f) : Flat S N :=
  of_linearEquiv (IsBaseChange.equiv h).symm

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