LeanPool.BruhatTits.Utils.ValuationRings

theorem maximalIdeal_smul_eq_uniformizer_smul {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] {ι : Type u_2} (M : Submodule (↥R) (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) : IsLocalRing.maximalIdeal ↥R • M = ϖ • M

@[simp]

theorem Subring.coe_zpow {K : Type u_1} [Field K] (R : Subring K) (a : (↥R)ˣ) (n : ℤ) : ↑↑(a ^ n) = ↑↑a ^ n

theorem mem_subring_iff_integer {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (x : K) : x ∈ R ↔ (ValuationRing.valuation (↥R) K) x ≤ 1

theorem coe_inv_eq_inv_coe {K : Type u_1} [Field K] {R : Subring K} (u : (↥R)ˣ) : (↑↑u)⁻¹ = ↑↑u⁻¹

theorem mem_or_inv_mem {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (x : K) : x ∈ R ∨ x⁻¹ ∈ R

theorem eq_unit_mul_pow_irreducible {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (x : K) (hx : x ≠ 0) : ∃ (n : ℤ) (u : (↥R)ˣ), x = ↑↑u * ↑ϖ ^ n

theorem eq_unit_mul_pow_irreducible' {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (x : Kˣ) : ∃ (n : ℤ) (u : (↥R)ˣ), x = (Units.map ↑R.subtype) u * Units.mk0 ↑ϖ ⋯ ^ n

theorem valuation_eq_iff {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (x y : K) : (ValuationRing.valuation (↥R) K) x = (ValuationRing.valuation (↥R) K) y ↔ ∃ (a : (↥R)ˣ), ↑↑a * y = x

theorem valuation_unit {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (a : (↥R)ˣ) : (ValuationRing.valuation (↥R) K) ↑↑a = 1

theorem valuation_isUnit {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (a : ↥R) (ha : IsUnit a) : (ValuationRing.valuation (↥R) K) ↑a = 1

theorem valuation_eq_one_iff {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (a : ↥R) : IsUnit a ↔ (ValuationRing.valuation (↥R) K) ↑a = 1

theorem valuation_unit_eq_one {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (x : (↥R)ˣ) : (ValuationRing.valuation (↥R) K) ↑↑x = 1

theorem valuation_lt_one_of_irreducible {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) : (ValuationRing.valuation (↥R) K) ↑ϖ < 1

noncomputable def zaddVal' {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (x : Kˣ) : ℤ

The exponent of a unit relative to a chosen irreducible element.

Equations

• zaddVal' ϖ hϖ x = ⋯.choose

noncomputable def zaddVal {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] [IsDiscreteValuationRing ↥R] (x : Kˣ) : ℤ

The exponent of a unit relative to an arbitrary chosen irreducible element of the DVR.

Equations

• zaddVal x = zaddVal' ⋯.choose ⋯ x

theorem zaddVal'_spec {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (x : Kˣ) : ∃ (u : (↥R)ˣ), x = (Units.map ↑R.subtype) u * Units.mk0 ↑ϖ ⋯ ^ zaddVal' ϖ hϖ x

theorem zaddVal_spec' {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] [IsDiscreteValuationRing ↥R] (x : Kˣ) : ∃ (ϖ : ↥R) (hϖ : Irreducible ϖ), zaddVal x = zaddVal' ϖ hϖ x

theorem zaddVal_spec {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] [IsDiscreteValuationRing ↥R] (x : Kˣ) : ∃ (ϖ : ↥R) (hϖ : Irreducible ϖ) (u : (↥R)ˣ), x = (Units.map ↑R.subtype) u * Units.mk0 ↑ϖ ⋯ ^ zaddVal x

theorem unit_mul_zpow_congr_zpow' {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (a b : (↥R)ˣ) (m n : ℤ) (h : ↑↑a * ↑ϖ ^ m = ↑↑b * ↑ϖ ^ n) : m = n

theorem unit_mul_zpow_congr_zpow {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] [IsDiscreteValuationRing ↥R] {p q : ↥R} (hp : Irreducible p) (hq : Irreducible q) (a b : (↥R)ˣ) (m n : ℤ) (h : ↑↑a * ↑p ^ m = ↑↑b * ↑q ^ n) : m = n

theorem valuation_irreducible_zpow_eq_one_iff {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) (n : ℤ) : (ValuationRing.valuation (↥R) K) (↑ϖ ^ n) = 1 ↔ n = 0

theorem inv_irreducible_not_mem_subring {K : Type u_1} [Field K] {R : Subring K} (ϖ : ↥R) (hϖ : Irreducible ϖ) : (↑ϖ)⁻¹ ∉ R

theorem neg_pow_not_mem_subring {K : Type u_1} [Field K] {R : Subring K} (ϖ : ↥R) (hϖ : Irreducible ϖ) (n : ℕ) (hn : n > 0) : ↑ϖ ^ (-↑n) ∉ R

theorem irreducible_zpow_mem_subring_iff {K : Type u_1} [Field K] {R : Subring K} (ϖ : ↥R) (hϖ : Irreducible ϖ) (n : ℤ) : ↑ϖ ^ n ∈ R ↔ n ≥ 0

theorem zaddVal'_eq_iff {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (n : ℤ) (x : Kˣ) : zaddVal' ϖ hϖ x = n ↔ ∃ (u : (↥R)ˣ), (Units.map ↑R.subtype) u * Units.mk0 ↑ϖ ⋯ ^ n = x

theorem zaddVal_eq_iff {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (n : ℤ) (x : Kˣ) : zaddVal x = n ↔ ∃ (u : (↥R)ˣ), (Units.map ↑R.subtype) u * Units.mk0 ↑ϖ ⋯ ^ n = x

theorem zaddVal_eq_iff' {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (n : ℤ) (x : Kˣ) : zaddVal x = n ↔ ∃ (u : (↥R)ˣ), ↑↑u * ↑ϖ ^ n = ↑x

theorem eq_unit_mul_zpow_zaddVal {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (x : Kˣ) : ∃ (u : (↥R)ˣ), ↑↑u * ↑ϖ ^ zaddVal x = ↑x

@[simp]

theorem zaddVal_mul {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] [IsDiscreteValuationRing ↥R] (x y : Kˣ) : zaddVal (x * y) = zaddVal x + zaddVal y

@[simp]

theorem zaddVal_units_map {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] [IsDiscreteValuationRing ↥R] (x : (↥R)ˣ) : zaddVal ((Units.map ↑R.subtype) x) = 0