The localisation topology: construction #
We construct the non-archimedean ring topology on a localisation S of A away from an element
s, following Proposition and Definition 5.51, §5.6, of Wedhorn's Adic Spaces, and show that
Aₛ under it is a Huber ring. The carrier is an arbitrary IsLocalization.Away s S rather than
the concrete Localization.Away s, so a consumer holding A[1/s] in another presentation can use
the topology directly.
The material about maps out of Aₛ is in the sibling modules: the continuity criterion and the
universal property in LocalizationTopology.UniversalProperty, the completion A⟨T/s⟩ in
LocalizationTopology.Completion.
Main definitions #
locSubring P T s S: the candidate ring of definitionD = A₀[t₁/s, …, tₙ/s].HasDenominatorPower P T s S: the standing hypothesis the construction runs under — some power ofIhas all of its fractionsb/salready inD.locIdeal P T s S: the candidate ideal of definitionJ = I · DinD.locIdealImage P T s S n: then-th neighborhoodimage(Jⁿ)inAₛ.locBasisandlocTopology: the neighbourhoods form aRingSubgroupsBasis, hence a ring topology onAₛ.localization P T s S: the pair of definitionAₛcarries under that topology.
Main results #
locSubring_eq_of_coe_eq_image_mul_left: rescaling numerators and denominator by one common factor leavesDunchanged — the first step of a change of presentation.locIdealImage_congrandlocTopology_congr: presentations sharing a ring of definition share the whole neighbourhood filtration, and so the topology — the step that lets a rescaled presentation stand in for the original.hasBasis_nhds_zero_locTopology,isTopologicalRing_locTopologyandnonarchimedeanRing_locTopology: the contract oflocTopology, to be used in place of unfolding the construction.TauCeti.Huber.HasDenominatorPower.mono: the standing hypothesis is monotone in the numerators.TauCeti.Huber.HasDenominatorPower.of_coe_eq_image_mul_left: it also survives rescaling the whole presentation by a unit — the second step of a change of presentation.hasDenominatorPower_of_idealOfDefinition_le_span: numerators containing a subset ofA₀whose span containsIsupply the standing denominator-power hypothesis for every denominator.hasDenominatorPower_of_isOpen_span: a finite numerator set spanning an open ideal supplies the standing denominator-power hypothesis for every denominator.isHuberRing_locTopology:AₛunderlocTopologyis a Huber ring.locIdeal_eq_span_singleton: when the ideal of definition is principal onπ, so isJ, on the image ofπ—Jis by construction the image ideal.mem_locIdealImage_add_iff: consequently the neighbourhood filtration isπ-adic — leveln + kis exactly theπᵏ-multiples of leveln. This sharpenslocIdealImage_antitonefrom "decreasing" to a uniform rate.locIdealImage_le_of_image_subsetandisOpen_map_algebraMap_locTopology: an ideal ofAₛcontaining the image ofIⁿcontains the wholen-th neighbourhood, so the ideal generated by the image of an open ideal ofAis open.awayLift_mem_locSubringandawayLift_mem_locIdealImage: passing to a multiplew = u * rof the denominator carriesDand its neighbourhood filtration forward, the latter at the same index — which is what makes the comparison map of two nested presentations continuous.isBounded_image_algebraMap_of_isBoundedandisPowerBounded_algebraMap_of_isPowerBounded: bounded sets have bounded image, so power-orbits transfer and each power-bounded element stays power-bounded. ThelocSubringroute reaches only a ring of definition, whose boundedness it uses; a ring of integral elementsA⁺need not be bounded at all, so it is the elementwise statement — not a bounded-set statement aboutA⁺— that carries over.
Provenance #
This is a port of AINTLIB's LocalizationTopology.lean, at commit d9f2fbbb.
locIdealImage_mul_algebraMap_subset, isBounded_image_algebraMap_of_isBounded and
isPowerBounded_algebraMap_of_isPowerBounded are later additions, following the skeleton at
LocalizationTopology.lean:690-753 of commit 37bbdaeb9. awayLift_mem_locSubring,
awayLift_mem_locIdealImage, divBy_mul_mem_locSubring, hasDenominatorPower_mul,
locIdeal_eq_span_singleton and mem_locIdealImage_add_iff are also later additions, and have
no AINTLIB analogue at all — commit 37bbdaeb9 carries no transfer of D-membership or of its
neighbourhood filtration along a comparison map, no combination of the denominator hypothesis for
a product denominator, and no π-adic characterisation of the filtration: its locNhd API states
no principal-ideal-of-definition hypothesis at all. They are new work for the
nested-presentation comparison of Wedhorn §8.2. locSubring_insert_eq_of_divBy_mem and
HasDenominatorPower.exists_unit_divBy_mem_locSubring are later additions with no AINTLIB
analogue either: commit 37bbdaeb9 has no lemma adjoining a numerator whose fraction already lies
in D, and none producing a unit u with u/s in D over a Tate ring. They are new work for the
structure-map case of Wedhorn's Proposition 8.30,
TauCeti.Huber.PairOfDefinition.flat_toCompletionLoc. locIdealImage_le_of_image_subset and
isOpen_map_algebraMap_locTopology are later additions with no AINTLIB analogue either: commit
37bbdaeb9 proves no openness statement about an ideal of Aₛ. They record that admissibility of
a numerator ideal survives the structure map A → Aₛ, as required by the forward direction of
Wedhorn Proposition 8.2(2). The main changes
are: adapted PairOfDefinition field names to TauCeti conventions (A₀→ringOfDefinition,
I→ideal, etc.); uses characteristic lemmas instead of destructuring definitions; removed
unused hypotheses to satisfy #lint checks; stated over an arbitrary localisation S away from
s, rather than the concrete model Localization.Away s the source uses.
References #
- T. Wedhorn, Adic Spaces, Proposition and Definition 5.51, §5.6, and Proposition 8.2(2).
- C. Birkbeck, AINTLIB, branch
dev/adic-spaces, commitd9f2fbbb,projects/AdicSpaces/Adic spaces/LocalizationTopology.lean
The candidate ring of definition D #
Everything below takes a PairOfDefinition as its first explicit argument, so it lives in
that namespace and reads P.locSubring T s S, matching TauCeti/RingTheory/Huber/Basic.lean.
The candidate ring of definition D = A₀[t₁/s, …, tₙ/s] of S.
Equations
- P.locSubring T s S = (Algebra.adjoin (↥P.ringOfDefinition) (Set.range fun (t : ↥T) => TauCeti.Localization.divBy (↑t) s)).toSubring
Instances For
D is the A₀-subalgebra generated by the fractions, as a subalgebra rather than as a
ring closure. The body of TauCeti.Huber.locSubring is not exported, so this is how a consumer
reaches Mathlib's Algebra.adjoin API for it — in particular
Algebra.adjoin_range_eq_range_aeval, which presents every element of D as the value of a
polynomial over A₀ at the fractions.
TauCeti.Huber.locSubring_def is the companion in the Subring.closure shape, which is what
arguments about ring generation want; this one is what arguments about polynomials want.
D is the subring generated by the image of A₀ together with the fractions tᵢ/s. The body
is not exported, so this is how a consumer reaches the generators.
The image of A₀ under algebraMap is contained in D.
Each element t/s (for t ∈ T) belongs to D.
An element of A₀ maps into D under algebraMap.
The universal property of D: a subring contains D exactly when it contains the image
of A₀ and every distinguished fraction. The body of locSubring is not exported, so this is the
elimination principle a consumer has.
Rescaling a presentation leaves D alone: if the numerators T' are exactly the
u-multiples of T, in the sense that (T' : Set A) = (u * ·) '' T, and the denominator is
rescaled by the same u, then (T', u * s) and (T, s) generate the same D inside S. Both
away-localisation structures are assumed: S is a localisation away from s and away from u * s
at once, which for a unit u comes free from IsLocalization.Away.iff_of_associated.
No unit hypothesis on u is needed, and the rescaled numerators are taken as a Finset with a
set-level equation rather than as T.image (u * ·), which would need DecidableEq A.
With no fractions adjoined, D is just the image of A₀.
D grows with the set of numerators.
The insertion formula for D: adjoining one more fraction gives the previous D with
that fraction adjoined as an algebra over it. The recursive step for locSubring on a Finset,
with locSubring_empty as its base.
The Algebra.adjoin form matches the shape of locSubring itself, and says concretely that an
element of locSubring P (insert t U) s S is a polynomial in t/s with coefficients in the
smaller subring.
Not a simp lemma: locSubring P U s S occurs on the right as a type index, so simp rewrites the
outermost insert and then stalls rather than reaching a normal form. The Subring.closure form
this replaced did iterate, which is why the attribute was there.
Adjoining a numerator whose fraction already lies in D leaves D alone: if t/s is in
locSubring P T s S, then insert t T gives the same D as T, so a presentation can take on an
extra numerator — s itself, as s/s = 1, or 1 once 1/s ∈ D — without changing D. This is
the degenerate case of locSubring_insert, where the adjoined fraction adds nothing.
The standing hypothesis #
The standing hypothesis of Wedhorn's construction: some power of the ideal of definition
I has all of its fractions b/s already inside D = A₀[t₁/s, …, tₙ/s]. It is exactly what
makes the locIdealImage into a basis of neighbourhoods of zero for a ring topology, so every
declaration about locTopology below carries it.
Equations
- P.HasDenominatorPower T s S = ∃ (N : ℕ), ∀ b ∈ P.idealOfDefinition ^ N, TauCeti.Localization.divBy (↑b) s ∈ P.locSubring T s S
Instances For
HasDenominatorPower unfolds to the existential it names. The body is not exported, so this
is how a consumer builds one by hand or takes one apart.
The standing hypothesis grows with the numerators. Adjoining numerators enlarges D, so a
denominator power that works for T works for any larger U: the fractions b/s it puts in
locSubring P T s S are still in locSubring P U s S.
The standing hypothesis survives a change of presentation by a unit. Rescaling both the
numerators and the denominator by a unit u carries HasDenominatorPower from (T, s) to
(u · T, u · s).
Of the data a presentation carries, this is the part whose invariance under rescaling is not immediate, so it is what a rescaled presentation needs in order to stand in for the original.
The standing hypothesis puts a unit fraction in D: over a Tate ring, some unit u has
u/s in D = A₀[t₁/s, …, tₙ/s].
Typically used to make 1 a numerator: after rescaling (T, s) by u⁻¹
(locSubring_eq_of_coe_eq_image_mul_left), u/s is the fraction 1/(u⁻¹ s), so 1 can be
adjoined to the numerators without changing D.
The Tate hypothesis is needed: over ℤ_[p], with T = ∅ and s = p, the standing hypothesis
holds, but D is the image of ℤ_[p] in ℚ_[p], which contains no u/p with u a unit.
Introduction: if some power of I lies in the ideal generated by s inside A₀, the
standing hypothesis holds. Indeed b = c · s makes b/s = c, which lies in A₀ ⊆ D. This is
the criterion in the standard case, where s itself is a topologically nilpotent element of
A₀ generating a power of I.
Introduction from a generating set of I: if the numerators T contain a set G ⊆ A₀
whose span is all of I, the standing hypothesis holds for every denominator, with N = 1.
Every element of I is an A₀-linear combination of the elements of G, and division by the
fixed denominator is linear in the numerator, so b/s is an A₀-combination of the fractions
g/s, all of which lie in D.
An open numerator ideal supplies the standing denominator-power hypothesis. If the ideal
spanned by T is open, a sufficiently small basic neighbourhood Iⁿ consists of T-linear
combinations whose coefficients lie in the ring of definition. Dividing such a combination by
s therefore puts it in A₀[T/s].
This is the bridge from the admissibility condition on a rational subset, stated as openness of
T · A, to the standing hypothesis needed to construct its topological coordinate ring.
Passing to a denominator that is a multiple #
A localisation away from u maps to one away from a multiple w = u * r, and under that map D
lands inside the finer D as soon as each t * r, for t ∈ U, is one of the finer numerators.
What transfers is exactly that: membership of the rescaled fraction, not the hypothesis
HasDenominatorPower itself. HasDenominatorPower P U u V bounds a single power of the ideal of
definition against u, and nothing here carries such a bound from u to w. For a product
denominator the two factors' hypotheses do combine — that is hasDenominatorPower_mul, and it needs
both, precisely because neither alone transfers. That combination is what makes the intersection of
two rational subsets a legitimate presentation, which is how nested presentations get compared
(Wedhorn §8.2).
D maps into the finer D. With w = u * r, the comparison map Aᵤ → A_w carries
locSubring P U u V into locSubring P Tw w W, provided each t * r for t ∈ U is a numerator of
the target. Both generating families land where they must: A₀ by algebraMap_mem_locSubring, and
t/u, which awayLift_divBy identifies with the distinguished fraction (t * r)/w.
The rescaled fraction lands in the finer D. With w = u * r, if a / u lies in
locSubring P U u V then (a * r) / w lies in locSubring P Tw w W. This is the fraction-level
form of awayLift_mem_locSubring, and it is the one consumers want: it spares them rewriting the
comparison map away at every use.
The standing hypothesis for a product denominator. If (T, s) and (T', s') both satisfy
HasDenominatorPower, and the numerator set T'' contains every t * s' for t ∈ T and every
t' * s for t' ∈ T', then (T'', s * s') satisfies it too.
The exponent adds: for b ∈ I ^ (N + N') write b as a sum of products x * y with x ∈ I ^ N
and y ∈ I ^ N', and split (x * y)/(s * s') as (x * s')/(s * s') · (y * s)/(s * s')
(divBy_mul_divBy_of_eq_mul). Each factor is the image of a fraction that the corresponding
hypothesis already places in the coarser D, so awayLift_mem_locSubring puts it in the finer one,
which is a subring and therefore closed under the products and sums involved.
insert s T * insert s' T' — the numerator set rationalSubset_inter produces for an intersection
of rational subsets — satisfies both membership conditions, which is the intended instance.
The candidate ideal of definition J #
The ring homomorphism A₀ →+* D induced by algebraMap.
Equations
- P.toLocSubring T s S = ((algebraMap A S).comp P.ringOfDefinition.subtype).codRestrict (P.locSubring T s S) ⋯
Instances For
toLocSubring is algebraMap with its codomain cut down to D, so its values coerce back to
algebraMap.
The candidate ideal of definition J = I · D in D.
Equations
- P.locIdeal T s S = Ideal.map (P.toLocSubring T s S) P.idealOfDefinition
Instances For
J is the ideal of D generated by the image of I.
The localised ideal is principal too. When I = (π), the ideal J = I · D is principal on
the image of π, because J is by construction the ideal of D generated by the image of I.
This is what makes the neighbourhood filtration π-adic: every statement about Jⁿ below reduces
to a divisibility in a principal ideal, with no induction over generators.
Jⁿ is the image of Iⁿ. The body of locIdeal is not exported, so this is how a consumer
reaches the powers that index the neighbourhood basis.
Jⁿ is spanned by the image of Iⁿ: the form the span inductions below run on.
The image of Iⁿ under A₀ →+* D lands in Jⁿ.
J is finitely generated, because I is and Ideal.map preserves that. This is one of
the two conditions (D, J) needs to be a TauCeti.Huber.PairOfDefinition; the other, that the
subspace topology on D is J-adic, is isAdic_locIdeal below.
The neighborhood basis #
The n-th neighborhood of 0 in S.
Equations
- P.locIdealImage T s S n = AddSubgroup.map (P.locSubring T s S).subtype.toAddMonoidHom (Submodule.toAddSubgroup (P.locIdeal T s S ^ n))
Instances For
An element of Aₛ lies in the n-th neighbourhood exactly when it is the image of an element
of Jⁿ.
The image of Iⁿ in Aₛ lands in the n-th basic neighbourhood: this is the introduction
rule for locIdealImage, and what continuity of the structure map is read off.
The zeroth neighbourhood is D itself, because J⁰ = ⊤.
The neighborhoods are antitone.
The preimage of locIdealImage n under the subtype embedding equals locIdeal^n.
The basis is graded: the i-th and j-th neighbourhoods multiply into the (i + j)-th,
because Jⁱ · Jʲ ⊆ Jⁱ⁺ʲ in D. The two special cases the subgroup basis needs follow.
Products of the n-th neighbourhood land in the n-th neighbourhood: this is the
multiplicative half of the subgroup basis, the diagonal case of locIdealImage_mul_subset_add.
Jⁿ's image absorbs multiplication by D, because D is the zeroth neighbourhood and the
basis is graded.
The neighbourhood filtration is π-adic when the ideal of definition is principal on π:
level n + k consists of exactly the πᵏ-multiples of level n.
locIdealImage_antitone records only that the filtration decreases. This says by how much: the
k levels between n + k and n are spent on πᵏ and nothing else, so a member of n + k
divides by πᵏ back into n, and every such multiple is already that deep. The depth is
therefore uniform in the element, which an inclusion alone does not give.
Both directions are needed in practice: the forward one to divide, the reverse to certify that the quotient's depth is recovered when it is multiplied back.
The neighbourhood filtration transfers to a finer denominator. With w = u * r, the
comparison map Aᵤ → A_w carries locIdealImage P U u V n into locIdealImage P Tw w W n, at
the same index n — passing to a multiple of the denominator costs no depth.
This is the filtration companion of awayLift_mem_locSubring, which carries D itself. The two
together are what a comparison of nested presentations needs. Since both topologies have these
filtrations as a neighbourhood basis of zero, the same-index inclusion implies continuity of
the comparison map; it is strictly stronger than continuity, which would allow the index to
grow.
Left multiplication is continuous for the localization topology: multiplication by a
fixed x pulls some neighbourhood locIdealImage j back inside locIdealImage i.
Wedhorn's topological localisation: the topology on Aₛ whose neighbourhoods of zero are the
images of the powers of J = I · D, the candidate ideal of definition of
D = A₀[t₁/s, …, tₙ/s].
Equations
- P.locTopology T s S hden = ⋯.topology
Instances For
The contract of locTopology: the locIdealImage n are a basis of neighbourhoods of zero.
Consumers should use this rather than unfolding the definition.
locTopology is a ring topology.
A change of presentation leaves the topology alone #
Presentations with the same ring of definition have the same neighbourhood filtration.
locIdealImage depends on (T, s) only through locSubring P T s S, so two presentations
sharing that subring give the same subgroup of Aₛ at every level.
A change of presentation with the same ring of definition leaves locTopology alone.
This is what lets a presentation be replaced by another one — for instance a rescaled one — while
the topology on Aₛ, and hence its completion, stays the same object.
locTopology is nonarchimedean: Aₛ inherits a basis of open additive subgroups at zero.
Every basic neighbourhood is open: it is a subgroup that is a neighbourhood of zero.
D is open: it is the zeroth basic neighbourhood of zero. With isBounded_locSubring,
fg_locIdeal and isAdic_locIdeal, this completes what
TauCeti.Huber.PairOfDefinition asks of (D, J).
D is bounded: each Jⁿ already absorbs it.
Every element of D is power-bounded: D is bounded, and IsBounded.isPowerBounded_of_mem
turns that into power-boundedness of each of its elements.
The image of a bounded subset of A is bounded in Aₛ.
A power-bounded element of A stays power-bounded in Aₛ.
The distinguished fractions t/s are power-bounded: they lie in D, and every element of
D is.
The structure map A → Aₛ is continuous for the localisation topology: the image of Iⁿ
already lands in the n-th basic neighbourhood.
An ideal of Aₛ swallowing the image of Iⁿ swallows the whole n-th neighbourhood.
This supplies the neighbourhood containment used to prove that mapping an open ideal along the
rational-localisation structure map produces an open ideal.
The powers of J are a neighbourhood basis of zero in D. The images image(Jⁿ) are one
in Aₛ by TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero_locTopology, and D carries the
subspace topology, so it suffices that pulling those images back along the inclusion returns the
Jⁿ themselves — which is
TauCeti.Huber.PairOfDefinition.locIdealImage_preimage_eq_locIdeal_pow.
The subspace topology on D is the J-adic topology. This is the last condition
TauCeti.Huber.PairOfDefinition asks of the candidate pair (D, J); fg_locIdeal supplies the
other.
IsAdic is an equality of topologies, and Ideal.isAdic_iff turns it into the two conditions the
basis already gives: each Jⁿ is open, and every neighbourhood of zero contains one.
The localisation is a Huber ring #
The pair of definition of Aₛ under locTopology — Wedhorn's A(T/s) of 5.51, written
Aₛ throughout this file: the subring D together with the ideal J = I · D.
TauCeti.Huber.PairOfDefinition has two data fields and three proof fields, and every one of them
is already established above. The data are locSubring and locIdeal; the three proofs are
isOpen_locSubring, fg_locIdeal and isAdic_locIdeal. Nothing new is proved here — this is the
value that packages them for isHuberRing_locTopology.
The topology is not an instance on S, so it is introduced in the statement; a consumer supplies
it the same way, or works under isHuberRing_locTopology instead.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The image of an open ideal of A generates an open ideal of Aₛ. This is the openness
assertion needed in the forward direction of Wedhorn Proposition 8.2(2) and is the companion of
continuity of the structure map
(TauCeti.Huber.PairOfDefinition.continuous_algebraMap_locTopology): continuity pulls an open
set back to A, while this pushes an open ideal forward.
The ring of definition of localization is D. The body of localization is not exposed, so
this is how a consumer recovers it — the same contract completion_ringOfDefinition provides for
the completion. Unlike that one, the statement has to introduce the topology, because
locTopology is not an instance and localization's own type depends on it.
Membership in the ideal of definition of localization is membership in J. Stated as a
membership rather than an equation because idealOfDefinition's type depends on
ringOfDefinition, exactly as mem_completion_idealOfDefinition is.
Wedhorn's topological localisation is a Huber ring. Under the standing hypothesis, Aₛ
carrying locTopology admits a pair of definition, namely (D, J).
This is what the whole file is for. Being Huber is exactly the existence of some pair of
definition, so the content is the three facts assembled in localization: D is open, J is
finitely generated, and the subspace topology on D is the J-adic one.
Both the topology and its ring structure are introduced in the statement, because locTopology is
deliberately not registered as an instance — Aₛ is an arbitrary localisation and carries no
topology of its own.