Documentation

TauCeti.NumberTheory.LocalField.Padic

Normalization of the p-adic absolute value #

These comparison lemmas let the generic normalized-valuation API interoperate with Mathlib's concrete p-adic norm and valuation APIs.

Main results #

The Padic and residue-field constructions used here are part of Mathlib's upstream NumberTheory/Padics development.

source
@[simp]
theorem Padic.normalizedValuationWithZero_eq_inv_mulValuation (p : ℕ) [Fact (Nat.Prime p)] (x : ℚ_[p]) :
(TauCeti.normalizedValuationWithZero ℚ_[p]) x = (mulValuation x)⁻¹

The zero-preserving normalized valuation on ℚ_[p] is the inverse of Mathlib's p-adic valuation.

source
@[simp]
theorem Padic.toAdd_normalizedValuation_eq_valuation (p : ℕ) [Fact (Nat.Prime p)] (x : ℚ_[p]ˣ) :
Multiplicative.toAdd ((TauCeti.normalizedValuation ℚ_[p]) x) = (↑x).valuation

The additive normalized valuation on ℚ_[p] is Mathlib's p-adic valuation.

source
theorem Padic.integerRing_eq_subring (p : ℕ) [Fact (Nat.Prime p)] :
(ValuativeRel.valuation ℚ_[p]).integer = PadicInt.subring p

The ring of integers of ℚ_[p] for its valuative relation is Mathlib's subring of elements of norm at most 1.

source
noncomputable def Padic.integerRingEquiv (p : ℕ) [Fact (Nat.Prime p)] :
↥(ValuativeRel.valuation ℚ_[p]).integer ≃+* ℤ_[p]

The ring of integers of ℚ_[p] for its valuative relation is ℤ_[p].

Equations
Instances For
    source
    @[simp]
    theorem Padic.coe_integerRingEquiv_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ↥(ValuativeRel.valuation ℚ_[p]).integer) :
    ↑((integerRingEquiv p) x) = ↑x

    The identification of the ring of integers of ℚ_[p] with ℤ_[p] is the identity on the underlying p-adic numbers.

    source
    @[simp]
    theorem Padic.coe_integerRingEquiv_symm_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) :
    ↑((integerRingEquiv p).symm x) = ↑x

    The inverse identification of ℤ_[p] with the ring of integers of ℚ_[p] is the identity on the underlying p-adic numbers.

    source
    @[simp]
    theorem Padic.natCard_residueField (p : ℕ) [Fact (Nat.Prime p)] :
    Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation ℚ_[p]).integer) = p

    The residue field of ℚ_[p] has cardinality p.

    source
    @[simp]
    theorem Padic.normalizedAbsoluteValue_eq_nnnorm (p : ℕ) [Fact (Nat.Prime p)] (x : ℚ_[p]) :
    ↑((TauCeti.normalizedAbsoluteValue ℚ_[p]) x) = ‖x‖₊

    The normalized absolute value on ℚ_[p] agrees with Mathlib's norm.

    source
    @[simp]
    theorem Padic.natCastValuation_eq_padicValNat (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : ↑n ≠ 0) :
    TauCeti.natCastValuation ℚ_[p] n hn = padicValNat p n

    The normalized valuation of a natural number in ℚ_[p] is its p-adic valuation.

    source
    theorem Padic.natCastValuation_self (p : ℕ) [Fact (Nat.Prime p)] :
    TauCeti.natCastValuation ℚ_[p] p ⋯ = 1

    The normalized valuation of the residue prime p in ℚ_[p] is 1; equivalently, ℚ_[p] is absolutely unramified.

    source
    theorem Padic.natCastValuation_two (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) :
    TauCeti.natCastValuation ℚ_[p] 2 ⋯ = 0

    The normalized valuation of 2 in ℚ_[p] vanishes for every odd p.

    source
    theorem Padic.not_isSquare_neg_one_of_mod_four_eq_three (p : ℕ) [Fact (Nat.Prime p)] (hp : p % 4 = 3) :
    ¬IsSquare (-1)

    If p ≡ 3 (mod 4), then -1 is not a square in ℚ_[p]. Combined with TauCeti.anisotropic_binary_one_one_iff, this shows that the binary form ⟨1, 1⟩ is anisotropic over ℚ_[p] for such primes.

    source
    theorem Padic.not_isSquare_intCast_of_not_isSquare_zmod {p : ℕ} [Fact (Nat.Prime p)] {a : ℤ} {k : ℕ} (h : ¬IsSquare ↑a) :
    ¬IsSquare ↑a

    A square root in ℚ_[p] of an integer is a p-adic integer, so an integer that is not a square modulo some power of p is not a square in ℚ_[p].

    source
    theorem Padic.not_isSquare_five :
    ¬IsSquare 5

    5 is not a square in ℚ_[2], since no square is 5 modulo 8.

    source
    theorem Padic.factPrimeFive :
    Fact (Nat.Prime 5)

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

    source
    theorem Padic.not_isSquare_neg_three :
    ¬IsSquare (-3)

    -3 is not a square in ℚ_[5], since its residue 2 is not a square modulo 5.

    source
    theorem Padic.irreducible_X_sq_add_X_add_one :
    Irreducible (Polynomial.X ^ 2 + Polynomial.X + 1)

    X² + X + 1 is irreducible over ℚ_[5]: a root r would make (2r + 1)² = −3 a square.

    source
    theorem TauCeti.Padic.irreducible_natCast_self (p : ℕ) [Fact (Nat.Prime p)] :
    Irreducible ↑p

    The residue prime p is a uniformizer of the integer ring of ℚ_[p].