# Neighborhood bases for non-archimedean rings and modules #

This file contains special families of filter bases on rings and modules that give rise to non-archimedean topologies.

The main definition is `RingSubgroupsBasis` which is a predicate on a family of additive subgroups of a ring. The predicate ensures there is a topology `RingSubgroupsBasis.topology` which is compatible with a ring structure and admits the given family as a basis of neighborhoods of zero. In particular, the given subgroups become open subgroups (bundled in `RingSubgroupsBasis.openAddSubgroup`) and we get a non-archimedean topological ring (`RingSubgroupsBasis.nonarchimedean`).

A special case of this construction is given by `SubmodulesBasis` where the subgroups are sub-modules in a commutative algebra. This important example gives rise to the adic topology (studied in its own file).

source
structure RingSubgroupsBasis {A : Type u_1} {ι : Type u_2} [Ring A] (B : ι → AddSubgroup A) :
Prop

A family of additive subgroups on a ring `A` is a subgroups basis if it satisfies some axioms ensuring there is a topology on `A` which is compatible with the ring structure and admits this family as a basis of neighborhoods of zero.

- inter (i j : ι) : ∃ (k : ι), B k ≤ B i ⊓ B j

  Condition for `B` to be a filter basis on `A`.

- mul (i : ι) : ∃ (j : ι), ↑(B j) * ↑(B j) ⊆ ↑(B i)

  For each set `B` in the submodule basis on `A`, there is another basis element `B'` such that the set-theoretic product `B' * B'` is in `B`.

- leftMul (x : A) (i : ι) : ∃ (j : ι), ↑(B j) ⊆ (fun (x_1 : A) => x * x_1) ⁻¹' ↑(B i)

  For any element `x : A` and any set `B` in the submodule basis on `A`, there is another basis element `B'` such that `B' * x` is in `B`.

- rightMul (x : A) (i : ι) : ∃ (j : ι), ↑(B j) ⊆ (fun (x_1 : A) => x_1 * x) ⁻¹' ↑(B i)

  For any element `x : A` and any set `B` in the submodule basis on `A`, there is another basis element `B'` such that `x * B'` is in `B`.

Instances For

source
theorem RingSubgroupsBasis.of_comm {A : Type u_3} {ι : Type u_4} [CommRing A] (B : ι → AddSubgroup A) (inter : ∀ (i j : ι), ∃ (k : ι), B k ≤ B i ⊓ B j) (mul : ∀ (i : ι), ∃ (j : ι), ↑(B j) * ↑(B j) ⊆ ↑(B i)) (leftMul : ∀ (x : A) (i : ι), ∃ (j : ι), ↑(B j) ⊆ (fun (y : A) => x * y) ⁻¹' ↑(B i)) :
RingSubgroupsBasis B
source
def RingSubgroupsBasis.toRingFilterBasis {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ι → AddSubgroup A} (hB : RingSubgroupsBasis B) :
RingFilterBasis A

Every subgroups basis on a ring leads to a ring filter basis.

Equations

- hB.toRingFilterBasis = { sets := {U : Set A | ∃ (i : ι), U = ↑(B i)}, nonempty := ⋯, inter_sets := ⋯, zero' := ⋯, add' := ⋯, neg' := ⋯, conj' := ⋯, mul' := ⋯, mul_left' := ⋯, mul_right' := ⋯ }

Instances For

source
theorem RingSubgroupsBasis.mem_addGroupFilterBasis_iff {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ι → AddSubgroup A} (hB : RingSubgroupsBasis B) {V : Set A} :
V ∈ hB.toRingFilterBasis.toAddGroupFilterBasis ↔ ∃ (i : ι), V = ↑(B i)
source
theorem RingSubgroupsBasis.mem_addGroupFilterBasis {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ι → AddSubgroup A} (hB : RingSubgroupsBasis B) (i : ι) :
↑(B i) ∈ hB.toRingFilterBasis.toAddGroupFilterBasis
source
def RingSubgroupsBasis.topology {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ι → AddSubgroup A} (hB : RingSubgroupsBasis B) :
TopologicalSpace A

The topology defined from a subgroups basis, admitting the given subgroups as a basis of neighborhoods of zero.

Equations

- hB.topology = hB.toRingFilterBasis.topology

Instances For

source
theorem RingSubgroupsBasis.hasBasis_nhds_zero {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ι → AddSubgroup A} (hB : RingSubgroupsBasis B) :
(nhds 0).HasBasis (fun (x : ι) => True) fun (i : ι) => ↑(B i)
source
theorem RingSubgroupsBasis.hasBasis_nhds {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ι → AddSubgroup A} (hB : RingSubgroupsBasis B) (a : A) :
(nhds a).HasBasis (fun (x : ι) => True) fun (i : ι) => {b : A | b - a ∈ B i}
source
def RingSubgroupsBasis.openAddSubgroup {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ι → AddSubgroup A} (hB : RingSubgroupsBasis B) (i : ι) :
OpenAddSubgroup A

Given a subgroups basis, the basis elements as open additive subgroups in the associated topology.

Equations

- hB.openAddSubgroup i = { toAddSubgroup := B i, isOpen' := ⋯ }

Instances For

source
theorem RingSubgroupsBasis.nonarchimedean {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ι → AddSubgroup A} (hB : RingSubgroupsBasis B) :
NonarchimedeanRing A
source
structure SubmodulesRingBasis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (B : ι → Submodule R A) :
Prop

A family of submodules in a commutative `R`-algebra `A` is a submodules basis if it satisfies some axioms ensuring there is a topology on `A` which is compatible with the ring structure and admits this family as a basis of neighborhoods of zero.

- inter (i j : ι) : ∃ (k : ι), B k ≤ B i ⊓ B j

  Condition for `B` to be a filter basis on `A`.

- leftMul (a : A) (i : ι) : ∃ (j : ι), a • B j ≤ B i

  For any element `a : A` and any set `B` in the submodule basis on `A`, there is another basis element `B'` such that `a • B'` is in `B`.

- mul (i : ι) : ∃ (j : ι), ↑(B j) * ↑(B j) ⊆ ↑(B i)

  For each set `B` in the submodule basis on `A`, there is another basis element `B'` such that the set-theoretic product `B' * B'` is in `B`.

Instances For

source
theorem SubmodulesRingBasis.toRing_subgroups_basis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {B : ι → Submodule R A} (hB : SubmodulesRingBasis B) :
RingSubgroupsBasis fun (i : ι) => (B i).toAddSubgroup
source
def SubmodulesRingBasis.topology {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {B : ι → Submodule R A} [Nonempty ι] (hB : SubmodulesRingBasis B) :
TopologicalSpace A

The topology associated to a basis of submodules in an algebra.

Equations

- hB.topology = ⋯.topology

Instances For

source
structure SubmodulesBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] (B : ι → Submodule R M) :
Prop

A family of submodules in an `R`-module `M` is a submodules basis if it satisfies some axioms ensuring there is a topology on `M` which is compatible with the module structure and admits this family as a basis of neighborhoods of zero.

- inter (i j : ι) : ∃ (k : ι), B k ≤ B i ⊓ B j

  Condition for `B` to be a filter basis on `M`.

- smul (m : M) (i : ι) : ∀ᶠ (a : R) in nhds 0, a • m ∈ B i

  For any element `m : M` and any set `B` in the basis, `a • m` lies in `B` for all `a` sufficiently close to `0`.

Instances For

source
def SubmodulesBasis.toModuleFilterBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] [Nonempty ι] {B : ι → Submodule R M} (hB : SubmodulesBasis B) :
ModuleFilterBasis R M

The image of a submodules basis is a module filter basis.

Equations

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

Instances For

source
def SubmodulesBasis.topology {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] [Nonempty ι] {B : ι → Submodule R M} (hB : SubmodulesBasis B) :
TopologicalSpace M

The topology associated to a basis of submodules in a module.

Equations

- hB.topology = hB.toModuleFilterBasis.topology

Instances For

source
def SubmodulesBasis.openAddSubgroup {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] [Nonempty ι] {B : ι → Submodule R M} (hB : SubmodulesBasis B) (i : ι) :
OpenAddSubgroup M

Given a submodules basis, the basis elements as open additive subgroups in the associated topology.

Equations

- hB.openAddSubgroup i = { toAddSubgroup := (B i).toAddSubgroup, isOpen' := ⋯ }

Instances For

source
theorem SubmodulesBasis.nonarchimedean {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] [Nonempty ι] {B : ι → Submodule R M} (hB : SubmodulesBasis B) :
NonarchimedeanAddGroup M
source
def SubmodulesBasis.Mathlib.LibraryNote.«non-Archimedean non-instances» :
LibraryNote

The non-Archimedean subgroup basis lemmas cannot be instances because some instances (such as `MeasureTheory.AEEqFun.instAddMonoid` or `IsTopologicalAddGroup.toContinuousAdd`) cause the search for `@IsTopologicalAddGroup β ?m1 ?m2`, i.e. a search for a topological group where the topology/group structure are unknown.

Equations

- SubmodulesBasis.Mathlib.LibraryNote.«non-Archimedean non-instances» = ()

Instances For

source
theorem SubmodulesRingBasis.toSubmodulesBasis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [TopologicalSpace R] {B : ι → Submodule R A} (hB : SubmodulesRingBasis B) (hsmul : ∀ (m : A) (i : ι), ∀ᶠ (a : R) in nhds 0, a • m ∈ B i) :
SubmodulesBasis B
source
structure RingFilterBasis.SubmodulesBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] (BR : RingFilterBasis R) (B : ι → Submodule R M) :
Prop

Given a ring filter basis on a commutative ring `R`, define a compatibility condition on a family of submodules of an `R`-module `M`. This compatibility condition allows to get a topological module structure.

- inter (i j : ι) : ∃ (k : ι), B k ≤ B i ⊓ B j

  Condition for `B` to be a filter basis on `M`.

- smul (m : M) (i : ι) : ∃ U ∈ BR, U ⊆ (fun (x : R) => x • m) ⁻¹' ↑(B i)

  For any element `m : M` and any set `B i` in the submodule basis on `M`, there is a `U` in the ring filter basis on `R` such that `U * m` is in `B i`.

Instances For

source
theorem RingFilterBasis.submodulesBasisIsBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] (BR : RingFilterBasis R) {B : ι → Submodule R M} (hB : BR.SubmodulesBasis B) :
_root_.SubmodulesBasis B
source
def RingFilterBasis.moduleFilterBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [Nonempty ι] (BR : RingFilterBasis R) {B : ι → Submodule R M} (hB : BR.SubmodulesBasis B) :
ModuleFilterBasis R M

The module filter basis associated to a ring filter basis and a compatible submodule basis. This allows to build a topological module structure compatible with the given module structure and the topology associated to the given ring filter basis.

Equations

- BR.moduleFilterBasis hB = ⋯.toModuleFilterBasis

Instances For