Connections between the regular, extensive and coherent topologies

This file compares the regular, extensive and coherent topologies.

Main results

• instance : Precoherent C given Preregular C and FinitaryPreExtensive C.

• extensive_union_regular_generates_coherent: the union of the regular and extensive coverages generates the coherent topology on C if C is precoherent, preextensive and preregular.

instance CategoryTheory.instPreregularOfPrecoherentOfHasFiniteCoproducts (C : Type u_1) [Category.{v_1, u_1} C] [Precoherent C] [Limits.HasFiniteCoproducts C] : Preregular C

instance CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular (C : Type u_1) [Category.{v_1, u_1} C] [FinitaryPreExtensive C] [Preregular C] : Precoherent C

theorem CategoryTheory.extensive_regular_generate_coherent (C : Type u_1) [Category.{v_1, u_1} C] [Preregular C] [FinitaryPreExtensive C] : (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck = coherentTopology C

The union of the extensive and regular coverages generates the coherent topology on C.