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 familyTop.sheaf_condition.to_Top: continuous functions into a topological space form a sheaf
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.sheaf_condition.to_Types X T = λ (ι : Type u) (U : ι → topological_space.opens ↥X), category_theory.limits.fork.is_limit.mk (Top.sheaf_condition.fork (X.presheaf_to_Types T) U) (λ (s : category_theory.limits.fork (Top.sheaf_condition.left_res (X.presheaf_to_Types T) U) (Top.sheaf_condition.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.sheaf_condition.to_Type X T = Top.sheaf_condition.to_Types X (λ (_x : ↥X), T)
Next we to check the sheaf condition for continuous functions.
The idea, of course, is to first lift to the underlying function, using the fact that the presheaf of functions is a sheaf. Because continuous functions are determined by their underlying functions, this takes care of our factorisation and uniqueness obligations in the sheaf condition.
To show continuity, we already know that our lifted function restricted to any U i is the
original continuous function we had here,
and since continuity is a local condition we should be done!
In fact, I'd like to do it for any "functions satisfying a local condition", for which there's a sketch at https://github.com/leanprover-community/mathlib/issues/1462
The natural transformation from the sheaf condition diagram for continuous functions to the sheaf condition diagram for arbitrary functions, given by forgetting continuity everywhere.
Equations
- Top.sheaf_condition.forget_continuity X T U = {app := λ (X_1 : category_theory.limits.walking_parallel_pair), X_1.cases_on (category_theory.limits.pi.map (λ (i : ι) (f : (X.presheaf_to_Top T).obj (opposite.op (U i))), f.to_fun)) (category_theory.limits.pi.map (λ (p : ι × ι) (f : (X.presheaf_to_Top T).obj (opposite.op (U p.fst ⊓ U p.snd))), f.to_fun)), naturality' := _}
The presheaf of continuous functions to a target topological space T satsifies the sheaf condition.
Equations
- Top.sheaf_condition.to_Top X T = λ (ι : Type u) (U : ι → topological_space.opens ↥X), category_theory.limits.fork.is_limit.mk (Top.sheaf_condition.fork (X.presheaf_to_Top T) U) (λ (s : category_theory.limits.fork (Top.sheaf_condition.left_res (X.presheaf_to_Top T) U) (Top.sheaf_condition.right_res (X.presheaf_to_Top T) U)), id (λ (f : s.X), {to_fun := let s' : category_theory.limits.cone (Top.sheaf_condition.diagram (X.presheaf_to_Type ↥T) U) := (category_theory.limits.cones.postcompose (Top.sheaf_condition.forget_continuity X T U)).obj s in (Top.sheaf_condition.to_Type X ↥T U).lift s' f, continuous_to_fun := _})) _ _