Limits of epimorphisms in coherent topoi

This file proves that a sequential limit of epimorphisms is epimorphic in the category of sheaves for the coherent topology on a preregular finitary extensive category where sequential limits of effective epimorphisms are effective epimorphisms.

In other words, given epimorphisms of sheaves

⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀,

the projection map lim Xₙ ⟶ X₀ is an epimorphism (see coherentTopology.epi_π_app_zero_of_epi).

This is deduced from the corresponding statement about locally surjective morphisms of sheaves (see coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map).

theorem CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (hF : ∀ (n : ℕ), CategoryTheory.Sheaf.IsLocallySurjective (F.map (CategoryTheory.homOfLE ⋯).op)) [CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C] (h : ∀ (G : CategoryTheory.Functor ℕᵒᵖ C), (∀ (n : ℕ), CategoryTheory.EffectiveEpi (G.map (CategoryTheory.homOfLE ⋯).op)) → CategoryTheory.EffectiveEpi (CategoryTheory.Limits.limit.π G (Opposite.op 0))) : CategoryTheory.Sheaf.IsLocallySurjective (c.π.app (Opposite.op 0))

theorem CategoryTheory.coherentTopology.epi_π_app_zero_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C] (h : ∀ (G : CategoryTheory.Functor ℕᵒᵖ C), (∀ (n : ℕ), CategoryTheory.EffectiveEpi (G.map (CategoryTheory.homOfLE ⋯).op)) → CategoryTheory.EffectiveEpi (CategoryTheory.Limits.limit.π G (Opposite.op 0))) [CategoryTheory.HasSheafify (CategoryTheory.coherentTopology C) (Type v)] [CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))] [(CategoryTheory.coherentTopology C).WEqualsLocallyBijective (Type v)] {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (hF : ∀ (n : ℕ), CategoryTheory.Epi (F.map (CategoryTheory.homOfLE ⋯).op)) : CategoryTheory.Epi (c.π.app (Opposite.op 0))