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:

• [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.1, Example 2.1.12.
• nLab, Coherent Coverage

class CategoryTheory.Precoherent (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : Prop

• pullback : ∀ {B₁ B₂ : C} (f : B₂ ⟶ B₁) (α : Type) [inst : Fintype α] (X₁ : α → C) (π₁ : (a : α) → X₁ a ⟶ B₁), CategoryTheory.EffectiveEpiFamily X₁ π₁ → ∃ β x X₂ π₂, CategoryTheory.EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), CategoryTheory.CategoryStruct.comp (ι b) (π₁ (i b)) = CategoryTheory.CategoryStruct.comp (π₂ b) f

  Given an effective epi family π₁ over B₁ and a morphism f : B₂ ⟶ B₁, there exists an effective epi family π₂ over B₂, such that π₂ factors through π₁.

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

def CategoryTheory.coherentCoverage (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] : CategoryTheory.Coverage C

The coherent coverage on a precoherent category C.

def CategoryTheory.coherentTopology (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] : CategoryTheory.GrothendieckTopology C

The coherent Grothendieck topology on a precoherent category C.

theorem CategoryTheory.isSheaf_coherent (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) P ↔ ∀ (B : C) (α : Type) [inst : Fintype α] (X : α → C) (π : (a : α) → X a ⟶ B), CategoryTheory.EffectiveEpiFamily X π → CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π)

theorem CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Precoherent C] {X : C} (S : CategoryTheory.Sieve X) : (∃ α x Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) → S ∈ CategoryTheory.GrothendieckTopology.sieves (CategoryTheory.coherentTopology C) X

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.

theorem CategoryTheory.coherentTopology.isSheaf_yoneda_obj {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Precoherent C] (W : C) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) (CategoryTheory.yoneda.obj W)

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

theorem CategoryTheory.coherentTopology.isSubcanonical {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Precoherent C] : CategoryTheory.Sheaf.Subcanonical (CategoryTheory.coherentTopology C)

The coherent topology on a precoherent category is subcanonical.

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 : α) → β a → C} (π_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.

theorem CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Precoherent C] {X : C} (S : CategoryTheory.Sieve X) : S ∈ CategoryTheory.GrothendieckTopology.sieves (CategoryTheory.coherentTopology C) X ↔ ∃ α x Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

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