map_surjective_iff — Mathlib

English

A linear map f induces a surjective map of exterior algebras if and only if f is surjective.

Русский

Линейное отображение f порождает сюръективное отображение алгебр внешних степеней тогда и только тогда, когда f сюръективно.

LaTeX

$$$ \\operatorname{Surjective}(\\operatorname{map} f) \\iff \\operatorname{Surjective}(f). $$$

Lean4

/-- A morphism of modules is surjective if and only the morphism of exterior algebras that it
induces is surjective. -/
@[simp]
theorem map_surjective_iff {f : M →ₗ[R] N} : Function.Surjective (map f) ↔ Function.Surjective f :=
  by
  refine ⟨fun h y ↦ ?_, fun h ↦ CliffordAlgebra.map_surjective _ h⟩
  obtain ⟨x, hx⟩ := h (ι R y)
  existsi ιInv x
  rw [← LinearMap.comp_apply, ← ιInv_comp_map, LinearMap.comp_apply]
  erw [hx, ExteriorAlgebra.ι_leftInverse]

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