English
Another presentation of the same principle: if a certain linear map derived from a basis is injective, then M and N are linearly disjoint.
Русский
Еще одна формулировка принципа: если линейное отображение, полученное от базиса, инъективно, то M и N линейно несовместны.
LaTeX
$$M.LinearDisjoint N$$
Lean4
/-- If `{ m_i }` is an `R`-basis of `M`, if `{ n_i }` is an `R`-basis of `N`,
such that the family `{ m_i * n_j }` in `S` is `R`-linearly independent
(in this result it is stated as the relevant `Finsupp.linearCombination` is injective),
then `M` and `N` are linearly disjoint. -/
theorem of_basis_mul' {κ ι : Type*} (m : Basis κ R M) (n : Basis ι R N)
(H : Function.Injective (Finsupp.linearCombination R fun i : κ × ι ↦ (m i.1 * n i.2 : S))) : M.LinearDisjoint N :=
by
let i0 := (finsuppTensorFinsupp' R κ ι).symm
let i1 := TensorProduct.congr m.repr n.repr
let i := mulMap M N ∘ₗ (i0.trans i1.symm).toLinearMap
have : i = Finsupp.linearCombination R fun i : κ × ι ↦ (m i.1 * n i.2 : S) :=
by
ext x
simp [i, i0, i1, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
simp_rw [← this, i, LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.injective_comp] at H
exact ⟨H⟩
