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 : 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).map f = CategoryTheory.Limits.Multiequalizer.lift (CategoryTheory.GrothendieckTopology.Cover.index x.unop P) ((fun S => CategoryTheory.Limits.multiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S.unop P)) S) (fun I => 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.Limits.MulticospanIndex.fstTo (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f.unop))) (CategoryTheory.Limits.MulticospanIndex.fst (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f.unop)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.Limits.MulticospanIndex.sndTo (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f.unop))) (CategoryTheory.Limits.MulticospanIndex.snd (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f.unop)))
@[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.obj S).unop P) ((CategoryTheory.GrothendieckTopology.diagram J P Y).obj S) (fun I => 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.obj S).unop P).R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.Limits.MulticospanIndex.fstTo (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.GrothendieckTopology.Cover.Relation.base I))) (CategoryTheory.Limits.MulticospanIndex.fst (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.GrothendieckTopology.Cover.Relation.base I)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.Limits.MulticospanIndex.sndTo (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.GrothendieckTopology.Cover.Relation.base I))) (CategoryTheory.Limits.MulticospanIndex.snd (CategoryTheory.GrothendieckTopology.Cover.index S.unop P) (CategoryTheory.GrothendieckTopology.Cover.Relation.base I)))
@[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)ᵒᵖ) :