of_le_of_flat_right — Mathlib

English

If M and N are linearly disjoint and at least one of them is flat, then the rank of their intersection M ⊓ N is at most 1 when any pair of elements commute.

Русский

Если M и N линейно раздельны и хотя бы один из них плоский, то ранг пересечения M ∩ N не более 1 при условии коммутирования пар элементов.

LaTeX

$$Module.rank R ↥(M ⊓ N) ≤ 1$$

Lean4

/-- If `M` and `N` are linearly disjoint, `M'` and `N'` are submodules of `M` and `N`,
respectively, such that `N` and `M'` are flat, then `M'` and `N'` are also linearly disjoint. -/
theorem of_le_of_flat_right (H : M.LinearDisjoint N) {M' N' : Submodule R S} (hm : M' ≤ M) (hn : N' ≤ N)
    [Module.Flat R N] [Module.Flat R M'] : M'.LinearDisjoint N' :=
  (H.of_le_left_of_flat hm).of_le_right_of_flat hn

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