mathlib documentation

topology.algebra.filter_basis

Group and ring filter bases #

A group_filter_basis is a filter_basis on a group with some properties relating the basis to the group structure. The main theorem is that a group_filter_basis on a group gives a topology on the group which makes it into a topological group with neighborhoods of the neutral element generated by the given basis.

Main definitions and results #

Given a group G and a ring R:

References #

@[class]
structure group_filter_basis (G : Type u) [group G] :
Type u

A group_filter_basis on a group is a filter_basis satisfying some additional axioms. Example : if G is a topological group then the neighbourhoods of the identity are a group_filter_basis. Conversely given a group_filter_basis one can define a topology compatible with the group structure on G.

Instances for group_filter_basis
@[class]
structure add_group_filter_basis (A : Type u) [add_group A] :
Type u

A add_group_filter_basis on an additive group is a filter_basis satisfying some additional axioms. Example : if G is a topological group then the neighbourhoods of the identity are a add_group_filter_basis. Conversely given a add_group_filter_basis one can define a topology compatible with the group structure on G.

Instances of this typeclass
Instances of other typeclasses for add_group_filter_basis
def add_group_filter_basis_of_comm {G : Type u_1} [add_comm_group G] (sets : set (set G)) (nonempty : sets.nonempty) (inter_sets : ∀ (x y : set G), x setsy sets(∃ (z : set G) (H : z sets), z x y)) (one : ∀ (U : set G), U sets0 U) (mul : ∀ (U : set G), U sets(∃ (V : set G) (H : V sets), V + V U)) (inv : ∀ (U : set G), U sets(∃ (V : set G) (H : V sets), V (λ (x : G), -x) ⁻¹' U)) :

add_group_filter_basis constructor in the commutative group case.

Equations
def group_filter_basis_of_comm {G : Type u_1} [comm_group G] (sets : set (set G)) (nonempty : sets.nonempty) (inter_sets : ∀ (x y : set G), x setsy sets(∃ (z : set G) (H : z sets), z x y)) (one : ∀ (U : set G), U sets1 U) (mul : ∀ (U : set G), U sets(∃ (V : set G) (H : V sets), V * V U)) (inv : ∀ (U : set G), U sets(∃ (V : set G) (H : V sets), V (λ (x : G), x⁻¹) ⁻¹' U)) :

group_filter_basis constructor in the commutative group case.

Equations
@[protected, instance]
Equations
theorem add_group_filter_basis.zero {G : Type u} [add_group G] {B : add_group_filter_basis G} {U : set G} :
U B0 U
theorem group_filter_basis.one {G : Type u} [group G] {B : group_filter_basis G} {U : set G} :
U B1 U
theorem group_filter_basis.mul {G : Type u} [group G] {B : group_filter_basis G} {U : set G} :
U B(∃ (V : set G) (H : V B), V * V U)
theorem add_group_filter_basis.add {G : Type u} [add_group G] {B : add_group_filter_basis G} {U : set G} :
U B(∃ (V : set G) (H : V B), V + V U)
theorem group_filter_basis.inv {G : Type u} [group G] {B : group_filter_basis G} {U : set G} :
U B(∃ (V : set G) (H : V B), V (λ (x : G), x⁻¹) ⁻¹' U)
theorem add_group_filter_basis.neg {G : Type u} [add_group G] {B : add_group_filter_basis G} {U : set G} :
U B(∃ (V : set G) (H : V B), V (λ (x : G), -x) ⁻¹' U)
theorem group_filter_basis.conj {G : Type u} [group G] {B : group_filter_basis G} (x₀ : G) {U : set G} :
U B(∃ (V : set G) (H : V B), V (λ (x : G), x₀ * x * x₀⁻¹) ⁻¹' U)
theorem add_group_filter_basis.conj {G : Type u} [add_group G] {B : add_group_filter_basis G} (x₀ : G) {U : set G} :
U B(∃ (V : set G) (H : V B), V (λ (x : G), x₀ + x + -x₀) ⁻¹' U)
@[protected, instance]

The trivial group filter basis consists of {1} only. The associated topology is discrete.

Equations
@[protected, instance]

The trivial additive group filter basis consists of {0} only. The associated topology is discrete.

Equations
theorem group_filter_basis.prod_subset_self {G : Type u} [group G] (B : group_filter_basis G) {U : set G} (h : U B) :
U U * U
theorem add_group_filter_basis.sum_subset_self {G : Type u} [add_group G] (B : add_group_filter_basis G) {U : set G} (h : U B) :
U U + U
def add_group_filter_basis.N {G : Type u} [add_group G] (B : add_group_filter_basis G) :
G → filter G

The neighborhood function of a add_group_filter_basis

Equations
def group_filter_basis.N {G : Type u} [group G] (B : group_filter_basis G) :
G → filter G

The neighborhood function of a group_filter_basis

Equations
@[protected]
theorem add_group_filter_basis.has_basis {G : Type u} [add_group G] (B : add_group_filter_basis G) (x : G) :
(B.N x).has_basis (λ (V : set G), V B) (λ (V : set G), (λ (y : G), x + y) '' V)
@[protected]
theorem group_filter_basis.has_basis {G : Type u} [group G] (B : group_filter_basis G) (x : G) :
(B.N x).has_basis (λ (V : set G), V B) (λ (V : set G), (λ (y : G), x * y) '' V)

The topological space structure coming from a group filter basis.

Equations

The topological space structure coming from an additive group filter basis.

Equations
theorem add_group_filter_basis.nhds_eq {G : Type u} [add_group G] (B : add_group_filter_basis G) {x₀ : G} :
nhds x₀ = B.N x₀
theorem group_filter_basis.nhds_eq {G : Type u} [group G] (B : group_filter_basis G) {x₀ : G} :
nhds x₀ = B.N x₀
theorem add_group_filter_basis.nhds_has_basis {G : Type u} [add_group G] (B : add_group_filter_basis G) (x₀ : G) :
(nhds x₀).has_basis (λ (V : set G), V B) (λ (V : set G), (λ (y : G), x₀ + y) '' V)
theorem group_filter_basis.nhds_has_basis {G : Type u} [group G] (B : group_filter_basis G) (x₀ : G) :
(nhds x₀).has_basis (λ (V : set G), V B) (λ (V : set G), (λ (y : G), x₀ * y) '' V)
theorem add_group_filter_basis.nhds_zero_has_basis {G : Type u} [add_group G] (B : add_group_filter_basis G) :
(nhds 0).has_basis (λ (V : set G), V B) id
theorem group_filter_basis.nhds_one_has_basis {G : Type u} [group G] (B : group_filter_basis G) :
(nhds 1).has_basis (λ (V : set G), V B) id
theorem group_filter_basis.mem_nhds_one {G : Type u} [group G] (B : group_filter_basis G) {U : set G} (hU : U B) :
U nhds 1
theorem add_group_filter_basis.mem_nhds_zero {G : Type u} [add_group G] (B : add_group_filter_basis G) {U : set G} (hU : U B) :
U nhds 0
@[protected, instance]

If a group is endowed with a topological structure coming from a group filter basis then it's a topological group.

@[protected, instance]

If a group is endowed with a topological structure coming from a group filter basis then it's a topological group.

@[class]
structure ring_filter_basis (R : Type u) [ring R] :
Type u

A ring_filter_basis on a ring is a filter_basis satisfying some additional axioms. Example : if R is a topological ring then the neighbourhoods of the identity are a ring_filter_basis. Conversely given a ring_filter_basis on a ring R, one can define a topology on R which is compatible with the ring structure.

Instances for ring_filter_basis
@[protected, instance]
def ring_filter_basis.has_mem {R : Type u} [ring R] :
Equations
theorem ring_filter_basis.mul {R : Type u} [ring R] (B : ring_filter_basis R) {U : set R} (hU : U B) :
∃ (V : set R) (H : V B), V * V U
theorem ring_filter_basis.mul_left {R : Type u} [ring R] (B : ring_filter_basis R) (x₀ : R) {U : set R} (hU : U B) :
∃ (V : set R) (H : V B), V (λ (x : R), x₀ * x) ⁻¹' U
theorem ring_filter_basis.mul_right {R : Type u} [ring R] (B : ring_filter_basis R) (x₀ : R) {U : set R} (hU : U B) :
∃ (V : set R) (H : V B), V (λ (x : R), x * x₀) ⁻¹' U

The topology associated to a ring filter basis. It has the given basis as a basis of neighborhoods of zero.

Equations
@[protected, instance]

If a ring is endowed with a topological structure coming from a ring filter basis then it's a topological ring.

structure module_filter_basis (R : Type u_1) (M : Type u_2) [comm_ring R] [topological_space R] [add_comm_group M] [module R M] :
Type u_2

A module_filter_basis on a module is a filter_basis satisfying some additional axioms. Example : if M is a topological module then the neighbourhoods of zero are a module_filter_basis. Conversely given a module_filter_basis one can define a topology compatible with the module structure on M.

Instances for module_filter_basis
theorem module_filter_basis.smul {R : Type u_1} {M : Type u_2} [comm_ring R] [topological_space R] [add_comm_group M] [module R M] (B : module_filter_basis R M) {U : set M} (hU : U B) :
∃ (V : set R) (H : V nhds 0) (W : set M) (H : W B), V W U
theorem module_filter_basis.smul_left {R : Type u_1} {M : Type u_2} [comm_ring R] [topological_space R] [add_comm_group M] [module R M] (B : module_filter_basis R M) (x₀ : R) {U : set M} (hU : U B) :
∃ (V : set M) (H : V B), V (λ (x : M), x₀ x) ⁻¹' U
theorem module_filter_basis.smul_right {R : Type u_1} {M : Type u_2} [comm_ring R] [topological_space R] [add_comm_group M] [module R M] (B : module_filter_basis R M) (m₀ : M) {U : set M} (hU : U B) :
∀ᶠ (x : R) in nhds 0, x m₀ U
@[protected, instance]

If R is discrete then the trivial additive group filter basis on any R-module is a module filter basis.

Equations
def module_filter_basis.topology {R : Type u_1} {M : Type u_2} [comm_ring R] [topological_space R] [add_comm_group M] [module R M] (B : module_filter_basis R M) :

The topology associated to a module filter basis on a module over a topological ring. It has the given basis as a basis of neighborhoods of zero.

Equations
def module_filter_basis.topology' {R : Type u_1} {M : Type u_2} [comm_ring R] {tR : topological_space R} [add_comm_group M] [module R M] (B : module_filter_basis R M) :

The topology associated to a module filter basis on a module over a topological ring. It has the given basis as a basis of neighborhoods of zero. This version gets the ring topology by unification instead of type class inference.

Equations
theorem has_continuous_smul.of_basis_zero {R : Type u_1} {M : Type u_2} [comm_ring R] [topological_space R] [add_comm_group M] [module R M] {ι : Type u_3} [topological_ring R] [topological_space M] [topological_add_group M] {p : ι → Prop} {b : ι → set M} (h : (nhds 0).has_basis p b) (hsmul : ∀ {i : ι}, p i(∃ (V : set R) (H : V nhds 0) (j : ι) (hj : p j), V b j b i)) (hsmul_left : ∀ (x₀ : R) {i : ι}, p i(∃ (j : ι) (hj : p j), b j (λ (x : M), x₀ x) ⁻¹' b i)) (hsmul_right : ∀ (m₀ : M) {i : ι}, p i(∀ᶠ (x : R) in nhds 0, x m₀ b i)) :

A topological add group whith a basis of 𝓝 0 satisfying the axioms of module_filter_basis is a topological module.

This lemma is mathematically useless because one could obtain such a result by applying module_filter_basis.has_continuous_smul and use the fact that group topologies are characterized by their neighborhoods of 0 to obtain the has_continuous_smul on the pre-existing topology.

But it turns out it's just easier to get it as a biproduct of the proof, so this is just a free quality-of-life improvement.

@[protected, instance]

If a module is endowed with a topological structure coming from a module filter basis then it's a topological module.

def module_filter_basis.of_bases {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (BR : ring_filter_basis R) (BM : add_group_filter_basis M) (smul : ∀ {U : set M}, U BM(∃ (V : set R) (H : V BR) (W : set M) (H : W BM), V W U)) (smul_left : ∀ (x₀ : R) {U : set M}, U BM(∃ (V : set M) (H : V BM), V (λ (x : M), x₀ x) ⁻¹' U)) (smul_right : ∀ (m₀ : M) {U : set M}, U BM(∃ (V : set R) (H : V BR), V (λ (x : R), x m₀) ⁻¹' U)) :

Build a module filter basis from compatible ring and additive group filter bases.

Equations