Documentation

Mathlib.CategoryTheory.Monoidal.Mod_

The category of module objects over a monoid object. #

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 Mod_Class.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [Mon_Class M] {X : C} (h₁ h₂ : Mod_Class M X) (H : smul = smul) :
          h₁ = h₂
          theorem Mod_Class.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [Mon_Class M] {X : C} {h₁ h₂ : Mod_Class 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 : Mod_Class 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✝⁴ : Mon_Class 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✝⁴ : Mon_Class 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 Mod_Class 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