proj_surjective — Mathlib

English

Let (φ_i) be a family of R-modules indexed by ι. For each i, the projection map proj_i from the product ∏_{j∈ι} φ_j onto φ_i is surjective.

Русский

Пусть (φ_i) — семейство модулей над кольцом R, индексируемое ι. Для каждого i проекция proj_i: ∏_{j∈ι} φ_j → φ_i является сюръективной.

LaTeX

$$$\\forall i,\\; \\operatorname{Surjective}(\\mathrm{proj}_i : \\prod_{j\\in \\iota} \\phi_j \\to \\phi_i).$$$

Lean4

theorem proj_surjective (i : ι) : Surjective (proj i : ((i : ι) → φ i) →ₗ[R] φ i) :=
  surjective_eval i

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