A rational localisation of A⟨T/s⟩ is a rational localisation of A #
Let B = A⟨T/s⟩, with structure map ρ : A → B, and let (T'', s'') refine (T, s):
s'' = s * r and every t * r, for t ∈ T, lies in T''. Wedhorn's Remark 8.4 identifies
A⟨T''/s''⟩ with the rational localisation B⟨ρ(T'')/ρ(s'')⟩ of B, compatibly with the
structure maps from A and from B. This file proves that identification for the rings.
B carries the pair of definition TauCeti.Huber.PairOfDefinition.completionLocalization: its
ring of definition B₀ is the closure of the image of A₀[T/s], and its ideal of definition is
generated by the image of I. The standing hypothesis HasDenominatorPower for
(ρ(T''), ρ(s'')) is derived, not assumed: it follows from the one for (T'', s''), because
A_{s''} → B_{ρ(s'')} carries A₀[T''/s''] into B₀[ρ(T'')/ρ(s'')] and the powers of the ideal
of definition of B are generated by the images of the powers of I. So the interface below asks
only for the hypotheses over A. The comparison maps come from the two universal properties, and
each of their composites fixes a structure map, hence is the identity.
The numerators over B are a finset TB with underlying set ρ '' T'', so that no decidable
equality on B enters the statements.
Under the isomorphism the restriction map A⟨T/s⟩ → A⟨T''/s''⟩ is the structure map
B → B⟨ρ(T'')/ρ(s'')⟩. This is the reduction that opens Wedhorn's proof of Proposition 8.30, after
which the Laurent chain of Remark 7.55 runs over B; it is how
TauCeti.Huber.PairOfDefinition.flat_restrictionRingHom obtains flatness of restriction maps that
change the denominator.
Main definitions #
TauCeti.Huber.PairOfDefinition.iteratedLocalizationRingEquiv: the isomorphismA⟨T''/s''⟩ ≃+* B⟨ρ(T'')/ρ(s'')⟩.
Main results #
TauCeti.Huber.PairOfDefinition.hasDenominatorPower_completionLocalization: the standing hypothesis for(ρ(T''), ρ(s''))overB, for anyTBcontaining the images, and…_of_coe_eq_image: its specialisation to aTBequal to the image, which is what the declarations below derive rather than assume.TauCeti.Huber.PairOfDefinition.continuous_iteratedLocalizationRingEquivand…_symm: the isomorphism is one of topological rings.TauCeti.Huber.PairOfDefinition.iteratedLocalizationRingEquiv_coe_comp_toCompletionLocand…_symm_coe_comp_toCompletionLoc: compatibility with the structure maps fromAand fromB; the latter says the inverse turns the structure map ofB⟨ρ(T'')/ρ(s'')⟩into the restriction map.TauCeti.Huber.PairOfDefinition.eq_iteratedLocalizationRingEquiv: continuity and compatibility with the structure maps fromAalready determine the isomorphism.
Provenance #
AINTLIB (branch dev/adic-spaces, commit 37bbdaeb9) builds the same identification in
projects/AdicSpaces/Adic spaces/RelativeRationalLocData.lean, as relativeRationalLocData, with
the comparison maps relativeLaurentNormalized_forwardHom and
relativeLaurentNormalized_backwardHom assembled into relativeLaurentNormalized_equiv. Its
openness condition relativeRationalLocData_hopen_proof is left unproved there, and is proved only
when 1 is a numerator (relativeRationalLocData_hopen_proof_of_laurentNormalized). There the two
presentations may carry different pairs of definition; here both use the pair of A, which is what
lets the standing hypothesis transfer in general. The comparison maps here come from the universal
property of A⟨T/s⟩, and no code is ported.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Remark 8.4, Proposition 8.30 and Remark 7.55.
- C. Birkbeck, AINTLIB, branch
dev/adic-spaces, commit37bbdaeb9,projects/AdicSpaces/Adic spaces/RelativeRationalLocData.lean.
The standing hypothesis over A⟨T/s⟩ #
The standing hypothesis over A⟨T/s⟩. If (T'', s'') satisfies HasDenominatorPower over
A, then so does (TB, ρ(s'')) over A⟨T/s⟩ for its pair of definition
TauCeti.Huber.PairOfDefinition.completionLocalization, for any finset TB containing the images
ρ(t) of the numerators t ∈ T''.
The exponent is unchanged: the N-th power of the ideal of definition of A⟨T/s⟩ is generated by
the images ρ(b) of the b ∈ I ^ N, and ρ(b)/ρ(s'') is the image of b/s'', which lies in
A₀[T''/s''] by hypothesis.
The standing hypothesis over A⟨T/s⟩, for the numerators on the nose. The specialisation
of hasDenominatorPower_completionLocalization to a TB that is the image ρ '' T'', rather
than merely containing it. This is the form the isomorphism below runs on, which is why none of
its interface takes the conclusion as a hypothesis.
The two comparison maps #
The isomorphism #
Wedhorn's Remark 8.4, for rings. Let B = A⟨T/s⟩ and let (T'', s'') refine (T, s) with
cofactor r. Then A⟨T''/s''⟩ is isomorphic to the rational localisation B⟨TB/ρ(s'')⟩, where
ρ : A → B is the structure map and TB is a finset with underlying set ρ(T'').
Its four defining properties are continuous_iteratedLocalizationRingEquiv and
continuous_iteratedLocalizationRingEquiv_symm (it is continuous in both directions),
iteratedLocalizationRingEquiv_coe_comp_toCompletionLoc (compatibility with the structure maps from
A) and iteratedLocalizationRingEquiv_symm_coe_comp_toCompletionLoc (compatibility with those
from B, which is what separates it from restrictionRingHom), and
eq_iteratedLocalizationRingEquiv says that the first and third already determine it. Those five
are the interface to use.
Equations
- P.iteratedLocalizationRingEquiv T s S hden T'' s'' S'' hden'' SB TB hTB r hs'' hT = ⋯.choose
Instances For
The isomorphism A⟨T''/s''⟩ ≃+* B⟨TB/ρ(s'')⟩ is continuous, for the topologies of the two
pairs of definition: P at (T'', s'') on the source, and B's pair
completionLocalization P T s S hden at (TB, ρ(s'')) on the target. For the other direction see
continuous_iteratedLocalizationRingEquiv_symm.
The inverse of the isomorphism A⟨T''/s''⟩ ≃+* B⟨TB/ρ(s'')⟩ is continuous, so the isomorphism
is one of topological rings. The topologies are those of the two pairs of definition, in the roles
opposite to continuous_iteratedLocalizationRingEquiv: B's pair
completionLocalization P T s S hden at (TB, ρ(s'')) on the source, and P at (T'', s'') on
the target.
Compatibility with the structure maps from A. The isomorphism carries the structure map
A → A⟨T''/s''⟩ to the composite A → B → B⟨TB/ρ(s'')⟩, for the topologies of the two pairs of
definition: P at (T'', s'') on the source, and B's pair completionLocalization P T s S hden
at (TB, ρ(s'')) on the target. Together with continuity this compatibility determines the
isomorphism (eq_iteratedLocalizationRingEquiv).
Compatibility with the structure maps from B. The inverse isomorphism carries the
structure map B → B⟨TB/ρ(s'')⟩ to the restriction map B → A⟨T''/s''⟩: up to the isomorphism,
the restriction map of the refinement is the structure map of a rational localisation of B. The
topologies are those of the two pairs of definition, in the roles opposite to
iteratedLocalizationRingEquiv_coe_comp_toCompletionLoc: B's pair
completionLocalization P T s S hden at (TB, ρ(s'')) on the source, and P at (T'', s'') on
the target.
Continuity and compatibility with the structure maps from A determine the isomorphism.
Any continuous ring isomorphism A⟨T''/s''⟩ ≃+* B⟨TB/ρ(s'')⟩ carrying the structure map
A → A⟨T''/s''⟩ to the composite A → B → B⟨TB/ρ(s'')⟩ is it, so the two properties of its
inverse come for free.