English
Let M and N be submodules of a ring extension S over R, with M and N linearly disjoint and N flat over R. If a family (m_i) of elements of M is linearly independent over R, then the R-linear map from the free N-module on the index set to S that sends the basis element corresponding to i to m_i · n_i (where n_i ranges over N) has trivial kernel; equivalently ker(mulLeftMap N m) = ⊥.
Русский
Пусть M и N — подмодули кольца S над R, причём M и N линейно независимы в тракте линейной дисъюнктности, а N плоский над R. Если множество элементов m_i ∈ M линейно независимо над R, то соответствующий линейный отображение из свободного модульного над N по индексу i в S, отправляющее базисный элемент на m_i · n_i (где n_i пробегает по N), имеет тривиальный ядро; то есть ker(mulLeftMap N m) = ⊥.
LaTeX
$$$\ker(\mathrm{mulLeftMap}\,N\,m) = \bot$$$
Lean4
/-- If `M` and `N` are linearly disjoint, if `N` is a flat `R`-module, then for any family of
`R`-linearly independent elements `{ m_i }` of `M`, they are also `N`-linearly independent,
in the sense that the `R`-linear map from `ι →₀ N` to `S` which maps `{ n_i }`
to the sum of `m_i * n_i` (`Submodule.mulLeftMap N m`) has trivial kernel. -/
theorem linearIndependent_left_of_flat (H : M.LinearDisjoint N) [Module.Flat R N] {ι : Type*} {m : ι → M}
(hm : LinearIndependent R m) : LinearMap.ker (mulLeftMap N m) = ⊥ :=
by
refine LinearMap.ker_eq_bot_of_injective ?_
classical
simp_rw [mulLeftMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe, ← Function.comp_assoc,
EquivLike.injective_comp]
rw [LinearIndependent] at hm
exact H.injective.comp (Module.Flat.rTensor_preserves_injective_linearMap (M := N) _ hm)
