Open ideals of a Huber ring

Fix a pair of definition (A₀, I) for a Huber ring A. The neighbourhoods of zero that are cofinal are the images of the powers Iⁿ in A, not the ideals they generate — an ideal span can be much larger than the additive subgroup it is spanned by. What makes the ideal statement work is that an ideal of A containing the image of Iⁿ automatically contains its span (I · A)ⁿ. So an ideal of A is open exactly when it contains one of those powers, and since I · A is finitely generated that is the same as asking I · A to lie in its radical.

Main results

• TauCeti.Huber.PairOfDefinition.extendedIdealOfDefinition_pow: the powers of I · A (defined in TauCeti/RingTheory/Huber/Basic.lean) are generated by the basic neighbourhoods of zero.
• TauCeti.Huber.PairOfDefinition.isOpen_iff_exists_pow_le: an ideal of A is open exactly when it contains a power of I · A.
• TauCeti.Huber.PairOfDefinition.isOpen_iff_le_radical: an ideal of A is open exactly when its radical contains I · A.
• TauCeti.Huber.PairOfDefinition.isOpen_mul: the product of two open ideals is open — the powers of I · A witnessing each add.
• TauCeti.Huber.PairOfDefinition.isOpen_map_of_isOpen_map_extendedIdealOfDefinition: a ring homomorphism that maps an ideal of definition to an open ideal maps every open ideal to an open ideal. A variant supplies the target pair of definition from its Huber structure.
• TauCeti.Huber.PairOfDefinition.isOpen_span_mul: the span of a pointwise product of sets is open when the two spans are.
• TauCeti.Huber.PairOfDefinition.isOpen_span_insert_mul_insert: its Finset form with the two denominators adjoined — the admissibility half of Wedhorn Remark 7.30(5).
• TauCeti.Huber.PairOfDefinition.exists_forall_mem_idealImage_exists_sum_eq: the sharpening of those criteria that the valuation theory needs — if a finite set T spans an open ideal, then a basic neighbourhood of zero consists of T-combinations whose coefficients lie in the image of the ideal of definition, hence are topologically nilpotent.
• TauCeti.Huber.isOpen_map_of_continuous_inverse: a ring homomorphism with a continuous inverse maps open ideals to open ideals.
• TauCeti.Huber.exists_finset_subset_isOpen_span: every neighbourhood of zero of a Huber ring contains a finite set generating an open ideal.
• TauCeti.Huber.exists_isOpen_span_forall_sub_mem_of_denseRange: along a continuous map with dense image out of a Huber ring, a finite set and a denominator downstairs are approximated, to within a neighbourhood of zero, by the image of a finite set that spans an open ideal.
• TauCeti.Huber.IsTateRing.isOpen_iff_eq_top: an ideal of a Tate ring is open exactly when it is the whole ring.
• TauCeti.Huber.IsTateRing.isOpen_map_of_isOpen: every ring homomorphism from a Tate ring maps open ideals to open ideals.

Provenance

AINTLIB formalises this same layer and was consulted for the choice of results; the statements, names and proofs here are independent of it. Its HuberRings.lean carries the extension I · A as PairOfDefinition.idealOfDefinition — a name this development gives to the ideal of A₀ itself, so extendedIdealOfDefinition is used here instead — with idealOfDefinition_fg proved, as fg_extendedIdealOfDefinition is, by Ideal.FG.map. Its projects/AdicSpaces/Adic spaces/OpenIdeals.lean is headed "We prove Lemma 6.6 … of [Wedhorn, Adic Spaces]" and reaches the radical criterion as ideal_isOpen_iff_topologicalNilradical_le_radical, phrased through the topological nilradical and hypothesising a finitely generated ideal of definition; the form below instead names the pair of definition and routes the whole lemma through Ideal.map_pow.

The product lemmas below are independent of it in a stronger sense: AINTLIB's ValuationSpectrum.HasRationalPresentation (projects/AdicSpaces/Adic spaces/RationalSubsets.lean) records only that a set is some R(T/s), with no openness condition on T A, so its HasRationalPresentation.inter is the set-level identity alone. Its blueprint asserts in prose that "the numerator family of the product still generates an open ideal", but that half is not formalised there and nothing could be ported.

References

• Wedhorn, Adic Spaces, Lemma 6.6 and Remark 7.30(5).
• AINTLIB, branch dev/adic-spaces, projects/AdicSpaces/Adic spaces/OpenIdeals.lean and HuberRings.lean.

theorem TauCeti.Huber.PairOfDefinition.extendedIdealOfDefinition_pow {A : Type u_1} [CommRing A] [TopologicalSpace A] (P : PairOfDefinition A) (n : ℕ) : P.extendedIdealOfDefinition ^ n = Ideal.span ↑(P.idealImage n)

The n-th power of I · A is generated by the n-th basic neighbourhood of zero: the image TauCeti.Huber.PairOfDefinition.idealImage n of Iⁿ in A.

theorem TauCeti.Huber.PairOfDefinition.isOpen_iff_exists_pow_le {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (a : Ideal A) : IsOpen ↑a ↔ ∃ (n : ℕ), P.extendedIdealOfDefinition ^ n ≤ a

Wedhorn Lemma 6.6: an ideal of a Huber ring is open exactly when it contains a power of the ideal I · A generated by an ideal of definition.

theorem TauCeti.Huber.PairOfDefinition.isOpen_iff_le_radical {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (a : Ideal A) : IsOpen ↑a ↔ P.extendedIdealOfDefinition ≤ a.radical

Wedhorn Lemma 6.6, radical form: an ideal of a Huber ring is open exactly when its radical contains the ideal I · A generated by an ideal of definition.

theorem TauCeti.Huber.PairOfDefinition.isOpen_mul {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) {a b : Ideal A} (ha : IsOpen ↑a) (hb : IsOpen ↑b) : IsOpen ↑(a * b)

The product of two open ideals is open. If a contains (I · A)ⁿ and b contains (I · A)ᵐ, then a * b contains (I · A)ⁿ⁺ᵐ. Note this is a statement about the product ideal, which is smaller than the intersection: openness survives the smaller of the two.

theorem TauCeti.Huber.PairOfDefinition.isOpen_map_of_isOpen_map_extendedIdealOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition A) (Q : PairOfDefinition B) (f : A →+* B) (hP : IsOpen ↑(Ideal.map f P.extendedIdealOfDefinition)) {a : Ideal A} (ha : IsOpen ↑a) : IsOpen ↑(Ideal.map f a)

A map taking an ideal of definition to an open ideal takes every open ideal to an open ideal. This criterion transports openness of ideals along ring homomorphisms once it is known for one ideal of definition.

theorem TauCeti.Huber.PairOfDefinition.isOpen_map_of_isOpen_map_extendedIdealOfDefinition_of_isHuberRing {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] (P : PairOfDefinition A) (f : A →+* B) (hP : IsOpen ↑(Ideal.map f P.extendedIdealOfDefinition)) {a : Ideal A} (ha : IsOpen ↑a) : IsOpen ↑(Ideal.map f a)

If the target is Huber, openness of the image of one ideal of definition implies openness of the image of every open ideal.

theorem TauCeti.Huber.PairOfDefinition.isOpen_span_mul {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) {S T : Set A} (hS : IsOpen ↑(Ideal.span S)) (hT : IsOpen ↑(Ideal.span T)) : IsOpen ↑(Ideal.span (S * T))

A span over a pointwise product of sets is open when the two factors' spans are, since Ideal.span_mul_span identifies it with the product ideal. This is the form Wedhorn's Remark 7.30(5) needs: the numerator set of an intersection of rational subsets is a pointwise product.

theorem TauCeti.Huber.PairOfDefinition.isOpen_span_insert_mul_insert {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) {T₁ T₂ : Finset A} {s₁ s₂ : A} (hT₁ : IsOpen ↑(Ideal.span ↑T₁)) (hT₂ : IsOpen ↑(Ideal.span ↑T₂)) : IsOpen ↑(Ideal.span ↑(insert s₁ T₁ * insert s₂ T₂))

The numerator set of an intersection of rational subsets spans an open ideal. Adjoining each denominator only enlarges a span, so this is isOpen_span_mul after two applications of Mathlib's Ideal.isOpen_of_isOpen_subideal. It is the admissibility half of Wedhorn Remark 7.30(5): the set identity TauCeti.ValuationSpectrum.rationalSubset_inter presents the intersection with numerators insert s₁ T₁ * insert s₂ T₂, and a rational subset is one whose numerator ideal is open.

theorem TauCeti.Huber.PairOfDefinition.exists_forall_mem_idealImage_exists_sum_eq {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (hT : IsOpen ↑(Ideal.span ↑T)) : ∃ (n : ℕ), ∀ a ∈ P.idealImage n, ∃ (w : A → A), (∀ t ∈ T, w t ∈ P.idealImage 1) ∧ ∑ t ∈ T, t * w t = a

An open numerator ideal swallows a whole neighbourhood of zero with coefficients that are themselves topologically nilpotent. If the ideal generated by a finite set T is open, then some basic neighbourhood Iⁿ of zero consists of combinations ∑ t ∈ T, t * w t whose coefficients w t lie in the image of the ideal of definition itself.

This sharpens TauCeti.Huber.PairOfDefinition.isOpen_iff_exists_pow_le, which only places Iⁿ inside the ideal T · A and so offers coefficients in A about which nothing is known. The sharpening is what a valuation-theoretic estimate needs: over a point of the adic spectrum a coefficient in A carries no bound at all, whereas one in I has value < 1 (an element of I is topologically nilpotent). Thus the resulting combination is strictly dominated by any chosen nonzero common upper bound for the values v t, such as a rational subset's denominator.

theorem TauCeti.Huber.isOpen_map_of_continuous_inverse {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] {φ : A →+* B} {ψ : B →+* A} (hψ : Continuous ⇑ψ) (hψφ : Function.LeftInverse ⇑ψ ⇑φ) (hφψ : Function.RightInverse ⇑ψ ⇑φ) {J : Ideal A} (hJ : IsOpen ↑J) : IsOpen ↑(Ideal.map φ J)

A ring homomorphism with a continuous inverse carries open ideals to open ideals: the image of an ideal is then its preimage under the inverse.

theorem TauCeti.Huber.exists_finset_subset_isOpen_span {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {V : Set A} (hV : V ∈ nhds 0) : ∃ (G : Finset A), ↑G ⊆ V ∧ IsOpen ↑(Ideal.span ↑G)

Every neighbourhood of zero of a Huber ring contains a finite set generating an open ideal. Unlike an open ideal itself, such a set can be chosen inside an arbitrarily small neighbourhood of zero.

theorem TauCeti.Huber.exists_isOpen_span_forall_sub_mem_of_denseRange {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing A] {φ : A →+* B} (hφc : Continuous ⇑φ) (hφ : DenseRange ⇑φ) {V : Set B} (hV : V ∈ nhds 0) {T : Finset B} (hT : 0 ∈ T) (s : B) : ∃ (T' : Finset A) (s' : A), IsOpen ↑(Ideal.span ↑T') ∧ (∀ t ∈ T, ∃ u ∈ Finset.image (⇑φ) T', t - u ∈ V) ∧ (∀ u ∈ Finset.image (⇑φ) T', ∃ t ∈ T, u - t ∈ V) ∧ s - φ s' ∈ V

A finite set and a denominator descend along a dense map, up to a neighbourhood of zero. Along a continuous φ : A → B with dense image out of a Huber ring A, a finite set T ∋ 0 of B is approximated within a neighbourhood V of zero, in both directions, by the image of a finite set of A that generates an open ideal, and an element s of B by the image of an element of A. The open-ideal condition is what makes the approximating data a presentation of a rational subset of Spa(A, A⁺), rather than merely a finite set and a denominator.

theorem TauCeti.Huber.IsTateRing.eq_top_of_isOpen {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] {J : Ideal A} (hJ : IsOpen ↑J) : J = ⊤

An open ideal in a Tate ring is the whole ring ⊤.

theorem TauCeti.Huber.IsTateRing.isOpen_map_of_isOpen {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] (f : A →+* B) {J : Ideal A} (hJ : IsOpen ↑J) : IsOpen ↑(Ideal.map f J)

A ring homomorphism from a Tate ring sends every open ideal to an open ideal.

@[simp]

theorem TauCeti.Huber.IsTateRing.isOpen_iff_eq_top {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] (J : Ideal A) : IsOpen ↑J ↔ J = ⊤

In a Tate ring, an ideal is open if and only if it is the whole ring ⊤.

theorem TauCeti.Huber.IsTateRing.not_isOpen_of_isMaximal {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] {𝔪 : Ideal A} (h𝔪 : 𝔪.IsMaximal) : ¬IsOpen ↑𝔪

No maximal ideal of a Tate ring is open. An open ideal is ⊤ and a maximal ideal is proper, so the two cannot meet. This is the sharp form: one maximal ideal is enough, and no hypothesis about the others is needed.

theorem TauCeti.Huber.IsTateRing.subsingleton_of_forall_isMaximal_isOpen {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] (hmax : ∀ (𝔪 : Ideal A), 𝔪.IsMaximal → IsOpen ↑𝔪) : Subsingleton A

Requiring every maximal ideal to be open forces a Tate ring to be zero, since a nonzero ring has a maximal ideal and IsTateRing.not_isOpen_of_isMaximal says that one cannot be open.

Worth naming because that hypothesis is easy to write down and impossible to satisfy. Wedhorn's Proposition 7.52(2) carries it, and the statements that inherit it — among them TauCeti.ValuationSpectrum.isUnit_of_forall_not_vle_zero — are therefore vacuous on exactly the affinoid rings they are meant for, since those are Tate.

Note the quantifier is doing real work: over the zero ring there is no maximal ideal, so hmax holds and the conclusion holds too. Dropping it to a single maximal ideal would give a statement whose own hypotheses are contradictory.