of_le_right_of_flat — Mathlib

English

In a flat-right setting, for any a,b in M ∩ N that commute, the pair a,b cannot be linearly independent.

Русский

В случае плоского справа любые элементы a,b из M ∩ N, commuting, не образуют линейно независимую пару.

LaTeX

$$¬LinearIndependent R ![a,b]$$

Lean4

/-- If `M` and `N` are linearly disjoint, if `M` is flat, then for any submodule `N'` of `N`,
`M` and `N'` are also linearly disjoint. -/
theorem of_le_right_of_flat (H : M.LinearDisjoint N) {N' : Submodule R S} (h : N' ≤ N) [Module.Flat R M] :
    M.LinearDisjoint N' := by
  let i := mulMap M N ∘ₗ (inclusion h).lTensor M
  have hi : Function.Injective i :=
    H.injective.comp <| Module.Flat.lTensor_preserves_injective_linearMap _ <| inclusion_injective h
  have : i = mulMap M N' := by ext; simp [i]
  exact ⟨this ▸ hi⟩

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