Continuous complex ring hom

Stream: Is there code for X?

[Xavier Roblot]

Do we have the fact that the only continuous ring homomorphisms from ℂ to ℂ are the identity and the complex conjugation?

[Ruben Van de Velde]

Hmm, I think I've seen that proved here on zulip, but not sure about mathlib

[Eric Wieser]

I think I've seen that too

[Eric Wieser]

Possibly in terms of isometries instead of continuity

[Kevin Buzzard]

I remember once being very confused by the fact that the only ring homomorphism from $\R$ to $\R$ is the identity (no continuity assumption needed; the image of a square is a square and hence the image of something nonnegative is nonnegative, so order is preserved, as are the rationals), but that there were uncountably many isomorphisms from $\mathbb{C}$ to $\mathbb{C}$ (dropping continuity has a major effect). It felt like it should contradict Galois theory, but of course it doesn't.

[Adam Topaz]

There is a p-adic analogue as well, using the fact that the valuation ring of $\mathbb{Q}_p$ is uniformly definable with no parameters in the ring language ;-) It's a nice exercise using Hensel's lemma to show this :)

[Kevin Buzzard]

Here's a Hensel-free proof that if $K/\mathbb{Q}_p$ is finite then the ring automorphisms of $K$ are all continuous (and hence fix $\mathbb{Q}_p$): the units of (the integers of) $K$ are precisely the elements of $K$ which admit $n$ th roots for infinitely many $n$; an element of $K$ is close to 1 iff it's a $p^N(q-1)$ th power of a unit (with $q$ the size of the residue field) and hence any ring hom maps small things to small things. This is like an unanalogue though, because there's a finite extension of $\mathbb{R}$ which has automorphisms which aren't continuous.

[Adam Topaz]

Is that really Hensel-free?

[Adam Topaz]

How do you know that the principal units have enough roots without Hensel?

[Kevin Buzzard]

exp and log ;-)

[Adam Topaz]

Oh yeah, sure

[Adam Topaz]

You could argue that that's Hensel for $X^n-a$

[Xavier Roblot]

Coming back to the complex case, would it be interesting to add this result to mathlib? I think I'll need something along these lines to prove that two complex embeddings of a number field define the same infinite place iff they are equal or complex conjugates.

[Adam Topaz]

Yeah I think it's worth having such a lemma in mathlib!

[Kevin Buzzard]

How are you defining infinite places? Do you know about @María Inés de Frutos Fernández 's work on adeles of number fields?

[Xavier Roblot]

Kevin Buzzard said:

How are you defining infinite places? Do you know about María Inés de Frutos Fernández 's work on adeles of number fields?

Infinite places are defined by composing the embeddings of $K$ into $\mathbb{C}$, with $K$ our number field , with the complex absolute value. Since we can consider embeddings of $K$ into any alg. closed field, we could define finite places in a similar way.

I heard of the impressive work of @María Inés de Frutos Fernández . We should definitely coordinate at same point so that everything gets together nicely.

[Xavier Roblot]

Kevin Buzzard said:

I remember once being very confused by the fact that the only ring homomorphism from $\R$ to $\R$ is the identity (no continuity assumption needed; the image of a square is a square and hence the image of something nonnegative is nonnegative, so order is preserved, as are the rationals).

Well, I made a PR for that #16049. I'll work on the complex case when I have the time but since I have a 15h flight coming soon, it won't be before a couple of days.