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.

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
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
@[simp]

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

Equations

An auxiliary definition used in plus below.

Equations
@[simp]

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

Equations
Instances for category_theory.grothendieck_topology.plus_functor

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

Equations

The natural transformation from the identity functor to plus.

Equations
@[simp]

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

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

Equations

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

Equations