Restriction in structure groupoid

Stream: maths

[Heather Macbeth]

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]

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]

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]

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]

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]

Sounds good to me.

[Heather Macbeth]

@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]

Yes, I think it is a good idea.

[Heather Macbeth]

Great, I will try it.

[Heather Macbeth]

#3347