English
A topological additive group with a basis at 0 satisfying ModuleFilterBasis axioms induces a continuous scalar action of R on M; i.e., the map R × M → M given by (r,m) ↦ r · m is continuous when R has its ring topology and M its ModuleFilterBasis topology.
Русский
Топологическая абелeва группа с базисом в 0, удовлетворяющая аксиомам ModuleFilterBasis, задаёт непрерывное действие скаляра: R × M → M непрерывно.
LaTeX
$$$\text{ContinuousSMul.of_basis_zero} : \text{ContinuousSMul } R M$.$$
Lean4
/-- A topological additive group with a basis of `𝓝 0` satisfying the axioms of `ModuleFilterBasis`
is a topological module.
This lemma is mathematically useless because one could obtain such a result by applying
`ModuleFilterBasis.continuousSMul` and use the fact that group topologies are characterized
by their neighborhoods of 0 to obtain the `ContinuousSMul` on the pre-existing topology.
But it turns out it's just easier to get it as a byproduct of the proof, so this is just a free
quality-of-life improvement. -/
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
