Zulip Chat Archive

Stream: new members

Topic: Invertible function


Nicolò Cavalleri (Jun 30 2020 at 17:04):

What is the correct way in Mathlib to say that a function is invertible and to say something about its inverse? Suppose fore example I wanted to state the lemma that, given a topological group, right multiplication is a homeomorphism, how do I express it?

Johan Commelin (Jun 30 2020 at 17:07):

There is equiv which records f, it's inverse and the proofs that both compositions are id.

Johan Commelin (Jun 30 2020 at 17:07):

Then there is mul_equiv for homomorphism

Johan Commelin (Jun 30 2020 at 17:07):

And add_equiv and ring_equiv etc...

Johan Commelin (Jun 30 2020 at 17:09):

src/topology/homeomorph.lean:13:structure homeomorph (α : Type*) (β : Type*) [topological_space α] [topological_space β]

Johan Commelin (Jun 30 2020 at 17:09):

Looks relevant

Bryan Gin-ge Chen (Jun 30 2020 at 17:11):

src#homeomorph

This reminds me, I've always wondered why this wasn't just called "homeo". Is "homeomorph" a more common abbreviation outside the US?

edit: I guess Johannes added it here and we've just stuck with it. I bring this up because in e.g. blackboard talks, I think I've only ever seen people write "homeo" (similarly "diffeo").

Nicolò Cavalleri (Jun 30 2020 at 17:17):

Johan Commelin said:

src/topology/homeomorph.lean:13:structure homeomorph (α : Type*) (β : Type*) [topological_space α] [topological_space β]

Well I am aware of homeomorph but I am not really sure how to use it to state this lemma! Like what should I write after this

lemma right_mul_is_homeomorph (G : Type*) [topological_space G] [group G] [topological_group G] :

?

Nicolò Cavalleri (Jun 30 2020 at 17:18):

Bryan Gin-ge Chen said:

src#homeomorph

This reminds me, I've always wondered why this wasn't just called "homeo". Is "homeomorph" a more common abbreviation outside the US?

I think in the UK homeo is the most used abbreviation as well

Johan Commelin (Jun 30 2020 at 17:19):

@Nicolò Cavalleri It is a defintion instead of a lemma (I know this is confusing), because you are recording data (the inverse function).

Johan Commelin (Jun 30 2020 at 17:19):

So you can continue by
:= _ and then click on the :bulb: if you put your cursor on the _.

Johan Commelin (Jun 30 2020 at 17:19):

Then click the "skeleton" option

Bryan Gin-ge Chen (Jun 30 2020 at 17:20):

Does src#homeomorph.mul_right help?

Nicolò Cavalleri (Jun 30 2020 at 17:22):

Bryan Gin-ge Chen said:

Does src#homeomorph.mul_right help?

Yes actually it does I probably did not see it because I was looking for a lemma

Heather Macbeth (Jun 30 2020 at 17:24):

Nicolò Cavalleri said:

What is the correct way in Mathlib to say that a function is invertible and to say something about its inverse? Suppose fore example I wanted to state the lemma that, given a topological group, right multiplication is a homeomorphism, how do I express it?

By the way, I am currently working towards the fact that the map AA1A \mapsto A^{-1} (for operators/matrices) is smooth, sounds like you will be using it?

Nicolò Cavalleri (Jun 30 2020 at 17:27):

Heather Macbeth said:

Nicolò Cavalleri said:

What is the correct way in Mathlib to say that a function is invertible and to say something about its inverse? Suppose fore example I wanted to state the lemma that, given a topological group, right multiplication is a homeomorphism, how do I express it?

By the way, I am currently working towards the fact that the map AA1A \mapsto A^{-1} (for operators/matrices) is smooth, sounds like you will be using it?

Well actually right now I made up this example to write something simpler than what I am actually doing, but I will be working soon on matrix Lie groups so that could be cool for that!

Heather Macbeth (Jun 30 2020 at 17:29):

Maybe you would be interested in taking over a task that @Patrick Massot , @Johan Commelin and I were discussing : to put a topological group structure on the group of units of a topological ring

Heather Macbeth (Jun 30 2020 at 17:30):

Using the restriction of the product topology on [ring] x [ring]

Kevin Buzzard (Jun 30 2020 at 19:27):

Nicolò Cavalleri said:

Bryan Gin-ge Chen said:

Does src#homeomorph.mul_right help?

Yes actually it does I probably did not see it because I was looking for a lemma

@Nicolò Cavalleri equiv X Y is the type of inverse bijections f : X -> Y and g : Y -> X. Computer scientists prefer these to f : X -> Y plus a proof of bijective f (which would be a lemma) because a computable bijection might have a non-computable inverse. equiv is nothing to do with equivalence relations -- I mean, it _is_ an equivalence relation on types, but what I mean is that if you want to prove lemmas about equivalence relations you don't use equiv. It is still hard for me three years on to remember that def is sometimes what the CS people use for what I would call a lemma. You just have to think very precisely about what you're saying and see whether implicitly you are, or want to, define data. For example we sometimes say "theorem: G1 and G2 are isomorphic. Proof: consider the following canonical map from G1 to G2. Let's prove that it's an isomorphism...". In Lean that canonical map is a definition, and you don't even want to prove the theorem that G1 and G2 are isomorphic, you want to prove the stronger statement that the canonical map is an isomorphism.

Nicolò Cavalleri (Jun 30 2020 at 22:00):

Heather Macbeth said:

Maybe you would be interested in taking over a task that Patrick Massot , Johan Commelin and I were discussing : to put a topological group structure on the group of units of a topological ring

It does look very interesting even if right now I am working on a summer project that is taking all of my time and I am not sure I would have time for that! Maybe at the end of this project!

Nicolò Cavalleri (Jun 30 2020 at 22:00):

Kevin Buzzard said:

Nicolò Cavalleri said:

Bryan Gin-ge Chen said:

Does src#homeomorph.mul_right help?

Yes actually it does I probably did not see it because I was looking for a lemma

Nicolò Cavalleri equiv X Y is the type of inverse bijections f : X -> Y and g : Y -> X. Computer scientists prefer these to f : X -> Y plus a proof of bijective f (which would be a lemma) because a computable bijection might have a non-computable inverse. equiv is nothing to do with equivalence relations -- I mean, it _is_ an equivalence relation on types, but what I mean is that if you want to prove lemmas about equivalence relations you don't use equiv. It is still hard for me three years on to remember that def is sometimes what the CS people use for what I would call a lemma. You just have to think very precisely about what you're saying and see whether implicitly you are, or want to, define data. For example we sometimes say "theorem: G1 and G2 are isomorphic. Proof: consider the following canonical map from G1 to G2. Let's prove that it's an isomorphism...". In Lean that canonical map is a definition, and you don't even want to prove the theorem that G1 and G2 are isomorphic, you want to prove the stronger statement that the canonical map is an isomorphism.

Thanks! Your explanations are always very clear!

Heather Macbeth (Jun 30 2020 at 22:47):

Nicolò Cavalleri said:

Heather Macbeth said:

Maybe you would be interested in taking over a task that Patrick Massot , Johan Commelin and I were discussing : to put a topological group structure on the group of units of a topological ring

It does look very interesting even if right now I am working on a summer project that is taking all of my time and I am not sure I would have time for that! Maybe at the end of this project!

I mentioned it because it might be relevant to the project you mentioned -- it would give you the topological group structure on GL(n) for free :)

Heather Macbeth (Jun 30 2020 at 22:50):

But of course, feel free not to go down that rabbit hole ...


Last updated: Dec 20 2023 at 11:08 UTC