Documentation

Mathlib.Algebra.Category.ModuleCat.Topology.Basic

The category TopModuleCat R of topological modules #

We define TopModuleCat R, the category of topological modules, and show that it has all limits and colimits.

We also provide various adjunctions:

Future projects #

Show that the forgetful functor to TopCat preserves filtered colimits.

structure TopModuleCat (R : Type u) [Ring R] [TopologicalSpace R] extends ModuleCat R :
Type (max u (v + 1))

The category of topological modules.

noncomputable instance TopModuleCat.instCoeSortType (R : Type u) [Ring R] [TopologicalSpace R] :
Equations
@[reducible, inline]

Make an object in TopModuleCat R from an unbundled topological module.

Equations
structure TopModuleCat.Hom {R : Type u} [Ring R] [TopologicalSpace R] (X Y : TopModuleCat R) :

Homs in TopModuleCat as one field structures over ContinuousLinearMap.

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev TopModuleCat.Hom.hom {R : Type u} [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} (f : X.Hom Y) :

Cast a hom in TopModuleCat into a continuous linear map.

Equations
@[reducible, inline]

Construct a hom in TopModuleCat from a continuous linear map.

Equations
@[simp]
theorem TopModuleCat.ofHom_hom (R : Type u) [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} (f : X.Hom Y) :
ofHom f.hom = f
@[simp]
theorem TopModuleCat.hom_comp (R : Type u) [Ring R] [TopologicalSpace R] {X Y Z : TopModuleCat R} (f : X Y) (g : Y Z) :

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations
def TopModuleCat.ofIso {R : Type u} [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} (e : X.toModuleCat ≃L[R] Y.toModuleCat) :
X Y

Construct an iso in TopModuleCat from a continuous linear equiv.

Equations

Cast an iso in TopModuleCat into a continuous linear equiv.

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
@[simp]
theorem TopModuleCat.hom_zero (R : Type u) [Ring R] [TopologicalSpace R] {M₁ M₂ : TopModuleCat R} :
@[simp]
theorem TopModuleCat.hom_zero_apply (R : Type u) [Ring R] [TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (m : M₁.toModuleCat) :
(Hom.hom 0) m = 0
@[simp]
theorem TopModuleCat.hom_add (R : Type u) [Ring R] [TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (φ₁ φ₂ : M₁ M₂) :
Hom.hom (φ₁ + φ₂) = Hom.hom φ₁ + Hom.hom φ₂
@[simp]
theorem TopModuleCat.hom_neg (R : Type u) [Ring R] [TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (φ : M₁ M₂) :
@[simp]
theorem TopModuleCat.hom_sub (R : Type u) [Ring R] [TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (φ₁ φ₂ : M₁ M₂) :
Hom.hom (φ₁ - φ₂) = Hom.hom φ₁ - Hom.hom φ₂
@[simp]
theorem TopModuleCat.hom_nsmul (R : Type u) [Ring R] [TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (n : ) (φ : M₁ M₂) :
Hom.hom (n φ) = n Hom.hom φ
@[simp]
theorem TopModuleCat.hom_zsmul (R : Type u) [Ring R] [TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (n : ) (φ : M₁ M₂) :
Hom.hom (n φ) = n Hom.hom φ
instance TopModuleCat.instModuleHom {S : Type u_1} [CommRing S] [TopologicalSpace S] {X Y : TopModuleCat S} :
Module S (X Y)
Equations
  • One or more equations did not get rendered due to their size.
Equations
@[simp]
theorem TopModuleCat.hom_smul {S : Type u_1} [CommRing S] [TopologicalSpace S] {M₁ M₂ : TopModuleCat S} (s : S) (φ : M₁ M₂) :
Hom.hom (s φ) = s Hom.hom φ
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def TopModuleCat.coinduced {R : Type u} [Ring R] [TopologicalSpace R] {M : ModuleCat R} {I : Type u_1} {X : ITopModuleCat R} (f : (i : I) → (X i).toModuleCat M) :

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

Equations
def TopModuleCat.toCoinduced {R : Type u} [Ring R] [TopologicalSpace R] {M : ModuleCat R} {I : Type u_1} {X : ITopModuleCat R} (f : (i : I) → (X i).toModuleCat M) (i : I) :

The maps into the coinduced topology as homs in TopModuleCat R.

Equations

The cocone of topological modules associated to a cocone over the underlying modules, where the cocone point is given the coinduced topology. This is colimiting when the given cocone is.

Equations

Given a colimit cocone over the underlying modules, equipping the cocone point with the coinduced topology gives a colimit cocone in TopModuleCat R.

Equations
  • One or more equations did not get rendered due to their size.
def TopModuleCat.induced {R : Type u} [Ring R] [TopologicalSpace R] {M : ModuleCat R} {I : Type u_1} {X : ITopModuleCat R} (f : (i : I) → M (X i).toModuleCat) :

The induced topology on M from a family of continuous linear map from M, which is the coarsest topology that makes every map continuous.

Equations
def TopModuleCat.fromInduced {R : Type u} [Ring R] [TopologicalSpace R] {M : ModuleCat R} {I : Type u_1} {X : ITopModuleCat R} (f : (i : I) → M (X i).toModuleCat) (i : I) :
induced f X i

The maps from the induced topology as homs in TopModuleCat R.

Equations

The cone of topological modules associated to a cone over the underlying modules, where the cone point is given the induced topology. This is limiting when the given cone is.

Equations

Given a limit cone over the underlying modules, equipping the cone point with the induced topology gives a limit cone in TopModuleCat R.

Equations
  • One or more equations did not get rendered due to their size.

The functor equipping a module over a topological ring with the finest possible topology making it into a topological module. This is left adjoint to the forgetful functor.

Equations
  • One or more equations did not get rendered due to their size.

The adjunction between withModuleTopology and the forgetful functor.

Equations
  • One or more equations did not get rendered due to their size.

The functor equipping a module with the indiscrete topology. This is right adjoint to the forgetful functor.

Equations
  • One or more equations did not get rendered due to their size.

The adjunction between the forgetful functor and the indiscrete topology functor.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def TopModuleCat.freeObj (R : Type u) [Ring R] [TopologicalSpace R] (X : TopCat) :

The free topological module over a topological space.

Equations
theorem TopModuleCat.coe_freeObj (R : Type u) [Ring R] [TopologicalSpace R] (X : TopCat) :
(freeObj R X).toModuleCat = (X →₀ R)
noncomputable def TopModuleCat.freeMap (R : Type u) [Ring R] [TopologicalSpace R] {X Y : TopCat} (f : X Y) :

The free topological module over a topological space is functorial.

Equations

The free topological module over a topological space as a functor. This is left adjoint to the forgetful functor.

Equations
@[simp]
theorem TopModuleCat.free_map (R : Type u) [Ring R] [TopologicalSpace R] {X✝ Y✝ : TopCat} (f : X✝ Y✝) :
(free R).map f = freeMap R f
@[simp]
theorem TopModuleCat.free_obj (R : Type u) [Ring R] [TopologicalSpace R] (X : TopCat) :
(free R).obj X = freeObj R X

The free-forgetful adjoint for TopModuleCat R.

Equations
  • One or more equations did not get rendered due to their size.