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

@[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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ) : (CategoryTheory.GrothendieckTopology.diagram J P X).toPrefunctor.obj S = CategoryTheory.Limits.multiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S.unop 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) {S : (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ} : ∀ {x : (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ} (f : S ⟶ x), (CategoryTheory.GrothendieckTopology.diagram J P X).toPrefunctor.map f = CategoryTheory.Limits.Multiequalizer.lift (CategoryTheory.GrothendieckTopology.Cover.index x.unop P) ((fun (S : (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ) => CategoryTheory.Limits.multiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S.unop P)) S) (fun (I : (CategoryTheory.GrothendieckTopology.Cover.index x.unop P).L) => CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.GrothendieckTopology.Cover.Arrow.map I f.unop)) (_ : ∀ (I : (CategoryTheory.GrothendieckTopology.Cover.index x.unop P).R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) ((CategoryTheory.GrothendieckTopology.Cover.index S.unop P).fstTo (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f.unop))) ((CategoryTheory.GrothendieckTopology.Cover.index S.unop P).fst (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f.unop)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) ((CategoryTheory.GrothendieckTopology.Cover.index S.unop P).sndTo (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f.unop))) ((CategoryTheory.GrothendieckTopology.Cover.index S.unop P).snd (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f.unop)))

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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) : CategoryTheory.Functor (CategoryTheory.GrothendieckTopology.Cover J 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.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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (P : CategoryTheory.Functor Cᵒᵖ D) {X : C} {Y : C} (f : X ⟶ Y) (S : (CategoryTheory.GrothendieckTopology.Cover J Y)ᵒᵖ) : (CategoryTheory.GrothendieckTopology.diagramPullback J P f).app S = CategoryTheory.Limits.Multiequalizer.lift (CategoryTheory.GrothendieckTopology.Cover.index ((CategoryTheory.GrothendieckTopology.pullback J f).op.toPrefunctor.obj S).unop P) ((CategoryTheory.GrothendieckTopology.diagram J P Y).toPrefunctor.obj S) (fun (I : (CategoryTheory.GrothendieckTopology.Cover.index ((CategoryTheory.GrothendieckTopology.pullback J f).op.toPrefunctor.obj S).unop P).L) => CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.GrothendieckTopology.Cover.Arrow.base I)) (_ : ∀ (I : (CategoryTheory.GrothendieckTopology.Cover.index ((CategoryTheory.GrothendieckTopology.pullback J f).op.toPrefunctor.obj S).unop P).R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) ((CategoryTheory.GrothendieckTopology.Cover.index S.unop P).fstTo (CategoryTheory.GrothendieckTopology.Cover.Relation.base I))) ((CategoryTheory.GrothendieckTopology.Cover.index S.unop P).fst (CategoryTheory.GrothendieckTopology.Cover.Relation.base I)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) ((CategoryTheory.GrothendieckTopology.Cover.index S.unop P).sndTo (CategoryTheory.GrothendieckTopology.Cover.Relation.base I))) ((CategoryTheory.GrothendieckTopology.Cover.index S.unop P).snd (CategoryTheory.GrothendieckTopology.Cover.Relation.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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (P : CategoryTheory.Functor Cᵒᵖ D) {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.GrothendieckTopology.diagram J P Y ⟶ CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.pullback J f).op (CategoryTheory.GrothendieckTopology.diagram J 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.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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (X : C) (W : (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ) : (CategoryTheory.GrothendieckTopology.diagramNatTrans J η X).app W = CategoryTheory.Limits.Multiequalizer.lift (CategoryTheory.GrothendieckTopology.Cover.index W.unop Q) ((CategoryTheory.GrothendieckTopology.diagram J P X).toPrefunctor.obj W) (fun (i : (CategoryTheory.GrothendieckTopology.Cover.index W.unop Q).L) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index W.unop P) i) (η.app (Opposite.op i.Y))) (_ : ∀ (i : (CategoryTheory.GrothendieckTopology.Cover.index W.unop Q).R), CategoryTheory.CategoryStruct.comp ((fun (i : (CategoryTheory.GrothendieckTopology.Cover.index W.unop Q).L) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index W.unop P) i) (η.app (Opposite.op i.Y))) ((CategoryTheory.GrothendieckTopology.Cover.index W.unop Q).fstTo i)) ((CategoryTheory.GrothendieckTopology.Cover.index W.unop Q).fst i) = CategoryTheory.CategoryStruct.comp ((fun (i : (CategoryTheory.GrothendieckTopology.Cover.index W.unop Q).L) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index W.unop P) i) (η.app (Opposite.op i.Y))) ((CategoryTheory.GrothendieckTopology.Cover.index W.unop Q).sndTo i)) ((CategoryTheory.GrothendieckTopology.Cover.index W.unop Q).snd 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (X : C) : CategoryTheory.GrothendieckTopology.diagram J P X ⟶ CategoryTheory.GrothendieckTopology.diagram J 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_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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (X : C) (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.GrothendieckTopology.diagramNatTrans J (CategoryTheory.CategoryStruct.id P) X = CategoryTheory.CategoryStruct.id (CategoryTheory.GrothendieckTopology.diagram J 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [CategoryTheory.Preadditive D] (X : C) (P : CategoryTheory.Functor Cᵒᵖ D) (Q : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.GrothendieckTopology.diagramNatTrans J 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} {R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (X : C) : CategoryTheory.GrothendieckTopology.diagramNatTrans J (CategoryTheory.CategoryStruct.comp η γ) X = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.diagramNatTrans J η X) (CategoryTheory.GrothendieckTopology.diagramNatTrans J γ X)

@[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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (X : C) : ∀ {X_1 Y : CategoryTheory.Functor Cᵒᵖ D} (η : X_1 ⟶ Y), (CategoryTheory.GrothendieckTopology.diagramFunctor J D X).toPrefunctor.map η = CategoryTheory.GrothendieckTopology.diagramNatTrans J η 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (X : C) (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.GrothendieckTopology.diagramFunctor J D X).toPrefunctor.obj P = CategoryTheory.GrothendieckTopology.diagram J P 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (X : C) : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Functor (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D)

J.diagram P, as a functor in P.

Equations

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

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

An auxiliary definition used in plus below.

Equations

• CategoryTheory.GrothendieckTopology.plusMap J η = CategoryTheory.NatTrans.mk fun (X : Cᵒᵖ) => CategoryTheory.Limits.colimMap (CategoryTheory.GrothendieckTopology.diagramNatTrans J η X.unop)

@[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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.GrothendieckTopology.plusMap J (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (CategoryTheory.GrothendieckTopology.plusObj J 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.Preadditive D] (P : CategoryTheory.Functor Cᵒᵖ D) (Q : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.GrothendieckTopology.plusMap J 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} {R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) : CategoryTheory.GrothendieckTopology.plusMap J (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusMap J η) (CategoryTheory.GrothendieckTopology.plusMap J γ)

@[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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] : ∀ {X Y : CategoryTheory.Functor Cᵒᵖ D} (η : X ⟶ Y), (CategoryTheory.GrothendieckTopology.plusFunctor J D).toPrefunctor.map η = CategoryTheory.GrothendieckTopology.plusMap J η

@[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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.GrothendieckTopology.plusFunctor J D).toPrefunctor.obj P = CategoryTheory.GrothendieckTopology.plusObj J P

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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Functor Cᵒᵖ D)

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

Equations

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

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

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

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

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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] : CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ D) ⟶ CategoryTheory.GrothendieckTopology.plusFunctor J D

The natural transformation from the identity functor to plus.

Equations

• CategoryTheory.GrothendieckTopology.toPlusNatTrans J D = CategoryTheory.NatTrans.mk fun (P : CategoryTheory.Functor Cᵒᵖ D) => CategoryTheory.GrothendieckTopology.toPlus J 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] : CategoryTheory.GrothendieckTopology.plusMap J (CategoryTheory.GrothendieckTopology.toPlus J P) = CategoryTheory.GrothendieckTopology.toPlus J (CategoryTheory.GrothendieckTopology.plusObj J 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.IsIso (CategoryTheory.GrothendieckTopology.toPlus J 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : P ≅ CategoryTheory.GrothendieckTopology.plusObj J P

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

Equations

• CategoryTheory.GrothendieckTopology.isoToPlus J P hP = CategoryTheory.asIso (CategoryTheory.GrothendieckTopology.toPlus J 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : (CategoryTheory.GrothendieckTopology.isoToPlus J P hP).hom = CategoryTheory.GrothendieckTopology.toPlus J 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : CategoryTheory.GrothendieckTopology.plusObj J P ⟶ Q

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

Equations

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

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

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

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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : CategoryTheory.GrothendieckTopology.plusObj J P ⟶ Q) (hγ : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toPlus J P) γ = η) : γ = CategoryTheory.GrothendieckTopology.plusLift J η 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : CategoryTheory.GrothendieckTopology.plusObj J P ⟶ Q) (γ : CategoryTheory.GrothendieckTopology.plusObj J P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toPlus J P) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toPlus J 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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : (CategoryTheory.GrothendieckTopology.isoToPlus J P hP).inv = CategoryTheory.GrothendieckTopology.plusLift J (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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} {R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusMap J η) (CategoryTheory.GrothendieckTopology.plusLift J γ hR) = CategoryTheory.GrothendieckTopology.plusLift J (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 : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.Preadditive D] : CategoryTheory.Functor.PreservesZeroMorphisms (CategoryTheory.GrothendieckTopology.plusFunctor J D)

Equations

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