English
In a sequential diagram of a concrete category where the forgetful functor preserves sequential limits, if each map F.map(homOfLE(n)) is surjective, then the projection at zero is surjective.
Русский
В последовательной диаграмме конкретной категории, где забывающий функтор сохраняет предельные пределы, если каждая карта F.map(homOfLE(n)) сюръективна, то проекция в ноль сюръективна.
LaTeX
$$$\\forall n,\\; \\mathrm{Surjective}\\big(F.map(\\mathrm{homOfLE}(\\mathrm{Nat}.\\mathrm{le\\_succ}\\, n)).op\\big)\\Rightarrow \\mathrm{Surjective}(\\,c.\\pi. app\\\\langle 0\\\\rangle) $$$
Lean4
/-- Given surjections `⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀` in a concrete category whose forgetful functor
preserves sequential limits, the projection map `lim Xₙ ⟶ X₀` is surjective.
-/
theorem surjective_π_app_zero_of_surjective_map {C : Type u} [Category.{v} C] {FC : C → C → Type*} {CC : C → Type v}
[∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory.{v} C FC] [PreservesLimitsOfShape ℕᵒᵖ (forget C)]
{F : ℕᵒᵖ ⥤ C} {c : Cone F} (hc : IsLimit c) (hF : ∀ n, Function.Surjective (F.map (homOfLE (Nat.le_succ n)).op)) :
Function.Surjective (c.π.app ⟨0⟩) :=
Types.surjective_π_app_zero_of_surjective_map (isLimitOfPreserves (forget C) hc) hF
