mulLeftMap_ker_eq_bot_iff_linearIndependent_op

English

For a family a: ι → A, the kernel of Submodule.mulLeftMap equals {0} if and only if the op-twisted family B.op ∘ A.val ∘ a is linearly independent.

Русский

Для семейства a: ι → A ядро Submodule.mulLeftMap равно нулю тогда и только тогда, когда семейство B.op ∘ A.val ∘ a линейно независимо.

LaTeX

$$$\\ker(Submodule.mulLeftMap\\ (M := toSubmodule\\ A)\\ (toSubmodule\\ B)\\ a)=\\{0\\} \\iff \\ LinearIndependent\\ B.op (MulOpposite.op \\circ A.val \\circ a)$$$

Lean4

theorem mulLeftMap_ker_eq_bot_iff_linearIndependent_op {ι : Type*} (a : ι → A) :
    LinearMap.ker (Submodule.mulLeftMap (M := toSubmodule A) (toSubmodule B) a) = ⊥ ↔
      LinearIndependent B.op (MulOpposite.op ∘ A.val ∘ a) :=
  by
  simp_rw [LinearIndependent, LinearMap.ker_eq_bot]
  let i : (ι →₀ B) →ₗ[R] S := Submodule.mulLeftMap (M := toSubmodule A) (toSubmodule B) a
  let j : (ι →₀ B) →ₗ[R] S :=
    (MulOpposite.opLinearEquiv _).symm.toLinearMap ∘ₗ
      (Finsupp.linearCombination B.op (MulOpposite.op ∘ A.val ∘ a)).restrictScalars R ∘ₗ
        (Finsupp.mapRange.linearEquiv (linearEquivOp B)).toLinearMap
  suffices i = j by
    change Function.Injective i ↔ _
    simp_rw [this, j, LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_injective, EquivLike.injective_comp,
      LinearMap.coe_restrictScalars]
  ext
  simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, coe_val,
    Finsupp.mapRange.linearEquiv_toLinearMap, LinearEquiv.coe_coe, MulOpposite.coe_opLinearEquiv_symm,
    LinearMap.coe_restrictScalars, Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single,
    Finsupp.linearCombination_single, MulOpposite.unop_smul, MulOpposite.unop_op, i, j]
  exact Submodule.mulLeftMap_apply_single _ _ _

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