Necessary and sufficient conditions for a locally compact valued 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.exists_norm_coe_lt_one (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] : ∃ (x : ↥(integer K)), 0 < ‖↑x‖ ∧ ‖↑x‖ < 1

theorem Valued.integer.exists_norm_lt_one (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] : ∃ (x : ↥(integer K)), 0 < ‖x‖ ∧ ‖x‖ < 1

theorem Valued.integer.exists_nnnorm_lt_one (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] : ∃ (x : ↥(integer K)), 0 < ‖x‖₊ ∧ ‖x‖₊ < 1

@[deprecated IsLocalRing.instFiniteQuotientIdealHPowNatMaximalIdealOfIsNoetherianRingOfResidueField (since := "2026-08-26")]

theorem Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Finite (IsLocalRing.ResidueField R)] (n : ℕ) : Finite (R ⧸ IsLocalRing.maximalIdeal R ^ n)

Alias of IsLocalRing.instFiniteQuotientIdealHPowNatMaximalIdealOfIsNoetherianRingOfResidueField.

theorem Valued.integer.totallyBounded_iff_finite_residueField {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] [v.RankOne] [IsDiscreteValuationRing ↥(integer K)] : TotallyBounded Set.univ ↔ Finite (ResidueField K)

theorem Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] (hc : IsCompact ↑(integer K)) : Nonempty (LocallyFiniteOrder (↥(MonoidHom.mrange v))ˣ)

theorem Valued.integer.mulArchimedean_mrange_of_isCompact_integer {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] (hc : IsCompact ↑(integer K)) : MulArchimedean ↥(MonoidHom.mrange v)

theorem Valued.integer.isPrincipalIdealRing_of_compactSpace {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] [hc : CompactSpace ↥(integer K)] : IsPrincipalIdealRing ↥(integer K)

theorem Valuation.isNontrivial_iff_not_a_field {K : Type u_3} {Γ : Type u_4} [Field K] [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) : v.IsNontrivial ↔ IsLocalRing.maximalIdeal ↥v.integer ≠ ⊥

theorem Valued.integer.isDiscreteValuationRing_of_compactSpace {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] [hn : v.IsNontrivial] [CompactSpace ↥(integer K)] : IsDiscreteValuationRing ↥(integer K)

theorem Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] [v.RankOne] : CompactSpace ↥(integer K) ↔ CompleteSpace ↥(integer K) ∧ IsDiscreteValuationRing ↥(integer K) ∧ Finite (ResidueField K)

theorem Valued.integer.properSpace_iff_compactSpace_integer {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] [v.RankOne] : ProperSpace K ↔ CompactSpace ↥(integer K)

theorem Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] [v.RankOne] : ProperSpace K ↔ CompleteSpace K ∧ IsDiscreteValuationRing ↥(integer K) ∧ Finite (ResidueField K)