TopCat.LocalPredicate.locality
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, ∃ (_ : ↑x ∈ V), ∃ i, self.pred fun x => f ((fun x => ⟨↑x, ⋯⟩) x)) → self.pred f
This theorem, `TopCat.LocalPredicate.locality`, states that a local predicate is indeed local in the context of the category of topological spaces (`TopCat`). Specifically, for any topological space `X` and any predicate `T` mapping points in `X` to some type `v`, if for every point `x` in an open set `U` of `X` we can find a neighborhood `V` of `x` such that `T` holds for all points in `V`, then `T` holds for all points in `U`. In other words, if a property is locally satisfied at every point in a region, it is satisfied across the whole region.
More concisely: If a local predicate holding in an open set of a topological space is satisfied at every point, then it holds for all points in that open set.
|
TopCat.stalkToFiber_injective
theorem TopCat.stalkToFiber_injective :
∀ {X : TopCat} {T : ↑X → Type v} (P : TopCat.LocalPredicate T) (x : ↑X),
(∀ (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 iU iV, ∀ (w : ↥W.obj), fU ((fun x_4 => ⟨↑x_4, ⋯⟩) w) = fV ((fun x_4 => ⟨↑x_4, ⋯⟩) w)) →
Function.Injective (TopCat.stalkToFiber P x)
The theorem `TopCat.stalkToFiber_injective` states that for any topological space `X` and a local predicate `P` on a type dependent on `X`, at any point `x` in the space, the function `stalkToFiber` (which maps from the stalk to the original fiber) is injective if for any two sections, if they agree at `x`, then they must also agree on some open neighborhood of `x`. This injectivity property encapsulates the intuition that 'local information determines global behavior' in the context of sheaves on topological spaces. Notice that the sections (functions `fU` and `fV`) themselves are required to satisfy the local predicate `P.pred`. The injectivity is defined in the sense that if `f(x) = g(x)` for two functions `f` and `g`, then `f = g`.
More concisely: Given a topological space X and a local predicate P, the function stalkToFiber is injective on sections satisfying P if they agree at any point x, they also agree on some open neighborhood of x.
|
TopCat.subpresheafToTypes.isSheaf
theorem TopCat.subpresheafToTypes.isSheaf :
∀ {X : TopCat} {T : ↑X → Type v} (P : TopCat.LocalPredicate T),
(TopCat.subpresheafToTypes P.toPrelocalPredicate).IsSheaf
This theorem states that for any topological space `X` and any type-valued function `T` on `X`, if `P` is a local predicate on `T`, then the subpresheaf of dependent functions on `X` satisfying the "pre-local" predicate `P` satisfies the sheaf condition. In other words, locally defined and locally agreeable data (according to the predicate `P`) can be uniquely glued together to give global data. This is a fundamental property of sheaves in topology.
More concisely: Given a topological space X and a type-valued function T on X, if local predicate P on T satisfies the sheaf condition, then the subpresheaf of dependent functions on X with values in T satisfying P is a sheaf.
|
TopCat.PrelocalPredicate.res
theorem TopCat.PrelocalPredicate.res :
∀ {X : TopCat} {T : ↑X → Type v} (self : TopCat.PrelocalPredicate T) {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V)
(f : (x : ↥V) → T ↑x), self.pred f → self.pred fun x => f ((fun x => ⟨↑x, ⋯⟩) x)
This theorem states that for any topological space `X` and a function `T` applied to points in `X`, if a prelocal predicate `self` holds for a function `f` over an open subset `V` of `X`, then `self` also holds for the restriction of `f` to a smaller open subset `U` of `X`, where `U` is a subset of `V`. Here, the restriction of `f` to `U` is represented by the function `fun x => f ((fun x => ⟨↑x, ⋯⟩) x)`, and `i : U ⟶ V` represents the inclusion of `U` in `V`. This theorem essentially captures the idea that the truth of the predicate does not change when `f` is restricted to a smaller domain.
More concisely: If a prelocal predicate holds for a function on an open subset of a topological space, then it also holds for the restriction of that function to any smaller open subset included in the larger one.
|
TopCat.stalkToFiber_surjective
theorem TopCat.stalkToFiber_surjective :
∀ {X : TopCat} {T : ↑X → Type v} (P : TopCat.LocalPredicate T) (x : ↑X),
(∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t) → Function.Surjective (TopCat.stalkToFiber P x)
The theorem `TopCat.stalkToFiber_surjective` states that for every topological space `X` and a type function `T` mapped from the points in `X`, and for every local predicate `P` and point `x` within `X`, the `stalkToFiber` map is surjective at point `x` if, and only if, every point in the fiber `T x` has an allowed section passing through it. In other words, for every target in the fiber `T x`, there exists a path such that the value of the path at `x` is the target. This is equivalent to saying that every point in the fiber `T x` can be reached by the `stalkToFiber` map from the stalk at `x`.
More concisely: The `stalkToFiber` map is surjective at a point `x` in a topological space `X` with type function `T` if and only if every point in the fiber `T x` has a local section passing through it.
|