The canonical topology on a finite module over a Tate ring

Let A be a complete Hausdorff noetherian Tate ring and let M be a finite A-module. This file proves that Mathlib's moduleTopology A M is Hausdorff, the separatedness clause of Wedhorn, Adic Spaces, Proposition 6.18(1).

Choose a finite spanning family of M. Its linear-combination map Aⁿ → M is an open quotient for the module topologies, and its kernel is closed by TauCeti.Huber.isClosed_of_isNoetherian, so the closed-equivalence-relation criterion applies.

Separatedness is the one clause of Proposition 6.18(1) that uses A being a noetherian Tate ring. The other three — first countability, nonarchimedeanness, and completeness of the canonical right uniformity — need nothing of A beyond those same properties, and are proved in that generality in TauCeti.Topology.Algebra.Module.Finite; a Huber ring supplies the hypotheses they do need through TauCeti.Huber.IsHuberRing.isCountablyGenerated_nhds_zero and TauCeti.Huber.IsHuberRing.toNonarchimedeanRing. That file is re-exported here, so that this module is the single entry point for the whole existence half of Proposition 6.18(1).

Together with TauCeti.Huber.IsTateRing.isModuleTopology, these results give the existence and uniqueness asserted by Proposition 6.18(1), among the complete Hausdorff first-countable nonarchimedean topological module structures occurring in the open-mapping theorem. The topology is kept as the explicit expression moduleTopology A M in the statement: this is a theorem constructor for a local instance, rather than a global instance whose head would hide the topology on M from typeclass search.

Main results

• TauCeti.Huber.IsTateRing.t2Space_moduleTopology: the canonical topology is Hausdorff.

The remaining three clauses are re-exported from TauCeti.Topology.Algebra.Module.Finite: TauCeti.firstCountableTopology_moduleTopology, TauCeti.nonarchimedeanAddGroup_moduleTopology and TauCeti.completeSpace_moduleTopology.

References

• Wedhorn, Adic Spaces, Proposition 6.18(1).

theorem TauCeti.Huber.IsTateRing.t2Space_moduleTopology {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] [UniformSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [CompleteSpace A] [T0Space A] [IsTateRing A] [IsNoetherianRing A] : T2Space M

The module topology on a finite module over a complete noetherian Tate ring is Hausdorff. This supplies the separatedness clause of Wedhorn Proposition 6.18(1).