Zulip Chat Archive

Stream: maths

Topic: Restriction of a groupoid


view this post on Zulip Heather Macbeth (Oct 22 2020 at 17:29):

Maths problem: Given a model space HH and fixed subspace KK, and a structure groupoid GG for HH, construct the groupoid GG' consisting of those elements of GG which stabilize KK. Is there automatically an induced (by restriction) groupoid for KK?

view this post on Zulip Heather Macbeth (Oct 22 2020 at 17:30):

I had assumed the answer was yes, and gone some way down this path: defining, firstly, the groupoid of all local homeomorphisms preserving KK:

def relative_continuous_pregroupoid : pregroupoid H :=
{ property := λ f s,  x  s  K, f x  K,
  comp := begin
    intros f g _ _ hf hg _ _ _ x hx,
    exact hg (f x) hx.1.2, hf x hx.1.1, hx.2⟩⟩,
  end,
  id_mem := ...,
  locality := ...,
  congr := ...,
  end }

def relative_continuous_groupoid : structure_groupoid H :=
(relative_continuous_pregroupoid K).groupoid

then a construction of has_inf for groupoids, so that the desired GG' is G ⊓ (relative_continuous_pregroupoid K).

view this post on Zulip Heather Macbeth (Oct 22 2020 at 17:30):

But it seems there is a problem with the locality condition: given an open subset s of K and a function f: s → K, and the hypothesis that about each point x of s there exist a K-preserving local homeomorphism of H which restricts to f near x, is it true that there must exist a K-preserving local homeomorphism of H which restricts to f on the whole of s? I don't see how to prove this. (Maybe it's useful to assume s is closed, so one gets access to the Tieze extension theorem, but this still only gives extensions which are continuous functions, not homeomorphisms.)

view this post on Zulip Heather Macbeth (Oct 22 2020 at 17:32):

If anyone sees a way of proving this, please tell me! If not, I suppose the solution is to make the central object a pair consisting of a groupoid GHG_H for HH and a groupoid GKG_K for KK, such that the elements of GKG_K can be proved to be exactly the restrictions of elements of GHG_H.

view this post on Zulip Heather Macbeth (Oct 22 2020 at 17:33):

@Sebastien Gouezel @Patrick Massot in particular might have opinions :up:

view this post on Zulip Sebastien Gouezel (Oct 22 2020 at 17:37):

I had an issue like that with smooth functions on arbitrary subsets, where gluing different nice germs at different points is something nonobvious (in particular over a general field). The solution I went for is to require the existence of germs around every point, not a globally nice function. Could you do the same here? (I.e., define your groupoid not as the restrictions of nice functions, but as the functions which, around every point, coincide with the restriction of a nice function -- that might depend on the point you're considering).

view this post on Zulip Heather Macbeth (Oct 22 2020 at 17:38):

Ah, so build the locality hypothesis into the property somehow. This seems promising! Let me think!

view this post on Zulip Heather Macbeth (Oct 22 2020 at 17:42):

So at the moment I define

def restr_pregroupoid : pregroupoid K :=
{ property := λ f s,  f' : local_homeomorph H H,
    f'  (relative_continuous_groupoid K)  eq_on (coe  f) (f'  coe) s,
...

and you are suggesting, instead,

def restr_pregroupoid : pregroupoid K :=
{ property := λ f s,  x, x  s   f' : local_homeomorph H H,  (u : set K),
    f'  (relative_continuous_groupoid K)  eq_on (coe  f) (f'  coe) (s  u),
...

(maybe with some openness hypotheses if needed). Is that right?

view this post on Zulip Sebastien Gouezel (Oct 22 2020 at 18:52):

Something like that, yes (probably also requiring that x belongs to the domain of f').


Last updated: May 11 2021 at 16:22 UTC