The plus ring A_U⁺ of a rational localisation #
For a rational subset U = R(T/s) of Spa(A, A⁺), Wedhorn (§8.1) completes the affinoid ring
(Aₛ, C), where C is the integral closure of A⁺[T/s] in Aₛ — a ring of integral elements of
the localised topology. The plus ring of A_U = A⟨T/s⟩ is therefore A_U⁺, the closure in
A⟨T/s⟩ of the image of C. This file defines it and proves that it is a ring of integral
elements of A_U, so that (A_U, A_U⁺) is a Huber pair.
The layers #
Algebra.adjoin A⁺ {t/s} A⁺[t₁/s, …, tₙ/s] (Mathlib's, unwrapped) ⊆ Aₛ
integralClosure A⁺[T/s] Aₛ C, a ring of integral elements of Aₛ ⊆ Aₛ
completedPlusSubring the closure of the image of C ⊆ A⟨T/s⟩
Why not the integral closure of the image #
An alternative definition of A_U⁺ is the integral closure in A_U of the image of A⁺[T/s].
That subring need not be open, so (A_U, A_U⁺) would not be a Huber pair: for
A = ℚ with the p-adic topology, A⁺ = ℤ_(p), T = {1} and s = 1, the completion is ℚ_p,
and the integral closure of ℤ_(p) in ℚ_p consists of elements algebraic over ℚ, a countable
set, whereas every nonempty open subset of ℚ_p is uncountable. The closure of the image of C
is open because C is, and it is integrally closed by Huber's Lemma 2.4.3(iv)
(UniformSpace.Completion.isIntegrallyClosedIn_topologicalClosure_map_coeRingHom), the half of
Wedhorn's Lemma 7.47(4) that this file needs.
Main definitions #
Main results #
TauCeti.Huber.PairOfDefinition.isRingOfIntegralElements_completedPlusSubring: whenA⁺consists of power-bounded elements and contains the image of the ideal of definition,A_U⁺is a ring of integral elements ofA⟨T/s⟩. Its three conditions are also available one at a time, each under the hypothesis it uses:isOpen_completedPlusSubringandisIntegrallyClosedIn_completedPlusSubringunder the ideal-of-definition hypothesis alone, andcompletedPlusSubring_le_powerBoundedSubringunder power-boundedness alone, the last also elementwise asisPowerBounded_of_mem_completedPlusSubring.TauCeti.Huber.PairOfDefinition.completionLocalization_ringOfDefinition_le_completedPlusSubring:A_U⁺contains the ring of definition ofA⟨T/s⟩whenA⁺contains that ofA.TauCeti.Huber.PairOfDefinition.coeRingHom_mem_completedPlusSubring: the completion map carriesCintoA_U⁺, making it a morphism of pairs(A(T/s), C) → (A⟨T/s⟩, A_U⁺).TauCeti.Huber.PairOfDefinition.toCompletionLoc_mem_completedPlusSubringandTauCeti.Huber.PairOfDefinition.divBy_mem_completedPlusSubring: the image ofA⁺and each fractiont/slie inA_U⁺.TauCeti.Huber.PairOfDefinition.isPowerBounded_of_mem_adjoin_plus: when every element ofA⁺is power-bounded inA, so is every element ofA⁺[T/s]inAₛ.TauCeti.Huber.PairOfDefinition.locSubring_mul_idealOfDefinition_mem_adjoin_plus: the absorption itself — insideAₛ, an element ofD = A₀[T/s]times an element of the ideal of definitionIlies inA⁺[T/s].TauCeti.Huber.PairOfDefinition.locIdealImage_one_le_adjoin_plus: insideAₛ,A⁺[T/s]absorbs the first basic neighbourhood of zero, which makes it open.TauCeti.Huber.PairOfDefinition.isOpen_adjoin_plus_toSubring: that openness itself, atlocTopology.TauCeti.Huber.PairOfDefinition.isRingOfIntegralElements_integralClosure_adjoin_plus: under the same hypotheses,Cis a ring of integral elements ofAₛ.TauCeti.Huber.PairOfDefinition.isOpen_integralClosure_adjoin_plus: openness ofCon its own, at the topology oflocUniformSpace.
Provenance #
AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0, branch dev/adic-spaces at 37bbdaeb9)
carries a version of this construction in projects/AdicSpaces/Adic spaces/Presheaf.lean as
RationalLocData.locPlusSubring, completedPlusSubringBase and completedPlusSubring; its
completedPlusSubringBase is the closure of the image of (A⁺[T/s])^int, the object defined here.
The absorption results are adapted from the same AINTLIB file:
locSubring_mul_idealOfDefinition_mem_adjoin_plus and locIdealImage_one_le_adjoin_plus follow
RationalLocData.locNhd_one_subset_locPlusSubring and the neighbourhood step of
RationalLocData.completedPlusSubringBase_isOpen. isPowerBounded_of_mem_adjoin_plus and the
power-boundedness half of isRingOfIntegralElements_integralClosure_adjoin_plus follow
RationalLocData.locPlusSubring_le_powerBounded and
RationalLocData.integralClosure_locPlusSubring_le_powerBounded. Integral closedness of A_U⁺
comes instead from this repository's Huber 2.4.3(iv). No proof text was copied.
References #
- Wedhorn, Adic Spaces, §8.1, §8.2, 8.16, 7.19, 7.20 and 7.47(4).
A_U⁺, Wedhorn's plus ring of A⟨T/s⟩: the closure in A⟨T/s⟩ of the image of C, the
integral closure of A⁺[T/s] in Aₛ. It needs no hypothesis on Aplus; under the hypotheses of
isRingOfIntegralElements_completedPlusSubring it is a ring of integral elements of A⟨T/s⟩.
Under the same hypotheses C is a ring of integral elements of Aₛ
(isRingOfIntegralElements_integralClosure_adjoin_plus), and A_U⁺ is its completed counterpart.
It is not the integral closure in A⟨T/s⟩ of the image of A⁺[T/s], a subring that need not be
open. The body is not exposed: coe_completedPlusSubring describes it as a set, and
toCompletionLoc_mem_completedPlusSubring and divBy_mem_completedPlusSubring show that it
contains the image of A⁺ and each t/s.
Equations
- One or more equations did not get rendered due to their size.
Instances For
As a set, A_U⁺ is the closure in A⟨T/s⟩ of the image of C, the integral closure of
A⁺[T/s] in Aₛ. The body of completedPlusSubring is not exposed, so this is how a consumer
unfolds it; UniformSpace.Completion.coe_topologicalClosure_map_coeRingHom is the same equation
for the closure of the image of an arbitrary subring. Here Aₛ carries locUniformSpace, so a
fact about Aₛ stated at locTopology, such as the openness of C, must first be moved across
locUniformSpace_toTopologicalSpace.
Membership in A_U⁺: an element of A⟨T/s⟩ lies in A_U⁺ exactly when it lies in the
closure of the image of C, the integral closure of A⁺[T/s] in Aₛ. This is the membership
form of coe_completedPlusSubring.
A_U⁺ is the smallest closed subring containing the image of C, the integral closure
of A⁺[T/s] in Aₛ: a closed subring of A⟨T/s⟩ contains A_U⁺ exactly when it contains the
image of every element of C.
A_U⁺ is closed in A⟨T/s⟩, with no hypothesis on Aplus.
The image of C lies in A_U⁺. The completion map A(T/s) → A⟨T/s⟩ carries the
integral closure C of A⁺[T/s] in A(T/s) into the plus ring of the completed localization,
which is by definition the closure of that image. Together with
UniformSpace.Completion.continuous_coeRingHom this makes the completion map a morphism of pairs
(A(T/s), C) → (A⟨T/s⟩, A_U⁺), the second factor of the structure map ρ : A → A⟨T/s⟩; the
first factor is covered by algebraMap_mem_integralClosure_adjoin_plus.
The structure map A → A⟨T/s⟩ carries A⁺ into A_U⁺, with no hypothesis on Aplus.
Together with continuous_toCompletionLoc, this makes the structure map a morphism of pairs
(A, A⁺) → (A⟨T/s⟩, A_U⁺). The companion divBy_mem_completedPlusSubring puts each fraction t/s
in A_U⁺ as well.
Each fraction t/s with t ∈ T lies in A_U⁺, with no hypothesis on Aplus. Here
t/s is divBy t s in Aₛ, carried into A⟨T/s⟩ by the completion map. The companion
toCompletionLoc_mem_completedPlusSubring puts the image of A⁺ in A_U⁺; together they give
the plus-ring conditions of the universal property of the rational localisation. A goal phrased
as the image of t times the inverse of the image of s is first rewritten into this form by
toCompletionLoc_mul_unit_inv_eq_divBy.
A_U⁺ contains the ring of definition of A⟨T/s⟩ when A⁺ contains the ring of definition
A₀ of A. The ring of definition of A⟨T/s⟩ is the closure of the image of A₀[T/s], and
A₀[T/s] ⊆ A⁺[T/s]. This is the hypothesis under which (A⟨T/s⟩, A_U⁺) and its pair of
definition completionLocalization P T s S hden carry the rational localisations and the
structure presheaf of Spa(A⟨T/s⟩, A_U⁺).
When every element of A⁺ is power-bounded, so is every element of A⁺[T/s], inside Aₛ
and before any completion. This is the pre-completion half of the power-boundedness of A_U⁺ in
TauCeti.Huber.PairOfDefinition.isRingOfIntegralElements_completedPlusSubring.
A⁺[T/s] absorbs the ideal of definition, inside Aₛ and before any completion: for c
in the ring of definition D = A₀[T/s] of the localised topology and i in the ideal of
definition I, the product c · i already lies in the subring A⁺[T/s] whose integral closure
C underlies A_U⁺. This is the absorption itself; locIdealImage_one_le_adjoin_plus
packages it as a statement about the first basic neighbourhood of zero. The strategy is
Wedhorn's, in the proofs of Proposition 7.19 and Lemma 7.20.
Two facts carry it. The image of I lies in Aplus, which is the hypothesis hIplus; and I
is an ideal of A₀, so a coefficient contributed by A₀ can be pushed onto the numerator
instead. Only the containment is needed, not power-boundedness or a nonarchimedean topology: for a
ring of integral elements A⁺ it is discharged by
TauCeti.Huber.IsRingOfIntegralElements.mem_of_isTopologicallyNilpotent applied to
TauCeti.Huber.PairOfDefinition.isTopologicallyNilpotent_of_mem_idealOfDefinition.
A⁺[T/s] absorbs the first basic neighbourhood of zero, inside Aₛ and before any
completion: the image in Aₛ of J = I · D, for D = A₀[T/s] the ring of definition of the
localised topology, lies in the subring A⁺[T/s].
This is the openness step for A_U⁺. Once Aₛ carries the localised topology — which needs
TauCeti.Huber.PairOfDefinition.HasDenominatorPower — the sets locIdealImage P T s S n are a
neighbourhood basis of zero, so absorbing the first of them is what makes A⁺[T/s] an open
subgroup of Aₛ. Its integral closure C, and then the closure of the image of C in
A⟨T/s⟩, inherit the openness.
Only the packaging is here. J is spanned over D by the image of I, so a span induction
reduces the containment to the absorption itself,
TauCeti.Huber.PairOfDefinition.locSubring_mul_idealOfDefinition_mem_adjoin_plus.
A⁺[T/s] is open in Aₛ at the localised topology, as soon as A⁺ contains the image of
the ideal of definition. This is the openness that C, and then A_U⁺, inherit.
The statement is at locTopology; a consumer working at the topology of locUniformSpace, the
one A⟨T/s⟩ completes, moves it across locUniformSpace_toTopologicalSpace.
A⁺ maps into C, the integral closure of A⁺[T/s] in Aₛ: an element of A⁺ lands in
the adjoined subring already, hence in its integral closure. No topology is involved.
When A⁺ consists of power-bounded elements and contains the image of the ideal of
definition, the integral closure of A⁺[T/s] in Aₛ is a ring of integral elements of the
localised topology: it is open, integrally closed in Aₛ, and contained in (Aₛ)°. Those are the
three conditions a Huber pair asks of its plus ring.
The integral closure is taken here in Aₛ, not in A⟨T/s⟩;
isRingOfIntegralElements_completedPlusSubring carries the three conditions to the closure of its
image in A⟨T/s⟩, which is A_U⁺.
C is open in Aₛ, the integral closure of A⁺[T/s] in the localisation, as soon as A⁺
contains the image of the ideal of definition.
This supplies the openness of C under hIplus alone, which is the form the completion statements
isOpen_completedPlusSubring and isIntegrallyClosedIn_completedPlusSubring consume;
isRingOfIntegralElements_integralClosure_adjoin_plus gives the same openness alongside its other
two conditions, under hAplus as well. The conclusion is at the topology of locUniformSpace, the
one A⟨T/s⟩ completes.
A_U⁺ lies in (A⟨T/s⟩)° as soon as every element of A⁺ is power-bounded. This is the
power-boundedness condition of isRingOfIntegralElements_completedPlusSubring, and unlike that
theorem it needs no hypothesis on the ideal of definition: enlarging a plus ring of A⟨T/s⟩ from
A_U⁺ to (A⟨T/s⟩)° along it only shrinks the adic spectrum.
Every element of A_U⁺ is power-bounded in A⟨T/s⟩ as soon as every element of A⁺ is
power-bounded in A. This is completedPlusSubring_le_powerBoundedSubring read elementwise,
which is the shape ∀ ⦃a⦄, a ∈ A⁺ → IsPowerBounded a of the power-boundedness hypothesis on a
plus ring.
A_U⁺ is open in A⟨T/s⟩ as soon as A⁺ contains the image of the ideal of definition.
This is the openness condition of isRingOfIntegralElements_completedPlusSubring, available here
under hIplus alone: openness makes no reference to (A⟨T/s⟩)°, so no power-boundedness
hypothesis enters.
A_U⁺ is integrally closed in A⟨T/s⟩ as soon as A⁺ contains the image of the ideal of
definition — Huber's Lemma 2.4.3(iv) for A_U⁺.
This is the integral-closedness condition of isRingOfIntegralElements_completedPlusSubring,
available here under hIplus alone, with no power-boundedness hypothesis.
(A⟨T/s⟩, A_U⁺) is a Huber pair: when A⁺ consists of power-bounded elements and contains
the image of the ideal of definition, A_U⁺ is a ring of integral elements of A⟨T/s⟩.
The three conditions are isOpen_completedPlusSubring,
isIntegrallyClosedIn_completedPlusSubring and completedPlusSubring_le_powerBoundedSubring,
each of which is available separately under the hypothesis it actually uses: the first two under
hIplus alone, the third under hAplus alone. Every ring of integral elements A⁺ of A
satisfies both hypotheses: hAplus is
TauCeti.Huber.IsRingOfIntegralElements.le_powerBoundedSubring, and hIplus follows from
TauCeti.Huber.IsRingOfIntegralElements.mem_of_isTopologicallyNilpotent applied to
TauCeti.Huber.PairOfDefinition.isTopologicallyNilpotent_of_mem_idealOfDefinition.