Documentation

TauCeti.CategoryTheory.Monoidal.Mod.Bimodule

Modules over a commutative monoid as bimodules #

A left module over a commutative monoid object has a canonical right action, obtained by moving the scalar past the module through the braiding. The two actions commute, so this gives a native bimodule. Module maps respect both actions. This adapter allows balanced tensor products of modules to use Mathlib's Bimod.TensorBimod construction rather than a second coequalizer construction.

The construction uses the inverse braiding from the scalar to the module; in a symmetric monoidal category it is also the forward braiding in the opposite order. No colimit or closedness assumptions are needed.

source
@[reducible, inline]
abbrev CategoryTheory.Bimod.toLeftMod {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : Mon C) :
Functor (Bimod A B) (Mod C A.X)

Forget the right action of a bimodule, retaining its native left module.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Bimod.toLeftMod_obj_X {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : Mon C) (M : Bimod A B) :
    ((toLeftMod A B).obj M).X = M.X
    source
    @[simp]
    theorem CategoryTheory.Bimod.toLeftMod_smul {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : Mon C) (M : Bimod A B) :
    ModObj.smul = M.actLeft

    The left action is unchanged when forgetting the right action.

    source
    @[reducible, inline]
    abbrev CategoryTheory.Mod.toBimod {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] :
    Functor (Mod C A) (Bimod { X := A, mon := inst✝ } { X := A, mon := inst✝ })

    Regard modules over a commutative monoid object as bimodules. The right action moves the scalar to the left using the inverse braiding.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Mod.toBimod_obj_X {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) :
      (toBimod.obj M).X = M.X
      source
      @[simp]
      theorem CategoryTheory.Mod.toBimod_obj_actLeft {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) :
      (toBimod.obj M).actLeft = ModObj.smul
      source
      @[simp]
      theorem CategoryTheory.Mod.toBimod_obj_actRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) :
      (toBimod.obj M).actRight = CategoryStruct.comp (β_ A M.X).inv ModObj.smul
      source
      @[simp]
      theorem CategoryTheory.Mod.toBimod_map_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] {M N : Mod C A} (f : M ⟶ N) :
      (toBimod.map f).hom = f.hom
      source
      def CategoryTheory.Mod.fullyFaithfulToBimod {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] :
      toBimod.FullyFaithful

      A bimodule map between the canonical bimodules is determined by, and uniquely lifts, a left-module map.

      Instances For
        source
        instance CategoryTheory.Mod.instFullBimodMkToBimod {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] :
        toBimod.Full
        source
        instance CategoryTheory.Mod.instFaithfulBimodMkToBimod {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] :
        toBimod.Faithful
        source
        def CategoryTheory.Mod.toBimodCompToLeftModIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] :
        toBimod.comp (Bimod.toLeftMod { X := A, mon := inst✝ } { X := A, mon := inst✝ }) ≅ Functor.id (Mod C A)

        Forgetting the added right action recovers the original module functorially.

        Instances For
          source
          @[simp]
          theorem CategoryTheory.Mod.toBimodCompToLeftModIso_hom_app_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) :
          (toBimodCompToLeftModIso.hom.app M).hom = CategoryStruct.id M.X
          source
          @[simp]
          theorem CategoryTheory.Mod.toBimodCompToLeftModIso_inv_app_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) :
          (toBimodCompToLeftModIso.inv.app M).hom = CategoryStruct.id M.X
          source
          def CategoryTheory.Mod.toBimodRegularIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] :
          toBimod.obj (regular A) ≅ Bimod.regular { X := A, mon := inst✝ }

          For the regular left module, the added right action is multiplication.

          Instances For
            source
            @[simp]
            theorem CategoryTheory.Mod.toBimodRegularIso_hom_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] :
            toBimodRegularIso.hom.hom = eqToHom ⋯
            source
            @[simp]
            theorem CategoryTheory.Mod.toBimodRegularIso_inv_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] :
            toBimodRegularIso.inv.hom = eqToHom ⋯
            source
            def CategoryTheory.Bimod.toLeftModToBimodIsoOfActRightEq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] (M : Bimod { X := A, mon := inst✝ } { X := A, mon := inst✝ }) (h : M.actRight = CategoryStruct.comp (β_ A M.X).inv M.actLeft) :
            Mod.toBimod.obj ((toLeftMod { X := A, mon := inst✝ } { X := A, mon := inst✝ }).obj M) ≅ M

            A bimodule whose right action is induced from its left action is recovered from that left module. Both comparison maps are the identity on the carrier.

            Instances For
              source
              @[simp]
              theorem CategoryTheory.Bimod.toLeftModToBimodIsoOfActRightEq_hom_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] (M : Bimod { X := A, mon := inst✝ } { X := A, mon := inst✝ }) (h : M.actRight = CategoryStruct.comp (β_ A M.X).inv M.actLeft) :
              (toLeftModToBimodIsoOfActRightEq M h).hom.hom = CategoryStruct.id M.X
              source
              @[simp]
              theorem CategoryTheory.Bimod.toLeftModToBimodIsoOfActRightEq_inv_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {A : C} [MonObj A] [IsCommMonObj A] (M : Bimod { X := A, mon := inst✝ } { X := A, mon := inst✝ }) (h : M.actRight = CategoryStruct.comp (β_ A M.X).inv M.actLeft) :
              (toLeftModToBimodIsoOfActRightEq M h).inv.hom = CategoryStruct.id M.X