Gluing of [continuous] functions

Stream: Is there code for X?

[Heather Macbeth]

Does mathlib have something resembling at least the first of these lemmas (gluing of functions parametrized by a family of sets, which agree on intersections of the sets), if not the second (a continuous version)?

import topology.continuous_function.basic

open set

variables  {α : Type*} {β : Type*} {ι : Type*} {s : ι → set α}

lemma glue (hs : ∀ x, ∃ i, x ∈ s i) {F : ι → α → β} (h : ∀ i j, eq_on (F i) (F j) (s i ∩ s j)) :
  ∃! f : α → β, ∀ i, eq_on (F i) f (s i) :=
begin
  refine exists_unique_of_exists_of_unique _ _,
  { choose I hI using hs,
    refine ⟨λ x, F (I x) x, _⟩,
    intros i x hx,
    exact h i (I x) ⟨hx, hI x⟩ },
  { intros f f' hf hf',
    ext x,
    obtain ⟨i, hi⟩ : ∃ i, x ∈ s i := by simp [← mem_Union, hs],
    exact (hf i hi).symm.trans (hf' i hi) },
end

lemma continuous_glue [topological_space α] [topological_space β] (hs : ∀ x : α, ∃ i, s i ∈ nhds x)
  {F : ι → C(α, β)} (h : ∀ i j, eq_on (F i) (F j) (s i ∩ s j)) :
  ∃! f : C(α, β), ∀ i, eq_on (F i) f (s i) :=
begin
  have hs' : ∀ x, ∃ i, x ∈ s i,
  { intros x,
    obtain ⟨i, hi⟩ := hs x,
    exact ⟨i, mem_of_mem_nhds hi⟩ },
  have exists_unique_f := glue hs' h,
  refine exists_unique_of_exists_of_unique _ _,
  { obtain ⟨f, hf⟩ := exists_unique_f.exists,
    refine ⟨⟨f, _⟩, hf⟩,
    rw continuous_iff_continuous_at,
    intros x,
    obtain ⟨i, hi⟩ := hs x,
    refine (F i).continuous.continuous_at.congr _,
    exact filter.eventually_eq_of_mem hi (hf i) },
  { intros _ _ hf hf',
    exact continuous_map.coe_inj (exists_unique_f.unique hf hf') }
end

[Heather Macbeth]

Maybe @Sebastien Gouezel used something like it in the various files on local equivalences and local homeomorphisms?

[Heather Macbeth]

Or maybe someone doing sheaf-y work like @Justus Springer?

[Kevin Buzzard]

@Chris Hughes you were just doing this with bare functions recently, right?

[Johan Commelin]

@Chris Hughes was looking at this only a few days ago

[Heather Macbeth]

Aha! This is #9019 right?

[Chris Hughes]

#9019. The hypotheses are slightly different, I guess the thing you'd need would be lift_of_eq_Union. I didn't do anything topological. Maybe there should be just one version for defining maps out of sets contained in a Union. The F : iota -> alpha-> beta isn't ideal for my application, the functions are alg_homs defined on a sub_alg, and I really don't want to have to give them junk values elsewhere.

[Chris Hughes]

I also think it might be worth having several versions of this.

[Heather Macbeth]

I like that your version allows one to lift "partway", i.e. in my setting just to the union of the sets, if they don't cover the space completely. Of course this loses the uniqueness part of my statement.

[Justus Springer]

We do have docs#Top.sheaf.exists_unique_gluing' and we have docs#Top.sheaf_to_Top. Putting them together gives something close to your second lemma, though not quite. See for yourself:

import topology.sheaves.local_predicate
import topology.sheaves.sheaf_condition.unique_gluing

universe u

open Top

variables  {α : Type u} {β : Type u} [topological_space α] [topological_space β]

#check (@sheaf_to_Top (Top.of α) (Top.of β)).exists_unique_gluing'

The difference is that this takes a family of open sets U : ι → opens α and a family f : Π i, C(U i, β).

[Justus Springer]

Note that (@sheaf_to_Top (Top.of α) (Top.of β)).presheaf.obj (op U) is defeq to C(U, β).

[Justus Springer]

(Also, it requires α and β to live in the same universe)

[Chris Hughes]

@Heather Macbeth What do you think of #9019 ? I was thinking of deleting Union_lift_of_eq and just having one version for defining maps out of any subtype contained in the Union.

[Heather Macbeth]

@Chris Hughes Maybe we don't need the of_eq version, but I think it would be nice to have a special version for when the union is the whole set. Full disclosure: I just tried to write such a special version myself, and found that I don't know enough about subtypes to do it!

[Jake Levinson]

Is this an ongoing part of mathlib development? I've been putting together (my own, not using the mathlib topology library, since I am an amateur) lemmas on exactly this stuff, about gluing along open sets + fiber products + fiber bundles.

I had figured stuff like this was probably already in mathlib, but if it isn't, would this be a reasonable topic where a newcomer like me could contribute?

[Jake Levinson]

(I realize I'd have to learn the Lean style, actually use mathlib instead of my own homebrewed topology stuff, etc)

[Jake Levinson]

(In particular I wrote a lemma nearly identical to @Heather Macbeth 's continuous_glue above, right down to the proof strategy of using "continuous iff continuous at each point"... :smile: )

[Heather Macbeth]

@Jake Levinson Welcome! We'll be glad to have your contributions!

I do wonder if these gluing lemmas are a bit of a special case, and less suited for a newcomer than most. It's clear that there are 100 possible variations (see the four versions mentioned by Chris, me, yourself and Justus, all in the last few days). It seems to me that the challenge here is not in the proofs themselves, but in figuring out the most efficient path -- which versions are special cases of other versions, what special cases deserve their own entries in the library, etc.

[Heather Macbeth]

Perhaps you could start by doing some testing -- can you deduce your version from Chris'? Or if not, can you generalize yours in a way that allows Chris' to be deduced from yours? Same for the one mentioned by Justus, etc etc.

[Jake Levinson]

Heather Macbeth said:

Jake Levinson Welcome! We'll be glad to have your contributions!

I do wonder if these gluing lemmas are a bit of a special case, and less suited for a newcomer than most. It's clear that there are 100 possible variations (see the four versions mentioned by Chris, me, yourself and Justus, all in the last few days). It seems to me that the challenge here is not in the proofs themselves, but in figuring out the most efficient path -- which versions are special cases of other versions, what special cases deserve their own entries in the library, etc.

Thanks! That makes sense to me. I am definitely not in a position to judge the global merits of one approach over another, though could potentially help fill in sorrys if needed.

I tried earlier today to deduce Chris's version from mine (which requires the sets to be a full cover). I think it's not too bad, but the main awkwardness indeed appeared to come from subtype stuff.

One (minor?) subtype issue I noticed regarding extending a function to Union S, vs extending to the entire type (in the case of a full cover), is that the latter is not a direct special case of the former (even with the additional lift_of_eq_Union definition). In particular, even if we have the hypothesis h : Union S = set.univ, lift_of_eq_Union will produce a function f : ↑set.univ → β rather than α → β. That is, the domain of f is the subtype {a : α // true} which is equivalent but not equal to α.

Something similar to this came up for me at one point and I found it annoying to have to deal with... so it may be handy to have some API to cover this case. I know there's plenty of support for the usual coe : {a : α // true} → α, but is there a standard name for the one going the other way, eoc : α → {a : α // true} := λ x, ⟨x, trivial⟩ as needed above?

[Heather Macbeth]

@Jake Levinson @Chris Hughes Sorry to have been slow in coming back to this. I have written a PR (#9239) containing just the version of continuous gluing I need. Feel free to hijack this PR with other versions, if you have suggestions!