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

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:

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 $A \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 $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 (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 evenwantto 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