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

class GroupFilterBasis (G : Type u) [Group G] extends FilterBasis G : Type u

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 : self.sets.Nonempty
• inter_sets {x y : Set G} : x ∈ self.sets → y ∈ self.sets → ∃ z ∈ self.sets, z ⊆ x ∩ y
• one' {U : Set G} : U ∈ self.sets → 1 ∈ U
• mul' {U : Set G} : U ∈ self.sets → ∃ V ∈ self.sets, V * V ⊆ U
• inv' {U : Set G} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : G) => x⁻¹) ⁻¹' U
• conj' (x₀ : G) {U : Set G} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : G) => x₀ * x * x₀⁻¹) ⁻¹' U

class AddGroupFilterBasis (A : Type u) [AddGroup A] extends FilterBasis A : Type u

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)
• nonempty : self.sets.Nonempty
• inter_sets {x y : Set A} : x ∈ self.sets → y ∈ self.sets → ∃ z ∈ self.sets, z ⊆ x ∩ y
• zero' {U : Set A} : U ∈ self.sets → 0 ∈ U
• add' {U : Set A} : U ∈ self.sets → ∃ V ∈ self.sets, V + V ⊆ U
• neg' {U : Set A} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : A) => -x) ⁻¹' U
• conj' (x₀ : A) {U : Set A} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : A) => x₀ + x + -x₀) ⁻¹' U

def groupFilterBasisOfComm {G : Type u_1} [CommGroup G] (sets : Set (Set G)) (nonempty : sets.Nonempty) (inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) (one : ∀ U ∈ sets, 1 ∈ U) (mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U) (inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun (x : G) => x⁻¹) ⁻¹' U) : GroupFilterBasis G

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

def addGroupFilterBasisOfComm {G : Type u_1} [AddCommGroup G] (sets : Set (Set G)) (nonempty : sets.Nonempty) (inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) (zero : ∀ U ∈ sets, 0 ∈ U) (add : ∀ U ∈ sets, ∃ V ∈ sets, V + V ⊆ U) (neg : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun (x : G) => -x) ⁻¹' U) : AddGroupFilterBasis G

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

instance GroupFilterBasis.instMembershipSet {G : Type u} [Group G] : Membership (Set G) (GroupFilterBasis G)

Equations

• GroupFilterBasis.instMembershipSet = { mem := fun (f : GroupFilterBasis G) (s : Set G) => s ∈ f.sets }

instance AddGroupFilterBasis.instMembershipSet {G : Type u} [AddGroup G] : Membership (Set G) (AddGroupFilterBasis G)

Equations

• AddGroupFilterBasis.instMembershipSet = { mem := fun (f : AddGroupFilterBasis G) (s : Set G) => s ∈ f.sets }

theorem GroupFilterBasis.one {G : Type u} [Group G] {B : GroupFilterBasis G} {U : Set G} : U ∈ B → 1 ∈ U

theorem AddGroupFilterBasis.zero {G : Type u} [AddGroup G] {B : AddGroupFilterBasis G} {U : Set G} : U ∈ B → 0 ∈ U

theorem GroupFilterBasis.mul {G : Type u} [Group G] {B : GroupFilterBasis G} {U : Set G} : U ∈ B → ∃ V ∈ B, V * V ⊆ U

theorem AddGroupFilterBasis.add {G : Type u} [AddGroup G] {B : AddGroupFilterBasis G} {U : Set G} : U ∈ B → ∃ V ∈ B, V + V ⊆ U

theorem GroupFilterBasis.inv {G : Type u} [Group G] {B : GroupFilterBasis G} {U : Set G} : U ∈ B → ∃ V ∈ B, V ⊆ (fun (x : G) => x⁻¹) ⁻¹' U

theorem AddGroupFilterBasis.neg {G : Type u} [AddGroup G] {B : AddGroupFilterBasis G} {U : Set G} : U ∈ B → ∃ V ∈ B, V ⊆ (fun (x : G) => -x) ⁻¹' U

theorem GroupFilterBasis.conj {G : Type u} [Group G] {B : GroupFilterBasis G} (x₀ : G) {U : Set G} : U ∈ B → ∃ V ∈ B, V ⊆ (fun (x : G) => x₀ * x * x₀⁻¹) ⁻¹' U

theorem AddGroupFilterBasis.conj {G : Type u} [AddGroup G] {B : AddGroupFilterBasis G} (x₀ : G) {U : Set G} : U ∈ B → ∃ V ∈ B, V ⊆ (fun (x : G) => x₀ + x + -x₀) ⁻¹' U

instance GroupFilterBasis.instInhabited {G : Type u} [Group G] : Inhabited (GroupFilterBasis G)

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

instance AddGroupFilterBasis.instInhabited {G : Type u} [AddGroup G] : Inhabited (AddGroupFilterBasis G)

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 GroupFilterBasis.subset_mul_self {G : Type u} [Group G] (B : GroupFilterBasis G) {U : Set G} (h : U ∈ B) : U ⊆ U * U

theorem AddGroupFilterBasis.subset_add_self {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) {U : Set G} (h : U ∈ B) : U ⊆ U + U

def GroupFilterBasis.N {G : Type u} [Group G] (B : GroupFilterBasis G) : G → Filter G

The neighborhood function of a GroupFilterBasis.

Equations

• B.N x = Filter.map (fun (y : G) => x * y) B.filter

def AddGroupFilterBasis.N {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) : G → Filter G

The neighborhood function of an AddGroupFilterBasis.

Equations

• B.N x = Filter.map (fun (y : G) => x + y) B.filter

@[simp]

theorem GroupFilterBasis.N_one {G : Type u} [Group G] (B : GroupFilterBasis G) : B.N 1 = B.filter

@[simp]

theorem AddGroupFilterBasis.N_zero {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) : B.N 0 = B.filter

theorem GroupFilterBasis.hasBasis {G : Type u} [Group G] (B : GroupFilterBasis G) (x : G) : (B.N x).HasBasis (fun (V : Set G) => V ∈ B) fun (V : Set G) => (fun (y : G) => x * y) '' V

theorem AddGroupFilterBasis.hasBasis {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) (x : G) : (B.N x).HasBasis (fun (V : Set G) => V ∈ B) fun (V : Set G) => (fun (y : G) => x + y) '' V

def GroupFilterBasis.topology {G : Type u} [Group G] (B : GroupFilterBasis G) : TopologicalSpace G

The topological space structure coming from a group filter basis.

Equations

• B.topology = TopologicalSpace.mkOfNhds B.N

def AddGroupFilterBasis.topology {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) : TopologicalSpace G

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

Equations

• B.topology = TopologicalSpace.mkOfNhds B.N

theorem GroupFilterBasis.nhds_eq {G : Type u} [Group G] (B : GroupFilterBasis G) {x₀ : G} : nhds x₀ = B.N x₀

theorem AddGroupFilterBasis.nhds_eq {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) {x₀ : G} : nhds x₀ = B.N x₀

theorem GroupFilterBasis.nhds_one_eq {G : Type u} [Group G] (B : GroupFilterBasis G) : nhds 1 = B.filter

theorem AddGroupFilterBasis.nhds_zero_eq {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) : nhds 0 = B.filter

theorem GroupFilterBasis.nhds_hasBasis {G : Type u} [Group G] (B : GroupFilterBasis G) (x₀ : G) : (nhds x₀).HasBasis (fun (V : Set G) => V ∈ B) fun (V : Set G) => (fun (y : G) => x₀ * y) '' V

theorem AddGroupFilterBasis.nhds_hasBasis {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) (x₀ : G) : (nhds x₀).HasBasis (fun (V : Set G) => V ∈ B) fun (V : Set G) => (fun (y : G) => x₀ + y) '' V

theorem GroupFilterBasis.nhds_one_hasBasis {G : Type u} [Group G] (B : GroupFilterBasis G) : (nhds 1).HasBasis (fun (V : Set G) => V ∈ B) id

theorem AddGroupFilterBasis.nhds_zero_hasBasis {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) : (nhds 0).HasBasis (fun (V : Set G) => V ∈ B) id

theorem GroupFilterBasis.mem_nhds_one {G : Type u} [Group G] (B : GroupFilterBasis G) {U : Set G} (hU : U ∈ B) : U ∈ nhds 1

theorem AddGroupFilterBasis.mem_nhds_zero {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) {U : Set G} (hU : U ∈ B) : U ∈ nhds 0

@[instance 100]

instance GroupFilterBasis.isTopologicalGroup {G : Type u} [Group G] (B : GroupFilterBasis G) : IsTopologicalGroup G

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

@[instance 100]

instance AddGroupFilterBasis.isTopologicalAddGroup {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) : IsTopologicalAddGroup G

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

class RingFilterBasis (R : Type u) [Ring R] extends AddGroupFilterBasis R : Type u

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)
• nonempty : self.sets.Nonempty
• inter_sets {x y : Set R} : x ∈ self.sets → y ∈ self.sets → ∃ z ∈ self.sets, z ⊆ x ∩ y
• zero' {U : Set R} : U ∈ self.sets → 0 ∈ U
• add' {U : Set R} : U ∈ self.sets → ∃ V ∈ self.sets, V + V ⊆ U
• neg' {U : Set R} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : R) => -x) ⁻¹' U
• conj' (x₀ : R) {U : Set R} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : R) => x₀ + x + -x₀) ⁻¹' U
• mul' {U : Set R} : U ∈ self.sets → ∃ V ∈ self.sets, V * V ⊆ U
• mul_left' (x₀ : R) {U : Set R} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : R) => x₀ * x) ⁻¹' U
• mul_right' (x₀ : R) {U : Set R} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : R) => x * x₀) ⁻¹' U

instance RingFilterBasis.instMembershipSet {R : Type u} [Ring R] : Membership (Set R) (RingFilterBasis R)

Equations

• RingFilterBasis.instMembershipSet = { mem := fun (B : RingFilterBasis R) (s : Set R) => s ∈ B.sets }

theorem RingFilterBasis.mul {R : Type u} [Ring R] (B : RingFilterBasis R) {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V * V ⊆ U

theorem RingFilterBasis.mul_left {R : Type u} [Ring R] (B : RingFilterBasis R) (x₀ : R) {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun (x : R) => x₀ * x) ⁻¹' U

theorem RingFilterBasis.mul_right {R : Type u} [Ring R] (B : RingFilterBasis R) (x₀ : R) {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun (x : R) => x * x₀) ⁻¹' U

def RingFilterBasis.topology {R : Type u} [Ring R] (B : RingFilterBasis R) : TopologicalSpace R

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

Equations

• B.topology = B.topology

@[instance 100]

instance RingFilterBasis.isTopologicalRing {R : Type u} [Ring R] (B : RingFilterBasis R) : IsTopologicalRing R

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

structure ModuleFilterBasis (R : Type u_1) (M : Type u_2) [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] extends AddGroupFilterBasis M : 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)
• nonempty : self.sets.Nonempty
• inter_sets {x y : Set M} : x ∈ self.sets → y ∈ self.sets → ∃ z ∈ self.sets, z ⊆ x ∩ y
• zero' {U : Set M} : U ∈ self.sets → 0 ∈ U
• add' {U : Set M} : U ∈ self.sets → ∃ V ∈ self.sets, V + V ⊆ U
• neg' {U : Set M} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : M) => -x) ⁻¹' U
• conj' (x₀ : M) {U : Set M} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : M) => x₀ + x + -x₀) ⁻¹' U
• smul' {U : Set M} : U ∈ self.sets → ∃ V ∈ nhds 0, ∃ W ∈ self.sets, V • W ⊆ U
• smul_left' (x₀ : R) {U : Set M} : U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun (x : M) => x₀ • x) ⁻¹' U
• smul_right' (m₀ : M) {U : Set M} : U ∈ self.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U

instance ModuleFilterBasis.GroupFilterBasis.hasMem {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] : Membership (Set M) (ModuleFilterBasis R M)

Equations

• ModuleFilterBasis.GroupFilterBasis.hasMem = { mem := fun (B : ModuleFilterBasis R M) (s : Set M) => s ∈ B.sets }

theorem ModuleFilterBasis.smul {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) {U : Set M} (hU : U ∈ B) : ∃ V ∈ nhds 0, ∃ W ∈ B, V • W ⊆ U

theorem ModuleFilterBasis.smul_left {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) (x₀ : R) {U : Set M} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun (x : M) => x₀ • x) ⁻¹' U

theorem ModuleFilterBasis.smul_right {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) (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} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [DiscreteTopology R] : Inhabited (ModuleFilterBasis 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} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) : TopologicalSpace 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.topology

def ModuleFilterBasis.topology' {R : Type u_3} {M : Type u_4} [CommRing R] {x✝ : TopologicalSpace R} [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) : TopologicalSpace 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

theorem ContinuousSMul.of_basis_zero {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] {ι : Type u_3} [IsTopologicalRing R] [TopologicalSpace M] [IsTopologicalAddGroup M] {p : ι → Prop} {b : ι → Set M} (h : (nhds 0).HasBasis p b) (hsmul : ∀ {i : ι}, p i → ∃ V ∈ nhds 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) : ContinuousSMul R M

A topological additive 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} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) [IsTopologicalRing R] : ContinuousSMul R M

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

def ModuleFilterBasis.ofBases {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (BR : RingFilterBasis R) (BM : AddGroupFilterBasis M) (smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U) (smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun (x : M) => x₀ • x) ⁻¹' U) (smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun (x : R) => x • m₀) ⁻¹' U) : ModuleFilterBasis R M

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

Equations

• ModuleFilterBasis.ofBases BR BM smul smul_left smul_right = { toAddGroupFilterBasis := BM, smul' := ⋯, smul_left' := smul_left, smul_right' := ⋯ }