Rings and ideals of definition of a Huber ring #
Wedhorn's characterisation of the rings of definition, the enlargement constructions for pairs of
definition, and the two union descriptions they yield. On the ring side: Wedhorn's Lemma 6.2
and the parts of his Corollary 6.4 covered here — that A° is the union of the rings of definition,
that the subring generated by two rings of definition is again one, and that their intersection is
one too. Corollary 6.4(2) is not included. On the ideal side, a companion of the union
description: A°° is the union of the ideals of definition, and is therefore open.
Both sides live here because they share the enlargement machinery: the ring-side results rest on
PairOfDefinition.enlarge, and the ideal-side ones on PairOfDefinition.enlargeIdeal, which keeps
the ring and grows only the ideal. The ideal-side statement is also proved from the ring-side one,
reusing isPowerBounded_iff_exists_mem_ringOfDefinition below rather than rebuilding a pair.
The two ring-side parts rest on a single observation, isolated here as
PairOfDefinition.enlarge: a bounded subring containing a ring of definition is itself a ring of
definition. Openness is inherited
from the smaller ring, and the new ideal of definition is the Ideal.map of the old one, so
finite generation comes for free. Boundedness of the larger ring is the only real hypothesis, and
both applications get it from the lattice: A₀[T] is A₀ ⊔ Subring.closure T, bounded by
isBounded_sup against Wedhorn 5.30(2) (isBounded_subringClosure), which adjoin combines in
two lines at the point of use. The join case is PairOfDefinition.enlargeSup, which takes an
arbitrary bounded B; joining two rings of definition is the case where B is one of them.
Taking T = {a} in the first application proves that every power-bounded element belongs to some
ring of definition; the converse holds because every ring of definition is bounded.
Enlargement does not reach every ring of definition, and the last section of the file supplies
what does: Wedhorn Lemma 6.2, that the rings of definition are exactly the open bounded
subrings. Its content is the implication from openness and boundedness, since a ring of definition
is open by definition and bounded by PairOfDefinition.isBounded_ringOfDefinition. The proof
builds an ideal of definition for B out of a pair of definition (A₀, I) of A: choose k ≥ 1
with Iᵏ ⊆ B — possible because B is open — and let J be the ideal of B generated by the
degree-k monomials in a finite generating set of I. Then I^(k * (n + 1)) ⊆ Jⁿ makes every
power of J open, while boundedness of B puts Jᵐ inside Iᵐ · B and hence eventually inside
any neighbourhood of 0.
That criterion is what the enlargement constructions cannot give. The intersection half of
Corollary 6.4 is a case in point: A₀ ∩ A₁ is smaller than A₀, so an enlargement argument
would produce its ideal by Ideal.comap rather than Ideal.map, and a comap of a finitely
generated ideal need not be finitely generated. enlarge and its descendants are kept because
they name the ideal of definition of the larger ring explicitly — Ideal.map of the smaller
one — which Lemma 6.2, being an existence statement, does not.
Main results #
TauCeti.Huber.PairOfDefinition.enlarge: a bounded subring containing a ring of definition is a ring of definition.TauCeti.Huber.PairOfDefinition.adjoin: adjoining finitely many power-bounded elements gives another pair of definition.TauCeti.Huber.PairOfDefinition.enlargeSup: joining a ring of definition with any bounded subring gives a ring of definition, withenlargeSup_ringOfDefinition,enlargeSup_idealOfDefinition,le_enlargeSup_leftandle_enlargeSup_rightnaming its components and inclusions.TauCeti.Huber.PairOfDefinition.sup: the join of two rings of definition is a ring of definition.TauCeti.Huber.PairOfDefinition.enlargeIdeal: adjoining a topologically nilpotent element to the ideal of definition again gives a pair of definition, withenlargeIdeal_ringOfDefinitionandenlargeIdeal_idealOfDefinitionnaming its two components — the ring is unchanged and the ideal becomesI ⊔ span {y}— andmem_enlargeIdeal_idealOfDefinitionrecording that the adjoined element is in it, which is the form consumers use.TauCeti.Huber.isTopologicallyNilpotent_iff_exists_mem_idealOfDefinition: the topologically nilpotent elements are exactly the union of the ideals of definition — the ideal-side companion of Corollary 6.4 below.TauCeti.Huber.isOpen_setOf_isTopologicallyNilpotent: consequently the topologically nilpotent elements form an open set, each ideal of definition having open image inA.TauCeti.Huber.isPowerBounded_iff_exists_mem_ringOfDefinition: the power-bounded subring is the union of the rings of definition.TauCeti.Huber.exists_pairOfDefinition_ringOfDefinition_eq: Wedhorn Lemma 6.2 — an open bounded subring of a Huber ring is a ring of definition. The three-way form isTauCeti.Huber.exists_pairOfDefinition_ringOfDefinition_eq_tfae, which adds the intermediate condition "open with adic subspace topology" viaTauCeti.Huber.isBounded_of_isAdic, and the two-way criterion isTauCeti.Huber.exists_pairOfDefinition_ringOfDefinition_eq_iff.TauCeti.Huber.exists_pairOfDefinition_ringOfDefinition_eq_inf: Wedhorn Corollary 6.4(1), the intersection half — the intersection of two rings of definition is a ring of definition.TauCeti.Huber.exists_pairOfDefinition_le_le: Wedhorn Corollary 6.4(4) — a bounded subring inside an open subring is contained in a ring of definition inside that open subring. The case used in practice,TauCeti.Huber.exists_pairOfDefinition_ringOfDefinition_le, is that every open subring of a Huber ring contains a ring of definition.TauCeti.Huber.exists_pairOfDefinition_ringOfDefinition_eq_top_iff: Wedhorn Corollary 6.4(5) — a Huber ring is adic exactly when it is bounded in itself.
Provenance #
The adjoin construction — and hence the adic-topology argument now extracted from it as
enlarge — is adapted from AINTLIB's HuberRings.lean (Apache 2.0), branch dev/adic-spaces
at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c. Names and the proof are adjusted to Tau
Ceti's PairOfDefinition and boundedness APIs.
The ideal-side headline, isTopologicallyNilpotent_iff_exists_mem_idealOfDefinition, corresponds to
AINTLIB's topologicallyNilpotent_subseteq_union_definitionIdeals in
projects/AdicSpaces/Adic spaces/HuberRings.lean (Apache 2.0, same branch and commit). Only the
statement was consulted: AINTLIB's proof is a sorry, whose note blames missing
definition-ring-enlargement infrastructure. Tau Ceti already had the ring-side enlargement, and what
was missing was the ideal-side enlargeIdeal supplied here, so no proof was ported. The
component lemmas of enlargeIdeal and the openness corollary have no AINTLIB counterpart.
enlargeSup, sup and the boundedness input isBounded_sup are not covered by that
attribution: AINTLIB cites Corollary 6.4 only for its parts (1)–(3), and has no counterpart to the
join of a ring of definition with a bounded subring.
The Lemma 6.2 section has no source. At the same AINTLIB commit, HuberRings.lean,
Bounded.lean and OpenIdeals.lean state no criterion recognising an open bounded subring as a
ring of definition, and the pinned Mathlib has no Huber rings at all. The proof below is written
from Wedhorn's, whose T(k), U and l become the monomials of Gk, the images of the powers
of I, and the exponent k itself, Iᵏ ⊆ B playing both roles at once.
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Lemma 6.2 and Corollary 6.4.
Enlarging the ideal of definition #
Adjoining a topologically nilpotent element to the ideal of definition. The ring of
definition is unchanged and the ideal becomes I ⊔ span {y}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ring of definition is unchanged by enlargeIdeal.
The ideal of definition gains exactly y: it becomes I ⊔ span {y}.
The adjoined element lies in the enlarged ideal of definition. This is the introduction
rule the enlargement exists for, and it reaches the membership through
enlargeIdeal_idealOfDefinition rather than by unfolding the constructor.
The element is presented as ⟨(y : A), h⟩ over the enlarged ring of definition rather than as
y itself. The two rings are equal — that is enlargeIdeal_ringOfDefinition — but only by
unfolding enlargeIdeal, whose body is sealed, so y ∈ (Q.enlargeIdeal hy).idealOfDefinition
cannot be stated directly: its Membership instance would have to unify
↥Q.ringOfDefinition with ↥(Q.enlargeIdeal hy).ringOfDefinition. Taking the membership witness
as an argument is also exactly the shape the existential in
isTopologicallyNilpotent_iff_exists_mem_idealOfDefinition needs.
Deliberately not @[simp]: enlargeIdeal_idealOfDefinition already is, so simp rewrites the
ideal to I ⊔ span {y} and this statement's left-hand side is not in simp-normal form. It is an
introduction rule to exact, not a rewrite.
Enlarging a ring of definition. Any bounded subring B containing a ring of definition
A₀ is itself one, with the image of I as its ideal of definition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ring of definition of P.enlarge B hle hB is B.
The old ring of definition is contained in the enlarged one.
The ideal of definition of P.enlarge B hle hB is the image of I.
Adjoin a finite set of power-bounded elements to a pair of definition. The new ring of
definition is A₀[T], and its ideal of definition is generated by the image of the old ideal.
Equations
- P.adjoin T hT = P.enlarge (Subring.closure (↑P.ringOfDefinition ∪ ↑T)) ⋯ ⋯
Instances For
The ring of definition of P.adjoin T hT is the subring A₀[T].
The old ring of definition is contained in the enlarged ring of definition.
The ideal of definition after adjoining T is generated by the image of the old ideal.
Every adjoined element belongs to the enlarged ring of definition.
Joining a ring of definition with a bounded subring. For any bounded B, the join
A₀ ⊔ B is again a ring of definition. The join of two rings of definition is the case
B = A₁.
Equations
- P.enlargeSup B hB = P.enlarge (P.ringOfDefinition ⊔ B) ⋯ ⋯
Instances For
The ring of definition of P.enlargeSup B hB is A₀ ⊔ B.
The original ring of definition is contained in the join.
The adjoined subring is contained in the join — the defining property of the construction.
The ideal of definition of P.enlargeSup B hB is the image of I, as for any enlarge.
Wedhorn Corollary 6.4, the product half. The join of two rings of definition is again a ring of definition; its ideal of definition is the image of the first one's.
Equations
- P.sup Q = P.enlargeSup Q.ringOfDefinition ⋯
Instances For
The ring of definition of P.sup Q is A₀ ⊔ A₁.
The first ring of definition is contained in the join.
The second ring of definition is contained in the join.
The ideal of definition of P.sup Q is the image of P's.
Wedhorn Corollary 6.4: an element of a Huber ring is power-bounded exactly when it belongs
to some ring of definition. Equivalently, A° is the union of all rings of definition.
The ideal-side companion of Corollary 6.4: an element of a Huber ring is topologically nilpotent exactly when it belongs to some ideal of definition. Equivalently, the topologically nilpotent elements are the union of all ideals of definition.
The topologically nilpotent elements of a Huber ring form an open set, i.e. A°° is open
in A.
Wedhorn Lemma 6.2: the rings of definition are the open bounded subrings #
Wedhorn Lemma 6.2, the substantial implication. Every open bounded subring B of a Huber
ring is a ring of definition.
The ideal of definition is J = (Gk), generated in B by the degree-k monomials in a finite
generating set of an ideal of definition I, for an exponent k ≥ 1 large enough that Iᵏ ⊆ B.
Two inclusions make J adic: I^(k * (n + 1)) ⊆ Jⁿ makes every power of J open, and
boundedness of B — the hypothesis doing the real work — puts Jᵐ inside Iᵐ · B, which is
eventually inside any neighbourhood of 0.
Wedhorn Lemma 6.2, the easy implication (b) ⇒ (c). An open subring whose subspace
topology is adic is bounded: the powers of the ideal are open in B, hence open in A, and each
of them absorbs multiplication by B because it is an ideal of B.
No finite generation of J is asked, and A need not be Huber.
Wedhorn Lemma 6.2. For a subring B of a Huber ring the following are equivalent:
Bis a ring of definition, that is, it carries a finitely generated ideal whose adic topology is the subspace topology;Bis open and its subspace topology is adic for some — not necessarily finitely generated — ideal;Bis open and bounded.
The implication 1 → 2 forgets the finite generation, 2 → 3 is isBounded_of_isAdic, and
3 → 1 is exists_pairOfDefinition_ringOfDefinition_eq, which manufactures a finitely generated
ideal out of boundedness.
Wedhorn Lemma 6.2 as a criterion: the rings of definition of a Huber ring are exactly its open bounded subrings.
Additional parts of Wedhorn Corollary 6.4 (excluding part (2)) #
Wedhorn Corollary 6.4(1), the intersection half. The intersection of two rings of definition is a ring of definition: it is open as an intersection of two opens and bounded as a subset of either.
Unlike the join TauCeti.Huber.PairOfDefinition.sup, this cannot be obtained by enlargement —
the ideal would arrive by Ideal.comap rather than Ideal.map, and a comap of a finitely
generated ideal need not be finitely generated. It is Lemma 6.2 that supplies one.
Every open subring of a Huber ring contains a ring of definition: intersect any ring of definition with it and apply Lemma 6.2. This is the form in which Wedhorn Corollary 6.4(4) is used, for instance to choose a ring of definition inside a ring of integral elements.
Wedhorn Corollary 6.4(4). A bounded subring B contained in an open subring C is
contained in a ring of definition which is itself contained in C: the candidate is
(A₀ ⊓ C) ⊔ B, open because it contains the open A₀ ⊓ C and bounded as a join of two bounded
subrings.
Wedhorn Corollary 6.4(5). A Huber ring is adic — the whole ring is a ring of definition, so that its topology is the adic topology of a finitely generated ideal — exactly when it is bounded in itself.