Powers of the ideal defining an adic topology

For an ideal I of a commutative ring R, Mathlib's Ideal.openAddSubgroup records that each power I ^ n is an open additive subgroup of R carried with the topology I.adicTopology. A ring is usually met the other way round: it comes with a topology already, and IsAdic I is the statement that this topology is the I-adic one. The results here transport such facts across that equation — the openness, the complementary closedness, and the topological nilpotence of the elements of I — so that a ring satisfying IsAdic I may be used directly.

Closedness is the form these are wanted in: an infinite sum all of whose terms lie in I ^ n again lies in I ^ n, because I ^ n is closed and tsum_mem applies. That is how a power series evaluated at arguments of I ^ n is confined to I ^ n, in TauCeti.RingTheory.MvPowerSeries.Evaluation.

Main results

• IsAdic.isOpen_pow : in a ring whose topology is I-adic, every power of I is open.
• IsAdic.isClosed_pow : in a ring whose topology is I-adic, every power of I is closed — an open additive subgroup of a topological group being closed.
• IsAdic.tendsto_zero_of_mem_pow : a family whose members lie in growing powers of I tends to zero, provided the exponents tend to infinity.
• IsAdic.isTopologicallyNilpotent_of_mem : in a ring whose topology is I-adic, every element of I is topologically nilpotent.
• IsAdic.isTopologicallyNilpotent_iff_mem_radical : conversely, a topologically nilpotent element has a power in I, so the topologically nilpotent elements are exactly the radical of I.
• IsAdic.isLinearTopology : a ring whose topology is I-adic is linearly topologized, the IsAdic counterpart of Ideal.isLinearTopology.
• IsAdic.continuous_of_map_le_radical : a ring homomorphism from an I-adic ring to a J-adic ring is continuous when it carries the finitely generated ideal I into the radical of J.

Provenance

Adapted from Michael Stoll's EllipticCurves (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0) at commit 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e, file EllipticCurves/Mathlib/Chabauty/AdicTopology.lean, where these appear under the same names among that development's Mathlib-bound material. That file describes its contents as the IsAdic counterparts of Ideal.isLinearTopology and WithIdeal.isTopologicallyNilpotent_of_mem, which is the reading taken here.

theorem IsAdic.isOpen_pow {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I) (n : ℕ) : IsOpen ↑(I ^ n)

In a ring whose topology is the I-adic one, every power of I is open.

theorem IsAdic.isClosed_pow {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I) (n : ℕ) : IsClosed ↑(I ^ n)

In a ring whose topology is the I-adic one, every power of I is closed: it is an open additive subgroup, and an open subgroup of a topological group is closed.

theorem IsAdic.tendsto_zero_of_mem_pow {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I) {γ : Type u_2} {l : Filter γ} {g : γ → R} {e : γ → ℕ} (hg : ∀ᶠ (i : γ) in l, g i ∈ I ^ e i) (he : Filter.Tendsto e l Filter.atTop) : Filter.Tendsto g l (nhds 0)

In a ring whose topology is the I-adic one, a family whose members lie in growing powers of I tends to zero, provided the exponents tend to infinity. Only eventual membership is needed, since convergence along l cannot see failures outside an l-large set; a pointwise caller supplies Filter.Eventually.of_forall. The index filter is arbitrary: atTop for a sequence, cofinite for the decay condition of MvPowerSeries.HasEval. For the powers of a single element of I use IsAdic.isTopologicallyNilpotent_of_mem instead.

theorem IsAdic.isTopologicallyNilpotent_of_mem {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I) {a : R} (ha : a ∈ I) : IsTopologicallyNilpotent a

In a ring whose topology is the I-adic one, every element of I is topologically nilpotent.

theorem IsAdic.isTopologicallyNilpotent_iff_mem_radical {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I) {a : R} : IsTopologicallyNilpotent a ↔ a ∈ I.radical

In a ring whose topology is the I-adic one, the topologically nilpotent elements are exactly the elements of the radical of I: a power of a topologically nilpotent element lies in the open ideal I, and if a ^ n ∈ I then a ^ m ∈ I ^ k as soon as m ≥ n * k.

theorem IsAdic.isLinearTopology {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I) : IsLinearTopology R R

A ring whose topology is the I-adic one is linearly topologized: the powers of I form a neighbourhood basis of zero consisting of ideals. This is the IsAdic counterpart of Ideal.isLinearTopology.

theorem IsAdic.continuous_of_map_le_radical {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} {S : Type u_2} [CommRing S] [TopologicalSpace S] {J : Ideal S} (hI : IsAdic I) (hJ : IsAdic J) (hfg : I.FG) {f : R →+* S} (hf : Ideal.map f I ≤ J.radical) : Continuous ⇑f

A ring homomorphism from an I-adic ring to a J-adic ring is continuous as soon as it carries I into the radical of J, provided I is finitely generated. Mapping I into J itself is the special case J ≤ J.radical.