Sheafification #
We construct the sheafification of a presheaf over a site C
with values in D
whenever
D
is a concrete category for which the forgetful functor preserves the appropriate (co)limits
and reflects isomorphisms.
We generally follow the approach of https://stacks.math.columbia.edu/tag/00W1
A concrete version of the multiequalizer, to be used below.
Equations
Instances for category_theory.meq
Equations
- category_theory.meq.has_coe_to_fun P S = {coe := λ (x : category_theory.meq P S), x.val}
Refine a term of meq P T
with respect to a refinement S ⟶ T
of covers.
Pull back a term of meq P S
with respect to a morphism f : Y ⟶ X
in C
.
Make a term of meq P S
.
The equivalence between the type associated to multiequalizer (S.index P)
and meq P S
.
Equations
Make a term of (J.plus_obj P).obj (op X)
from x : meq P S
.
Equations
- category_theory.grothendieck_topology.plus.mk x = ⇑(category_theory.limits.colimit.ι (J.diagram P X) (opposite.op S)) (⇑((category_theory.meq.equiv P S).symm) x)
P⁺
is always separated.
An auxiliary definition to be used in the proof of exists_of_sep
below.
Given a compatible family of local sections for P⁺
, and representatives of said sections,
construct a compatible family of local sections of P
over the combination of the covers
associated to the representatives.
The separatedness condition is used to prove compatibility among these local sections of P
.
Equations
- category_theory.grothendieck_topology.plus.meq_of_sep P hsep X S s T t ht = ⟨λ (I : (S.bind T).arrow), ⇑(t I.from_middle) I.to_middle, _⟩
If P
is separated, then P⁺
is a sheaf.
P⁺⁺
is always a sheaf.
The sheafification of a presheaf P
.
NOTE: Additional hypotheses are needed to obtain a proof that this is a sheaf!
The canonical map from P
to its sheafification.
The canonical map on sheafifications induced by a morphism.
Equations
- J.sheafify_map η = J.plus_map (J.plus_map η)
The sheafification of a presheaf P
, as a functor.
NOTE: Additional hypotheses are needed to obtain a proof that this is a sheaf!
Equations
- J.sheafification D = J.plus_functor D ⋙ J.plus_functor D
Instances for category_theory.grothendieck_topology.sheafification
The canonical map from P
to its sheafification, as a natural transformation.
Note: We only show this is a sheaf under additional hypotheses on D
.
Equations
- J.to_sheafification D = J.to_plus_nat_trans D ≫ category_theory.whisker_right (J.to_plus_nat_trans D) (J.plus_functor D)
If P
is a sheaf, then P
is isomorphic to J.sheafify P
.
Equations
- J.iso_sheafify hP = let _inst : category_theory.is_iso (J.to_sheafify P) := _ in category_theory.as_iso (J.to_sheafify P)
Given a sheaf Q
and a morphism P ⟶ Q
, construct a morphism from
J.sheafifcation P
to Q
.
Equations
- J.sheafify_lift η hQ = J.plus_lift (J.plus_lift η hQ) hQ
The sheafification functor, as a functor taking values in Sheaf
.
Equations
Instances for category_theory.presheaf_to_Sheaf
The sheafification functor is left adjoint to the forgetful functor.
Equations
- category_theory.sheafification_adjunction J D = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (P : Cᵒᵖ ⥤ D) (Q : category_theory.Sheaf J D), {to_fun := λ (e : (category_theory.presheaf_to_Sheaf J D).obj P ⟶ Q), J.to_sheafify P ≫ e.val, inv_fun := λ (e : P ⟶ (category_theory.Sheaf_to_presheaf J D).obj Q), {val := J.sheafify_lift e _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
Equations
- category_theory.Sheaf_to_presheaf_is_right_adjoint J D = {left := category_theory.presheaf_to_Sheaf J D _inst_8, adj := category_theory.sheafification_adjunction J D _inst_8}
A sheaf P
is isomorphic to its own sheafification.
Equations
- category_theory.sheafification_iso P = {hom := {val := (J.iso_sheafify _).hom}, inv := {val := (J.iso_sheafify _).inv}, hom_inv_id' := _, inv_hom_id' := _}