# mathlibdocumentation

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.

@[simp]
theorem Top.presheaf.res_π_apply {X : Top} (F : Top.presheaf (Type u) X) {ι : Type u} (U : ι → ) (i : ι) (s : F.obj (opposite.op (supr U))) :
def Top.presheaf.is_compatible {X : Top} (F : Top.presheaf (Type u) X) {ι : Type u} (U : ι → ) (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
def Top.presheaf.pi_opens_iso_sections_family {X : Top} (F : Top.presheaf (Type u) X) {ι : Type u} (U : ι → ) :
Π (i : ι), F.obj (opposite.op (U i))

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

Equations
theorem Top.presheaf.compatible_iff_left_res_eq_right_res {X : Top} (F : Top.presheaf (Type u) X) {ι : Type u} (U : ι → )  :

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 : ι → ) (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]
theorem Top.presheaf.is_gluing_iff_eq_res {X : Top} (F : Top.presheaf (Type u) X) {ι : Type u} (U : ι → ) (s : F.obj (opposite.op (supr U))) :
F.is_gluing U .hom sf) s

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 : ι → ) (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 "equalizer" sheaf condition can be obtained from the sheaf condition in terms of unique gluings

Equations

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

Equations

The sheaf condition in terms of unique gluings is equivalent to the usual sheaf condition in terms of equalizer diagrams.

Equations
def Top.presheaf.sheaf_condition_of_exists_unique_gluing {X : Top} (F : Top.presheaf (Type u) X) (h : ∀ ⦃ι : Type u⦄ (U : ι → (sf : Π (i : ι), F.obj (opposite.op (U i))), 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 : ι → ) (sf : Π (i : ι), F.presheaf.obj (opposite.op (U i))) (h : sf) :
∃! (s : F.presheaf.obj (opposite.op (supr 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 : ι → ) (V : topological_space.opens X) (iUV : Π (i : ι), U i V) (hcover : V supr U) (sf : Π (i : ι), F.presheaf.obj (opposite.op (U i))) (h : 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 : ι → ) (s t : F.presheaf.obj (opposite.op (supr U))) (h : ∀ (i : ι), s = t) :
s = t
theorem Top.sheaf.eq_of_locally_eq' {X : Top} (F : Top.sheaf (Type u) X) {ι : Type u} (U : ι → ) (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.