fromEnd_injective — Mathlib

English

If the family {b_i} spans M, the map fromEnd R b is injective; i.e., distinct endomorphisms act differently on the b-span.

Русский

Если подпространство, порождаемое {b_i}, равно всей M, отображение fromEnd R b инъективно.

LaTeX

$$$\\text{hb: } \\operatorname{span}_R(\\{b_i\\}) = \\top \\quad \\Rightarrow\\quad \\mathrm{fromEnd}(R,b): \\mathrm{End}_R(M) \\to (\\,ι \\to R\\, )^M\\text{ is injective}$$$

Lean4

theorem fromEnd_injective (hb : Submodule.span R (Set.range b) = ⊤) : Function.Injective (PiToModule.fromEnd R b) :=
  by
  intro x y e
  ext m
  obtain ⟨m, rfl⟩ : m ∈ LinearMap.range (Fintype.linearCombination R b) :=
    by
    rw [(Fintype.range_linearCombination R b).trans hb]
    exact Submodule.mem_top
  exact (LinearMap.congr_fun e m :)

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