mathlib documentation

topology.sheaves.local_predicate

Functions satisfying a local predicate form a sheaf.

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

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.

structure Top.prelocal_predicate {X : Top} :
(X → Type v)Type v

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 each U : opens X, of the form (Π x : U, T x) → Prop
  • a proof that if f : Π x : V, T x satisfies the predicate on V : opens X, then the restriction of f to any open subset U also satisfies the predicate.

Continuity is a "prelocal" predicate on functions to a fixed topological space T.

Equations
@[instance]

Satisfying the inhabited linter.

Equations
structure Top.local_predicate {X : Top} :
(X → Type v)Type v

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 each U : opens X, of the form (Π x : U, T x) → Prop
  • a proof that if f : Π x : V, T x satisfies the predicate on V : opens X, then the restriction of f to any open subset U also satisfies the predicate, and
  • a proof that given some f : Π x : U, T x, if for every x : U we can find an open set x ∈ V ≤ U so that the restriction of f to V satisfies the predicate, then f itself satisfies the predicate.
def Top.continuous_local (X T : Top) :

Continuity is a "local" predicate on functions to a fixed topological space T.

Equations
@[instance]

Satisfying the inhabited linter.

Equations

Given a P : prelocal_predicate, we can always construct a local_predicate by asking that the condition from P holds locally near every point.

Equations
theorem Top.prelocal_predicate.sheafify_of {X : Top} {T : X → Type v} {P : Top.prelocal_predicate T} {U : topological_space.opens X} {f : Π (x : U), T x} :

@[simp]
theorem Top.subpresheaf_to_Types_map_val {X : Top} {T : X → Type v} (P : Top.prelocal_predicate T) (U V : (topological_space.opens X)ᵒᵖ) (i : U V) (f : {f // P.pred f}) (x : (opposite.unop V)) :

def Top.subpresheaf_to_Types {X : Top} {T : X → Type v} :

The subpresheaf of dependent functions on X satisfying the "pre-local" predicate P.

Equations
@[simp]
theorem Top.subpresheaf_to_Types_obj {X : Top} {T : X → Type v} (P : Top.prelocal_predicate T) (U : (topological_space.opens X)ᵒᵖ) :

The natural transformation including the subpresheaf of functions satisfying a local predicate into the presheaf of all functions.

Equations

The natural transformation from the sheaf condition diagram for functions satisfying a local predicate to the sheaf condition diagram for arbitrary functions, given by forgetting that the local predicate holds.

Equations
def Top.subsheaf_to_Types {X : Top} {T : X → Type v} :

The subsheaf of the sheaf of all dependently typed functions satisfying the local predicate P.

Equations
theorem Top.stalk_to_fiber_surjective {X : Top} {T : X → Type v} (P : Top.local_predicate T) (x : X) :
(∀ (t : T x), ∃ (U : topological_space.open_nhds x) (f : Π (y : (U.val)), T y) (h : P.to_prelocal_predicate.pred f), f x, _⟩ = t)function.surjective (Top.stalk_to_fiber P x)

The stalk_to_fiber map is surjective at x if every point in the fiber T x has an allowed section passing through it.

theorem Top.stalk_to_fiber_injective {X : Top} {T : X → Type v} (P : Top.local_predicate T) (x : X) :
(∀ (U V : topological_space.open_nhds x) (fU : Π (y : (U.val)), T y), P.to_prelocal_predicate.pred fU∀ (fV : Π (y : (V.val)), T y), P.to_prelocal_predicate.pred fVfU x, _⟩ = fV x, _⟩(∃ (W : topological_space.open_nhds x) (iU : W U) (iV : W V), ∀ (w : (W.val)), fU (iU w) = fV (iV w)))function.injective (Top.stalk_to_fiber P x)

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