Description of the covering sieves of the extensive topology

This file characterises the covering sieves of the extensive topology.

Main result

• extensiveTopology.mem_sieves_iff_contains_colimit_cofan: a sieve is a covering sieve for the extensive topology if and only if it contains a finite family of morphisms with fixed target exhibiting the target as a coproduct of the sources.

theorem CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.FinitaryPreExtensive C] {X : C} (S : CategoryTheory.Sieve X) : S ∈ (CategoryTheory.extensiveTopology C) X ↔ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)