Dense submodules of a module-finite complete Tate-module

A dense submodule of a module-finite, complete, metrisable module over a complete Tate ring is the whole module. This is Bosch–Güntzer–Remmert §3.7.2/1 in its intrinsic form, and it is the step that makes finitely generated submodules closed on the route to Wedhorn 6.17/6.18.

The argument is the open mapping theorem followed by Nakayama. A finite spanning family presents V as an open quotient of Aⁿ (TauCeti.Huber.IsTateRing.isOpenMap_linearCombination), so the image of a neighbourhood of zero consisting of topologically nilpotent scalars is a neighbourhood of zero in V. Density writes each generator as gᵥ = mᵥ + ∑ⱼ aᵥⱼ • gⱼ with mᵥ in the submodule and every aᵥⱼ topologically nilpotent, and matrix Nakayama in the quotient (TauCeti.Huber.eq_zero_of_isTopologicallyNilpotent_entries_of_forall_eq_sum_smul) forces every generator into the submodule.

The neighbourhood of topologically nilpotent scalars is A°° itself, which is open (TauCeti.Huber.isOpen_setOf_isTopologicallyNilpotent) and contains zero, so neither an ideal of definition nor a pseudouniformiser has to be chosen.

Main results

• TauCeti.Huber.eq_top_of_dense_of_module_finite: a dense submodule of a module-finite complete Tate-module is everything.

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch_guntzer_remmert], §3.7.2/1.
• Wedhorn, Adic Spaces, Propositions 6.17–6.18.

Adapted from the AINTLIB development (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9, file projects/AdicSpaces/Adic spaces/WedhornBanachTheorem.lean, where the same statement is eq_top_of_dense_of_finite. The argument is AINTLIB's; three things differ. The target is separated by T0Space rather than T2Space. The neighbourhood of topologically nilpotent scalars is A°° itself rather than ϖ • A⁰ for a chosen pseudouniformiser, so no unit has to be produced. And the open presentation is the named TauCeti.Huber.IsTateRing.isOpenMap_linearCombination rather than a locally built linear map.

theorem TauCeti.Huber.eq_top_of_dense_of_module_finite {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsTateRing A] {V : Type u_2} [AddCommGroup V] [UniformSpace V] [IsUniformAddGroup V] [CompleteSpace V] [(uniformity V).IsCountablyGenerated] [T0Space V] [Module A V] [ContinuousSMul A V] [Module.Finite A V] (N : Submodule A V) (hN : Dense ↑N) : N = ⊤

A dense submodule of a module-finite complete Tate-module is everything (Bosch–Güntzer–Remmert §3.7.2/1).

N is a submodule of V whose closure is all of V; the conclusion is that N was already all of V. The hypotheses are carried by the ambient instances: A is a complete Hausdorff Tate ring, V is a complete T0 topological A-module with countably generated uniformity and continuous scalar action, and V is module-finite over A. Module-finiteness is what makes the statement true — a dense submodule of an infinite-dimensional complete module need not be everything.

The proof is the open mapping theorem followed by matrix Nakayama; see the module docstring.