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
    theorem CategoryTheory.Presieve.regular.single_epi {C : Type u_1} :
    ∀ {inst : CategoryTheory.Category.{u_4, u_1} C} {X : C} {R : CategoryTheory.Presieve X} [self : R.regular], ∃ (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.

    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
      Instances For
        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
        Instances For

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

          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 Yoneda-presheaf is a sheaf for the regular topology.