Finitely generated adic rings are Huber rings

Let A be a commutative topological ring whose topology is I-adic. If I is finitely generated, then (A, I) is a pair of definition: the ring of definition is all of A, and the ideal of definition is I, transported to the top subring. Consequently A is a Huber ring. Such a ring is a Tate ring only in the degenerate case I = ⊤: a power of a topologically nilpotent element lies in I.

This is the bridge from algebraic adic completeness to Huber theory. In particular, Mathlib's IsAdic.isAdicComplete_iff can be applied to an adically complete ring equipped with its adic topology, while isHuberRing_adicTopology supplies its Huber structure. The construction is used for Witt-vector rings with their (p, [ϖ])-adic topology.

Main definitions

• TauCeti.Huber.PairOfDefinition.adic: the pair of definition (A, I) associated to a finitely generated ideal defining the topology.

Main results

• TauCeti.Huber.PairOfDefinition.adic_extendedIdealOfDefinition: the ideal of definition of this pair, extended to A, is I.
• TauCeti.Huber.PairOfDefinition.adic_idealImage: the neighbourhood subgroup furnished by this pair in degree n is exactly I ^ n.
• TauCeti.Huber.isHuberRing_of_isAdic: a ring with a finitely generated ideal defining its topology is Huber.
• TauCeti.Huber.isHuberRing_adicTopology: a commutative ring equipped with the adic topology of a finitely generated ideal is Huber.
• TauCeti.Huber.IsTateRing.eq_top_of_isAdic and TauCeti.Huber.isTateRing_iff_eq_top_of_isAdic: an adic ring is Tate only in the degenerate case I = ⊤, where the topology is indiscrete. So ℤ_[p] and W(𝒪_F) with its (p, [ϖ])-adic topology are Huber rings that are not Tate.

References

• T. Wedhorn, Adic Spaces, the definition of an f-adic ring in §6.

noncomputable def TauCeti.Huber.PairOfDefinition.adic {A : Type u_1} [CommRing A] [TopologicalSpace A] (I : Ideal A) (hI : IsAdic I) (hfg : I.FG) : PairOfDefinition A

The pair of definition (A, I) attached to a finitely generated ideal I defining the topology of A.

The ideal is transported to the top subring because a PairOfDefinition stores its ideal in its ring of definition, even when that ring of definition is all of A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.adic_ringOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] (I : Ideal A) (hI : IsAdic I) (hfg : I.FG) : (adic I hI hfg).ringOfDefinition = ⊤

@[simp]

theorem TauCeti.Huber.PairOfDefinition.mem_adic_idealOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] (I : Ideal A) (hI : IsAdic I) (hfg : I.FG) {x : ↥(adic I hI hfg).ringOfDefinition} : x ∈ (adic I hI hfg).idealOfDefinition ↔ ↑x ∈ I

Membership in the ideal of definition of adic I hI hfg is membership in I.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.adic_extendedIdealOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] (I : Ideal A) (hI : IsAdic I) (hfg : I.FG) : (adic I hI hfg).extendedIdealOfDefinition = I

The ideal of definition of adic I hI hfg, extended to A, is I.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.adic_idealImage {A : Type u_1} [CommRing A] [TopologicalSpace A] (I : Ideal A) (hI : IsAdic I) (hfg : I.FG) (n : ℕ) : (adic I hI hfg).idealImage n = Submodule.toAddSubgroup (I ^ n)

The n-th neighbourhood subgroup supplied by the adic pair is I ^ n itself.

theorem TauCeti.Huber.isHuberRing_of_isAdic {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (I : Ideal A) (hI : IsAdic I) (hfg : I.FG) : IsHuberRing A

A commutative topological ring is Huber when its topology is defined by a finitely generated ideal.

theorem TauCeti.Huber.isHuberRing_adicTopology {A : Type u_2} [CommRing A] (I : Ideal A) (hfg : I.FG) : IsHuberRing A

A commutative ring equipped with the adic topology of a finitely generated ideal is a Huber ring. This form lets callers install the topology and Huber structure together without first naming the tautological proof IsAdic I.

theorem TauCeti.Huber.IsTateRing.eq_top_of_isAdic {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] {I : Ideal A} (hI : IsAdic I) : I = ⊤

An adic ring is Tate only for the unit ideal. If the topology of A is I-adic and A has a pseudouniformiser a, then some power of a lies in the open ideal I, and that power is a unit.

theorem TauCeti.Huber.isTateRing_iff_eq_top_of_isAdic {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {I : Ideal A} (hI : IsAdic I) : IsTateRing A ↔ I = ⊤

An adic ring is Tate exactly when its ideal is the unit ideal. For I = ⊤ the topology is indiscrete and 1 is a pseudouniformiser; otherwise TauCeti.Huber.IsTateRing.eq_top_of_isAdic applies.