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

Equations

• (_ : CategoryTheory.Preregular C) = (_ : CategoryTheory.Preregular C)

theorem CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.FinitaryPreExtensive C] {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) : CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π) ↔ CategoryTheory.EffectiveEpiFamily X π

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

Equations

• (_ : CategoryTheory.Precoherent 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.