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.

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.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.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.

References

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

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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, and the k = 0 case says the completion map A → Â is one too.

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] [IsTopologicalRing 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.

theorem TauCeti.Huber.IsTopologicallyFiniteType.quotientMk {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing 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.

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] [CompleteSpace 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 complete 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.

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.