mathlib3 documentation

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 #

source
@[protected, instance]
def Top.of.charted_space {H : Type u_1} [topological_space H] (M : Type u) [topological_space M] [charted_space H M] :
charted_space H ↥(Top.of M)
Equations
source
@[protected, instance]
def Top.of.has_groupoid {H : Type u_1} [topological_space H] {G : structure_groupoid H} (M : Type u) [topological_space M] [charted_space H M] [has_groupoid M G] :
has_groupoid ↥(Top.of M) G
source
def structure_groupoid.local_invariant_prop.local_predicate {H : Type u_1} [topological_space H] {H' : Type u_2} [topological_space H'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H') → set H → H → Prop} (M : Type u) [topological_space M] [charted_space H M] (M' : Type u) [topological_space M'] [charted_space H' M'] (hG : G.local_invariant_prop G' 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
source
def structure_groupoid.local_invariant_prop.sheaf {H : Type u_1} [topological_space H] {H' : Type u_2} [topological_space H'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H') → set H → H → Prop} (M : Type u) [topological_space M] [charted_space H M] (M' : Type u) [topological_space M'] [charted_space H' M'] (hG : G.local_invariant_prop G' P) :
Top.sheaf (Type u) (Top.of 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 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
source
@[protected, instance]
def structure_groupoid.local_invariant_prop.sheaf_has_coe_to_fun {H : Type u_1} [topological_space H] {H' : Type u_2} [topological_space H'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H') → set H → H → Prop} (M : Type u) [topological_space M] [charted_space H M] (M' : Type u) [topological_space M'] [charted_space H' M'] (hG : G.local_invariant_prop G' P) (U : (topological_space.opens ↥(Top.of M))ᵒᵖ) :
has_coe_to_fun ((structure_groupoid.local_invariant_prop.sheaf M M' hG).val.obj U) (λ (_x : (structure_groupoid.local_invariant_prop.sheaf M M' hG).val.obj U), ↥(opposite.unop U) → M')
Equations
source
theorem structure_groupoid.local_invariant_prop.section_spec {H : Type u_1} [topological_space H] {H' : Type u_2} [topological_space H'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H') → set H → H → Prop} (M : Type u) [topological_space M] [charted_space H M] (M' : Type u) [topological_space M'] [charted_space H' M'] (hG : G.local_invariant_prop G' P) (U : (topological_space.opens ↥(Top.of M))ᵒᵖ) (f : (structure_groupoid.local_invariant_prop.sheaf M M' hG).val.obj U) :
charted_space.lift_prop P ⇑f