Finite extension over Real

Stream: Is there code for X?

[Edison Xie]

Do we have the theorem that for any finite extension over ℝ is either ℝ or ℂ ?

[Daniel Weber]

@loogle Algebra, FiniteDimensional, Real

[loogle]

:shrug: nothing found

[Daniel Weber]

Doesn't look like it

[Riccardo Brasca]

Even if the literal result is maybe missing, we can surely prove it very quickly, the math is there

[Daniel Weber]

@loogle FiniteDimensional, IsAlgebraicClosure

[loogle]

:exclamation: unknown identifier 'IsAlgebraicClosure'
Did you mean FiniteDimensional, "IsAlgebraicClosure"?

[Riccardo Brasca]

Let me see if I can prove it quickyl

[Riccardo Brasca]

Is this statement what you want?

import Mathlib

variable (K : Type) [Field K] [Algebra ℝ K] [FiniteDimensional ℝ K]

example : Nonempty (ℝ ≃ₐ[ℝ] K) ∨ Nonempty (ℂ ≃ₐ[ℝ] K) := sorry

[Kevin Buzzard]

You could state it using ROrCLike :-)

[Riccardo Brasca]

Yeah, that is another possibility. Anyway here is a proof

import Mathlib

variable (K : Type*) [Field K] [Algebra ℝ K] [FiniteDimensional ℝ K]

open Polynomial Module Algebra Subalgebra

example : Nonempty (K ≃ₐ[ℝ] ℝ) ∨ Nonempty (K ≃ₐ[ℝ] ℂ) := by
  obtain ⟨α, hα⟩ := Field.exists_primitive_element ℝ K
  have halg : IsIntegral ℝ α := IsIntegral.isIntegral α
  match h : (minpoly ℝ α).natDegree with
  | 0 => simpa [h] using (minpoly.natDegree_pos halg).ne'
  | 1 =>
    left
    refine ⟨IntermediateField.topEquiv.symm.trans ?_⟩
    rw [← hα, IntermediateField.adjoin_simple_eq_bot_iff.2 (minpoly.natDegree_eq_one_iff.1 h)]
    exact IntermediateField.botEquiv ℝ K
  | 2 =>
    right
    let φ : K →ₐ[ℝ] ℂ := IsAlgClosed.lift
    refine ⟨AlgEquiv.ofBijective φ ⟨RingHom.injective _, (range_top_iff_surjective _).1 ?_⟩⟩
    refine eq_of_le_of_finrank_le le_top ?_
    by_contra! H
    change _ < finrank ℝ (⊤ : Submodule ℝ ℂ) at H
    simp only [finrank_top, Complex.finrank_real_complex] at H
    have : finrank ℝ φ.range = 1 := by
      refine le_antisymm (Nat.le_of_lt_succ H) (Nat.succ_le_of_lt (finrank_pos_iff.2 ?_))
      infer_instance
    rw [← bot_eq_top_iff_finrank_eq_one] at this
    have : ⟨φ α, Set.mem_range_self α⟩ ∈ (⊥ : Subalgebra ℝ φ.range) := this ▸ trivial
    obtain ⟨x, hx⟩ := mem_bot.1 this
    simp only [← Subtype.coe_inj, SubalgebraClass.coe_algebraMap, Complex.coe_algebraMap] at hx
    simp [← minpoly.algHom_eq φ (RingHom.injective _) α, ← hx, ← Complex.coe_algebraMap,
      minpoly.natDegree_eq_one_iff.2 (Set.mem_range_self x)] at h
  | n+3 => linarith [(minpoly.irreducible halg).natDegree_le_two]

[Riccardo Brasca]

I guess Frobenius theorem should also be doable

[Riccardo Brasca]

The

  have : P.natDegree = 1 ∨ P.natDegree = 2 := by
    match h : P.natDegree with
    | 0 => simpa [h] using (minpoly.natDegree_pos halg).ne'
    | 1 => exact Or.inl rfl
    | 2 => exact Or.inr rfl
    | n+3 => linarith

makes me a little sad. Is there a way to golf it with fin_cases or something else?

[Riccardo Brasca]

Well, maybe I can just to the long proof inside the various cases

[Daniel Weber]

There is interval_cases

[Riccardo Brasca]

I've updated the above proof working directly inside the match.

[Daniel Weber]

Another approach might be to show that K must be equivalent to an IntermediateField ℝ ℂ and then use docs#IsGalois.intermediateFieldEquivSubgroup and the fact that the fixing subgroup of ℂ is $C_2$, but I'm not sure if that'll be easier

[Riccardo Brasca]

The above proof is really simple, and very similar to what we'd do on paper: K is generated by α, and the degree of the minimal polynomial of α must be 1 or 2. The first case is done via minpoly.natDegree_eq_one_iff and IntermediateField.adjoin_simple_eq_bot_iff. The second one is a little more annoying, the fasted way I found is to embed K in ℂ and prove that the embedding is also surjective. This is because if the dimension of the image is 1 then any element is real, and so the image of α would have minimal polynomial of degree 1.

[Edison Xie]

Thanks guys, really helpful! Appreciate the proof! :)

[Andrew Yang]

Another approach:

import Mathlib

variable (K : Type*) [Field K] [Algebra ℝ K] [FiniteDimensional ℝ K]

open Polynomial Module Algebra Subalgebra

lemma isSimpleOrder_subalgebra_of_finrank_eq_two
    {L K} [Field K] [Ring L] [Nontrivial L] [Algebra K L] (h : finrank K L = 2) :
    IsSimpleOrder (Subalgebra K L) := by
  have : Module.Finite K L := finite_of_finrank_eq_succ h
  have : Nontrivial (Subalgebra K L) :=
    ⟨⊥, ⊤, bot_eq_top_iff_finrank_eq_one (F := K) (E := L).not.mpr (by simp [h])⟩
  constructor
  intros S
  have : finrank K S ∈ Finset.Ioc 0 2 := Finset.mem_Ioc.mpr ⟨finrank_pos, h ▸ S.toSubmodule.finrank_le⟩
  match h' : finrank K S with
  | 0 => exact (finrank_pos.ne' h').elim
  | 1 => exact .inl (Subalgebra.finrank_eq_one_iff.mp h')
  | 2 => exact .inr (Subalgebra.eq_of_le_of_finrank_eq le_top ((h'.trans h.symm).trans (finrank_top _ _).symm))
  | n + 3 => simpa using h'.symm.trans_le (S.toSubmodule.finrank_le.trans_eq h)

instance : IsSimpleOrder (Subalgebra ℝ ℂ) :=
  isSimpleOrder_subalgebra_of_finrank_eq_two Complex.finrank_real_complex

example : Nonempty (K ≃ₐ[ℝ] ℝ) ∨ Nonempty (K ≃ₐ[ℝ] ℂ) := by
  let φ : K →ₐ[ℝ] ℂ := IsAlgClosed.lift
  refine (IsSimpleOrder.eq_bot_or_eq_top φ.range).imp ?_ ?_
  · exact (⟨(AlgEquiv.ofInjectiveField φ).trans <| · ▸ botEquiv ℝ ℂ⟩)
  · exact (⟨(AlgEquiv.ofInjectiveField φ).trans <| · ▸ topEquiv⟩)

(we probably want the first two in mathlib)

[Daniel Weber]

I think the last result should also be in Mathlib, perhaps in the docs#RCLike form Kevin suggested

[Ruben Van de Velde]

Weren't we going to have a Prop version of ROrCLike?

[Daniel Weber]

There's docs#IsRCLikeNormedField, but it requires an existing normed field structure