Functions satisfying a local predicate form a sheaf. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
At this stage, in topology/sheaves/sheaf_of_functions.lean
we've proved that not-necessarily-continuous functions from a topological space
into some type (or type family) form a sheaf.
Why do the continuous functions form a sheaf? The point is just that continuity is a local condition, so one can use the lifting condition for functions to provide a candidate lift, then verify that the lift is actually continuous by using the factorisation condition for the lift (which guarantees that on each open set it agrees with the functions being lifted, which were assumed to be continuous).
This file abstracts this argument to work for any collection of dependent functions on a topological space satisfying a "local predicate".
As an application, we check that continuity is a local predicate in this sense, and provide
Top.sheaf_to_Top: continuous functions into a topological space form a sheaf
A sheaf constructed in this way has a natural map stalk_to_fiber from the stalks
to the types in the ambient type family.
We give conditions sufficient to show that this map is injective and/or surjective.
- pred : Π {U : topological_space.opens ↥X}, (Π (x : ↥U), T ↑x) → Prop
- res : ∀ {U V : topological_space.opens ↥X} (i : U ⟶ V) (f : Π (x : ↥V), T ↑x), self.pred f → self.pred (λ (x : ↥U), f (⇑i x))
Given a topological space X : Top and a type family T : X → Type,
a P : prelocal_predicate T consists of:
- a family of predicates
P.pred, one for eachU : opens X, of the form(Π x : U, T x) → Prop - a proof that if
f : Π x : V, T xsatisfies the predicate onV : opens X, then the restriction offto any open subsetUalso satisfies the predicate.
Instances for Top.prelocal_predicate
- Top.prelocal_predicate.has_sizeof_inst
- Top.inhabited_prelocal_predicate
Continuity is a "prelocal" predicate on functions to a fixed topological space T.
Equations
- X.continuous_prelocal T = {pred := λ (U : topological_space.opens ↥X) (f : ↥U → ↥T), continuous f, res := _}
Satisfying the inhabited linter.
Equations
- X.inhabited_prelocal_predicate T = {default := X.continuous_prelocal T}
- to_prelocal_predicate : Top.prelocal_predicate T
- locality : ∀ {U : topological_space.opens ↥X} (f : Π (x : ↥U), T ↑x), (∀ (x : ↥U), ∃ (V : topological_space.opens ↥X) (m : x.val ∈ V) (i : V ⟶ U), self.to_prelocal_predicate.pred (λ (x : ↥V), f (⇑i x))) → self.to_prelocal_predicate.pred f
Given a topological space X : Top and a type family T : X → Type,
a P : local_predicate T consists of:
- a family of predicates
P.pred, one for eachU : opens X, of the form(Π x : U, T x) → Prop - a proof that if
f : Π x : V, T xsatisfies the predicate onV : opens X, then the restriction offto any open subsetUalso satisfies the predicate, and - a proof that given some
f : Π x : U, T x, if for everyx : Uwe can find an open setx ∈ V ≤ Uso that the restriction offtoVsatisfies the predicate, thenfitself satisfies the predicate.
Instances for Top.local_predicate
- Top.local_predicate.has_sizeof_inst
- Top.inhabited_local_predicate
Continuity is a "local" predicate on functions to a fixed topological space T.
Equations
- X.continuous_local T = {to_prelocal_predicate := {pred := (X.continuous_prelocal T).pred, res := _}, locality := _}
Satisfying the inhabited linter.
Equations
- X.inhabited_local_predicate T = {default := X.continuous_local T}
Given a P : prelocal_predicate, we can always construct a local_predicate
by asking that the condition from P holds locally near every point.
The subpresheaf of dependent functions on X satisfying the "pre-local" predicate P.
The natural transformation including the subpresheaf of functions satisfying a local predicate into the presheaf of all functions.
Equations
- Top.subpresheaf_to_Types.subtype P = {app := λ (U : (topological_space.opens ↥X)ᵒᵖ) (f : (Top.subpresheaf_to_Types P).obj U), f.val, naturality' := _}
The functions satisfying a local predicate satisfy the sheaf condition.
The subsheaf of the sheaf of all dependently typed functions satisfying the local predicate P.
Equations
- Top.subsheaf_to_Types P = {val := Top.subpresheaf_to_Types P.to_prelocal_predicate, cond := _}
There is a canonical map from the stalk to the original fiber, given by evaluating sections.
Equations
- Top.stalk_to_fiber P x = category_theory.limits.colimit.desc (((category_theory.whiskering_left (topological_space.open_nhds x)ᵒᵖ (topological_space.opens ↥X)ᵒᵖ (Type v)).obj (topological_space.open_nhds.inclusion x).op).obj (Top.subsheaf_to_Types P).presheaf) {X := T x, ι := {app := λ (U : (topological_space.open_nhds x)ᵒᵖ) (f : (((category_theory.whiskering_left (topological_space.open_nhds x)ᵒᵖ (topological_space.opens ↥X)ᵒᵖ (Type v)).obj (topological_space.open_nhds.inclusion x).op).obj (Top.subsheaf_to_Types P).presheaf).obj U), f.val ⟨x, _⟩, naturality' := _}}
The stalk_to_fiber map is surjective at x if
every point in the fiber T x has an allowed section passing through it.
The stalk_to_fiber map is injective at x if any two allowed sections which agree at x
agree on some neighborhood of x.
Some repackaging:
the presheaf of functions satisfying continuous_prelocal is just the same thing as
the presheaf of continuous functions.
Equations
- T.subpresheaf_continuous_prelocal_iso_presheaf_to_Top = category_theory.nat_iso.of_components (λ (X_1 : (topological_space.opens ↥X)ᵒᵖ), {hom := id (λ (ᾰ : (Top.subpresheaf_to_Types (X.continuous_prelocal T)).obj X_1), subtype.cases_on ᾰ (λ (f : Π (x : ↥(opposite.unop X_1)), (λ (x : ↥X), ↥T) ↑x) (c : (X.continuous_prelocal T).pred f), {to_fun := f, continuous_to_fun := c})), inv := id (λ (ᾰ : (X.presheaf_to_Top T).obj X_1), continuous_map.cases_on ᾰ (λ (f : ↥(opposite.unop ((topological_space.opens.to_Top X).op.obj X_1)) → ↥T) (c : continuous f . "continuity'"), ⟨f, c⟩)), hom_inv_id' := _, inv_hom_id' := _}) _
The sheaf of continuous functions on X with values in a space T.
Equations
- T.sheaf_to_Top = {val := X.presheaf_to_Top T, cond := _}