English
If A and B are linearly disjoint and their elements commute, and B is flat over R, then for any R-linearly independent family in A, the corresponding A-valued images commute with B and remain independent after the operation.
Русский
Если A и B линейно несовместны и их элементы коммутируют, и B является плоским над R, тогда любая R-линейно независимая совокупность в A сохраняет независимость под операцией и совместна с B.
LaTeX
$$$H \\text{ LinearDisjoint } B \\Rightarrow [Module.Flat R B] \\Rightarrow (ha) \\to (hc) \\Rightarrow LinearIndependent B (A \\circ a)$$$
Lean4
/-- If `A` and `B` are linearly disjoint, if `A` is a flat `R`-module, then for any family of
`R`-linearly independent elements of `B`, they are also `A`-linearly independent. -/
theorem linearIndependent_right_of_flat (H : A.LinearDisjoint B) [Module.Flat R A] {ι : Type*} {b : ι → B}
(hb : LinearIndependent R b) : LinearIndependent A (B.val ∘ b) :=
by
have h := Submodule.LinearDisjoint.linearIndependent_right_of_flat H hb
rwa [mulRightMap_ker_eq_bot_iff_linearIndependent] at h
