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.

noncomputable def CategoryTheory.GrothendieckTopology.diagram {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) (X : C) : Functor (J.Cover X)ᵒᵖ D

The diagram whose colimit defines the values of plus.

@[simp]

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagram_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) (X : C) (S : (J.Cover X)ᵒᵖ) : (J.diagram P X).obj S = Limits.multiequalizer ((Opposite.unop S).index P)

noncomputable def CategoryTheory.GrothendieckTopology.diagramPullback {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) {X 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.

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramPullback_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) {X Y : C} (f : X ⟶ Y) (S : (J.Cover Y)ᵒᵖ) : (J.diagramPullback P f).app S = Limits.Multiequalizer.lift ((Opposite.unop ((J.pullback f).op.obj S)).index P) ((J.diagram P Y).obj S) (fun (I : (Opposite.unop ((J.pullback f).op.obj S)).shape.L) => Limits.Multiequalizer.ι ((Opposite.unop S).index P) (Cover.Arrow.base I)) ⋯

noncomputable def CategoryTheory.GrothendieckTopology.diagramNatTrans {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) (X : C) : J.diagram P X ⟶ J.diagram Q X

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) (X : C) (W : (J.Cover X)ᵒᵖ) : (J.diagramNatTrans η X).app W = Limits.Multiequalizer.lift ((Opposite.unop W).index Q) ((J.diagram P X).obj W) (fun (x : (Opposite.unop W).shape.L) => CategoryStruct.comp (Limits.Multiequalizer.ι ((Opposite.unop W).index P) x) (η.app (Opposite.op x.Y))) ⋯

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_id {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (X : C) (P : Functor Cᵒᵖ D) : J.diagramNatTrans (CategoryStruct.id P) X = CategoryStruct.id (J.diagram P X)

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_zero {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [Preadditive D] (X : C) (P Q : Functor Cᵒᵖ D) : J.diagramNatTrans 0 X = 0

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_comp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {P Q R : Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (X : C) : J.diagramNatTrans (CategoryStruct.comp η γ) X = CategoryStruct.comp (J.diagramNatTrans η X) (J.diagramNatTrans γ X)

noncomputable def CategoryTheory.GrothendieckTopology.diagramFunctor {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (X : C) : Functor (Functor Cᵒᵖ D) (Functor (J.Cover X)ᵒᵖ D)

J.diagram P, as a functor in P.

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramFunctor_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (X : C) (P : Functor Cᵒᵖ D) : (J.diagramFunctor D X).obj P = J.diagram P X

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramFunctor_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (X : C) {X✝ Y✝ : Functor Cᵒᵖ D} (η : X✝ ⟶ Y✝) : (J.diagramFunctor D X).map η = J.diagramNatTrans η X

noncomputable def CategoryTheory.GrothendieckTopology.plusObj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : Functor Cᵒᵖ D

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

noncomputable def CategoryTheory.GrothendieckTopology.plusMap {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) : J.plusObj P ⟶ J.plusObj Q

An auxiliary definition used in plus below.

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusMap_id {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : Functor Cᵒᵖ D) : J.plusMap (CategoryStruct.id P) = CategoryStruct.id (J.plusObj P)

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusMap_zero {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [Preadditive D] (P Q : Functor Cᵒᵖ D) : J.plusMap 0 = 0

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusMap_comp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) : J.plusMap (CategoryStruct.comp η γ) = CategoryStruct.comp (J.plusMap η) (J.plusMap γ)

theorem CategoryTheory.GrothendieckTopology.plusMap_comp_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) {Z : Functor Cᵒᵖ D} (h : J.plusObj R ⟶ Z) : CategoryStruct.comp (J.plusMap (CategoryStruct.comp η γ)) h = CategoryStruct.comp (J.plusMap η) (CategoryStruct.comp (J.plusMap γ) h)

noncomputable def CategoryTheory.GrothendieckTopology.plusFunctor {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : Functor (Functor Cᵒᵖ D) (Functor Cᵒᵖ D)

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusFunctor_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : Functor Cᵒᵖ D) : (J.plusFunctor D).obj P = J.plusObj P

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusFunctor_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {X✝ Y✝ : Functor Cᵒᵖ D} (η : X✝ ⟶ Y✝) : (J.plusFunctor D).map η = J.plusMap η

noncomputable def CategoryTheory.GrothendieckTopology.toPlus {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : P ⟶ J.plusObj P

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.toPlus_naturality {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) : CategoryStruct.comp η (J.toPlus Q) = CategoryStruct.comp (J.toPlus P) (J.plusMap η)

@[simp]

theorem CategoryTheory.GrothendieckTopology.toPlus_naturality_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : Functor Cᵒᵖ D} (h : J.plusObj Q ⟶ Z) : CategoryStruct.comp η (CategoryStruct.comp (J.toPlus Q) h) = CategoryStruct.comp (J.toPlus P) (CategoryStruct.comp (J.plusMap η) h)

noncomputable def CategoryTheory.GrothendieckTopology.toPlusNatTrans {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : Functor.id (Functor Cᵒᵖ D) ⟶ J.plusFunctor D

The natural transformation from the identity functor to plus.

@[simp]

theorem CategoryTheory.GrothendieckTopology.toPlusNatTrans_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : Functor Cᵒᵖ D) : (J.toPlusNatTrans D).app P = J.toPlus P

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusMap_toPlus {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P)

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

theorem CategoryTheory.GrothendieckTopology.isIso_toPlus_of_isSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : Presheaf.IsSheaf J P) : IsIso (J.toPlus P)

noncomputable def CategoryTheory.GrothendieckTopology.isoToPlus {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : Presheaf.IsSheaf J P) : P ≅ J.plusObj P

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.isoToPlus_hom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : Presheaf.IsSheaf J P) : (J.isoToPlus P hP).hom = J.toPlus P

noncomputable def CategoryTheory.GrothendieckTopology.plusLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) : J.plusObj P ⟶ Q

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.toPlus_plusLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) : CategoryStruct.comp (J.toPlus P) (J.plusLift η hQ) = η

@[simp]

theorem CategoryTheory.GrothendieckTopology.toPlus_plusLift_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) {Z : Functor Cᵒᵖ D} (h : Q ⟶ Z) : CategoryStruct.comp (J.toPlus P) (CategoryStruct.comp (J.plusLift η hQ) h) = CategoryStruct.comp η h

theorem CategoryTheory.GrothendieckTopology.plusLift_unique {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) (γ : J.plusObj P ⟶ Q) (hγ : CategoryStruct.comp (J.toPlus P) γ = η) : γ = J.plusLift η hQ

theorem CategoryTheory.GrothendieckTopology.plus_hom_ext {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : Functor Cᵒᵖ D} (η γ : J.plusObj P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) (h : CategoryStruct.comp (J.toPlus P) η = CategoryStruct.comp (J.toPlus P) γ) : η = γ

@[simp]

theorem CategoryTheory.GrothendieckTopology.isoToPlus_inv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : Presheaf.IsSheaf J P) : (J.isoToPlus P hP).inv = J.plusLift (CategoryStruct.id P) hP

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusMap_plusLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : Presheaf.IsSheaf J R) : CategoryStruct.comp (J.plusMap η) (J.plusLift γ hR) = J.plusLift (CategoryStruct.comp η γ) hR

instance CategoryTheory.GrothendieckTopology.plusFunctor_preservesZeroMorphisms {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [Preadditive D] : (J.plusFunctor D).PreservesZeroMorphisms