mathlib3 documentation

category_theory.sites.sheafification

Sheafification #

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

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

@[nolint]

A concrete version of the multiequalizer, to be used below.

Equations
Instances for category_theory.meq
@[ext]

Refine a term of meq P T with respect to a refinement S ⟶ T of covers.

Equations
@[simp]
theorem category_theory.meq.refine_apply {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [category_theory.concrete_category D] {X : C} {P : Cᵒᵖ D} {S T : J.cover X} (x : category_theory.meq P T) (e : S T) (I : S.arrow) :
(x.refine e) I = x {Y := I.Y, f := I.f, hf := _}

Pull back a term of meq P S with respect to a morphism f : Y ⟶ X in C.

Equations
@[simp]
theorem category_theory.meq.pullback_apply {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [category_theory.concrete_category D] {Y X : C} {P : Cᵒᵖ D} {S : J.cover X} (x : category_theory.meq P S) (f : Y X) (I : ((J.pullback f).obj S).arrow) :
(x.pullback f) I = x {Y := I.Y, f := I.f f, hf := _}

Make a term of meq P S.

Equations

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

The sheafification of a presheaf P. NOTE: Additional hypotheses are needed to obtain a proof that this is a sheaf!

Equations

The canonical map from P to its sheafification.

Equations

The canonical map on sheafifications induced by a morphism.

Equations

The sheafification of a presheaf P, as a functor. NOTE: Additional hypotheses are needed to obtain a proof that this is a sheaf!

Equations
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

Given a sheaf Q and a morphism P ⟶ Q, construct a morphism from J.sheafifcation P to Q.

Equations