# Documentation

Mathlib.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 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).

structure RingSubgroupsBasis {A : Type u_1} {ι : Type u_2} [Ring A] (B : ι) :
• 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 => 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 => 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.

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.

Instances For
theorem RingSubgroupsBasis.of_comm {A : Type u_3} {ι : Type u_4} [] (B : ι) (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 => x * y) ⁻¹' ↑(B i)) :
def RingSubgroupsBasis.toRingFilterBasis {A : Type u_1} {ι : Type u_2} [Ring A] [] {B : ι} (hB : ) :

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

Instances For
theorem RingSubgroupsBasis.mem_addGroupFilterBasis_iff {A : Type u_1} {ι : Type u_2} [Ring A] [] {B : ι} (hB : ) {V : Set A} :
V RingFilterBasis.toAddGroupFilterBasis i, V = ↑(B i)
theorem RingSubgroupsBasis.mem_addGroupFilterBasis {A : Type u_1} {ι : Type u_2} [Ring A] [] {B : ι} (hB : ) (i : ι) :
def RingSubgroupsBasis.topology {A : Type u_1} {ι : Type u_2} [Ring A] [] {B : ι} (hB : ) :

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

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

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

Instances For
theorem RingSubgroupsBasis.nonarchimedean {A : Type u_1} {ι : Type u_2} [Ring A] [] {B : ι} (hB : ) :
structure SubmodulesRingBasis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] (B : ι) :
• 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.

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.

Instances For
theorem SubmodulesRingBasis.toRing_subgroups_basis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {B : ι} (hB : ) :
def SubmodulesRingBasis.topology {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {B : ι} [] (hB : ) :

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

Instances For
structure SubmodulesBasis {ι : Type u_1} {R : Type u_2} [] {M : Type u_4} [] [Module R M] [] (B : ι) :
• 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.

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.

Instances For
def SubmodulesBasis.toModuleFilterBasis {ι : Type u_1} {R : Type u_2} [] {M : Type u_4} [] [Module R M] [] [] {B : ι} (hB : ) :

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

Instances For
def SubmodulesBasis.topology {ι : Type u_1} {R : Type u_2} [] {M : Type u_4} [] [Module R M] [] [] {B : ι} (hB : ) :

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

Instances For
def SubmodulesBasis.openAddSubgroup {ι : Type u_1} {R : Type u_2} [] {M : Type u_4} [] [Module R M] [] [] {B : ι} (hB : ) (i : ι) :

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

Instances For
theorem SubmodulesBasis.nonarchimedean {ι : Type u_1} {R : Type u_2} [] {M : Type u_4} [] [Module R M] [] [] {B : ι} (hB : ) :
theorem SubmodulesRingBasis.toSubmodulesBasis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] [] {B : ι} (hB : ) (hsmul : ∀ (m : A) (i : ι), ∀ᶠ (a : R) in nhds 0, a m B i) :
structure RingFilterBasis.SubmodulesBasis {ι : Type u_1} {R : Type u_2} [] {M : Type u_4} [] [Module R M] (BR : ) (B : ι) :
• 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, U BR U (fun x => 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.

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.

Instances For
theorem RingFilterBasis.submodulesBasisIsBasis {ι : Type u_1} {R : Type u_2} [] {M : Type u_4} [] [Module R M] (BR : ) {B : ι} (hB : ) :
def RingFilterBasis.moduleFilterBasis {ι : Type u_1} {R : Type u_2} [] {M : Type u_4} [] [Module R M] [] (BR : ) {B : ι} (hB : ) :

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.

Instances For