Integer rings of valued rings and nonarchimedean normed fields

Let K be a nontrivially normed field with an ultrametric norm, with valuation ring 𝒪[K] (the closed unit ball) and maximal ideal 𝓂[K] (the open unit ball).

For an arbitrary valued ring, its integer ring has a linear topology, and it is complete when the ring is complete. These instances support topological evaluation of power series with integral coefficients.

Every 𝒪[K]-linear map between finite products of copies of K is K-linear, since K is the fraction field of 𝒪[K]; hence it is continuous and carries bounded sets to bounded sets. If the norm of K is dense, for instance if its value group is all of ℝ_{>0}, the maximal ideal 𝓂[K] is not finitely generated.

A ring homomorphism φ : K → L of nonarchimedean fields with ‖φ x‖ ≤ ‖x‖ maps 𝒪[K] into 𝒪[L], and the restriction is local, so it induces a homomorphism of residue fields. Such maps are the coefficient maps along which reductions modulo the maximal ideal are functorial.

Main results

• Valued.instIsLinearTopologyInteger: the integer ring of a valued ring has a linear topology.
• Valued.instCompleteSpaceInteger: the integer ring of a complete valued ring is complete.
• Valued.integer.mem_maximalIdeal_iff: the maximal ideal of 𝒪[K] is the open unit ball.
• Valued.integer.residue_eq_residue_iff_norm_sub_lt_one: elements of 𝒪[K] have the same residue exactly when their difference has norm less than 1.
• Valued.integer.exists_mem_maximalIdeal_coe_ne_zero: the maximal ideal of 𝒪[K] contains a nonzero element.
• Valued.integer.smul_def: on a K-module, 𝒪[K] acts through the inclusion 𝒪[K] → K.
• Valued.integer.dvd_iff_norm_le: divisibility in 𝒪[K] is comparison of norms.
• Valued.integer.submodule_mem_of_norm_le: an 𝒪[K]-submodule of K contains every element of norm at most that of one of its elements.
• Valued.integer.exists_eq_mul_of_linearMap_maximalIdeal: every 𝒪[K]-linear map 𝓂[K] → K is multiplication by an element of K.
• RingHom.integerRestrict: a norm-nonincreasing homomorphism of nonarchimedean fields restricts to a local homomorphism 𝒪[K] →+* 𝒪[L] of valuation rings (RingHom.isLocalHom_integerRestrict), hence induces a map of residue fields.
• Valued.integer.exists_seq_mem_maximalIdeal: for a densely normed field, 𝓂[K] contains a sequence of nonzero elements of increasing norm which is cofinal for the norm.
• LinearMap.continuous_of_integer: an 𝒪[K]-linear map from ι → K, ι finite, to a normed K-space is continuous.
• LinearEquiv.isBounded_image_iff_of_integer: 𝒪[K]-linear equivalences between finite products of K preserve and reflect bounded sets.
• TauCeti.not_fg_maximalIdeal_integer: for a densely normed field the maximal ideal of 𝒪[K] is not finitely generated.

instance Valued.instIsLinearTopologyInteger {K : Type u_1} {Γ₀ : Type u_2} [Ring K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] : IsLinearTopology ↥v.integer ↥v.integer

The integer ring of a valued ring has a linear topology, with valuation balls as open ideals. This is the Valued form of Mathlib's corresponding IsValuativeTopology instance.

instance Valued.instCompleteSpaceInteger {K : Type u_1} {Γ₀ : Type u_2} [Ring K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] [CompleteSpace K] : CompleteSpace ↥v.integer

The integer ring of a complete valued ring is complete for its induced uniformity.

theorem Valued.integer.mem_maximalIdeal_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {x : ↥(integer K)} : x ∈ IsLocalRing.maximalIdeal ↥(integer K) ↔ ‖x‖ < 1

An element of the valuation ring of a nonarchimedean field lies in its maximal ideal exactly when its norm is less than 1.

theorem Valued.integer.residue_eq_zero_iff_norm_lt_one {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {x : ↥(integer K)} : (IsLocalRing.residue ↥(integer K)) x = 0 ↔ ‖↑x‖ < 1

An element of the valuation ring of a nonarchimedean field has residue zero exactly when its norm is less than 1.

theorem Valued.integer.residue_eq_residue_iff_norm_sub_lt_one {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {x y : ↥(integer K)} : (IsLocalRing.residue ↥(integer K)) x = (IsLocalRing.residue ↥(integer K)) y ↔ ‖↑x - ↑y‖ < 1

Two elements of the valuation ring of a nonarchimedean field have the same residue exactly when their difference has norm less than 1.

theorem Valued.integer.exists_mem_maximalIdeal_coe_ne_zero {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] : ∃ a ∈ IsLocalRing.maximalIdeal ↥(integer K), ↑a ≠ 0

The maximal ideal of the valuation ring of a nontrivially normed nonarchimedean field contains a nonzero element.

theorem Valued.integer.smul_def {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {E : Type u_2} [AddCommMonoid E] [Module K E] [Module (↥(integer K)) E] [IsScalarTower (↥(integer K)) K E] (c : ↥(integer K)) (v : E) : c • v = ↑c • v

On a K-module E with a compatible 𝒪[K]-module structure, 𝒪[K] acts through the inclusion 𝒪[K] → K.

theorem Valued.integer.dvd_iff_norm_le {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {a b : ↥(integer K)} : b ∣ a ↔ ‖↑a‖ ≤ ‖↑b‖

In the valuation ring of a nonarchimedean field, b divides a exactly when ‖a‖ ≤ ‖b‖.

theorem Valued.integer.submodule_mem_of_norm_le {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {M : Submodule (↥(integer K)) K} {x y : K} (hy : y ∈ M) (h : ‖x‖ ≤ ‖y‖) : x ∈ M

An 𝒪[K]-submodule of K containing y contains every x with ‖x‖ ≤ ‖y‖.

theorem Valued.integer.exists_eq_mul_of_linearMap_maximalIdeal {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] (f : ↥(IsLocalRing.maximalIdeal ↥(integer K)) →ₗ[↥(integer K)] K) : ∃ (q : K), ∀ (c : ↥(IsLocalRing.maximalIdeal ↥(integer K))), f c = ↑↑c * q

Every 𝒪[K]-linear map from the maximal ideal 𝓂[K] to K is multiplication by an element of K.

theorem LinearMap.continuous_of_integer {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {ι : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace K F] [Module (↥(Valued.integer K)) F] [IsScalarTower (↥(Valued.integer K)) K F] [Finite ι] (f : (ι → K) →ₗ[↥(Valued.integer K)] F) : Continuous ⇑f

An 𝒪[K]-linear map from a finite product of copies of K to a normed K-space is continuous: it is K-linear, since K is the fraction field of 𝒪[K].

theorem LinearMap.isBounded_image_of_integer {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {ι : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace K F] [Module (↥(Valued.integer K)) F] [IsScalarTower (↥(Valued.integer K)) K F] [Finite ι] (f : (ι → K) →ₗ[↥(Valued.integer K)] F) {s : Set (ι → K)} (hs : Bornology.IsBounded s) : Bornology.IsBounded (⇑f '' s)

An 𝒪[K]-linear map from a finite product of copies of K to a normed K-space carries bounded sets to bounded sets.

theorem LinearEquiv.isBounded_image_iff_of_integer {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {ι : Type u_2} [Finite ι] {ι' : Type u_4} [Finite ι'] (e : (ι → K) ≃ₗ[↥(Valued.integer K)] ι' → K) {s : Set (ι → K)} : Bornology.IsBounded (⇑e '' s) ↔ Bornology.IsBounded s

An 𝒪[K]-linear equivalence between finite products of copies of K preserves and reflects bounded sets. In particular a submodule M is bounded exactly when M.map e is.

noncomputable def RingHom.integerRestrict {K : Type u_1} {L : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [NontriviallyNormedField L] [IsUltrametricDist L] (φ : K →+* L) (hφ : ∀ (x : K), ‖φ x‖ ≤ ‖x‖) : ↥(Valued.integer K) →+* ↥(Valued.integer L)

A ring homomorphism of nonarchimedean fields that does not increase norms maps the valuation ring 𝒪[K] into 𝒪[L]; this is its restriction 𝒪[K] →+* 𝒪[L].

@[simp]

theorem RingHom.coe_integerRestrict_apply {K : Type u_1} {L : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [NontriviallyNormedField L] [IsUltrametricDist L] (φ : K →+* L) (hφ : ∀ (x : K), ‖φ x‖ ≤ ‖x‖) (x : ↥(Valued.integer K)) : ↑((φ.integerRestrict hφ) x) = φ ↑x

RingHom.integerRestrict acts as φ on the underlying elements.

instance RingHom.isLocalHom_integerRestrict {K : Type u_1} {L : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [NontriviallyNormedField L] [IsUltrametricDist L] (φ : K →+* L) (hφ : ∀ (x : K), ‖φ x‖ ≤ ‖x‖) : IsLocalHom (φ.integerRestrict hφ)

The restriction of a norm-nonincreasing homomorphism of nonarchimedean fields to their valuation rings is a local homomorphism: an element of 𝒪[K] whose image has norm one has norm one. It therefore induces the homomorphism of residue fields IsLocalRing.ResidueField.map (φ.integerRestrict hφ) : 𝓀[K] →+* 𝓀[L].

theorem Valued.integer.exists_seq_mem_maximalIdeal {K : Type u_1} [DenselyNormedField K] [IsUltrametricDist K] : ∃ (a : ℕ → ↥(integer K)), (∀ (n : ℕ), ↑(a n) ≠ 0) ∧ (∀ (n : ℕ), a n ∈ IsLocalRing.maximalIdeal ↥(integer K)) ∧ (Monotone fun (n : ℕ) => ‖↑(a n)‖) ∧ ∀ b ∈ IsLocalRing.maximalIdeal ↥(integer K), ∃ (n : ℕ), ‖↑b‖ ≤ ‖↑(a n)‖

Over a densely normed field, the maximal ideal of 𝒪[K] contains a sequence of nonzero elements of increasing norm which is cofinal for the norm.

theorem TauCeti.not_fg_maximalIdeal_integer {K : Type u_1} [DenselyNormedField K] [IsUltrametricDist K] : ¬(IsLocalRing.maximalIdeal ↥(Valued.integer K)).FG

The maximal ideal of the valuation ring of a densely normed nonarchimedean field is not finitely generated: a generator would bound the norms of all elements of the open unit ball.