Documentation

Mathlib.CategoryTheory.Monoidal.Mod_

The category of module objects over a monoid object. #

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
    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
        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]