English
For a rank-one valuation and a discrete valuation ring, the valuation ring is totally bounded if and only if the residue field is finite.
Русский
Для ранга единицы оценки и дискретного оценочного кольца кольцо оценки полностью ограничено тогда и только тогда, когда остаточное поле конечно.
LaTeX
$$$$\mathrm{TotallyBounded}(\mathcal{O}_K) \;\iff\; \mathrm{Finite}(\kappa(K)).$$$$
Lean4
theorem totallyBounded_iff_finite_residueField [(Valued.v : Valuation K Γ₀).RankOne] [IsDiscreteValuationRing 𝒪[K]] :
TotallyBounded (Set.univ (α := 𝒪[K])) ↔ Finite 𝓀[K] :=
by
constructor
· intro H
obtain ⟨p, hp⟩ := IsDiscreteValuationRing.exists_irreducible 𝒪[K]
have := Metric.finite_approx_of_totallyBounded H ‖p‖ (norm_pos_iff.mpr hp.ne_zero)
simp only [Set.subset_univ, Set.univ_subset_iff, true_and] at this
obtain ⟨t, ht, ht'⟩ := this
rw [← Set.finite_univ_iff]
refine (ht.image (IsLocalRing.residue _)).subset ?_
rintro ⟨x⟩
replace ht' := ht'.ge (Set.mem_univ x)
simp only [Set.mem_iUnion, Metric.mem_ball, exists_prop] at ht'
obtain ⟨y, hy, hy'⟩ := ht'
simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, Set.mem_univ, IsLocalRing.residue,
Set.mem_image, true_implies]
refine ⟨y, hy, ?_⟩
convert
(Ideal.Quotient.mk_eq_mk_iff_sub_mem (I := 𝓂[K]) y x).mpr
_
-- TODO: make Valued.maximalIdeal abbreviations instead of def
rw [Valued.maximalIdeal, hp.maximalIdeal_eq, ← SetLike.mem_coe,
(Valuation.integer.integers _).coe_span_singleton_eq_setOf_le_v_algebraMap]
rw [dist_comm] at hy'
simpa [dist_eq_norm] using hy'.le
· intro H
rw [Metric.totallyBounded_iff]
intro ε εpos
obtain ⟨p, hp⟩ := IsDiscreteValuationRing.exists_irreducible 𝒪[K]
have hp' := Valuation.integer.v_irreducible_lt_one hp
obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖(p : K)‖ ^ n < ε := exists_pow_lt_of_lt_one εpos (toNormedField.norm_lt_one_iff.mpr hp')
have hF := finite_quotient_maximalIdeal_pow_of_finite_residueField H n
refine ⟨Quotient.out '' (Set.univ (α := 𝒪[K] ⧸ (𝓂[K] ^ n))), Set.toFinite _, ?_⟩
have : {y : 𝒪[K] | v (y : K) ≤ v (p : K) ^ n} = Metric.closedBall 0 (‖p‖ ^ n) :=
by
ext
simp [← norm_pow]
simp only [Ideal.univ_eq_iUnion_image_add (𝓂[K] ^ n), hp.maximalIdeal_pow_eq_setOf_le_v_coe_pow, this,
AddSubgroupClass.coe_norm, Set.image_univ, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq',
Set.iUnion_subset_iff, Metric.vadd_closedBall, vadd_eq_add, add_zero]
intro
exact (Metric.closedBall_subset_ball hn).trans (Set.subset_iUnion_of_subset _ le_rfl)
