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

• StructureGroupoid.LocalInvariantProp.localPredicate: the TopCat.LocalPredicate (in the sheaf-theoretic sense) on functions from open subsets of M into M', which states whether such functions satisfy LiftProp P.
• StructureGroupoid.LocalInvariantProp.sheaf: the sheaf-of-types of functions f : M → M' which satisfy the lifted property LiftProp P.

instance TopCat.of.chartedSpace {H : Type u_1} [TopologicalSpace H] (M : Type u) [TopologicalSpace M] [ChartedSpace H M] : ChartedSpace H ↑(of M)

Equations

• TopCat.of.chartedSpace M = inferInstance

instance TopCat.of.hasGroupoid {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] [HasGroupoid M G] : HasGroupoid (↑(of M)) G

def StructureGroupoid.LocalInvariantProp.localPredicate {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (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

• StructureGroupoid.LocalInvariantProp.localPredicate M M' hG = { pred := fun {U : TopologicalSpace.Opens ↑(TopCat.of M)} (f : ↥U → M') => ChartedSpace.LiftProp P f, res := ⋯, locality := ⋯ }

def StructureGroupoid.LocalInvariantProp.sheaf {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u) [TopologicalSpace M'] [ChartedSpace H' M'] (hG : G.LocalInvariantProp G' P) : TopCat.Sheaf (Type u) (TopCat.of 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 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

• StructureGroupoid.LocalInvariantProp.sheaf M M' hG = TopCat.subsheafToTypes (StructureGroupoid.LocalInvariantProp.localPredicate M M' hG)

instance StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (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 ((sheaf M M' hG).val.obj U) fun (x : (sheaf M M' hG).val.obj U) => ↥(Opposite.unop U) → M'

Equations

• StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun M M' hG U = { coe := fun (a : (StructureGroupoid.LocalInvariantProp.sheaf M M' hG).val.obj U) => ↑a }

theorem StructureGroupoid.LocalInvariantProp.section_spec {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (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 : (sheaf M M' hG).val.obj U) : ChartedSpace.LiftProp P ↑f