Restricted series lift along an open surjection

A continuous open surjection φ : A → B of nonarchimedean rings whose source has countably generated 𝓝 0 induces a surjection of restricted power-series rings — the trivial-weight TauCeti.Huber.weightedRestrictedSubring, before completion — coefficientwise.

Openness is the hypothesis that matters. Surjectivity of φ alone lifts each coefficient of a restricted series separately, but the preimages so chosen need not tend to zero, and then the lift is a power series and not a restricted one. Openness is what lets the preimages be drawn from a shrinking family of neighbourhoods; TauCeti.exists_lift_tendsto_cofinite_nhds is where that choice is made, and this file is its transcription into the weighted language, at the trivial weight family where restrictedness is convergence to zero (TauCeti.Huber.isWeightedRestricted_one_weight_iff).

Countable generation of 𝓝 (0 : A) is a hypothesis of both results here, not a background assumption: it is what supplies the shrinking family the lifted coefficients are drawn from, and a general NonarchimedeanRing need not have it. It is not restrictive in the intended application — a Huber ring satisfies it, by TauCeti.Huber.IsHuberRing.isCountablyGenerated_nhds_zero.

Main results

• TauCeti.Huber.weightedMap_one_weight_surjective, with IsOpenQuotientMap.weightedMap_one_weight_surjective the form taking the bundled structure — in that namespace so hq.weightedMap_one_weight_surjective works.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §5.6 and Proposition & Definition 6.36.

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, projects/AdicSpaces/Adic spaces/RestrictedModule.lean, has the corresponding statement for modules in one variable, restrictedModule_map_surjective, with both sides assumed Hausdorff. Nothing was copied.

theorem TauCeti.Huber.weightedMap_one_weight_surjective {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] [(nhds 0).IsCountablyGenerated] {φ : A →+* B} (hφ : Continuous ⇑φ) (hsurj : Function.Surjective ⇑φ) (hnhds : nhds 0 ≤ Filter.map (⇑φ) (nhds 0)) : Function.Surjective ⇑(weightedMap hφ ⋯ ⋯ ⋯)

A continuous surjection carrying neighbourhoods of zero onto neighbourhoods of zero stays surjective on restricted series, provided 𝓝 (0 : A) is countably generated. Every restricted series over B is then the image of one over A.

The hypothesis is stated as the filter inequality the proof consumes. Alongside the surjectivity assumed here it is the filter-level formulation of IsOpenMap φ, not a weakening of it — for a surjective continuous additive map the two say the same thing, since openness of a group homomorphism is decided at zero. IsOpenQuotientMap.weightedMap_one_weight_surjective is the form for a caller holding the bundled open-quotient structure.

This is a step towards what Wedhorn's Proposition & Definition 6.36(ii) needs, not the whole of it. TauCeti.Huber.IsStrictlyTopologicallyFiniteType asks for an open quotient map whose domain is TauCeti.Huber.restrictedMvPowerSeriesCompletion k A — the completion A⟨X₁,…,Xₖ⟩ at the trivial weight — whereas the surjection here is one level below, between the restricted subrings themselves. Passing from this to an open quotient out of the completion is a separate step.

TauCeti.Huber.IsTopologicallyFiniteType is the weaker notion, and what weakens it is the weight family, not completion: it allows an arbitrary finite family T in place of the trivial one. Both notions take their quotient out of a completion.

theorem IsOpenQuotientMap.weightedMap_one_weight_surjective {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] [(nhds 0).IsCountablyGenerated] {φ : A →+* B} (hq : IsOpenQuotientMap ⇑φ) : Function.Surjective ⇑(TauCeti.Huber.weightedMap ⋯ ⋯ ⋯ ⋯)

The open-quotient form of TauCeti.Huber.weightedMap_one_weight_surjective, for a caller holding the bundled IsOpenQuotientMap φ.

That is the interface finite-type presentations come in — TauCeti.Huber .IsStrictlyTopologicallyFiniteType produces one — so it is the form a consumer actually has, and it bundles exactly the continuity, surjectivity and openness the filter-level theorem needs.