atlases

Stream: maths

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Johan Commelin]

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]

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

[Chris Hughes]

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)⟩

[Patrick Massot]

Maybe

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Chris Hughes]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

the equiv namespace never ended :)

[Kenny Lau]

equiv.set.range

[Patrick Massot]

Oh, that's nasty

[Patrick Massot]

thanks Kenny

[Patrick Massot]

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

[Patrick Massot]

it seems the match started already

[Sebastien Gouezel]

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]

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]

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

[Patrick Massot]

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]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

It's purely an artefact of the type theoretic foundations

[Sebastien Gouezel]

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]

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]

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]

Do you have the same crazyness in Isabelle then?

[Sebastien Gouezel]

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]

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

[Sebastien Gouezel]

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 :)

[Patrick Massot]

thanks

[Sebastien Gouezel]

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]

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]

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]

I want submanifolds of manifolds to be manifolds

[Patrick Massot]

But I'll try this total function road

[Sebastien Gouezel]

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]

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

[Sebastien Gouezel]

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]

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]

thank you very much for this conversation

[Patrick Massot]

good night!

[Patrick Massot]

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]

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]

What would be that vocabulary?

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Patrick Massot]

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

[Reid Barton]

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]

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

[Patrick Massot]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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

[Patrick Massot]

I'll look at roption and pfun

[Reid Barton]

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]

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

[Patrick Massot]

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

[Reid Barton]

Again, only a question of implementation

[Reid Barton]

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

[Reid Barton]

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]

as in using equiv rather than bijective you mean?

[Reid Barton]

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

[Reid Barton]

Exactly

[Sebastien Gouezel]

What about defining rather

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]

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]

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]

The definition of inverse_on without injectivity assumption really looks weird

[Patrick Massot]

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]

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]

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]

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]

My inverse_on_spec is the conjunction of these two statements

[Sebastien Gouezel]

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

[Patrick Massot]

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

[Patrick Massot]

:)

[Sebastien Gouezel]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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]

I would say that the difference is the use of sets

[Patrick Massot]

There are sets everywhere in both

[Mario Carneiro]

logic.function does not import data.set.basic

[Mario Carneiro]

so the only set stuff is what is available in core

[Patrick Massot]

Would putting everything in the same file create dependency issues?

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Mario Carneiro]

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