Mathlib.Topology.Algebra.FilterBasis

GroupFilterBasis structure

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

Full source

/-- 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 GroupFilterBasis (G : Type u) [Group G] extends FilterBasis G where
  one' : ∀ {U}, U ∈ sets → (1 : G) ∈ U
  mul' : ∀ {U}, U ∈ sets → ∃ V ∈ sets, V * V ⊆ U
  inv' : ∀ {U}, U ∈ sets → ∃ V ∈ sets, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U
  conj' : ∀ x₀, ∀ {U}, U ∈ sets → ∃ V ∈ sets, V ⊆ (fun x ↦ x₀ * x * x₀⁻¹) ⁻¹' U

Group Filter Basis

Informal description

A `GroupFilterBasis` on a group $ G $ is a filter basis on $ G $ satisfying the following additional properties: 1. The neutral element $ 1 $ is contained in every set of the basis. 2. For any set $ U $ in the basis, there exists a set $ V $ in the basis such that the product $ V \cdot V $ is contained in $ U $. 3. For any set $ U $ in the basis, there exists a set $ V $ in the basis such that $ V $ is contained in the preimage of $ U $ under the inversion map $ x \mapsto x^{-1} $. This structure is used to define a topology on $ G $ that makes it a topological group, where the neighborhoods of the identity are generated by the given basis.

AddGroupFilterBasis structure

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

Full source

/-- 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`. -/
class AddGroupFilterBasis (A : Type u) [AddGroup A] extends FilterBasis A where
  zero' : ∀ {U}, U ∈ sets → (0 : A) ∈ U
  add' : ∀ {U}, U ∈ sets → ∃ V ∈ sets, V + V ⊆ U
  neg' : ∀ {U}, U ∈ sets → ∃ V ∈ sets, V ⊆ (fun x ↦ -x) ⁻¹' U
  conj' : ∀ x₀, ∀ {U}, U ∈ sets → ∃ V ∈ sets, V ⊆ (fun x ↦ x₀ + x + -x₀) ⁻¹' U

Additive Group Filter Basis

Informal description

An additive group filter basis on an additive group $A$ is a filter basis on $A$ satisfying additional axioms that ensure compatibility with the group structure. Specifically, it is a collection of subsets of $A$ that is nonempty, closed under finite intersections, and satisfies properties related to the group operations: for any set $U$ in the basis, there exists a set $V$ in the basis such that $V + V \subseteq U$ (additive version of the multiplication property), and for any set $U$ in the basis, there exists a set $V$ in the basis such that $V \subseteq -U$ (additive version of the inverse property). This structure is used to define a topology on $A$ that makes it into a topological additive group, where the neighborhoods of the identity are generated by the given basis.

groupFilterBasisOfComm definition

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

Full source

/-- `GroupFilterBasis` constructor in the commutative group case. -/
@[to_additive "`AddGroupFilterBasis` constructor in the additive commutative group case."]
def groupFilterBasisOfComm {G : Type*} [CommGroup G] (sets : Set (Set G))
    (nonempty : sets.Nonempty) (inter_sets : ∀ x y, x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y)
    (one : ∀ U ∈ sets, (1 : G) ∈ U) (mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U)
    (inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U) : GroupFilterBasis G :=
  { sets := sets
    nonempty := nonempty
    inter_sets := inter_sets _ _
    one' := one _
    mul' := mul _
    inv' := inv _
    conj' := fun x U U_in ↦ ⟨U, U_in, by simp only [mul_inv_cancel_comm, preimage_id']; rfl⟩ }

Group Filter Basis Construction for Commutative Groups

Informal description

Given a commutative group $ G $ and a collection of subsets `sets` of $ G $, the function `groupFilterBasisOfComm` constructs a `GroupFilterBasis` structure on $ G $ provided the following conditions are satisfied: 1. The collection `sets` is nonempty. 2. For any two subsets $ x $ and $ y $ in `sets`, there exists a subset $ z $ in `sets` contained in their intersection $ x \cap y $. 3. The neutral element $ 1 $ is contained in every subset $ U $ in `sets`. 4. For any subset $ U $ in `sets`, there exists a subset $ V $ in `sets` such that the product $ V \cdot V $ is contained in $ U $. 5. For any subset $ U $ in `sets`, there exists a subset $ V $ in `sets` such that $ V $ is contained in the preimage of $ U $ under the inversion map $ x \mapsto x^{-1} $. The constructed `GroupFilterBasis` ensures that the group operations are compatible with the topology generated by the basis, making $ G $ a topological group.

GroupFilterBasis.instMembershipSet instance

: Membership (Set G) (GroupFilterBasis G)

Full source

@[to_additive]
instance : Membership (Set G) (GroupFilterBasis G) :=
  ⟨fun f s ↦ s ∈ f.sets⟩

Membership Relation for Group Filter Basis Sets

Informal description

For any group $G$ with a group filter basis, the sets in the basis can be treated as members of the basis structure, allowing notation like $U \in B$ where $B$ is a `GroupFilterBasis` and $U$ is a set in $G$.

GroupFilterBasis.one theorem

{U : Set G} : U ∈ B → (1 : G) ∈ U

Full source

@[to_additive]
theorem one {U : Set G} : U ∈ B → (1 : G) ∈ U :=
  GroupFilterBasis.one'

Neutral Element in Group Filter Basis Sets

Informal description

For any set $U$ in a group filter basis $B$ on a group $G$, the neutral element $1$ is contained in $U$.

GroupFilterBasis.mul theorem

{U : Set G} : U ∈ B → ∃ V ∈ B, V * V ⊆ U

Full source

@[to_additive]
theorem mul {U : Set G} : U ∈ B → ∃ V ∈ B, V * V ⊆ U :=
  GroupFilterBasis.mul'

Existence of Squared Neighborhood in Group Filter Basis

Informal description

For any set $U$ in a group filter basis $B$ on a group $G$, there exists a set $V$ in $B$ such that the product set $V \cdot V$ is contained in $U$.

GroupFilterBasis.inv theorem

{U : Set G} : U ∈ B → ∃ V ∈ B, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U

Full source

@[to_additive]
theorem inv {U : Set G} : U ∈ B → ∃ V ∈ B, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U :=
  GroupFilterBasis.inv'

Inversion Compatibility in Group Filter Basis

Informal description

For any set $U$ in a group filter basis $B$ on a group $G$, there exists a set $V$ in $B$ such that $V$ is contained in the preimage of $U$ under the inversion map $x \mapsto x^{-1}$.

GroupFilterBasis.conj theorem

: ∀ x₀, ∀ {U}, U ∈ B → ∃ V ∈ B, V ⊆ (fun x ↦ x₀ * x * x₀⁻¹) ⁻¹' U

Full source

@[to_additive]
theorem conj : ∀ x₀, ∀ {U}, U ∈ B → ∃ V ∈ B, V ⊆ (fun x ↦ x₀ * x * x₀⁻¹) ⁻¹' U :=
  GroupFilterBasis.conj'

Conjugation Invariance of Group Filter Basis

Informal description

For any element $x₀$ in a group $G$ with a group filter basis $B$, and for any set $U$ in $B$, there exists a set $V$ in $B$ such that $V$ is contained in the preimage of $U$ under the conjugation map $x \mapsto x₀ x x₀^{-1}$.

GroupFilterBasis.instInhabited instance

: Inhabited (GroupFilterBasis G)

Full source

/-- The trivial group filter basis consists of `{1}` only. The associated topology
is discrete. -/
@[to_additive "The trivial additive group filter basis consists of `{0}` only. The associated
topology is discrete."]
instance : Inhabited (GroupFilterBasis G) where
  default := {
    sets := {{1}}
    nonempty := singleton_nonempty _
    inter_sets := by simp
    one' := by simp
    mul' := by simp
    inv' := by simp
    conj' := by simp }

Existence of Trivial Group Filter Basis

Informal description

For any group $G$, there exists a trivial group filter basis consisting only of the singleton set $\{1\}$. The associated topology induced by this basis is the discrete topology.

GroupFilterBasis.subset_mul_self theorem

(B : GroupFilterBasis G) {U : Set G} (h : U ∈ B) : U ⊆ U * U

Full source

@[to_additive]
theorem subset_mul_self (B : GroupFilterBasis G) {U : Set G} (h : U ∈ B) : U ⊆ U * U :=
  fun x x_in ↦ ⟨1, one h, x, x_in, one_mul x⟩

Self-Product Containment in Group Filter Basis

Informal description

For any group filter basis $B$ on a group $G$ and any set $U$ in $B$, the set $U$ is contained in the product set $U \cdot U$, where $U \cdot U$ denotes the set of all products $u_1 \cdot u_2$ for $u_1, u_2 \in U$.

GroupFilterBasis.N definition

(B : GroupFilterBasis G) : G → Filter G

Full source

/-- The neighborhood function of a `GroupFilterBasis`. -/
@[to_additive "The neighborhood function of an `AddGroupFilterBasis`."]
def N (B : GroupFilterBasis G) : G → Filter G :=
  fun x ↦ map (fun y ↦ x * y) B.toFilterBasis.filter

Neighborhood filter induced by a group filter basis

Informal description

Given a group filter basis $ B $ on a group $ G $, the function $ N $ maps each element $ x \in G $ to the filter generated by the left translates $ x \cdot U $ for all sets $ U $ in the basis $ B $. Specifically, $ N(x) $ is the filter obtained by applying the left multiplication map $ y \mapsto x \cdot y $ to the filter associated with the basis $ B $.

GroupFilterBasis.N_one theorem

(B : GroupFilterBasis G) : B.N 1 = B.toFilterBasis.filter

Full source

@[to_additive (attr := simp)]
theorem N_one (B : GroupFilterBasis G) : B.N 1 = B.toFilterBasis.filter := by
  simp only [N, one_mul, map_id']

Neighborhood Filter of Identity in Group Filter Basis

Informal description

For a group filter basis $B$ on a group $G$, the neighborhood filter of the identity element $1$ is equal to the filter generated by the basis $B$, i.e., $B.N(1) = B.\text{filter}$.

GroupFilterBasis.hasBasis theorem

(B : GroupFilterBasis G) (x : G) : HasBasis (B.N x) (fun V : Set G ↦ V ∈ B) fun V ↦ (fun y ↦ x * y) '' V

Full source

@[to_additive]
protected theorem hasBasis (B : GroupFilterBasis G) (x : G) :
    HasBasis (B.N x) (fun V : Set G ↦ V ∈ B) fun V ↦ (fun y ↦ x * y) '' V :=
  HasBasis.map (fun y ↦ x * y) toFilterBasis.hasBasis

Basis Characterization of Neighborhood Filters in Group Filter Basis

Informal description

Let $G$ be a group equipped with a group filter basis $B$. For any element $x \in G$, the neighborhood filter $B.N(x)$ has a basis consisting of the sets $\{x \cdot y \mid y \in V\}$ where $V$ ranges over all sets in the basis $B$.

GroupFilterBasis.topology definition

(B : GroupFilterBasis G) : TopologicalSpace G

Full source

/-- The topological space structure coming from a group filter basis. -/
@[to_additive "The topological space structure coming from an additive group filter basis."]
def topology (B : GroupFilterBasis G) : TopologicalSpace G :=
  TopologicalSpace.mkOfNhds B.N

Topology induced by a group filter basis

Informal description

Given a group filter basis $ B $ on a group $ G $, the topology on $ G $ is defined such that the neighborhood filter of each point $ x \in G $ is given by $ B.N(x) $, where $ B.N(x) $ is the filter generated by the left translates $ x \cdot U $ for all sets $ U $ in the basis $ B $. This topology makes $ G $ into a topological group where the neighborhoods of the identity are generated by the basis $ B $.

GroupFilterBasis.nhds_eq theorem

(B : GroupFilterBasis G) {x₀ : G} : @nhds G B.topology x₀ = B.N x₀

Full source

@[to_additive]
theorem nhds_eq (B : GroupFilterBasis G) {x₀ : G} : @nhds G B.topology x₀ = B.N x₀ := by
  apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun x ↦ (FilterBasis.hasBasis _).map _)
  · intro a U U_in
    exact ⟨1, B.one U_in, mul_one a⟩
  · intro a U U_in
    rcases GroupFilterBasis.mul U_in with ⟨V, V_in, hVU⟩
    filter_upwards [image_mem_map (B.mem_filter_of_mem V_in)]
    rintro _ ⟨x, hx, rfl⟩
    calc
      (a * x) • V ∈ (a * x) • B.filter := smul_set_mem_smul_filter <| B.mem_filter_of_mem V_in
      _ = a • x • V := smul_smul .. |>.symm
      _ ⊆ a • (V * V)calc
      (a * x) • V ∈ (a * x) • B.filter := smul_set_mem_smul_filter <| B.mem_filter_of_mem V_in
      _ = a • x • V := smul_smul .. |>.symm
      _ ⊆ a • (V * V) := smul_set_mono <| smul_set_subset_smul hx
      _ ⊆ a • U := smul_set_mono hVU

Neighborhood Filter Characterization in Group Filter Basis Topology

Informal description

Let $G$ be a group equipped with a group filter basis $B$. For any element $x_0 \in G$, the neighborhood filter of $x_0$ in the topology induced by $B$ is equal to $B.N(x_0)$, where $B.N(x_0)$ is the filter generated by the left translates $x_0 \cdot U$ for all sets $U$ in the basis $B$.

GroupFilterBasis.nhds_one_eq theorem

(B : GroupFilterBasis G) : @nhds G B.topology (1 : G) = B.toFilterBasis.filter

Full source

@[to_additive]
theorem nhds_one_eq (B : GroupFilterBasis G) :
    @nhds G B.topology (1 : G) = B.toFilterBasis.filter := by
  rw [B.nhds_eq]
  simp only [N, one_mul]
  exact map_id

Neighborhood Filter of Identity in Group Filter Basis Topology

Informal description

Let $G$ be a group equipped with a group filter basis $B$. The neighborhood filter of the identity element $1 \in G$ in the topology induced by $B$ is equal to the filter generated by the basis $B$.

GroupFilterBasis.nhds_hasBasis theorem

 (B : GroupFilterBasis G) (x₀ : G) :
  HasBasis (@nhds G B.topology x₀) (fun V : Set G ↦ V ∈ B) fun V ↦ (fun y ↦ x₀ * y) '' V

Full source

@[to_additive]
theorem nhds_hasBasis (B : GroupFilterBasis G) (x₀ : G) :
    HasBasis (@nhds G B.topology x₀) (fun V : Set G ↦ V ∈ B) fun V ↦ (fun y ↦ x₀ * y) '' V := by
  rw [B.nhds_eq]
  apply B.hasBasis

Basis Characterization of Neighborhood Filters in Group Filter Basis Topology

Informal description

Let $G$ be a group equipped with a group filter basis $B$. For any element $x_0 \in G$, the neighborhood filter of $x_0$ in the topology induced by $B$ has a basis consisting of the sets $\{x_0 \cdot y \mid y \in V\}$ where $V$ ranges over all sets in the basis $B$.

GroupFilterBasis.nhds_one_hasBasis theorem

(B : GroupFilterBasis G) : HasBasis (@nhds G B.topology 1) (fun V : Set G ↦ V ∈ B) id

Full source

@[to_additive]
theorem nhds_one_hasBasis (B : GroupFilterBasis G) :
    HasBasis (@nhds G B.topology 1) (fun V : Set G ↦ V ∈ B) id := by
  rw [B.nhds_one_eq]
  exact B.toFilterBasis.hasBasis

Basis characterization of identity neighborhoods in group filter basis topology

Informal description

Let $G$ be a group equipped with a group filter basis $B$. The neighborhood filter of the identity element $1 \in G$ in the topology induced by $B$ has a basis consisting of the sets $V$ where $V$ ranges over all sets in $B$.

GroupFilterBasis.mem_nhds_one theorem

(B : GroupFilterBasis G) {U : Set G} (hU : U ∈ B) : U ∈ @nhds G B.topology 1

Full source

@[to_additive]
theorem mem_nhds_one (B : GroupFilterBasis G) {U : Set G} (hU : U ∈ B) :
    U ∈ @nhds G B.topology 1 := by
  rw [B.nhds_one_hasBasis.mem_iff]
  exact ⟨U, hU, rfl.subset⟩

Neighborhoods of Identity in Group Filter Basis Topology

Informal description

Let $G$ be a group equipped with a group filter basis $B$. For any set $U$ in $B$, $U$ is a neighborhood of the identity element $1$ in the topology induced by $B$.

GroupFilterBasis.isTopologicalGroup instance

(B : GroupFilterBasis G) : @IsTopologicalGroup G B.topology _

Full source

/-- If a group is endowed with a topological structure coming from a group filter basis then it's a
topological group. -/
@[to_additive "If a group is endowed with a topological structure coming from a group filter basis
then it's a topological group."]
instance (priority := 100) isTopologicalGroup (B : GroupFilterBasis G) :
    @IsTopologicalGroup G B.topology _ := by
  letI := B.topology
  have basis := B.nhds_one_hasBasis
  have basis' := basis.prod basis
  refine IsTopologicalGroup.of_nhds_one ?_ ?_ ?_ ?_
  · rw [basis'.tendsto_iff basis]
    suffices ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
    intro U U_in
    rcases mul U_in with ⟨V, V_in, hV⟩
    refine ⟨V, V, ⟨V_in, V_in⟩, ?_⟩
    intro a b a_in b_in
    exact hV <| mul_mem_mul a_in b_in
  · rw [basis.tendsto_iff basis]
    intro U U_in
    simpa using inv U_in
  · intro x₀
    rw [nhds_eq, nhds_one_eq]
    rfl
  · intro x₀
    rw [basis.tendsto_iff basis]
    intro U U_in
    exact conj x₀ U_in

Topological Group Structure from Group Filter Basis

Informal description

For any group $G$ equipped with a group filter basis $B$, the topology induced by $B$ makes $G$ into a topological group.

RingFilterBasis structure

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

Full source

/-- 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. -/
class RingFilterBasis (R : Type u) [Ring R] extends AddGroupFilterBasis R where
  mul' : ∀ {U}, U ∈ sets → ∃ V ∈ sets, V * V ⊆ U
  mul_left' : ∀ (x₀ : R) {U}, U ∈ sets → ∃ V ∈ sets, V ⊆ (fun x ↦ x₀ * x) ⁻¹' U
  mul_right' : ∀ (x₀ : R) {U}, U ∈ sets → ∃ V ∈ sets, V ⊆ (fun x ↦ x * x₀) ⁻¹' U

Ring Filter Basis

Informal description

A `RingFilterBasis` on a ring $R$ is a filter basis on $R$ that satisfies additional axioms ensuring compatibility with the ring structure. Specifically, it extends an additive group filter basis and includes conditions such as the existence of a set $V$ in the basis for any set $U$ in the basis, such that $V \cdot V \subseteq U$. This structure allows defining a topology on $R$ that is compatible with the ring operations.

RingFilterBasis.instMembershipSet instance

: Membership (Set R) (RingFilterBasis R)

Full source

instance : Membership (Set R) (RingFilterBasis R) :=
  ⟨fun B s ↦ s ∈ B.sets⟩

Membership Structure for Sets in a Ring Filter Basis

Informal description

For any ring $R$ with a ring filter basis, the collection of sets in the basis forms a membership structure where a set $U$ is considered to be in the basis if it satisfies the conditions required by the ring filter basis.

RingFilterBasis.mul theorem

{U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V * V ⊆ U

Full source

theorem mul {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V * V ⊆ U :=
  mul' hU

Existence of Squared Neighborhood in Ring Filter Basis

Informal description

Let $B$ be a ring filter basis on a ring $R$. For any set $U \in B$, there exists a set $V \in B$ such that the product set $V \cdot V$ is contained in $U$.

RingFilterBasis.mul_left theorem

(x₀ : R) {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x₀ * x) ⁻¹' U

Full source

theorem mul_left (x₀ : R) {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x₀ * x) ⁻¹' U :=
  mul_left' x₀ hU

Existence of Left Multiplication-Compatible Neighborhood in Ring Filter Basis

Informal description

Let $B$ be a ring filter basis on a ring $R$. For any element $x_0 \in R$ and any set $U \in B$, there exists a set $V \in B$ such that $V$ is contained in the preimage of $U$ under the left multiplication map by $x_0$, i.e., $V \subseteq \{x \in R \mid x_0 \cdot x \in U\}$.

RingFilterBasis.mul_right theorem

(x₀ : R) {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x * x₀) ⁻¹' U

Full source

theorem mul_right (x₀ : R) {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x * x₀) ⁻¹' U :=
  mul_right' x₀ hU

Existence of Right Multiplication-Compatible Neighborhood in Ring Filter Basis

Informal description

Let $B$ be a ring filter basis on a ring $R$. For any element $x_0 \in R$ and any set $U \in B$, there exists a set $V \in B$ such that $V$ is contained in the preimage of $U$ under the right multiplication map by $x_0$, i.e., $V \subseteq \{x \in R \mid x \cdot x_0 \in U\}$.

RingFilterBasis.topology definition

: TopologicalSpace R

Full source

/-- The topology associated to a ring filter basis.
It has the given basis as a basis of neighborhoods of zero. -/
def topology : TopologicalSpace R :=
  B.toAddGroupFilterBasis.topology

Topology induced by a ring filter basis

Informal description

The topology on a ring $R$ induced by a ring filter basis $B$, where the basis consists of neighborhoods of zero that are compatible with the ring structure. This topology makes $R$ into a topological ring.

RingFilterBasis.isTopologicalRing instance

{R : Type u} [Ring R] (B : RingFilterBasis R) : @IsTopologicalRing R B.topology _

Full source

/-- If a ring is endowed with a topological structure coming from
a ring filter basis then it's a topological ring. -/
instance (priority := 100) isTopologicalRing {R : Type u} [Ring R] (B : RingFilterBasis R) :
    @IsTopologicalRing R B.topology _ := by
  let B' := B.toAddGroupFilterBasis
  letI := B'.topology
  have basis := B'.nhds_zero_hasBasis
  have basis' := basis.prod basis
  haveI := B'.isTopologicalAddGroup
  apply IsTopologicalRing.of_addGroup_of_nhds_zero
  · rw [basis'.tendsto_iff basis]
    suffices ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
    intro U U_in
    rcases B.mul U_in with ⟨V, V_in, hV⟩
    refine ⟨V, V, ⟨V_in, V_in⟩, ?_⟩
    intro a b a_in b_in
    exact hV <| mul_mem_mul a_in b_in
  · intro x₀
    rw [basis.tendsto_iff basis]
    intro U
    simpa using B.mul_left x₀
  · intro x₀
    rw [basis.tendsto_iff basis]
    intro U
    simpa using B.mul_right x₀

Topological Ring Structure from Ring Filter Basis

Informal description

For any ring $R$ equipped with a ring filter basis $B$, the topology induced by $B$ makes $R$ into a topological ring.

ModuleFilterBasis structure

(R M : Type*) [CommRing R] [TopologicalSpace R] [AddCommGroup M]
  [Module R M] extends AddGroupFilterBasis M

Full source

/-- 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`. -/
structure ModuleFilterBasis (R M : Type*) [CommRing R] [TopologicalSpace R] [AddCommGroup M]
  [Module R M] extends AddGroupFilterBasis M where
  smul' : ∀ {U}, U ∈ sets → ∃ V ∈ 𝓝 (0 : R), ∃ W ∈ sets, V • W ⊆ U
  smul_left' : ∀ (x₀ : R) {U}, U ∈ sets → ∃ V ∈ sets, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
  smul_right' : ∀ (m₀ : M) {U}, U ∈ sets → ∀ᶠ x in 𝓝 (0 : R), x • m₀ ∈ U

Module Filter Basis

Informal description

A `ModuleFilterBasis` on a module $M$ over a commutative ring $R$ is a filter basis on $M$ satisfying additional axioms that ensure compatibility with the module structure. Specifically, it extends an additive group filter basis on $M$ and includes the property that for any set $U$ in the basis, there exist a neighborhood $V$ of $0$ in $R$ and a set $W$ in the basis such that the scalar product $V \cdot W$ is contained in $U$.

ModuleFilterBasis.GroupFilterBasis.hasMem instance

: Membership (Set M) (ModuleFilterBasis R M)

Full source

instance GroupFilterBasis.hasMem : Membership (Set M) (ModuleFilterBasis R M) :=
  ⟨fun B s ↦ s ∈ B.sets⟩

Membership Relation in Module Filter Basis

Informal description

For a module $M$ over a commutative ring $R$ with a topological space structure, the module filter basis on $M$ inherits a membership relation where a set $U$ is considered a member if it satisfies the conditions of the module filter basis structure.

ModuleFilterBasis.smul theorem

{U : Set M} (hU : U ∈ B) : ∃ V ∈ 𝓝 (0 : R), ∃ W ∈ B, V • W ⊆ U

Full source

theorem smul {U : Set M} (hU : U ∈ B) : ∃ V ∈ 𝓝 (0 : R), ∃ W ∈ B, V • W ⊆ U :=
  B.smul' hU

Existence of Neighborhoods for Scalar Multiplication in Module Filter Basis

Informal description

For any set $U$ in a module filter basis $B$ of an $R$-module $M$, there exists a neighborhood $V$ of $0$ in $R$ and a set $W$ in $B$ such that the scalar product $V \cdot W$ is contained in $U$.

ModuleFilterBasis.smul_left theorem

(x₀ : R) {U : Set M} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U

Full source

theorem smul_left (x₀ : R) {U : Set M} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U :=
  B.smul_left' x₀ hU

Existence of Filter Basis Set for Scalar Multiplication by Fixed Ring Element

Informal description

For any element $x₀$ in a commutative ring $R$ and any set $U$ in a module filter basis $B$ on an $R$-module $M$, there exists a set $V$ in $B$ such that $V$ is contained in the preimage of $U$ under the scalar multiplication map $x \mapsto x₀ \cdot x$.

ModuleFilterBasis.smul_right theorem

(m₀ : M) {U : Set M} (hU : U ∈ B) : ∀ᶠ x in 𝓝 (0 : R), x • m₀ ∈ U

Full source

theorem smul_right (m₀ : M) {U : Set M} (hU : U ∈ B) : ∀ᶠ x in 𝓝 (0 : R), x • m₀ ∈ U :=
  B.smul_right' m₀ hU

Continuity of Scalar Multiplication at Zero for Fixed Module Element

Informal description

For any element $m_0$ in a module $M$ over a topological ring $R$ with a module filter basis $B$, and for any set $U$ in $B$, there exists a neighborhood $V$ of $0$ in $R$ such that for all $x$ in $V$, the scalar product $x \cdot m_0$ lies in $U$.

ModuleFilterBasis.instInhabitedOfDiscreteTopology instance

[DiscreteTopology R] : Inhabited (ModuleFilterBasis R M)

Full source

/-- If `R` is discrete then the trivial additive group filter basis on any `R`-module is a
module filter basis. -/
instance [DiscreteTopology R] : Inhabited (ModuleFilterBasis R M) :=
  ⟨{
      show AddGroupFilterBasis M from
        default with
      smul' := by
        rintro U (rfl : U ∈ {{(0 : M)}})
        use univ, univ_mem, {0}, rfl
        rintro a ⟨x, -, m, rfl, rfl⟩
        simp only [smul_zero, mem_singleton_iff]
      smul_left' := by
        rintro x₀ U (h : U ∈ {{(0 : M)}})
        rw [mem_singleton_iff] at h
        use {0}, rfl
        simp [h]
      smul_right' := by
        rintro m₀ U (h : U ∈ (0 : Set (Set M)))
        rw [Set.mem_zero] at h
        simp [h, nhds_discrete] }⟩

Existence of Module Filter Basis for Discrete Topology on Ring

Informal description

When the commutative ring $R$ is equipped with the discrete topology, there exists a canonical module filter basis on any $R$-module $M$.

ModuleFilterBasis.topology definition

: TopologicalSpace M

Full source

/-- 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. -/
def topology : TopologicalSpace M :=
  B.toAddGroupFilterBasis.topology

Topology induced by a module filter basis

Informal description

The topology on a module $M$ over a topological ring $R$ induced by a module filter basis $B$, where the sets in $B$ form a basis of neighborhoods of zero. This topology is constructed from the additive group filter basis associated with $B$.

ModuleFilterBasis.topology' definition

 {R M : Type*} [CommRing R] {_ : TopologicalSpace R} [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) :
  TopologicalSpace M

Full source

/-- 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. -/
def topology' {R M : Type*} [CommRing R] {_ : TopologicalSpace R} [AddCommGroup M] [Module R M]
    (B : ModuleFilterBasis R M) : TopologicalSpace M :=
  B.toAddGroupFilterBasis.topology

Topology induced by a module filter basis

Informal description

Given a commutative ring $R$ with a topological space structure, an additive commutative group $M$, and a module structure of $M$ over $R$, the function `ModuleFilterBasis.topology'` takes a module filter basis $B$ on $M$ and returns the topological space structure on $M$ induced by $B$. This topology has the sets in $B$ as a basis of neighborhoods of zero.

ContinuousSMul.of_basis_zero theorem

 {ι : Type*} [IsTopologicalRing R] [TopologicalSpace M] [IsTopologicalAddGroup M] {p : ι → Prop} {b : ι → Set M}
  (h : HasBasis (𝓝 0) p b) (hsmul : ∀ {i}, p i → ∃ V ∈ 𝓝 (0 : R), ∃ j, p j ∧ V • b j ⊆ b i)
  (hsmul_left : ∀ (x₀ : R) {i}, p i → ∃ j, p j ∧ MapsTo (x₀ • ·) (b j) (b i))
  (hsmul_right : ∀ (m₀ : M) {i}, p i → ∀ᶠ x in 𝓝 (0 : R), x • m₀ ∈ b i) : ContinuousSMul R M

Full source

/-- 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. -/
theorem _root_.ContinuousSMul.of_basis_zero {ι : Type*} [IsTopologicalRing R] [TopologicalSpace M]
    [IsTopologicalAddGroup M] {p : ι → Prop} {b : ι → Set M} (h : HasBasis (𝓝 0) p b)
    (hsmul : ∀ {i}, p i → ∃ V ∈ 𝓝 (0 : R), ∃ j, p j ∧ V • b j ⊆ b i)
    (hsmul_left : ∀ (x₀ : R) {i}, p i → ∃ j, p j ∧ MapsTo (x₀ • ·) (b j) (b i))
    (hsmul_right : ∀ (m₀ : M) {i}, p i → ∀ᶠ x in 𝓝 (0 : R), x • m₀ ∈ b i) : ContinuousSMul R M := by
  apply ContinuousSMul.of_nhds_zero
  · rw [h.tendsto_right_iff]
    intro i hi
    rcases hsmul hi with ⟨V, V_in, j, hj, hVj⟩
    apply mem_of_superset (prod_mem_prod V_in <| h.mem_of_mem hj)
    rintro ⟨v, w⟩ ⟨v_in : v ∈ V, w_in : w ∈ b j⟩
    exact hVj (Set.smul_mem_smul v_in w_in)
  · intro m₀
    rw [h.tendsto_right_iff]
    intro i hi
    exact hsmul_right m₀ hi
  · intro x₀
    rw [h.tendsto_right_iff]
    intro i hi
    rcases hsmul_left x₀ hi with ⟨j, hj, hji⟩
    exact mem_of_superset (h.mem_of_mem hj) hji

Continuous Scalar Multiplication via Basis at Zero

Informal description

Let $R$ be a topological ring and $M$ be a topological additive group with a basis $\{b_i\}_{i \in \iota}$ for the neighborhood filter of $0$ in $M$, indexed by a type $\iota$ with a predicate $p$. Suppose the following conditions hold: 1. For any $i$ with $p(i)$, there exists a neighborhood $V$ of $0$ in $R$ and an index $j$ with $p(j)$ such that $V \cdot b_j \subseteq b_i$. 2. For any $x_0 \in R$ and any $i$ with $p(i)$, there exists $j$ with $p(j)$ such that $x_0 \cdot b_j \subseteq b_i$. 3. For any $m_0 \in M$ and any $i$ with $p(i)$, there exists a neighborhood $V$ of $0$ in $R$ such that $V \cdot m_0 \subseteq b_i$. Then the scalar multiplication operation $R \times M \to M$ is continuous, i.e., $M$ is a topological module over $R$.

ModuleFilterBasis.continuousSMul instance

[IsTopologicalRing R] : @ContinuousSMul R M _ _ B.topology

Full source

/-- If a module is endowed with a topological structure coming from
a module filter basis then it's a topological module. -/
instance (priority := 100) continuousSMul [IsTopologicalRing R] :
    @ContinuousSMul R M _ _ B.topology := by
  let B' := B.toAddGroupFilterBasis
  let _ := B'.topology
  have _ := B'.isTopologicalAddGroup
  exact ContinuousSMul.of_basis_zero B'.nhds_zero_hasBasis
      (fun {_} => by simpa using B.smul)
      (by simpa using B.smul_left) B.smul_right

Continuity of Scalar Multiplication in Module Filter Basis Topology

Informal description

For a module $M$ over a topological ring $R$ equipped with a module filter basis $B$, the scalar multiplication operation $R \times M \to M$ is continuous with respect to the topology induced by $B$.

ModuleFilterBasis.ofBases definition

 {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (BR : RingFilterBasis R) (BM : AddGroupFilterBasis M)
  (smul : ∀ {U}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U)
  (smul_left : ∀ (x₀ : R) {U}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U)
  (smul_right : ∀ (m₀ : M) {U}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U) :
  @ModuleFilterBasis R M _ BR.topology _ _

Full source

/-- Build a module filter basis from compatible ring and additive group filter bases. -/
def ofBases {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (BR : RingFilterBasis R)
    (BM : AddGroupFilterBasis M) (smul : ∀ {U}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U)
    (smul_left : ∀ (x₀ : R) {U}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U)
    (smul_right : ∀ (m₀ : M) {U}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U) :
    @ModuleFilterBasis R M _ BR.topology _ _ :=
  let _ := BR.topology
  { BM with
    smul' := by
      intro U U_in
      rcases smul U_in with ⟨V, V_in, W, W_in, H⟩
      exact ⟨V, BR.toAddGroupFilterBasis.mem_nhds_zero V_in, W, W_in, H⟩
    smul_left' := smul_left
    smul_right' := by
      intro m₀ U U_in
      rcases smul_right m₀ U_in with ⟨V, V_in, H⟩
      exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) H }

Construction of Module Filter Basis from Compatible Ring and Additive Group Filter Bases

Informal description

Given a commutative ring $R$ and an $R$-module $M$, let $B_R$ be a ring filter basis on $R$ and $B_M$ be an additive group filter basis on $M$. Suppose the following conditions hold: 1. For any set $U \in B_M$, there exist sets $V \in B_R$ and $W \in B_M$ such that the scalar product $V \cdot W \subseteq U$. 2. For any $x_0 \in R$ and any set $U \in B_M$, there exists a set $V \in B_M$ such that $V \subseteq \{x \in M \mid x_0 \cdot x \in U\}$. 3. For any $m_0 \in M$ and any set $U \in B_M$, there exists a set $V \in B_R$ such that $V \subseteq \{x \in R \mid x \cdot m_0 \in U\}$. Then the structure `ModuleFilterBasis R M` can be constructed, where the topology on $R$ is induced by $B_R$ and the module operations are compatible with the topologies.

Mathlib.Topology.Algebra.FilterBasis

Main definitions and results

References