Invertible function

Stream: new members

[Nicolò Cavalleri]

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]

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

[Johan Commelin]

Then there is mul_equiv for homomorphism

[Johan Commelin]

And add_equiv and ring_equiv etc...

[Johan Commelin]

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

[Johan Commelin]

Looks relevant

[Bryan Gin-ge Chen]

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]

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]

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]

@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]

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

[Johan Commelin]

Then click the "skeleton" option

[Bryan Gin-ge Chen]

Does src#homeomorph.mul_right help?

[Nicolò Cavalleri]

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]

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 $A \mapsto A^{-1}$ (for operators/matrices) is smooth, sounds like you will be using it?

[Nicolò Cavalleri]

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 $A \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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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