mathlib3 documentation

topology.algebra.filter_basis

Group and ring filter bases #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

N. Bourbaki, General Topology

@[class]

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

to_filter_basis : filter_basis G
one' : ∀ {U : set G}, U ∈ group_filter_basis.to_filter_basis.sets → 1 ∈ U
mul' : ∀ {U : set G}, U ∈ group_filter_basis.to_filter_basis.sets → (∃ (V : set G) (H : V ∈ group_filter_basis.to_filter_basis.sets), V * V ⊆ U)
inv' : ∀ {U : set G}, U ∈ group_filter_basis.to_filter_basis.sets → (∃ (V : set G) (H : V ∈ group_filter_basis.to_filter_basis.sets), V ⊆ (λ (x : G), x⁻¹) ⁻¹' U)
conj' : ∀ (x₀ : G) {U : set G}, U ∈ group_filter_basis.to_filter_basis.sets → (∃ (V : set G) (H : V ∈ group_filter_basis.to_filter_basis.sets), 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

group_filter_basis.has_sizeof_inst
group_filter_basis.has_mem
group_filter_basis.inhabited

@[class]

structure add_group_filter_basis (A : Type u) [add_group A] :

to_filter_basis : filter_basis A
zero' : ∀ {U : set A}, U ∈ add_group_filter_basis.to_filter_basis.sets → 0 ∈ U
add' : ∀ {U : set A}, U ∈ add_group_filter_basis.to_filter_basis.sets → (∃ (V : set A) (H : V ∈ add_group_filter_basis.to_filter_basis.sets), V + V ⊆ U)
neg' : ∀ {U : set A}, U ∈ add_group_filter_basis.to_filter_basis.sets → (∃ (V : set A) (H : V ∈ add_group_filter_basis.to_filter_basis.sets), V ⊆ (λ (x : A), -x) ⁻¹' U)
conj' : ∀ (x₀ : A) {U : set A}, U ∈ add_group_filter_basis.to_filter_basis.sets → (∃ (V : set A) (H : V ∈ add_group_filter_basis.to_filter_basis.sets), 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

ring_filter_basis.to_add_group_filter_basis

Instances of other typeclasses for add_group_filter_basis

add_group_filter_basis.has_sizeof_inst
add_group_filter_basis.has_mem
add_group_filter_basis.inhabited

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 ∈ sets → y ∈ sets → (∃ (z : set G) (H : z ∈ sets), z ⊆ x ∩ y)) (one : ∀ (U : set G), U ∈ sets → 0 ∈ 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 G

add_group_filter_basis constructor in the additive commutative group case.

Equations

add_group_filter_basis_of_comm sets nonempty inter_sets one mul inv = {to_filter_basis := {sets := sets, nonempty := nonempty, inter_sets := inter_sets}, zero' := one, add' := mul, neg' := inv, conj' := _}

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 ∈ sets → y ∈ sets → (∃ (z : set G) (H : z ∈ sets), z ⊆ x ∩ y)) (one : ∀ (U : set G), U ∈ sets → 1 ∈ 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 G

group_filter_basis constructor in the commutative group case.

Equations

group_filter_basis_of_comm sets nonempty inter_sets one mul inv = {to_filter_basis := {sets := sets, nonempty := nonempty, inter_sets := inter_sets}, one' := one, mul' := mul, inv' := inv, conj' := _}

@[protected, instance]

def add_group_filter_basis.has_mem {G : Type u} [add_group G] :

has_mem (set G) (add_group_filter_basis G)

Equations

add_group_filter_basis.has_mem = {mem := λ (s : set G) (f : add_group_filter_basis G), s ∈ add_group_filter_basis.to_filter_basis.sets}

@[protected, instance]

def group_filter_basis.has_mem {G : Type u} [group G] :

has_mem (set G) (group_filter_basis G)

Equations

group_filter_basis.has_mem = {mem := λ (s : set G) (f : group_filter_basis G), s ∈ group_filter_basis.to_filter_basis.sets}

theorem add_group_filter_basis.zero {G : Type u} [add_group G] {B : add_group_filter_basis G} {U : set G} :

U ∈ B → 0 ∈ U

theorem group_filter_basis.one {G : Type u} [group G] {B : group_filter_basis G} {U : set G} :

U ∈ B → 1 ∈ 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]

def group_filter_basis.inhabited {G : Type u} [group G] :

inhabited (group_filter_basis G)

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

Equations

group_filter_basis.inhabited = {default := {to_filter_basis := {sets := {{1}}, nonempty := _, inter_sets := _}, one' := _, mul' := _, inv' := _, conj' := _}}

@[protected, instance]

def add_group_filter_basis.inhabited {G : Type u} [add_group G] :

inhabited (add_group_filter_basis G)

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

Equations

add_group_filter_basis.inhabited = {default := {to_filter_basis := {sets := {{0}}, nonempty := _, inter_sets := _}, zero' := _, add' := _, neg' := _, conj' := _}}

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) :

The neighborhood function of a add_group_filter_basis

Equations

B.N = λ (x : G), filter.map (λ (y : G), x + y) add_group_filter_basis.to_filter_basis.filter

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

The neighborhood function of a group_filter_basis

Equations

B.N = λ (x : G), filter.map (λ (y : G), x * y) group_filter_basis.to_filter_basis.filter

@[simp]

theorem group_filter_basis.N_one {G : Type u} [group G] (B : group_filter_basis G) :

B.N 1 = group_filter_basis.to_filter_basis.filter

@[simp]

theorem add_group_filter_basis.N_zero {G : Type u} [add_group G] (B : add_group_filter_basis G) :

B.N 0 = add_group_filter_basis.to_filter_basis.filter

@[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)

def group_filter_basis.topology {G : Type u} [group G] (B : group_filter_basis G) :

topological_space G

The topological space structure coming from a group filter basis.

Equations

B.topology = topological_space.mk_of_nhds B.N

def add_group_filter_basis.topology {G : Type u} [add_group G] (B : add_group_filter_basis G) :

topological_space G

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

Equations

B.topology = topological_space.mk_of_nhds B.N

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 group_filter_basis.nhds_one_eq {G : Type u} [group G] (B : group_filter_basis G) :

nhds 1 = group_filter_basis.to_filter_basis.filter

theorem add_group_filter_basis.nhds_zero_eq {G : Type u} [add_group G] (B : add_group_filter_basis G) :

nhds 0 = add_group_filter_basis.to_filter_basis.filter

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) :

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) :

@[protected, instance]

def add_group_filter_basis.is_topological_add_group {G : Type u} [add_group G] (B : add_group_filter_basis G) :

topological_add_group G

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

@[protected, instance]

def group_filter_basis.is_topological_group {G : Type u} [group G] (B : group_filter_basis G) :

topological_group G

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

to_add_group_filter_basis : add_group_filter_basis R
mul' : ∀ {U : set R}, U ∈ add_group_filter_basis.to_filter_basis.sets → (∃ (V : set R) (H : V ∈ add_group_filter_basis.to_filter_basis.sets), V * V ⊆ U)
mul_left' : ∀ (x₀ : R) {U : set R}, U ∈ add_group_filter_basis.to_filter_basis.sets → (∃ (V : set R) (H : V ∈ add_group_filter_basis.to_filter_basis.sets), V ⊆ (λ (x : R), x₀ * x) ⁻¹' U)
mul_right' : ∀ (x₀ : R) {U : set R}, U ∈ add_group_filter_basis.to_filter_basis.sets → (∃ (V : set R) (H : V ∈ add_group_filter_basis.to_filter_basis.sets), 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

ring_filter_basis.has_sizeof_inst
ring_filter_basis.has_mem

@[protected, instance]

def ring_filter_basis.has_mem {R : Type u} [ring R] :

has_mem (set R) (ring_filter_basis R)

Equations

ring_filter_basis.has_mem = {mem := λ (s : set R) (B : ring_filter_basis R), s ∈ add_group_filter_basis.to_filter_basis.sets}

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) :

topological_space R

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

Equations

B.topology = ring_filter_basis.to_add_group_filter_basis.topology

@[protected, instance]

def ring_filter_basis.is_topological_ring {R : Type u} [ring R] (B : ring_filter_basis R) :

topological_ring R

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

to_add_group_filter_basis : add_group_filter_basis M
smul' : ∀ {U : set M}, U ∈ add_group_filter_basis.to_filter_basis.sets → (∃ (V : set R) (H : V ∈ nhds 0) (W : set M) (H : W ∈ add_group_filter_basis.to_filter_basis.sets), V • W ⊆ U)
smul_left' : ∀ (x₀ : R) {U : set M}, U ∈ add_group_filter_basis.to_filter_basis.sets → (∃ (V : set M) (H : V ∈ add_group_filter_basis.to_filter_basis.sets), V ⊆ (λ (x : M), x₀ • x) ⁻¹' U)
smul_right' : ∀ (m₀ : M) {U : set M}, U ∈ add_group_filter_basis.to_filter_basis.sets → (∀ᶠ (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

module_filter_basis.has_sizeof_inst
module_filter_basis.group_filter_basis.has_mem
module_filter_basis.inhabited

@[protected, instance]

def module_filter_basis.group_filter_basis.has_mem {R : Type u_1} {M : Type u_2} [comm_ring R] [topological_space R] [add_comm_group M] [module R M] :

has_mem (set M) (module_filter_basis R M)

Equations

module_filter_basis.group_filter_basis.has_mem = {mem := λ (s : set M) (B : module_filter_basis R M), s ∈ add_group_filter_basis.to_filter_basis.sets}

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]

def module_filter_basis.inhabited {R : Type u_1} {M : Type u_2} [comm_ring R] [topological_space R] [add_comm_group M] [module R M] [discrete_topology R] :

inhabited (module_filter_basis R M)

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

Equations

module_filter_basis.inhabited = {default := {to_add_group_filter_basis := {to_filter_basis := add_group_filter_basis.to_filter_basis (show add_group_filter_basis M, from inhabited.default), zero' := _, add' := _, neg' := _, conj' := _}, smul' := _, smul_left' := _, smul_right' := _}}

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) :

topological_space 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

B.topology = B.to_add_group_filter_basis.topology

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) :

topological_space 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

B.topology' = B.to_add_group_filter_basis.topology

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)) :

has_continuous_smul R M

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] [topological_space R] [add_comm_group M] [module R M] (B : module_filter_basis R M) [topological_ring R] :

has_continuous_smul R 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] [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)) :

module_filter_basis R M

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

Equations

module_filter_basis.of_bases BR BM smul smul_left smul_right = {to_add_group_filter_basis := {to_filter_basis := add_group_filter_basis.to_filter_basis BM, zero' := _, add' := _, neg' := _, conj' := _}, smul' := _, smul_left' := smul_left, smul_right' := _}