Neighborhood bases for non-archimedean rings and modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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).
- 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.
Every subgroups basis on a ring leads to a ring filter basis.
Equations
- hB.to_ring_filter_basis = {to_add_group_filter_basis := {to_filter_basis := {sets := {U : set A | ∃ (i : ι), U = ↑(B i)}, nonempty := _, inter_sets := _}, zero' := _, add' := _, neg' := _, conj' := _}, mul' := _, mul_left' := _, mul_right' := _}
The topology defined from a subgroups basis, admitting the given subgroups as a basis of neighborhoods of zero.
Equations
Given a subgroups basis, the basis elements as open additive subgroups in the associated topology.
- 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.
- 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.
The image of a submodules basis is a module filter basis.
Equations
- hB.to_module_filter_basis = {to_add_group_filter_basis := {to_filter_basis := {sets := {U : set M | ∃ (i : ι), U = ↑(B i)}, nonempty := _, inter_sets := _}, zero' := _, add' := _, neg' := _, conj' := _}, smul' := _, smul_left' := _, smul_right' := _}
The topology associated to a basis of submodules in a module.
Equations
Given a submodules basis, the basis elements as open additive subgroups in the associated topology.
Equations
- hB.open_add_subgroup i = {to_add_subgroup := {carrier := (B i).to_add_subgroup.carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, is_open' := _}
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.
- 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.
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.