English
If M and N are linearly disjoint and M is flat, and any two commuting elements in M ∩ N exist, then rank of the intersection is ≤ 1.
Русский
Если M и N линейно раздельны и M плоско, и существуют любые две коммутирующие элементы в M ∩ N, то ранг пересечения ≤ 1.
LaTeX
$$Module.rank R ↥(M ⊓ N) ≤ 1$$
Lean4
/-- If `M` and `N` are linearly disjoint, if `M` 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_left [Module.Flat R M] (a b : ↥(M ⊓ N)) (hc : Commute a.1 b.1) :
¬LinearIndependent R ![a, b] := fun h ↦
by
let n : Fin 2 → N := (inclusion inf_le_right) ∘ ![a, b]
have hn : LinearIndependent R n :=
h.map' _
(ker_inclusion _ _ _)
-- need this instance otherwise it only has semigroup structure
letI : AddCommGroup (Fin 2 →₀ M) := Finsupp.instAddCommGroup
let m : Fin 2 →₀ M := .single 0 ⟨b.1, b.2.1⟩ - .single 1 ⟨a.1, a.2.1⟩
have hm : mulRightMap M n m = 0 := by simp [m, n, show _ * _ = _ * _ from hc]
rw [← LinearMap.mem_ker, H.linearIndependent_right_of_flat hn, mem_bot] at hm
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, m] at hm
repeat rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hm
exact h.ne_zero 0 hm.2
