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.
The diagram whose colimit defines the values of plus
.
Equations
- J.diagram P X = {obj := λ (S : (J.cover X)ᵒᵖ), category_theory.limits.multiequalizer ((opposite.unop S).index P), map := λ (S T : (J.cover X)ᵒᵖ) (f : S ⟶ T), 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)) _, map_id' := _, map_comp' := _}
A helper definition used to define the morphisms for plus
.
Equations
- J.diagram_pullback P f = {app := λ (S : (J.cover Y)ᵒᵖ), 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)) _, naturality' := _}
A natural transformation P ⟶ Q
induces a natural transformation
between diagrams whose colimits define the values of plus
.
Equations
- J.diagram_nat_trans η X = {app := λ (W : (J.cover X)ᵒᵖ), 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)) _, naturality' := _}
J.diagram P
, as a functor in P
.
Equations
Instances for category_theory.grothendieck_topology.diagram_functor
The plus construction, associating a presheaf to any presheaf.
See plus_functor
below for a functorial version.
Equations
- J.plus_obj P = {obj := λ (X : Cᵒᵖ), category_theory.limits.colimit (J.diagram P (opposite.unop X)), map := λ (X Y : Cᵒᵖ) (f : X ⟶ Y), category_theory.limits.colim_map (J.diagram_pullback P f.unop) ≫ category_theory.limits.colimit.pre (J.diagram P (opposite.unop Y)) (J.pullback f.unop).op, map_id' := _, map_comp' := _}
An auxiliary definition used in plus
below.
Equations
- J.plus_map η = {app := λ (X : Cᵒᵖ), category_theory.limits.colim_map (J.diagram_nat_trans η (opposite.unop X)), naturality' := _}
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
- J.to_plus P = {app := λ (X : Cᵒᵖ), ⊤.to_multiequalizer P ≫ category_theory.limits.colimit.ι (J.diagram P (opposite.unop X)) (opposite.op ⊤), naturality' := _}
The natural transformation from the identity functor to plus
.
Equations
- J.to_plus_nat_trans D = {app := λ (P : Cᵒᵖ ⥤ D), J.to_plus P, naturality' := _}
(P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺
The natural isomorphism between P
and P⁺
when P
is a sheaf.
Equations
- J.iso_to_plus P hP = let _inst : category_theory.is_iso (J.to_plus P) := _ in category_theory.as_iso (J.to_plus P)
Lift a morphism P ⟶ Q
to P⁺ ⟶ Q
when Q
is a sheaf.