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) [Group G] extends FilterBasis : Type u

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

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

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

theorem addGroupFilterBasisOfComm.proof_1 {G : Type u_1} [AddCommGroup G] (sets : Set (Set G)) (nonempty : Set.Nonempty sets) (inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z, z ∈ sets ∧ z ⊆ x ∩ y) (x : G) (U : Set G) (U_in : U ∈ { sets := sets, nonempty := nonempty, inter_sets := fun {x y} => inter_sets x y }.sets) : ∃ V, V ∈ { sets := sets, nonempty := nonempty, inter_sets := fun {x y} => inter_sets x y }.sets ∧ V ⊆ (fun x => x + x + -x) ⁻¹' U

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

AddGroupFilterBasis constructor in the additive commutative group case.

Equations

• One or more equations did not get rendered due to their size.

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

GroupFilterBasis constructor in the commutative group case.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• AddGroupFilterBasis.instMembershipSetAddGroupFilterBasis = { mem := fun s f => s ∈ f.sets }

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

Equations

• GroupFilterBasis.instMembershipSetGroupFilterBasis = { mem := fun s f => s ∈ f.sets }

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

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

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

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

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

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

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

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

theorem AddGroupFilterBasis.instInhabitedAddGroupFilterBasis.proof_4 {G : Type u_1} [AddGroup G] {U : Set G} : U ∈ { sets := {{0}}, nonempty := (_ : Set.Nonempty {{0}}), inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{0}} → y ∈ {{0}} → ∃ z, z ∈ {{0}} ∧ z ⊆ x ∩ y) }.sets → ∃ V, V ∈ { sets := {{0}}, nonempty := (_ : Set.Nonempty {{0}}), inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{0}} → y ∈ {{0}} → ∃ z, z ∈ {{0}} ∧ z ⊆ x ∩ y) }.sets ∧ V + V ⊆ U

theorem AddGroupFilterBasis.instInhabitedAddGroupFilterBasis.proof_5 {G : Type u_1} [AddGroup G] {U : Set G} : U ∈ { sets := {{0}}, nonempty := (_ : Set.Nonempty {{0}}), inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{0}} → y ∈ {{0}} → ∃ z, z ∈ {{0}} ∧ z ⊆ x ∩ y) }.sets → ∃ V, V ∈ { sets := {{0}}, nonempty := (_ : Set.Nonempty {{0}}), inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{0}} → y ∈ {{0}} → ∃ z, z ∈ {{0}} ∧ z ⊆ x ∩ y) }.sets ∧ V ⊆ (fun x => -x) ⁻¹' U

theorem AddGroupFilterBasis.instInhabitedAddGroupFilterBasis.proof_3 {G : Type u_1} [AddGroup G] {U : Set G} : U ∈ { sets := {{0}}, nonempty := (_ : Set.Nonempty {{0}}), inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{0}} → y ∈ {{0}} → ∃ z, z ∈ {{0}} ∧ z ⊆ x ∩ y) }.sets → 0 ∈ U

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem AddGroupFilterBasis.instInhabitedAddGroupFilterBasis.proof_2 {G : Type u_1} [AddGroup G] {x : Set G} {y : Set G} : x ∈ {{0}} → y ∈ {{0}} → ∃ z, z ∈ {{0}} ∧ z ⊆ x ∩ y

theorem AddGroupFilterBasis.instInhabitedAddGroupFilterBasis.proof_6 {G : Type u_1} [AddGroup G] (x₀ : G) {U : Set G} : U ∈ { sets := {{0}}, nonempty := (_ : Set.Nonempty {{0}}), inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{0}} → y ∈ {{0}} → ∃ z, z ∈ {{0}} ∧ z ⊆ x ∩ y) }.sets → ∃ V, V ∈ { sets := {{0}}, nonempty := (_ : Set.Nonempty {{0}}), inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{0}} → y ∈ {{0}} → ∃ z, z ∈ {{0}} ∧ z ⊆ x ∩ y) }.sets ∧ V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U

theorem AddGroupFilterBasis.instInhabitedAddGroupFilterBasis.proof_1 {G : Type u_1} [AddGroup G] : Set.Nonempty {{0}}

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

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

Equations

• One or more equations did not get rendered due to their size.

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

theorem GroupFilterBasis.prod_subset_self {G : Type u} [Group G] (B : GroupFilterBasis G) {U : Set G} (h : U ∈ B) : U ⊆ U * U

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

The neighborhood function of an AddGroupFilterBasis.

Equations

• AddGroupFilterBasis.N B x = Filter.map (fun y => x + y) (FilterBasis.filter AddGroupFilterBasis.toFilterBasis)

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

The neighborhood function of a GroupFilterBasis.

Equations

• GroupFilterBasis.N B x = Filter.map (fun y => x * y) (FilterBasis.filter GroupFilterBasis.toFilterBasis)

@[simp]

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

@[simp]

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

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

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

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

• AddGroupFilterBasis.topology B = TopologicalSpace.mkOfNhds (AddGroupFilterBasis.N B)

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

The topological space structure coming from a group filter basis.

Equations

• GroupFilterBasis.topology B = TopologicalSpace.mkOfNhds (GroupFilterBasis.N B)

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

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

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

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

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

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

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

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

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

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

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

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

Equations

• @AddGroupFilterBasis.isTopologicalAddGroup = @AddGroupFilterBasis.isTopologicalAddGroup.proof_1

theorem AddGroupFilterBasis.isTopologicalAddGroup.proof_1 {G : Type u_1} [AddGroup G] (B : AddGroupFilterBasis G) : TopologicalAddGroup G

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

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

Equations

• @GroupFilterBasis.isTopologicalGroup = @GroupFilterBasis.isTopologicalGroup.proof_1

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

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

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

Equations

• RingFilterBasis.instMembershipSetRingFilterBasis = { mem := fun s B => s ∈ B.sets }

theorem RingFilterBasis.mul {R : Type u} [Ring R] (B : RingFilterBasis R) {U : Set R} (hU : U ∈ B) : ∃ V, 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, V ∈ B ∧ V ⊆ (fun x => x₀ * x) ⁻¹' U

theorem RingFilterBasis.mul_right {R : Type u} [Ring R] (B : RingFilterBasis R) (x₀ : R) {U : Set R} (hU : U ∈ B) : ∃ V, V ∈ B ∧ V ⊆ (fun x => 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

• RingFilterBasis.topology B = AddGroupFilterBasis.topology RingFilterBasis.toAddGroupFilterBasis

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

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

Equations

• @RingFilterBasis.isTopologicalRing = @RingFilterBasis.isTopologicalRing.proof_1

structure ModuleFilterBasis (R : Type u_1) (M : Type u_2) [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] extends AddGroupFilterBasis : Type u_2

• sets : Set (Set M)
• nonempty : Set.Nonempty s.sets
• inter_sets : ∀ {x y : Set M}, x ∈ s.sets → y ∈ s.sets → ∃ z, z ∈ s.sets ∧ z ⊆ x ∩ y
• zero' : ∀ {U : Set M}, U ∈ s.sets → 0 ∈ U
• add' : ∀ {U : Set M}, U ∈ s.sets → ∃ V, V ∈ s.sets ∧ V + V ⊆ U
• neg' : ∀ {U : Set M}, U ∈ s.sets → ∃ V, V ∈ s.sets ∧ V ⊆ (fun x => -x) ⁻¹' U
• conj' : ∀ (x₀ : M) {U : Set M}, U ∈ s.sets → ∃ V, V ∈ s.sets ∧ V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U
• smul' : ∀ {U : Set M}, U ∈ s.sets → ∃ V, V ∈ nhds 0 ∧ ∃ W, W ∈ s.sets ∧ V • W ⊆ U
• smul_left' : ∀ (x₀ : R) {U : Set M}, U ∈ s.sets → ∃ V, V ∈ s.sets ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
• smul_right' : ∀ (m₀ : M) {U : Set M}, U ∈ s.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U

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.

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 s B => 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, V ∈ nhds 0 ∧ ∃ W, 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, V ∈ B ∧ V ⊆ (fun x => 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.instInhabitedModuleFilterBasis {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

• ModuleFilterBasis.topology B = AddGroupFilterBasis.topology B.toAddGroupFilterBasis

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

• ModuleFilterBasis.topology' B = AddGroupFilterBasis.topology B.toAddGroupFilterBasis

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} [TopologicalRing R] [TopologicalSpace M] [TopologicalAddGroup M] {p : ι → Prop} {b : ι → Set M} (h : Filter.HasBasis (nhds 0) p b) (hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ nhds 0 ∧ ∃ j x, V • b j ⊆ b i) (hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i) (hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ b i) : ContinuousSMul R M

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 ModuleFilterBasis.continuousSMul {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) [TopologicalRing 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.

Equations

• @ModuleFilterBasis.continuousSMul = @ModuleFilterBasis.continuousSMul.proof_1

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, V ∈ BR ∧ ∃ W, W ∈ BM ∧ V • W ⊆ U) (smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V, V ∈ BM ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U) (smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ V ⊆ (fun x => x • m₀) ⁻¹' U) : ModuleFilterBasis R M

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

Equations

• One or more equations did not get rendered due to their size.