of_le_left_of_flat — Mathlib

English

In a flat-left scenario, for any a,b in M ⊓ N that commute, the pair a,b cannot be linearly independent.

Русский

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

LaTeX

$$¬LinearIndepedent_R ![a,b]$$

Lean4

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

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