## Stream: maths

### Topic: Restriction of a groupoid

#### Heather Macbeth (Oct 22 2020 at 17:29):

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

#### 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 $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 (Oct 22 2020 at 17:33):

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

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

#### Heather Macbeth (Oct 22 2020 at 17:38):

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

#### 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,
...


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 (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