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

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

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

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