Zulip Chat Archive

Stream: Is there code for X?

Topic: Automorphisms of ℂ


view this post on Zulip Alena Gusakov (Dec 31 2020 at 06:50):

This might be a stretch, but is there a proof of the existence of wild automorphisms of the complex numbers assuming the axiom of choice? Or any work being done with that intention?

view this post on Zulip Mario Carneiro (Dec 31 2020 at 06:53):

Well we do have the existence of bases on arbitrary vector spaces

view this post on Zulip Mario Carneiro (Dec 31 2020 at 06:53):

I forget how much more is needed to turn that into a field hom

view this post on Zulip Alena Gusakov (Dec 31 2020 at 06:58):

That's fair, I don't think I really understand the full proof yet anyway. I just thought it was a cool result and was wondering whether it would make for a good project, way out in the future, once I've gained a lot more experience with Lean and do actually understand the proof lol

view this post on Zulip Johan Commelin (Dec 31 2020 at 07:04):

We need a bit of stuff on transcendental field extensions, but I don't think that much is missing.

view this post on Zulip Johan Commelin (Dec 31 2020 at 07:04):

Once you have the concept of a transcendence basis, you are basically done.


Last updated: May 07 2021 at 21:10 UTC