The non-Galois cubic ℚ₅(∛5)

Adjoining a root of the Eisenstein polynomial X³ − 5 to ℚ₅ gives a totally ramified cubic extension ℚ₅(∛5). It is not Galois: a nontrivial ℚ₅-automorphism would send ∛5 to ζ ∛5 for a primitive cube root of unity ζ, and ζ, a root of the irreducible quadratic X² + X + 1 over ℚ₅ (since −3 is not a square in ℚ₅), would generate a quadratic subfield of a cubic extension. So its automorphism group is trivial, of order 1 < 3 = [ℚ₅(∛5) : ℚ₅].

This makes ℚ₅(∛5) the standard instance of a finite layer of p-adic fields whose automorphism group is finite but smaller than its degree. On such a layer the rational decomposition A(L) ⊗ ℚ_p ≃ ℚ_p[Gal(L/K)]^N ⊕ ℚ_p of the completed multiplicative module fails: here the two ℚ₅-dimensions are [L : ℚ₅] + 1 = 4 and N · #Aut(L) + 1 = 2 (TauCeti.not_nonempty_padicCompletionUnits_tensorRat_linearEquiv_of_card_lt). The field is an explicit witness that the Galois hypothesis of that decomposition cannot be replaced by finiteness of the automorphism group.

Main definitions

• TauCeti.NonGaloisCubic: the field ℚ₅(∛5).
• TauCeti.NonGaloisCubic.cbrtFive: the cube root of 5 generating it.

Main results

• TauCeti.NonGaloisCubic.finrank_eq_three: [ℚ₅(∛5) : ℚ₅] = 3.
• TauCeti.NonGaloisCubic.eq_one_of_pow_three_eq_one: ℚ₅(∛5) has no nontrivial cube root of unity.
• TauCeti.NonGaloisCubic.subsingleton_algEquiv: the automorphism group of ℚ₅(∛5)/ℚ₅ is trivial, so TauCeti.NonGaloisCubic.natCard_algEquiv_lt_finrank and TauCeti.NonGaloisCubic.not_isGalois.
• TauCeti.NonGaloisCubic.not_nonempty_padicCompletionUnits_tensorRat_linearEquiv: the rational decomposition of A(ℚ₅(∛5)) as ℤ₅[Aut]-module fails.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (7.4.4).
• J.-P. Serre, Local Fields, Chapter I, §6.

instance TauCeti.NonGaloisCubic.factPrimeFive : Fact (Nat.Prime 5)

The prime 5, as a Fact, so that ℚ_[5] can be written.

def TauCeti.NonGaloisCubic : Type

The field ℚ₅(∛5), obtained from ℚ₅ by adjoining a root of X³ − 5.

theorem TauCeti.NonGaloisCubic.factIrreducible : Fact (Irreducible (Polynomial.X ^ 3 - Polynomial.C 5))

X³ − 5 is irreducible over ℚ₅: it is Eisenstein at 5.

@[instance_reducible]

noncomputable instance TauCeti.NonGaloisCubic.instField : Field NonGaloisCubic

@[instance_reducible]

noncomputable instance TauCeti.NonGaloisCubic.instAlgebraPadicOfNatNat : Algebra ℚ_[5] NonGaloisCubic

instance TauCeti.NonGaloisCubic.instFiniteDimensionalPadicOfNatNat : FiniteDimensional ℚ_[5] NonGaloisCubic

instance TauCeti.NonGaloisCubic.instCharZero : CharZero NonGaloisCubic

noncomputable def TauCeti.NonGaloisCubic.cbrtFive : NonGaloisCubic

The cube root ∛5 of 5 in ℚ₅(∛5), the class of X.

@[simp]

theorem TauCeti.NonGaloisCubic.cbrtFive_pow_three : cbrtFive ^ 3 = 5

The cube of ∛5 is 5.

theorem TauCeti.NonGaloisCubic.finrank_eq_three : Module.finrank ℚ_[5] NonGaloisCubic = 3

ℚ₅(∛5) is a cubic extension of ℚ₅.

theorem TauCeti.NonGaloisCubic.eq_one_of_pow_three_eq_one {ζ : NonGaloisCubic} (hζ : ζ ^ 3 = 1) : ζ = 1

ℚ₅(∛5) contains no nontrivial cube root of unity: such a root would generate a quadratic subfield of a cubic extension.

theorem TauCeti.NonGaloisCubic.apply_cbrtFive (σ : Gal(NonGaloisCubic/ℚ_[5])) : σ cbrtFive = cbrtFive

Every ℚ₅-automorphism of ℚ₅(∛5) fixes ∛5, since the only cube root of unity in ℚ₅(∛5) is 1.

instance TauCeti.NonGaloisCubic.subsingleton_algEquiv : Subsingleton Gal(NonGaloisCubic/ℚ_[5])

The automorphism group of ℚ₅(∛5)/ℚ₅ is trivial.

theorem TauCeti.NonGaloisCubic.natCard_algEquiv_lt_finrank : Nat.card Gal(NonGaloisCubic/ℚ_[5]) < Module.finrank ℚ_[5] NonGaloisCubic

The automorphism group of ℚ₅(∛5)/ℚ₅ has order 1, less than the degree 3.

theorem TauCeti.NonGaloisCubic.not_isGalois : ¬IsGalois ℚ_[5] NonGaloisCubic

ℚ₅(∛5)/ℚ₅ is not Galois.

theorem TauCeti.NonGaloisCubic.not_nonempty_padicCompletionUnits_tensorRat_linearEquiv : ¬Nonempty (TensorProduct ℤ_[5] (Additive ↥(padicCompletionUnits 5 NonGaloisCubic)) ℚ_[5] ≃ₗ[MonoidAlgebra ℤ_[5] Gal(NonGaloisCubic/ℚ_[5])] TensorProduct ℤ_[5] ((Fin 1 → MonoidAlgebra ℤ_[5] Gal(NonGaloisCubic/ℚ_[5])) × MonoidAlgebra ℤ_[5] Gal(NonGaloisCubic/ℚ_[5]) ⧸ RingHom.ker (MonoidAlgebra.augmentation ℤ_[5] Gal(NonGaloisCubic/ℚ_[5]))) ℚ_[5])

The rational decomposition fails on the non-Galois cubic. A(ℚ₅(∛5)) ⊗ ℚ₅ is not ℤ₅[Aut]-isomorphic to (ℤ₅[Aut]^1 × ℤ₅[Aut] ⧸ I) ⊗ ℚ₅, for Aut the (trivial) automorphism group of ℚ₅(∛5)/ℚ₅ and I its augmentation ideal: the two sides have ℚ₅-dimensions 3 + 1 = 4 and 1 · 1 + 1 = 2.