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:

• TopModuleCat.withModuleTopologyAdj: equipping the module topology is left adjoint to the forgetful functor into ModuleCat R.
• TopModuleCat.indiscreteAdj: equipping the indiscrete topology is right adjoint to the forgetful functor into ModuleCat R.
• TopModuleCat.freeAdj: the free-forgetful adjunction between TopModuleCat R and TopCat.

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.

• carrier : Type v
• isAddCommGroup : AddCommGroup ↑self.toModuleCat
• isModule : Module R ↑self.toModuleCat
• topologicalSpace : TopologicalSpace ↑self.toModuleCat

  The underlying topological space.

• isTopologicalAddGroup : IsTopologicalAddGroup ↑self.toModuleCat
• continuousSMul : ContinuousSMul R ↑self.toModuleCat

@[implicit_reducible]

noncomputable instance TopModuleCat.instCoeSortType (R : Type u) [Ring R] [TopologicalSpace R] : CoeSort (TopModuleCat R) (Type v)

@[reducible, inline]

abbrev TopModuleCat.of (R : Type u) [Ring R] [TopologicalSpace R] (M : Type v) [AddCommGroup M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] : TopModuleCat R

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

theorem TopModuleCat.coe_of (R : Type u) [Ring R] [TopologicalSpace R] (M : Type v) [AddCommGroup M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] : ↑(of R M).toModuleCat = M

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

Homs in TopModuleCat as one field structures over ContinuousLinearMap.

• ofHom' :: (
• hom' : ↑X.toModuleCat →L[R] ↑Y.toModuleCat

  The underlying continuous linear map. Use hom instead.

• )

@[implicit_reducible]

instance TopModuleCat.instCategory (R : Type u) [Ring R] [TopologicalSpace R] : CategoryTheory.Category.{u_1, max u (u_1 + 1)} (TopModuleCat R)

@[implicit_reducible]

instance TopModuleCat.instConcreteCategoryContinuousLinearMapIdCarrier (R : Type u) [Ring R] [TopologicalSpace R] : CategoryTheory.ConcreteCategory (TopModuleCat R) fun (x1 x2 : TopModuleCat R) => ↑x1.toModuleCat →L[R] ↑x2.toModuleCat

@[reducible, inline]

abbrev TopModuleCat.Hom.hom {R : Type u} [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} (f : X.Hom Y) : ↑X.toModuleCat →L[R] ↑Y.toModuleCat

Cast a hom in TopModuleCat into a continuous linear map.

@[reducible, inline]

abbrev TopModuleCat.ofHom {R : Type u} [Ring R] [TopologicalSpace R] {X Y : Type v} [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X] [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y] (f : X →L[R] Y) : of R X ⟶ of R Y

Construct a hom in TopModuleCat from a continuous linear map.

@[simp]

theorem TopModuleCat.hom_ofHom (R : Type u) [Ring R] [TopologicalSpace R] {X Y : Type v} [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X] [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y] (f : X →L[R] Y) : Hom.hom (ofHom f) = f

@[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) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem TopModuleCat.hom_id (R : Type u) [Ring R] [TopologicalSpace R] (X : TopModuleCat R) : CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X) = ContinuousLinearMap.id R ↑X.toModuleCat

def TopModuleCat.Hom.Simps.hom (R : Type u) [Ring R] [TopologicalSpace R] (A B : TopModuleCat R) (f : A.Hom B) : ↑A.toModuleCat →L[R] ↑B.toModuleCat

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

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.

def CategoryTheory.Iso.toContinuousLinearEquiv {R : Type u} [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} (e : X ≅ Y) : ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat

Cast an iso in TopModuleCat into a continuous linear equiv.

@[implicit_reducible]

instance TopModuleCat.instAddCommGroupHom (R : Type u) [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} : AddCommGroup (X ⟶ Y)

@[implicit_reducible]

instance TopModuleCat.instPreadditive (R : Type u) [Ring R] [TopologicalSpace R] : CategoryTheory.Preadditive (TopModuleCat R)

@[simp]

theorem TopModuleCat.hom_zero (R : Type u) [Ring R] [TopologicalSpace R] {M₁ M₂ : TopModuleCat R} : Hom.hom 0 = 0

@[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₂) : Hom.hom (-φ) = -Hom.hom φ

@[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 φ

@[implicit_reducible]

instance TopModuleCat.instModuleHom {S : Type u_1} [CommRing S] [TopologicalSpace S] {X Y : TopModuleCat S} : Module S (X ⟶ Y)

@[implicit_reducible]

instance TopModuleCat.instLinear {S : Type u_1} [CommRing S] [TopologicalSpace S] : CategoryTheory.Linear S (TopModuleCat S)

@[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 φ

@[implicit_reducible]

instance TopModuleCat.instTopologicalSpaceCarrier (R : Type u) [Ring R] [TopologicalSpace R] (M : TopModuleCat R) : TopologicalSpace ↑M.toModuleCat

instance TopModuleCat.instIsTopologicalAddGroupCarrier (R : Type u) [Ring R] [TopologicalSpace R] (M : TopModuleCat R) : IsTopologicalAddGroup ↑M.toModuleCat

@[implicit_reducible]

instance TopModuleCat.instHasForget₂ContinuousLinearMapIdCarrierModuleCatLinearMap (R : Type u) [Ring R] [TopologicalSpace R] : CategoryTheory.HasForget₂ (TopModuleCat R) (ModuleCat R)

@[implicit_reducible]

instance TopModuleCat.instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier (R : Type u) [Ring R] [TopologicalSpace R] : CategoryTheory.HasForget₂ (TopModuleCat R) TopCat

instance TopModuleCat.instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier (R : Type u) [Ring R] [TopologicalSpace R] : (CategoryTheory.forget₂ (TopModuleCat R) TopCat).ReflectsIsomorphisms

@[simp]

theorem TopModuleCat.hom_forget₂_TopCat_map (R : Type u) [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} (f : X ⟶ Y) : TopCat.Hom.hom ((CategoryTheory.forget₂ (TopModuleCat R) TopCat).map f) = ↑(Hom.hom f)

@[simp]

theorem TopModuleCat.forget₂_TopCat_obj (R : Type u) [Ring R] [TopologicalSpace R] {X : TopModuleCat R} : ↑((CategoryTheory.forget₂ (TopModuleCat R) TopCat).obj X) = ↑X.toModuleCat

def TopModuleCat.coinduced {R : Type u} [Ring R] [TopologicalSpace R] {M : ModuleCat R} {I : Type u_1} {X : I → TopModuleCat R} (f : (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.

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

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

def TopModuleCat.ofCocone {R : Type u} [Ring R] [TopologicalSpace R] {J : Type u_2} [CategoryTheory.Category.{v_1, u_2} J] {F : CategoryTheory.Functor J (TopModuleCat R)} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))) : CategoryTheory.Limits.Cocone F

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.

def TopModuleCat.isColimit {R : Type u} [Ring R] [TopologicalSpace R] {J : Type u_2} [CategoryTheory.Category.{v_1, u_2} J] {F : CategoryTheory.Functor J (TopModuleCat R)} {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (ofCocone c)

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

instance TopModuleCat.instHasColimitOfModuleCatCompForget₂ContinuousLinearMapIdCarrierLinearMap {R : Type u} [Ring R] [TopologicalSpace R] {J : Type u_2} [CategoryTheory.Category.{v_1, u_2} J] {F : CategoryTheory.Functor J (TopModuleCat R)} [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))] : CategoryTheory.Limits.HasColimit F

instance TopModuleCat.instHasColimitsOfShapeOfModuleCat {R : Type u} [Ring R] [TopologicalSpace R] {J : Type u_2} [CategoryTheory.Category.{v_1, u_2} J] [CategoryTheory.Limits.HasColimitsOfShape J (ModuleCat R)] : CategoryTheory.Limits.HasColimitsOfShape J (TopModuleCat R)

instance TopModuleCat.instHasColimits {R : Type u} [Ring R] [TopologicalSpace R] : CategoryTheory.Limits.HasColimits (TopModuleCat R)

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

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

def TopModuleCat.fromInduced {R : Type u} [Ring R] [TopologicalSpace R] {M : ModuleCat R} {I : Type u_1} {X : I → TopModuleCat 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.

def TopModuleCat.ofCone {R : Type u} [Ring R] [TopologicalSpace R] {J : Type u_2} [CategoryTheory.Category.{v_1, u_2} J] {F : CategoryTheory.Functor J (TopModuleCat R)} (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))) : CategoryTheory.Limits.Cone F

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.

def TopModuleCat.isLimit {R : Type u} [Ring R] [TopologicalSpace R] {J : Type u_2} [CategoryTheory.Category.{v_1, u_2} J] {F : CategoryTheory.Functor J (TopModuleCat R)} {c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (ofCone c)

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

instance TopModuleCat.hasLimit_of_hasLimit_forget₂ {R : Type u} [Ring R] [TopologicalSpace R] {J : Type u_2} [CategoryTheory.Category.{v_1, u_2} J] {F : CategoryTheory.Functor J (TopModuleCat R)} [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))] : CategoryTheory.Limits.HasLimit F

instance TopModuleCat.instHasLimitsOfShapeOfModuleCat {R : Type u} [Ring R] [TopologicalSpace R] {J : Type u_2} [CategoryTheory.Category.{v_1, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J (ModuleCat R)] : CategoryTheory.Limits.HasLimitsOfShape J (TopModuleCat R)

instance TopModuleCat.instHasLimits {R : Type u} [Ring R] [TopologicalSpace R] : CategoryTheory.Limits.HasLimits (TopModuleCat R)

instance TopModuleCat.instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget {R : Type u} [Ring R] [TopologicalSpace R] {J : Type u_2} [CategoryTheory.Category.{v_1, u_2} J] {F : CategoryTheory.Functor J (TopModuleCat R)} [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))] [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R))) (CategoryTheory.forget (ModuleCat R))] : CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ (TopModuleCat R) TopCat)

instance TopModuleCat.instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap {R : Type u} [Ring R] [TopologicalSpace R] {J : Type u_2} [CategoryTheory.Category.{v_1, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J (ModuleCat R)] [CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget (ModuleCat R))] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ (TopModuleCat R) TopCat)

instance TopModuleCat.instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier {R : Type u} [Ring R] [TopologicalSpace R] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (TopModuleCat R) TopCat)

def TopModuleCat.withModuleTopology (R : Type u) [Ring R] [TopologicalSpace R] : CategoryTheory.Functor (ModuleCat R) (TopModuleCat R)

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.

def TopModuleCat.withModuleTopologyAdj (R : Type u) [Ring R] [TopologicalSpace R] : withModuleTopology R ⊣ CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)

The adjunction between withModuleTopology and the forgetful functor.

instance TopModuleCat.instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap (R : Type u) [Ring R] [TopologicalSpace R] : (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).IsRightAdjoint

instance TopModuleCat.instIsLeftAdjointModuleCatWithModuleTopology (R : Type u) [Ring R] [TopologicalSpace R] : (withModuleTopology R).IsLeftAdjoint

def TopModuleCat.indiscrete (R : Type u) [Ring R] [TopologicalSpace R] : CategoryTheory.Functor (ModuleCat R) (TopModuleCat R)

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

def TopModuleCat.indiscreteAdj (R : Type u) [Ring R] [TopologicalSpace R] : CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R) ⊣ indiscrete R

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

instance TopModuleCat.instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap (R : Type u) [Ring R] [TopologicalSpace R] : (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).IsLeftAdjoint

instance TopModuleCat.instIsRightAdjointModuleCatIndiscrete (R : Type u) [Ring R] [TopologicalSpace R] : (indiscrete R).IsRightAdjoint

noncomputable def TopModuleCat.freeObj (R : Type u) [Ring R] [TopologicalSpace R] (X : TopCat) : TopModuleCat R

The free topological module over a topological space.

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) : freeObj R X ⟶ freeObj R Y

The free topological module over a topological space is functorial.

theorem TopModuleCat.freeMap_map (R : Type u) [Ring R] [TopologicalSpace R] {X Y : TopCat} (f : X ⟶ Y) (v : ↑X →₀ R) : (CategoryTheory.ConcreteCategory.hom (freeMap R f)) v = Finsupp.mapDomain (⇑(TopCat.Hom.hom f)) v

noncomputable def TopModuleCat.free (R : Type u) [Ring R] [TopologicalSpace R] : CategoryTheory.Functor TopCat (TopModuleCat R)

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

@[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

noncomputable def TopModuleCat.freeAdj (R : Type u) [Ring R] [TopologicalSpace R] : free R ⊣ CategoryTheory.forget₂ (TopModuleCat R) TopCat

The free-forgetful adjoint for TopModuleCat R.

instance TopModuleCat.instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier (R : Type u) [Ring R] [TopologicalSpace R] : (CategoryTheory.forget₂ (TopModuleCat R) TopCat).IsRightAdjoint

instance TopModuleCat.instIsLeftAdjointTopCatFree (R : Type u) [Ring R] [TopologicalSpace R] : (free R).IsLeftAdjoint