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

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

theorem GroupFilterBasis.one' {G : Type u} : ∀ {inst : Group G} [self : GroupFilterBasis G] {U : Set G}, U ∈ GroupFilterBasis.toFilterBasis.sets → 1 ∈ U

theorem GroupFilterBasis.mul' {G : Type u} : ∀ {inst : Group G} [self : GroupFilterBasis G] {U : Set G}, U ∈ GroupFilterBasis.toFilterBasis.sets → ∃ V ∈ GroupFilterBasis.toFilterBasis.sets, V * V ⊆ U

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

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

class AddGroupFilterBasis (A : Type u) [AddGroup A] extends FilterBasis : 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 : AddGroupFilterBasis.toFilterBasis.sets.Nonempty
• inter_sets : ∀ {x y : Set A}, x ∈ AddGroupFilterBasis.toFilterBasis.sets → y ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ z ∈ AddGroupFilterBasis.toFilterBasis.sets, z ⊆ x ∩ y
• zero' : ∀ {U : Set A}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → 0 ∈ U
• add' : ∀ {U : Set A}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V + V ⊆ U
• neg' : ∀ {U : Set A}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun (x : A) => -x) ⁻¹' U
• conj' : ∀ (x₀ : A) {U : Set A}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun (x : A) => x₀ + x + -x₀) ⁻¹' U

theorem AddGroupFilterBasis.zero' {A : Type u} : ∀ {inst : AddGroup A} [self : AddGroupFilterBasis A] {U : Set A}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → 0 ∈ U

theorem AddGroupFilterBasis.add' {A : Type u} : ∀ {inst : AddGroup A} [self : AddGroupFilterBasis A] {U : Set A}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V + V ⊆ U

theorem AddGroupFilterBasis.neg' {A : Type u} : ∀ {inst : AddGroup A} [self : AddGroupFilterBasis A] {U : Set A}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun (x : A) => -x) ⁻¹' U

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

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) (one : ∀ U ∈ sets, 0 ∈ U) (mul : ∀ U ∈ sets, ∃ V ∈ sets, V + V ⊆ U) (inv : ∀ 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' := ⋯ }

theorem addGroupFilterBasisOfComm.proof_1 {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) (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 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' := ⋯ }

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 ∈ AddGroupFilterBasis.toFilterBasis.sets }

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 ∈ GroupFilterBasis.toFilterBasis.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 ∈ B, V + V ⊆ U

theorem GroupFilterBasis.mul {G : Type u} [Group G] {B : GroupFilterBasis G} {U : Set G} : U ∈ B → ∃ V ∈ B, V * V ⊆ 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.inv {G : Type u} [Group G] {B : GroupFilterBasis G} {U : Set G} : U ∈ B → ∃ V ∈ B, V ⊆ (fun (x : G) => 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

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.instInhabited.proof_5 {G : Type u_1} [AddGroup G] (a : Set G) : a ∈ {{0}} → ∃ x ∈ {{0}}, x ⊆ -a

theorem AddGroupFilterBasis.instInhabited.proof_4 {G : Type u_1} [AddGroup G] (a : Set G) : a ∈ {{0}} → ∃ x ∈ {{0}}, x + x ⊆ a

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

theorem AddGroupFilterBasis.instInhabited.proof_3 {G : Type u_1} [AddGroup G] (a : Set G) : a ∈ {{0}} → 0 ∈ a

theorem AddGroupFilterBasis.instInhabited.proof_6 {G : Type u_1} [AddGroup G] (a : G) (a : Set G) : a ∈ {{0}} → ∃ x ∈ {{0}}, x ⊆ (fun (x : G) => a✝ + x + -a✝) ⁻¹' a

theorem AddGroupFilterBasis.instInhabited.proof_2 {G : Type u_1} [AddGroup G] (a : Set G) (a : Set G) : a✝ ∈ {{0}} → a ∈ {{0}} → ∃ x ∈ {{0}}, x ⊆ a✝ ∩ a

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

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

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

theorem GroupFilterBasis.subset_mul_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

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

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) GroupFilterBasis.toFilterBasis.filter

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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_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_zero_hasBasis {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) : (nhds 0).HasBasis (fun (V : Set G) => V ∈ B) id

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.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 100]

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

• ⋯ = ⋯

@[instance 100]

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

• ⋯ = ⋯

class RingFilterBasis (R : Type u) [Ring R] extends AddGroupFilterBasis : 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 : AddGroupFilterBasis.toFilterBasis.sets.Nonempty
• inter_sets : ∀ {x y : Set R}, x ∈ AddGroupFilterBasis.toFilterBasis.sets → y ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ z ∈ AddGroupFilterBasis.toFilterBasis.sets, z ⊆ x ∩ y
• zero' : ∀ {U : Set R}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → 0 ∈ U
• add' : ∀ {U : Set R}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V + V ⊆ U
• neg' : ∀ {U : Set R}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun (x : R) => -x) ⁻¹' U
• conj' : ∀ (x₀ : R) {U : Set R}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun (x : R) => x₀ + x + -x₀) ⁻¹' U
• mul' : ∀ {U : Set R}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V * V ⊆ U
• mul_left' : ∀ (x₀ : R) {U : Set R}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun (x : R) => x₀ * x) ⁻¹' U
• mul_right' : ∀ (x₀ : R) {U : Set R}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun (x : R) => x * x₀) ⁻¹' U

theorem RingFilterBasis.mul' {R : Type u} : ∀ {inst : Ring R} [self : RingFilterBasis R] {U : Set R}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V * V ⊆ U

theorem RingFilterBasis.mul_left' {R : Type u} : ∀ {inst : Ring R} [self : RingFilterBasis R] (x₀ : R) {U : Set R}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun (x : R) => x₀ * x) ⁻¹' U

theorem RingFilterBasis.mul_right' {R : Type u} : ∀ {inst : Ring R} [self : RingFilterBasis R] (x₀ : R) {U : Set R}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.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 ∈ AddGroupFilterBasis.toFilterBasis.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 = RingFilterBasis.toAddGroupFilterBasis.topology

@[instance 100]

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

• ⋯ = ⋯

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

theorem ModuleFilterBasis.smul' {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (self : ModuleFilterBasis R M) {U : Set M} : U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ nhds 0, ∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, V • W ⊆ U

theorem ModuleFilterBasis.smul_left' {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (self : ModuleFilterBasis R M) (x₀ : R) {U : Set M} : U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, 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] (self : ModuleFilterBasis R M) (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} [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 ∈ AddGroupFilterBasis.toFilterBasis.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} → [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

• 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} [TopologicalRing R] [TopologicalSpace M] [TopologicalAddGroup 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 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} [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

• ⋯ = ⋯

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