The unramified quadratic extension ℚ_2(√5)

Since 5 is not a square in ℚ_2, adjoining a root of X² − 5 gives a quadratic extension ℚ_2(√5) of ℚ_2. This file equips it with the structure of a nonarchimedean local field extending ℚ_2, through the spectral norm of TauCeti.algebraicExtensionValuativeRel, and computes its Frobenius.

The extension is unramified: the golden ratio φ = (1 + √5) / 2 is a root of X² − X − 1, whose derivative at φ is 2φ − 1 = √5, a unit because its square 5 is a unit of ℤ_2. So the residue field is 𝔽_4, and the Galois group is generated by the arithmetic Frobenius, which lifts x ↦ x² on 𝔽_4. Being nontrivial, Frobenius is the conjugation √5 ↦ −√5.

Since a local field has, up to isomorphism, a unique unramified extension of each degree, ℚ_2(√5) is an explicit model of the unramified quadratic extension of ℚ_2. It makes the residue correspondence Gal(ℚ_2(√5)/ℚ_2) ≃ Gal(𝔽_4/𝔽_2) concrete, with the Frobenius of 𝔽_4 lifting to an explicit automorphism of ℚ_2(√5).

It also makes the norm-equation criterion for unramified extensions concrete. Since the residue degree is 2, an element of ℚ_2ˣ is a norm from ℚ_2(√5) exactly when its 2-adic valuation is even. So a² − 5b² = 3 is solvable in ℚ_2, while a² − 5b² = 2 is not. The first equation has no solution in ℚ, since 3 is not a square modulo 5, so its solvability in ℚ_2 is a genuinely local fact.

Main definitions

• TauCeti.DyadicSqrtFive: the field ℚ_2(√5), as a nonarchimedean local field over ℚ_2.
• TauCeti.DyadicSqrtFive.sqrtFive: the square root of 5 generating it.

Main results

• TauCeti.DyadicSqrtFive.finrank_eq_two: [ℚ_2(√5) : ℚ_2] = 2.
• The instance IsUnramified ℚ_[2] DyadicSqrtFive: ℚ_2(√5)/ℚ_2 is unramified.
• TauCeti.DyadicSqrtFive.inertiaDegree_eq_two and TauCeti.DyadicSqrtFive.natCard_residueField: the residue field has 2 ^ 2 = 4 elements.
• TauCeti.DyadicSqrtFive.frobeniusAlgEquiv_sqrtFive: arithmetic Frobenius sends √5 to −√5.
• TauCeti.DyadicSqrtFive.norm_add_mul_sqrtFive: the norm of a + b√5 is a² − 5b².
• TauCeti.DyadicSqrtFive.mem_normGroup_iff_even_valuation: x ∈ ℚ_2ˣ is a norm from ℚ_2(√5) exactly when its 2-adic valuation is even.
• TauCeti.DyadicSqrtFive.exists_sq_sub_five_mul_sq_eq_three and TauCeti.DyadicSqrtFive.not_exists_sq_sub_five_mul_sq_eq_two: the norm equation a² − 5b² = 3 is solvable in ℚ_2, and a² − 5b² = 2 is not.

References

• J.-P. Serre, Local Fields, Chapter III, §5 and Chapter V, §2.
• J. Neukirch, Algebraic Number Theory, Chapter II, §7.

def TauCeti.DyadicSqrtFive : Type

The field ℚ_2(√5), obtained from ℚ_2 by adjoining a root of X² − 5. It carries the nonarchimedean local field structure of TauCeti.algebraicExtensionValuativeRel, which is the unique one extending that of ℚ_2.

theorem TauCeti.DyadicSqrtFive.instFactIrreduciblePolynomialPadicOfNatNatHSubHPowXCoeRingHomC : Fact (Irreducible (Polynomial.X ^ 2 - Polynomial.C 5))

X² − 5 is irreducible over ℚ_2, because 5 is not a square in ℚ_2.

@[instance_reducible]

noncomputable instance TauCeti.DyadicSqrtFive.instField : Field DyadicSqrtFive

@[instance_reducible]

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

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

instance TauCeti.DyadicSqrtFive.instCharZero : CharZero DyadicSqrtFive

@[instance_reducible]

noncomputable instance TauCeti.DyadicSqrtFive.instValuativeRel : ValuativeRel DyadicSqrtFive

@[instance_reducible]

noncomputable instance TauCeti.DyadicSqrtFive.instTopologicalSpace : TopologicalSpace DyadicSqrtFive

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

instance TauCeti.DyadicSqrtFive.instIsNonarchimedeanLocalField : IsNonarchimedeanLocalField DyadicSqrtFive

noncomputable def TauCeti.DyadicSqrtFive.sqrtFive : DyadicSqrtFive

The square root √5 of 5 in ℚ_2(√5), the class of X.

@[simp]

theorem TauCeti.DyadicSqrtFive.sqrtFive_sq : sqrtFive ^ 2 = 5

The square of √5 is 5.

theorem TauCeti.DyadicSqrtFive.sqrtFive_not_mem : sqrtFive ∉ Set.range ⇑(algebraMap ℚ_[2] DyadicSqrtFive)

√5 does not belong to the embedded base field ℚ_2.

theorem TauCeti.DyadicSqrtFive.adjoin_sqrtFive_eq_top : ℚ_[2]⟮sqrtFive⟯ = ⊤

√5 generates ℚ_2(√5) over ℚ_2.

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

ℚ_2(√5) is a quadratic extension of ℚ_2.

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

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

ℚ_2(√5)/ℚ_2 is unramified: it is generated by the golden ratio φ, a root of the integral polynomial X² − X − 1 at which the derivative 2φ − 1 = √5 is a unit.

theorem TauCeti.DyadicSqrtFive.inertiaDegree_eq_two : inertiaDegree ℚ_[2] DyadicSqrtFive = 2

The residue degree of ℚ_2(√5)/ℚ_2 is 2.

@[simp]

theorem TauCeti.DyadicSqrtFive.natCard_residueField : Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation DyadicSqrtFive).integer) = 4

The residue field of ℚ_2(√5) has 4 elements.

@[simp]

theorem TauCeti.DyadicSqrtFive.frobeniusAlgEquiv_sqrtFive : frobeniusAlgEquiv sqrtFive = -sqrtFive

The arithmetic Frobenius of ℚ_2(√5)/ℚ_2 is the conjugation √5 ↦ −√5.

theorem TauCeti.DyadicSqrtFive.exists_eq_add_mul_sqrtFive (y : DyadicSqrtFive) : ∃ (a : ℚ_[2]) (b : ℚ_[2]), y = (algebraMap ℚ_[2] DyadicSqrtFive) a + (algebraMap ℚ_[2] DyadicSqrtFive) b * sqrtFive

Every element of ℚ_2(√5) is a + b√5 for some a b : ℚ_2.

theorem TauCeti.DyadicSqrtFive.norm_add_mul_sqrtFive (a b : ℚ_[2]) : (Algebra.norm ℚ_[2]) ((algebraMap ℚ_[2] DyadicSqrtFive) a + (algebraMap ℚ_[2] DyadicSqrtFive) b * sqrtFive) = a ^ 2 - 5 * b ^ 2

The norm form of ℚ_2(√5)/ℚ_2. The norm of a + b√5 is a² − 5b².

theorem TauCeti.DyadicSqrtFive.mem_normGroup_iff_even_valuation {x : ℚ_[2]ˣ} : x ∈ normGroup ℚ_[2] DyadicSqrtFive ↔ Even (↑x).valuation

The norm group of ℚ_2(√5)/ℚ_2. An element of ℚ_2ˣ is a norm from ℚ_2(√5) exactly when its 2-adic valuation is even.

theorem TauCeti.DyadicSqrtFive.exists_sq_sub_five_mul_sq_eq_iff {x : ℚ_[2]} : (∃ (a : ℚ_[2]) (b : ℚ_[2]), a ^ 2 - 5 * b ^ 2 = x) ↔ Even x.valuation

The norm equation of ℚ_2(√5)/ℚ_2. For x : ℚ_2, the equation a² − 5b² = x has a solution in ℚ_2 exactly when the 2-adic valuation of x is even. For x = 0 both sides hold trivially, the valuation of 0 being 0.

theorem TauCeti.DyadicSqrtFive.exists_sq_sub_five_mul_sq_eq_three : ∃ (a : ℚ_[2]) (b : ℚ_[2]), a ^ 2 - 5 * b ^ 2 = 3

A solvable norm equation. 3 is a norm from ℚ_2(√5): the equation a² − 5b² = 3 has a solution in ℚ_2, because 3 has even valuation 0.

theorem TauCeti.DyadicSqrtFive.not_exists_sq_sub_five_mul_sq_eq_two : ¬∃ (a : ℚ_[2]) (b : ℚ_[2]), a ^ 2 - 5 * b ^ 2 = 2

An unsolvable norm equation. 2 is not a norm from ℚ_2(√5): the equation a² − 5b² = 2 has no solution in ℚ_2, because 2 has odd valuation.