Documentation

Mathlib.CategoryTheory.Monoidal.Mod_

The category of module objects over a monoid object. #

@[deprecated ModObj (since := "2025-09-14")]

Alias of ModObj.


Given an action of a monoidal category C on a category D, an action of a monoid object M in C on an object X in D is the data of a map smul : M ⊙ₗ XX that satisfies unitality and associativity with multiplication.

See MulAction for the non-categorical version.

Equations
Instances For

    The action map

    Equations
    Instances For

      The action map

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The action map

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[reducible, inline]

          The action of a monoid object on itself.

          Equations
          Instances For

            If C acts monoidally on D, then every object of D is canonically a module over the trivial monoid.

            Equations
            theorem ModObj.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [MonObj M] {X : C} (h₁ h₂ : ModObj M X) (H : smul = smul) :
            h₁ = h₂
            theorem ModObj.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [MonObj M] {X : C} {h₁ h₂ : ModObj M X} :
            h₁ = h₂ smul = smul

            A module object for a monoid object in a monoidal category acting on the ambient category.

            • X : D

              The underlying object in the ambient category

            • mod : ModObj A self.X
            Instances For

              A morphism of module objects.

              Instances For
                theorem Mod_.Hom.ext_iff {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {A : C} {inst✝⁴ : MonObj A} {M N : Mod_ D A} {x y : M.Hom N} :
                x = y x.hom = y.hom
                theorem Mod_.Hom.ext {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {A : C} {inst✝⁴ : MonObj A} {M N : Mod_ D A} {x y : M.Hom N} (hom : x.hom = y.hom) :
                x = y

                An alternative constructor for Hom, taking a morphism without a [isMod_Hom] instance, as well as the relevant equality to put such an instance.

                Equations
                Instances For

                  An alternative constructor for Hom, taking a morphism without a [isMod_Hom] instance, between objects with a ModObj instance (rather than bundled as Mod_), as well as the relevant equality to put such an instance.

                  Equations
                  Instances For

                    The identity morphism on a module object.

                    Equations
                    Instances For

                      Composition of module object morphisms.

                      Equations
                      Instances For

                        A monoid object as a module over itself.

                        Equations
                        Instances For

                          The forgetful functor from module objects to the ambient category.

                          Equations
                          Instances For

                            When M is a B-module in D and f : A ⟶ B is a morphism of internal monoid objects, M inherits an A-module structure via "restriction of scalars", i.e γ[A, M] = f.hom ⊵ₗ M ≫ γ[B, M].

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              If g : M ⟶ N is a B-linear morphisms of B-modules, then it induces an A-linear morphism when M and N have an A-module structure obtained by restricting scalars along a monoid morphism A ⟶ B.

                              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