Zulip Chat Archive

Stream: new members

Topic: Invertible function


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 30 2020 at 17:07):

Then there is mul_equiv for homomorphism

view this post on Zulip Johan Commelin (Jun 30 2020 at 17:07):

And add_equiv and ring_equiv etc...

view this post on Zulip Johan Commelin (Jun 30 2020 at 17:09):

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

view this post on Zulip Johan Commelin (Jun 30 2020 at 17:09):

Looks relevant

view this post on Zulip 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").

view this post on Zulip 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] :

?

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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 _.

view this post on Zulip Johan Commelin (Jun 30 2020 at 17:19):

Then click the "skeleton" option

view this post on Zulip Bryan Gin-ge Chen (Jun 30 2020 at 17:20):

Does src#homeomorph.mul_right help?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Jun 30 2020 at 17:30):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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 :)

view this post on Zulip Heather Macbeth (Jun 30 2020 at 22:50):

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


Last updated: May 14 2021 at 22:15 UTC