Documentation

Iwasawalib.NumberTheory.AbsoluteValue.Normalization

Normalization of an `ℝ`-valued `AbsoluteValue` over a characteristic zero field #

Typeclass asserting that an absolute value is normalized #

class inductive AbsoluteValue.IsNormalized {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) :

If v is an ℝ-valued AbsoluteValue over a characteristic zero field, then AbsoluteValue.IsNormalized v is a typeclass asserting that v is normalized, in the sense that the restriction of v to ℚ is equal to the usual ∞-adic valuation or p-adic valuation on ℚ. In particular such v is non-trivial.

of_archimedean {K : Type u_1} [Field K] [CharZero K] {v : AbsoluteValue K ℝ} (h : v.comp ⋯ = Rat.AbsoluteValue.real) : v.IsNormalized
of_nonarchimedean {K : Type u_1} [Field K] [CharZero K] {v : AbsoluteValue K ℝ} (p : ℕ) [Fact (Nat.Prime p)] (h : v.comp ⋯ = Rat.AbsoluteValue.padic p) : v.IsNormalized

Instances

theorem AbsoluteValue.isNormalized_iff {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) :

v.IsNormalized ↔ v.comp ⋯ = Rat.AbsoluteValue.real ∨ ∃ (p : ℕ) (inst : Fact (Nat.Prime p)), v.comp ⋯ = Rat.AbsoluteValue.padic p

theorem AbsoluteValue.isNontrivial_of_isNormalized' {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) [v.IsNormalized] :

(v.comp ⋯).IsNontrivial

theorem AbsoluteValue.isNontrivial_of_isNormalized {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) [v.IsNormalized] :

theorem AbsoluteValue.isNormalized_iff_forall_apply_natCast_eq {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) :

v.IsNormalized ↔ (∀ (n : ℕ), v ↑n = ↑n) ∨ ∃ (p : ℕ) (_ : Fact (Nat.Prime p)), ∀ (n : ℕ), v ↑n = ↑(padicNorm p ↑n)

To check if an absolute value is normalized, one only needs to check it on natural numbers.

theorem AbsoluteValue.isNormalized_iff_of_liesOver {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [CharZero K] [CharZero L] (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ) [w.LiesOver v] :

v.IsNormalized ↔ w.IsNormalized

theorem AbsoluteValue.IsEquiv.eq_of_isNormalized {K : Type u_1} [Field K] [CharZero K] {v w : AbsoluteValue K ℝ} (h : v.IsEquiv w) [v.IsNormalized] [w.IsNormalized] :

v = w

theorem AbsoluteValue.isEquiv_iff_eq_of_isNormalized {K : Type u_1} [Field K] [CharZero K] {v w : AbsoluteValue K ℝ} [v.IsNormalized] [w.IsNormalized] :

v.IsEquiv w ↔ v = w

instance Rat.AbsoluteValue.isNormalized_real :

real.IsNormalized

instance Rat.AbsoluteValue.isNormalized_padic (p : ℕ) [Fact (Nat.Prime p)] :

(padic p).IsNormalized

theorem Rat.AbsoluteValue.eq_real_or_padic_of_isNormalized (v : AbsoluteValue ℚ ℝ) [v.IsNormalized] :

v = real ∨ ∃! p : ℕ , ∃ (x : Fact (Nat.Prime p)), v = padic p

theorem Rat.AbsoluteValue.eq_real_of_not_isNonarchimedean_of_isNormalized (v : AbsoluteValue ℚ ℝ) (h : ¬IsNonarchimedean ⇑v) [v.IsNormalized] :

theorem Rat.AbsoluteValue.eq_padic_of_isNonarchimedean_of_isNormalized (v : AbsoluteValue ℚ ℝ) (h : IsNonarchimedean ⇑v) [v.IsNormalized] :

∃! p : ℕ , ∃ (x : Fact (Nat.Prime p)), v = padic p

theorem AbsoluteValue.apply_adic_eq_inv_of_isNormalized {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) [v.IsNormalized] :

v ↑v.adic = (↑v.adic)⁻¹

Normalization of an absolute value #

noncomputable def AbsoluteValue.normalizationExponent {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) :

The exponent c which makes v ^ c normalized.

Equations

v.normalizationExponent = if nontriv : (v.comp ⋯).IsNontrivial then if h : v.comp ⋯ ≈ Rat.AbsoluteValue.real then 1 / ⋯.choose else 1 / ⋯.choose else 1

Instances For

theorem AbsoluteValue.normalizationExponent_pos {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) :

0 < v.normalizationExponent

noncomputable def AbsoluteValue.normalization {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) :

AbsoluteValue K ℝ

The normalization of an absolute value.

Equations

v.normalization = { toFun := fun (x : K) => v x ^ v.normalizationExponent, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }

Instances For

@[simp]

theorem AbsoluteValue.normalization_apply {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) (x : K) :

v.normalization x = v x ^ v.normalizationExponent

theorem AbsoluteValue.isEquiv_normalization {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) :

v.IsEquiv v.normalization

theorem AbsoluteValue.isNormalized_normalization_of_isNontrivial {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) (hv : (v.comp ⋯).IsNontrivial) :

v.normalization.IsNormalized

theorem AbsoluteValue.isNormalized_normalization_of_isNontrivial_of_isAlgebraic {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) (hv : v.IsNontrivial) [Algebra.IsAlgebraic ℚ K] :

v.normalization.IsNormalized