Theorems · Definition · category theory

TopModuleCat.coinduced

{R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {M : ModuleCat R} → {I : Type u_1} → {X : I → TopModuleCat R} → ((i : I) → (X i).toModuleCat ⟶ M) → TopModuleCat R

The coinduced topology on M from a family of continuous linear maps into M, which is the finest topology that makes it into a topological module and makes every map continuous.

Defined in

Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Cited by

0 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingTopologicalSpace