Necessary and sufficient conditions for a locally compact nonarchimedean normed field

Main Definitions

• totallyBounded_iff_finite_residueField: when the valuation ring is a DVR, it is totally bounded iff the residue field is finite.

Tags

norm, nonarchimedean, rank one, compact, locally compact

@[simp]

theorem NormedField.v_eq_valuation {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] (x : K) : Valued.v x = valuation x

theorem Valued.integer.mem_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {x : K} : x ∈ integer K ↔ ‖x‖ ≤ 1

An element is in the valuation ring if the norm is bounded by 1. This is a variant of Valuation.mem_integer_iff, phrased using norms instead of the valuation.

theorem Valued.integer.norm_le_one {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] (x : ↥(integer K)) : ‖x‖ ≤ 1

@[simp]

theorem Valued.integer.norm_coe_unit {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] (u : (↥(integer K))ˣ) : ‖↑↑u‖ = 1

theorem Valued.integer.norm_unit {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] (u : (↥(integer K))ˣ) : ‖↑u‖ = 1

theorem Valued.integer.isUnit_iff_norm_eq_one {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {u : ↥(integer K)} : IsUnit u ↔ ‖u‖ = 1

theorem Valued.integer.norm_irreducible_lt_one {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {ϖ : ↥(integer K)} (h : Irreducible ϖ) : ‖ϖ‖ < 1

theorem Valued.integer.norm_irreducible_pos {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {ϖ : ↥(integer K)} (h : Irreducible ϖ) : 0 < ‖ϖ‖

theorem Valued.integer.coe_span_singleton_eq_closedBall {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] (x : ↥(integer K)) : ↑(Ideal.span {x}) = Metric.closedBall 0 ‖x‖

theorem Irreducible.maximalIdeal_eq_closedBall {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [IsDiscreteValuationRing ↥(Valued.integer K)] {ϖ : ↥(Valued.integer K)} (h : Irreducible ϖ) : ↑(Valued.maximalIdeal K) = Metric.closedBall 0 ‖ϖ‖

theorem Irreducible.maximalIdeal_pow_eq_closedBall_pow {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [IsDiscreteValuationRing ↥(Valued.integer K)] {ϖ : ↥(Valued.integer K)} (h : Irreducible ϖ) (n : ℕ) : ↑(Valued.maximalIdeal K ^ n) = Metric.closedBall 0 (‖ϖ‖ ^ n)

theorem Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField {K : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [IsDiscreteValuationRing ↥(integer K)] (h : Finite (ResidueField K)) (n : ℕ) : Finite (↥(integer K) ⧸ maximalIdeal K ^ n)

theorem Valued.integer.totallyBounded_iff_finite_residueField {K : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [IsDiscreteValuationRing ↥(integer K)] : TotallyBounded Set.univ ↔ Finite (ResidueField K)