## Stream: new members

### Topic: gluing functions

#### Jean Lo (Jun 03 2019 at 21:19):

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

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

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

Last updated: May 15 2021 at 02:11 UTC