English
Given a map f: R → S and a topology on R, the coinduced ring topology on S is the finest topology making f continuous and S a topological ring.
Русский
Дано отображение f: R → S и топология на R; на S определяется наилучшая топология, делающая f непрерывной и S топологическим кольцом.
LaTeX
$$RingTopology.coinduced f := sInf {b : RingTopology S | t.coinduced f ≤ b.toTopologicalSpace}$$
Lean4
/-- Given `f : R → S` and a topology on `R`, the coinduced ring topology on `S` is the finest
topology such that `f` is continuous and `S` is a topological ring. -/
def coinduced {R S : Type*} [t : TopologicalSpace R] [Ring S] (f : R → S) : RingTopology S :=
sInf {b : RingTopology S | t.coinduced f ≤ b.toTopologicalSpace}
