From 748b3858b1a163c7088a5e5528e1fc169e5b190b Mon Sep 17 00:00:00 2001 From: Jason Yuen Date: Thu, 6 Apr 2023 07:51:02 +0000 Subject: [PATCH] feat: port Topology.Algebra.FilterBasis (#3279) Co-authored-by: Parcly Taxel Co-authored-by: Chris Hughes Co-authored-by: Jeremy Tan Jie Rui --- Mathlib.lean | 1 + Mathlib/Topology/Algebra/FilterBasis.lean | 467 ++++++++++++++++++++++ 2 files changed, 468 insertions(+) create mode 100644 Mathlib/Topology/Algebra/FilterBasis.lean diff --git a/Mathlib.lean b/Mathlib.lean index 90f28c8785b70..b489ea24b1656 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1604,6 +1604,7 @@ import Mathlib.Topology.Algebra.Algebra import Mathlib.Topology.Algebra.ConstMulAction import Mathlib.Topology.Algebra.Constructions import Mathlib.Topology.Algebra.Field +import Mathlib.Topology.Algebra.FilterBasis import Mathlib.Topology.Algebra.Group.Basic import Mathlib.Topology.Algebra.Group.Compact import Mathlib.Topology.Algebra.GroupCompletion diff --git a/Mathlib/Topology/Algebra/FilterBasis.lean b/Mathlib/Topology/Algebra/FilterBasis.lean new file mode 100644 index 0000000000000..4a30cd2103ecf --- /dev/null +++ b/Mathlib/Topology/Algebra/FilterBasis.lean @@ -0,0 +1,467 @@ +/- +Copyright (c) 2021 Patrick Massot. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Patrick Massot + +! This file was ported from Lean 3 source module topology.algebra.filter_basis +! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Order.Filter.Bases +import Mathlib.Topology.Algebra.Module.Basic + +/-! +# 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] +-/ + + +open Filter Set TopologicalSpace Function + +open Topology Filter Pointwise + +universe 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 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 +#align group_filter_basis GroupFilterBasis + +/-- 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 +#align add_group_filter_basis AddGroupFilterBasis + +attribute [to_additive existing] GroupFilterBasis GroupFilterBasis.conj' + GroupFilterBasis.toFilterBasis + +/-- `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⟩ } +#align group_filter_basis_of_comm groupFilterBasisOfComm +#align add_group_filter_basis_of_comm addGroupFilterBasisOfComm + +namespace GroupFilterBasis + +variable {G : Type u} [Group G] {B : GroupFilterBasis G} + +@[to_additive] +instance : Membership (Set G) (GroupFilterBasis G) := + ⟨fun s f ↦ s ∈ f.sets⟩ + +@[to_additive] +theorem one {U : Set G} : U ∈ B → (1 : G) ∈ U := + GroupFilterBasis.one' +#align group_filter_basis.one GroupFilterBasis.one +#align add_group_filter_basis.zero AddGroupFilterBasis.zero + +@[to_additive] +theorem mul {U : Set G} : U ∈ B → ∃ V ∈ B, V * V ⊆ U := + GroupFilterBasis.mul' +#align group_filter_basis.mul GroupFilterBasis.mul +#align add_group_filter_basis.add AddGroupFilterBasis.add + +@[to_additive] +theorem inv {U : Set G} : U ∈ B → ∃ V ∈ B, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U := + GroupFilterBasis.inv' +#align group_filter_basis.inv GroupFilterBasis.inv +#align add_group_filter_basis.neg AddGroupFilterBasis.neg + +@[to_additive] +theorem conj : ∀ x₀, ∀ {U}, U ∈ B → ∃ V ∈ B, V ⊆ (fun x ↦ x₀ * x * x₀⁻¹) ⁻¹' U := + GroupFilterBasis.conj' +#align group_filter_basis.conj GroupFilterBasis.conj +#align add_group_filter_basis.conj AddGroupFilterBasis.conj + +/-- 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) := ⟨by + refine' + { sets := {{1}} + nonempty := singleton_nonempty _.. } + all_goals simp only [exists_prop, mem_singleton_iff] + · rintro - - rfl rfl + use {1} + simp + · simp + · rintro - rfl + use {1} + simp + · rintro - rfl + use {1} + simp + · rintro x₀ - rfl + use {1} + simp⟩ + +@[to_additive] +theorem prod_subset_self (B : GroupFilterBasis G) {U : Set G} (h : U ∈ B) : U ⊆ U * U := + fun x x_in ↦ ⟨1, x, one h, x_in, one_mul x⟩ +#align group_filter_basis.prod_subset_self GroupFilterBasis.prod_subset_self +#align add_group_filter_basis.sum_subset_self AddGroupFilterBasis.sum_subset_self + +/-- 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 +set_option linter.uppercaseLean3 false in +#align group_filter_basis.N GroupFilterBasis.N +set_option linter.uppercaseLean3 false in +#align add_group_filter_basis.N AddGroupFilterBasis.N + +@[to_additive (attr := simp)] +theorem N_one (B : GroupFilterBasis G) : B.N 1 = B.toFilterBasis.filter := by + simp only [N, one_mul, map_id'] +set_option linter.uppercaseLean3 false in +#align group_filter_basis.N_one GroupFilterBasis.N_one +set_option linter.uppercaseLean3 false in +#align add_group_filter_basis.N_zero AddGroupFilterBasis.N_zero + +@[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 +#align group_filter_basis.has_basis GroupFilterBasis.hasBasis +#align add_group_filter_basis.has_basis AddGroupFilterBasis.hasBasis + +/-- 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 +#align group_filter_basis.topology GroupFilterBasis.topology +#align add_group_filter_basis.topology AddGroupFilterBasis.topology + +@[to_additive] +theorem nhds_eq (B : GroupFilterBasis G) {x₀ : G} : @nhds G B.topology x₀ = B.N x₀ := by + rw [TopologicalSpace.nhds_mkOfNhds] + · intro x U U_in + rw [(B.hasBasis x).mem_iff] at U_in + rcases U_in with ⟨V, V_in, H⟩ + simpa [mem_pure] using H (mem_image_of_mem _ (GroupFilterBasis.one V_in)) + · intro x U U_in + rw [(B.hasBasis x).mem_iff] at U_in + rcases U_in with ⟨V, V_in, H⟩ + rcases GroupFilterBasis.mul V_in with ⟨W, W_in, hW⟩ + use (fun y ↦ x * y) '' W, image_mem_map (FilterBasis.mem_filter_of_mem _ W_in) + constructor + · rw [image_subset_iff] at H⊢ + exact ((B.prod_subset_self W_in).trans hW).trans H + · rintro y ⟨t, tW, rfl⟩ + rw [(B.hasBasis _).mem_iff] + use W, W_in + apply Subset.trans _ H + clear H + rintro z ⟨w, wW, rfl⟩ + exact ⟨t * w, hW (mul_mem_mul tW wW), by simp [mul_assoc]⟩ +#align group_filter_basis.nhds_eq GroupFilterBasis.nhds_eq +#align add_group_filter_basis.nhds_eq AddGroupFilterBasis.nhds_eq + +@[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 +#align group_filter_basis.nhds_one_eq GroupFilterBasis.nhds_one_eq +#align add_group_filter_basis.nhds_zero_eq AddGroupFilterBasis.nhds_zero_eq + +@[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 +#align group_filter_basis.nhds_has_basis GroupFilterBasis.nhds_hasBasis +#align add_group_filter_basis.nhds_has_basis AddGroupFilterBasis.nhds_hasBasis + +@[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 +#align group_filter_basis.nhds_one_has_basis GroupFilterBasis.nhds_one_hasBasis +#align add_group_filter_basis.nhds_zero_has_basis AddGroupFilterBasis.nhds_zero_hasBasis + +@[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⟩ +#align group_filter_basis.mem_nhds_one GroupFilterBasis.mem_nhds_one +#align add_group_filter_basis.mem_nhds_zero AddGroupFilterBasis.mem_nhds_zero + +-- See note [lower instance priority] +/-- 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) : + @TopologicalGroup G B.topology _ := by + letI := B.topology + have basis := B.nhds_one_hasBasis + have basis' := basis.prod basis + refine' TopologicalGroup.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 ⟨a, b, a_in, b_in, rfl⟩ + · 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 +#align group_filter_basis.is_topological_group GroupFilterBasis.isTopologicalGroup +#align add_group_filter_basis.is_topological_add_group AddGroupFilterBasis.isTopologicalAddGroup + +end GroupFilterBasis + +/-- 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 +#align ring_filter_basis RingFilterBasis + +namespace RingFilterBasis + +variable {R : Type u} [Ring R] (B : RingFilterBasis R) + +instance : Membership (Set R) (RingFilterBasis R) := + ⟨fun s B ↦ s ∈ B.sets⟩ + +theorem mul {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V * V ⊆ U := + mul' hU +#align ring_filter_basis.mul RingFilterBasis.mul + +theorem mul_left (x₀ : R) {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x₀ * x) ⁻¹' U := + mul_left' x₀ hU +#align ring_filter_basis.mul_left RingFilterBasis.mul_left + +theorem mul_right (x₀ : R) {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x * x₀) ⁻¹' U := + mul_right' x₀ hU +#align ring_filter_basis.mul_right RingFilterBasis.mul_right + +/-- 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 +#align ring_filter_basis.topology RingFilterBasis.topology + +/-- 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) : + @TopologicalRing 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 TopologicalRing.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 ⟨a, b, a_in, b_in, rfl⟩ + · 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₀ +#align ring_filter_basis.is_topological_ring RingFilterBasis.isTopologicalRing + +end RingFilterBasis + +/-- 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 +#align module_filter_basis ModuleFilterBasis + +namespace ModuleFilterBasis + +variable {R M : Type _} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] + (B : ModuleFilterBasis R M) + +instance GroupFilterBasis.hasMem : Membership (Set M) (ModuleFilterBasis R M) := + ⟨fun s B ↦ s ∈ B.sets⟩ +#align module_filter_basis.group_filter_basis.has_mem ModuleFilterBasis.GroupFilterBasis.hasMem + +theorem smul {U : Set M} (hU : U ∈ B) : ∃ V ∈ 𝓝 (0 : R), ∃ W ∈ B, V • W ⊆ U := + B.smul' hU +#align module_filter_basis.smul ModuleFilterBasis.smul + +theorem smul_left (x₀ : R) {U : Set M} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U := + B.smul_left' x₀ hU +#align module_filter_basis.smul_left ModuleFilterBasis.smul_left + +theorem smul_right (m₀ : M) {U : Set M} (hU : U ∈ B) : ∀ᶠ x in 𝓝 (0 : R), x • m₀ ∈ U := + B.smul_right' m₀ hU +#align module_filter_basis.smul_right ModuleFilterBasis.smul_right + +/-- 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] }⟩ + +/-- 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 +#align module_filter_basis.topology ModuleFilterBasis.topology + +/-- 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 +#align module_filter_basis.topology' ModuleFilterBasis.topology' + +/-- 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 _} [TopologicalRing R] [TopologicalSpace M] + [TopologicalAddGroup 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), b j ⊆ (fun x ↦ x₀ • x) ⁻¹' 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 +#align has_continuous_smul.of_basis_zero ContinuousSMul.of_basis_zero + +/-- 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 [TopologicalRing 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 +#align module_filter_basis.has_continuous_smul ModuleFilterBasis.continuousSMul + +/-- 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 } +#align module_filter_basis.of_bases ModuleFilterBasis.ofBases + +end ModuleFilterBasis