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.{u_2, u_1} C] [Precoherent C] [Limits.HasFiniteCoproducts C] : Preregular C

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

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

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