putting topology on a monoid

Stream: Is there code for X?

[Kevin Buzzard]

The background to this question is the following. I have a commutative ring $R$ and an $R$-algebra $A$, and the structure map $f:R\to A$ is injective. I also have a topology on $R$ making it a topological ring. I know (on paper) that there's a unique topology on $A$ making the image of $f$ open, and making $f$ a topological embedding. Given that this topology exists, it must be the one obtained by "dragging around $R$" using addition, which can be used to give a neighbourhood basis of every point. Un-toadditivising this and simplifying down to the bare bones gives the following construction:

import Mathlib.Tactic

open Topology

example (M : Type*) [Monoid M] (X : Type*) [TopologicalSpace X] [One X]
    (f : OneHom X M) : TopologicalSpace M where
  IsOpen U := ∀ u ∈ U, {x : X | u * f x ∈ U} ∈ 𝓝 1
  isOpen_univ := by simp_all
  isOpen_inter U V hU hV w hw := Filter.inter_mem (hU w hw.1) (hV w hw.2)
  isOpen_sUnion U h u hu := by
    obtain ⟨V, hVU, huV⟩ := hu
    apply Filter.mem_of_superset (h V hVU u huV)
    intro b hb
    exact Set.subset_sUnion_of_subset U V (subset_refl _) hVU hb

Am I reinventing the wheel here? Do we have this already? There will then be some conditions on the inputs which will guarantee that $M$ is a topological monoid; in my case $X$ is also a topological monoid (commutative) and $f$ is a morphism of monoids, so there will now be some nice criterion for when $M$ also ends up as a topological monoid.

My memory from 2018/9 was that @Patrick Massot formalised a bunch of Bourbaki Top Gen including tricks like this to give topological group and topological ring structures on things, but looking through that work I now see that it was things like docs#TopologicalGroup.of_nhds_one , which shows that something is a topological group given a topology already on the group (i.e. the next step). What I have above is something different: we're making the topology. Does mathlib want this construction?

[Patrick Massot]

Did you look around https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Nonarchimedean/Bases.html? This is full of constructions of topologies.

[Kevin Buzzard]

Oh this looks like exactly what I'm looking for -- thanks!