Restriction of a groupoid

Stream: maths

[Heather Macbeth]

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

[Heather Macbeth]

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

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 $G'$ is G ⊓ (relative_continuous_pregroupoid K).

[Heather Macbeth]

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.)

[Heather Macbeth]

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 $G_H$ for $H$ and a groupoid $G_K$ for $K$, such that the elements of $G_K$ can be proved to be exactly the restrictions of elements of $G_H$.

[Heather Macbeth]

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

[Sebastien Gouezel]

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).

[Heather Macbeth]

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

[Heather Macbeth]

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?

[Sebastien Gouezel]

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