mathlib3documentation

geometry.manifold.sheaf.basic

Generic construction of a sheaf from a local_invariant_prop on a manifold #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file constructs the sheaf-of-types of functions f : M → M' (for charted spaces M, M') which satisfy the lifted property lift_prop P associated to some locally invariant (in the sense of structure_groupoid.local_invariant_prop) property P on the model spaces of M and M'. For example, differentiability and smoothness are locally invariant properties in this sense, so this construction can be used to construct the sheaf of differentiable functions on a manifold and the sheaf of smooth functions on a manifold.

The mathematical work is in associating a Top.local_predicate to a structure_groupoid.local_invariant_prop: that is, showing that a differential-geometric "locally invariant" property is preserved under restriction and gluing.

Main definitions #

• structure_groupoid.local_invariant_prop.local_predicate: the Top.local_predicate (in the sheaf-theoretic sense) on functions from open subsets of M into M', which states whether such functions satisfy lift_prop P.
• structure_groupoid.local_invariant_prop.sheaf: the sheaf-of-types of functions f : M → M' which satisfy the lifted property lift_prop P.
@[protected, instance]
def Top.of.charted_space {H : Type u_1} (M : Type u) [ M] :
Equations
@[protected, instance]
def Top.of.has_groupoid {H : Type u_1} {G : structure_groupoid H} (M : Type u) [ M] [ G] :
G
def structure_groupoid.local_invariant_prop.local_predicate {H : Type u_1} {H' : Type u_2} {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H H') set H H Prop} (M : Type u) [ M] (M' : Type u) [ M'] (hG : P) :
Top.local_predicate (λ (x : (Top.of M)), M')

Let P be a local_invariant_prop for functions between spaces with the groupoids G, G' and let M, M' be charted spaces modelled on the model spaces of those groupoids. Then there is an induced local_predicate on the functions from M to M', given by lift_prop P.

Equations
def structure_groupoid.local_invariant_prop.sheaf {H : Type u_1} {H' : Type u_2} {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H H') set H H Prop} (M : Type u) [ M] (M' : Type u) [ M'] (hG : P) :

Let P be a local_invariant_prop for functions between spaces with the groupoids G, G' and let M, M' be charted spaces modelled on the model spaces of those groupoids. Then there is a sheaf of types on M which, to each open set U in M, associates the type of bundled functions from U to M' satisfying the lift of P.

Equations
@[protected, instance]
def structure_groupoid.local_invariant_prop.sheaf_has_coe_to_fun {H : Type u_1} {H' : Type u_2} {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H H') set H H Prop} (M : Type u) [ M] (M' : Type u) [ M'] (hG : P) (U : ᵒᵖ) :
(λ (_x : U), M')
Equations
theorem structure_groupoid.local_invariant_prop.section_spec {H : Type u_1} {H' : Type u_2} {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H H') set H H Prop} (M : Type u) [ M] (M' : Type u) [ M'] (hG : P) (U : ᵒᵖ) (f : U) :