mathlib documentation

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

source
@[simp]
theorem category_theory.grothendieck_topology.diagram_map {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) (X : C) (S T : (J.cover X)ᵒᵖ) (f : S ⟶ T) :
(J.diagram P X).map f = category_theory.limits.multiequalizer.lift ((opposite.unop T).index P) (category_theory.limits.multiequalizer ((opposite.unop S).index P)) (λ (I : ((opposite.unop T).index P).L), category_theory.limits.multiequalizer.ι ((opposite.unop S).index P) (category_theory.grothendieck_topology.cover.arrow.map I f.unop)) _
source
noncomputable def category_theory.grothendieck_topology.diagram {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) (X : C) :
(J.cover X)ᵒᵖ ⥤ D

The diagram whose colimit defines the values of plus.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.diagram_obj {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) (X : C) (S : (J.cover X)ᵒᵖ) :
(J.diagram P X).obj S = category_theory.limits.multiequalizer ((opposite.unop S).index P)
source
noncomputable def category_theory.grothendieck_topology.diagram_pullback {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) {X Y : C} (f : X ⟶ Y) :
J.diagram P Y ⟶ (J.pullback f).op ⋙ J.diagram P X

A helper definition used to define the morphisms for plus.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.diagram_pullback_app {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) {X Y : C} (f : X ⟶ Y) (S : (J.cover Y)ᵒᵖ) :
(J.diagram_pullback P f).app S = category_theory.limits.multiequalizer.lift ((opposite.unop ((J.pullback f).op.obj S)).index P) ((J.diagram P Y).obj S) (λ (I : ((opposite.unop ((J.pullback f).op.obj S)).index P).L), category_theory.limits.multiequalizer.ι ((opposite.unop S).index P) (category_theory.grothendieck_topology.cover.arrow.base I)) _
source
@[simp]
theorem category_theory.grothendieck_topology.diagram_nat_trans_app {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (X : C) (W : (J.cover X)ᵒᵖ) :
(J.diagram_nat_trans η X).app W = category_theory.limits.multiequalizer.lift ((opposite.unop W).index Q) ((J.diagram P X).obj W) (λ (i : ((opposite.unop W).index Q).L), category_theory.limits.multiequalizer.ι ((opposite.unop W).index P) i ≫ η.app (opposite.op i.Y)) _
source
noncomputable def category_theory.grothendieck_topology.diagram_nat_trans {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] {P Q : 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
source
@[simp]
theorem category_theory.grothendieck_topology.diagram_nat_trans_id {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) (P : Cᵒᵖ ⥤ D) :
J.diagram_nat_trans (𝟙 P) X = 𝟙 (J.diagram P X)
source
@[simp]
theorem category_theory.grothendieck_topology.diagram_nat_trans_comp {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) (X : C) :
J.diagram_nat_trans (η ≫ γ) X = J.diagram_nat_trans η X ≫ J.diagram_nat_trans γ X
source
@[simp]
theorem category_theory.grothendieck_topology.diagram_functor_map {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) (P Q : Cᵒᵖ ⥤ D) (η : P ⟶ Q) :
(J.diagram_functor D X).map η = J.diagram_nat_trans η X
source
@[simp]
theorem category_theory.grothendieck_topology.diagram_functor_obj {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) (P : Cᵒᵖ ⥤ D) :
(J.diagram_functor D X).obj P = J.diagram P X
source
noncomputable def category_theory.grothendieck_topology.diagram_functor {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) :
(Cᵒᵖ ⥤ D) ⥤ (J.cover X)ᵒᵖ ⥤ D

J.diagram P, as a functor in P.

Equations
Instances for category_theory.grothendieck_topology.diagram_functor
source
noncomputable def category_theory.grothendieck_topology.plus_obj {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :
Cᵒᵖ ⥤ D

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

Equations
source
noncomputable def category_theory.grothendieck_topology.plus_map {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :
J.plus_obj P ⟶ J.plus_obj Q

An auxiliary definition used in plus below.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.plus_map_id {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (P : Cᵒᵖ ⥤ D) :
J.plus_map (𝟙 P) = 𝟙 (J.plus_obj P)
source
@[simp]
theorem category_theory.grothendieck_topology.plus_map_comp {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) :
J.plus_map (η ≫ γ) = J.plus_map η ≫ J.plus_map γ
source
@[simp]
theorem category_theory.grothendieck_topology.plus_functor_obj {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (P : Cᵒᵖ ⥤ D) :
(J.plus_functor D).obj P = J.plus_obj P
source
noncomputable def category_theory.grothendieck_topology.plus_functor {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :
(Cᵒᵖ ⥤ D) ⥤ Cᵒᵖ ⥤ D

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

Equations
Instances for category_theory.grothendieck_topology.plus_functor
source
@[simp]
theorem category_theory.grothendieck_topology.plus_functor_map {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (P Q : Cᵒᵖ ⥤ D) (η : P ⟶ Q) :
(J.plus_functor D).map η = J.plus_map η
source
noncomputable def category_theory.grothendieck_topology.to_plus {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :
P ⟶ J.plus_obj P

The canonical map from P to J.plus.obj P. See to_plus for a functorial version.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.to_plus_naturality {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :
η ≫ J.to_plus Q = J.to_plus P ≫ J.plus_map η
source
@[simp]
theorem category_theory.grothendieck_topology.to_plus_naturality_assoc {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) {X' : Cᵒᵖ ⥤ D} (f' : J.plus_obj Q ⟶ X') :
η ≫ J.to_plus Q ≫ f' = J.to_plus P ≫ J.plus_map η ≫ f'
source
@[simp]
theorem category_theory.grothendieck_topology.to_plus_nat_trans_app {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (P : Cᵒᵖ ⥤ D) :
(J.to_plus_nat_trans D).app P = J.to_plus P
source
noncomputable def category_theory.grothendieck_topology.to_plus_nat_trans {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :
𝟭 (Cᵒᵖ ⥤ D) ⟶ J.plus_functor D

The natural transformation from the identity functor to plus.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.plus_map_to_plus {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :
J.plus_map (J.to_plus P) = J.to_plus (J.plus_obj P)

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

source
theorem category_theory.grothendieck_topology.is_iso_to_plus_of_is_sheaf {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (hP : category_theory.presheaf.is_sheaf J P) :
category_theory.is_iso (J.to_plus P)
source
noncomputable def category_theory.grothendieck_topology.iso_to_plus {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (hP : category_theory.presheaf.is_sheaf J P) :
P ≅ J.plus_obj P

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

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.iso_to_plus_hom {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (hP : category_theory.presheaf.is_sheaf J P) :
(J.iso_to_plus P hP).hom = J.to_plus P
source
noncomputable def category_theory.grothendieck_topology.plus_lift {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : category_theory.presheaf.is_sheaf J Q) :
J.plus_obj P ⟶ Q

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

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.to_plus_plus_lift_assoc {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : category_theory.presheaf.is_sheaf J Q) {X' : Cᵒᵖ ⥤ D} (f' : Q ⟶ X') :
J.to_plus P ≫ J.plus_lift η hQ ≫ f' = η ≫ f'
source
@[simp]
theorem category_theory.grothendieck_topology.to_plus_plus_lift {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : category_theory.presheaf.is_sheaf J Q) :
J.to_plus P ≫ J.plus_lift η hQ = η
source
theorem category_theory.grothendieck_topology.plus_lift_unique {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : category_theory.presheaf.is_sheaf J Q) (γ : J.plus_obj P ⟶ Q) (hγ : J.to_plus P ≫ γ = η) :
γ = J.plus_lift η hQ
source
theorem category_theory.grothendieck_topology.plus_hom_ext {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η γ : J.plus_obj P ⟶ Q) (hQ : category_theory.presheaf.is_sheaf J Q) (h : J.to_plus P ≫ η = J.to_plus P ≫ γ) :
η = γ
source
@[simp]
theorem category_theory.grothendieck_topology.iso_to_plus_inv {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (hP : category_theory.presheaf.is_sheaf J P) :
(J.iso_to_plus P hP).inv = J.plus_lift (𝟙 P) hP
source
@[simp]
theorem category_theory.grothendieck_topology.plus_map_plus_lift {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : category_theory.presheaf.is_sheaf J R) :
J.plus_map η ≫ J.plus_lift γ hR = J.plus_lift (η ≫ γ) hR