English
For any topological space X and any family T: X → Type, the presheaf that assigns to an open U the set of all sections U → T(x) (with x varying in U) is a sheaf.
Русский
Для любого пространства X и любой семейства T: X → Type, предперешаф, который присваивает каждому открытому U множество всех функций, локально задающих значения в T(x), удовлетворяет условию локальности-склейки.
LaTeX
$$$\text{IsSheaf}(\text{presheafToTypes } X T)$.$$
Lean4
/-- We show that the presheaf of functions to a type `T`
(no continuity assumptions, just plain functions)
form a sheaf.
In fact, the proof is identical when we do this for dependent functions to a type family `T`,
so we do the more general case.
-/
theorem toTypes_isSheaf (T : X → Type*) : (presheafToTypes X T).IsSheaf :=
isSheaf_of_isSheafUniqueGluing_types _ fun ι U sf hsf => by
-- We use the sheaf condition in terms of unique gluing
-- U is a family of open sets, indexed by `ι` and `sf` is a compatible family of sections.
-- In the informal comments below, I'll just write `U` to represent the union.
-- Our first goal is to define a function "lifted" to all of `U`.
-- We do this one point at a time. Using the axiom of choice, we can pick for each
-- `x : ↑(iSup U)` an index `i : ι` such that `x` lies in `U i`
choose index index_spec using fun x : ↑(iSup U) =>
Opens.mem_iSup.mp
x.2
-- Using this data, we can glue our functions together to a single section
let s : ∀ x : ↑(iSup U), T x := fun x => sf (index x) ⟨x.1, index_spec x⟩
refine ⟨s, ?_, ?_⟩
· intro i
funext x
exact congr_fun (hsf (index ⟨x, _⟩) i) ⟨x, ⟨index_spec ⟨x.1, _⟩, x.2⟩⟩
· -- Now we just need to check that the lift we picked was the only possible one.
-- So we suppose we had some other gluing `t` of our sections
intro t ht
funext x
exact
congr_fun (ht (index x))
⟨x.1, index_spec x⟩
-- We verify that the non-dependent version is an immediate consequence:
