Documentation

Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Description of the covering sieves of the coherent topology #

This file characterises the covering sieves of the coherent topology.

Main result #

theorem CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] {X : C} (S : CategoryTheory.Sieve X) :
(∃ (α : Type) (_ : Finite α) (Y : αC) (π : (a : α) → Y a X), CategoryTheory.EffectiveEpiFamily Y π ∀ (a : α), S.arrows (π a))S (CategoryTheory.coherentTopology C).sieves 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.EffectiveEpiFamily.transitive_of_finite {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] {X : C} {α : Type} [Finite α] {Y : αC} (π : (a : α) → Y a X) (h : CategoryTheory.EffectiveEpiFamily Y π) {β : αType} [∀ (a : α), Finite (β 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 : (a : α) × β a) => Y_n c.fst c.snd) fun (c : (a : α) × β a) => 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.

instance CategoryTheory.precoherentEffectiveEpiFamilyCompEffectiveEpis {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] {X : C} {α : Type} [Finite α] {Y : αC} {Z : αC} (π : (a : α) → Y a X) [CategoryTheory.EffectiveEpiFamily Y π] (f : (a : α) → Z a Y a) [h : ∀ (a : α), CategoryTheory.EffectiveEpi (f a)] :
Equations
  • =
theorem CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] {X : C} (S : CategoryTheory.Sieve X) :
S (CategoryTheory.coherentTopology C).sieves X ∃ (α : Type) (_ : Finite α) (Y : αC) (π : (a : α) → Y a X), CategoryTheory.EffectiveEpiFamily Y π ∀ (a : α), S.arrows (π a)

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