Zulip Chat Archive
Stream: new members
Topic: gluing functions
Jean Lo (Jun 03 2019 at 21:19):
Was trying to (settheoretically) 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 (Jun 03 2019 at 21:20):
omit h
from the definition of glue
Kenny Lau (Jun 03 2019 at 21:21):
include it in the lemmas
Jean Lo (Jun 03 2019 at 21:21):
and add it as a hypothesis in the lemmas?
Kenny Lau (Jun 03 2019 at 21:21):
right
Jean Lo (Jun 03 2019 at 21:21):
ah okay, got it. Thanks!
Scott Morrison (Jun 03 2019 at 21:22):
What do you do when ι
is empty?
Jean Lo (Jun 03 2019 at 21:24):
either ι
or Y
being nonempty would prevent the sadness, I think. Probably add nonemptiness of ι
as a hypothesis?
Kevin Buzzard (Jun 03 2019 at 21:38):
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 (Jun 03 2019 at 21:39):
Existence and uniqueness of the glued function is the sheaf axiom for the cover
Jean Lo (Jun 03 2019 at 21:52):
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 (Jun 03 2019 at 21:58):
You could define a glued function only on the union
Jean Lo (Jun 03 2019 at 22:34):
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 (Jun 03 2019 at 22:35):
You will need to use choice
or something equivalent (and glue
will have to be noncomputable)
Kevin Buzzard (Jun 03 2019 at 22:37):
noncomputable theorem indefinite_description {α : Sort u} (p : α → Prop) : (∃ x, p x) → {x // p x} :=
Kevin Buzzard (Jun 03 2019 at 22:38):
noncomputable def some {a : Sort u} {p : a → Prop} (h : ∃ x, p x) : a :=
Kevin Buzzard (Jun 03 2019 at 22:38):
(and some_spec
too). See https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#choice
Jean Lo (Jun 03 2019 at 22:39):
ow, I really need to go and actually understand the computability stuff. Thanks for the help!
Kevin Buzzard (Jun 03 2019 at 22:39):
They're all in the classical
namespace. You can't make this computable I don't think. Even with the hypothesis that the subfunctions agree on overlaps!
Kevin Buzzard (Jun 03 2019 at 22:41):
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 (Jun 03 2019 at 22:42):
Patrick wrote a choose
tactic to do exactly this, but using tactics to define data is not always a good idea.
Kevin Buzzard (Jun 03 2019 at 22:43):
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 (Jun 03 2019 at 22:51):
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 (Jun 03 2019 at 22:54):
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 (Jun 04 2019 at 06:29):
@Jean Lo You could go on to show that the union is the colimit...
Johan Commelin (Jun 04 2019 at 06:45):
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 (Jun 04 2019 at 07:03):
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 (Jun 04 2019 at 07:12):
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 (Jun 04 2019 at 07:23):
I certainly think that it will be quite useful
Johan Commelin (Jun 04 2019 at 07:24):
It shouldn't be too hard to prove its a colimit. It would be a nice test case (;
Jean Lo (Jun 04 2019 at 13:58):
The code now exists on the gluingfunctions
branch: https://github.com/leanprovercommunity/mathlib/blob/gluingfunctions/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 coveruniv
for the source type, but ideally I'd want to do gluing even without that hypothesis (asglue_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
orfunction
namespaces?
Reid Barton (Jun 04 2019 at 14:05):
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 (Jun 04 2019 at 14:08):
I would recommend testing out the design in some application
Jean Lo (Jun 04 2019 at 17:35):
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 (Jun 04 2019 at 19:40):
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 nonidiomatic, 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 plainfunction cases in the function
namespace or something.
Kevin Buzzard (Jun 04 2019 at 22:12):
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 (Jun 04 2019 at 22:13):
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 (Jun 04 2019 at 22:17):
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 (Jun 04 2019 at 22:24):
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 (Jun 04 2019 at 22:27):
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 (Jun 04 2019 at 22:29):
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 (Jun 05 2019 at 04:21):
I've always found the mem
relation counterintuitive... but I guess I'll get used to it.
Johan Commelin (Jun 05 2019 at 04:21):
/me goes of to refactor some of his code
Kevin Buzzard (Jun 05 2019 at 07:40):
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 (Jun 05 2019 at 07:40):
exact H _ _ _ _ _ ⟨_, rfl⟩ ⟨h1, h2⟩,
also works
Jean Lo (Jun 05 2019 at 10:11):
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 (Jun 05 2019 at 12:23):
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 (Jun 05 2019 at 12:24):
plus, that composite assumption can also be written a few other ways, like a \in dom (glue f)
Mario Carneiro (Jun 05 2019 at 12:25):
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 (Jun 05 2019 at 12:32):
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 (Jun 05 2019 at 13:00):
tried to write a nicelooking 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 (Jun 05 2019 at 14:53):
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 (Jun 05 2019 at 15:27):
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 (Jun 05 2019 at 22:48):
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 have
s, 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.
Last updated: May 15 2021 at 02:11 UTC