# Group and ring filter bases #

A GroupFilterBasis is a FilterBasis on a group with some properties relating the basis to the group structure. The main theorem is that a GroupFilterBasis 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:

• GroupFilterBasis G: the type of filter bases that will become neighborhood of 1 for a topology on G compatible with the group structure
• GroupFilterBasis.topology: the associated topology
• GroupFilterBasis.isTopologicalGroup: the compatibility between the above topology and the group structure
• RingFilterBasis R: the type of filter bases that will become neighborhood of 0 for a topology on R compatible with the ring structure
• RingFilterBasis.topology: the associated topology
• RingFilterBasis.isTopologicalRing: the compatibility between the above topology and the ring structure

## References #

• [N. Bourbaki, General Topology][bourbaki1966]
class GroupFilterBasis (G : Type u) [] extends :

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

• sets : Set (Set G)
• nonempty : GroupFilterBasis.toFilterBasis.sets.Nonempty
• inter_sets : ∀ {x y : Set G}, x GroupFilterBasis.toFilterBasis.setsy GroupFilterBasis.toFilterBasis.setszGroupFilterBasis.toFilterBasis.sets, z x y
• one' : ∀ {U : Set G}, U GroupFilterBasis.toFilterBasis.sets1 U
• mul' : ∀ {U : Set G}, U GroupFilterBasis.toFilterBasis.setsVGroupFilterBasis.toFilterBasis.sets, V * V U
• inv' : ∀ {U : Set G}, U GroupFilterBasis.toFilterBasis.setsVGroupFilterBasis.toFilterBasis.sets, V (fun (x : G) => x⁻¹) ⁻¹' U
• conj' : ∀ (x₀ : G) {U : Set G}, U GroupFilterBasis.toFilterBasis.setsVGroupFilterBasis.toFilterBasis.sets, V (fun (x : G) => x₀ * x * x₀⁻¹) ⁻¹' U
Instances
theorem GroupFilterBasis.one' {G : Type u} [] [self : ] {U : Set G} :
U GroupFilterBasis.toFilterBasis.sets1 U
theorem GroupFilterBasis.mul' {G : Type u} [] [self : ] {U : Set G} :
U GroupFilterBasis.toFilterBasis.setsVGroupFilterBasis.toFilterBasis.sets, V * V U
theorem GroupFilterBasis.inv' {G : Type u} [] [self : ] {U : Set G} :
U GroupFilterBasis.toFilterBasis.setsVGroupFilterBasis.toFilterBasis.sets, V (fun (x : G) => x⁻¹) ⁻¹' U
theorem GroupFilterBasis.conj' {G : Type u} [] [self : ] (x₀ : G) {U : Set G} :
U GroupFilterBasis.toFilterBasis.setsVGroupFilterBasis.toFilterBasis.sets, V (fun (x : G) => x₀ * x * x₀⁻¹) ⁻¹' U
class AddGroupFilterBasis (A : Type u) [] extends :

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

• sets : Set (Set A)
• zero' : ∀ {U : Set A}, U AddGroupFilterBasis.toFilterBasis.sets0 U
• neg' : ∀ {U : Set A}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : A) => -x) ⁻¹' U
• conj' : ∀ (x₀ : A) {U : Set A}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : A) => x₀ + x + -x₀) ⁻¹' U
Instances
theorem AddGroupFilterBasis.zero' {A : Type u} [] [self : ] {U : Set A} :
theorem AddGroupFilterBasis.add' {A : Type u} [] [self : ] {U : Set A} :
theorem AddGroupFilterBasis.neg' {A : Type u} [] [self : ] {U : Set A} :
theorem AddGroupFilterBasis.conj' {A : Type u} [] [self : ] (x₀ : A) {U : Set A} :
U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : A) => x₀ + x + -x₀) ⁻¹' U
theorem addGroupFilterBasisOfComm.proof_1 {G : Type u_1} [] (sets : Set (Set G)) (nonempty : sets.Nonempty) (inter_sets : ∀ (x y : Set G), x setsy setszsets, z x y) (x : G) (U : Set G) (U_in : U { sets := sets, nonempty := nonempty, inter_sets := }.sets) :
V{ sets := sets, nonempty := nonempty, inter_sets := }.sets, V (fun (x_1 : G) => x + x_1 + -x) ⁻¹' U
def addGroupFilterBasisOfComm {G : Type u_1} [] (sets : Set (Set G)) (nonempty : sets.Nonempty) (inter_sets : ∀ (x y : Set G), x setsy setszsets, z x y) (one : Usets, 0 U) (mul : Usets, Vsets, V + V U) (inv : Usets, Vsets, V (fun (x : G) => -x) ⁻¹' U) :

AddGroupFilterBasis constructor in the additive commutative group case.

Equations
• addGroupFilterBasisOfComm sets nonempty inter_sets one mul inv = { sets := sets, nonempty := nonempty, inter_sets := , zero' := , add' := , neg' := , conj' := }
Instances For
def groupFilterBasisOfComm {G : Type u_1} [] (sets : Set (Set G)) (nonempty : sets.Nonempty) (inter_sets : ∀ (x y : Set G), x setsy setszsets, z x y) (one : Usets, 1 U) (mul : Usets, Vsets, V * V U) (inv : Usets, Vsets, V (fun (x : G) => x⁻¹) ⁻¹' U) :

GroupFilterBasis constructor in the commutative group case.

Equations
• groupFilterBasisOfComm sets nonempty inter_sets one mul inv = { sets := sets, nonempty := nonempty, inter_sets := , one' := , mul' := , inv' := , conj' := }
Instances For
Equations
• AddGroupFilterBasis.instMembershipSet = { mem := fun (s : Set G) (f : ) => s AddGroupFilterBasis.toFilterBasis.sets }
Equations
• GroupFilterBasis.instMembershipSet = { mem := fun (s : Set G) (f : ) => s GroupFilterBasis.toFilterBasis.sets }
theorem AddGroupFilterBasis.zero {G : Type u} [] {B : } {U : Set G} :
U B0 U
theorem GroupFilterBasis.one {G : Type u} [] {B : } {U : Set G} :
U B1 U
theorem AddGroupFilterBasis.add {G : Type u} [] {B : } {U : Set G} :
U BVB, V + V U
theorem GroupFilterBasis.mul {G : Type u} [] {B : } {U : Set G} :
U BVB, V * V U
theorem AddGroupFilterBasis.neg {G : Type u} [] {B : } {U : Set G} :
U BVB, V (fun (x : G) => -x) ⁻¹' U
theorem GroupFilterBasis.inv {G : Type u} [] {B : } {U : Set G} :
U BVB, V (fun (x : G) => x⁻¹) ⁻¹' U
theorem AddGroupFilterBasis.conj {G : Type u} [] {B : } (x₀ : G) {U : Set G} :
U BVB, V (fun (x : G) => x₀ + x + -x₀) ⁻¹' U
theorem GroupFilterBasis.conj {G : Type u} [] {B : } (x₀ : G) {U : Set G} :
U BVB, V (fun (x : G) => x₀ * x * x₀⁻¹) ⁻¹' U
theorem AddGroupFilterBasis.instInhabited.proof_3 {G : Type u_1} [] (a : Set G) :
a {{0}}0 a
theorem AddGroupFilterBasis.instInhabited.proof_2 {G : Type u_1} [] (a : Set G) (a : Set G) :
a✝ {{0}}a {{0}}x{{0}}, x a✝ a
theorem AddGroupFilterBasis.instInhabited.proof_1 {G : Type u_1} [] :
{{0}}.Nonempty

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

Equations
• AddGroupFilterBasis.instInhabited = { default := { sets := {{0}}, nonempty := , inter_sets := , zero' := , add' := , neg' := , conj' := } }
theorem AddGroupFilterBasis.instInhabited.proof_4 {G : Type u_1} [] (a : Set G) :
a {{0}}x{{0}}, x + x a
theorem AddGroupFilterBasis.instInhabited.proof_6 {G : Type u_1} [] (a : G) (a : Set G) :
a {{0}}x{{0}}, x (fun (x : G) => a✝ + x + -a✝) ⁻¹' a
theorem AddGroupFilterBasis.instInhabited.proof_5 {G : Type u_1} [] (a : Set G) :
a {{0}}x{{0}}, x -a
instance GroupFilterBasis.instInhabited {G : Type u} [] :

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

Equations
• GroupFilterBasis.instInhabited = { default := { sets := {{1}}, nonempty := , inter_sets := , one' := , mul' := , inv' := , conj' := } }
theorem AddGroupFilterBasis.subset_add_self {G : Type u} [] (B : ) {U : Set G} (h : U B) :
U U + U
theorem GroupFilterBasis.subset_mul_self {G : Type u} [] (B : ) {U : Set G} (h : U B) :
U U * U
def AddGroupFilterBasis.N {G : Type u} [] (B : ) :
G

The neighborhood function of an AddGroupFilterBasis.

Equations
• B.N x = Filter.map (fun (y : G) => x + y) AddGroupFilterBasis.toFilterBasis.filter
Instances For
def GroupFilterBasis.N {G : Type u} [] (B : ) :
G

The neighborhood function of a GroupFilterBasis.

Equations
• B.N x = Filter.map (fun (y : G) => x * y) GroupFilterBasis.toFilterBasis.filter
Instances For
@[simp]
theorem AddGroupFilterBasis.N_zero {G : Type u} [] (B : ) :
@[simp]
theorem GroupFilterBasis.N_one {G : Type u} [] (B : ) :
B.N 1 = GroupFilterBasis.toFilterBasis.filter
theorem AddGroupFilterBasis.hasBasis {G : Type u} [] (B : ) (x : G) :
(B.N x).HasBasis (fun (V : Set G) => V B) fun (V : Set G) => (fun (y : G) => x + y) '' V
theorem GroupFilterBasis.hasBasis {G : Type u} [] (B : ) (x : G) :
(B.N x).HasBasis (fun (V : Set G) => V B) fun (V : Set G) => (fun (y : G) => x * y) '' V
def AddGroupFilterBasis.topology {G : Type u} [] (B : ) :

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

Equations
• B.topology =
Instances For
def GroupFilterBasis.topology {G : Type u} [] (B : ) :

The topological space structure coming from a group filter basis.

Equations
• B.topology =
Instances For
theorem AddGroupFilterBasis.nhds_eq {G : Type u} [] (B : ) {x₀ : G} :
nhds x₀ = B.N x₀
theorem GroupFilterBasis.nhds_eq {G : Type u} [] (B : ) {x₀ : G} :
nhds x₀ = B.N x₀
theorem AddGroupFilterBasis.nhds_zero_eq {G : Type u} [] (B : ) :
theorem GroupFilterBasis.nhds_one_eq {G : Type u} [] (B : ) :
nhds 1 = GroupFilterBasis.toFilterBasis.filter
theorem AddGroupFilterBasis.nhds_hasBasis {G : Type u} [] (B : ) (x₀ : G) :
(nhds x₀).HasBasis (fun (V : Set G) => V B) fun (V : Set G) => (fun (y : G) => x₀ + y) '' V
theorem GroupFilterBasis.nhds_hasBasis {G : Type u} [] (B : ) (x₀ : G) :
(nhds x₀).HasBasis (fun (V : Set G) => V B) fun (V : Set G) => (fun (y : G) => x₀ * y) '' V
theorem AddGroupFilterBasis.nhds_zero_hasBasis {G : Type u} [] (B : ) :
(nhds 0).HasBasis (fun (V : Set G) => V B) id
theorem GroupFilterBasis.nhds_one_hasBasis {G : Type u} [] (B : ) :
(nhds 1).HasBasis (fun (V : Set G) => V B) id
theorem AddGroupFilterBasis.mem_nhds_zero {G : Type u} [] (B : ) {U : Set G} (hU : U B) :
U nhds 0
theorem GroupFilterBasis.mem_nhds_one {G : Type u} [] (B : ) {U : Set G} (hU : U B) :
U nhds 1
@[instance 100]

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

Equations
• =
@[instance 100]
instance GroupFilterBasis.isTopologicalGroup {G : Type u} [] (B : ) :

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

Equations
• =
class RingFilterBasis (R : Type u) [Ring R] extends :

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

• sets : Set (Set R)
• zero' : ∀ {U : Set R}, U AddGroupFilterBasis.toFilterBasis.sets0 U
• neg' : ∀ {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : R) => -x) ⁻¹' U
• conj' : ∀ (x₀ : R) {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : R) => x₀ + x + -x₀) ⁻¹' U
• mul' : ∀ {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V * V U
• mul_left' : ∀ (x₀ : R) {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : R) => x₀ * x) ⁻¹' U
• mul_right' : ∀ (x₀ : R) {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : R) => x * x₀) ⁻¹' U
Instances
theorem RingFilterBasis.mul' {R : Type u} [Ring R] [self : ] {U : Set R} :
theorem RingFilterBasis.mul_left' {R : Type u} [Ring R] [self : ] (x₀ : R) {U : Set R} :
U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : R) => x₀ * x) ⁻¹' U
theorem RingFilterBasis.mul_right' {R : Type u} [Ring R] [self : ] (x₀ : R) {U : Set R} :
U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : R) => x * x₀) ⁻¹' U
Equations
• RingFilterBasis.instMembershipSet = { mem := fun (s : Set R) (B : ) => s AddGroupFilterBasis.toFilterBasis.sets }
theorem RingFilterBasis.mul {R : Type u} [Ring R] (B : ) {U : Set R} (hU : U B) :
VB, V * V U
theorem RingFilterBasis.mul_left {R : Type u} [Ring R] (B : ) (x₀ : R) {U : Set R} (hU : U B) :
VB, V (fun (x : R) => x₀ * x) ⁻¹' U
theorem RingFilterBasis.mul_right {R : Type u} [Ring R] (B : ) (x₀ : R) {U : Set R} (hU : U B) :
VB, V (fun (x : R) => x * x₀) ⁻¹' U
def RingFilterBasis.topology {R : Type u} [Ring R] (B : ) :

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

Equations
Instances For
@[instance 100]
instance RingFilterBasis.isTopologicalRing {R : Type u} [Ring R] (B : ) :

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

Equations
• =
structure ModuleFilterBasis (R : Type u_1) (M : Type u_2) [] [] [] [Module R M] extends :
Type u_2

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

• sets : Set (Set M)
• zero' : ∀ {U : Set M}, U AddGroupFilterBasis.toFilterBasis.sets0 U
• neg' : ∀ {U : Set M}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : M) => -x) ⁻¹' U
• conj' : ∀ (x₀ : M) {U : Set M}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : M) => x₀ + x + -x₀) ⁻¹' U
• smul' : ∀ {U : Set M}, U AddGroupFilterBasis.toFilterBasis.setsVnhds 0, WAddGroupFilterBasis.toFilterBasis.sets, V W U
• smul_left' : ∀ (x₀ : R) {U : Set M}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : M) => x₀ x) ⁻¹' U
• smul_right' : ∀ (m₀ : M) {U : Set M}, U AddGroupFilterBasis.toFilterBasis.sets∀ᶠ (x : R) in nhds 0, x m₀ U
Instances For
theorem ModuleFilterBasis.smul' {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] (self : ) {U : Set M} :
theorem ModuleFilterBasis.smul_left' {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] (self : ) (x₀ : R) {U : Set M} :
U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : M) => x₀ x) ⁻¹' U
theorem ModuleFilterBasis.smul_right' {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] (self : ) (m₀ : M) {U : Set M} :
U AddGroupFilterBasis.toFilterBasis.sets∀ᶠ (x : R) in nhds 0, x m₀ U
instance ModuleFilterBasis.GroupFilterBasis.hasMem {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] :
Equations
• ModuleFilterBasis.GroupFilterBasis.hasMem = { mem := fun (s : Set M) (B : ) => s AddGroupFilterBasis.toFilterBasis.sets }
theorem ModuleFilterBasis.smul {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] (B : ) {U : Set M} (hU : U B) :
Vnhds 0, WB, V W U
theorem ModuleFilterBasis.smul_left {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] (B : ) (x₀ : R) {U : Set M} (hU : U B) :
VB, V (fun (x : M) => x₀ x) ⁻¹' U
theorem ModuleFilterBasis.smul_right {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] (B : ) (m₀ : M) {U : Set M} (hU : U B) :
∀ᶠ (x : R) in nhds 0, x m₀ U
instance ModuleFilterBasis.instInhabitedOfDiscreteTopology {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] [] :

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

Equations
• One or more equations did not get rendered due to their size.
def ModuleFilterBasis.topology {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] (B : ) :

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.topology
Instances For
def ModuleFilterBasis.topology' {R : Type u_3} {M : Type u_4} [] :
{x : } → [inst : ] → [inst_1 : Module 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
• B.topology' = B.topology
Instances For
theorem ContinuousSMul.of_basis_zero {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] {ι : Type u_3} [] [] {p : ιProp} {b : ιSet M} (h : (nhds 0).HasBasis p b) (hsmul : ∀ {i : ι}, p iVnhds 0, ∃ (j : ι), p j V b j b i) (hsmul_left : ∀ (x₀ : R) {i : ι}, p i∃ (j : ι), p j Set.MapsTo (fun (x : M) => x₀ x) (b j) (b i)) (hsmul_right : ∀ (m₀ : M) {i : ι}, p i∀ᶠ (x : R) in nhds 0, x m₀ b i) :

A topological add group with a basis of 𝓝 0 satisfying the axioms of ModuleFilterBasis is a topological module.

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

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

@[instance 100]
instance ModuleFilterBasis.continuousSMul {R : Type u_1} {M : Type u_2} [] [] [] [Module R M] (B : ) [] :

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

Equations
• =
def ModuleFilterBasis.ofBases {R : Type u_3} {M : Type u_4} [] [] [Module R M] (BR : ) (BM : ) (smul : ∀ {U : Set M}, U BMVBR, WBM, V W U) (smul_left : ∀ (x₀ : R) {U : Set M}, U BMVBM, V (fun (x : M) => x₀ x) ⁻¹' U) (smul_right : ∀ (m₀ : M) {U : Set M}, U BMVBR, V (fun (x : R) => x m₀) ⁻¹' U) :

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

Equations
• ModuleFilterBasis.ofBases BR BM smul smul_left smul_right = let x := BR.topology; { toAddGroupFilterBasis := BM, smul' := , smul_left' := smul_left, smul_right' := }
Instances For