Sheaf conditions for presheaves of (continuous) functions.
We show that
Top.sheaf_condition.to_Type: not-necessarily-continuous functions into a type form a sheafTop.sheaf_condition.to_Types: in fact, these may be dependent functions into a type family
For
Top.sheaf_condition.to_Top: continuous functions into a topological space form a sheaf please seetopology/sheaves/local_predicate.lean, where we set up a general framework for constructing sub(pre)sheaves of the sheaf of dependent functions.
Future work
Obviously there's more to do:
- sections of a fiber bundle
- various classes of smooth and structure preserving functions
- functions into spaces with algebraic structure, which the sections inherit
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.
Equations
- Top.presheaf.to_Types X T = λ (ι : Type u) (U : ι → topological_space.opens ↥X), category_theory.limits.fork.is_limit.mk (Top.presheaf.sheaf_condition_equalizer_products.fork (X.presheaf_to_Types T) U) (λ (s : category_theory.limits.fork (Top.presheaf.sheaf_condition_equalizer_products.left_res (X.presheaf_to_Types T) U) (Top.presheaf.sheaf_condition_equalizer_products.right_res (X.presheaf_to_Types T) U)), id (λ (f : s.X), id (λ (x : ↥(opposite.unop (opposite.op (supr U)))), subtype.cases_on x (λ (x : ↥X) (mem : x ∈ has_coe_t_aux.coe (opposite.unop (opposite.op (supr U)))), id (λ (mem : x ∈ supr U), (λ (_x : x ∈ U (classical.some _)), (s.ι ≫ category_theory.limits.pi.π (λ (i : ι), (X.presheaf_to_Types T).obj (opposite.op (U i))) (classical.some _)) f ⟨x, _x⟩) _) mem)))) _ _
The presheaf of not-necessarily-continuous functions to
a target type T satsifies the sheaf condition.
Equations
- Top.presheaf.to_Type X T = Top.presheaf.to_Types X (λ (_x : ↥X), T)
The sheaf of not-necessarily-continuous functions on X with values in type family T : X → Type u.
Equations
- X.sheaf_to_Types T = {presheaf := X.presheaf_to_Types T, sheaf_condition := Top.presheaf.to_Types X T}
The sheaf of not-necessarily-continuous functions on X with values in a type T.
Equations
- X.sheaf_to_Type T = {presheaf := X.presheaf_to_Type T, sheaf_condition := Top.presheaf.to_Type X T}