The Laurent quotient of a numerator enlargement, and the maps between it and `A⟨T'/s⟩` #

Let (T', s) refine (T, s) by enlarging the numerators, and let t ∈ T'. Adjoining a variable X to A⟨T/s⟩ and imposing the relation X = t/s gives A⟨T/s⟩⟨X⟩ ⧸ (t/s - X). This file constructs the two canonical continuous ring homomorphisms between that quotient and A⟨T'/s⟩, each the only one of its kind:

A⟨T/s⟩⟨X⟩ ⧸ (t/s - X)  →  A⟨T'/s⟩          constants ↦ restriction,  X ↦ t/s
A⟨T'/s⟩  →  A⟨T/s⟩⟨X⟩ ⧸ (t/s - X)          compatibly with the structure maps from `A`

The first needs nothing of the shape of T', which is what keeps DecidableEq A out of the statements. The second needs the numerators of T' to be exhausted by those of T together with t, since the fractions u/s for u ∈ T' must land in the power-bounded elements of the quotient; that is the hypothesis hsplit, again a splitting rather than T' = insert t T. It needs one hypothesis more, to make its target a legitimate one for the universal property of A⟨T'/s⟩: the relation ideal must be closed, which is what separates the quotient. A topologically nilpotent s over a strongly noetherian A⟨T/s⟩ gives that, and the ..._of_isStronglyNoetherian forms below take those two in its place.

The two maps are mutually inverse, under the same hsplit that the second one needs, and so the quotient is A⟨T'/s⟩ — Wedhorn's Remark 7.55. That is proved in TauCeti.RingTheory.Huber.LocalizationTopology.Laurent.Identification, which builds laurentQuotientRingEquiv from the two maps this file constructs. For a general enlargement no identification is expected, since T' may adjoin numerators other than t; hsplit is what rules that out.

The restriction map itself, and the fact that it carries t/s to t/s, live one file earlier in TauCeti.RingTheory.Huber.LocalizationTopology.Restriction: they need only the restriction/localisation theory, not the weighted-evaluation machinery imported here.

Main definitions #

TauCeti.Huber.PairOfDefinition.laurentRelationIdeal: the ideal (t/s - X) of A⟨T/s⟩⟨X⟩, where t/s is TauCeti.Localization.divBy read in the completion via TauCeti.Huber.PairOfDefinition.toCompletionLoc_mul_unit_inv_eq_divBy.

Main results #

TauCeti.Huber.PairOfDefinition.laurentRelationIdeal_quotientMk_weightedC: in the quotient, the constant t/s and the variable X agree. This is the relation the ideal imposes.
TauCeti.Huber.PairOfDefinition.existsUnique_continuous_ringHom_laurentQuotient_restriction: the map out of the quotient, with its uniqueness; and TauCeti.Huber.PairOfDefinition.laurentQuotientRestrictionRingHom, that map named, with TauCeti.Huber.PairOfDefinition.continuous_laurentQuotientRestrictionRingHom, its two evaluation lemmas and TauCeti.Huber.PairOfDefinition.eq_laurentQuotientRestrictionRingHom as its interface.
TauCeti.Huber.PairOfDefinition.existsUnique_continuous_ringHom_completion_laurentQuotient: the map into it, with its uniqueness, for a closed relation ideal; the ..._of_isStronglyNoetherian variant takes the hypotheses in the form they are met in.
TauCeti.Huber.PairOfDefinition.laurentQuotientRingHom: that map, named, with TauCeti.Huber.PairOfDefinition.continuous_laurentQuotientRingHom, TauCeti.Huber.PairOfDefinition.laurentQuotientRingHom_comp_toCompletionLoc and TauCeti.Huber.PairOfDefinition.eq_laurentQuotientRingHom as its interface.
TauCeti.Huber.PairOfDefinition.isClosed_laurentRelationIdeal: the relation ideal is closed when A⟨T/s⟩ is Tate and A⟨T/s⟩⟨X⟩ is noetherian; the ..._of_isStronglyNoetherian variant takes a topologically nilpotent denominator over a strongly noetherian base instead.

References #

T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Remark 7.55 and Proposition 8.30.

The Laurent quotient of a numerator enlargement, and the maps between it and A⟨T'/s⟩ #

Main definitions #

Main results #

References #

The Laurent quotient of a numerator enlargement, and the maps between it and `A⟨T'/s⟩` #