The natural topology of a finite module over a Huber ring

Let A be a Huber ring with a pair of definition (A₀, I) and let M be an A-module carrying its natural topology, Mathlib's IsModuleTopology A M. For a finitely generated A₀-submodule M₀ ⊆ M spanning M over A, the submodules Iⁿ • M₀ form a neighbourhood basis of 0 (Huber, A generalization of formal schemes and rigid analytic varieties, §2, before Lemma 2.3). No noetherian, Tate, or completeness hypothesis is needed.

This is the description of the natural topology through which finite modules over a Huber ring are compared with I-adically topologised modules over its ring of definition: it is the input for strictness of linear maps and for completeness of finite modules when A₀ is noetherian.

The file also records the absorption property of a ring of definition: a power of I carries a finitely generated A₀-submodule lying in the A-span of K into K.

Main results

• TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero_idealOfDefinition_pow_smul: the submodules Iⁿ • M₀ form a neighbourhood basis of 0 for the natural topology.
• TauCeti.Huber.PairOfDefinition.isOpen_of_span_eq_top: an A₀-submodule spanning a finite module over A is open.
• TauCeti.Huber.PairOfDefinition.exists_pow_smul_le: some Iʲ • L lies in K whenever L is finitely generated and lies in the A-span of K. This is the ideal-of-definition analogue of Subring.exists_pow_smul_le, which uses the powers of a single topologically nilpotent element.
• TauCeti.Huber.exists_span_range_eq_top_of_mem_nhds_zero: a finite module over a Tate ring, with any topology making scalar multiplication continuous, is spanned by finitely many elements of any neighbourhood of zero.

References

• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, before Lemma 2.3.

theorem TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero_idealOfDefinition_pow_smul {A : Type u_1} [CommRing A] [TopologicalSpace A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsTopologicalRing A] (P : PairOfDefinition A) [TopologicalSpace M] [IsModuleTopology A M] {M₀ : Submodule (↥P.ringOfDefinition) M} (hM₀ : M₀.FG) (hspan : Submodule.span A ↑M₀ = ⊤) : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => ↑(P.idealOfDefinition ^ n • M₀)

The natural topology of a module over a Huber ring is the I-adic topology of any finitely generated spanning lattice. If M carries its natural topology and M₀ is a finitely generated A₀-submodule spanning M over A, then the submodules Iⁿ • M₀ form a neighbourhood basis of 0 in M.

theorem TauCeti.Huber.PairOfDefinition.isOpen_of_span_eq_top {A : Type u_1} [CommRing A] [TopologicalSpace A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsTopologicalRing A] (P : PairOfDefinition A) [Module.Finite A M] [TopologicalSpace M] [IsModuleTopology A M] {M₀ : Submodule (↥P.ringOfDefinition) M} (hspan : Submodule.span A ↑M₀ = ⊤) : IsOpen ↑M₀

A spanning lattice is open. If M is a finite A-module with its natural topology, every A₀-submodule of M spanning M over A is open in M.

theorem TauCeti.Huber.PairOfDefinition.exists_pow_smul_le {A : Type u_1} [CommRing A] [TopologicalSpace A] {M : Type u_2} [AddCommGroup M] [Module A M] [SeparatelyContinuousMul A] (P : PairOfDefinition A) (K : Submodule (↥P.ringOfDefinition) M) {L : Submodule (↥P.ringOfDefinition) M} (hL : L.FG) (hLK : ↑L ⊆ ↑(Submodule.span A ↑K)) : ∃ (j : ℕ), P.idealOfDefinition ^ j • L ≤ K

A ring of definition absorbs finitely generated submodules of the span. If L is a finitely generated A₀-submodule lying in the A-span of an A₀-submodule K, then Iʲ • L ≤ K for some j.

theorem TauCeti.Huber.exists_span_range_eq_top_of_mem_nhds_zero {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [TopologicalSpace M] [ContinuousSMul A M] [Module.Finite A M] {W : Set M} (hW : W ∈ nhds 0) : ∃ (n : ℕ) (b : Fin n → M), (∀ (j : Fin n), b j ∈ W) ∧ Submodule.span A (Set.range b) = ⊤

A finite module over a Tate ring is spanned by finitely many elements of any neighbourhood of zero, for any topology making scalar multiplication continuous: scaling a finite generating family by a high power of a pseudouniformiser moves it into the neighbourhood without changing its span.