surjective_π_app_zero_of_surjective_map

English

The projection to the 0th component of a limit cone is surjective under the given surjectivity assumptions.

Русский

Проекция на нулевой компонент предельного конуса сюръективна при данных предположениях.

LaTeX

$$$\\text{surjective }(c.\\pi.app\\langle 0\\rangle)$$$

Lean4

/-- Given surjections `⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀`, the projection map `lim Xₙ ⟶ X₀` is surjective.
-/
theorem surjective_π_app_zero_of_surjective_map (hc : IsLimit c)
    (hF : ∀ n, Function.Surjective (F.map (homOfLE (Nat.le_succ n)).op)) : Function.Surjective (c.π.app ⟨0⟩) :=
  by
  let i := hc.conePointUniqueUpToIso (limitConeIsLimit F)
  have : c.π.app ⟨0⟩ = i.hom ≫ (limitCone F).π.app ⟨0⟩ := by simp [i]
  rw [this]
  apply Function.Surjective.comp
  · exact surjective_π_app_zero_of_surjective_map_aux hF
  · rw [← epi_iff_surjective]
    infer_instance

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