English
If M and N are linearly disjoint and M is flat, then for any LI families { m_i } ⊂ M and { n_j } ⊂ N, the family { m_i · n_j } in S is R-linearly independent.
Русский
Если M и N линейно несовместны и M плоско над R, то любая пара линейно независимых множеств { m_i }⊂M и { n_j }⊂N образует в S линейно независимую семью { m_i · n_j }.
LaTeX
$$LinearIndependent R (λ i, λ j. m i.1 * n j.2) = $$
Lean4
/-- If `M` and `N` are linearly disjoint, if `M` is flat, then for any family of
`R`-linearly independent elements `{ m_i }` of `M`, and any family of
`R`-linearly independent elements `{ n_j }` of `N`, the family `{ m_i * n_j }` in `S` is
also `R`-linearly independent. -/
theorem linearIndependent_mul_of_flat_left (H : M.LinearDisjoint N) [Module.Flat R M] {κ ι : Type*} {m : κ → M}
{n : ι → N} (hm : LinearIndependent R m) (hn : LinearIndependent R n) :
LinearIndependent R fun (i : κ × ι) ↦ (m i.1).1 * (n i.2).1 :=
by
rw [LinearIndependent] at hm hn ⊢
let i0 := (finsuppTensorFinsupp' R κ ι).symm
let i1 := LinearMap.rTensor (ι →₀ R) (Finsupp.linearCombination R m)
let i2 := LinearMap.lTensor M (Finsupp.linearCombination R n)
let i := mulMap M N ∘ₗ i2 ∘ₗ i1 ∘ₗ i0.toLinearMap
have h1 : Function.Injective i1 := Module.Flat.rTensor_preserves_injective_linearMap _ hm
have h2 : Function.Injective i2 := Module.Flat.lTensor_preserves_injective_linearMap _ hn
have h : Function.Injective i := H.injective.comp h2 |>.comp h1 |>.comp i0.injective
have : i = Finsupp.linearCombination R fun i ↦ (m i.1).1 * (n i.2).1 :=
by
ext x
simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
rwa [this] at h
