Huber rings and Tate rings #
A pair of definition for a topological ring A is an open subring A₀ ⊆ A together with a
finitely generated ideal I ⊆ A₀ whose adic topology is the subspace topology of A₀. A ring
admitting one is a Huber ring (Wedhorn's f-adic ring), and a Huber ring containing a
topologically nilpotent unit is a Tate ring.
Everything the later layers use about the topology of a Huber ring comes from one statement: the
images in A of the powers Iⁿ are a neighbourhood basis of zero
(TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero). They are open additive subgroups, so a
Huber ring is nonarchimedean, which is exactly the hypothesis under which
TauCeti/RingTheory/Huber/PowerBounded.lean makes A° a subring.
Main definitions #
TauCeti.Huber.PairOfDefinition: a pair of definition(A₀, I)forA.TauCeti.Huber.IsHuberRing:Aadmits a pair of definition.TauCeti.Huber.IsTateRing: a Huber ring with a topologically nilpotent unit.TauCeti.Huber.IsPseudoUniformizer: a topologically nilpotent unit ofA.
Main results #
TauCeti.Huber.PairOfDefinition.mem_idealImageandTauCeti.Huber.PairOfDefinition.coe_idealImage: membership in the image ofIⁿ.TauCeti.Huber.PairOfDefinition.span_image_eq_extendedIdealOfDefinition: generators ofIcontinue to generate its extension toA.TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero: the images ofIⁿare a neighbourhood basis of zero.TauCeti.Huber.PairOfDefinition.isOpen_closure_zero_of_eventually_constant_powers: if two adjacent powers ofIagree, the closure of zero in the Huber ring is open.TauCeti.Huber.PairOfDefinition.exists_pow_idealOfDefinition_mul_mem: someIⁿmultiplies a given element into a given open subring.TauCeti.Huber.IsAdic.comap: an adic topology transports along a ring equivalence that is an inducing map. This is what lets a ring of definition carry an ideal of definition that natively lives in a merely equivalent ring, which is whatTauCeti.Huber.PairOfDefinitionneeds.TauCeti.Huber.IsTateRing.of_continuous: a continuous homomorphism out of a Tate ring makes a Huber target Tate.TauCeti.Huber.IsHuberRing.toNonarchimedeanRing: a Huber ring is nonarchimedean.TauCeti.Huber.IsHuberRing.isCountablyGenerated_nhds_zero: its neighbourhoods of zero are countably generated. With the previous bullet these are exactly the two hypotheses Henkel's open mapping theorem asks of the underlying group, so both are instances.TauCeti.Huber.PairOfDefinition.exists_pow_mul_mem: a power of a topologically nilpotentscarries anyc : Ainto the ring of definition.IsTopologicallyNilpotent.exists_pow_mulandTauCeti.Huber.IsTateRing.exists_isTopologicallyNilpotent_pow_mul: a power of a topologically nilpotent element — a pseudouniformiser, in the Tate case — rescales any element ofAto a topologically nilpotent one. The multiplier is a unit in the Tate case, so the rescaled element is an associate of the original.TauCeti.Huber.IsHuberRing.quotient: a quotient of a Huber ring is a Huber ring.TauCeti.Huber.PairOfDefinition.isBounded_ringOfDefinition: a ring of definition is bounded, henceA₀ ≤ A°(TauCeti.Huber.PairOfDefinition.le_powerBoundedSubring). This is the boundedness half of Wedhorn Corollary 6.4.TauCeti.Huber.isOpen_powerBoundedSubring:A°is open in a Huber ring.TauCeti.Huber.IsPseudoUniformizer.hasBasis_nhds_zero: for a pseudouniformiserϖand a ring of definitionA₀of a Tate ring, the setsϖⁿ A₀are a neighbourhood basis of zero; the Tate-ring form isTauCeti.Huber.IsTateRing.exists_hasBasis_nhds_zero.TauCeti.Huber.IsHuberRing.of_discreteTopology: a discrete ring is Huber, the first of the roadmap's Layer-0 examples.TauCeti.Huber.exists_sum_eq_of_mem_span_mul: pure algebra, stated here because it is what finite generation of an ideal of definition is used through — an element of(G) * K, for a finite familyG, is aK-linear combination ofGitself.
Provenance #
PairOfDefinition and IsHuberRing follow the shape of sfingali's mathlib4#42312, which bundles
the same five fields; the name PairOfDefinition is used rather than that PR's RingOfDefinition
because the structure carries the pair (A₀, I), which is what Wedhorn calls a pair of
definition — a ring of definition is the A₀ alone. Everything else here is new. The selection
of results follows AdicSpaces/Suggested.lean in the roadmap.
Implementation notes #
The pair of definition is data, not a Prop-valued field of the ring: a Huber ring has many
pairs of definition and later layers choose between them. IsHuberRing is the Prop asserting
that the type of pairs is nonempty, in the shape used by mathlib4#42312.
References #
- Wedhorn, Adic Spaces, Proposition and Definition 6.1, Lemma 6.2 and Corollary 6.4.
- sfingali, feat(Topology): huber (f-adic) rings, mathlib4#42312.
An element of (G) * K is a K-linear combination of the finite family G.
This is Mathlib's Submodule.mem_ideal_smul_span_iff_exists_sum' in the form the Huber theory
uses it: a Finset.sum over G itself, with cofactors given by a function on all of R, rather
than a Finsupp on the subtype ↥G. It is what bounds, uniformly in k, the number of terms
needed to write an element of Iⁿ⁺ᵏ = Iⁿ * Iᵏ over generators of Iⁿ, both in Wedhorn Remark 6.8
(TauCeti.RingTheory.Huber.Completion) and in the identification of the neighbourhood subgroups
of A⟨X⟩_T with the powers of one finitely generated ideal
(TauCeti.RingTheory.Huber.WeightedRestrictedSeries.PairOfDefinition).
A pair of definition (A₀, I) for a topological ring A: an open subring A₀ together
with a finitely generated ideal I of A₀ whose adic topology is the subspace topology.
This is data rather than a proposition, because a Huber ring generally has many pairs of definition and the later theory chooses among them.
- ringOfDefinition : Subring A
The ring of definition
A₀. - isOpen_ringOfDefinition : IsOpen ↑self.ringOfDefinition
The ring of definition is open in
A. - idealOfDefinition : Ideal ↥self.ringOfDefinition
The ideal of definition
I ⊆ A₀. - fg_idealOfDefinition : self.idealOfDefinition.FG
The ideal of definition is finitely generated.
- isAdic_idealOfDefinition : IsAdic self.idealOfDefinition
The subspace topology on
A₀is theI-adic topology.
Instances For
A topological ring is a Huber ring — Wedhorn's f-adic ring — if it admits a pair of definition.
- nonempty_pairOfDefinition : Nonempty (PairOfDefinition A)
A Huber ring admits at least one pair of definition.
Instances
A pseudouniformiser of a topological ring is a topologically nilpotent unit.
This is the topological notion, unrelated to Mathlib's Valuation.IsUniformizer, which asks a
discretely valued ring's element to have valuation the generator of the value group. A Tate
ring need carry no valuation at all.
Equations
Instances For
Unfolding lemma for TauCeti.Huber.IsPseudoUniformizer.
A pseudouniformiser is a unit.
A pseudouniformiser is topologically nilpotent.
A continuous morphism of topological monoids with zero sends pseudouniformisers to pseudouniformisers.
A Tate ring is a Huber ring containing a pseudouniformiser, that is, a topologically nilpotent unit.
- exists_isPseudoUniformizer : ∃ (a : A), IsPseudoUniformizer a
A Tate ring contains a topologically nilpotent unit.
Instances
An adic topology transports along a ring equivalence that is also an inducing map.
This is what lets a ring of definition carry an ideal of definition: PairOfDefinition asks for
an Ideal A₀ whose adic topology is the subspace topology, while the ideal at hand usually lives
in a ring that is only equivalent to A₀.
A continuous homomorphism out of a Tate ring makes a Huber target Tate (Wedhorn,
Adic Spaces, Proposition 6.25): the image of a pseudouniformiser of A is a pseudouniformiser
of B.
The target must already be known to be Huber; this supplies only the pseudouniformiser.
The image in A of the n-th power of the ideal of definition. These sets are the
neighbourhood basis of zero of a Huber ring.
Equations
Instances For
As a set, Iⁿ's image in A is the image of Iⁿ ⊆ A₀ under the inclusion A₀ → A.
Membership in the image of Iⁿ.
The images of the powers of the ideal of definition are nested.
Iⁿ ⊆ A lies in the ring of definition.
Iⁿ ⊆ A absorbs multiplication by an element of the ring of definition.
The images of the powers of the ideal of definition multiply: Iᵃ · Iᵇ ⊆ Iᵃ⁺ᵇ.
One coefficient, decomposed. An element of Iⁿ⁺¹ ⊆ A is a combination of a finite
generating set G of I with cofactors in Iⁿ.
The ideal I · A of A generated by the ideal of definition I ⊆ A₀. This is core data of
a pair of definition; TauCeti/RingTheory/Huber/OpenIdeal.lean characterises the open ideals of
A in terms of its powers.
Equations
Instances For
Unfolding lemma for TauCeti.Huber.PairOfDefinition.extendedIdealOfDefinition.
Membership in I · A is membership in the ideal spanned by the image of I.
There is no simpler characterisation: the image of I under A₀ → A is an additive subgroup but
not in general an ideal of A, so x ∈ I · A is strictly weaker than ∃ y ∈ I, ↑y = x. For
A₀ = ℤ_[p] ⊆ A = ℚ_[p] and I = p • ℤ_[p] the image is p • ℤ_[p] while the ideal it
generates is all of ℚ_[p].
The extended ideal I · A is finitely generated, because I is.
A finite generating set of the ideal of definition, mapped into A, generates the extended
ideal of definition.
Each Iⁿ is open in A.
Wedhorn Proposition and Definition 6.1: the images in A of the powers of the ideal of
definition are a neighbourhood basis of zero.
If two adjacent powers of an ideal of definition agree, then the closure of zero in the ambient Huber ring is open. The stable image of that power is both a basic open neighbourhood and the intersection of all basic neighbourhoods.
A power of the ideal of definition multiplies any element into any open subring.
Multiplication by x is continuous, so the preimage of B is a neighbourhood of 0, and the
images of the powers of I are a neighbourhood basis there
(TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero).
A unit multiple of one level of the filtration contains a deeper level: for a unit u of
A and any N, some Iᴺ' lands inside u · Iᴺ.
This is what lets a denominator be rescaled by a unit: the standing hypotheses of a presentation are stated at some level of the filtration, and rescaling moves that level by a unit.
An element of the ideal of definition is topologically nilpotent. Its powers lie in the
successive Iⁿ, whose images are a neighbourhood basis of zero
(TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero), so they converge to 0 in A.
This is the property Wedhorn uses throughout §7.2: it is what forces a continuous valuation to
have cofinal values on I, and hence v a < 1 there (Theorem 7.10).
An element of the image of Iⁿ is topologically nilpotent, for n ≠ 0. Unpacking the
membership gives an element of Iⁿ ⊆ I, so isTopologicallyNilpotent_of_mem_idealOfDefinition
applies. This is the form consumers meet, idealImage being what
TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero is stated with.
n ≠ 0 is needed, not incidental: I ^ 0 = ⊤, so idealImage 0 is the image of the whole ring
of definition and its elements are not topologically nilpotent in general.
A ring admitting a pair of definition is nonarchimedean.
Wedhorn Corollary 6.4: a ring of definition is bounded.
A ring of definition consists of power-bounded elements: A₀ ≤ A°. The nonarchimedean
hypothesis is only needed to state it, since P itself supplies one.
Some power of a topologically nilpotent s carries any c : A into the ring of
definition. The ring of definition is open and sⁿ c → 0, so sⁿ c is eventually inside it.
This is the arbitrary-c generalisation of
TauCeti.Huber.IsPseudoUniformizer.eventually_pow_mem_ringOfDefinition, which is the case
c = 1; it also asks only for topological nilpotence rather than for a pseudouniformiser.
A topologically nilpotent element rescales any element to a topologically nilpotent one.
In a Huber ring, for topologically nilpotent ϖ and any s, some ϖ ^ i * s is topologically
nilpotent.
Use it to make a hypothesis of topological nilpotence available for an element that need not have
it: replace s by ϖ ^ i * s, which differs from it by a factor drawn from the topology rather
than an arbitrary one. When ϖ is a pseudouniformiser that factor is a unit, so the replacement
is an associate of s; TauCeti.Huber.IsTateRing.exists_isTopologicallyNilpotent_pow_mul is the
form that records this.
A pseudouniformiser rescales any element to a topologically nilpotent one. For s : A
in a Tate ring there are a pseudouniformiser ϖ and an exponent i with ϖ ^ i * s
topologically nilpotent.
ϖ ^ i is a unit, so s and ϖ ^ i * s are associated. Any construction depending on an
element only up to associates is therefore unchanged by the rescaling, while hypotheses asking
topological nilpotence of that element become available; IsLocalization.Away is the case that
matters, by IsLocalization.Away.of_associated.
Rescaling a denominator alone is not such a construction: the fractions t / s are not the
fractions t / (ϖ ^ i * s), so a rational localisation A⟨T/s⟩ is preserved only if the
numerators are rescaled by the same unit.
A caller who already holds a topologically nilpotent element should use
IsTopologicallyNilpotent.exists_pow_mul, which neither asks for a Tate ring nor chooses the
multiplier.
Quotients of Huber rings, with the quotient topology, are Huber rings.
The pair of definition of a discrete ring: the whole ring, with the zero ideal.
Equations
Instances For
A discrete ring is Huber, with (A, 0) as a pair of definition. This is the first of the
roadmap's Layer-0 examples, and the witness that IsHuberRing is not vacuous.
Every Huber ring is nonarchimedean. This is what makes A° a subring.
The neighbourhoods of zero in a Huber ring are countably generated. The images of the
powers of an ideal of definition are a basis of 𝓝 0 indexed by ℕ
(TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero), and a basis indexed by a countable type
generates a countably generated filter.
This is one of the two hypotheses Henkel's open mapping theorem asks of a topological group, the
other being TauCeti.Huber.IsHuberRing.toNonarchimedeanRing above: nonarchimedean makes the open
subgroups a basis at zero, and countable generation extracts an antitone sequence from that
basis (NonarchimedeanAddGroup.exists_antitone_basis_openAddSubgroup). Being an instance is the
point — it is what lets a Huber ring be handed to that theorem without the caller discharging
anything.
Wedhorn Corollary 6.4: the power-bounded subring of a Huber ring is open.
Wedhorn: sufficiently high powers of a pseudouniformiser lie in a given ring of definition.
The scaled copy ϖⁿ A₀ of a ring of definition is a neighbourhood of zero.
Only continuity of multiplication by a constant is needed: multiplication by the unit ϖⁿ is a
homeomorphism, so it carries the neighbourhood A₀ of zero to a neighbourhood of zero.
Wedhorn: in a Tate ring the sets ϖⁿ A₀ are a neighbourhood basis of zero, for any
pseudouniformiser ϖ and any ring of definition A₀.
Cofinality is the boundedness of A₀ (PairOfDefinition.isBounded_ringOfDefinition) together
with ϖⁿ → 0; that each ϖⁿ A₀ is itself a neighbourhood is
smul_ringOfDefinition_mem_nhds_zero.
In a Tate ring one may choose a pseudouniformiser ϖ and a ring of definition A₀ whose
scaled copies ϖⁿ A₀ are a neighbourhood basis of zero.