Sheaves for the regular topology

This file characterises sheaves for the regular topology.

Main results

• equalizerCondition_iff_isSheaf: 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} [Category.{u_4, u_1} C] {X : C} (R : Presieve X) : Prop

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

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

  R consists of a single epimorphism.

theorem CategoryTheory.regularTopology.equalizerCondition_w {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (P : Functor Cᵒᵖ D) {X B : C} {π : X ⟶ B} (c : Limits.PullbackCone π π) : CategoryStruct.comp (P.map π.op) (P.map c.fst.op) = CategoryStruct.comp (P.map π.op) (P.map c.snd.op)

def CategoryTheory.regularTopology.SingleEqualizerCondition {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (P : Functor Cᵒᵖ D) ⦃X B : C⦄ (π : X ⟶ B) : Prop

A contravariant functor on C satisfies SingleEqualizerCondition with respect to a morphism π if it takes its kernel pair to an equalizer diagram.

def CategoryTheory.regularTopology.EqualizerCondition {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (P : Functor Cᵒᵖ D) : Prop

A contravariant functor on C satisfies EqualizerCondition if it takes kernel pairs of effective epimorphisms to equalizer diagrams.

theorem CategoryTheory.regularTopology.equalizerCondition_of_natIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {P P' : Functor Cᵒᵖ D} (i : P ≅ P') (hP : EqualizerCondition P) : EqualizerCondition P'

The equalizer condition is preserved by natural isomorphism.

theorem CategoryTheory.regularTopology.equalizerCondition_precomp_of_preservesPullback {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] (P : Functor Cᵒᵖ D) (F : Functor E C) [∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], Limits.PreservesLimit (Limits.cospan π π) F] [F.PreservesEffectiveEpis] (hP : EqualizerCondition P) : EqualizerCondition (F.op.comp P)

Precomposing with a pullback-preserving functor preserves the equalizer condition.

def CategoryTheory.regularTopology.MapToEqualizer {C : Type u_1} [Category.{u_5, u_1} C] (P : Functor Cᵒᵖ (Type u_4)) {W X B : C} (f : X ⟶ B) (g₁ g₂ : W ⟶ X) (w : CategoryStruct.comp g₁ f = 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 canonical map to the explicit equalizer.

theorem CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback {C : Type u_1} [Category.{u_5, u_1} C] (P : Functor Cᵒᵖ (Type u_4)) (hP : EqualizerCondition P) (X B : C) (π : X ⟶ B) [EffectiveEpi π] [Limits.HasPullback π π] : Function.Bijective (MapToEqualizer P π (Limits.pullback.fst π π) (Limits.pullback.snd π π) ⋯)

theorem CategoryTheory.regularTopology.EqualizerCondition.mk {C : Type u_1} [Category.{u_5, u_1} C] (P : Functor Cᵒᵖ (Type u_4)) (hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : Limits.HasPullback π π], Function.Bijective (MapToEqualizer P π (Limits.pullback.fst π π) (Limits.pullback.snd π π) ⋯)) : EqualizerCondition P

theorem CategoryTheory.regularTopology.equalizerCondition_w' {C : Type u_1} [Category.{u_5, u_1} C] (P : Functor Cᵒᵖ (Type u_4)) {X B : C} (π : X ⟶ B) [Limits.HasPullback π π] : CategoryStruct.comp (P.map π.op) (P.map (Limits.pullback.fst π π).op) = CategoryStruct.comp (P.map π.op) (P.map (Limits.pullback.snd π π).op)

theorem CategoryTheory.regularTopology.mapToEqualizer_eq_comp {C : Type u_1} [Category.{u_5, u_1} C] (P : Functor Cᵒᵖ (Type u_4)) {X B : C} (π : X ⟶ B) [Limits.HasPullback π π] : MapToEqualizer P π (Limits.pullback.fst π π) (Limits.pullback.snd π π) ⋯ = CategoryStruct.comp (Limits.equalizer.lift (P.map π.op) ⋯) (Limits.Types.equalizerIso (P.map (Limits.pullback.fst π π).op) (P.map (Limits.pullback.snd π π).op)).hom

theorem CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift {C : Type u_1} [Category.{u_5, u_1} C] (P : Functor Cᵒᵖ (Type u_4)) : EqualizerCondition P ↔ ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : Limits.HasPullback π π], IsIso (Limits.equalizer.lift (P.map π.op) ⋯)

An alternative phrasing of the explicit equalizer condition, using more categorical language.

theorem CategoryTheory.regularTopology.equalizerCondition_iff_of_equivalence {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] (P : Functor Cᵒᵖ D) (e : C ≌ E) : EqualizerCondition P ↔ EqualizerCondition (e.op.inverse.comp P)

P satisfies the equalizer condition iff its precomposition by an equivalence does.

theorem CategoryTheory.regularTopology.parallelPair_pullback_initial {C : Type u_1} [Category.{u_4, u_1} C] {X B : C} (π : X ⟶ B) (c : Limits.PullbackCone π π) (hc : Limits.IsLimit c) : (Limits.parallelPair (Over.homMk c.fst ⋯).op (Over.homMk c.snd ⋯).op).Initial

noncomputable def CategoryTheory.regularTopology.isLimit_forkOfι_equiv {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (P : Functor Cᵒᵖ D) {X B : C} (π : X ⟶ B) (c : Limits.PullbackCone π π) (hc : Limits.IsLimit c) : Limits.IsLimit (Limits.Fork.ofι (P.map π.op) ⋯) ≃ Limits.IsLimit (P.mapCone (Sieve.ofArrows (fun (x : Unit) => X) fun (x : Unit) => π).arrows.cocone.op)

Given a limiting pullback cone, the fork in SingleEqualizerCondition is limiting iff the diagram in Presheaf.isSheaf_iff_isLimit_coverage is limiting.

theorem CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (P : Functor Cᵒᵖ D) ⦃X B : C⦄ (π : X ⟶ B) [Limits.HasPullback π π] : SingleEqualizerCondition P π ↔ Nonempty (Limits.IsLimit (P.mapCone (Sieve.ofArrows (fun (x : Unit) => X) fun (x : Unit) => π).arrows.cocone.op))

theorem CategoryTheory.regularTopology.equalizerCondition_iff_isSheaf {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor Cᵒᵖ D) [Preregular C] [∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], Limits.HasPullback f f] : EqualizerCondition F ↔ Presheaf.IsSheaf (regularTopology C) F

theorem CategoryTheory.regularTopology.isSheafFor_regular_of_projective {C : Type u_1} [Category.{u_5, u_1} C] {X : C} (S : Presieve X) [S.regular] [Projective X] (F : Functor Cᵒᵖ (Type u_4)) : Presieve.IsSheafFor F S

theorem CategoryTheory.regularTopology.isSheaf_of_projective {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor Cᵒᵖ D) [Preregular C] [∀ (X : C), Projective X] : Presheaf.IsSheaf (regularTopology C) F

Every presheaf is a sheaf for the regular topology if every object of C is projective.

theorem CategoryTheory.regularTopology.isSheaf_yoneda_obj {C : Type u_1} [Category.{u_4, u_1} C] [Preregular C] (W : C) : Presieve.IsSheaf (regularTopology C) (yoneda.obj W)

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

instance CategoryTheory.regularTopology.subcanonical {C : Type u_1} [Category.{u_4, u_1} C] [Preregular C] : (regularTopology C).Subcanonical

The regular topology on any preregular category is subcanonical.