English
If M and N are linearly disjoint and M is flat, then for any R-linearly independent family (n_j) of elements of N, the R-linear map from ι →₀ M to S sending m_i to m_i · n_i has trivial kernel; i.e., ker(mulRightMap M n) = ⊥.
Русский
Если M и N линейно несовместны, и M плоско над R, то для любой R-линейно независимой семьи элементов N ядро соответствующего отображения izquierdo не содержит нетривиальных элементов.
LaTeX
$$ker(\mathrm{mulRightMap}\,M\,n) = \bot$$
Lean4
/-- If `M` and `N` are linearly disjoint, if `M` is a flat `R`-module, then for any family of
`R`-linearly independent elements `{ n_i }` of `N`, they are also `M`-linearly independent,
in the sense that the `R`-linear map from `ι →₀ M` to `S` which maps `{ m_i }`
to the sum of `m_i * n_i` (`Submodule.mulRightMap M n`) has trivial kernel. -/
theorem linearIndependent_right_of_flat (H : M.LinearDisjoint N) [Module.Flat R M] {ι : Type*} {n : ι → N}
(hn : LinearIndependent R n) : LinearMap.ker (mulRightMap M n) = ⊥ :=
by
refine LinearMap.ker_eq_bot_of_injective ?_
classical
simp_rw [mulRightMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe, ← Function.comp_assoc,
EquivLike.injective_comp]
rw [LinearIndependent] at hn
exact H.injective.comp (Module.Flat.lTensor_preserves_injective_linearMap (M := M) _ hn)
