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} [Category.{v, u} C] [Preregular C] [FinitaryExtensive C] {F : Functor ℕᵒᵖ (Sheaf (coherentTopology C) (Type v))} {c : Limits.Cone F} (hc : Limits.IsLimit c) (hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)) [Limits.HasLimitsOfShape ℕᵒᵖ C] (h : ∀ (G : Functor ℕᵒᵖ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (Limits.limit.π G (Opposite.op 0))) : Sheaf.IsLocallySurjective (c.π.app (Opposite.op 0))

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