Functions satisfying a local predicate form a sheaf.

At this stage, in Mathlib/Topology/Sheaves/SheafOfFunctions.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

• TopCat.sheafToTop: continuous functions into a topological space form a sheaf

A sheaf constructed in this way has a natural map stalkToFiber 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 TopCat.PrelocalPredicate {X : TopCat} (T : ↑X → Type v) : Type v

Given a topological space X : TopCat and a type family T : X → Type, a P : PrelocalPredicate 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.

• pred : {U : TopologicalSpace.Opens ↑X} → ((x : ↥U) → T ↑x) → Prop

  The underlying predicate of a prelocal predicate

• res : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (f : (x : ↥V) → T ↑x), self.pred f → self.pred fun (x : ↥U) => f ((fun (x : ↥U) => ⟨↑x, ⋯⟩) x)

  The underlying predicate should be invariant under restriction

theorem TopCat.PrelocalPredicate.res {X : TopCat} {T : ↑X → Type v} (self : TopCat.PrelocalPredicate T) {U : TopologicalSpace.Opens ↑X} {V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (f : (x : ↥V) → T ↑x) : self.pred f → self.pred fun (x : ↥U) => f ((fun (x : ↥U) => ⟨↑x, ⋯⟩) x)

The underlying predicate should be invariant under restriction

def TopCat.continuousPrelocal (X : TopCat) (T : TopCat) : TopCat.PrelocalPredicate fun (x : ↑X) => ↑T

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

Equations

• X.continuousPrelocal T = { pred := fun {x : TopologicalSpace.Opens ↑X} (f : ↥x → ↑T) => Continuous f, res := ⋯ }

@[simp]

theorem TopCat.continuousPrelocal_pred (X : TopCat) (T : TopCat) : ∀ {x : TopologicalSpace.Opens ↑X} (f : ↥x → ↑T), (X.continuousPrelocal T).pred f = Continuous f

instance TopCat.inhabitedPrelocalPredicate (X : TopCat) (T : TopCat) : Inhabited (TopCat.PrelocalPredicate fun (x : ↑X) => ↑T)

Satisfying the inhabited linter.

Equations

• X.inhabitedPrelocalPredicate T = { default := X.continuousPrelocal T }

structure TopCat.LocalPredicate {X : TopCat} (T : ↑X → Type v) extends TopCat.PrelocalPredicate : Type v

Given a topological space X : TopCat and a type family T : X → Type, a P : LocalPredicate 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.

• pred : {U : TopologicalSpace.Opens ↑X} → ((x : ↥U) → T ↑x) → Prop
• res : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (f : (x : ↥V) → T ↑x), self.pred f → self.pred fun (x : ↥U) => f ((fun (x : ↥U) => ⟨↑x, ⋯⟩) x)
• locality : ∀ {U : TopologicalSpace.Opens ↑X} (f : (x : ↥U) → T ↑x), (∀ (x : ↥U), ∃ (V : TopologicalSpace.Opens ↑X) (_ : ↑x ∈ V) (i : V ⟶ U), self.pred fun (x : ↥V) => f ((fun (x : ↥V) => ⟨↑x, ⋯⟩) x)) → self.pred f

  A local predicate must be local --- provided that it is locally satisfied, it is also globally satisfied

theorem TopCat.LocalPredicate.locality {X : TopCat} {T : ↑X → Type v} (self : TopCat.LocalPredicate T) {U : TopologicalSpace.Opens ↑X} (f : (x : ↥U) → T ↑x) : (∀ (x : ↥U), ∃ (V : TopologicalSpace.Opens ↑X) (_ : ↑x ∈ V) (i : V ⟶ U), self.pred fun (x : ↥V) => f ((fun (x : ↥V) => ⟨↑x, ⋯⟩) x)) → self.pred f

A local predicate must be local --- provided that it is locally satisfied, it is also globally satisfied

def TopCat.continuousLocal (X : TopCat) (T : TopCat) : TopCat.LocalPredicate fun (x : ↑X) => ↑T

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

Equations

• X.continuousLocal T = { toPrelocalPredicate := X.continuousPrelocal T, locality := ⋯ }

instance TopCat.inhabitedLocalPredicate (X : TopCat) (T : TopCat) : Inhabited (TopCat.LocalPredicate fun (x : ↑X) => ↑T)

Satisfying the inhabited linter.

Equations

• X.inhabitedLocalPredicate T = { default := X.continuousLocal T }

def TopCat.PrelocalPredicate.sheafify {X : TopCat} {T : ↑X → Type v} (P : TopCat.PrelocalPredicate T) : TopCat.LocalPredicate T

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

Equations

• One or more equations did not get rendered due to their size.

theorem TopCat.PrelocalPredicate.sheafifyOf {X : TopCat} {T : ↑X → Type v} {P : TopCat.PrelocalPredicate T} {U : TopologicalSpace.Opens ↑X} {f : (x : ↥U) → T ↑x} (h : P.pred f) : P.sheafify.pred f

def TopCat.subpresheafToTypes {X : TopCat} {T : ↑X → Type v} (P : TopCat.PrelocalPredicate T) : TopCat.Presheaf (Type v) X

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopCat.subpresheafToTypes_map_coe {X : TopCat} {T : ↑X → Type v} (P : TopCat.PrelocalPredicate T) : ∀ {x x_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : x ⟶ x_1) (f : { f : (x_2 : ↥(Opposite.unop x)) → T ↑x_2 // P.pred f }) (x_2 : ↥(Opposite.unop x_1)), ↑((TopCat.subpresheafToTypes P).map i f) x_2 = ↑f ⟨↑x_2, ⋯⟩

@[simp]

theorem TopCat.subpresheafToTypes_obj {X : TopCat} {T : ↑X → Type v} (P : TopCat.PrelocalPredicate T) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (TopCat.subpresheafToTypes P).obj U = { f : (x : ↥(Opposite.unop U)) → T ↑x // P.pred f }

def TopCat.subpresheafToTypes.subtype {X : TopCat} {T : ↑X → Type v} (P : TopCat.PrelocalPredicate T) : TopCat.subpresheafToTypes P ⟶ X.presheafToTypes T

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

Equations

• TopCat.subpresheafToTypes.subtype P = { app := fun (x : (TopologicalSpace.Opens ↑X)ᵒᵖ) (f : (TopCat.subpresheafToTypes P).obj x) => ↑f, naturality := ⋯ }

theorem TopCat.subpresheafToTypes.isSheaf {X : TopCat} {T : ↑X → Type v} (P : TopCat.LocalPredicate T) : (TopCat.subpresheafToTypes P.toPrelocalPredicate).IsSheaf

The functions satisfying a local predicate satisfy the sheaf condition.

def TopCat.subsheafToTypes {X : TopCat} {T : ↑X → Type v} (P : TopCat.LocalPredicate T) : TopCat.Sheaf (Type v) X

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

Equations

• TopCat.subsheafToTypes P = { val := TopCat.subpresheafToTypes P.toPrelocalPredicate, cond := ⋯ }

@[simp]

theorem TopCat.subsheafToTypes_val {X : TopCat} {T : ↑X → Type v} (P : TopCat.LocalPredicate T) : (TopCat.subsheafToTypes P).val = TopCat.subpresheafToTypes P.toPrelocalPredicate

def TopCat.stalkToFiber {X : TopCat} {T : ↑X → Type v} (P : TopCat.LocalPredicate T) (x : ↑X) : (TopCat.subsheafToTypes P).presheaf.stalk x ⟶ T x

There is a canonical map from the stalk to the original fiber, given by evaluating sections.

Equations

• One or more equations did not get rendered due to their size.

theorem TopCat.stalkToFiber_germ {X : TopCat} {T : ↑X → Type v} (P : TopCat.LocalPredicate T) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : (TopCat.subsheafToTypes P).presheaf.obj (Opposite.op U)) : TopCat.stalkToFiber P x ((TopCat.subsheafToTypes P).presheaf.germ U x hx f) = ↑f ⟨x, hx⟩

theorem TopCat.stalkToFiber_surjective {X : TopCat} {T : ↑X → Type v} (P : TopCat.LocalPredicate T) (x : ↑X) (w : ∀ (t : T x), ∃ (U : TopologicalSpace.OpenNhds x) (f : (y : ↥U.obj) → T ↑y) (_ : P.pred f), f ⟨x, ⋯⟩ = t) : Function.Surjective (TopCat.stalkToFiber P x)

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

theorem TopCat.stalkToFiber_injective {X : TopCat} {T : ↑X → Type v} (P : TopCat.LocalPredicate T) (x : ↑X) (w : ∀ (U V : TopologicalSpace.OpenNhds x) (fU : (y : ↥U.obj) → T ↑y), P.pred fU → ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ (W : TopologicalSpace.OpenNhds x) (iU : W ⟶ U) (iV : W ⟶ V), ∀ (w : ↥W.obj), fU ((fun (x_4 : ↥W.obj) => ⟨↑x_4, ⋯⟩) w) = fV ((fun (x_4 : ↥W.obj) => ⟨↑x_4, ⋯⟩) w)) : Function.Injective (TopCat.stalkToFiber P x)

The stalkToFiber map is injective at x if any two allowed sections which agree at x agree on some neighborhood of x.

def TopCat.subpresheafContinuousPrelocalIsoPresheafToTop {X : TopCat} (T : TopCat) : TopCat.subpresheafToTypes (X.continuousPrelocal T) ≅ X.presheafToTop T

Some repackaging: the presheaf of functions satisfying continuousPrelocal is just the same thing as the presheaf of continuous functions.

Equations

• One or more equations did not get rendered due to their size.

def TopCat.sheafToTop {X : TopCat} (T : TopCat) : TopCat.Sheaf (Type v) X

The sheaf of continuous functions on X with values in a space T.

Equations

• TopCat.sheafToTop T = { val := X.presheafToTop T, cond := ⋯ }