Sheaves for the regular topology

This file characterises sheaves for the regular topology.

Main results

• 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.

class CategoryTheory.Presieve.regular {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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_1} [CategoryTheory.Category.{u_3, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_2)) {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 := ⋯ }

def CategoryTheory.regularCoverage.EqualizerCondition {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_2)) : 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_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {S : CategoryTheory.Presieve B} [CategoryTheory.Presieve.regular S] [CategoryTheory.Presieve.hasPullbacks S] {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} (hF : CategoryTheory.regularCoverage.EqualizerCondition F) : CategoryTheory.Presieve.IsSheafFor F S

theorem CategoryTheory.regularCoverage.equalizerCondition_of_regular {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} (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_1} [CategoryTheory.Category.{u_3, u_1} C] {X : C} (S : CategoryTheory.Presieve X) [CategoryTheory.Presieve.regular S] [CategoryTheory.Projective X] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)) : CategoryTheory.Presieve.IsSheafFor F S

theorem CategoryTheory.regularCoverage.EqualizerCondition.isSheaf_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)) [∀ ⦃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_1} [CategoryTheory.Category.{u_3, u_1} C] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)) [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_1} [CategoryTheory.Category.{u_2, u_1} 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_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preregular C] : CategoryTheory.Sheaf.Subcanonical (CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.regularCoverage C))

The regular topology on any preregular category is subcanonical.