English
For a flat-left setting, any pair a,b in M ⊓ N that commute cannot be linearly independent.
Русский
В случае плоской левой стороны любой пара a,b в M ∩ N, которые commute, не линейно независимы.
LaTeX
$$¬LinearIndependent R ![a, b]$$
Lean4
/-- If `M` and `N` are linearly disjoint, if `N` is flat, then any two commutative
elements of `↥(M ⊓ N)` are not `R`-linearly independent (namely, their span is not `R ^ 2`). -/
theorem not_linearIndependent_pair_of_commute_of_flat_right [Module.Flat R N] (a b : ↥(M ⊓ N)) (hc : Commute a.1 b.1) :
¬LinearIndependent R ![a, b] := fun h ↦
by
let m : Fin 2 → M := (inclusion inf_le_left) ∘ ![a, b]
have hm : LinearIndependent R m :=
h.map' _
(ker_inclusion _ _ _)
-- need this instance otherwise it only has semigroup structure
letI : AddCommGroup (Fin 2 →₀ N) := Finsupp.instAddCommGroup
let n : Fin 2 →₀ N := .single 0 ⟨b.1, b.2.2⟩ - .single 1 ⟨a.1, a.2.2⟩
have hn : mulLeftMap N m n = 0 := by simp [m, n, show _ * _ = _ * _ from hc]
rw [← LinearMap.mem_ker, H.linearIndependent_left_of_flat hm, mem_bot] at hn
simp only [Fin.isValue, sub_eq_zero, Finsupp.single_eq_single_iff, zero_ne_one, Subtype.mk.injEq, SetLike.coe_eq_coe,
false_and, false_or, n] at hn
repeat rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hn
exact h.ne_zero 0 hn.2
