English
If M and N are linearly disjoint and N is flat, then for LI families { m_i } ⊂ M and { n_j } ⊂ N, the same product-independence holds for mulRightMap.
Русский
Если M и N линейно неразделимы и N плоско над R, то аналогично сохраняется линейная независимость для отображения mulRightMap.
LaTeX
$$LinearIndependent R (i : κ × ι) ↦ (m i.1).1 * (n i.2).1$$
Lean4
/-- If `M` and `N` are linearly disjoint, if `N` 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_right (H : M.LinearDisjoint N) [Module.Flat R N] {κ ι : 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.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
let i2 := LinearMap.rTensor N (Finsupp.linearCombination R m)
let i := mulMap M N ∘ₗ i2 ∘ₗ i1 ∘ₗ i0.toLinearMap
have h1 : Function.Injective i1 := Module.Flat.lTensor_preserves_injective_linearMap _ hn
have h2 : Function.Injective i2 := Module.Flat.rTensor_preserves_injective_linearMap _ hm
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
