Documentation

TauCeti.RingTheory.Huber.PowSmulBasis.Basic

The ϖⁿ • M₀ submodules basis, and the A-module topology it induces #

Let A be a Tate ring, A₀ a ring of definition, ϖ ∈ A₀ a pseudouniformiser, and M₀ an A₀-submodule of an A-module M with A · M₀ = M. This file exhibits the family ϖⁿ • M₀ as a SubmodulesBasis, which is Mathlib's machinery for turning such a family into a topology; SubmodulesBasis.topology and .nonarchimedean then apply.

The result that the family is a neighbourhood basis at 0 says nothing about ϖ: it is proved for an arbitrary SubmodulesBasis in TauCeti/Topology/Algebra/Nonarchimedean/SubmodulesBasis.lean, and hasBasis_nhds_zero_pow_smul specializes it to this family. The abstract result that mutually cofinal families induce the same topology is SubmodulesBasis.topology_eq; submodulesBasis_pow_smul_topology_eq combines it with the lattice- and pseudouniformiser-cofinality theorems below.

Two of Proposition 6.18(1)'s clauses are established for the induced topology — that it is an A-module topology (powSmulModuleFilterBasis, since SubmodulesBasis.toModuleFilterBasis gives only an A₀-module one) and that it is first countable at 0 (isCountablyGenerated_nhds_zero).

Completeness and uniqueness are not. 6.18(1) asserts the topology is the unique complete first-countable A-module topology on a finitely generated module; neither half is proved below, so this is a construction of that topology's neighbourhood basis together with three of its properties, not an identification with the topology 6.18(1) characterises. What is proved is the weaker statement that the construction does not depend on the lattice or the pseudouniformiser it starts from (submodulesBasis_pow_smul_topology_eq): two finitely generated lattices spanning M, and two pseudouniformisers lying in the fixed ring of definition, give the same topology. That is well-definedness of Remark 6.19's recipe in those two choices, for a fixed ring of definition A₀: the remark chooses A₀ as well, and independence of that choice is not proved here. Nor is it 6.18(1)'s uniqueness, which quantifies over topologies never presented by a lattice at all.

The hypotheses are weaker than Wedhorn's, deliberately. Remark 6.19 assumes A noetherian and M₀ finitely generated. The basis and topology declarations use neither — only A · M₀ = M — and exists_pow_smul_le and exists_pow_smul_le_pow_smul not even that, asking instead the weaker containment that one lattice lie in the A-span of the other. Finite generation enters in those two, as a hypothesis on the submodule being compared, where a single exponent has to serve a whole submodule at once. submodulesBasis_pow_smul_topology_eq asks both of each lattice: spanning, because each side has to present a topology at all, and finite generation, because it runs the comparison in both directions. A noetherian is used nowhere in this file. Several declarations are weaker still, taking an arbitrary S : Subring A rather than a ring of definition, so a caller holding powerBoundedSubring A can use them.

Main results #

The elementary facts about rⁿ • M₀ over an arbitrary subring — antitonicity, absorption of further powers, and the ambient-scalar bridge — carry no Huber content and live in TauCeti.Algebra.Module.Submodule.Pointwise.

Implementation notes #

The neighbourhoods are A₀-submodules, not A-submodules, so SubmodulesBasis is instantiated at R := P.ringOfDefinition: M carries its A₀-module structure by restriction of scalars along A₀ → A, which typeclass inference supplies unaided.

The family is written out as ϖⁿ • M₀ rather than wrapped in a definition of its own: Mathlib's pointwise action on submodules already is that operation, and TauCeti.Algebra.Module.Submodule.Pointwise supplies the facts about it.

The family is ϖⁿ • M₀ rather than Iⁿ • M₀ for the ideal of definition I. That is Wedhorn's own indexing, and it is what the proofs below run on: both exists_pow_smul_mem and eventually_smul_mem_pow_smul consume the pseudouniformiser's own neighbourhood basis, TauCeti.Huber.IsPseudoUniformizer.hasBasis_nhds_zero. This is a choice of presentation and not a constraint — nothing here shows an I-indexed family would fail.

References #

source
theorem TauCeti.Huber.PairOfDefinition.exists_pow_smul_mem {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s : A} (hs : IsTopologicallyNilpotent s) (hs0 : s ∈ P.ringOfDefinition) (M₀ : Submodule (↥P.ringOfDefinition) M) {m : M} (hm : m ∈ Submodule.span A ↑M₀) :
∃ (k : ℕ), s ^ k • m ∈ M₀

A power of s carries any element of M = A · M₀ into M₀. This is where the hypothesis A · M₀ = M is spent, and it is what makes the smul condition of SubmodulesBasis an identity inside A₀.

source
theorem TauCeti.Huber.PairOfDefinition.eventually_smul_mem_pow_smul {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s : A} (hs : IsPseudoUniformizer s) (hs0 : s ∈ P.ringOfDefinition) (M₀ : Submodule (↥P.ringOfDefinition) M) {m : M} (hm : m ∈ Submodule.span A ↑M₀) (n : ℕ) :
∀ᶠ (a : ↥P.ringOfDefinition) in nhds 0, a • m ∈ ⟨s, hs0⟩ ^ n • M₀

The smul half of SubmodulesBasis: every scalar close enough to 0 in A₀ carries a given m into ϖⁿ • M₀.

m is carried into M₀ by ϖᵏ for some k (exists_pow_smul_mem), and ϖⁿ⁺ᵏ A₀ is a neighbourhood of 0; the two combine by arithmetic inside A₀.

source
theorem TauCeti.Huber.PairOfDefinition.submodulesBasis_pow_smul {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s : A} (hs : IsPseudoUniformizer s) (hs0 : s ∈ P.ringOfDefinition) (M₀ : Submodule (↥P.ringOfDefinition) M) (hspan : Submodule.span A ↑M₀ = ⊤) :
SubmodulesBasis fun (x : ℕ) => ⟨s, hs0⟩ ^ x • M₀

The ϖⁿ • M₀ family is a SubmodulesBasis, for a pseudouniformiser ϖ in a ring of definition A₀ and an A₀-submodule M₀ spanning M over A.

SubmodulesBasis.topology then makes M a topological A₀-module for which this family is a neighbourhood basis of 0, and SubmodulesBasis.nonarchimedean makes it a nonarchimedean additive group.

This is the basis half of Wedhorn's Remark 6.19. He states it for A noetherian and M₀ finitely generated, and identifies the resulting topology with the one of his Proposition 6.18(1); neither hypothesis is used here, and no such identification is proved here.

source
def TauCeti.Huber.PairOfDefinition.powSmulModuleFilterBasis {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s : A} (hs : IsPseudoUniformizer s) (hs0 : s ∈ P.ringOfDefinition) (M₀ : Submodule (↥P.ringOfDefinition) M) (hspan : Submodule.span A ↑M₀ = ⊤) :
ModuleFilterBasis A M

The A-module filter basis. SubmodulesBasis.toModuleFilterBasis only ever produces a filter basis over A₀; Wedhorn's Proposition 6.18(1) is about an A-module topology, so the three ModuleFilterBasis axioms are re-established with scalars from A.

Exposed because TauCeti.Huber.PairOfDefinition.powSmulModuleFilterBasis_topology states an equation between this basis's topology and the SubmodulesBasis one, which no proof can establish without unfolding this body.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Huber.PairOfDefinition.mem_powSmulModuleFilterBasis {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s : A} (hs : IsPseudoUniformizer s) (hs0 : s ∈ P.ringOfDefinition) (M₀ : Submodule (↥P.ringOfDefinition) M) (hspan : Submodule.span A ↑M₀ = ⊤) {U : Set M} :
    U ∈ (P.powSmulModuleFilterBasis hs hs0 M₀ hspan).toFilterBasis ↔ ∃ (n : ℕ), U = ↑(⟨s, hs0⟩ ^ n • M₀)

    Membership in the filter basis is the ϖⁿ • M₀ family, in normal form, so a consumer never unfolds TauCeti.Huber.PairOfDefinition.powSmulModuleFilterBasis.

    source
    @[simp]
    theorem TauCeti.Huber.PairOfDefinition.powSmulModuleFilterBasis_topology {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s : A} (hs : IsPseudoUniformizer s) (hs0 : s ∈ P.ringOfDefinition) (M₀ : Submodule (↥P.ringOfDefinition) M) (hspan : Submodule.span A ↑M₀ = ⊤) :
    (P.powSmulModuleFilterBasis hs hs0 M₀ hspan).topology = ⋯.topology

    The A-module topology is the A₀-level one. Widening the scalars from A₀ to A re-establishes the ModuleFilterBasis axioms but leaves the underlying AddGroupFilterBasis untouched, hence the topology too. This is what lets a consumer transport SubmodulesBasis.nonarchimedean and the rest of the A₀-level API across.

    source
    theorem TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero_pow_smul {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s : A} (hs : IsPseudoUniformizer s) (hs0 : s ∈ P.ringOfDefinition) (M₀ : Submodule (↥P.ringOfDefinition) M) (hspan : Submodule.span A ↑M₀ = ⊤) :
    (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => ⟨s, hs0⟩ ^ n • ↑M₀

    The ϖⁿ • M₀ family is a neighbourhood basis at 0, indexed by ℕ. A set is a neighbourhood of 0 for the topology M₀ induces exactly when it contains ϖⁿ • M₀ for some n.

    This is SubmodulesBasis.hasBasis_nhds_zero at this family; nothing about ϖ, M₀ or the Huber data enters. Stated for the SubmodulesBasis topology; TauCeti.Huber.PairOfDefinition.powSmulModuleFilterBasis_topology identifies that with the A-module one.

    source
    theorem TauCeti.Huber.PairOfDefinition.isCountablyGenerated_nhds_zero {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s : A} (hs : IsPseudoUniformizer s) (hs0 : s ∈ P.ringOfDefinition) (M₀ : Submodule (↥P.ringOfDefinition) M) (hspan : Submodule.span A ↑M₀ = ⊤) :
    (nhds 0).IsCountablyGenerated

    The topology has a countable fundamental system of neighbourhoods of 0, namely the ℕ-indexed family ϖⁿ • M₀. This is the first-countability clause of Proposition 6.18(1).

    Stated for the SubmodulesBasis topology, as the two neighbourhood facts above are; TauCeti.Huber.PairOfDefinition.powSmulModuleFilterBasis_topology identifies that with the A-module topology Proposition 6.18(1) is about.

    source
    theorem TauCeti.Huber.PairOfDefinition.exists_pow_smul_le {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s : A} (hs : IsTopologicallyNilpotent s) (hs0 : s ∈ P.ringOfDefinition) (M₀ M₁ : Submodule (↥P.ringOfDefinition) M) (hspan : ↑M₁ ⊆ ↑(Submodule.span A ↑M₀)) (hfg : M₁.FG) :
    ∃ (k : ℕ), ⟨s, hs0⟩ ^ k • M₁ ≤ M₀

    A power of ϖ carries a finitely generated A₀-submodule into M₀ wholesale.

    A single exponent serves all of M₁ at once. That uniformity is exactly what finite generation buys: without it exists_pow_smul_mem still gives an exponent for each element separately, but those exponents need not be bounded, and no power of ϖ need carry the whole submodule.

    M₀ is not required to span M; only M₁ need lie in its span.

    source
    theorem TauCeti.Huber.PairOfDefinition.exists_pow_smul_le_pow_smul {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s : A} (hs : IsTopologicallyNilpotent s) (hs0 : s ∈ P.ringOfDefinition) (M₀ M₁ : Submodule (↥P.ringOfDefinition) M) (hspan : ↑M₁ ⊆ ↑(Submodule.span A ↑M₀)) (hfg : M₁.FG) (n : ℕ) :
    ∃ (k : ℕ), ⟨s, hs0⟩ ^ k • M₁ ≤ ⟨s, hs0⟩ ^ n • M₀

    One-sided cofinality of the two ϖ-adic filtrations. Every member of the family built from M₀ contains a member of the family built from a finitely generated M₁.

    This is the comparison Remark 6.19's well-definedness in the lattice rests on, in one direction only: it gives the inclusion of the induced neighbourhood filters, not their equality. The reverse inclusion is this same theorem with the roles of M₀ and M₁ exchanged, which asks instead that M₀ lie in the A-span of M₁ and that M₀ be finitely generated. Note it is not that M₁ spans M: the hypothesis is one containment, not a spanning condition. submodulesBasis_pow_smul_topology_eq combines this with the analogous cofinality of the filtrations defined by two pseudouniformisers.

    submodulesBasis_pow_smul proves the basis half of Remark 6.19 without finite generation; this is where M₁.FG does its work.

    source
    theorem TauCeti.Huber.PairOfDefinition.exists_pow_smul_le_pow_smul_of_isPseudoUniformizer {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s t : A} (hs : IsUnit s) (ht : IsPseudoUniformizer t) (hs0 : s ∈ P.ringOfDefinition) (ht0 : t ∈ P.ringOfDefinition) (M₀ : Submodule (↥P.ringOfDefinition) M) (n : ℕ) :
    ∃ (k : ℕ), ⟨t, ht0⟩ ^ k • M₀ ≤ ⟨s, hs0⟩ ^ n • M₀

    The filtrations defined by two pseudouniformisers are cofinal. For every sⁿ • M₀, some tᵏ • M₀ is contained in it.

    Only t need be a pseudouniformiser (s need only be a unit), and no finite-generation or spanning hypothesis on M₀ is needed.

    source
    theorem TauCeti.Huber.PairOfDefinition.submodulesBasis_pow_smul_topology_eq_of_isPseudoUniformizer {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s t : A} (hs : IsPseudoUniformizer s) (ht : IsPseudoUniformizer t) (hs0 : s ∈ P.ringOfDefinition) (ht0 : t ∈ P.ringOfDefinition) (M₀ : Submodule (↥P.ringOfDefinition) M) (hspan : Submodule.span A ↑M₀ = ⊤) :
    ⋯.topology = ⋯.topology

    Changing the pseudouniformiser does not change the induced topology. This is the direct topological form of TauCeti.Huber.PairOfDefinition.exists_pow_smul_le_pow_smul_of_isPseudoUniformizer; unlike the comparison of two lattices, it requires no finite-generation hypothesis.

    source
    theorem TauCeti.Huber.PairOfDefinition.submodulesBasis_pow_smul_topology_eq {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (P : PairOfDefinition A) {s t : A} (hs : IsPseudoUniformizer s) (ht : IsPseudoUniformizer t) (hs0 : s ∈ P.ringOfDefinition) (ht0 : t ∈ P.ringOfDefinition) (M₀ M₁ : Submodule (↥P.ringOfDefinition) M) (hspan₀ : Submodule.span A ↑M₀ = ⊤) (hspan₁ : Submodule.span A ↑M₁ = ⊤) (hfg₀ : M₀.FG) (hfg₁ : M₁.FG) :
    ⋯.topology = ⋯.topology

    The induced topology does not depend on the lattice or the pseudouniformiser. Two finitely generated A₀-submodules that each span M over A, filtered by any two pseudouniformisers in A₀, induce the same topology.

    This is what makes Remark 6.19 well posed in its lattice. The remark says to choose a finitely generated M₀ with A · M₀ = M and then describes the topology by the family ϖⁿ • M₀; for that description to name a topology at all, neither the lattice nor the pseudouniformiser may matter. The ring of definition P is still fixed on both sides here, so independence of that remaining choice — which Remark 6.19 makes as well — is not proved.

    Finite generation is required of both lattices. Nothing else is: each already spans M, so no containment hypothesis between them is needed.

    Proposition 6.18(1) asserts something strictly stronger — uniqueness among all complete first-countable A-module topologies, including those given by no lattice — which is not proved here.