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.
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.
Instances
R
consists of a single epimorphism.
A contravariant functor on C
satisfies 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.
Instances For
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 π
Instances For
The equalizer condition is preserved by natural isomorphism.
Precomposing with a pullback-preserving functor preserves the equalizer condition.
The canonical map to the explicit equalizer.
Equations
- CategoryTheory.regularTopology.MapToEqualizer P f g₁ g₂ w t = ⟨P.map f.op t, ⋯⟩
Instances For
An alternative phrasing of the explicit equalizer condition, using more categorical language.
P
satisfies the equalizer condition iff its precomposition by an equivalence does.
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.
Instances For
Every presheaf is a sheaf for the regular topology if every object of C
is projective.
Every Yoneda-presheaf is a sheaf for the regular topology.
The regular topology on any preregular category is subcanonical.