Flatness of the Laurent quotient, and of rational restriction maps

Restriction maps between rational localisations are flat, at the ring level. For a fixed denominator the statements below run in increasing generality:

• the Laurent quotient A⟨T/s⟩⟨X⟩ ⧸ (t/s - X) is a flat A⟨T/s⟩-module when that base is a complete noetherian Tate ring;
• Wedhorn's Proposition 8.30, elementary case: the restriction map A⟨T/s⟩ → A⟨T'/s⟩ is flat when T' is T with one numerator t adjoined. It asks the hypotheses above of A⟨T/s⟩, together with closedness of the Laurent relation ideal, only when t ∉ T;
• the restriction map of an arbitrary enlargement T ⊆ T' is flat, assuming s topologically nilpotent and A⟨U/s⟩ strongly noetherian for every U with T ⊆ U ⊂ T'. On its own this is not Wedhorn's Proposition 8.30, which assumes strong noetherianity of the base alone; see The three chain results, and which to use;
• the same conclusion asking strong noetherianity only at T, the per-intermediate hypothesis being derived rather than assumed;
• the same conclusion asking strong noetherianity of A alone, for a presentation whose numerators generate the unit ideal together with s — Wedhorn's Proposition 8.30 for a numerator enlargement.

Two further cases of Proposition 8.30 change the denominator. The structure map A → A⟨T/s⟩ of any presentation over a complete separated strongly noetherian Tate ring is flat, which is the case where the larger rational subset is all of Spa A. And over a strongly noetherian Tate ring the restriction map A⟨T/s⟩ → A⟨T''/s''⟩ of any refinement — s'' = s * r, with each t * r a numerator of T'' — is flat when T together with s generates the unit ideal. By Remark 8.4 it is a structure map over A⟨T/s⟩, to which the previous case applies.

Changing the localisation that carries a presentation is flat with no hypotheses at all.

Each ..._of_isStronglyNoetherian variant states the analytic hypotheses in the form they are met in: s topologically nilpotent over a strongly noetherian base.

Main results

• TauCeti.Huber.PairOfDefinition.flat_quotient_laurentRelationIdeal : flatness over a base that is a noetherian Tate ring.
• TauCeti.Huber.PairOfDefinition.flat_quotient_laurentRelationIdeal_of_isStronglyNoetherian : flatness for a topologically nilpotent denominator over a strongly noetherian base, the form in which the hypotheses are met in practice.
• TauCeti.Huber.flat_quotient_rationalRelationIdeal_one : Lemma 8.31(2) in the weighted presentation — A⟨X⟩ ⧸ (1 - f X) is a flat A-module over a complete noetherian Tate ring.
• TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset : Proposition 8.30's elementary case — the restriction map A⟨T/s⟩ → A⟨T'/s⟩ is flat when T' adds the single numerator t, its analytic hypotheses being asked only for t ∉ T; the ..._of_isStronglyNoetherian variant takes them in their usual form, and asks them equally only for t ∉ T.
• TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_self : the identity enlargement — two presentations with the same numerator set, on possibly different localisations, are compared by a flat map. This one is hypothesis-free.
• TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_forall_isStronglyNoetherian : the chain form — the restriction map of an arbitrary enlargement T ⊆ T' is flat, assuming A⟨U/s⟩ strongly noetherian for every U with T ⊆ U ⊂ T'. That family hypothesis is what separates this from Wedhorn's Proposition 8.30, which assumes it of A alone; see The three chain results, and which to use.
• TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_isStronglyNoetherian_base : the same conclusion asking strong noetherianity only at T, the family hypothesis above being derived from it rather than assumed.
• PairOfDefinition.flat_restrictionRingHomOfSubset_of_span_eq_top : Wedhorn's Proposition 8.30 for a numerator enlargement. Strong noetherianity is asked of A, as Wedhorn asks it, and the unit-ideal condition on (T, s) is the algebraic form of rationality over a Tate ring. No condition is imposed on the denominator itself.
• TauCeti.Huber.PairOfDefinition.flat_toCompletionLoc : the structure map A → A⟨T/s⟩ is flat for every presentation of a complete separated strongly noetherian Tate ring, with no unit-ideal condition on (T, s). After rescaling by a unit, 1 can be adjoined as a numerator without changing A⟨T/s⟩; the denominator change then goes through A⟨X⟩ ⧸ (1 - f X) ≃ A⟨{1}/f⟩ (TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv at the single numerator 1) and Lemma 8.31(2), and the other numerators are adjoined by Proposition 8.30.
• TauCeti.Huber.PairOfDefinition.flat_restrictionRingHom_of_isStronglyNoetherian_base : the same statement asking the Tate condition and strong noetherianity of A⟨T/s⟩ rather than of A, and no unit-ideal condition. It is the general form; the next item is its corollary.
• TauCeti.Huber.PairOfDefinition.flat_restrictionRingHom : Wedhorn's Proposition 8.30 for a refinement, whose denominator may change — the restriction map A⟨T/s⟩ → A⟨T''/s''⟩ is flat over a strongly noetherian Tate ring when T together with s generates the unit ideal. It is the structure map of a rational localisation of A⟨T/s⟩ (TauCeti.Huber.PairOfDefinition.iteratedLocalizationRingEquiv), so the previous item applies over A⟨T/s⟩.

The three chain results, and which to use

Where strong noetherianity is assumed is the primary distinction, and each is the right one for a different caller. It is not the only one: the third asks the Tate condition, strong noetherianity, and the unit-ideal condition on (T, s) — all three only of a proper enlargement, as explicit hypotheses rather than instances. Its one unconditional assumption is [IsHuberRing A].

TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_forall_isStronglyNoetherian asks it of A⟨U/s⟩ for every U with T ⊆ U ⊂ T' — a family of hypotheses, carried rather than derived, and the theorem is named for what it assumes. It is the one to use when strong noetherianity is known only at the intermediate presentations.

TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_isStronglyNoetherian_base asks it only at T, deriving the rest by TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion_of_subset. It is the one to use when the localisation is known to be strongly noetherian but A is not, or when (T, s) is not known to cut out a rational subset.

PairOfDefinition.flat_restrictionRingHomOfSubset_of_span_eq_top asks it of A, which is Wedhorn's own hypothesis. It costs three explicit hypotheses, each asked only when T ⊂ T': IsTateRing A, IsStronglyNoetherian A, and the unit-ideal condition on (T, s). All three are free in the intended use — restriction between rational subsets of Spa(A, A⁺) of a strongly noetherian Tate ring — where the first two hold by hypothesis and the third follows from rationality, since an open ideal of a Tate ring is ⊤ (TauCeti.Huber.IsTateRing.isOpen_iff_eq_top). A caller there passes fun _ ↦ inferInstance for the first two.

Only [IsHuberRing A] remains an instance binder, because stating IsStronglyNoetherian A needs the nonarchimedean structure it carries.

The elementary case is unaffected: it needs strong noetherianity only at its own base, which is where Lemma 8.31 needs it too.

The refinement results are the same distinction one layer up. TauCeti.Huber.PairOfDefinition.flat_restrictionRingHom_of_isStronglyNoetherian_base asks the Tate condition and strong noetherianity of A⟨T/s⟩, and nothing of A or of (T, s); TauCeti.Huber.PairOfDefinition.flat_restrictionRingHom asks it of A together with the unit-ideal condition, and derives the other by TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion. Use the first when only the localisation is known to be strongly noetherian, the second for Wedhorn's own hypotheses.

References

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

theorem TauCeti.Huber.PairOfDefinition.flat_quotient_laurentRelationIdeal {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) (hTate : IsTateRing (UniformSpace.Completion S)) (hnoeth : IsNoetherianRing (UniformSpace.Completion S)) : Module.Flat (UniformSpace.Completion S) (↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯) ⧸ P.laurentRelationIdeal T s t S hden)

The Laurent quotient is flat over A⟨T/s⟩: A⟨T/s⟩⟨X⟩ ⧸ (t/s - X) is a flat A⟨T/s⟩-module.

This is Wedhorn's Lemma 8.31(2) over the base A⟨T/s⟩, whose remaining standing hypotheses — completeness, separation, non-archimedeanness and countable generation of the uniformity — hold of A⟨T/s⟩ unconditionally.

theorem TauCeti.Huber.PairOfDefinition.flat_quotient_laurentRelationIdeal_of_isStronglyNoetherian {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) (hnil : IsTopologicallyNilpotent s) (hSN : IsStronglyNoetherian (UniformSpace.Completion S)) : Module.Flat (UniformSpace.Completion S) (↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯) ⧸ P.laurentRelationIdeal T s t S hden)

The Laurent quotient is flat over A⟨T/s⟩, for a topologically nilpotent denominator over a strongly noetherian base.

A topologically nilpotent s makes A⟨T/s⟩ a Tate ring, and a strongly noetherian A⟨T/s⟩ is in particular noetherian, so this is TauCeti.Huber.PairOfDefinition.flat_quotient_laurentRelationIdeal with its two hypotheses discharged.

theorem TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_self {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) (S' : Type u_5) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T s S') : (P.restrictionRingHomOfSubset T s S hden T S' hden' ⋯).Flat

Changing the localisation that carries a presentation is flat. For two presentations with the same numerator set, carried by different localisations of A at s, the restriction map between them is flat.

This is the identity enlargement, and it assumes nothing: no nilpotence, no noetherianity. It is what lets the chain below end at an arbitrary localisation of T' rather than the one its induction runs on.

theorem TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset {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) (hTate : t ∉ T → IsTateRing (UniformSpace.Completion S)) (hnoeth : t ∉ T → IsNoetherianRing (UniformSpace.Completion S)) (hcl : t ∉ T → IsClosed ↑(P.laurentRelationIdeal T s t S hden)) : (P.restrictionRingHomOfSubset T s S hden T' S' hden' hTT').Flat

Proposition 8.30, the elementary case: the restriction map A⟨T/s⟩ → A⟨T'/s⟩ of a one-numerator enlargement is flat.

hsplit says that T' is the numerators of T together with the single t; hTate and hnoeth are Lemma 8.31's hypotheses on the base A⟨T/s⟩, and hcl asks the Laurent relation ideal to be closed. All three are asked only for t ∉ T. The ..._of_isStronglyNoetherian variant below takes them in the form they are met in.

theorem TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_isStronglyNoetherian {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) (hnil : t ∉ T → IsTopologicallyNilpotent s) (hSN : t ∉ T → IsStronglyNoetherian (UniformSpace.Completion S)) : (P.restrictionRingHomOfSubset T s S hden T' S' hden' hTT').Flat

Proposition 8.30, the elementary case, for a topologically nilpotent denominator over a strongly noetherian base: the hypotheses of TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset in the form they are met in, and asked — as there — only for t ∉ T.

theorem TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_forall_isStronglyNoetherian {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) (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) (hSN : ∀ (U : Finset A) (hU : T ⊆ U), U ⊂ T' → IsStronglyNoetherian (UniformSpace.Completion S)) : (P.restrictionRingHomOfSubset T s S hden T' S' hden' hTT').Flat

The chain form of Proposition 8.30, with strong noetherianity assumed at every proper intermediate presentation: the restriction map A⟨T/s⟩ → A⟨T'/s⟩ of an arbitrary enlargement is flat.

This is not Wedhorn's Proposition 8.30, and should not be cited as it. He assumes strong noetherianity of A alone; hSN here asks it of A⟨U/s⟩ for every U with T ⊆ U ⊂ T'. What separates the two is the standing hypothesis of his §8.2 — that rational localisations of a strongly noetherian ring are again strongly noetherian — which hSN assumes case by case rather than deriving.

TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_isStronglyNoetherian_base supplies that derivation, reducing the family hypothesis to strong noetherianity of A⟨T/s⟩ alone. The passage from A to A⟨T/s⟩ is supplied in turn by flat_restrictionRingHomOfSubset_of_span_eq_top, which reaches Wedhorn's own hypothesis at the cost of the unit-ideal condition on (T, s). This form remains the one to use when strong noetherianity is known only at the intermediate presentations.

The enlargement is arbitrary and so is the localisation S' carrying the target, matching TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset and the rest of the restriction API.

Both hypotheses are asked only of a proper enlargement, and for the same reason: the identity enlargement is TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_self, which assumes nothing. Strong noetherianity is then asked at every U with T ⊆ U ⊂ T', not only at T, because the elementary step needs it at its own base and it does not descend along an enlargement.

theorem TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_isStronglyNoetherian_base {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) (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) (hSN : T ⊂ T' → IsStronglyNoetherian (UniformSpace.Completion S)) : (P.restrictionRingHomOfSubset T s S hden T' S' hden' hTT').Flat

The chain form of Proposition 8.30 asking strong noetherianity only at T: if the completed localisation carrying the T-topology is strongly noetherian, the restriction map of any numerator enlargement is flat.

It is not Wedhorn's Proposition 8.30 as he states it. He assumes strong noetherianity of A; this asks it of A⟨T/s⟩. The passage between the two is TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion, applied in flat_restrictionRingHomOfSubset_of_span_eq_top below, which asks A alone but adds the unit-ideal condition on (T, s). Both hypotheses here are asked only of a proper enlargement: for T' = T the map is flat outright, by TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_self.

theorem TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_span_eq_top {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) (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') [IsHuberRing A] (hTate : T ⊂ T' → IsTateRing A) (hSN : T ⊂ T' → IsStronglyNoetherian A) (hspan : T ⊂ T' → Ideal.span (insert s ↑T) = ⊤) : (P.restrictionRingHomOfSubset T s S hden T' S' hden' hTT').Flat

Wedhorn's Proposition 8.30. Over a strongly noetherian Tate ring, the restriction map A⟨T/s⟩ → A⟨T'/s⟩ attached to a numerator enlargement is flat when T together with s generates the unit ideal.

No topological-nilpotence condition is imposed on s. The three hypotheses are conditional on T ⊂ T'. Thus the identity enlargement remains hypothesis-free, while in the intended application to rational subsets of a strongly noetherian Tate ring they are supplied by the ambient instances and by TauCeti.Huber.IsTateRing.isOpen_iff_eq_top.

theorem TauCeti.Huber.flat_quotient_rationalRelationIdeal_one {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [(uniformity A).IsCountablyGenerated] [T0Space A] [NonarchimedeanRing A] [IsTateRing A] [IsNoetherianRing A] (f : A) : Module.Flat A (↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯) ⧸ rationalRelationIdeal (fun (x : Fin 1) => 1) f)

Lemma 8.31(2) in the weighted presentation: over a complete noetherian Tate ring A, the quotient A⟨X⟩ ⧸ (1 - f X) by TauCeti.Huber.rationalRelationIdeal at the single numerator 1 over the denominator f is a flat A-module. Here A⟨X⟩ is the weighted restricted series ring with weight {1}, the presentation in which TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv identifies the quotient with A⟨{1}/f⟩. The hypotheses are those of TauCeti.Huber.flat_quotient_one_sub_algebraMap_mul_restrictedX, the same statement for the restricted power series ring.

Compare TauCeti.Huber.PairOfDefinition.flat_quotient_laurentRelationIdeal, the flatness over A⟨T/s⟩ of the quotient by (t/s - X).

theorem TauCeti.Huber.PairOfDefinition.flat_toCompletionLoc {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [CompleteSpace A] [T0Space A] [IsTateRing A] [IsStronglyNoetherian 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) : (P.toCompletionLoc T s S hden).Flat

The structure map A → A⟨T/s⟩ is flat for every presentation (T, s) of a complete separated strongly noetherian Tate ring: Wedhorn's Proposition 8.30 for the restriction from all of Spa A, whose ring of sections is A itself because A is complete and separated.

Nothing is asked of (T, s) beyond the standing hypothesis HasDenominatorPower. This is what separates it from TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_span_eq_top, which keeps the denominator s fixed and, for a proper enlargement, asks the unit-ideal condition on (T, s); here the source is A and the denominator is arbitrary.

theorem TauCeti.Huber.PairOfDefinition.flat_restrictionRingHom_of_isStronglyNoetherian_base {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) (T'' : Finset A) (s'' : A) (S'' : Type u_3) [CommRing S''] [Algebra A S''] [IsLocalization.Away s'' S''] (hden'' : P.HasDenominatorPower T'' s'' S'') (r : A) (hs'' : s'' = s * r) (hT : ∀ t ∈ T, t * r ∈ T'') (hTate : IsTateRing (UniformSpace.Completion S)) (hSN : IsStronglyNoetherian (UniformSpace.Completion S)) : (P.restrictionRingHom T s S hden T'' s'' S'' hden'' r hs'' hT).Flat

Wedhorn's Proposition 8.30 for a refinement, asking everything of A⟨T/s⟩. The restriction map A⟨T/s⟩ → A⟨T''/s''⟩ of a refinement is flat as soon as B = A⟨T/s⟩ is Tate and strongly noetherian: up to an isomorphism it is the structure map of a rational localisation of B.

Nothing is asked of A beyond the standing hypotheses — in particular A need not be Tate, so this covers a Tate localisation of a non-Tate base. This is the form to use when the localisation, rather than A, is what is known. When A itself is strongly noetherian and T together with s generates the unit ideal, use TauCeti.Huber.PairOfDefinition.flat_restrictionRingHom, which derives hSN from those. The pair mirrors …OfSubset_of_isStronglyNoetherian_base and …OfSubset_of_span_eq_top for a numerator enlargement.

theorem TauCeti.Huber.PairOfDefinition.flat_restrictionRingHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] [IsStronglyNoetherian 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) (T'' : Finset A) (s'' : A) (S'' : Type u_3) [CommRing S''] [Algebra A S''] [IsLocalization.Away s'' S''] (hden'' : P.HasDenominatorPower T'' s'' S'') (r : A) (hs'' : s'' = s * r) (hT : ∀ t ∈ T, t * r ∈ T'') (hspan : Ideal.span (insert s ↑T) = ⊤) : (P.restrictionRingHom T s S hden T'' s'' S'' hden'' r hs'' hT).Flat

Wedhorn's Proposition 8.30 for a refinement. Over a strongly noetherian Tate ring A, the restriction map A⟨T/s⟩ → A⟨T''/s''⟩ is flat whenever (T'', s'') refines (T, s) — that is, s'' = s * r and every t * r, for t ∈ T, lies in T'' — and T together with s generates the unit ideal. The denominator may change, and nothing is asked of (T'', s'') beyond the standing hypothesis.

When the denominator is unchanged, use PairOfDefinition.flat_restrictionRingHomOfSubset_of_span_eq_top instead: it is stated for TauCeti.Huber.PairOfDefinition.restrictionRingHomOfSubset, and asks the Tate condition, strong noetherianity and the unit-ideal condition only of a proper numerator enlargement. The restriction from all of Spa A is TauCeti.Huber.PairOfDefinition.flat_toCompletionLoc.