mathlib3 documentation

category_theory.sites.plus

The plus construction for presheaves. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

A helper definition used to define the morphisms for plus.

Equations

A natural transformation P ⟶ Q induces a natural transformation between diagrams whose colimits define the values of plus.

Equations

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

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

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