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 #

N. Bourbaki, General Topology

source

@[class]

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

Type u

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.

source

@[class]

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

Type u

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

ring_filter_basis.to_add_group_filter_basis

source

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 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' := _}

source

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' := _}

source

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

source

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

source

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

source

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

U ∈ B → 1 ∈ U

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

@[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' := _}}

source

@[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' := _}}

source

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

source

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

source

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

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

source

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

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

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem add_group_filter_basis.nhds_eq {G : Type u} [add_group G] (B : add_group_filter_basis G) {x₀ : G} :

𝓝 x₀ = B.N x₀

source

theorem group_filter_basis.nhds_eq {G : Type u} [group G] (B : group_filter_basis G) {x₀ : G} :

𝓝 x₀ = B.N x₀

source

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

𝓝 1 = group_filter_basis.to_filter_basis.filter

source

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

𝓝 0 = add_group_filter_basis.to_filter_basis.filter

source

theorem add_group_filter_basis.nhds_has_basis {G : Type u} [add_group G] (B : add_group_filter_basis G) (x₀ : G) :

(𝓝 x₀).has_basis (λ (V : set G), V ∈ B) (λ (V : set G), (λ (y : G), x₀ + y) '' V)

source

theorem group_filter_basis.nhds_has_basis {G : Type u} [group G] (B : group_filter_basis G) (x₀ : G) :

(𝓝 x₀).has_basis (λ (V : set G), V ∈ B) (λ (V : set G), (λ (y : G), x₀ * y) '' V)

source

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

(𝓝 0).has_basis (λ (V : set G), V ∈ B) id

source

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

(𝓝 1).has_basis (λ (V : set G), V ∈ B) id

source

theorem group_filter_basis.mem_nhds_one {G : Type u} [group G] (B : group_filter_basis G) {U : set G} (hU : U ∈ B) :

U ∈ 𝓝 1

source

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 ∈ 𝓝 0

source

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

source

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

source

@[class]

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

Type u

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.

source

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

source

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

source

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

source

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

source

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

source

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

source

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 ∈ 𝓝 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 𝓝 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.

source

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

source

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 ∈ 𝓝 0) (W : set M) (H : W ∈ B), V • W ⊆ U

source

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

source

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 𝓝 0, x • m₀ ∈ U

source

@[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 default), zero' := _, add' := _, neg' := _, conj' := _}, smul' := _, smul_left' := _, smul_right' := _}}

source

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

source

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

source

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

source

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' := _}