Rational localisation of a quotient ring #
Let J be an ideal of a ring A with a pair of definition P, and write q : A → A ⧸ J for
the quotient map, so that A ⧸ J carries the quotient pair of definition P.quotient J. A
presentation (T, s) of a rational localisation of A induces the presentation (q(T), q(s))
of A ⧸ J, and localising q gives the map
A[1/s] → (A ⧸ J)[1/q(s)],
which is IsLocalization.Away.map. This file shows that the rational localisation of A ⧸ J is
the quotient of that of A:
- before completion, the map is an open quotient map for the localisation topologies: it carries
the ring of definition
A₀[T/s]onto(A ⧸ J)₀[q(T)/q(s)]and each basic neighbourhood of zero onto the corresponding one; - after completion, the induced map
A⟨T/s⟩ → (A ⧸ J)⟨q(T)/q(s)⟩is again surjective and open, and its kernel is the closure of the ideal generated by the image ofJ.
So (A ⧸ J)⟨q(T)/q(s)⟩ is A⟨T/s⟩ modulo the closure of J · A⟨T/s⟩, as a topological ring.
The same holds for the plus rings. Give A ⧸ J the plus ring (A ⧸ J)⁺ of the quotient Huber
pair, the integral closure of q(A⁺). Then the completed map is a quotient mapping of Huber pairs
(A⟨T/s⟩, A_U⁺) → ((A ⧸ J)⟨q(T)/q(s)⟩, (A ⧸ J)_U⁺): the plus ring of the target is the
integral closure of the image of A_U⁺. Together, these identify the rational localisation of
the quotient pair with the quotient Huber pair of (A⟨T/s⟩, A_U⁺) by the closed ideal
closure(J · A⟨T/s⟩). This is the algebraic input for describing the restriction of the closed
subspace Spa(A ⧸ J, (A ⧸ J)⁺) of Wedhorn's Proposition 7.38 to a rational subset R(T/s); that
geometric statement is not proved here.
The numerators over A ⧸ J are a finset T' with underlying set q '' T, so that no decidable
equality on A ⧸ J enters the statements. The standing hypothesis HasDenominatorPower for
(T', q(s)) is derived from the one for (T, s), not assumed.
Main definitions #
TauCeti.Huber.PairOfDefinition.completionLocQuotientHom: the mapA⟨T/s⟩ →+* (A ⧸ J)⟨q(T)/q(s)⟩induced by the quotient map.TauCeti.Huber.PairOfDefinition.completionLocQuotientPairHom: the same map as a morphism from the rational localisation pair of(A, A⁺)to that of the quotient pair(A ⧸ J, (A ⧸ J)⁺).
Main results #
TauCeti.Huber.PairOfDefinition.locSubring_map_awayMap_quotientMkandTauCeti.Huber.PairOfDefinition.locIdealImage_map_awayMap_quotientMk: the localised quotient map carries the ring of definition and the basic neighbourhoods of zero ofA[1/s]onto those of(A ⧸ J)[1/q(s)].TauCeti.Huber.PairOfDefinition.hasDenominatorPower_quotient: the standing hypothesis passes to the quotient.TauCeti.Huber.PairOfDefinition.isOpenQuotientMap_awayMap_quotientMk: the localised quotient map is an open quotient map for the localisation topologies.TauCeti.Huber.PairOfDefinition.completionLocQuotientHom_comp_toCompletionLoc: the completed map is compatible with the structure maps, andTauCeti.Huber.PairOfDefinition.eq_completionLocQuotientHomsays that this, with continuity, determines it.TauCeti.Huber.PairOfDefinition.isOpenQuotientMap_completionLocQuotientHom: the completed map is an open quotient map.TauCeti.Huber.PairOfDefinition.ker_completionLocQuotientHom: its kernel is the closure of the ideal ofA⟨T/s⟩generated by the image ofJ.TauCeti.Huber.PairOfDefinition.completionLocQuotientPairHom_comp_toCompletionLocHom: the morphism of pairs is compatible with the structure morphisms.TauCeti.Huber.PairOfDefinition.isQuotientMapping_completionLocQuotientPairHom: it is a quotient mapping of Huber pairs, so(A ⧸ J)_U⁺is the integral closure of the image ofA_U⁺.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition and Definition 5.51 for the rational localisation, §8.1 for its plus ring, Definition 7.22 and Proposition 7.38 for the quotient Huber pair, and Definition 8.42 for quotient mappings.
- N. Bourbaki, General Topology, Chapter IX, §3.1, Proposition 4, for the completion of an open quotient.
The localised quotient map, before completion #
The localised quotient map carries the ring of definition onto the ring of definition:
the image of A₀[T/s] in (A ⧸ J)[1/q(s)] is (A ⧸ J)₀[q(T)/q(s)], where (A ⧸ J)₀ = q(A₀)
is the ring of definition of the quotient pair P.quotient J.
The localised quotient map carries the basic neighbourhoods of zero onto the basic
neighbourhoods of zero: the image of the n-th neighbourhood locIdealImage of A[1/s] is
the n-th neighbourhood of (A ⧸ J)[1/q(s)].
The standing hypothesis passes to the quotient: if some power of I has all its fractions
b/s in A₀[T/s], the same power of the ideal of definition of P.quotient J has all its
fractions in (A ⧸ J)₀[q(T)/q(s)].
The localised quotient map is an open quotient map A[1/s] → (A ⧸ J)[1/q(s)] for the
localisation topologies: it is surjective, continuous and open.
The completed map #
The map A⟨T/s⟩ → (A ⧸ J)⟨q(T)/q(s)⟩ induced by the quotient map: the completion of the
localised quotient map A[1/s] → (A ⧸ J)[1/q(s)], which is continuous by
isOpenQuotientMap_awayMap_quotientMk.
Instances For
On the image of A[1/s], the completed map is the localised quotient map.
The completed map is continuous.
The completed map is compatible with the structure maps: A → A⟨T/s⟩ followed by it is
A → A ⧸ J → (A ⧸ J)⟨q(T)/q(s)⟩.
The completed map is determined by continuity and compatibility with the structure maps:
a continuous ring homomorphism A⟨T/s⟩ → (A ⧸ J)⟨q(T)/q(s)⟩ carrying the structure map of A to
that of A ⧸ J after the quotient map is completionLocQuotientHom.
The completed map A⟨T/s⟩ → (A ⧸ J)⟨q(T)/q(s)⟩ is an open quotient map: it is
surjective, continuous and open.
The kernel of A⟨T/s⟩ → (A ⧸ J)⟨q(T)/q(s)⟩ is the closure of J · A⟨T/s⟩, the closure of
the ideal generated by the image of J under the structure map. With
isOpenQuotientMap_completionLocQuotientHom, this identifies (A ⧸ J)⟨q(T)/q(s)⟩ with the
quotient of A⟨T/s⟩ by that closed ideal.
The plus rings #
The completed quotient map as a morphism of Huber pairs #
The completed quotient map as a morphism of Huber pairs
(A⟨T/s⟩, A_U⁺) → ((A ⧸ J)⟨q(T)/q(s)⟩, (A ⧸ J)_U⁺), from the rational localisation of
(A, A⁺) to that of the quotient pair (A ⧸ J, (A ⧸ J)⁺). Its underlying ring homomorphism is
completionLocQuotientHom; isQuotientMapping_completionLocQuotientPairHom shows that it is a
quotient mapping of Huber pairs.
Instances For
The underlying ring homomorphism of completionLocQuotientPairHom is
completionLocQuotientHom.
completionLocQuotientPairHom is compatible with the structure morphisms: the structure
morphism (A, A⁺) → (A⟨T/s⟩, A_U⁺) followed by it is the quotient morphism
(A, A⁺) → (A ⧸ J, (A ⧸ J)⁺) followed by the structure morphism of the quotient pair.
The plus ring of the rational localisation of a quotient pair (Wedhorn, Definition 7.22
and §8.1): completionLocQuotientPairHom is a quotient mapping of Huber pairs. Its underlying map
A⟨T/s⟩ → (A ⧸ J)⟨q(T)/q(s)⟩ is an open quotient map, and the plus ring (A ⧸ J)_U⁺ of the
target is the integral closure of the image of A_U⁺. With ker_completionLocQuotientHom, this
identifies ((A ⧸ J)⟨q(T)/q(s)⟩, (A ⧸ J)_U⁺) with the quotient Huber pair of
(A⟨T/s⟩, A_U⁺) by the closure of J · A⟨T/s⟩, through
TauCeti.Huber.Pair.Hom.IsQuotientMapping.quotientKerInverse.