gluing functions

Stream: new members

[Jean Lo]

Was trying to (set-theoretically) glue functions together in Lean. My first thought was to write down something like

variables {X : Type*} {Y : Type*}

def glue {ι : Type*} {s : ι → set X} {f : ι → X → Y}
  (h : ∀ i j x, x ∈ s i ∩ s j → f i x = f j x) : X → Y := sorry

and going on to prove some lemmas saying that the resultant function agrees on each f i on s i.

Is it a good idea to do this? What would be the idiomatic way of doing something like this in Lean?

[Kenny Lau]

omit h from the definition of glue

[Kenny Lau]

include it in the lemmas

[Jean Lo]

and add it as a hypothesis in the lemmas?

[Kenny Lau]

right

[Jean Lo]

ah okay, got it. Thanks!

[Scott Morrison]

What do you do when ι is empty?

[Jean Lo]

either ι or Y being nonempty would prevent the sadness, I think. Probably add nonemptiness of ιas a hypothesis?

[Kevin Buzzard]

You could instead just ask that the Union of s is X, for one of the unions in Lean, I forget what it's called

[Kevin Buzzard]

Existence and uniqueness of the glued function is the sheaf axiom for the cover

[Jean Lo]

that's very tempting because asking the union to be X would eliminate one of the ite's that I currently have to deal with.

there's maybe some loss in generality in that I don't get to glue together function whose values I only care about within some subset, but I don't know how much I should worry about that.

[Kevin Buzzard]

You could define a glued function only on the union

[Jean Lo]

got stuck.

import data.set

variables {X : Type*} {Y : Type*} {ι : Type*}

open set function

def glue {s : ι → set X} (h : ∀ x, x ∈ ⋃ i, s i) (f : ι → X → Y) : X → Y :=
λ x,
have l₁ : ∃ i : ι, x ∈ s i, from mem_Union.1 (h x),
let ⟨i, hi⟩ := l₁ in f i x

If I replace the f i x with an underscore, Lean tells me that it knows that i is of type ι and hi says x ∈ s i, but it's also unhappy about the let because recursor 'Exists.dcases_on' can only eliminate into Prop.

[Reid Barton]

You will need to use choice or something equivalent (and glue will have to be noncomputable)

[Kevin Buzzard]

noncomputable theorem indefinite_description
    {α : Sort u} (p : α → Prop) :
  (∃ x, p x) → {x // p x} :=

[Kevin Buzzard]

noncomputable def some {a : Sort u} {p : a → Prop}
  (h : ∃ x, p x) : a :=

[Kevin Buzzard]

(and some_spec too). See https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#choice

[Jean Lo]

ow, I really need to go and actually understand the computability stuff. Thanks for the help!

[Kevin Buzzard]

They're all in the classical namespace. You can't make this computable I don't think. Even with the hypothesis that the sub-functions agree on overlaps!

[Kevin Buzzard]

The example I found most jarring was that even if you can prove that f : X \to Y is a bijection, and computable, you can't construct a computable inverse; you have to use classical.some to get from the abstract surjectivity statement ("there exists x in X such that...") to the actual value of x (even though it's unique!)

[Kevin Buzzard]

Patrick wrote a choose tactic to do exactly this, but using tactics to define data is not always a good idea.

[Kevin Buzzard]

You're moving from Prop to Type. We do it all the time in the maths department, but basically you have to switch on maths mode to get Lean to do it without complaining.

[Jean Lo]

aha.

import data.set

variables {X : Type*} {Y : Type*} {ι : Type*}

open set

noncomputable def glue {s : ι → set X}
  (h : ∀ x, x ∈ ⋃ i, s i) (f : ι → X → Y) : X → Y :=
λ x, f (classical.some (mem_Union.1 (h x))) x

lemma glue_eq {s : ι → set X} {f : ι → X → Y}
  (h : ∀ x, x ∈ ⋃ i, s i) (heq : ∀ i j x, x ∈ s i ∩ s j → f i x = f j x) :
  ∀ i x, x ∈ s i → glue h f x = f i x :=
λ i x hi,
  have hq : ∀ j, x ∈ s j → f j x = f i x, from λ j hj,
  heq j i x ⟨hj, hi⟩, classical.some_spec2 _ hq

there! surely this looks sane now.

[Jean Lo]

and I guess actually proving the lemma is some exercise in fiddling around with classical.some_spec? will go try and do that.

(...and done, i guess.)

[Johan Commelin]

@Jean Lo You could go on to show that the union is the colimit...

[Johan Commelin]

I'm really excited about this stuff! Once we know what the correct picture is for gluing ordinary functions, I suggest we look into two things:

1. Gluing of continuous functions
2. Extract a useful/informed formal definition of the sheaf condition.

[Jean Lo]

It did start off with trying to glue continuous functions, actually - @Chris Hughes has proven the pasting lemma(s) in #1110, and I'm trying to do this so that I can construct some continuous functions piecewise.

[Jean Lo]

actually showing that it's the colimit sounds fun, but I also have no idea how easy/hard that would be since I admittedly have never looked at the category theory in mathlib.

I spent some more time yesterday finishing a proof that the glued function is unique (which I guess could be superceded by colimit arguments if there comes a proof for that?) and also versions for the different ways of doing unions in Lean. Is this stuff useful enough to other people be worth tossing in a PR? maybe appended to one of the files in data/set or something?

[Johan Commelin]

I certainly think that it will be quite useful

[Johan Commelin]

It shouldn't be too hard to prove its a colimit. It would be a nice test case (-;

[Jean Lo]

The code now exists on the gluing-functions branch: https://github.com/leanprover-community/mathlib/blob/gluing-functions/src/data/set/glue.lean

Not PR'd yet because I'd like to ask for some thoughts:

• I've been asking @Chris Hughes earlier about use cases, and what the definitions should actually be. Currently to invoke glue_on_Union I'd need to provide a proof that the family of sets actually cover univ for the source type, but ideally I'd want to do gluing even without that hypothesis (as glue_on_union currently does for the union of just two sets.) Would it be a good idea to

  • have glue_on_Union instead return from a subtype, and maybe provide some separate way of getting back a function from the original type given an additional hypothesis? or

  • have some a separate definition that doesn't require the covering hypothesis, but instead a proof/instance that one of the relevant types are nonempty?

• also, should these definitions/results actually belong under some existing file and/or under the set or function namespaces?

[Reid Barton]

Another possible approach is to use pfun and glue partial functions to a partial function, and prove that the domain of the resulting function is the union of the original domains

[Reid Barton]

I would recommend testing out the design in some application

[Jean Lo]

ooh, using roption stuff sounds like it might end up cleaner. It might even give me much of what I wanted with the subtype stuff, via as_subtype and friends. I think I'll have a go at implementing that and see how it handles in practice. Thanks for the pointers!

[Jean Lo]

wrote down the definition using roption, I like how tidy it looks:

import data.pfun

variables {α : Type*} {β : Type*} {ι : Sort*}

open pfun

noncomputable def glue (f_ : ι → α →. β) : α →. β :=
λ a, ⟨∃ i : ι, a ∈ dom (f_ i), λ ha, (f_ _ a).get (classical.some_spec ha)⟩

theorem glue_dom_eq_Union {f_ : ι → α →. β} {x : α} :
  dom (glue f_) = ⋃ i, dom (f_ i) :=
set.ext $ λ x, by { rw set.mem_Union, exact iff.rfl }

I'm less sure about the following theorem statement though:

theorem glue_eq {f_ : ι → α →. β} {i : ι} {x : α}
  (h : ∀ a i₁ i₂ h₁ h₂, (f_ i₁).fn a h₁ = (f_ i₂).fn a h₂)
  (hx : x ∈ dom (f_ i)) : (glue f_).fn x ⟨i, hx⟩ = (f_ i).fn x hx :=
  sorry

apart from being a little verbose and suspiciously non-idiomatic, I'm not entirely sure it actually says what I want. What would be the right way of stating this result?

I'm using some code for paths and homotopies as a test case, and in some cases I found that I'd still want to glue (plain) functions together without worrying about this restriction stuff. I'm currently thinking about appending the lemmas about gluing partial functions to pfun.lean, and having helper definitions available for some plain-function cases in the function namespace or something.

[Kevin Buzzard]

theorem glue_eq {f_ : ι → α →. β} {i : ι} {x : α}
  (h : ∀ a i₁ i₂ h₁ h₂, (f_ i₁).fn a h₁ = (f_ i₂).fn a h₂)
  (hx : x ∈ dom (f_ i)) : (glue f_).fn x ⟨i, hx⟩ = (f_ i).fn x hx :=
h _ _ _ _ _

[Kevin Buzzard]

I am not the person to talk to about idiomatic Lean but your theorem looks to me like it says what you want it to say.

[Chris Hughes]

Is that the proof? That was easy. Should we do the funny topology on roption idea, so if all the sets are open the function returnin roption is continuous iff the subtype function is continuous.

[Kevin Buzzard]

Yes, that proof works for me. It was discovered like this:

begin
  unfold glue,
  refine h _ _ _ _ _
  -- done?!
end

I thought the discussion about the topology on roption ended up undecided, with the issue being that Reid suggested several functors it could represent and we didn't know the best one.

[Mario Carneiro]

I would say this is not idiomatic, in that you should avoid talking about fn or get if you can avoid it, in favor of the mem relation. Here is a theorem you can prove about the function value without the equality constraint:

theorem glue_mem {f : ι → α →. β} {a : α}
  (ha : ∃ i, a ∈ dom (f i)) : ∃ i b, b ∈ f i a ∧ b ∈ glue f a :=
sorry

[Mario Carneiro]

and with the equality constraint:

theorem glue_eq_mem {f : ι → α →. β}
  (H : ∀ i i' a b b', b ∈ f i a → b' ∈ f i' a → b = b')
  {i : ι} {a : α} {b : β} (ha : b ∈ f i a) : b ∈ glue f a :=
sorry

[Johan Commelin]

I've always found the mem relation counterintuitive... but I guess I'll get used to it.

[Johan Commelin]

/me goes of to refactor some of his code

[Kevin Buzzard]

theorem glue_eq_mem {f : ι → α →. β}
  (H : ∀ i i' a b b', b ∈ f i a → b' ∈ f i' a → b = b')
  {i : ι} {a : α} {b : β} (ha : b ∈ f i a) : b ∈ glue f a :=
begin
  cases ha with h1 h2,
  use ⟨i, h1⟩,
  exact H _ i a _ b ⟨_, rfl⟩ ⟨h1, h2⟩,
end

[Kevin Buzzard]

exact H _ _ _ _ _ ⟨_, rfl⟩ ⟨h1, h2⟩, also works

[Jean Lo]

oh, nice. I feel like the fact that the statements & proofs are so much shorter is a sign that this is an appropriate way to formalise these things.

Another idiom question: in @Mario Carneiro 's theorem statements, glue_mem asks for an existence statement ha : ∃ i, a ∈ dom (f i), but glue_eq_mem wants the user to specify which i has a in the domain. What is the reason for this?

About the roption topology thing: the lemmas from the topology library that are currently relevant to the stuff I'm doing phrase things in terms of functions from subtypes, which I think will work pretty well with the code for gluing in this thread. I should go construct some concrete piecewise functions to see if anything turns out to be unexpectedly painful.

[Mario Carneiro]

Usually we don't put existence statements in the hypotheses, because it's easier to "uncurry" them as in glue_eq_mem. But I thought it might be easier to not get confused in glue_mem since the i in the assumption is not the same as the i in the conclusion. In glue_eq_mem there is only one i

[Mario Carneiro]

plus, that composite assumption can also be written a few other ways, like a \in dom (glue f)

[Mario Carneiro]

I'm not happy with Kevin's proof for essentially the same reason - it's unfolding all the abstractions and proving stuff on the base representation. You should be able to prove glue_eq_mem using glue_mem

[Jean Lo]

good point; i did just spend a few minutes being confused about the i. That the composite assumption just says a \in dom (glue f) means this proof is many rfl's:

theorem glue_mem {f : ι → α →. β} {a : α}
  (ha : ∃ i, a ∈ dom (f i)) : ∃ i b, b ∈ f i a ∧ b ∈ glue f a :=
⟨_, _, ⟨classical.some_spec ha, rfl⟩, _, rfl⟩

[Jean Lo]

tried to write a nice-looking proof of glue_eq_mem using glue_mem, but I think I still ended up unfolding too many terms — having to spend two lines pulling ha_w from ha looks particularly upsetting:

theorem glue_eq_mem {f : ι → α →. β}
  (H : ∀ i i' a b b', b ∈ f i a → b' ∈ f i' a → b = b')
  {i : ι} {a : α} {b : β} (ha : b ∈ f i a) : b ∈ glue f a :=
begin
  rcases (glue_mem _) with ⟨_, _, hi', hb'⟩,
  exact (H _ _ _ _ _ hi' ha) ▸ hb',
  cases ha, exact ⟨_, ha_w⟩,
end

[Mario Carneiro]

theorem glue_eq_mem {f : ι → α →. β}
  (H : ∀ {{i i' a b b'}}, b ∈ f i a → b' ∈ f i' a → b = b')
  {i : ι} {a : α} {b : β} (ha : b ∈ f i a) : b ∈ glue f a :=
let ⟨i', b', h₁, h₂⟩ := glue_mem ⟨_, (mem_dom _ _).2 ⟨_, ha⟩⟩ in
H h₁ ha ▸ h₂

[Jean Lo]

Nice! thanks for all the examples, it really helps with me trying to understand the reasoning behind how pfun works.

some context from the topology stuff I'm trying to write: I guess an immediate goal for me is to be able to do things like (the pasting lemma, but stated with partial functions, with their domains being the closed cover.)

realised that I was being a goof: pcontinuous doesn't mean what I thought it means — it checks continuity with respect to the topology on α, not the subspace topology on its domain! so the domains of a pcontinuous function are always open and that statement of the lemma made no sense.

[Jean Lo]

Meanwhile, some more problems: I felt like gluing two functions is a special case worth having separate statements for. I think these are okay:

noncomputable def glue₂ (f₁ : α →. β) (f₂ : α →. β) : α →. β :=
glue (λ b, cond b f₁ f₂)

variables {f₁ f₂ : α →. β}

theorem glue₂_dom_eq_union : dom (glue₂ f₁ f₂) = dom f₁ ∪ dom f₂ :=
have (λ b, cond b (dom f₁) (dom f₂)) = (λ b, dom (cond b f₁ f₂)), from
  funext $ λ b, by cases b; simp only [bool.cond_tt, bool.cond_ff],
by {
  rw [set.union_eq_Union, this],
  exact glue_dom_eq_Union }

(I couldn't get Lean to figure out the lambdas without the haves, but that's, like, two lines, so it doesn't bother me that much yet.)

but I can't seem to find a pretty way of doing the following proof:

theorem glue₂_eq_mem_left (H : ∀ a b b', b ∈ f₁ a → b' ∈ f₂ a → b = b')
  {a : α} {b : β} (ha : b ∈ f₁ a) : b ∈ glue₂ f₁ f₂ a :=
let f := λ b, cond b f₁ f₂ in
have hf₁ : f₁ = f tt, from bool.cond_tt _ f₁,
have hf₂ : f₂ = f ff, from bool.cond_tt _ f₂,
have H' : ∀ i i' a b b', b ∈ f i a → b' ∈ f i' a → b = b', from
λ i i' a b b' ⟨hi, hb⟩ ⟨hi', hb'⟩,
begin
  rw [hf₁, hf₂] at H,
  -- cases hell
  sorry
end,
have h₁ : b ∈ f tt a, by rwa ←hf₁,
glue_eq_mem H' h₁

This makes me a little sad. It'd be easier if glue₂ had been defined with some sort of ite instead of glue-ing functions indexed by bool, but that feels iffy.