The maximal real subfield of a rational cyclotomic field

Let K be the n-th cyclotomic field over ℚ. Under Mathlib's identification IsCyclotomicExtension.Rat.galEquivZMod of Gal(K/ℚ) with (ℤ/nℤ)ˣ, the class -1 is the automorphism ζ ↦ ζ⁻¹, and every complex embedding of K turns it into complex conjugation. Its fixed field is therefore the maximal real subfield K⁺, and an element of K lies in K⁺ as soon as it is real under one complex embedding.

Under the correspondence IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar between intermediate fields of K / ℚ and groups of Dirichlet characters of level n, the maximal real subfield corresponds to the even characters: a character is trivial on the fixing subgroup {1, τ} of K⁺ exactly when χ (-1) = 1. This is the classical description of K⁺ as the field cut out by the even characters.

Main results

All results are in the namespace TauCeti.IsCyclotomicExtension.Rat.

• complexEmbedding_galEquivZMod_symm_neg_one_apply: the automorphism attached to -1 is complex conjugation under every complex embedding.
• galEquivZMod_symm_neg_one_apply_eq_self_iff: its fixed points are the maximal real subfield.
• mem_maximalRealSubfield_iff_star_eq: one complex embedding suffices to test membership in the maximal real subfield.
• toSubfield_intermediateFieldEquivSubgroupChar_symm_evenSubgroup: the even characters cut out the maximal real subfield.

References

• L. C. Washington, Introduction to Cyclotomic Fields, Chapter 3.

theorem TauCeti.IsCyclotomicExtension.Rat.complexEmbedding_galEquivZMod_symm_neg_one_apply (n : ℕ) [NeZero n] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (φ : K →+* ℂ) (x : K) : φ (((IsCyclotomicExtension.Rat.galEquivZMod n K).symm (-1)) x) = (starRingEnd ℂ) (φ x)

The automorphism of ℚ(ζₙ) attached to -1 is complex conjugation. Under every complex embedding φ, the automorphism ζ ↦ ζ⁻¹ corresponds to complex conjugation.

theorem TauCeti.IsCyclotomicExtension.Rat.galEquivZMod_symm_neg_one_apply_eq_self_iff (n : ℕ) [NeZero n] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (x : K) : ((IsCyclotomicExtension.Rat.galEquivZMod n K).symm (-1)) x = x ↔ x ∈ NumberField.maximalRealSubfield K

The fixed field of ζ ↦ ζ⁻¹ is the maximal real subfield. An element of ℚ(ζₙ) is fixed by the automorphism attached to -1 exactly when it is real under every complex embedding.

theorem TauCeti.IsCyclotomicExtension.Rat.mem_maximalRealSubfield_iff_star_eq (n : ℕ) [NeZero n] {K : Type u_1} [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (φ : K →+* ℂ) (x : K) : x ∈ NumberField.maximalRealSubfield K ↔ star (φ x) = φ x

One complex embedding detects the maximal real subfield of ℚ(ζₙ). An element lies in the maximal real subfield as soon as its image under a single complex embedding is real.

theorem TauCeti.IsCyclotomicExtension.Rat.toSubfield_fixedField_zpowers_galEquivZMod_symm_neg_one (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] : (IntermediateField.fixedField (Subgroup.zpowers ((IsCyclotomicExtension.Rat.galEquivZMod n K).symm (-1)))).toSubfield = NumberField.maximalRealSubfield K

The fixed field of the cyclic subgroup generated by ζ ↦ ζ⁻¹ is the maximal real subfield of the cyclotomic field.

theorem TauCeti.IsCyclotomicExtension.Rat.mem_intermediateFieldEquivSubgroupChar_fixedField_zpowers_iff (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [CommRing R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [IsAbelianGalois ℚ K] (σ : Gal(K/ℚ)) (χ : DirichletCharacter R n) : χ ∈ (IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar n K R) (IntermediateField.fixedField (Subgroup.zpowers σ)) ↔ χ ↑((IsCyclotomicExtension.Rat.galEquivZMod n K) σ) = 1

A character belongs to the character group of a cyclic fixed field exactly when it is trivial on the chosen generator.

theorem TauCeti.IsCyclotomicExtension.Rat.toSubfield_intermediateFieldEquivSubgroupChar_symm_evenSubgroup (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [CommRing R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [IsAbelianGalois ℚ K] : ((IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar n K R).symm (DirichletCharacter.evenSubgroup R n)).toSubfield = NumberField.maximalRealSubfield K

The even characters cut out the maximal real subfield. Under the correspondence between intermediate fields of ℚ(ζₙ) / ℚ and groups of Dirichlet characters of level n, the group of even characters corresponds to the maximal real subfield of ℚ(ζₙ).