CategoryTheory.extensive_regular_generate_coherent

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

This theorem states that for any category 'C' which is pre-regular and finitarily pre-extensive, the Grothendieck topology generated by the union of the extensive coverage and the regular coverage of 'C' is equal to the coherent topology on 'C'. In other words, the coherent topology on a category can be obtained by unifying the extensive and regular coverages and then converting this unified coverage into the Grothendieck topology.

More concisely: In a pre-regular and finitarily pre-extensive category 'C', the coherent topology is equal to the Grothendieck topology generated by the union of the extensive and regular coverages.