# mathlibdocumentation

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:

• group_filter_basis G: the type of filter bases that will become neighborhood of 1 for a topology on G compatible with the group structure
• group_filter_basis.topology: the associated topology
• group_filter_basis.is_topological_group: the compatibility between the above topology and the group structure
• ring_filter_basis R: the type of filter bases that will become neighborhood of 0 for a topology on R compatible with the ring structure
• ring_filter_basis.topology: the associated topology
• ring_filter_basis.is_topological_ring: the compatibility between the above topology and the ring structure

## References #

@[class]
structure group_filter_basis (G : Type u) [group G] :
Type u
• to_filter_basis :
• one' : ∀ {U : set G},
• mul' : ∀ {U : set G}, (∃ (V : set G) (H : , V * V U)
• inv' : ∀ {U : set G}, (∃ (V : set G) (H : , V (λ (x : G), x⁻¹) ⁻¹' U)
• conj' : ∀ (x₀ : G) {U : set G}, (∃ (V : set G) (H : , V (λ (x : G), x₀ * x * x₀⁻¹) ⁻¹' 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]
Type u
• to_filter_basis :
• zero' : ∀ {U : set A},
• add' : ∀ {U : set A}, (∃ (V : set A) (H : , V + V U)
• neg' : ∀ {U : set A}, (∃ (V : set A) (H : , V (λ (x : A), -x) ⁻¹' U)
• conj' : ∀ (x₀ : A) {U : set A}, (∃ (V : set A) (H : , V (λ (x : A), x₀ + x + -x₀) ⁻¹' 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} (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
@[protected, instance]
def group_filter_basis.has_mem {G : Type u} [group G] :
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)
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]
def group_filter_basis.inhabited {G : Type u} [group G] :

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
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 →

The neighborhood function of a group_filter_basis

Equations
@[simp]
theorem group_filter_basis.N_one {G : Type u} [group G] (B : group_filter_basis G) :
@[simp]
@[protected]
(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)
def group_filter_basis.topology {G : Type u} [group G] (B : group_filter_basis G) :

The topological space structure coming from a group filter basis.

Equations

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

Equations
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 group_filter_basis.nhds_one_eq {G : Type u} [group G] (B : group_filter_basis 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)
(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
• mul' : ∀ {U : set R}, (∃ (V : set R) (H : , V * V U)
• mul_left' : ∀ (x₀ : R) {U : set R}, (∃ (V : set R) (H : , V (λ (x : R), x₀ * x) ⁻¹' U)
• mul_right' : ∀ (x₀ : R) {U : set R}, (∃ (V : set R) (H : , V (λ (x : R), x * x₀) ⁻¹' 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
def ring_filter_basis.topology {R : Type u} [ring R] (B : ring_filter_basis R) :

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] [ M] :
Type u_2
• smul' : ∀ {U : set M}, (∃ (V : set R) (H : V nhds 0) (W : set M) (H : , V W U)
• smul_left' : ∀ (x₀ : R) {U : set M}, (∃ (V : set M) (H : , V (λ (x : M), x₀ x) ⁻¹' U)
• smul_right' : ∀ (m₀ : M) {U : set M}, (∀ᶠ (x : R) in nhds 0, x m₀ U)

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
@[protected, instance]
def module_filter_basis.group_filter_basis.has_mem {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] :
has_mem (set M) M)
Equations
theorem module_filter_basis.smul {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (B : 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] [ M] (B : 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] [ M] (B : M) (m₀ : M) {U : set M} (hU : U B) :
∀ᶠ (x : R) in nhds 0, x m₀ U
@[protected, instance]
def module_filter_basis.inhabited {R : Type u_1} {M : Type u_2} [comm_ring R] [ M]  :

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] [ M] (B : 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} [ M] (B : 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] [ M] {ι : Type u_3} {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]
def module_filter_basis.has_continuous_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (B : M)  :

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] [ 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