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.

def CategoryTheory.GrothendieckTopology.diagram {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) : CategoryTheory.Functor (J.Cover X)ᵒᵖ D

The diagram whose colimit defines the values of plus.

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagram_obj {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)ᵒᵖ) : (J.diagram P X).obj S = CategoryTheory.Limits.multiequalizer ((Opposite.unop S).index P)

@[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 x✝ : (J.Cover X)ᵒᵖ} (f : S ⟶ x✝) : (J.diagram P X).map f = CategoryTheory.Limits.Multiequalizer.lift ((Opposite.unop x✝).index P) ((fun (S : (J.Cover X)ᵒᵖ) => CategoryTheory.Limits.multiequalizer ((Opposite.unop S).index P)) S) (fun (I : ((Opposite.unop x✝).index P).L) => CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop S).index P) (CategoryTheory.GrothendieckTopology.Cover.Arrow.map I f.unop)) ⋯

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 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.

@[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 Y : C} (f : X ⟶ Y) (S : (J.Cover Y)ᵒᵖ) : (J.diagramPullback P f).app S = CategoryTheory.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)).index P).L) => CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop S).index P) (CategoryTheory.GrothendieckTopology.Cover.Arrow.base I)) ⋯

def CategoryTheory.GrothendieckTopology.diagramNatTrans {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 Q : CategoryTheory.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.

Equations

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

@[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 Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (X : C) (W : (J.Cover X)ᵒᵖ) : (J.diagramNatTrans η X).app W = CategoryTheory.Limits.Multiequalizer.lift ((Opposite.unop W).index Q) ((J.diagram P X).obj W) (fun (x : ((Opposite.unop W).index Q).L) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) x) (η.app (Opposite.op x.Y))) ⋯

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_id {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) (P : CategoryTheory.Functor Cᵒᵖ D) : J.diagramNatTrans (CategoryTheory.CategoryStruct.id P) X = CategoryTheory.CategoryStruct.id (J.diagram P X)

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_zero {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)] [CategoryTheory.Preadditive D] (X : C) (P Q : CategoryTheory.Functor Cᵒᵖ D) : J.diagramNatTrans 0 X = 0

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_comp {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 Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (X : C) : J.diagramNatTrans (CategoryTheory.CategoryStruct.comp η γ) X = CategoryTheory.CategoryStruct.comp (J.diagramNatTrans η X) (J.diagramNatTrans γ X)

def CategoryTheory.GrothendieckTopology.diagramFunctor {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) : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Functor (J.Cover X)ᵒᵖ D)

J.diagram P, as a functor in P.

Equations

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

@[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✝ Y✝ : CategoryTheory.Functor Cᵒᵖ D} (η : X✝ ⟶ Y✝) : (J.diagramFunctor D X).map η = J.diagramNatTrans η X

@[simp]

theorem CategoryTheory.GrothendieckTopology.diagramFunctor_obj {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) (P : CategoryTheory.Functor Cᵒᵖ D) : (J.diagramFunctor D X).obj P = J.diagram P X

def CategoryTheory.GrothendieckTopology.plusObj {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : CategoryTheory.Functor Cᵒᵖ D

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.

def CategoryTheory.GrothendieckTopology.plusMap {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : J.plusObj P ⟶ J.plusObj Q

An auxiliary definition used in plus below.

Equations

• J.plusMap η = { app := fun (X : Cᵒᵖ) => CategoryTheory.Limits.colimMap (J.diagramNatTrans η (Opposite.unop X)), naturality := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusMap_id {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : J.plusMap (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (J.plusObj P)

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusMap_zero {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.Preadditive D] (P Q : CategoryTheory.Functor Cᵒᵖ D) : J.plusMap 0 = 0

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusMap_comp {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) : J.plusMap (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (J.plusMap η) (J.plusMap γ)

theorem CategoryTheory.GrothendieckTopology.plusMap_comp_assoc {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : J.plusObj R ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.plusMap (CategoryTheory.CategoryStruct.comp η γ)) h = CategoryTheory.CategoryStruct.comp (J.plusMap η) (CategoryTheory.CategoryStruct.comp (J.plusMap γ) h)

def CategoryTheory.GrothendieckTopology.plusFunctor {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Functor Cᵒᵖ D)

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

Equations

• J.plusFunctor D = { obj := fun (P : CategoryTheory.Functor Cᵒᵖ D) => J.plusObj P, map := fun {X Y : CategoryTheory.Functor Cᵒᵖ D} (η : X ⟶ Y) => J.plusMap η, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusFunctor_obj {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.plusFunctor D).obj P = J.plusObj P

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusFunctor_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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ D} (η : X✝ ⟶ Y✝) : (J.plusFunctor D).map η = J.plusMap η

def CategoryTheory.GrothendieckTopology.toPlus {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), CategoryTheory.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.

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.toPlus_naturality {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : CategoryTheory.CategoryStruct.comp η (J.toPlus Q) = CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusMap η)

@[simp]

theorem CategoryTheory.GrothendieckTopology.toPlus_naturality_assoc {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : J.plusObj Q ⟶ Z) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (J.toPlus Q) h) = CategoryTheory.CategoryStruct.comp (J.toPlus P) (CategoryTheory.CategoryStruct.comp (J.plusMap η) h)

def CategoryTheory.GrothendieckTopology.toPlusNatTrans {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ D) ⟶ J.plusFunctor D

The natural transformation from the identity functor to plus.

Equations

• J.toPlusNatTrans D = { app := fun (P : CategoryTheory.Functor Cᵒᵖ D) => J.toPlus P, naturality := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.toPlusNatTrans_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)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.toPlusNatTrans D).app P = J.toPlus P

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusMap_toPlus {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), CategoryTheory.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} [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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.IsIso (J.toPlus P)

def CategoryTheory.GrothendieckTopology.isoToPlus {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : P ≅ J.plusObj P

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

Equations

• J.isoToPlus P hP = CategoryTheory.asIso (J.toPlus P)

@[simp]

theorem CategoryTheory.GrothendieckTopology.isoToPlus_hom {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : (J.isoToPlus P hP).hom = J.toPlus P

def CategoryTheory.GrothendieckTopology.plusLift {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : J.plusObj P ⟶ Q

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

Equations

• J.plusLift η hQ = CategoryTheory.CategoryStruct.comp (J.plusMap η) (J.isoToPlus Q hQ).inv

@[simp]

theorem CategoryTheory.GrothendieckTopology.toPlus_plusLift {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusLift η hQ) = η

@[simp]

theorem CategoryTheory.GrothendieckTopology.toPlus_plusLift_assoc {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.toPlus P) (CategoryTheory.CategoryStruct.comp (J.plusLift η hQ) h) = CategoryTheory.CategoryStruct.comp η h

theorem CategoryTheory.GrothendieckTopology.plusLift_unique {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : J.plusObj P ⟶ Q) (hγ : CategoryTheory.CategoryStruct.comp (J.toPlus P) γ = η) : γ = J.plusLift η hQ

theorem CategoryTheory.GrothendieckTopology.plus_hom_ext {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η γ : J.plusObj P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (h : CategoryTheory.CategoryStruct.comp (J.toPlus P) η = CategoryTheory.CategoryStruct.comp (J.toPlus P) γ) : η = γ

@[simp]

theorem CategoryTheory.GrothendieckTopology.isoToPlus_inv {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : (J.isoToPlus P hP).inv = J.plusLift (CategoryTheory.CategoryStruct.id P) hP

@[simp]

theorem CategoryTheory.GrothendieckTopology.plusMap_plusLift {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R) : CategoryTheory.CategoryStruct.comp (J.plusMap η) (J.plusLift γ hR) = J.plusLift (CategoryTheory.CategoryStruct.comp η γ) hR

instance CategoryTheory.GrothendieckTopology.plusFunctor_preservesZeroMorphisms {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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.Preadditive D] : (J.plusFunctor D).PreservesZeroMorphisms