English
If there is a topological space A with IsModuleTopology R A, then the topology on A equals moduleTopology R A.
Русский
Если дана топология A с IsModuleTopology R A, тогда топология на A совпадает с moduleTopology R A.
LaTeX
$$$\tau_A = \text{moduleTopology } R A$$$
Lean4
/-- The topology on a topological semiring `R` agrees with the module topology when considering
`R` as an `R`-module in the obvious way (i.e., via `Semiring.toModule`). -/
instance _root_.IsTopologicalSemiring.toIsModuleTopology : IsModuleTopology R R := by
/- By a previous lemma it suffices to show that the identity from (R,usual) to
(R, module topology) is continuous. -/
apply of_continuous_id
rw [show (id : R → R) = (fun rs ↦ rs.1 • rs.2) ∘ (fun r ↦ (r, 1)) by ext; simp]
/-
It thus suffices to show that each of these maps are continuous. For this claim to even make
sense, we need to topologise `R × R`. The trick is to do this by giving the first `R` the usual
topology `τR` and the second `R` the module topology. To do this we have to "fight mathlib"
a bit with `@`, because there is more than one topology on `R` here.
-/
apply @Continuous.comp R (R × R) R τR (@instTopologicalSpaceProd R R τR (moduleTopology R R)) (moduleTopology R R)
· /-
The map R × R → R is `•`, so by a fundamental property of the module topology,
this is continuous. -/
exact @continuous_smul _ _ _ _ (moduleTopology R R) <| ModuleTopology.continuousSMul ..
· /-
The map `R → R × R` sending `r` to `(r,1)` is a map into a product, so it suffices to show
that each of the two factors is continuous. But the first is the identity function
on `(R, usual topology)` and the second is a constant function. -/
exact
@Continuous.prodMk _ _ _ _ (moduleTopology R R) _ _ _ continuous_id <|
@continuous_const _ _ _ (moduleTopology R R) _
