Documentation

Mathlib.Geometry.Manifold.Sheaf.Basic

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

This file constructs the sheaf-of-types of functions f : M → M' (for charted spaces M, M') which satisfy the lifted property LiftProp P associated to some locally invariant (in the sense of StructureGroupoid.LocalInvariantProp) 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 TopCat.LocalPredicate to a StructureGroupoid.LocalInvariantProp: that is, showing that a differential-geometric "locally invariant" property is preserved under restriction and gluing.

Main definitions #

Equations
Equations
  • =
def StructureGroupoid.LocalInvariantProp.localPredicate {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (HH')Set HHProp} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u) [TopologicalSpace M'] [ChartedSpace H' M'] (hG : G.LocalInvariantProp G' P) :
TopCat.LocalPredicate fun (x : (TopCat.of M)) => M'

Let P be a LocalInvariantProp 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 LocalPredicate on the functions from M to M', given by LiftProp P.

Equations
Instances For
    def StructureGroupoid.LocalInvariantProp.sheaf {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (HH')Set HHProp} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u) [TopologicalSpace M'] [ChartedSpace H' M'] (hG : G.LocalInvariantProp G' P) :

    Let P be a LocalInvariantProp 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
    Instances For
      instance StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (HH')Set HHProp} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u) [TopologicalSpace M'] [ChartedSpace H' M'] (hG : G.LocalInvariantProp G' P) (U : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ) :
      CoeFun ((StructureGroupoid.LocalInvariantProp.sheaf M M' hG).val.obj U) fun (x : (StructureGroupoid.LocalInvariantProp.sheaf M M' hG).val.obj U) => (Opposite.unop U)M'
      Equations
      theorem StructureGroupoid.LocalInvariantProp.section_spec {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (HH')Set HHProp} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u) [TopologicalSpace M'] [ChartedSpace H' M'] (hG : G.LocalInvariantProp G' P) (U : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ) (f : (StructureGroupoid.LocalInvariantProp.sheaf M M' hG).val.obj U) :