Homomorphisms topologically of finite type

Wedhorn's §6.6. A ring homomorphism φ : A → B is topologically of finite type when B is presented as an A-algebra by an open quotient map out of the completion of a weighted restricted power-series ring A⟨X₁, …, Xₖ⟩_T on finitely many variables, each weight Tᵢ finite. It is strictly topologically of finite type when the trivial weight family Tᵢ = {1} suffices, so that the presenting algebra is TauCeti.Huber.restrictedMvPowerSeriesCompletion, the object this library writes A⟨X₁, …, Xₖ⟩.

The notion is what three results the adic-spaces roadmap needs are stated in terms of: the second half of Proposition and Definition 6.36 (a Tate ring is strongly noetherian exactly when every Tate ring topologically of finite type over it is noetherian), Remark 6.37(1), and Example 6.38, which Proposition 8.30 cites by name.

What is and is not assumed

Wedhorn states 6.28 and 6.29 for an f-adic A and a complete f-adic B. Those standing hypotheses are deliberately not imposed here: the definitions ask only that A be a nonarchimedean topological commutative ring — the least that lets A⟨X⟩_T be formed at all — and that B be a topological commutative ring. The predicates are therefore defined on a wider class than Wedhorn's, and agree with his on the class he considers. A consumer that needs completeness of B should assume it alongside, not read it out of these definitions.

Notation, and one thing it is easy to get backwards

A⟨X₁, …, Xₖ⟩_T names the uncompleted weighted ring TauCeti.Huber.weightedRestrictedSubring of Wedhorn's Remark and Definition 5.48, as it does in the roadmap (AdicSpaces/README.md, §0.4). Wedhorn's presenting algebra in 6.28/6.29 is its completion, which he writes Â⟨…⟩; at the trivial weight family that completion is restrictedMvPowerSeriesCompletion, which this library writes A⟨X₁, …, Xₖ⟩ without a subscript. So the domain of π below is a completion throughout, never the subring itself.

The weighted algebra, and why not the Tate-only one

The presenting algebra is the weighted one. That is Wedhorn's own 6.29(i), and it is what the roadmap asks for (AdicSpaces/README.md, §5.2): the Tate-only algebra is too narrow downstream, since A_inf is Huber and not Tate. Definition 6.28, the strict variant, is the Tate-only case; the implication between them is IsStrictlyTopologicallyFiniteType.isTopologicallyFiniteType, and over a Tate ring the converse IsTopologicallyFiniteType.isStrictlyTopologicallyFiniteType holds as well.

Two conditions on the weight family are in play and they are not the same. Wedhorn's standing hypothesis on T — needed even to form A⟨X⟩_T — is TauCeti.Huber.IsWeightFamily, that Tᵢ^m · U is a neighbourhood of zero for every m and every neighbourhood U of zero. The phrasing in 6.29(i), that each Tᵢ · A is open, is the U = ⊤ case, and is recovered from it by TauCeti.Huber.IsWeightFamily.isOpen_weightMul_top; the converse is not available here (see that lemma's docstring). Finiteness of each Tᵢ is a separate requirement of 6.29(i) — it is what makes the notion one of finite type — and is carried explicitly, since IsWeightFamily does not imply it.

Main definitions

• TauCeti.Huber.IsStrictlyTopologicallyFiniteType: Wedhorn Definition 6.28.
• TauCeti.Huber.IsTopologicallyFiniteType: Wedhorn Proposition and Definition 6.29(i).

Main results

• TauCeti.Huber.isStrictlyTopologicallyFiniteType_algebraMap: the structure map A → A⟨X₁, …, Xₖ⟩ is strictly topologically of finite type — the presentation by the identity.
• TauCeti.Huber.IsStrictlyTopologicallyFiniteType.isTopologicallyFiniteType: strictly topologically of finite type implies topologically of finite type, by the trivial weight family.
• TauCeti.Huber.IsTopologicallyFiniteType.continuous: such a φ is continuous, since it factors through the presenting algebra's structure map.
• TauCeti.Huber.IsTopologicallyFiniteType.isOpen_map: out of a Huber ring, such a φ carries open ideals to ideals generating open ideals.
• TauCeti.Huber.IsStrictlyTopologicallyFiniteType.comp_isOpenQuotientMap and TauCeti.Huber.IsTopologicallyFiniteType.comp_isOpenQuotientMap: both notions are stable under composing with a further open quotient map.
• TauCeti.Huber.IsStrictlyTopologicallyFiniteType.quotientMk and TauCeti.Huber.IsTopologicallyFiniteType.quotientMk: in particular, stable under passing to a quotient by an ideal.
• TauCeti.Huber.IsTopologicallyFiniteType.comp_ringEquiv: topological finite type is stable under precomposing with an isomorphism of topological rings of the base.
• TauCeti.Huber.isStrictlyTopologicallyFiniteType_quotientMk_algebraMap: every quotient of A⟨X₁, …, Xₖ⟩ is strictly topologically of finite type over A — the shape of every Laurent and rational presentation.
• TauCeti.Huber.isStrictlyTopologicallyFiniteType_id: the identity of a complete Hausdorff nonarchimedean ring is strictly topologically of finite type, presented with no variables.
• TauCeti.Huber.isStrictlyTopologicallyFiniteType_coeRingHom: the completion map A → Â of a nonarchimedean uniform ring is strictly topologically of finite type, presented with no variables.
• TauCeti.Huber.IsStrictlyTopologicallyFiniteType.isStronglyNoetherian: over a strongly noetherian Huber ring, an algebra strictly topologically of finite type is again strongly noetherian.
• TauCeti.Huber.isStrictlyTopologicallyFiniteType_of_surjective: over a Tate ring, a surjection out of A⟨X₁, …, Xₖ⟩ that is continuous at zero is already a strict presentation — openness is supplied by the open mapping theorem rather than assumed.
• TauCeti.Huber.exists_isOpenQuotientMap_completion_weightedRestrictedSubring_append: over a Huber ring the completion of A⟨X₁, …, Xₖ⟩_T is an open quotient of the completion of A⟨X'₁, …, X'ₖ, Y₁, …, Yₘ⟩_{V, 1}, for any weights V making each Vᵢ Xᵢ power-bounded, with X'ᵢ going to Xᵢ and each unweighted Yⱼ to a weighted variable t Xᵢ.
• TauCeti.Huber.exists_isOpenQuotientMap_restrictedMvPowerSeriesCompletion: over a Tate ring the completion of A⟨X₁, …, Xₖ⟩_T is an open quotient of an unweighted A⟨Y₁, …, Yₘ⟩, each Yⱼ going to a weighted variable t Xᵢ and every weighted variable being hit.
• TauCeti.Huber.isStrictlyTopologicallyFiniteType_algebraMap_completion_weightedRestrictedSubring: over a Tate ring the completion of A⟨X₁, …, Xₖ⟩_T is strictly topologically of finite type, presented by one variable for each element of each Tᵢ.
• TauCeti.Huber.IsTopologicallyFiniteType.isStrictlyTopologicallyFiniteType and TauCeti.Huber.isStrictlyTopologicallyFiniteType_iff_isTopologicallyFiniteType: over a Tate ring the two notions agree, Wedhorn Proposition 6.34.
• TauCeti.Huber.IsTopologicallyFiniteType.isStronglyNoetherian: over a strongly noetherian Tate ring, an algebra topologically of finite type is strongly noetherian.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §6.6, Definition 6.28 and Proposition and Definition 6.29, and Proposition 6.34.

theorem TauCeti.Huber.image_append_algebraMap_weights {A : Type u_1} {B : Type u_2} {D : Type u_3} [CommRing A] [CommRing B] [CommRing D] [Algebra A D] {φ : A →+* B} {m n : ℕ} (V : Fin m → Set A) (π : D →+* B) (hπφ : ∀ (a : A), π ((algebraMap A D) a) = φ a) (i : Fin (m + n)) : ⇑π '' Fin.append (fun (i : Fin m) => ⇑(algebraMap A D) '' V i) (fun (x : Fin n) => {1}) i = Fin.append (fun (i : Fin m) => ⇑φ '' V i) (fun (x : Fin n) => {1}) i

The image under a ring map π : D → B of the weights algebraMap A D '' V i, followed by the trivial weights, is the corresponding weight family φ '' V i, followed by the trivial weights, whenever π restricts to φ on A.

theorem TauCeti.Huber.image_algebraMap_append_append_weights {A : Type u_1} {D : Type u_2} [CommRing A] [CommRing D] [Algebra A D] {k m n : ℕ} (T : Fin k → Set A) (V : Fin m → Set A) (j : Fin (m + n)) : ⇑(algebraMap A D) '' Fin.append T (Fin.append V fun (x : Fin n) => {1}) (Fin.natAdd k j) = Fin.append (fun (i : Fin m) => ⇑(algebraMap A D) '' V i) (fun (x : Fin n) => {1}) j

The image under algebraMap A D of the weights Fin.append T (Fin.append V 1) after the T block is algebraMap A D '' V i, followed by the trivial weights.

theorem TauCeti.Huber.finite_append_append_weights {A : Type u_1} [One A] {k m n : ℕ} {T : Fin k → Set A} {V : Fin m → Set A} (hT : ∀ (i : Fin k), (T i).Finite) (hV : ∀ (i : Fin m), (V i).Finite) (i : Fin (k + (m + n))) : (Fin.append T (Fin.append V fun (x : Fin n) => {1}) i).Finite

Appending T, V and the trivial weights keeps all weight sets finite.

def TauCeti.Huber.IsTopologicallyFiniteType {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] (φ : A →+* B) : Prop

Wedhorn Proposition and Definition 6.29(i): φ : A → B is topologically of finite type when B is presented, as an A-algebra, by an open quotient map out of the completion of a weighted restricted power-series ring on finitely many variables with each weight Tᵢ finite.

theorem TauCeti.Huber.isTopologicallyFiniteType_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] {φ : A →+* B} : IsTopologicallyFiniteType φ ↔ ∃ (k : ℕ) (T : Fin k → Set A) (_ : ∀ (i : Fin k), (T i).Finite) (hT : IsWeightFamily T) (π : UniformSpace.Completion ↥(weightedRestrictedSubring T hT) →+* B), IsOpenQuotientMap ⇑π ∧ π.comp (algebraMap A (UniformSpace.Completion ↥(weightedRestrictedSubring T hT))) = φ

Unfolding lemma for the sealed definition TauCeti.Huber.IsTopologicallyFiniteType.

def TauCeti.Huber.IsStrictlyTopologicallyFiniteType {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] (φ : A →+* B) : Prop

Wedhorn Definition 6.28: φ : A → B is strictly topologically of finite type when the presenting algebra can be taken to be A⟨X₁, …, Xₖ⟩, the trivial weight family.

theorem TauCeti.Huber.isStrictlyTopologicallyFiniteType_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] {φ : A →+* B} : IsStrictlyTopologicallyFiniteType φ ↔ ∃ (k : ℕ) (π : restrictedMvPowerSeriesCompletion k A →+* B), IsOpenQuotientMap ⇑π ∧ π.comp (algebraMap A (restrictedMvPowerSeriesCompletion k A)) = φ

Unfolding lemma for the sealed definition TauCeti.Huber.IsStrictlyTopologicallyFiniteType.

theorem TauCeti.Huber.isStrictlyTopologicallyFiniteType_algebraMap {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (k : ℕ) : IsStrictlyTopologicallyFiniteType (algebraMap A (restrictedMvPowerSeriesCompletion k A))

The presentation by the identity: the structure map A → A⟨X₁, …, Xₖ⟩ is strictly topologically of finite type. This is the witness that the conditions are simultaneously satisfiable. At k = 0 it presents the structure map A → A⟨⟩; for the completion map A → Â itself see TauCeti.Huber.isStrictlyTopologicallyFiniteType_coeRingHom.

theorem TauCeti.Huber.IsStrictlyTopologicallyFiniteType.isTopologicallyFiniteType {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] {φ : A →+* B} (h : IsStrictlyTopologicallyFiniteType φ) : IsTopologicallyFiniteType φ

The trivial weight family is finite and satisfies the standing hypothesis, so a strict presentation is a presentation.

theorem TauCeti.Huber.IsTopologicallyFiniteType.continuous {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] {φ : A →+* B} (h : IsTopologicallyFiniteType φ) : Continuous ⇑φ

A homomorphism topologically of finite type is continuous: it factors as an open quotient map after the presenting algebra's structure map, and both are continuous.

Stability under a further open quotient

Wedhorn presents an algebra topologically of finite type as an open quotient of a restricted power-series ring, so composing that presentation with another open quotient map is again a presentation of the same shape. This is what lets a quotient of A⟨X₁, …, Xₖ⟩ — the form every rational localisation and Laurent presentation takes — inherit finite type without exhibiting a fresh presentation by hand.

theorem TauCeti.Huber.IsStrictlyTopologicallyFiniteType.comp_isOpenQuotientMap {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] {C : Type u_3} [CommRing C] [TopologicalSpace C] {φ : A →+* B} {ψ : B →+* C} (h : IsStrictlyTopologicallyFiniteType φ) (hψ : IsOpenQuotientMap ⇑ψ) : IsStrictlyTopologicallyFiniteType (ψ.comp φ)

A strict presentation pushes along an open quotient map. If φ : A → B is strictly topologically of finite type and ψ : B → C is an open quotient map, then so is ψ ∘ φ: compose the presenting A⟨X₁, …, Xₖ⟩ ↠ B with ψ, and use that open quotient maps compose.

theorem TauCeti.Huber.IsTopologicallyFiniteType.comp_isOpenQuotientMap {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] {C : Type u_3} [CommRing C] [TopologicalSpace C] {φ : A →+* B} {ψ : B →+* C} (h : IsTopologicallyFiniteType φ) (hψ : IsOpenQuotientMap ⇑ψ) : IsTopologicallyFiniteType (ψ.comp φ)

A presentation pushes along an open quotient map, the weighted form of TauCeti.Huber.IsStrictlyTopologicallyFiniteType.comp_isOpenQuotientMap. The weight family is carried across unchanged; only the presenting map moves.

theorem TauCeti.Huber.IsStrictlyTopologicallyFiniteType.quotientMk {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] {φ : A →+* B} (h : IsStrictlyTopologicallyFiniteType φ) (I : Ideal B) : IsStrictlyTopologicallyFiniteType ((Ideal.Quotient.mk I).comp φ)

Strict finite type passes to a quotient by an ideal. The quotient map of a topological ring is an open quotient map, so this is the previous lemma at ψ = Ideal.Quotient.mk I. The topological ring structure of B comes from the presentation, as an open quotient of a topological ring.

theorem TauCeti.Huber.IsTopologicallyFiniteType.quotientMk {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] {φ : A →+* B} (h : IsTopologicallyFiniteType φ) (I : Ideal B) : IsTopologicallyFiniteType ((Ideal.Quotient.mk I).comp φ)

Finite type passes to a quotient by an ideal.

theorem TauCeti.Huber.isStrictlyTopologicallyFiniteType_quotientMk_algebraMap {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (k : ℕ) (I : Ideal (restrictedMvPowerSeriesCompletion k A)) : IsStrictlyTopologicallyFiniteType ((Ideal.Quotient.mk I).comp (algebraMap A (restrictedMvPowerSeriesCompletion k A)))

Every quotient of A⟨X₁, …, Xₖ⟩ is strictly topologically of finite type over A. This is the form every Laurent and rational presentation takes — Wedhorn's Examples 6.38 and 6.39 exhibit their rings this way — so it is the statement those examples reduce to once the presenting ideal is named.

Change of base along an isomorphism

theorem TauCeti.Huber.IsTopologicallyFiniteType.comp_ringEquiv {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] {A' : Type u_3} [CommRing A'] [TopologicalSpace A'] [NonarchimedeanRing A'] {φ : A →+* B} (h : IsTopologicallyFiniteType φ) (e : A' ≃+* A) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : IsTopologicallyFiniteType (φ.comp ↑e)

Topological finite type is stable under precomposition with an isomorphism of topological rings. If φ : A → B is topologically of finite type and e : A' ≃+* A is a ring isomorphism continuous in both directions, then φ ∘ e : A' → B is topologically of finite type. Compare TauCeti.Huber.IsTopologicallyFiniteType.comp_isOpenQuotientMap, which changes the target rather than the base.

The identity of a complete ring

theorem TauCeti.Huber.isStrictlyTopologicallyFiniteType_id {R : Type u_3} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [NonarchimedeanRing R] [CompleteSpace R] [T0Space R] : IsStrictlyTopologicallyFiniteType (RingHom.id R)

The identity of a complete Hausdorff nonarchimedean ring is strictly topologically of finite type, presented in no variables. Compare the k = 0 case of TauCeti.Huber.isStrictlyTopologicallyFiniteType_algebraMap, which presents the completion map R → R⟨⟩ of an arbitrary R rather than the identity.

The completion map

theorem TauCeti.Huber.isStrictlyTopologicallyFiniteType_coeRingHom {R : Type u_3} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [NonarchimedeanRing R] : IsStrictlyTopologicallyFiniteType UniformSpace.Completion.coeRingHom

The completion map R → R̂ is strictly topologically of finite type, presented in no variables: the comparison R⟨⟩ ≅ R of the uncompleted rings extends to an isomorphism of topological rings R⟨⟩ ≅ R̂ of their completions, under which the structure map of R⟨⟩ becomes the completion map. The completion R̂ is formed for the given uniformity of R.

Strong noetherianness

Strong noetherianness passes from A to any algebra strictly topologically of finite type over it. This is the standing hypothesis of Wedhorn's §8.2 in the form the flatness results consume: rational localisations of a strongly noetherian ring are again strongly noetherian, once they are known to be strictly topologically of finite type.

theorem TauCeti.Huber.IsStrictlyTopologicallyFiniteType.isStronglyNoetherian {A : Type u_3} {B : Type u_4} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [IsStronglyNoetherian A] [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [NonarchimedeanRing B] [T0Space B] {φ : A →+* B} (hφ : IsStrictlyTopologicallyFiniteType φ) : IsStronglyNoetherian B

Strong noetherianness passes to an algebra strictly topologically of finite type. Over a strongly noetherian Huber ring A, a Hausdorff nonarchimedean ring B admitting a map φ : A →+* B strictly topologically of finite type is again strongly noetherian.

The intended use is Wedhorn's §8.2, where TauCeti.Huber.PairOfDefinition.flat_restrictionRingHomOfSubset_of_forall_isStronglyNoetherian asks that every rational localisation in a cover be strongly noetherian. Combined with a strict finite type presentation of such a localisation over its base — the shape TauCeti.Huber.isStrictlyTopologicallyFiniteType_quotientMk_algebraMap produces, and the one Wedhorn's Examples 6.38 and 6.39 exhibit — this theorem reduces that hypothesis to strong noetherianness of the base alone.

Open ideals

theorem TauCeti.Huber.IsTopologicallyFiniteType.isOpen_map {A : Type u_3} {B : Type u_4} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] {φ : A →+* B} (h : IsTopologicallyFiniteType φ) {J : Ideal A} (hJ : IsOpen ↑J) : IsOpen ↑(Ideal.map φ J)

A homomorphism topologically of finite type out of a Huber ring carries open ideals to ideals generating open ideals, part of the adicity in Wedhorn's Proposition and Definition 6.29.

Presentations supplied by the open mapping theorem

Over a Tate ring a strict presentation need not be exhibited as an open map: openness is automatic. A surjection out of A⟨X₁, …, Xₖ⟩ onto a complete Hausdorff first countable algebra that is continuous at zero is open, so continuity and surjectivity together already make it a strict presentation.

theorem TauCeti.Huber.isStrictlyTopologicallyFiniteType_of_surjective {A : Type u_3} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [IsTateRing A] {B : Type u_4} [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [CompleteSpace B] [(uniformity B).IsCountablyGenerated] [T0Space B] [Algebra A B] [ContinuousConstSMul A B] {k : ℕ} (π : restrictedMvPowerSeriesCompletion k A →ₐ[A] B) (hπ : ContinuousAt (⇑π) 0) (hs : Function.Surjective ⇑π) : IsStrictlyTopologicallyFiniteType (algebraMap A B)

Over a Tate ring, a surjection out of A⟨X₁, …, Xₖ⟩ that is continuous at zero is a strict presentation. Openness is not a third obligation: with continuity at zero and surjectivity in hand, Wedhorn Definition 6.28 asks for nothing more.

The hypotheses on the target are the standing hypotheses of Wedhorn's §8.2: complete, Hausdorff, and first countable in the form of a countably generated uniformity. The source needs nothing beyond what A⟨X₁, …, Xₖ⟩ already carries.

The target is an arbitrary ring receiving a surjection, not the literal quotient type A⟨X₁, …, Xₖ⟩ ⧸ I that TauCeti.Huber.isStrictlyTopologicallyFiniteType_quotientMk_algebraMap covers. That is what a consumer holds: a completed rational localisation is not a quotient type.

This constructs no surjection. Exhibiting one onto a given B is the work; this theorem removes openness from the list of things that then have to be checked.

Trading weights for variables

Over a Huber ring the substitution Y_{(i, t)} ↦ t Xᵢ, with one unweighted variable for each t ∈ Tᵢ, maps A⟨Yⱼ⟩ openly into the completed weighted algebra A⟨X₁, …, Xₖ⟩_T, onto an open subring. Adjoining the variables Xᵢ themselves, with any weights Vᵢ making Vᵢ Xᵢ power-bounded, gives an open quotient map onto A⟨X₁, …, Xₖ⟩_T.

Over a Tate ring the weights can be removed altogether: the open subring already contains each Xᵢ, since the pseudouniformiser is a unit, so A⟨X₁, …, Xₖ⟩_T is an open quotient of the unweighted A⟨Yⱼ⟩. Consequently the two finite-type notions of Wedhorn's §6.6 coincide over a Tate ring (Wedhorn Proposition 6.34), and strong noetherianness passes to every algebra topologically of finite type over a strongly noetherian Tate ring, which is the input to Corollary 8.35.

theorem TauCeti.Huber.exists_isOpenQuotientMap_completion_weightedRestrictedSubring_append {A : Type u_3} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {k : ℕ} {T : Fin k → Set A} (hT : IsWeightFamily T) {V : Fin k → Set A} (hTfin : ∀ (i : Fin k), (T i).Finite) (hV : IsWeightFamily V) (hVX : IsWeightedVarPowerBounded (algebraMap A (UniformSpace.Completion ↥(weightedRestrictedSubring T hT))) V fun (i : Fin k) => ↑(weightedX T hT i)) : ∃ (m : ℕ) (idx : Fin m → Fin k) (t : Fin m → A), (∀ (j : Fin m), t j ∈ T (idx j)) ∧ (∀ (i : Fin k), ∀ a ∈ T i, ∃ (j : Fin m), idx j = i ∧ t j = a) ∧ ∃ (θ : UniformSpace.Completion ↥(weightedRestrictedSubring (Fin.append V fun (x : Fin m) => {1}) ⋯) →+* UniformSpace.Completion ↥(weightedRestrictedSubring T hT)), IsOpenQuotientMap ⇑θ ∧ θ.comp (algebraMap A (UniformSpace.Completion ↥(weightedRestrictedSubring (Fin.append V fun (x : Fin m) => {1}) ⋯))) = algebraMap A (UniformSpace.Completion ↥(weightedRestrictedSubring T hT)) ∧ (∀ (i : Fin k), θ ↑(weightedX (Fin.append V fun (x : Fin m) => {1}) ⋯ (Fin.castAdd m i)) = ↑(weightedX T hT i)) ∧ ∀ (j : Fin m), θ ↑(weightedX (Fin.append V fun (x : Fin m) => {1}) ⋯ (Fin.natAdd k j)) = ↑((weightedC T hT) (t j) * weightedX T hT (idx j))

Over a Huber ring the completed weighted algebra is an open quotient of a partly unweighted one. Let T be a finite weight family and V a weight family such that each weighted variable Vᵢ Xᵢ is power-bounded in the completion of A⟨X₁, …, Xₖ⟩_T. For an enumeration j ↦ (idx j, t j) of the pairs (i, t) with t ∈ Tᵢ, there is an open quotient map over A from the completion of A⟨X'₁, …, X'ₖ, Y₁, …, Yₘ⟩_{V, 1} onto that of A⟨X₁, …, Xₖ⟩_T, sending X'ᵢ to Xᵢ and Yⱼ to tⱼ X_{idx j}.

Each unweighted Yⱼ stands for the weighted variable tⱼ X_{idx j}, so the weights T reappear as variables. The variables X'ᵢ are needed because over a general Huber ring the tⱼ X_{idx j} need not generate Xᵢ: over ℤ_[p] with T = {p}, the series in p X do not contain X. They may carry any weights V for which Vᵢ Xᵢ is power-bounded. Over a Tate ring the X'ᵢ can be dropped: TauCeti.Huber.exists_isOpenQuotientMap_restrictedMvPowerSeriesCompletion.

theorem TauCeti.Huber.exists_isOpenQuotientMap_restrictedMvPowerSeriesCompletion {A : Type u_3} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] {k : ℕ} {T : Fin k → Set A} (hT : IsWeightFamily T) (hTfin : ∀ (i : Fin k), (T i).Finite) : ∃ (m : ℕ) (idx : Fin m → Fin k) (t : Fin m → A), (∀ (j : Fin m), t j ∈ T (idx j)) ∧ (∀ (i : Fin k), ∀ a ∈ T i, ∃ (j : Fin m), idx j = i ∧ t j = a) ∧ ∃ (θ : restrictedMvPowerSeriesCompletion m A →+* UniformSpace.Completion ↥(weightedRestrictedSubring T hT)), IsOpenQuotientMap ⇑θ ∧ θ.comp (algebraMap A (restrictedMvPowerSeriesCompletion m A)) = algebraMap A (UniformSpace.Completion ↥(weightedRestrictedSubring T hT)) ∧ ∀ (j : Fin m), θ ↑(weightedX (fun (x : Fin m) => {1}) ⋯ j) = ↑((weightedC T hT) (t j) * weightedX T hT (idx j))

Over a Tate ring the completed weighted algebra is an open quotient of an unweighted one. For a finite weight family T there is an enumeration j ↦ (idx j, t j) of the pairs (i, t) with t ∈ Tᵢ, and an open quotient map θ : A⟨Y₁, …, Yₘ⟩ → A⟨X₁, …, Xₖ⟩_T (completed) over A sending Yⱼ to tⱼ X_{idx j}.

theorem TauCeti.Huber.isStrictlyTopologicallyFiniteType_algebraMap_completion_weightedRestrictedSubring {A : Type u_3} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] {k : ℕ} {T : Fin k → Set A} (hT : IsWeightFamily T) (hTfin : ∀ (i : Fin k), (T i).Finite) : IsStrictlyTopologicallyFiniteType (algebraMap A (UniformSpace.Completion ↥(weightedRestrictedSubring T hT)))

Over a Tate ring the completed weighted algebra is strictly topologically of finite type. For a finite weight family T, the completion of A⟨X₁, …, Xₖ⟩_T is an open quotient of an unweighted A⟨Y₁, …, Yₘ⟩ with one variable for each pair (i, t) with t ∈ Tᵢ, mapped to t Xᵢ.

theorem TauCeti.Huber.IsTopologicallyFiniteType.isStrictlyTopologicallyFiniteType {A : Type u_3} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] {B : Type u_4} [CommRing B] [TopologicalSpace B] {φ : A →+* B} (hφ : IsTopologicallyFiniteType φ) : IsStrictlyTopologicallyFiniteType φ

Over a Tate ring, topologically of finite type is strictly topologically of finite type: a presentation by a weighted restricted power-series algebra can be replaced by one by A⟨Y₁, …, Yₘ⟩. The converse is TauCeti.Huber.IsStrictlyTopologicallyFiniteType.isTopologicallyFiniteType, for any base.

theorem TauCeti.Huber.isStrictlyTopologicallyFiniteType_iff_isTopologicallyFiniteType {A : Type u_3} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] {B : Type u_4} [CommRing B] [TopologicalSpace B] {φ : A →+* B} : IsStrictlyTopologicallyFiniteType φ ↔ IsTopologicallyFiniteType φ

Wedhorn Proposition 6.34: over a Tate ring the two finite-type notions of Wedhorn's §6.6 agree. Wedhorn assumes B complete f-adic; no hypothesis on B is needed here.

theorem TauCeti.Huber.IsTopologicallyFiniteType.isStronglyNoetherian {A : Type u_3} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] [IsStronglyNoetherian A] {B : Type u_4} [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [NonarchimedeanRing B] [T0Space B] {φ : A →+* B} (hφ : IsTopologicallyFiniteType φ) : IsStronglyNoetherian B

Strong noetherianness passes to an algebra topologically of finite type over a Tate ring. Over a strongly noetherian Tate ring A, a Hausdorff nonarchimedean ring B admitting a map φ : A →+* B topologically of finite type is again strongly noetherian.