Documentation

Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Sheaves for the regular topology #

This file characterises sheaves for the regular topology.

Main results #

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

Instances

    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.

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

    Equations

    The equalizer condition is preserved by natural isomorphism.

    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.

    Equations

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

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

    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.

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

    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.