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_1 : CategoryTheory.MonoidalCategory C} {A : Mon_ C} {M N : Mod_ A} {x y : M.Hom N}, x.hom = y.homx = y
theorem Mod_.Hom.ext_iff {C : Type u₁} :
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {A : Mon_ C} {M N : Mod_ A} {x y : M.Hom N}, x = y x.hom = y.hom
structure Mod_.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (M : Mod_ A) (N : Mod_ A) :
Type v₁

A morphism of module objects.

Instances For

    The identity morphism on a module object.

    Equations
    Instances For
      Equations
      • M.homInhabited = { default := M.id }
      @[simp]
      theorem Mod_.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M : Mod_ A} {N : Mod_ A} {O : Mod_ A} (f : M.Hom N) (g : N.Hom O) :
      def Mod_.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M : Mod_ A} {N : Mod_ A} {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_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M : Mod_ A} {N : Mod_ A} {f₁ : M N} {f₂ : M N} :
        f₁ = f₂ f₁.hom = f₂.hom
        theorem Mod_.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M : Mod_ A} {N : Mod_ A} (f₁ : M N) (f₂ : M N) (h : f₁.hom = f₂.hom) :
        f₁ = f₂
        @[simp]

        A monoid object as a module over itself.

        Equations
        • Mod_.regular A = { X := A.X, act := A.mul, one_act := , assoc := }
        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
            @[simp]
            theorem Mod_.comap_obj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (f : A B) (M : Mod_ B) :
            ((Mod_.comap f).obj M).X = M.X
            @[simp]
            theorem Mod_.comap_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (f : A B) :
            ∀ {X Y : Mod_ B} (g : X Y), ((Mod_.comap f).map g).hom = g.hom

            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