Local properties invariant under a groupoid #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
local_invariant_prop G G' Psays that a propertyPof a triple(g, s, x)is local, and invariant under composition by elements of the groupoidsGandG'ofHandH'respectively.charted_space.lift_prop_within_at(resp.lift_prop_at,lift_prop_onandlift_prop): given a propertyPof(g, s, x)whereg : H → H', define the corresponding property for functionsM → M'whereMandM'are charted spaces modelled respectively onHandH'. We define these properties within a set at a point, or at a point, or on a set, or in the whole space. This lifting process (obtained by restricting to suitable chart domains) can always be done, but it only behaves well under locality and invariance assumptions.
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}
{H' : Type u_3}
[topological_space H]
[topological_space H']
(G : structure_groupoid H)
(G' : structure_groupoid H')
(P : (H → H') → set H → H → Prop) :
Prop
- is_local : ∀ {s : set H} {x : H} {u : set H} {f : H → H'}, is_open u → x ∈ u → (P f s x ↔ P f (s ∩ u) x)
- right_invariance' : ∀ {s : set H} {x : H} {f : H → H'} {e : local_homeomorph H H}, e ∈ G → x ∈ e.to_local_equiv.source → P f s x → P (f ∘ ⇑(e.symm)) (⇑(e.symm) ⁻¹' s) (⇑e x)
- congr_of_forall : ∀ {s : set H} {x : H} {f g : H → H'}, (∀ (y : H), y ∈ s → f y = g y) → f x = g x → P f s x → P g s x
- left_invariance' : ∀ {s : set H} {x : H} {f : H → H'} {e' : local_homeomorph H' H'}, e' ∈ G' → s ⊆ f ⁻¹' e'.to_local_equiv.source → f x ∈ e'.to_local_equiv.source → P f s x → P (⇑e' ∘ f) s x
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.
theorem
structure_groupoid.local_invariant_prop.congr_set
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{s t : set H}
{x : H}
{f : H → H'}
(hu : s =ᶠ[nhds x] t) :
P f s x ↔ P f t x
theorem
structure_groupoid.local_invariant_prop.is_local_nhds
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{s u : set H}
{x : H}
{f : H → H'}
(hu : u ∈ nhds_within x s) :
theorem
structure_groupoid.local_invariant_prop.congr_iff_nhds_within
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{s : set H}
{x : H}
{f g : H → H'}
(h1 : f =ᶠ[nhds_within x s] g)
(h2 : f x = g x) :
P f s x ↔ P g s x
theorem
structure_groupoid.local_invariant_prop.congr_nhds_within
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{s : set H}
{x : H}
{f g : H → H'}
(h1 : f =ᶠ[nhds_within x s] g)
(h2 : f x = g x)
(hP : P f s x) :
P g s x
theorem
structure_groupoid.local_invariant_prop.congr_nhds_within'
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{s : set H}
{x : H}
{f g : H → H'}
(h1 : f =ᶠ[nhds_within x s] g)
(h2 : f x = g x)
(hP : P g s x) :
P f s x
theorem
structure_groupoid.local_invariant_prop.congr_iff
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{s : set H}
{x : H}
{f g : H → H'}
(h : f =ᶠ[nhds x] g) :
P f s x ↔ P g s x
theorem
structure_groupoid.local_invariant_prop.congr
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{s : set H}
{x : H}
{f g : H → H'}
(h : f =ᶠ[nhds x] g)
(hP : P f s x) :
P g s x
theorem
structure_groupoid.local_invariant_prop.congr'
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{s : set H}
{x : H}
{f g : H → H'}
(h : f =ᶠ[nhds x] g)
(hP : P g s x) :
P f s x
theorem
structure_groupoid.local_invariant_prop.left_invariance
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{s : set H}
{x : H}
{f : H → H'}
{e' : local_homeomorph H' H'}
(he' : e' ∈ G')
(hfs : continuous_within_at f s x)
(hxe' : f x ∈ e'.to_local_equiv.source) :
theorem
structure_groupoid.local_invariant_prop.right_invariance
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{s : set H}
{x : H}
{f : H → H'}
{e : local_homeomorph H H}
(he : e ∈ G)
(hxe : x ∈ e.to_local_equiv.source) :
def
charted_space.lift_prop_within_at
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
(P : (H → H') → set H → H → Prop)
(f : M → M')
(s : set M)
(x : M) :
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
- charted_space.lift_prop_within_at P f s x = (continuous_within_at f s x ∧ P (⇑(charted_space.chart_at H' (f x)) ∘ f ∘ ⇑((charted_space.chart_at H x).symm)) (⇑((charted_space.chart_at H x).symm) ⁻¹' s) (⇑(charted_space.chart_at H x) x))
def
charted_space.lift_prop_on
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
(P : (H → H') → set H → H → Prop)
(f : M → M')
(s : 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
- charted_space.lift_prop_on P f s = ∀ (x : M), x ∈ s → charted_space.lift_prop_within_at P f s x
def
charted_space.lift_prop_at
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
(P : (H → H') → set H → H → Prop)
(f : M → M')
(x : 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
theorem
charted_space.lift_prop_at_iff
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{P : (H → H') → set H → H → Prop}
{f : M → M'}
{x : M} :
charted_space.lift_prop_at P f x ↔ continuous_at f x ∧ P (⇑(charted_space.chart_at H' (f x)) ∘ f ∘ ⇑((charted_space.chart_at H x).symm)) set.univ (⇑(charted_space.chart_at H x) x)
def
charted_space.lift_prop
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
(P : (H → H') → set H → H → Prop)
(f : 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
- charted_space.lift_prop P f = ∀ (x : M), charted_space.lift_prop_at P f x
theorem
charted_space.lift_prop_iff
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{P : (H → H') → set H → H → Prop}
{f : M → M'} :
charted_space.lift_prop P f ↔ continuous f ∧ ∀ (x : M), P (⇑(charted_space.chart_at H' (f x)) ∘ f ∘ ⇑((charted_space.chart_at H x).symm)) set.univ (⇑(charted_space.chart_at H x) x)
theorem
structure_groupoid.lift_prop_within_at_univ
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{x : M} :
theorem
structure_groupoid.lift_prop_on_univ
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{P : (H → H') → set H → H → Prop}
{g : M → M'} :
theorem
structure_groupoid.lift_prop_within_at_self
{H : Type u_1}
{H' : Type u_3}
[topological_space H]
[topological_space H']
{P : (H → H') → set H → H → Prop}
{f : H → H'}
{s : set H}
{x : H} :
charted_space.lift_prop_within_at P f s x ↔ continuous_within_at f s x ∧ P f s x
theorem
structure_groupoid.lift_prop_within_at_self_source
{H : Type u_1}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space H']
[topological_space M']
[charted_space H' M']
{P : (H → H') → set H → H → Prop}
{f : H → M'}
{s : set H}
{x : H} :
charted_space.lift_prop_within_at P f s x ↔ continuous_within_at f s x ∧ P (⇑(charted_space.chart_at H' (f x)) ∘ f) s x
theorem
structure_groupoid.lift_prop_within_at_self_target
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
{P : (H → H') → set H → H → Prop}
{s : set M}
{x : M}
{f : M → H'} :
charted_space.lift_prop_within_at P f s x ↔ continuous_within_at f s x ∧ P (f ∘ ⇑((charted_space.chart_at H x).symm)) (⇑((charted_space.chart_at H x).symm) ⁻¹' s) (⇑(charted_space.chart_at H x) x)
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_iff
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
{f : M → M'} :
charted_space.lift_prop_within_at P f s x ↔ continuous_within_at f s x ∧ P (⇑(charted_space.chart_at H' (f x)) ∘ f ∘ ⇑((charted_space.chart_at H x).symm)) ((charted_space.chart_at H x).to_local_equiv.target ∩ ⇑((charted_space.chart_at H x).symm) ⁻¹' (s ∩ f ⁻¹' (charted_space.chart_at H' (f x)).to_local_equiv.source)) (⇑(charted_space.chart_at H x) x)
lift_prop_within_at P f s x is equivalent to a definition where we restrict the set we are
considering to the domain of the charts at x and f x.
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_indep_chart_source_aux
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{e e' : local_homeomorph M H}
{P : (H → H') → set H → H → Prop}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
(g : M → H')
(he : e ∈ structure_groupoid.maximal_atlas M G)
(xe : x ∈ e.to_local_equiv.source)
(he' : e' ∈ structure_groupoid.maximal_atlas M G)
(xe' : x ∈ e'.to_local_equiv.source) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_indep_chart_target_aux2
{H : Type u_1}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{f f' : local_homeomorph M' H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
(g : H → M')
{x : H}
{s : set H}
(hf : f ∈ structure_groupoid.maximal_atlas M' G')
(xf : g x ∈ f.to_local_equiv.source)
(hf' : f' ∈ structure_groupoid.maximal_atlas M' G')
(xf' : g x ∈ f'.to_local_equiv.source)
(hgs : continuous_within_at g s x) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_indep_chart_target_aux
{H : Type u_1}
{H' : Type u_3}
{M' : Type u_4}
{X : Type u_5}
[topological_space H]
[topological_space H']
[topological_space M']
[charted_space H' M']
[topological_space X]
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{f f' : local_homeomorph M' H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{g : X → M'}
{e : local_homeomorph X H}
{x : X}
{s : set X}
(xe : x ∈ e.to_local_equiv.source)
(hf : f ∈ structure_groupoid.maximal_atlas M' G')
(xf : g x ∈ f.to_local_equiv.source)
(hf' : f' ∈ structure_groupoid.maximal_atlas M' G')
(xf' : g x ∈ f'.to_local_equiv.source)
(hgs : continuous_within_at g s x) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_indep_chart_aux
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[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 H → H → Prop}
{g : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
(he : e ∈ structure_groupoid.maximal_atlas M G)
(xe : x ∈ e.to_local_equiv.source)
(he' : e' ∈ structure_groupoid.maximal_atlas M G)
(xe' : x ∈ e'.to_local_equiv.source)
(hf : f ∈ structure_groupoid.maximal_atlas M' G')
(xf : g x ∈ f.to_local_equiv.source)
(hf' : f' ∈ structure_groupoid.maximal_atlas M' G')
(xf' : g x ∈ f'.to_local_equiv.source)
(hgs : continuous_within_at g s x) :
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}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[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 H → H → Prop}
{g : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
[has_groupoid M G]
[has_groupoid M' G']
(he : e ∈ structure_groupoid.maximal_atlas M G)
(xe : x ∈ e.to_local_equiv.source)
(hf : f ∈ structure_groupoid.maximal_atlas M' G')
(xf : g x ∈ f.to_local_equiv.source) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_indep_chart_source
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{e : local_homeomorph M H}
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
[has_groupoid M G]
(he : e ∈ structure_groupoid.maximal_atlas M G)
(xe : x ∈ e.to_local_equiv.source) :
charted_space.lift_prop_within_at P g s x ↔ charted_space.lift_prop_within_at P (g ∘ ⇑(e.symm)) (⇑(e.symm) ⁻¹' s) (⇑e x)
A version of lift_prop_within_at_indep_chart, only for the source.
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_indep_chart_target
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{f : local_homeomorph M' H'}
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
[has_groupoid M' G']
(hf : f ∈ structure_groupoid.maximal_atlas M' G')
(xf : g x ∈ f.to_local_equiv.source) :
charted_space.lift_prop_within_at P g s x ↔ continuous_within_at g s x ∧ charted_space.lift_prop_within_at P (⇑f ∘ g) s x
A version of lift_prop_within_at_indep_chart, only for the target.
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_indep_chart'
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[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 H → H → Prop}
{g : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
[has_groupoid M G]
[has_groupoid M' G']
(he : e ∈ structure_groupoid.maximal_atlas M G)
(xe : x ∈ e.to_local_equiv.source)
(hf : f ∈ structure_groupoid.maximal_atlas M' G')
(xf : g x ∈ f.to_local_equiv.source) :
charted_space.lift_prop_within_at P g s x ↔ continuous_within_at g s x ∧ charted_space.lift_prop_within_at P (⇑f ∘ g ∘ ⇑(e.symm)) (⇑(e.symm) ⁻¹' s) (⇑e x)
A version of lift_prop_within_at_indep_chart, that uses lift_prop_within_at on both sides.
theorem
structure_groupoid.local_invariant_prop.lift_prop_on_indep_chart
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[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 H → H → 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 : charted_space.lift_prop_on P g s)
{y : H}
(hy : y ∈ e.to_local_equiv.target ∩ ⇑(e.symm) ⁻¹' (s ∩ g ⁻¹' f.to_local_equiv.source)) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_inter'
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s t : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
(ht : t ∈ nhds_within x s) :
charted_space.lift_prop_within_at P g (s ∩ t) x ↔ charted_space.lift_prop_within_at P g s x
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_inter
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s t : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
(ht : t ∈ nhds x) :
charted_space.lift_prop_within_at P g (s ∩ t) x ↔ charted_space.lift_prop_within_at P g s x
theorem
structure_groupoid.local_invariant_prop.lift_prop_at_of_lift_prop_within_at
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
(h : charted_space.lift_prop_within_at P g s x)
(hs : s ∈ nhds 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}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
(h : charted_space.lift_prop_at P g x)
(hs : s ∈ nhds x) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_on_of_locally_lift_prop_on
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s : set M}
(hG : G.local_invariant_prop G' P)
(h : ∀ (x : M), x ∈ s → (∃ (u : set M), is_open u ∧ x ∈ u ∧ charted_space.lift_prop_on P g (s ∩ u))) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_of_locally_lift_prop_on
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g : M → M'}
(hG : G.local_invariant_prop G' P)
(h : ∀ (x : M), ∃ (u : set M), is_open u ∧ x ∈ u ∧ charted_space.lift_prop_on P g u) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_congr_of_eventually_eq
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g g' : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
(h : charted_space.lift_prop_within_at P g s x)
(h₁ : g' =ᶠ[nhds_within x s] g)
(hx : g' x = g x) :
charted_space.lift_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}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g g' : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
(h₁ : g' =ᶠ[nhds_within x s] g)
(hx : g' x = g x) :
charted_space.lift_prop_within_at P g' s x ↔ charted_space.lift_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}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g g' : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
(h₁ : ∀ (y : M), y ∈ s → g' y = g y)
(hx : g' x = g x) :
charted_space.lift_prop_within_at P g' s x ↔ charted_space.lift_prop_within_at P g s x
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_congr
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g g' : M → M'}
{s : set M}
{x : M}
(hG : G.local_invariant_prop G' P)
(h : charted_space.lift_prop_within_at P g s x)
(h₁ : ∀ (y : M), y ∈ s → g' y = g y)
(hx : g' x = g x) :
charted_space.lift_prop_within_at P g' s x
theorem
structure_groupoid.local_invariant_prop.lift_prop_at_congr_iff_of_eventually_eq
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g g' : M → M'}
{x : M}
(hG : G.local_invariant_prop G' P)
(h₁ : g' =ᶠ[nhds x] g) :
charted_space.lift_prop_at P g' x ↔ charted_space.lift_prop_at P g x
theorem
structure_groupoid.local_invariant_prop.lift_prop_at_congr_of_eventually_eq
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g g' : M → M'}
{x : M}
(hG : G.local_invariant_prop G' P)
(h : charted_space.lift_prop_at P g x)
(h₁ : g' =ᶠ[nhds x] g) :
charted_space.lift_prop_at P g' x
theorem
structure_groupoid.local_invariant_prop.lift_prop_on_congr
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g g' : M → M'}
{s : set M}
(hG : G.local_invariant_prop G' P)
(h : charted_space.lift_prop_on P g s)
(h₁ : ∀ (y : M), y ∈ s → g' y = g y) :
charted_space.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}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
{g g' : M → M'}
{s : set M}
(hG : G.local_invariant_prop G' P)
(h₁ : ∀ (y : M), y ∈ s → g' y = g y) :
charted_space.lift_prop_on P g' s ↔ charted_space.lift_prop_on P g s
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_mono_of_mem
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s t : set M}
{x : M}
(mono_of_mem : ∀ ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H → H'⦄, s ∈ nhds_within x t → P f s x → P f t x)
(h : charted_space.lift_prop_within_at P g s x)
(hst : s ∈ nhds_within x t) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_mono
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s t : set M}
{x : M}
(mono : ∀ ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x)
(h : charted_space.lift_prop_within_at P g s x)
(hts : t ⊆ s) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_within_at_of_lift_prop_at
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s : set M}
{x : M}
(mono : ∀ ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x)
(h : charted_space.lift_prop_at P g x) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_on_mono
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s t : set M}
(mono : ∀ ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x)
(h : charted_space.lift_prop_on P g t)
(hst : s ⊆ t) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_on_of_lift_prop
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{P : (H → H') → set H → H → Prop}
{g : M → M'}
{s : set M}
(mono : ∀ ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x)
(h : charted_space.lift_prop P g) :
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 H → H → Prop}
[has_groupoid M G]
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y)
(he : e ∈ structure_groupoid.maximal_atlas M G)
(hx : x ∈ e.to_local_equiv.source) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_on_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 H → H → Prop}
[has_groupoid M G]
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y)
(he : e ∈ structure_groupoid.maximal_atlas 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 H → H → Prop}
[has_groupoid M G]
{x : H}
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y)
(he : e ∈ structure_groupoid.maximal_atlas M G)
(hx : x ∈ e.to_local_equiv.target) :
charted_space.lift_prop_at Q ⇑(e.symm) x
theorem
structure_groupoid.local_invariant_prop.lift_prop_on_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 H → H → Prop}
[has_groupoid M G]
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y)
(he : e ∈ structure_groupoid.maximal_atlas M G) :
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 H → H → Prop}
[has_groupoid M G]
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y) :
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 H → H → Prop}
[has_groupoid M G]
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y) :
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 H → H → Prop}
[has_groupoid M G]
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y) :
charted_space.lift_prop_at Q ⇑((charted_space.chart_at H x).symm) (⇑(charted_space.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 H → H → Prop}
[has_groupoid M G]
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_at_of_mem_groupoid
{H : Type u_1}
[topological_space H]
{G : structure_groupoid H}
{Q : (H → H) → set H → H → Prop}
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y)
{f : local_homeomorph H H}
(hf : f ∈ G)
{x : H}
(hx : x ∈ f.to_local_equiv.source) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_on_of_mem_groupoid
{H : Type u_1}
[topological_space H]
{G : structure_groupoid H}
{Q : (H → H) → set H → H → Prop}
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y)
{f : local_homeomorph H H}
(hf : f ∈ G) :
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 H → H → Prop}
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y) :
theorem
structure_groupoid.local_invariant_prop.lift_prop_at_iff_comp_inclusion
{H : Type u_1}
{M : Type u_2}
{H' : Type u_3}
{M' : Type u_4}
[topological_space H]
[topological_space M]
[charted_space H M]
[topological_space H']
[topological_space M']
[charted_space H' M']
{G : structure_groupoid H}
{G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop}
(hG : G.local_invariant_prop G' P)
{U V : topological_space.opens M}
(hUV : U ≤ V)
(f : ↥V → M')
(x : ↥U) :
charted_space.lift_prop_at P f (set.inclusion hUV x) ↔ charted_space.lift_prop_at P (f ∘ set.inclusion hUV) x
theorem
structure_groupoid.local_invariant_prop.lift_prop_inclusion
{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 H → H → Prop}
(hG : G.local_invariant_prop G Q)
(hQ : ∀ (y : H), Q id set.univ y)
{U V : topological_space.opens M}
(hUV : U ≤ V) :
charted_space.lift_prop Q (set.inclusion hUV)
def
structure_groupoid.is_local_structomorph_within_at
{H : Type u_1}
[topological_space H]
(G : structure_groupoid H)
(f : H → H)
(s : set H)
(x : H) :
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
- G.is_local_structomorph_within_at f s x = (x ∈ s → (∃ (e : local_homeomorph H H), e ∈ G ∧ set.eq_on f e.to_local_equiv.to_fun (s ∩ e.to_local_equiv.source) ∧ x ∈ e.to_local_equiv.source))
theorem
structure_groupoid.is_local_structomorph_within_at_local_invariant_prop
{H : Type u_1}
[topological_space H]
(G : structure_groupoid H)
[closed_under_restriction G] :
For a groupoid G which is closed_under_restriction, being a local structomorphism is a local
invariant property.
theorem
local_homeomorph.is_local_structomorph_within_at_iff
{H : Type u_1}
[topological_space H]
{G : structure_groupoid H}
[closed_under_restriction G]
(f : local_homeomorph H H)
{s : set H}
{x : H}
(hx : x ∈ f.to_local_equiv.source ∪ sᶜ) :
G.is_local_structomorph_within_at ⇑f s x ↔ x ∈ s → (∃ (e : local_homeomorph H H), e ∈ G ∧ e.to_local_equiv.source ⊆ f.to_local_equiv.source ∧ set.eq_on ⇑f ⇑e (s ∩ e.to_local_equiv.source) ∧ x ∈ e.to_local_equiv.source)
A slight reformulation of is_local_structomorph_within_at when f is a local homeomorph.
This gives us an e that is defined on a subset of f.source.
theorem
local_homeomorph.is_local_structomorph_within_at_iff'
{H : Type u_1}
[topological_space H]
{G : structure_groupoid H}
[closed_under_restriction G]
(f : local_homeomorph H H)
{s : set H}
{x : H}
(hs : f.to_local_equiv.source ⊆ s)
(hx : x ∈ f.to_local_equiv.source ∪ sᶜ) :
G.is_local_structomorph_within_at ⇑f s x ↔ x ∈ s → (∃ (e : local_homeomorph H H), e ∈ G ∧ e.to_local_equiv.source ⊆ f.to_local_equiv.source ∧ set.eq_on ⇑f ⇑e e.to_local_equiv.source ∧ x ∈ e.to_local_equiv.source)
A slight reformulation of is_local_structomorph_within_at when f is a local homeomorph and
the set we're considering is a superset of f.source.
theorem
local_homeomorph.is_local_structomorph_within_at_source_iff
{H : Type u_1}
[topological_space H]
{G : structure_groupoid H}
[closed_under_restriction G]
(f : local_homeomorph H H)
{x : H} :
G.is_local_structomorph_within_at ⇑f f.to_local_equiv.source x ↔ x ∈ f.to_local_equiv.source → (∃ (e : local_homeomorph H H), e ∈ G ∧ e.to_local_equiv.source ⊆ f.to_local_equiv.source ∧ set.eq_on ⇑f ⇑e e.to_local_equiv.source ∧ x ∈ e.to_local_equiv.source)
A slight reformulation of is_local_structomorph_within_at when f is a local homeomorph and
the set we're considering is f.source.
theorem
structure_groupoid.has_groupoid.comp
{H₁ : Type u_6}
[topological_space H₁]
{H₂ : Type u_7}
[topological_space H₂]
{H₃ : Type u_8}
[topological_space H₃]
[charted_space H₁ H₂]
[charted_space H₂ H₃]
{G₁ : structure_groupoid H₁}
[has_groupoid H₂ G₁]
[closed_under_restriction G₁]
(G₂ : structure_groupoid H₂)
[has_groupoid H₃ G₂]
(H : ∀ (e : local_homeomorph H₂ H₂), e ∈ G₂ → charted_space.lift_prop_on G₁.is_local_structomorph_within_at ⇑e e.to_local_equiv.source) :
has_groupoid H₃ G₁