Strong noetherianness of a completed rational localisation

Two results, one about the carrier of a presentation and one about the ring it presents.

Carrier-independence. A presentation (T, s) of a rational localisation is carried by some localisation S of A at s, and the choice is immaterial: two carriers of the same presentation have isomorphic completions. Strong noetherianness therefore depends on the presentation alone.

Strong noetherianity itself. When A is a strongly noetherian Tate ring and the numerators generate the unit ideal together with s, the completion A⟨T/s⟩ is again strongly noetherian. The route is the presentation: A⟨T/s⟩ is strictly topologically of finite type over A (TauCeti.Huber.PairOfDefinition.isStrictlyTopologicallyFiniteType_toCompletionLoc), and strong noetherianity travels along such a presentation. This is what a caller needs in order to iterate the construction, and hence what the sheaf condition for a strongly noetherian Huber pair rests on.

Nothing here is specific to Laurent presentations or to enlarging the numerator set; those live in TauCeti.RingTheory.Huber.LocalizationTopology.Laurent.StronglyNoetherian, which consumes this.

Main results

• TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion_self: the carrier does not matter.
• TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion: a rational localisation of a strongly noetherian Tate ring is strongly noetherian.

theorem TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion_self {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T s S') (hSN : IsStronglyNoetherian (UniformSpace.Completion S)) : IsStronglyNoetherian (UniformSpace.Completion S')

Strong noetherianness does not depend on which localisation carries a presentation. Two presentations with the same numerator set and denominator, carried by different localisations of A at s, have isomorphic completions, so one is strongly noetherian exactly when the other is. Nothing else is assumed: no nilpotence, no noetherianity.

This is the invariance a caller needs in order to change carriers.

theorem TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] [IsStronglyNoetherian A] [(nhds 0).IsCountablyGenerated] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (hspan : Ideal.span (insert s ↑T) = ⊤) : IsStronglyNoetherian (UniformSpace.Completion S)

A rational localisation of a strongly noetherian Tate ring is strongly noetherian, whenever the numerators together with the denominator s generate the unit ideal.

Strong noetherianity of A alone suffices: nothing is assumed of the localisation, and the hypothesis on the numerators is the rational-subset condition, which holds by definition wherever A⟨T/s⟩ is the ring of a rational subset.

This is the form Wedhorn's §8.2 needs in order to iterate: it makes strong noetherianity stable under passing to a rational localisation, so the argument may be repeated inside A⟨T/s⟩.