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} [Category.{u_2, u_1} C] [FinitaryPreExtensive C] {X : C} (S : Sieve X) : S ∈ (extensiveTopology C) X ↔ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), Nonempty (Limits.IsColimit (Limits.Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)