The algebraic extensions of ℝ

Stream: Is there code for X?

[Michael Stoll]

Do we have some form of the following?

import Mathlib

example {F : Type*} [Field F] [Algebra ℝ F] (h : (algebraMap ℝ F).IsIntegral) :
    Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ) := sorry

(Of course, we do have the fact that ℂ is algebraically closed and has dimension 2 over ℝ, from which one can certainly put together a proof, but I'd be surprised if this was missing...)

[Junyan Xu]

Quick proof:

import Mathlib.FieldTheory.IsAlgClosed.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
import Mathlib.Data.Complex.FiniteDimensional
import Mathlib.Analysis.Complex.Polynomial.Basic

theorem nonempty_algEquiv_or_of_finrank_algClosure_eq_two
    {F F' : Type*} (E : Type*) [Field F] [Field F'] [Field E] [Algebra F F'] [Algebra F E]
    [Algebra.IsAlgebraic F E] [IsAlgClosed F'] (h : Module.finrank F F' = 2) :
    Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F') := by
  have emb : E →ₐ[F] F' := IsAlgClosed.lift
  have e := AlgEquiv.ofInjectiveField emb
  have := Subalgebra.isSimpleOrder_of_finrank h
  obtain h | h := IsSimpleOrder.eq_bot_or_eq_top emb.range <;> rw [h] at e
  exacts [.inl ⟨e.trans <| Algebra.botEquiv ..⟩, .inr ⟨e.trans Subalgebra.topEquiv⟩]

example {F : Type*} [Field F] [Algebra ℝ F] (h : (algebraMap ℝ F).IsIntegral) :
    Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ) :=
  have : Algebra.IsIntegral ℝ F := ⟨h⟩
  nonempty_algEquiv_or_of_finrank_algClosure_eq_two F Complex.finrank_real_complex

[Eric Wieser]

I think there are a number of zulip threads about this

[Eric Wieser]

#Is there code for X? > Finite extension over Real @ 💬

[Junyan Xu]

My proof is the same as #Is there code for X? > Finite extension over Real @ 💬 :)

[Michael Stoll]

@Junyan Xu Can you PR it to Mathlib?

[Eric Wieser]

Is it also true for docs#StarAlgEquiv ?

[Junyan Xu]

@Michael Stoll #25332
I'm only adding the first lemma as it fits in an existing file and the second is a direct application of it.

[Jireh Loreaux]

Eric, what is your instance of Star F?

[Eric Wieser]

I guess I'm working on the speculation that there is only one possible ring-compatible star operation on the reals / complexes

[Junyan Xu]

Hmm, I just found unicode in a decl name Polynomial.Gal.splits_ℚ_ℂ ported from Lean 3 ... it's an instance though.

[Kevin Buzzard]

The complexes has uncountably many algebraic automorphisms most of which do not commute with complex conjugation so the star is not an algebraically intrinsic function. But if it has to fix the reals then you're ok

[Eric Wieser]

You're still in trouble I guess because you could have "the complex numbers where conjugation is the identity"

[Michael Stoll]

Kevin Buzzard said:

The complexes has uncountably many algebraic automorphisms most of which do not commute with complex conjugation

I had to remember this when I was trying to prove that an absolute value on the reals that restricts to the archimedean absolute value on the rationals is the standard absolute value :smiley: It turns out there are lots of such absolute values on the reals (but only one that gives a complete space). (You can even put $p$-adic absolute values on the reals via $\mathbb{R} \to \mathbb{C} \stackrel{\cong}{\to} \bar{\mathbb{Q}}_p$, the second map being an isomorphism of abstract fields...)

[Kevin Buzzard]

Right, doesn't the proof that you can't chop up a square into an odd number of triangles with the same area rely on this?

[David J. Webb]

Well that sent me down a rabbit hole... incredible that in this instance, you seem to need number theory to do geometry!