surjective_piEquiv_apply_iff — Mathlib

English

For any v, piEquiv is surjective if and only if the span of the range of v is the top submodule.

Русский

Для любого v условие: piEquiv является сюръективным эквивалентно тому, что порождение диапазона v заполняет всю модульную оболочку.

LaTeX

$$$\text{Surjective}(\piEquiv\ ι\ R\ M\ v) \iff \operatorname{span}_R(\operatorname{range}(v)) = \top$$$

Lean4

@[simp]
theorem surjective_piEquiv_apply_iff (v : ι → M) : Surjective (piEquiv ι R M v) ↔ span R (range v) = ⊤ := by
  rw [← LinearMap.range_eq_top, range_piEquiv]

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