The Coherent Grothendieck Topology #

This file defines the coherent Grothendieck topology (and coverage) on a category C. The category C must satisfy a Precoherent C condition, which is essentially the minimal requirement for the coherent coverage to exist. Given such a category, the coherent coverage is coherentCoverage C and the corresponding Grothendieck topology is coherentTopology C.

In isSheaf_coherent, we characterize the sheaf condition for presheaves of types for the coherent Grothendieck topology in terms of finite effective epimorphic families.

References: #

The condition Precoherent C is essentially the minimal condition required to define the coherent coverage on C.


    The coherent coverage on a precoherent category C.

    Instances For

      The coherent Grothendieck topology on a precoherent category C.

      Instances For

        For a precoherent category, any sieve that contains an EffectiveEpiFamily is a sieve of the coherent topology. Note: This is one direction of mem_sieves_iff_hasEffectiveEpiFamily, but is needed for the proof.

        Every Yoneda-presheaf is a sheaf for the coherent topology.

        theorem CategoryTheory.EffectiveEpiFamily.transitive_of_finite {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Precoherent C] {X : C} {α : Type} [Fintype α] {Y : αC} (π : (a : α) → Y a X) (h : CategoryTheory.EffectiveEpiFamily Y π) {β : αType} [(a : α) → Fintype (β a)] {Y_n : (a : α) → β aC} (π_n : (a : α) → (b : β a) → Y_n a b Y a) (H : ∀ (a : α), CategoryTheory.EffectiveEpiFamily (Y_n a) (π_n a)) :
        CategoryTheory.EffectiveEpiFamily (fun c => Y_n c.fst c.snd) fun c => CategoryTheory.CategoryStruct.comp (π_n c.fst c.snd) (π c.fst)

        Effective epi families in a precoherent category are transitive, in the sense that an EffectiveEpiFamily and an EffectiveEpiFamily over each member, the composition is an EffectiveEpiFamily. Note: The finiteness condition is an artifact of the proof and is probably unnecessary.

        A sieve belongs to the coherent topology if and only if it contains a finite EffectiveEpiFamily.