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.comap : an adic topology transports along an inducing ring equivalence, without separate assumptions that either ring has continuous operations.
• IsAdic.isOpen_pow : in a ring whose topology is I-adic, every power of I is open.
• IsAdic.isOpen_iff_le_of_isRadical : in a ring whose topology is I-adic, a radical ideal is open if and only if it contains I.
• 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.map_of_isOpenQuotientMap : an open quotient ring map transports an adic topology to the adic topology of the extended ideal, without finite generation or completeness.
• IsAdic.isOpenQuotientMap_of_surjective : conversely, a surjection onto a ring with the adic topology of the extended ideal is an open quotient map.
• 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.
• IsAdic.continuous_iff_map_le_radical and IsAdic.continuous_iff_forall_isTopologicallyNilpotent : when the source topology has some finitely generated ideal of definition, continuity can be tested on any ideals of definition, without requiring completeness or finite generation of the tested ideals.
• IsAdic.of_radical_eq and Ideal.adicTopology_eq_of_radical_eq : finitely generated ideals with the same radical define the same adic topology.
• IsAdic.isAdic_iff_isOpen_and_exists_pow_le : an ideal of definition is characterized by openness and containment of one of its powers in a fixed ideal of definition.
• IsAdic.exists_pow_succ_le : some positive power of an ideal of definition lies in any open ideal.
• IsAdic.exists_pow_succ_le_comap : a continuous ring homomorphism carries some positive power of an ideal of definition into any open ideal of its target.
• IsAdic.radical_eq, IsAdic.le_radical, and IsAdic.radical : ideals of definition have the same radical, and a finitely generated radical is the largest ideal of definition.

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.

The ideal-of-definition criterion and the results about radicals additionally follow A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique I, Ch. 0, §§7.1.4–7.1.7. The open-quotient transport theorem follows Ch. 0, (7.3.5).

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.discreteTopology_quotient {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I) : DiscreteTopology (R ⧸ I)

The quotient by an ideal of definition has the discrete quotient topology.

theorem IsAdic.comap {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} {S : Type u_2} [CommRing S] [TopologicalSpace S] (hI : IsAdic I) (e : S ≃+* R) (he : Topology.IsInducing ⇑e) : IsAdic (Ideal.comap e I)

An adic topology transports along a ring equivalence that is an inducing map.

Neither ring needs an explicit topological-ring assumption: the adic topology makes the target of the equivalence a topological ring, and the inducing map transports continuity to its source.

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.isOpen_iff_le_of_isRadical {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I) {P : Ideal R} (hP : P.IsRadical) : IsOpen ↑P ↔ I ≤ P

In a ring whose topology is the I-adic one, a radical ideal (for instance a prime ideal) is open if and only if it contains I: an open radical ideal contains a power of I, hence I itself.

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.radical_eq {R : Type u_1} [CommRing R] [TopologicalSpace R] {I J : Ideal R} (hI : IsAdic I) (hJ : IsAdic J) : I.radical = J.radical

Ideals defining the same adic topology have the same radical: both radicals consist of the topologically nilpotent elements.

theorem IsAdic.le_radical {R : Type u_1} [CommRing R] [TopologicalSpace R] {I J : Ideal R} (hI : IsAdic I) (hJ : IsAdic J) : I ≤ J.radical

Every ideal of definition is contained in the radical of any other ideal of definition.

theorem IsAdic.isAdic_iff_isOpen_and_exists_pow_le {R : Type u_1} [CommRing R] [TopologicalSpace R] {I J : Ideal R} (hI : IsAdic I) : IsAdic J ↔ IsOpen ↑J ∧ ∃ (n : ℕ), J ^ n ≤ I

An ideal defines the I-adic topology exactly when it is open and some power lies in I. No finite generation hypothesis is needed (EGA I, Ch. 0, 7.1.4).

theorem IsAdic.exists_pow_succ_le {R : Type u_1} [CommRing R] [TopologicalSpace R] {I J : Ideal R} (hI : IsAdic I) (hJ : IsOpen ↑J) : ∃ (n : ℕ), I ^ (n + 1) ≤ J

Some positive power of an ideal of definition lies in any open ideal.

theorem IsAdic.exists_pow_succ_le_comap {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 : IsOpen ↑J) {f : R →+* S} (hf : Continuous ⇑f) : ∃ (n : ℕ), I ^ (n + 1) ≤ Ideal.comap f J

A continuous ring homomorphism carries some positive power of an ideal of definition of its source into any open ideal of its target.

theorem IsAdic.radical {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I) (hfg : I.radical.FG) : IsAdic I.radical

The radical of an ideal of definition is again an ideal of definition whenever that radical is finitely generated, in particular over a noetherian ring (EGA I, Ch. 0, 7.1.7).

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.

theorem IsAdic.map_le_radical_of_continuous {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) {f : R →+* S} (hf : Continuous ⇑f) : Ideal.map f I ≤ J.radical

A continuous ring homomorphism carries an ideal of definition into the radical of every ideal of definition of its target. Unlike the converse, this needs no finite generation.

theorem IsAdic.continuous_iff_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} {K : Ideal R} (hI : IsAdic I) (hJ : IsAdic J) (hK : IsAdic K) (hKfg : K.FG) {f : R →+* S} : Continuous ⇑f ↔ Ideal.map f I ≤ J.radical

Continuity can be tested on arbitrary ideals of definition, provided some finitely generated ideal defines the source topology. The tested ideals need not be finitely generated, and neither ring needs to be complete.

theorem IsAdic.continuous_iff_forall_isTopologicallyNilpotent {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} {S : Type u_2} [CommRing S] [TopologicalSpace S] {J : Ideal S} {K : Ideal R} (hI : IsAdic I) (hJ : IsAdic J) (hK : IsAdic K) (hKfg : K.FG) {f : R →+* S} : Continuous ⇑f ↔ ∀ a ∈ I, IsTopologicallyNilpotent (f a)

When the source topology has a finitely generated ideal of definition, a ring homomorphism is continuous exactly when it sends every element of any ideal of definition to a topologically nilpotent element. Neither ring needs to be complete.

theorem IsAdic.of_radical_eq {R : Type u_1} [CommRing R] [TopologicalSpace R] {I J : Ideal R} (hI : IsAdic I) (hIfg : I.FG) (hJfg : J.FG) (h : I.radical = J.radical) : IsAdic J

A ring whose topology is the I-adic one is also J-adic for every finitely generated ideal J with the same radical as the finitely generated ideal I: each power of either ideal contains a power of the other.

theorem IsAdic.map_of_isOpenQuotientMap {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [TopologicalSpace R] [TopologicalSpace S] {I : Ideal R} (hI : IsAdic I) (f : R →+* S) (hf : IsOpenQuotientMap ⇑f) : IsAdic (Ideal.map f I)

An open quotient of an adic ring has the adic topology of the extended ideal. Neither finite generation nor completeness of the defining ideal is required, and the quotient needs no topological-ring assumption.

theorem IsAdic.isOpenQuotientMap_of_surjective {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [TopologicalSpace R] [TopologicalSpace S] {I : Ideal R} (hI : IsAdic I) {f : R →+* S} (hf : Function.Surjective ⇑f) (hS : IsAdic (Ideal.map f I)) : IsOpenQuotientMap ⇑f

Conversely, a surjective ring homomorphism out of an I-adic ring is an open quotient map when its target carries the adic topology of the extended ideal. Neither finite generation nor completeness of the defining ideal is required.

theorem Ideal.adicTopology_eq_of_radical_eq {R : Type u_1} [CommRing R] {I J : Ideal R} (hIfg : I.FG) (hJfg : J.FG) (h : I.radical = J.radical) : I.adicTopology = J.adicTopology

Finitely generated ideals with the same radical define the same adic topology.