map_injective_field — Mathlib

English

If f: M → N has a linear retraction g, then the map on exterior algebras is injective.

Русский

Если у отображения f есть линейное разложение g, то отображение на алгебрах внешних степеней инъективно.

LaTeX

$$$ \\text{map\_injective} \\{f : M \\rightarrow N\\} (\\text{hf} : \\exists g, g \\circ f = \\mathrm{id}) : \\operatorname{Injective}(\\operatorname{map} f). $$$

Lean4

/-- An injective morphism of vector spaces induces an injective morphism of exterior algebras. -/
theorem map_injective_field {f : E →ₗ[K] F} (hf : LinearMap.ker f = ⊥) : Function.Injective (map f) :=
  map_injective (LinearMap.exists_leftInverse_of_injective f hf)

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