# Documentation

Mathlib.CategoryTheory.Sites.Coherent

# 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: #

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

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.

Instances

The coherent coverage on a precoherent category C.

Instances For

The coherent Grothendieck topology on a precoherent category C.

Instances For
theorem CategoryTheory.isSheaf_coherent (C : Type u_1) [] (P : ) :
∀ (B : C) (α : Type) [inst : ] (X : αC) (π : (a : α) → X a B),
theorem CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily {C : Type u_2} [] {X : C} (S : ) :
(α x Y π, ∀ (a : α), S.arrows (π a)) →

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} [] (W : C) :
CategoryTheory.Presieve.IsSheaf () (CategoryTheory.yoneda.obj W)

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

The coherent topology on a precoherent category is subcanonical.

theorem CategoryTheory.EffectiveEpiFamily.transitive_of_finite {C : Type u_2} [] {X : C} {α : Type} [] {Y : αC} (π : (a : α) → Y a X) (h : ) {β : α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.

theorem CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily {C : Type u_2} [] {X : C} (S : ) :
α x Y π, ∀ (a : α), S.arrows (π a)

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