English
A specialization of the previous ker-equivalence: the equation holds for A,B subalgebras with an appropriate indexing.
Русский
Уточнение предыдущего эквивалента ядра: выражение верно для подалгебр A,B с соответствующей индексацией.
LaTeX
$$$\\ker( Submodule.mulLeftMap (M := toSubmodule A) (toSubmodule B) a ) = \\{0\\} \\iff \\ LinearIndependent B.op (MulOpposite.op \\circ A.val \\circ a)$$$
Lean4
/-- If `A` and `B` are linearly disjoint, if `B` is a flat `R`-module, then for any family of
`R`-linearly independent elements of `A`, they are also `B`-linearly independent
in the opposite ring. -/
theorem linearIndependent_left_op_of_flat (H : A.LinearDisjoint B) [Module.Flat R B] {ι : Type*} {a : ι → A}
(ha : LinearIndependent R a) : LinearIndependent B.op (MulOpposite.op ∘ A.val ∘ a) :=
by
have h := Submodule.LinearDisjoint.linearIndependent_left_of_flat H ha
rwa [mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at h
