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} [CategoryTheory.Category.{u_4, 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.

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

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

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

Equations

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

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

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

Equations

• CategoryTheory.regularTopology.EqualizerCondition P = ∀ ⦃X B : C⦄ (π : X ⟶ B) [inst_1 : CategoryTheory.EffectiveEpi π], CategoryTheory.regularTopology.SingleEqualizerCondition P π

theorem CategoryTheory.regularTopology.equalizerCondition_of_natIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {P : CategoryTheory.Functor Cᵒᵖ D} {P' : CategoryTheory.Functor Cᵒᵖ D} (i : P ≅ P') (hP : CategoryTheory.regularTopology.EqualizerCondition P) : CategoryTheory.regularTopology.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} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] (P : CategoryTheory.Functor Cᵒᵖ D) (F : CategoryTheory.Functor E C) [{X B : E} → (π : X ⟶ B) → [inst : CategoryTheory.EffectiveEpi π] → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) F] [CategoryTheory.Functor.PreservesEffectiveEpis F] (hP : CategoryTheory.regularTopology.EqualizerCondition P) : CategoryTheory.regularTopology.EqualizerCondition (CategoryTheory.Functor.comp F.op P)

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

def CategoryTheory.regularTopology.MapToEqualizer {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)) {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 canonical map to the explicit equalizer.

Equations

• CategoryTheory.regularTopology.MapToEqualizer P f g₁ g₂ w t = { val := P.map f.op t, property := ⋯ }

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

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

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

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

theorem CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)) : CategoryTheory.regularTopology.EqualizerCondition P ↔ ∀ (X B : C) (π : X ⟶ B) [inst : CategoryTheory.EffectiveEpi π] [inst : CategoryTheory.Limits.HasPullback π π], CategoryTheory.IsIso (CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] (P : CategoryTheory.Functor Cᵒᵖ D) (e : C ≌ E) : CategoryTheory.regularTopology.EqualizerCondition P ↔ CategoryTheory.regularTopology.EqualizerCondition (CategoryTheory.Functor.comp (CategoryTheory.Equivalence.op e).inverse P)

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

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

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

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

Equations

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

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

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

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

theorem CategoryTheory.regularTopology.isSheaf_of_projective {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Preregular C] [∀ (X : C), CategoryTheory.Projective X] : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preregular C] (W : C) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.regularTopology C) (CategoryTheory.yoneda.obj W)

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

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

The regular topology on any preregular category is subcanonical.