English
Given a map f: α → β and a topology on α, the coinduced topology on β is the finest topology that makes f continuous while giving β the structure of a topological group.
Русский
Дано отображение f: α → β и топология на α. Коиндукционная топология на β есть самая тонкаяTopology, которая делает f непрерывной и при этом β является топологической группой.
LaTeX
$$$\\text{coinduced}(f,t) = \\bigwedge\\{ b : GroupTopology(β) \\mid TopologicalSpace.coinduced(f,t) \\le b.toTopologicalSpace\\}$$$
Lean4
/-- Given `f : α → β` and a topology on `α`, the coinduced group topology on `β` is the finest
topology such that `f` is continuous and `β` is a topological group. -/
@[to_additive /-- Given `f : α → β` and a topology on `α`, the coinduced additive group topology on `β`
is the finest topology such that `f` is continuous and `β` is a topological additive group. -/
]
def coinduced {α β : Type*} [t : TopologicalSpace α] [Group β] (f : α → β) : GroupTopology β :=
sInf {b : GroupTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}
