linearIndependent_left_of_flat_of_commute

English

For x ∈ A, the i-th coefficient under basisLeft_repr maps to the corresponding coefficient under b's repr via algebra maps.

Русский

Для x ∈ A, i-й коэффициент при basisLeft_repr сопоставляется соответствующим коэффициентом через отображения алгебр.

LaTeX

$$$\\mathrm{basisOfBasisLeft\\_repr\\_apply} \\;: \\mathrm{repr}_{B} (x,i) \\to \\mathrm{repr}_{R} (x,i)$$$

Lean4

/-- If `A` and `B` are linearly disjoint and their elements commute, if `B` is a flat `R`-module,
then for any family of `R`-linearly independent elements of `A`,
they are also `B`-linearly independent. -/
theorem linearIndependent_left_of_flat_of_commute (H : A.LinearDisjoint B) [Module.Flat R B] {ι : Type*} {a : ι → A}
    (ha : LinearIndependent R a) (hc : ∀ (a : A) (b : B), Commute a.1 b.1) : LinearIndependent B (A.val ∘ a) :=
  (H.symm_of_commute hc).linearIndependent_right_of_flat ha

Похожие утверждения