Strong noetherianness of a completed rational localisation

Preservation of strong noetherianness by a numerator enlargement. This is not Wedhorn's Proposition 8.30, whose stated conclusion is flatness; it is the auxiliary result that proposition is proved from. The flatness statement itself lives in TauCeti.RingTheory.Huber.LocalizationTopology.Laurent.Flat, which consumes what is proved here.

The argument is the chain of Wedhorn's Remark 7.55. Adjoining a single numerator t presents the enlarged localisation as a quotient of a one-variable restricted power-series algebra over the smaller one, by TauCeti.Huber.PairOfDefinition.laurentQuotientRingEquiv. For a topologically nilpotent denominator the presenting ideal is then closed as soon as that smaller ring is strongly noetherian, by TauCeti.Huber.PairOfDefinition.isClosed_laurentRelationIdeal_of_isStronglyNoetherian. Given the nilpotence, one hypothesis therefore carries the whole induction: strong noetherianness of the base both closes the ideal and, through IsOpenQuotientMap.isStronglyNoetherian, passes to the quotient. Nilpotence is asked only of a genuine enlargement — for T' = T there is nothing to prove.

Only the topology varies along the chain. The localisation S itself is fixed, because IsLocalization.Away s S does not mention the numerators, so each step is a hden.mono away and the base case of the induction is the hypothesis itself.

Main results

• TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion_of_isClosed : one enlargement step, with the presenting ideal assumed closed.
• TauCeti.Huber.PairOfDefinition .isStronglyNoetherian_completion_of_isTopologicallyNilpotent : the same step with closedness discharged, which is the form the induction consumes.
• TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion_of_subset : the chain form. Strong noetherianness propagates from T to every T' ⊇ T, which is what TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_union assumes at every proper intermediate presentation.

References

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

theorem TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion_of_isClosed {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hcl : t ∉ T → IsClosed ↑(P.laurentRelationIdeal T s t S hden)) (hSN : IsStronglyNoetherian (UniformSpace.Completion S)) : IsStronglyNoetherian (UniformSpace.Completion S')

Adjoining one numerator preserves strong noetherianness of the completed localisation, given that the smaller completed localisation is strongly noetherian and that the Laurent relation ideal is closed. T' is T with t adjoined, in the splitting form hsplit, so closedness is asked only when t is a genuinely new numerator: if t ∈ T then T' = T and this is invariance under changing the localisation carrier.

theorem TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion_of_isTopologicallyNilpotent {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (hnil : t ∉ T → IsTopologicallyNilpotent s) (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hSN : IsStronglyNoetherian (UniformSpace.Completion S)) : IsStronglyNoetherian (UniformSpace.Completion S')

Adjoining one numerator preserves strong noetherianness, for a topologically nilpotent denominator. No closedness hypothesis: over a strongly noetherian base the Laurent relation ideal is closed of its own accord. Nilpotence is asked only when t is a genuinely new numerator; if t ∈ T then T' = T and the statement is the invariance above. This is the form the induction over the numerators consumes.

theorem TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion_of_subset {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_4) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (hTT' : T ⊆ T') (hnil : T ⊂ T' → IsTopologicallyNilpotent s) (hSN : IsStronglyNoetherian (UniformSpace.Completion S)) : IsStronglyNoetherian (UniformSpace.Completion S)

Strong noetherianness is preserved by a numerator enlargement. If the completed localisation carrying the T-topology is strongly noetherian, then it is strongly noetherian for the T'-topology of any T' ⊇ T. Topological nilpotence of the denominator is asked only of a proper enlargement: for T' = T the conclusion is the hypothesis.

This is the auxiliary preservation result that Wedhorn's Proposition 8.30 is proved from, not the proposition itself, whose conclusion is flatness. It is what supplies strong noetherianness at the intermediate enlargements that TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_isStronglyNoetherian_base needs, from strong noetherianness at T alone.