map_injective — Mathlib

English

For a linear map f over a field K, ιInv.comp (ExteriorAlgebra.map f).toLinearMap equals f.comp ιInv.

Русский

Для линейного отображения над полем K: ιInv ∘ map f = f ∘ ιInv.

LaTeX

$$$ ιInv \\circ (ExteriorAlgebra.map\\ f).toLinearMap = f \\circ ιInv. $$$

Lean4

/-- A morphism of modules that admits a linear retraction induces an injective morphism of
exterior algebras. -/
theorem map_injective {f : M →ₗ[R] N} (hf : ∃ (g : N →ₗ[R] M), g.comp f = LinearMap.id) : Function.Injective (map f) :=
  let ⟨_, hgf⟩ := hf;
  (leftInverse_map_iff.mpr (DFunLike.congr_fun hgf)).injective

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