mathlib documentation

topology.algebra.nonarchimedean.bases

Neighborhood bases for non-archimedean rings and modules #

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

The main definition is ring_subgroups_basis which is a predicate on a family of additive subgroups of a ring. The predicate ensures there is a topology ring_subgroups_basis.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 ring_subgroups_basis.open_add_subgroup) and we get a non-archimedean topological ring (ring_subgroups_basis.nonarchimedean).

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

structure ring_subgroups_basis {A : Type u_1} {ι : Type u_2} [ring A] (B : ι → add_subgroup A) :
Prop
  • inter : ∀ (i j : ι), ∃ (k : ι), B k B i B j
  • mul : ∀ (i : ι), ∃ (j : ι), (B j) * (B j) (B i)
  • left_mul : ∀ (x : A) (i : ι), ∃ (j : ι), (B j) (λ (y : A), x * y) ⁻¹' (B i)
  • right_mul : ∀ (x : A) (i : ι), ∃ (j : ι), (B j) (λ (y : A), y * x) ⁻¹' (B i)

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.

theorem ring_subgroups_basis.of_comm {A : Type u_1} {ι : Type u_2} [comm_ring A] (B : ι → add_subgroup A) (inter : ∀ (i j : ι), ∃ (k : ι), B k B i B j) (mul : ∀ (i : ι), ∃ (j : ι), (B j) * (B j) (B i)) (left_mul : ∀ (x : A) (i : ι), ∃ (j : ι), (B j) (λ (y : A), x * y) ⁻¹' (B i)) :
def ring_subgroups_basis.to_ring_filter_basis {A : Type u_1} {ι : Type u_2} [ring A] [nonempty ι] {B : ι → add_subgroup A} (hB : ring_subgroups_basis B) :

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

Equations
theorem ring_subgroups_basis.mem_add_group_filter_basis_iff {A : Type u_1} {ι : Type u_2} [ring A] [nonempty ι] {B : ι → add_subgroup A} (hB : ring_subgroups_basis B) {V : set A} :
theorem ring_subgroups_basis.mem_add_group_filter_basis {A : Type u_1} {ι : Type u_2} [ring A] [nonempty ι] {B : ι → add_subgroup A} (hB : ring_subgroups_basis B) (i : ι) :
def ring_subgroups_basis.topology {A : Type u_1} {ι : Type u_2} [ring A] [nonempty ι] {B : ι → add_subgroup A} (hB : ring_subgroups_basis B) :

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

Equations
theorem ring_subgroups_basis.has_basis_nhds_zero {A : Type u_1} {ι : Type u_2} [ring A] [nonempty ι] {B : ι → add_subgroup A} (hB : ring_subgroups_basis B) :
(nhds 0).has_basis (λ (_x : ι), true) (λ (i : ι), (B i))
theorem ring_subgroups_basis.has_basis_nhds {A : Type u_1} {ι : Type u_2} [ring A] [nonempty ι] {B : ι → add_subgroup A} (hB : ring_subgroups_basis B) (a : A) :
(nhds a).has_basis (λ (_x : ι), true) (λ (i : ι), {b : A | b - a B i})
def ring_subgroups_basis.open_add_subgroup {A : Type u_1} {ι : Type u_2} [ring A] [nonempty ι] {B : ι → add_subgroup A} (hB : ring_subgroups_basis B) (i : ι) :

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

Equations
theorem ring_subgroups_basis.nonarchimedean {A : Type u_1} {ι : Type u_2} [ring A] [nonempty ι] {B : ι → add_subgroup A} (hB : ring_subgroups_basis B) :
structure submodules_ring_basis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] (B : ι → submodule R A) :
Prop
  • inter : ∀ (i j : ι), ∃ (k : ι), B k B i B j
  • left_mul : ∀ (a : A) (i : ι), ∃ (j : ι), a B j B i
  • mul : ∀ (i : ι), ∃ (j : ι), (B j) * (B j) (B i)

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.

theorem submodules_ring_basis.to_ring_subgroups_basis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] {B : ι → submodule R A} (hB : submodules_ring_basis B) :
def submodules_ring_basis.topology {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] {B : ι → submodule R A} [nonempty ι] (hB : submodules_ring_basis B) :

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

Equations
structure submodules_basis {ι : Type u_1} {R : Type u_2} [comm_ring R] {M : Type u_4} [add_comm_group M] [module R M] [topological_space R] (B : ι → submodule R M) :
Prop
  • inter : ∀ (i j : ι), ∃ (k : ι), B k B i B j
  • smul : ∀ (m : M) (i : ι), ∀ᶠ (a : R) in nhds 0, a m B i

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.

def submodules_basis.to_module_filter_basis {ι : Type u_1} {R : Type u_2} [comm_ring R] {M : Type u_4} [add_comm_group M] [module R M] [topological_space R] [nonempty ι] {B : ι → submodule R M} (hB : submodules_basis B) :

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

Equations
def submodules_basis.topology {ι : Type u_1} {R : Type u_2} [comm_ring R] {M : Type u_4} [add_comm_group M] [module R M] [topological_space R] [nonempty ι] {B : ι → submodule R M} (hB : submodules_basis B) :

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

Equations
def submodules_basis.open_add_subgroup {ι : Type u_1} {R : Type u_2} [comm_ring R] {M : Type u_4} [add_comm_group M] [module R M] [topological_space R] [nonempty ι] {B : ι → submodule R M} (hB : submodules_basis B) (i : ι) :

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

Equations
theorem submodules_basis.nonarchimedean {ι : Type u_1} {R : Type u_2} [comm_ring R] {M : Type u_4} [add_comm_group M] [module R M] [topological_space R] [nonempty ι] {B : ι → submodule R M} (hB : submodules_basis B) :

The non archimedean subgroup basis lemmas cannot be instances because some instances (such as measure_theory.ae_eq_fun.add_monoid or topological_add_group.to_has_continuous_add) cause the search for @topological_add_group β ?m1 ?m2, i.e. a search for a topological group where the topology/group structure are unknown.

theorem submodules_ring_basis.to_submodules_basis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] [topological_space R] {B : ι → submodule R A} (hB : submodules_ring_basis B) (hsmul : ∀ (m : A) (i : ι), ∀ᶠ (a : R) in nhds 0, a m B i) :
structure ring_filter_basis.submodules_basis {ι : Type u_1} {R : Type u_2} [comm_ring R] {M : Type u_4} [add_comm_group M] [module R M] (BR : ring_filter_basis R) (B : ι → submodule R M) :
Prop
  • inter : ∀ (i j : ι), ∃ (k : ι), B k B i B j
  • smul : ∀ (m : M) (i : ι), ∃ (U : set R) (H : U BR), U (λ (a : R), a m) ⁻¹' (B i)

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

theorem ring_filter_basis.submodules_basis_is_basis {ι : Type u_1} {R : Type u_2} [comm_ring R] {M : Type u_4} [add_comm_group M] [module R M] (BR : ring_filter_basis R) {B : ι → submodule R M} (hB : BR.submodules_basis B) :
def ring_filter_basis.module_filter_basis {ι : Type u_1} {R : Type u_2} [comm_ring R] {M : Type u_4} [add_comm_group M] [module R M] [nonempty ι] (BR : ring_filter_basis R) {B : ι → submodule R M} (hB : BR.submodules_basis B) :

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