English
If M and itself are linearly disjoint and M is flat, then any two commuting elements in M are constrained to have rank ≤ 1.
Русский
Если M линейно раздельно с самим M и M плосок, то любые две коммутирующие элементы в M образуют систему ранга ≤ 1.
LaTeX
$$Module.rank R M ≤ 1$$
Lean4
/-- If `M` and `N` are linearly disjoint, if one of `M` and `N` is flat,
if any two elements of `↥(M ⊓ N)` are commutative, then the rank of `↥(M ⊓ N)` is at most one. -/
theorem rank_inf_le_one_of_commute_of_flat (hf : Module.Flat R M ∨ Module.Flat R N)
(hc : ∀ (m n : ↥(M ⊓ N)), Commute m.1 n.1) : Module.rank R ↥(M ⊓ N) ≤ 1 :=
by
nontriviality R
refine _root_.rank_le fun s h ↦ ?_
by_contra hs
rw [not_le, ← Fintype.card_coe, Fintype.one_lt_card_iff_nontrivial] at hs
obtain ⟨a, b, hab⟩ := hs.exists_pair_ne
refine H.not_linearIndependent_pair_of_commute_of_flat hf a.1 b.1 (hc a.1 b.1) ?_
have :=
h.comp ![a, b] fun i j hij ↦ by
fin_cases i <;> fin_cases j
· rfl
· simp [hab] at hij
· simp [hab.symm] at hij
· rfl
convert this
ext i
fin_cases i <;> simp
