Complex conjugation in the absolute Galois group

Stream: Is there code for X?

[Stepan Nesterov]

How to define complex conjugation as an element of Field.absoluteGaloisGroup ℝ?
I tried showing that the algebraic closure of ℝ is isomorphic to ℂ by using
example : AlgebraicClosure ℝ ≃ₐ[ℝ] ℂ := by exact?
but didn't get any results

[Junyan Xu]

import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

instance : IsAlgClosure ℝ ℂ where
  isAlgClosed := inferInstance
  isAlgebraic := inferInstance

noncomputable example : AlgebraicClosure ℝ ≃ₐ[ℝ] ℂ := IsAlgClosure.equiv ℝ _ _

[Riccardo Brasca]

Maybe we can generalize NumberField.IsCMField to consider the complex numbers. @Xavier Roblot what do you think? Of couse at some point one has to work with number fields, but maybe the very basic theory works in general

[Xavier Roblot]

I am not sure how much of it would work if we remove the NumberField assumption but I can have a look.

[Riccardo Brasca]

CharZero is surely OK

[Riccardo Brasca]

I mean, it's ok to assume it

[Junyan Xu]

Some naming inconsistency between docs#AlgEquiv.autCongr and docs#LinearEquiv.conj ... (had trouble finding the first one)

[Xavier Roblot]

Looks like the NumberField assumptions can be removed at some places. I'll have a closer look tomorrow

[Stepan Nesterov]

Riccardo Brasca said:

Maybe we can generalize NumberField.IsCMField to consider the complex numbers. Xavier Roblot what do you think? Of couse at some point one has to work with number fields, but maybe the very basic theory works in general

My ultimate goal was to define a complex conjugation as an element of the absolute Galois group of $\mathbb{Q}$, by doing this:

noncomputable def complexConjugationReal : Γ ℝ := sorry

noncomputable def complexConjugation : Γ ℚ := (Field.absoluteGaloisGroup.mapAux (Rat.castHom ℝ))
  complexConjugationReal

Are you proposing that mathlib should know $\overline{\mathbb{Q}}$ is a CM-field in some generalised sense and therefore should have a complex conjugation?

[Riccardo Brasca]

I am just saying that trivially the complex numbers are a quadratic extension of their maximal real subfield (the reals!), and yes, the same is true for the algebraic numbers, so in this sense they are a "CM field", but it's just an observation, nothing really deep.

[Junyan Xu]

It would be reasonable to make algebraicClosure ℚ ℂ into a docs#StarSubalgebra.

import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.FieldTheory.AlgebraicClosure
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
noncomputable example : algebraicClosure ℚ ℂ ≃ₐ[ℚ] AlgebraicClosure ℚ :=
  IsAlgClosure.equiv ..

[Xavier Roblot]

Riccardo Brasca said:

I am just saying that trivially the complex numbers are a quadratic extension of their maximal real subfield (the reals!), and yes, the same is true for the algebraic numbers, so in this sense they are a "CM field", but it's just an observation, nothing really deep.

There is a problem though because, if I am not mistaken, I do not think that ℝ is totally real according to our definition. Recall that this mean that all φ : ℝ →+* ℂ are contained in the image of ℝ in ℂ and I don't think that it's true if you don't assume in addition that φ is continuous.

Proving that the algebraic closure of ℚ is CM should be possible though.

[Riccardo Brasca]

Ouch

[Riccardo Brasca]

Your 100% right, the reals are not totally real

[Kevin Buzzard]

And the algebraic closure of Q should surely not be CM, the point about CM fields is that there's a unique sensible notion of complex conjugation, and this is far from true in Qbar.

[Xavier Roblot]

Yes, indeed. Sorry, I was thinking about $\bar{\mathbb{Q}}^{ab}$

[Xavier Roblot]

(Wait, why is math mode not working here?)

[Ruben Van de Velde]

I assume $$\bar$$

[Xavier Roblot]

Indeed, thanks. I fixed it.

[Riccardo Brasca]

Well, maybe it's just not worth it

[Xavier Roblot]

Well, I have already started to work on it so let's see how far I can get

[Xavier Roblot]

Ok, so this is what I can prove

example (K : Type*) [Field K] [CharZero K] (S : Set ℕ) (hS : ∃ n ∈ S, 2 < n)
    [IsCyclotomicExtension S ℚ K] :
    IsCMField K :=

[Xavier Roblot]

(I guess that doesn't help Stepan at all :sweat_smile: )

[Riccardo Brasca]

Well, free to open a PR for that! We already have a weak version in flt-regular, but this is surely a reasonable instance

[Kevin Buzzard]

It's not an instance because of hS.

Taylor likes the predicate "totally real or CM" (which AFAIK we don't have), which is equivalent to "well-defined complex conjugation", and it could be an instance for that.

[Kevin Buzzard]

(Taylor calls it "CM field" but this is not a standard use of the term)