Documentation

Mathlib.CategoryTheory.Sites.Plus

The plus construction for presheaves. #

This file contains the construction of P⁺, for a presheaf P : Cᵒᵖ ⥤ D where C is endowed with a grothendieck topology J.

See https://stacks.math.columbia.edu/tag/00W1 for details.

@[simp]
theorem CategoryTheory.GrothendieckTopology.diagram_map {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) {S : (J.Cover X)ᵒᵖ} :
∀ {x : (J.Cover X)ᵒᵖ} (f : S x), (J.diagram P X).map f = CategoryTheory.Limits.Multiequalizer.lift (x.unop.index P) ((fun (S : (J.Cover X)ᵒᵖ) => CategoryTheory.Limits.multiequalizer (S.unop.index P)) S) (fun (I : (x.unop.index P).L) => CategoryTheory.Limits.Multiequalizer.ι (S.unop.index P) (CategoryTheory.GrothendieckTopology.Cover.Arrow.map I f.unop))

The diagram whose colimit defines the values of plus.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.diagramPullback_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (P : CategoryTheory.Functor Cᵒᵖ D) {X : C} {Y : C} (f : X Y) (S : (J.Cover Y)ᵒᵖ) :
    (J.diagramPullback P f).app S = CategoryTheory.Limits.Multiequalizer.lift (((J.pullback f).op.obj S).unop.index P) ((J.diagram P Y).obj S) (fun (I : (((J.pullback f).op.obj S).unop.index P).L) => CategoryTheory.Limits.Multiequalizer.ι (S.unop.index P) (CategoryTheory.GrothendieckTopology.Cover.Arrow.base I))
    def CategoryTheory.GrothendieckTopology.diagramPullback {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (P : CategoryTheory.Functor Cᵒᵖ D) {X : C} {Y : C} (f : X Y) :
    J.diagram P Y (J.pullback f).op.comp (J.diagram P X)

    A helper definition used to define the morphisms for plus.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P Q) (X : C) (W : (J.Cover X)ᵒᵖ) :
      (J.diagramNatTrans η X).app W = CategoryTheory.Limits.Multiequalizer.lift (W.unop.index Q) ((J.diagram P X).obj W) (fun (i : (W.unop.index Q).L) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (W.unop.index P) i) (η.app { unop := i.Y }))

      A natural transformation P ⟶ Q induces a natural transformation between diagrams whose colimits define the values of plus.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.diagramFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (X : C) :
        ∀ {X_1 Y : CategoryTheory.Functor Cᵒᵖ D} (η : X_1 Y), (J.diagramFunctor D X).map η = J.diagramNatTrans η X

        J.diagram P, as a functor in P.

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

          The plus construction, associating a presheaf to any presheaf. See plusFunctor below for a functorial version.

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

            An auxiliary definition used in plus below.

            Equations
            Instances For
              @[simp]

              The plus construction, a functor sending P to J.plusObj P.

              Equations
              Instances For

                The canonical map from P to J.plusObj P. See toPlusNatTrans for a functorial version.

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

                  The natural transformation from the identity functor to plus.

                  Equations
                  Instances For
                    @[simp]

                    (P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺

                    The natural isomorphism between P and P⁺ when P is a sheaf.

                    Equations
                    Instances For

                      Lift a morphism P ⟶ Q to P⁺ ⟶ Q when Q is a sheaf.

                      Equations
                      Instances For