## Stream: maths

### Topic: atlases

#### Patrick Massot (Jun 26 2018 at 10:03):

I decided to try to move forward in my differential topology project without waiting for experts to sort out the module type class issues. So let's say I'm ready to sorry the definition of a diffeomorphism between two open subsets of R^n. Then the definition to formalize is https://en.wikipedia.org/wiki/Differentiable_manifold#Atlases I have no idea how to attack this coercion mess. I'd like to understand the definition of the transitions maps, and understand they are maps between open subsets of R^n

#### Patrick Massot (Jun 26 2018 at 10:04):

Even restricting a function to a subset is non-trivial in Lean

#### Patrick Massot (Jun 26 2018 at 10:05):

and here I need that the restriction of a homeo to a subset is a homeo onto its image

#### Johan Commelin (Jun 26 2018 at 11:19):

Even restricting a function to a subset is non-trivial in Lean

Can't you compose with subtype.val? And then you need that subtype.val is an immersion, and C^k for every value of k.

#### Patrick Massot (Jun 26 2018 at 12:21):

I need to invert the restriction of an equiv to some subset

#### Chris Hughes (Jun 26 2018 at 13:40):

Is this any use?

import analysis.topology.continuity
variables {α : Type*} {β : Type*} [topological_space α] [topological_space β]
(A : set α) (f : {f : α ≃ β // continuous f})

def restriction : {g : A ≃ f '' A // continuous g} :=
⟨{  to_fun := (λ a, ⟨f a.1, a, a.2, rfl⟩),
inv_fun := λ b, ⟨(equiv.symm (f : α ≃ β)) b, let ⟨a, ha₁, (ha₂ : f a = b)⟩ := b.2 in
calc _ = a : by rw ← ha₂; exact equiv.inverse_apply_apply _ _
... ∈ A : ha₁⟩,
left_inv := λ ⟨_, _⟩, subtype.eq (f.1.3 _),
right_inv := λ ⟨_, _⟩, subtype.eq (f.1.4 _)  },
continuous_subtype_mk (λ x, ⟨x, x.2, rfl⟩)
(continuous.comp continuous_subtype_val f.2)⟩


Maybe

#### Patrick Massot (Jun 26 2018 at 13:43):

I'm exploring a lot of ways to try to make Lean understanding this definition or variations on this definition

#### Patrick Massot (Jun 26 2018 at 13:44):

I already knew there were plenty of variations on the definition of manifolds but I'm discovering many more

#### Patrick Massot (Jun 26 2018 at 13:52):

A variation on this kind of effort could be to adapt

protected noncomputable def image {α β} (f : α → β) (s : set α) (H : injective f) :
s ≃ (f '' s) :=
⟨λ ⟨x, h⟩, ⟨f x, mem_image_of_mem _ h⟩,
λ ⟨y, h⟩, ⟨classical.some h, (classical.some_spec h).1⟩,
λ ⟨x, h⟩, subtype.eq (H (classical.some_spec (mem_image_of_mem f h)).2),
λ ⟨y, h⟩, subtype.eq (classical.some_spec h).2⟩


from equiv.lean to a version where H would be inj_on f s, which seems like a much more relevant hypothesis anyway

#### Patrick Massot (Jun 26 2018 at 13:54):

But maybe I don't care. I don't know. There are so many ways to try to setup this thing...

#### Chris Hughes (Jun 26 2018 at 13:56):

You're losing computability with that def, though I'm not sure you care.

#### Patrick Massot (Jun 26 2018 at 13:57):

Ah, at least there is something I know: I don't care about computability.

#### Patrick Massot (Jun 26 2018 at 13:57):

Chris, this remark worries me. I think you may be spending too much time with Kenny.

#### Patrick Massot (Jun 26 2018 at 14:01):

I'm completely confused about https://github.com/leanprover/mathlib/blob/master/data/equiv.lean#L527 How do you access this definition? It seems to be in namespace set but is obviously not the same as set.range

#### Kenny Lau (Jun 26 2018 at 14:02):

the equiv namespace never ended :)

#### Kenny Lau (Jun 26 2018 at 14:02):

equiv.set.range

Oh, that's nasty

thanks Kenny

#### Patrick Massot (Jun 26 2018 at 14:04):

hum, I hear I urgently need to go to the main lecture hall in IHES

#### Patrick Massot (Jun 26 2018 at 14:04):

it seems the match started already

#### Sebastien Gouezel (Jun 26 2018 at 20:27):

Are you planning to implement only C^\infty manifolds over the reals, or manifolds with different classes of smoothness (say C^0, or C^1, or C^k, or analytic, or PL, or whatever you like, over R or C)? It seems to me that it would be better to implement various classes of smoothness in the same framework. For instance, one could axiomatize what one needs to have a "smoothness class" (families of maps which are all homeos between open subsets of a given topological space, stable under restriction and composition and inverses), and then one could define a manifold with respect to this smoothness class. Two advantages of this approach:
- this is more general, and useful
- you don't need to define R^n and smooth maps to start working with this definition (but of course, you will have no example at the beginning, except maybe for C^0 manifolds which would be the first example to work out)
Any thoughts?

#### Patrick Massot (Jun 26 2018 at 20:29):

Unfortunately I'm pretty far from being able to do that. The trouble is partially defined functions are everywhere. A chart is defined on part of the manifold, a transition function is defined on the image of part of the domain of a chart. I really struggle with this. How is this handled in Isabelle? Do you have smooth functions defined on open subsets of R^n and a convenient way to restrict a smooth function to an open subset?

#### Patrick Massot (Jun 26 2018 at 20:30):

But, to answer your question, I was indeed hoping to implement manifolds modeled on any pseudo-group

#### Patrick Massot (Jun 26 2018 at 20:31):

I also find it very interesting to see that, once again, the only source which seems to be suitable for formalization is Bourbaki.

#### Sebastien Gouezel (Jun 26 2018 at 20:35):

In Isabelle, I would model a smoothness class by a set of pairs (U, f) where U is an open subset of R^n and f is a map from R^nto itself such that its restriction to U is a homeomorphism. So, I would have a predicate homeomorphism_on U f saying that f is a homeomorphism on U, together with basic properties of homeomorphisms (say, if f is a homeomorphism on U and gis a homeomorphism on V and f(U) \subseteq V, then g o f is a homeomorphism on U). Then you don't ever need to restrict your functions to subsets, and you avoid a lot of trouble.

#### Sebastien Gouezel (Jun 26 2018 at 20:35):

and the smoothness on open subsets is also defined for total functions, using a predicate as above.

#### Patrick Massot (Jun 26 2018 at 20:40):

I thought about trying to get functions defined everywhere and asking for injectivity and smoothness only on subsets. But I fear it will be a nightmare when trying to prove things because every function would be defined by lambda x, if x in U then real_thing x else 42.

#### Patrick Massot (Jun 26 2018 at 20:41):

And also I don't like this has nothing to do with math

#### Patrick Massot (Jun 26 2018 at 20:41):

It's purely an artefact of the type theoretic foundations

#### Sebastien Gouezel (Jun 26 2018 at 20:51):

You would never have any if in your definitions. The composition of two homeomorphisms fon U and g on V is just g o f on U (and it only makes sense if f(U) \subseteq V, but this is also the case with the true definition). The restriction of a homeomorphism fon U to a smaller subset U' is still f . And so on. This may seem surprising at first sight, but in fact it is not so surprising: if you only do meaningful constructions, then the values of your function outside of its "domain of definition" should never play any role, so what happens there is never relevant, and it can behave in the way it wants.

#### Patrick Massot (Jun 26 2018 at 20:52):

I know it's the theory, I've seen it countless times with 0/0 and other crazy stuff. But you still need to define an arbitrary crazy value. For 0/0 you can choose 0, fine. What if the target is a manifold?

#### Sebastien Gouezel (Jun 26 2018 at 20:53):

It is just like the fact that the division is total on real numbers: surprising and annoying at the beginning, and then when you get used to it you realize you don't care at all what it does at zero because you're not stupid and you never apply it at 0 (and of course you always have to check that the denominator is nonzero -- here in the same way you would always have to check that the points you apply your function to are in the "domain of definition")

#### Patrick Massot (Jun 26 2018 at 20:55):

Do you have the same crazyness in Isabelle then?

#### Sebastien Gouezel (Jun 26 2018 at 20:55):

At least for the definition of a manifold in terms of an atlas of compatible charts, you would never need to specify a value, it is just some axioms you want to satisfy.
Probably, when you define a manifold structure on some object, yes, you will have to make some arbitrary and irrelevant choice at some point. But that would be very rare, I guess.

#### Patrick Massot (Jun 26 2018 at 20:56):

Yes, I want to define actual manifolds, like smooth affine varieties in R^n (say S^{n-1})

#### Sebastien Gouezel (Jun 26 2018 at 20:56):

The crazyness of what? Every function is total, yes. And it turns out to be a non-issue once you're used to it. (Takes some time to get used to it :)

thanks

#### Sebastien Gouezel (Jun 26 2018 at 20:58):

Think of S^{n-1}. Take the two natural stereographic charts: they are defined on the whole of R^{n-1}, so no issue of arbitrary choice when you define them. And then you just have to check the axiom that the composition of one chart and the inverse of the other one, restricted to the good sets, are smooth. No arbitrary choice again.

#### Sebastien Gouezel (Jun 26 2018 at 20:59):

Same think if you define Grassmannians, say: the natural local charts using linear maps are defined on the whole R^k. No arbitrary choice again.

#### Patrick Massot (Jun 26 2018 at 20:59):

This is not the definition I want to use. This one is only an exercise in understanding the internal plumbing that is the precise definition of a manifold. I want S^{n-1} defined by |x|² = 1

#### Patrick Massot (Jun 26 2018 at 20:59):

I want submanifolds of manifolds to be manifolds

#### Patrick Massot (Jun 26 2018 at 21:00):

But I'll try this total function road

#### Sebastien Gouezel (Jun 26 2018 at 21:00):

Then you want to use two theorems, that the preimage of a regular value by a map is a submanifold, and that a submanifold is a manifold. Again no choice :)

#### Patrick Massot (Jun 26 2018 at 21:01):

Are you sure the second one will require no choice? Maybe.

#### Sebastien Gouezel (Jun 26 2018 at 21:02):

The way answers are intermingled is really strange in such a chat. Anyway, to prove that a submanifold is a manifold, essentially you will first straighten your submanifold, and then restrict your charts to the submanifold. Then there should be no ifin the involved arguments.

#### Patrick Massot (Jun 26 2018 at 21:04):

I'll try all this tomorrow (what I tried today is on https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/manifold.lean if you are curious (there may be stupid things there, I switched gears so many times...)

#### Patrick Massot (Jun 26 2018 at 21:05):

thank you very much for this conversation

good night!

#### Patrick Massot (Jun 27 2018 at 13:38):

I try to get used to totalization of functions. What do people think about:

universes u v
variables {α : Type u} [inhabited α] {β : Type v}

def inverse_on  {U : set α} {f : α → β} (H : inj_on f U) : β → α :=
λ b, if h : b ∈ f '' U then classical.some h else default α

lemma inverse_on_spec {U : set α} {f : α → β} (H : inj_on f U) :
inv_on (inverse_on H) f U (f '' U) :=
begin
split ; intros x h,
{ have H' := mem_image_of_mem f h,
cases classical.some_spec H' with h1 h2,
simp [inverse_on, H', H h1 h h2] },
{ cases classical.some_spec h with h1 h2,
simpa [inverse_on, h] using h2 }
end


Is it something I should be doing?

#### Reid Barton (Jun 27 2018 at 14:05):

I don't see why it should be necessary to work with total functions here, and this approach has its own disadvantages. I think the root problem is that you currently lack a sufficient Lean vocabulary to work with partial functions and partial bijections

#### Patrick Massot (Jun 27 2018 at 14:06):

What would be that vocabulary?

#### Reid Barton (Jun 27 2018 at 14:09):

For example, looking at the definition of pseudogroup, you could state most of these axioms immediately given:

• A type pequiv a b representing a bijection between a subset of the type a and a subset of the type b. Note that the subsets of a and b are not indices of the type pequiv a b.
• A "restricted composition" operation pequiv a b \to pequiv b c \to pequiv a c.
• A "restricted identity" of type pequiv a a for each s : set a, which is the identity bijection between s and itself. From this and the previous one, you can implement restriction of a pequiv to a subset of the domain or codomain.
• A way to extract from a pequiv a b the domain s as a set a, and a function subtype s \to b, which you can then check for continuity or smoothness or whatever.

#### Patrick Massot (Jun 27 2018 at 14:11):

What would be a "restricted composition" in a world where all functions are total? That's precisely the trouble.

#### Reid Barton (Jun 27 2018 at 14:11):

Also I forgot the "symmetry" pequiv a b \to pequiv b a.

#### Reid Barton (Jun 27 2018 at 14:12):

Well then you are asking about how to implement this interface, right?

#### Patrick Massot (Jun 27 2018 at 14:12):

Everything is about implementation in this discussion, I already know what is a manifold.

#### Reid Barton (Jun 27 2018 at 14:12):

Or are you asking about the meaning of the operation? It's just the one which, given partial bijections f and g, is defined on x when f(x) is defined and g(f(x)) is also defined

#### Patrick Massot (Jun 27 2018 at 14:13):

Indeed having the subsets as fields instead of parameters may be enough to do the trick

#### Patrick Massot (Jun 27 2018 at 14:15):

I guess this is closer in spirit to the option a type than totalizing functions

#### Reid Barton (Jun 27 2018 at 14:16):

You might also want to check out roption and the data.pfun module

#### Reid Barton (Jun 27 2018 at 14:17):

But the main point is that for a computer, everything is hard, even these utterly trivial notions like "bijection between a subset of a and a subset of b".

#### Reid Barton (Jun 27 2018 at 14:18):

It helps to decompose the problem into pieces, so you are not thinking about manifolds when trying to define the composition of partial bijections. Of course this concept is not foreign to mathematicians, but here the pieces are much smaller than we are used to.

#### Patrick Massot (Jun 27 2018 at 14:20):

Yes I noticed all this (but noticing doesn't make it easy to use Lean)

#### Reid Barton (Jun 27 2018 at 14:20):

Once you have settled on the right interface for pequiv, the choice of implementation is not so important

#### Patrick Massot (Jun 27 2018 at 14:20):

I'll look at roption and pfun

#### Reid Barton (Jun 27 2018 at 14:23):

Something that may not be obvious from the pfun module is that because roption is a monad, you get a composition operation (a -> roption b) -> (b -> roption c) -> (a -> roption c) for free

#### Reid Barton (Jun 27 2018 at 14:28):

Apparently it doesn't really have a name in Lean aside from  >=>

#### Patrick Massot (Jun 27 2018 at 14:29):

I hope I'll be able to avoid this kind of notations...

#### Reid Barton (Jun 27 2018 at 14:29):

Again, only a question of implementation

#### Reid Barton (Jun 27 2018 at 14:29):

Of course for pequiv, you can choose whichever notation you like

#### Reid Barton (Jun 27 2018 at 14:32):

By the way, even though you don't care about constructiveness, I think things will be easier in the long run if you keep the maps in both directions as data in a bijection

#### Patrick Massot (Jun 27 2018 at 14:33):

as in using equiv rather than bijective you mean?

#### Reid Barton (Jun 27 2018 at 14:33):

Otherwise, when defining the canonical manifold structure on R^n for example, I think the transition maps will turn out to be something like lam x, classical.choice (\ex y, y = x) rather than lam x, x

Exactly

#### Sebastien Gouezel (Jun 27 2018 at 14:43):

def inverse_on  (U : set α) (f : α → β) : β → α :=
λ b, if h : b ∈ f '' U then classical.some h else default α


and having the injectivity as an assumption in your lemma inverse_on_spec. So that inverse_on is really taking as argument a function, and not a proof: formulas with inverse_on U f should be much more understandable than inverse_on H where you don't remember what H is. (This is really an implementation detail, everything is clearly equivalent, but still aiming at readability is always good!)

#### Reid Barton (Jun 27 2018 at 14:44):

If you keep track of both directions, then you can always produce the inverse using bijective and "unique choice" whenever it would be less convenient to provide it manually. But if you throw away the inverse direction and only keep the Prop of bijectivity, you can only recover the inverse function up to propositional equality. Then you may be faced with proving some equality these reconstructed inverses, where if you had kept the original inverses the proof would just be rfl

#### Patrick Massot (Jun 27 2018 at 14:46):

Thanks to both of you, this is all very interesting. I'll keep on working on the totalization path until I can define manifolds modulo the definition of smooth maps (it looks like it will work). But then I'll try to redo everything using the pequiv idea, and compare.

#### Patrick Massot (Jun 27 2018 at 14:48):

The definition of inverse_on without injectivity assumption really looks weird

#### Patrick Massot (Jun 27 2018 at 14:49):

I don't care at all about constructivism, and I don't mind using the axiom of choice. But this really doesn't feel like defining a function.

#### Sebastien Gouezel (Jun 27 2018 at 14:52):

I like my functions to be total :) So inverse_on is also total with this definition.
More seriously, in some settings, just taking one (any) preimage will make sense. For instance if you are working in a coarse geometry setting and you know that the preimages of any point have bounded diameter. This is the way one inverts quasi-isometries.

#### Kevin Buzzard (Jun 27 2018 at 14:52):

The axiom of choice is a pain to use in practice, because you need to keep track of random proof terms. I had two types X and Y in bijection recently, with a computable map X -> Y and a noncomptable map Y -> X, and after failing to construct something of type equiv X Y directly because of proof terms giving me problems I just proved X->Y was a bijection and then invoked equiv.of_bijection. Working with the axiom of choice can be a pain. Basically if you invoke it twice then there's no guaranteeing you got the same answer twice, so you can only invoke it once and then you have to keep a very careful track of where you invoked it and what you got.

#### Sebastien Gouezel (Jun 27 2018 at 14:54):

The idea would be that you never ever come back to the definition of inverse_on, but only use the two lemmas saying that f (inverse_on U f y) = y if y \in f''(U), and that inverse_on U f( f x) = x if x \in U and f is injective on U.

#### Patrick Massot (Jun 27 2018 at 14:56):

My inverse_on_spec is the conjunction of these two statements

#### Sebastien Gouezel (Jun 27 2018 at 14:56):

Yes, but for one of them you don't need the injectivity.

#### Patrick Massot (Jun 27 2018 at 14:57):

Sure. But I needed injectivity in the definition for psychological confort.

:)

#### Sebastien Gouezel (Jun 27 2018 at 14:57):

Go for the minimal assumptions. It will simplify your proofs if there are less assumptions to check!

#### Patrick Massot (Jun 27 2018 at 15:52):

I noticed Mario sometimes goes for biconditional statements in this situation. It indeed feels weird.

#### Patrick Massot (Jun 27 2018 at 15:53):

I will need a more precise stub for smoothness if I want to prove that equivalence of atlases is an equivalence relation...

#### Johannes Hölzl (Jul 02 2018 at 07:57):

inverse_on is inv_fun_on in logic/function.lean. For surjective functions there is also surj_inv (there the range doesn't need to be inhabited).

#### Patrick Massot (Jul 02 2018 at 09:38):

Thanks! I completely failed to see that file. I still don't understand the criterion separating stuff in data/set/function.lean and logic/function.lean.

#### Mario Carneiro (Jul 02 2018 at 09:44):

I would say that the difference is the use of sets

#### Patrick Massot (Jul 02 2018 at 09:44):

There are sets everywhere in both

#### Mario Carneiro (Jul 02 2018 at 09:45):

logic.function does not import data.set.basic

#### Mario Carneiro (Jul 02 2018 at 09:45):

so the only set stuff is what is available in core

#### Patrick Massot (Jul 02 2018 at 09:46):

Would putting everything in the same file create dependency issues?

yes

#### Mario Carneiro (Jul 02 2018 at 09:47):

although it is likely that inv_fun_on can be moved to set safely

#### Mario Carneiro (Jul 02 2018 at 09:48):

I like to think of the logic directory as covering more or less the "pure type theory" part of lean, just functions and pis and such

Last updated: May 09 2021 at 10:11 UTC