The unramified quadratic extension ℚ₂(ζ₃)

The polynomial X² + X + 1 is irreducible over ℚ₂: a root would make -3 a square, although -3 is not a square modulo 8. Its root field is the cyclotomic extension ℚ₂(ζ₃), equipped here with the canonical nonarchimedean local-field structure extending that of ℚ₂.

The extension is unramified. Its distinguished root ζ₃ is integral, and the derivative 2ζ₃ + 1 has square -3, a unit in ℤ₂. Thus the simple-root criterion applies. In particular, the extension has exactly two 2-power roots of unity, and its arithmetic Frobenius has order two, so its Galois group is nontrivial.

Main definitions

• TauCeti.unramifiedQuadraticPoly: the polynomial X² + X + 1 over ℚ₂.
• TauCeti.UnramifiedQuadratic: its root field ℚ₂(ζ₃).
• TauCeti.UnramifiedQuadratic.zetaThree: the distinguished primitive cube root.

Main results

• TauCeti.unramifiedQuadraticPoly_irreducible: X² + X + 1 is irreducible over ℚ₂.
• TauCeti.UnramifiedQuadratic.finrank_eq_two: the root field has degree two.
• The instance TauCeti.IsUnramified ℚ_[2] TauCeti.UnramifiedQuadratic.
• TauCeti.localRootOfUnityOrder_two_unramifiedQuadratic: q(ℚ₂(ζ₃)) = 2.
• TauCeti.nontrivial_algEquiv_unramifiedQuadratic: the Galois group is nontrivial.

References

• J.-P. Serre, Local Fields, Chapter III, §5.

@[reducible, inline]

noncomputable abbrev TauCeti.unramifiedQuadraticPoly : Polynomial ℚ_[2]

The third cyclotomic polynomial X² + X + 1 over ℚ₂.

theorem TauCeti.unramifiedQuadraticPoly_irreducible : Irreducible unramifiedQuadraticPoly

The third cyclotomic polynomial is irreducible over ℚ₂, since its discriminant -3 is not a square modulo 8.

instance TauCeti.instFactIrreduciblePolynomialPadicOfNatNatUnramifiedQuadraticPoly : Fact (Irreducible unramifiedQuadraticPoly)

@[reducible, inline]

abbrev TauCeti.UnramifiedQuadratic : Type

The unramified quadratic extension ℚ₂(ζ₃), presented as the root field of X² + X + 1.

@[instance_reducible]

noncomputable instance TauCeti.UnramifiedQuadratic.instField : Field UnramifiedQuadratic

@[instance_reducible]

noncomputable instance TauCeti.UnramifiedQuadratic.instAlgebraPadicOfNatNat : Algebra ℚ_[2] UnramifiedQuadratic

instance TauCeti.UnramifiedQuadratic.instFiniteDimensionalPadicOfNatNat : FiniteDimensional ℚ_[2] UnramifiedQuadratic

instance TauCeti.UnramifiedQuadratic.instCharZero : CharZero UnramifiedQuadratic

@[instance_reducible]

noncomputable instance TauCeti.UnramifiedQuadratic.instValuativeRel : ValuativeRel UnramifiedQuadratic

@[instance_reducible]

noncomputable instance TauCeti.UnramifiedQuadratic.instTopologicalSpace : TopologicalSpace UnramifiedQuadratic

instance TauCeti.UnramifiedQuadratic.instValuativeExtensionPadicOfNatNat : ValuativeExtension ℚ_[2] UnramifiedQuadratic

instance TauCeti.UnramifiedQuadratic.instIsNonarchimedeanLocalField : IsNonarchimedeanLocalField UnramifiedQuadratic

noncomputable def TauCeti.UnramifiedQuadratic.zetaThree : UnramifiedQuadratic

The distinguished primitive cube root in ℚ₂(ζ₃).

theorem TauCeti.UnramifiedQuadratic.zetaThree_sq_add_zetaThree_add_one : zetaThree ^ 2 + zetaThree + 1 = 0

The defining equation ζ₃² + ζ₃ + 1 = 0.

theorem TauCeti.UnramifiedQuadratic.isPrimitiveRoot_zetaThree : IsPrimitiveRoot zetaThree 3

The distinguished root ζ₃ is a primitive cube root of unity.

theorem TauCeti.UnramifiedQuadratic.adjoin_zetaThree_eq_top : ℚ_[2]⟮zetaThree⟯ = ⊤

The distinguished root generates ℚ₂(ζ₃) over ℚ₂.

theorem TauCeti.UnramifiedQuadratic.finrank_eq_two : Module.finrank ℚ_[2] UnramifiedQuadratic = 2

The extension ℚ₂(ζ₃)/ℚ₂ has degree two.

instance TauCeti.UnramifiedQuadratic.instIsQuadraticExtensionPadicOfNatNat : Algebra.IsQuadraticExtension ℚ_[2] UnramifiedQuadratic

instance TauCeti.UnramifiedQuadratic.instIsUnramifiedPadicOfNatNat : IsUnramified ℚ_[2] UnramifiedQuadratic

The extension ℚ₂(ζ₃)/ℚ₂ is unramified. The integral generator ζ₃ is a simple root of X² + X + 1, since the square of the derivative 2ζ₃ + 1 is the unit -3.

theorem TauCeti.localRootOfUnityOrder_two_unramifiedQuadratic : localRootOfUnityOrder 2 UnramifiedQuadratic ⋯ = 2

The 2-power roots of unity in ℚ₂(ζ₃) have order two.

theorem TauCeti.nontrivial_algEquiv_unramifiedQuadratic : Nontrivial Gal(UnramifiedQuadratic/ℚ_[2])

The automorphism group of the unramified quadratic extension ℚ₂(ζ₃)/ℚ₂ is nontrivial.