Documentation

Mathlib.CategoryTheory.Monoidal.Mod_

The category of module objects over a monoid object. #

structure Mod_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) :
Type (max u₁ v₁)

A module object for a monoid object, all internal to some monoidal category.

Instances For

    A morphism of module objects.

    Instances For
      theorem Mod_.Hom.ext {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {A : Mon_ C} {M N : Mod_ A} {x y : M.Hom N} (hom : x.hom = y.hom) :
      x = y

      The identity morphism on a module object.

      Equations
      Instances For
        Equations
        def Mod_.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M N O : Mod_ A} (f : M.Hom N) (g : N.Hom O) :
        M.Hom O

        Composition of module object morphisms.

        Equations
        Instances For
          theorem Mod_.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M N : Mod_ A} (f₁ f₂ : M N) (h : f₁.hom = f₂.hom) :
          f₁ = f₂

          A monoid object as a module over itself.

          Equations
          Instances For

            The forgetful functor from module objects to the ambient category.

            Equations
            • Mod_.forget A = { obj := fun (A_1 : Mod_ A) => A_1.X, map := fun {X Y : Mod_ A} (f : X Y) => f.hom, map_id := , map_comp := }
            Instances For

              A morphism of monoid objects induces a "restriction" or "comap" functor between the categories of module objects.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem Mod_.comap_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : Mon_ C} (f : A B) {X✝ Y✝ : Mod_ B} (g : X✝ Y✝) :
                ((comap f).map g).hom = g.hom
                @[simp]
                theorem Mod_.comap_obj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : Mon_ C} (f : A B) (M : Mod_ B) :
                ((comap f).obj M).X = M.X