Stream: maths

Topic: Restriction in structure groupoid

Heather Macbeth (Jul 09 2020 at 05:48):

From docs#structure_groupoid, it seems that a structure groupoid need not be closed under restriction, i.e. if e : local_homeomorph H H is in the groupoid then a restriction of e to a smaller set is not necessarily in the groupoid. For example, the trivial groupoid docs#id_groupoid contains the identity map from H to itself, but not local_homeomorph.of_set s (the restriction of the identity to an open set s).

Is there a reason for this? I believe the obvious structure groupoids (continuous, smooth, analytic, ...) all have the restriction property. Also, AFAICT, this property (for a groupoid G) is what is needed for the charted_space structure on a space α induced by an open embedding f : α → H to be has_groupoid ... G.

Heather Macbeth (Jul 09 2020 at 05:55):

import geometry.manifold.charted_space
variables {H : Type*} [topological_space H]
variables {α : Type*} [topological_space α]
variables {e : local_homeomorph α H}

def singleton_charted_space (h : e.source = set.univ) : charted_space H α :=
{ atlas := λ e', e' = e,
chart_at := λ _, e,
mem_chart_source := λ _, by {rw h, simp},
chart_mem_atlas := λ _, by tauto }

lemma singleton_charted_space_one_chart (h : e.source = set.univ) (e' : local_homeomorph α H)
(h' : e' ∈ (singleton_charted_space h).atlas) : e' = e := h'

def singleton_has_groupoid (h : e.source = set.univ) (G : structure_groupoid H) :
@has_groupoid _ _ _ _ (singleton_charted_space h) G :=
{ compatible := begin
intros e' e'' he' he'',
rw singleton_charted_space_one_chart h e' he',
rw singleton_charted_space_one_chart h e'' he'',
refine G.eq_on_source _ e.trans_symm_self,
/- goal state :
⊢ local_homeomorph.of_set e.to_local_equiv.target _ ∈ G -/
sorry,
end }


Sebastien Gouezel (Jul 09 2020 at 06:58):

Yes, there is a reason for this (which hopefully should be explained in the docs just around the definition of structure_groupoid, but maybe I forgot to add it there). The reason is vector bundles: a vector bundle corresponds to a charted space structure where the structure group is the group made of maps of the form $(x, y)\mapsto (f x, A_x (y))$ where $A_x$ is linear, and where the chart domains should be of the form s \times univ. If you remove this last requirement and the field is not connected, then such a charted space structure would not be enough to guarantee that you have a vector bundle.

Note that all this is pure fantasy: vector bundles as charted spaces have not yet been developed in mathlib. But still, I think this potential application is important enough to motivate the definition.

Heather Macbeth (Jul 09 2020 at 12:45):

Thank you! I see, there is a long comment explaining this, but it is /- rather than /-- so I did not notice it in the docs.

Sebastien Gouezel (Jul 09 2020 at 12:48):

Ah, yes. Do you think we should make it /--? I am afraid it would be a little too long for a docstring that shows up in the tooltip, but still it would be good to have it in the docs and not just in the code. Maybe with a /-! block it would be better.

Heather Macbeth (Jul 09 2020 at 12:50):

Sounds good to me.

Heather Macbeth (Jul 09 2020 at 13:22):

@Sebastien Gouezel , do you think it would be useful to add a closed_under_restriction typeclass for groupoids? I think there are several arguments that use this property (such as the example I gave above).

Sebastien Gouezel (Jul 09 2020 at 13:56):

Yes, I think it is a good idea.

Heather Macbeth (Jul 09 2020 at 13:56):

Great, I will try it.

Heather Macbeth (Jul 09 2020 at 20:37):

#3347

Last updated: May 10 2021 at 06:13 UTC