The Regular and Extensive Coverages

This file defines two coverages on a category C.

The first one is called the regular coverage and for that to exist, the category C must satisfy a condition called Preregular C. This means that effective epimorphisms can be "pulled back". The covering sieves of this coverage are generated by presieves consisting of a single effective epimorphism.

The second one is called the extensive coverage and for that to exist, the category C must satisfy a condition called FinitaryPreExtensive C. This means C has finite coproducts and that those are preserved by pullbacks. The covering sieves of this coverage are generated by presieves consisting finitely many arrows that together induce an isomorphism from the coproduct to the target. This condition is weaker than FinitaryExtensive, where in addition finite coproducts are disjoint.

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.

• isSheaf_iff_equalizerCondition: In a preregular category with pullbacks, the sheaves for the regular topology are precisely the presheaves satisfying an equaliser condition with respect to effective epimorphisms.

• isSheaf_of_projective: In a preregular category in which every object is projective, every presheaf is a sheaf for the regular topology.

• isSheaf_iff_preservesFiniteProducts: In a finitary extensive category, the sheaves for the extensive topology are precisely those preserving finite products.

class CategoryTheory.Preregular (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

The condition Preregular C is property that effective epis can be "pulled back" along any morphism. This is satisfied e.g. by categories that have pullbacks that preserve effective epimorphisms (like Profinite and CompHaus), and categories where every object is projective (like Stonean).

• exists_fac : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ Y) [inst : CategoryTheory.EffectiveEpi g], ∃ (W : C) (h : W ⟶ X) (_ : CategoryTheory.EffectiveEpi h) (i : W ⟶ Z), CategoryTheory.CategoryStruct.comp i g = CategoryTheory.CategoryStruct.comp h f

  For X, Y, Z, f, g like in the diagram, where g is an effective epi, there exists an object W, an effective epi h : W ⟶ X and a morphism i : W ⟶ Z making the diagram commute.

  W --i-→ Z
  |       |
  h       g
  ↓       ↓
  X --f-→ Y
  

instance CategoryTheory.instPreregular (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Precoherent C] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Preregular C

Equations

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

def CategoryTheory.regularCoverage (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preregular C] : CategoryTheory.Coverage C

The regular coverage on a regular category C.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.extensiveCoverage (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] : CategoryTheory.Coverage C

The extensive coverage on an extensive category C

TODO: use general colimit API instead of IsIso (Sigma.desc π)

Equations

• One or more equations did not get rendered due to their size.

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

instance CategoryTheory.instPrecoherent (C : Type u) [CategoryTheory.Category.{v, u} 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) [CategoryTheory.Category.{v, u} 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.

class CategoryTheory.Presieve.regular {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.Presieve X) : Prop

A presieve is regular if it consists of a single effective epimorphism.

• single_epi : ∃ (Y : C) (f : Y ⟶ X), (R = CategoryTheory.Presieve.ofArrows (fun (x : Unit) => Y) fun (x : Unit) => f) ∧ CategoryTheory.EffectiveEpi f

  R consists of a single epimorphism.

def CategoryTheory.regularCoverage.MapToEqualizer {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) {W : C} {X : C} {B : C} (f : X ⟶ B) (g₁ : W ⟶ X) (g₂ : W ⟶ X) (w : CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f) : P.obj (Opposite.op B) → ↑{x : P.obj (Opposite.op X) | P.map g₁.op x = P.map g₂.op x}

The map to the explicit equalizer used in the sheaf condition.

Equations

• CategoryTheory.regularCoverage.MapToEqualizer P f g₁ g₂ w t = { val := P.map f.op t, property := (_ : P.map g₁.op (P.map f.op t) = P.map g₂.op (P.map f.op t)) }

def CategoryTheory.regularCoverage.EqualizerCondition {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : Prop

The sheaf condition with respect to regular presieves, given the existence of the relavant pullback.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.regularCoverage.EqualizerCondition.isSheafFor {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {S : CategoryTheory.Presieve B} [CategoryTheory.Presieve.regular S] [CategoryTheory.Presieve.hasPullbacks S] {F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} (hF : CategoryTheory.regularCoverage.EqualizerCondition F) : CategoryTheory.Presieve.IsSheafFor F S

theorem CategoryTheory.regularCoverage.equalizerCondition_of_regular {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} (hSF : ∀ {B : C} (S : CategoryTheory.Presieve B) [inst : CategoryTheory.Presieve.regular S] [inst : CategoryTheory.Presieve.hasPullbacks S], CategoryTheory.Presieve.IsSheafFor F S) : CategoryTheory.regularCoverage.EqualizerCondition F

theorem CategoryTheory.regularCoverage.isSheafFor_regular_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Presieve X) [CategoryTheory.Presieve.regular S] [CategoryTheory.Projective X] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : CategoryTheory.Presieve.IsSheafFor F S

theorem CategoryTheory.regularCoverage.EqualizerCondition.isSheaf_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) [∀ ⦃X Y : C⦄ (π : X ⟶ Y) [inst : CategoryTheory.EffectiveEpi π], CategoryTheory.Limits.HasPullback π π] [CategoryTheory.Preregular C] : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.regularCoverage C)) F ↔ CategoryTheory.regularCoverage.EqualizerCondition F

theorem CategoryTheory.regularCoverage.isSheaf_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) [CategoryTheory.Preregular C] [∀ (X : C), CategoryTheory.Projective X] : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.regularCoverage C)) F

theorem CategoryTheory.regularCoverage.isSheaf_yoneda_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preregular C] (W : C) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.regularCoverage C)) (CategoryTheory.yoneda.obj W)

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

theorem CategoryTheory.regularCoverage.subcanonical {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preregular C] : CategoryTheory.Sheaf.Subcanonical (CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.regularCoverage C))

The regular topology on any preregular category is subcanonical.

class CategoryTheory.Presieve.extensive {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.Presieve X) : Prop

A presieve is extensive if it is finite and its arrows induce an isomorphism from the coproduct to the target.

• arrows_nonempty_isColimit : ∃ (α : Type) (x : Fintype α) (Z : α → C) (π : (a : α) → Z a ⟶ X), R = CategoryTheory.Presieve.ofArrows Z π ∧ Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X π))

  R consists of a finite collection of arrows that together induce an isomorphism from the coproduct of their sources.

instance CategoryTheory.instHasPullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {X : C} (S : CategoryTheory.Presieve X) [CategoryTheory.Presieve.extensive S] : CategoryTheory.Presieve.hasPullbacks S

Equations

• (_ : CategoryTheory.Presieve.hasPullbacks S) = (_ : CategoryTheory.Presieve.hasPullbacks S)

instance CategoryTheory.instPreservesLimitTypeTypesDiscreteDiscreteCategoryFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type} [Fintype α] {Z : α → C} {F : CategoryTheory.Functor C (Type w)} [CategoryTheory.Limits.PreservesFiniteProducts F] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun (a : α) => Z a) F

Equations

• CategoryTheory.instPreservesLimitTypeTypesDiscreteDiscreteCategoryFunctor = CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit

theorem CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {X : C} (S : CategoryTheory.Presieve X) [CategoryTheory.Presieve.extensive S] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) [CategoryTheory.Limits.PreservesFiniteProducts F] : CategoryTheory.Presieve.IsSheafFor F S

A finite product preserving presheaf is a sheaf for the extensive topology on a category which is FinitaryPreExtensive.

instance CategoryTheory.instExtensiveSigmaObjHasColimitOfHasColimitsOfShapeDiscreteDiscreteCategoryHasColimitsOfShape_discreteHasFiniteCoproductsOf_fintypeFunctorOfArrowsι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {α : Type} [Fintype α] (Z : α → C) : CategoryTheory.Presieve.extensive (CategoryTheory.Presieve.ofArrows Z fun (i : α) => CategoryTheory.Limits.Sigma.ι Z i)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.isSheaf_iff_preservesFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] [CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.extensiveCoverage C)) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F)

A presheaf on a category which is FinitaryExtensive is a sheaf iff it preserves finite products.