The open-ball ideal and Neumann estimates in ultrametric normed rings

Let R be an ultrametric seminormed ring with ‖1‖ = 1, and let R⁰ = Subring.unitClosedBall R be its closed unit ball. The elements of R⁰ of norm less than one form an ideal R⁰⁰ = TauCeti.unitBallIdeal R of R⁰. Its elements are topologically nilpotent in R (this is Mathlib's tendsto_pow_atTop_nhds_zero_of_norm_lt_one); conversely, for a power-multiplicative norm every topologically nilpotent element has norm less than one. Without power-multiplicativity the converse fails (in the dual numbers over ℚ_[p] with the maximum norm, ε is nilpotent of norm one), which is why the ideal is described by the norm.

If R is moreover a normed ring in which geometric series converge (for instance a complete one), the inverse of 1 - x for ‖x‖ < 1 is controlled exactly by the ultrametric inequality: ‖(1 - x)⁻¹‖ = 1 and ‖(1 - x)⁻¹ - 1‖ = ‖x‖. Consequently elements of R⁰ within distance less than one of 1 are units of R⁰, the ideal R⁰⁰ lies in the Jacobson radical of R⁰ when R is commutative, and units of the reduction R⁰ ⧸ R⁰⁰ lift to units of R⁰. When the norm of R is multiplicative, the units of R⁰ are exactly the units of R of norm one. For an ultrametric normed field K the ring K⁰ is local with maximal ideal K⁰⁰, so its reduction is the residue field. These are the facts about the unit ball that underlie reduction arguments for Banach modules over nonarchimedean Banach rings.

Conversely, a ring homomorphism into the closed unit ball of a seminormed ring with ‖1‖ = 1 maps units to elements of norm one. If its source is a local ring and it maps the maximal ideal into the open unit ball, it maps exactly the units to elements of norm one, and the maximal ideal is the preimage of the open unit ball. This needs no ultrametric hypothesis; the model case is the valuation ring of a nonarchimedean field.

Main definitions

• TauCeti.unitBallIdeal R: the ideal of elements of norm less than one in the closed unit ball.

Main results

• TauCeti.exists_norm_lt_one_forall_norm_le_of_fg: if the open-ball ideal is finitely generated, some element has the largest norm less than one.
• TauCeti.isTopologicallyNilpotent_iff_norm_lt_one_of_isPowMul: for a power-multiplicative norm, topological nilpotence is equivalent to norm less than one.
• TauCeti.norm_inverse_one_sub and TauCeti.norm_inverse_one_sub_sub_one: the ultrametric Neumann estimates ‖(1 - x)⁻¹‖ = 1 and ‖(1 - x)⁻¹ - 1‖ = ‖x‖ for ‖x‖ < 1.
• TauCeti.isUnit_unitClosedBall_of_norm_sub_one_lt: perturbations of one are units of the unit ball.
• TauCeti.unitBallIdeal_le_jacobson_bot: the open-ball ideal lies in the Jacobson radical of the unit ball, so the reduction map is a local homomorphism (TauCeti.isLocalHom_quotientMk_unitBallIdeal).
• TauCeti.isUnit_unitClosedBall_iff: for a multiplicative norm, the units of the unit ball are the units of norm one.
• TauCeti.isUnit_unitClosedBall_iff_norm_eq_one, TauCeti.isLocalRing_unitClosedBall and TauCeti.maximalIdeal_unitClosedBall: over an ultrametric normed division ring the unit ball is a local ring, and over an ultrametric normed field its maximal ideal is the open-ball ideal.
• TauCeti.isPrincipalIdealRing_unitClosedBall_of_norm_eq_zpow: if the nonzero norms of K are the integer powers of ‖π‖ for some 0 < ‖π‖ < 1, then K⁰ is a principal ideal ring.
• TauCeti.norm_map_eq_one_of_isUnit: a ring homomorphism into the closed unit ball maps units to elements of norm one.
• TauCeti.norm_map_eq_one_iff_isUnit and TauCeti.norm_map_lt_one_iff_mem_maximalIdeal: a ring homomorphism from a local ring into the closed unit ball, mapping the maximal ideal into the open unit ball, maps exactly the units to norm one and pulls the open unit ball back to the maximal ideal.

References

• S. Bosch, U. Güntzer and R. Remmert, Non-Archimedean Analysis, Springer, 1984, §1.2.
• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.

def TauCeti.unitBallIdeal (R : Type u_1) [SeminormedRing R] [IsUltrametricDist R] [NormOneClass R] : Ideal ↥(Subring.unitClosedBall R)

The open-ball ideal. In an ultrametric seminormed ring with ‖1‖ = 1, the elements of norm less than one form an ideal of the closed unit ball Subring.unitClosedBall R.

@[simp]

theorem TauCeti.mem_unitBallIdeal {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] [NormOneClass R] {x : ↥(Subring.unitClosedBall R)} : x ∈ unitBallIdeal R ↔ ‖↑x‖ < 1

An element of the closed unit ball lies in the open-ball ideal exactly when its norm is less than one.

theorem TauCeti.unitBallIdeal_ne_top (R : Type u_1) [SeminormedRing R] [IsUltrametricDist R] [NormOneClass R] : unitBallIdeal R ≠ ⊤

The open-ball ideal is proper, since ‖1‖ = 1.

theorem TauCeti.exists_norm_lt_one_forall_norm_le_of_fg {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] [NormOneClass R] (h : (unitBallIdeal R).FG) : ∃ (π : R), ‖π‖ < 1 ∧ ∀ (a : R), ‖a‖ < 1 → ‖a‖ ≤ ‖π‖

A largest norm below one. If the open-ball ideal is finitely generated, for instance when the closed unit ball is noetherian, some π has the largest norm less than one: the generator of largest norm bounds every combination of the generators, by the ultrametric inequality.

theorem TauCeti.isTopologicallyNilpotent_iff_norm_lt_one_of_isPowMul {R : Type u_1} [SeminormedRing R] (hR : IsPowMul fun (x : R) => ‖x‖) {x : R} : IsTopologicallyNilpotent x ↔ ‖x‖ < 1

Topological nilpotence for power-multiplicative norms. If ‖x ^ n‖ = ‖x‖ ^ n for all n ≥ 1, then x is topologically nilpotent exactly when ‖x‖ < 1. The implication from right to left holds for every seminormed ring (tendsto_pow_atTop_nhds_zero_of_norm_lt_one).

@[simp]

theorem TauCeti.norm_inverse_one_sub {R : Type u_1} [NormedRing R] [NormOneClass R] [HasSummableGeomSeries R] [IsUltrametricDist R] {x : R} (hx : ‖x‖ < 1) : ‖Ring.inverse (1 - x)‖ = 1

Ultrametric Neumann estimate. In a normed ring with ‖1‖ = 1, convergent geometric series and an ultrametric norm, the inverse of 1 - x has norm one whenever ‖x‖ < 1.

@[simp]

theorem TauCeti.norm_inverse_one_sub_sub_one {R : Type u_1} [NormedRing R] [NormOneClass R] [HasSummableGeomSeries R] [IsUltrametricDist R] {x : R} (hx : ‖x‖ < 1) : ‖Ring.inverse (1 - x) - 1‖ = ‖x‖

Ultrametric Neumann estimate. In a normed ring with ‖1‖ = 1, convergent geometric series and an ultrametric norm, ‖(1 - x)⁻¹ - 1‖ = ‖x‖ whenever ‖x‖ < 1.

theorem TauCeti.isUnit_unitClosedBall_of_norm_sub_one_lt {R : Type u_1} [NormedRing R] [NormOneClass R] [HasSummableGeomSeries R] [IsUltrametricDist R] {x : ↥(Subring.unitClosedBall R)} (hx : ‖↑x - 1‖ < 1) : IsUnit x

Units of the unit ball. In a normed ring with ‖1‖ = 1, convergent geometric series and an ultrametric norm, an element of the closed unit ball within distance less than one of 1 is a unit of the closed unit ball: its inverse again has norm one.

theorem TauCeti.unitBallIdeal_le_jacobson_bot (R : Type u_1) [NormedCommRing R] [NormOneClass R] [HasSummableGeomSeries R] [IsUltrametricDist R] : unitBallIdeal R ≤ ⊥.jacobson

The open-ball ideal lies in the Jacobson radical of the unit ball. In a commutative normed ring with ‖1‖ = 1, convergent geometric series and an ultrametric norm, every element x of norm less than one makes x * y + 1 a unit of the unit ball for each y in it.

instance TauCeti.isLocalHom_quotientMk_unitBallIdeal (R : Type u_1) [NormedCommRing R] [NormOneClass R] [HasSummableGeomSeries R] [IsUltrametricDist R] : IsLocalHom (Ideal.Quotient.mk (unitBallIdeal R))

Unit lifting. The reduction map from the unit ball to its quotient by the open-ball ideal is a local homomorphism: an element of the unit ball whose reduction is a unit is itself a unit of the unit ball.

theorem TauCeti.isUnit_unitClosedBall_iff {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] [NormOneClass R] [NormMulClass R] {x : ↥(Subring.unitClosedBall R)} : IsUnit x ↔ IsUnit ↑x ∧ ‖↑x‖ = 1

Units of the unit ball for a multiplicative norm. An element of the closed unit ball is a unit of the unit ball exactly when it is a unit of the ambient ring and has norm one. A unit of norm less than one, such as a nonzero scalar of small norm, is therefore not a unit of the unit ball.

theorem TauCeti.isUnit_unitClosedBall_iff_norm_eq_one {K : Type u_1} [NormedDivisionRing K] [IsUltrametricDist K] {x : ↥(Subring.unitClosedBall K)} : IsUnit x ↔ ‖↑x‖ = 1

Over an ultrametric normed division ring, an element of the closed unit ball is a unit of the unit ball exactly when its norm is one.

instance TauCeti.isLocalRing_unitClosedBall {K : Type u_1} [NormedDivisionRing K] [IsUltrametricDist K] : IsLocalRing ↥(Subring.unitClosedBall K)

The unit ball of an ultrametric normed division ring is a local ring. For x in the unit ball, either ‖x‖ = 1 or ‖1 - x‖ = 1, so x or 1 - x is a unit.

theorem TauCeti.maximalIdeal_unitClosedBall {K : Type u_1} [NormedField K] [IsUltrametricDist K] : IsLocalRing.maximalIdeal ↥(Subring.unitClosedBall K) = unitBallIdeal K

The residue ring of an ultrametric normed field. The maximal ideal of the unit ball is the open-ball ideal, so the reduction K⁰ ⧸ K⁰⁰ is the residue field of K⁰.

instance TauCeti.isMaximal_unitBallIdeal {K : Type u_1} [NormedField K] [IsUltrametricDist K] : (unitBallIdeal K).IsMaximal

Over an ultrametric normed field the open-ball ideal is maximal, so the reduction K⁰ ⧸ K⁰⁰ is a field (Ideal.Quotient.field).

theorem TauCeti.isPrincipalIdealRing_unitClosedBall_of_norm_eq_zpow {K : Type u_1} [NormedField K] [IsUltrametricDist K] {π : K} (hπ0 : 0 < ‖π‖) (hπ1 : ‖π‖ < 1) (hdisc : ∀ (x : K), x ≠ 0 → ∃ (k : ℤ), ‖x‖ = ‖π‖ ^ k) : IsPrincipalIdealRing ↥(Subring.unitClosedBall K)

Discretely valued fields. If every nonzero norm of K is an integer power of ‖π‖ for some 0 < ‖π‖ < 1, then the unit ball K⁰ is a principal ideal ring, hence noetherian: a nonzero ideal is generated by any of its elements of largest norm.

theorem TauCeti.norm_map_eq_one_of_isUnit {O : Type u_1} {R : Type u_2} [Semiring O] [SeminormedRing R] [NormOneClass R] {φ : O →+* R} (hφ : ∀ (x : O), ‖φ x‖ ≤ 1) {x : O} (hx : IsUnit x) : ‖φ x‖ = 1

A ring homomorphism into the closed unit ball of a normed ring maps units to elements of norm one.

theorem TauCeti.norm_map_eq_one_iff_isUnit {O : Type u_1} {R : Type u_2} [CommRing O] [IsLocalRing O] [SeminormedRing R] [NormOneClass R] {φ : O →+* R} (hφ : ∀ (x : O), ‖φ x‖ ≤ 1) (hm : ∀ x ∈ IsLocalRing.maximalIdeal O, ‖φ x‖ < 1) {x : O} : ‖φ x‖ = 1 ↔ IsUnit x

A ring homomorphism from a local ring into the closed unit ball of a normed ring, mapping the maximal ideal into the open unit ball, maps exactly the units to elements of norm one.

theorem TauCeti.norm_map_lt_one_iff_mem_maximalIdeal {O : Type u_1} {R : Type u_2} [CommRing O] [IsLocalRing O] [SeminormedRing R] [NormOneClass R] {φ : O →+* R} (hφ : ∀ (x : O), ‖φ x‖ ≤ 1) (hm : ∀ x ∈ IsLocalRing.maximalIdeal O, ‖φ x‖ < 1) {x : O} : ‖φ x‖ < 1 ↔ x ∈ IsLocalRing.maximalIdeal O

A ring homomorphism from a local ring into the closed unit ball of a normed ring, mapping the maximal ideal into the open unit ball, pulls the open unit ball back to the maximal ideal.