mathlib documentation

geometry.manifold.local_invariant_properties

Local properties invariant under a groupoid

We study properties of a triple (g, s, x) where g is a function between two spaces H and H', s is a subset of H and x is a point of H. Our goal is to register how such a property should behave to make sense in charted spaces modelled on H and H'.

The main examples we have in mind are the properties "g is differentiable at x within s", or "g is smooth at x within s". We want to develop general results that, when applied in these specific situations, say that the notion of smooth function in a manifold behaves well under restriction, intersection, is local, and so on.

Main definitions

Given hG : local_invariant_prop G G' P, we deduce many properties of the lifted property on the charted spaces. For instance, hG.lift_prop_within_at_inter says that P g s x is equivalent to P g (s ∩ t) x whenever t is a neighborhood of x.

Implementation notes

We do not use dot notation for properties of the lifted property. For instance, we have hG.lift_prop_within_at_congr saying that if lift_prop_within_at P g s x holds, and g and g' coincide on s, then lift_prop_within_at P g' s x holds. We can't call it lift_prop_within_at.congr as it is in the namespace associated to local_invariant_prop, not in the one for lift_prop_within_at.

structure structure_groupoid.local_invariant_prop {H : Type u_1} [topological_space H] {H' : Type u_3} [topological_space H'] :
structure_groupoid Hstructure_groupoid H'((H → H')set HH → Prop) → Prop

Structure recording good behavior of a property of a triple (f, s, x) where f is a function, s a set and x a point. Good behavior here means locality and invariance under given groupoids (both in the source and in the target). Given such a good behavior, the lift of this property to charted spaces admitting these groupoids will inherit the good behavior.

def charted_space.lift_prop_within_at {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] :
((H → H')set HH → Prop)(M → M')set MM → Prop

Given a property of germs of functions and sets in the model space, then one defines a corresponding property in a charted space, by requiring that it holds at the preferred chart at this point. (When the property is local and invariant, it will in fact hold using any chart, see lift_prop_within_at_indep_chart). We require continuity in the lifted property, as otherwise one single chart might fail to capture the behavior of the function.

Equations
def charted_space.lift_prop_on {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] :
((H → H')set HH → Prop)(M → M')set M → Prop

Given a property of germs of functions and sets in the model space, then one defines a corresponding property of functions on sets in a charted space, by requiring that it holds around each point of the set, in the preferred charts.

Equations
def charted_space.lift_prop_at {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] :
((H → H')set HH → Prop)(M → M')M → Prop

Given a property of germs of functions and sets in the model space, then one defines a corresponding property of a function at a point in a charted space, by requiring that it holds in the preferred chart.

Equations
def charted_space.lift_prop {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] :
((H → H')set HH → Prop)(M → M') → Prop

Given a property of germs of functions and sets in the model space, then one defines a corresponding property of a function in a charted space, by requiring that it holds in the preferred chart around every point.

Equations
theorem structure_groupoid.lift_prop_within_at_univ {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {P : (H → H')set HH → Prop} {g : M → M'} {x : M} :

theorem structure_groupoid.lift_prop_on_univ {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {P : (H → H')set HH → Prop} {g : M → M'} :

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_indep_chart_aux {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {e e' : local_homeomorph M H} {f f' : local_homeomorph M' H'} {P : (H → H')set HH → Prop} {g : M → M'} {s : set M} {x : M} :

If a property of a germ of function g on a pointed set (s, x) is invariant under the structure groupoid (by composition in the source space and in the target space), then expressing it in charted spaces does not depend on the element of the maximal atlas one uses both in the source and in the target manifolds, provided they are defined around x and g x respectively, and provided g is continuous within s at x (otherwise, the local behavior of g at x can not be captured with a chart in the target).

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_indep_chart {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {e : local_homeomorph M H} {f : local_homeomorph M' H'} {P : (H → H')set HH → Prop} {g : M → M'} {s : set M} {x : M} (hG : G.local_invariant_prop G' P) [has_groupoid M G] [has_groupoid M' G'] :

theorem structure_groupoid.local_invariant_prop.lift_prop_on_indep_chart {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {e : local_homeomorph M H} {f : local_homeomorph M' H'} {P : (H → H')set HH → Prop} {g : M → M'} {s : set M} (hG : G.local_invariant_prop G' P) [has_groupoid M G] [has_groupoid M' G'] (he : e structure_groupoid.maximal_atlas M G) (hf : f structure_groupoid.maximal_atlas M' G') (h : lift_prop_on P g s) (y : H) :

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_inter' {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g : M → M'} {s t : set M} {x : M} :

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_inter {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g : M → M'} {s t : set M} {x : M} :

theorem structure_groupoid.local_invariant_prop.lift_prop_at_of_lift_prop_within_at {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g : M → M'} {s : set M} {x : M} :
G.local_invariant_prop G' Plift_prop_within_at P g s xs 𝓝 xlift_prop_at P g x

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_of_lift_prop_at_of_mem_nhds {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g : M → M'} {s : set M} {x : M} :
G.local_invariant_prop G' Plift_prop_at P g xs 𝓝 xlift_prop_within_at P g s x

theorem structure_groupoid.local_invariant_prop.lift_prop_on_of_locally_lift_prop_on {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g : M → M'} {s : set M} :
G.local_invariant_prop G' P(∀ (x : M), x s(∃ (u : set M), is_open u x u lift_prop_on P g (s u)))lift_prop_on P g s

theorem structure_groupoid.local_invariant_prop.lift_prop_of_locally_lift_prop_on {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g : M → M'} :
G.local_invariant_prop G' P(∀ (x : M), ∃ (u : set M), is_open u x u lift_prop_on P g u)lift_prop P g

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_congr {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g g' : M → M'} {s : set M} {x : M} :
G.local_invariant_prop G' Plift_prop_within_at P g s x(∀ (y : M), y sg' y = g y)g' x = g xlift_prop_within_at P g' s x

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_congr_iff {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g g' : M → M'} {s : set M} {x : M} :
G.local_invariant_prop G' P(∀ (y : M), y sg' y = g y)g' x = g x(lift_prop_within_at P g' s x lift_prop_within_at P g s x)

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_congr_of_eventually_eq {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g g' : M → M'} {s : set M} {x : M} :
G.local_invariant_prop G' Plift_prop_within_at P g s xg' =ᶠ[𝓝[s] x] gg' x = g xlift_prop_within_at P g' s x

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_congr_iff_of_eventually_eq {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g g' : M → M'} {s : set M} {x : M} :
G.local_invariant_prop G' Pg' =ᶠ[𝓝[s] x] gg' x = g x(lift_prop_within_at P g' s x lift_prop_within_at P g s x)

theorem structure_groupoid.local_invariant_prop.lift_prop_at_congr_of_eventually_eq {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g g' : M → M'} {x : M} :
G.local_invariant_prop G' Plift_prop_at P g xg' =ᶠ[𝓝 x] glift_prop_at P g' x

theorem structure_groupoid.local_invariant_prop.lift_prop_at_congr_iff_of_eventually_eq {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g g' : M → M'} {x : M} :
G.local_invariant_prop G' Pg' =ᶠ[𝓝 x] g(lift_prop_at P g' x lift_prop_at P g x)

theorem structure_groupoid.local_invariant_prop.lift_prop_on_congr {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g g' : M → M'} {s : set M} :
G.local_invariant_prop G' Plift_prop_on P g s(∀ (y : M), y sg' y = g y)lift_prop_on P g' s

theorem structure_groupoid.local_invariant_prop.lift_prop_on_congr_iff {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {G : structure_groupoid H} {G' : structure_groupoid H'} {P : (H → H')set HH → Prop} {g g' : M → M'} {s : set M} :
G.local_invariant_prop G' P(∀ (y : M), y sg' y = g y)(lift_prop_on P g' s lift_prop_on P g s)

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_mono {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {P : (H → H')set HH → Prop} {g : M → M'} {s t : set M} {x : M} :
(∀ ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H → H'⦄, t sP f s xP f t x)lift_prop_within_at P g t xs tlift_prop_within_at P g s x

theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_of_lift_prop_at {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {P : (H → H')set HH → Prop} {g : M → M'} {s : set M} {x : M} :
(∀ ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H → H'⦄, t sP f s xP f t x)lift_prop_at P g xlift_prop_within_at P g s x

theorem structure_groupoid.local_invariant_prop.lift_prop_on_mono {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {P : (H → H')set HH → Prop} {g : M → M'} {s t : set M} :
(∀ ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H → H'⦄, t sP f s xP f t x)lift_prop_on P g ts tlift_prop_on P g s

theorem structure_groupoid.local_invariant_prop.lift_prop_on_of_lift_prop {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {H' : Type u_3} {M' : Type u_4} [topological_space H'] [topological_space M'] [charted_space H' M'] {P : (H → H')set HH → Prop} {g : M → M'} {s : set M} :
(∀ ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H → H'⦄, t sP f s xP f t x)lift_prop P glift_prop_on P g s

theorem structure_groupoid.local_invariant_prop.lift_prop_at_of_mem_maximal_atlas {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {G : structure_groupoid H} {e : local_homeomorph M H} {x : M} {Q : (H → H)set HH → Prop} [has_groupoid M G] :

theorem structure_groupoid.local_invariant_prop.lift_prop_at_symm_of_mem_maximal_atlas {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {G : structure_groupoid H} {e : local_homeomorph M H} {Q : (H → H)set HH → Prop} [has_groupoid M G] {x : H} :

theorem structure_groupoid.local_invariant_prop.lift_prop_at_chart {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {G : structure_groupoid H} {x : M} {Q : (H → H)set HH → Prop} [has_groupoid M G] :
G.local_invariant_prop G Q(∀ (y : H), Q id set.univ y)lift_prop_at Q (chart_at H x) x

theorem structure_groupoid.local_invariant_prop.lift_prop_on_chart {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {G : structure_groupoid H} {x : M} {Q : (H → H)set HH → Prop} [has_groupoid M G] :
G.local_invariant_prop G Q(∀ (y : H), Q id set.univ y)lift_prop_on Q (chart_at H x) (chart_at H x).to_local_equiv.source

theorem structure_groupoid.local_invariant_prop.lift_prop_at_chart_symm {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {G : structure_groupoid H} {x : M} {Q : (H → H)set HH → Prop} [has_groupoid M G] :
G.local_invariant_prop G Q(∀ (y : H), Q id set.univ y)lift_prop_at Q ((chart_at H x).symm) ((chart_at H x) x)

theorem structure_groupoid.local_invariant_prop.lift_prop_on_chart_symm {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {G : structure_groupoid H} {x : M} {Q : (H → H)set HH → Prop} [has_groupoid M G] :
G.local_invariant_prop G Q(∀ (y : H), Q id set.univ y)lift_prop_on Q ((chart_at H x).symm) (chart_at H x).to_local_equiv.target

theorem structure_groupoid.local_invariant_prop.lift_prop_id {H : Type u_1} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {G : structure_groupoid H} {Q : (H → H)set HH → Prop} :
G.local_invariant_prop G Q(∀ (y : H), Q id set.univ y)lift_prop Q id

def structure_groupoid.is_local_structomorph_within_at {H : Type u_1} [topological_space H] :
structure_groupoid H(H → H)set HH → Prop

A function from a model space H to itself is a local structomorphism, with respect to a structure groupoid G for H, relative to a set s in H, if for all points x in the set, the function agrees with a G-structomorphism on s in a neighbourhood of x.

Equations

For a groupoid G which is closed_under_restriction, being a local structomorphism is a local invariant property.