mathlib documentation

topology.sheaves.sheaf_condition.unique_gluing

The sheaf condition for a type-valued presheaf #

We provide an alternative formulation of the sheaf condition for type-valued presheaves.

A presheaf F : presheaf (Type u) X satisfies the sheaf condition if and only if, for every compatible family of sections sf : Π i : ι, F.obj (op (U i)), there exists a unique gluing s : F.obj (op (supr U)).

Here, the family sf is called compatible, if for all i j : ι, the restrictions of sf i and sf j to U i ⊓ U j agree. A section s : F.obj (op (supr U)) is a gluing for the family sf, if s restricts to sf i on U i for all i : ι

We show that the sheaf condition in terms of unique gluings is equivalent to the definition in terms of equalizers.

def Top.presheaf.is_compatible {X : Top} (F : Top.presheaf (Type u) X) {ι : Type u} (U : ι → topological_space.opens X) (sf : Π (i : ι), F.obj (opposite.op (U i))) :
Prop

A family of sections sf is compatible, if the restrictions of sf i and sf j to U i ⊓ U j agree, for all i and j

Equations

For presheaves of types, terms of pi_opens F U are just families of sections

Equations

Under the isomorphism pi_opens_iso_sections_family, compatibility of sections is the same as being equalized by the arrows left_res and right_res of the equalizer diagram.

def Top.presheaf.is_gluing {X : Top} (F : Top.presheaf (Type u) X) {ι : Type u} (U : ι → topological_space.opens X) (sf : Π (i : ι), F.obj (opposite.op (U i))) (s : F.obj (opposite.op (supr U))) :
Prop

A section s is a gluing for a family of sections sf if it restricts to sf i on U i, for all i

Equations
@[simp]

Under the isomorphism pi_opens_iso_sections_family, being a gluing of a family of sections sf is the same as lying in the preimage of res (the leftmost arrow of the equalizer diagram).

@[nolint]
def Top.presheaf.gluing {X : Top} (F : Top.presheaf (Type u) X) {ι : Type u} (U : ι → topological_space.opens X) (sf : Π (i : ι), F.obj (opposite.op (U i))) :
Type u

The subtype of all gluings for a given family of sections

Equations
@[nolint]
def Top.presheaf.sheaf_condition_unique_gluing {X : Top} (F : Top.presheaf (Type u) X) :
Type (u+1)

The sheaf condition of type-valued presheaves in terms of unique gluings. A presheaf F : presheaf (Type u) X satisfies this sheaf condition if and only if, for every compatible family of sections sf : Π i : ι, F.obj (op (U i)), there exists a unique gluing s : F.obj (op (supr U)).

We prove this to be equivalent to the usual one below in sheaf_condition_equiv_sheaf_condition_unique_gluing

Equations

The sheaf condition in terms of unique gluings can be obtained from the usual "equalizer" sheaf condition

Equations
def Top.presheaf.sheaf_condition_of_exists_unique_gluing {X : Top} (F : Top.presheaf (Type u) X) (h : ∀ ⦃ι : Type u⦄ (U : ι → topological_space.opens X) (sf : Π (i : ι), F.obj (opposite.op (U i))), F.is_compatible U sf(∃! (s : F.obj (opposite.op (supr U))), F.is_gluing U sf s)) :

A slightly more convenient way of obtaining the sheaf condition for type-valued sheaves

Equations
theorem Top.sheaf.exists_unique_gluing {X : Top} (F : Top.sheaf (Type u) X) {ι : Type u} (U : ι → topological_space.opens X) (sf : Π (i : ι), F.presheaf.obj (opposite.op (U i))) (h : F.presheaf.is_compatible U sf) :
∃! (s : F.presheaf.obj (opposite.op (supr U))), F.presheaf.is_gluing U sf s

A more convenient way of obtaining a unique gluing of sections for a sheaf

theorem Top.sheaf.exists_unique_gluing' {X : Top} (F : Top.sheaf (Type u) X) {ι : Type u} (U : ι → topological_space.opens X) (V : topological_space.opens X) (iUV : Π (i : ι), U i V) (hcover : V supr U) (sf : Π (i : ι), F.presheaf.obj (opposite.op (U i))) (h : F.presheaf.is_compatible U sf) :
∃! (s : F.presheaf.obj (opposite.op V)), ∀ (i : ι), F.presheaf.map (iUV i).op s = sf i

In this version of the lemma, the inclusion homs iUV can be specified directly by the user, which can be more convenient in practice.

@[ext]
theorem Top.sheaf.eq_of_locally_eq {X : Top} (F : Top.sheaf (Type u) X) {ι : Type u} (U : ι → topological_space.opens X) (s t : F.presheaf.obj (opposite.op (supr U))) (h : ∀ (i : ι), F.presheaf.map (topological_space.opens.le_supr U i).op s = F.presheaf.map (topological_space.opens.le_supr U i).op t) :
s = t
theorem Top.sheaf.eq_of_locally_eq' {X : Top} (F : Top.sheaf (Type u) X) {ι : Type u} (U : ι → topological_space.opens X) (V : topological_space.opens X) (iUV : Π (i : ι), U i V) (hcover : V supr U) (s t : F.presheaf.obj (opposite.op V)) (h : ∀ (i : ι), F.presheaf.map (iUV i).op s = F.presheaf.map (iUV i).op t) :
s = t

In this version of the lemma, the inclusion homs iUV can be specified directly by the user, which can be more convenient in practice.