Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Module objects in cartesian monoidal categories #

In this file we study module objects in a cartesian monoidal category C action on itself by ⊗.

In particular, for a monoid object M : C action on X : C, we equip Z ⟶ X with a M ⟶ X action for every Z : C.

source
@[reducible]
def CategoryTheory.ModObj.trivialAction {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : C) [MonObj M] (X : C) :
ModObj M X

Every object is a module over a monoid object via the trivial action.

Equations
Instances For
    source
    def CategoryTheory.Mod.trivialAction {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : Mon C) (X : C) :
    Mod C M.X

    Every object is a module over a monoid object via the trivial action.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Mod.trivialAction_mod_smul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : Mon C) (X : C) :
      ModObj.smul = SemiCartesianMonoidalCategory.snd M.X X
      source
      @[simp]
      theorem CategoryTheory.Mod.trivialAction_X {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : Mon C) (X : C) :
      (trivialAction M X).X = X
      source
      @[instance_reducible]
      instance CategoryTheory.Hom.instSMulHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Y : C) :
      SMul (Y ⟶ M) (Y ⟶ X)

      Morphisms Y ⟶ M act on morphisms Y ⟶ X via the internal scalar multiplication.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance CategoryTheory.Hom.instVAddHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] (Y : C) :
      VAdd (Y ⟶ M) (Y ⟶ X)

      Morphisms Y ⟶ M act on morphisms Y ⟶ X via the internal additive action.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      theorem CategoryTheory.Hom.vadd_def {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] (Y : C) (m : Y ⟶ M) (x : Y ⟶ X) :
      m +ᵥ x = CategoryStruct.comp (CartesianMonoidalCategory.lift m x) AddModObj.vadd
      source
      theorem CategoryTheory.Hom.smul_def {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Y : C) (m : Y ⟶ M) (x : Y ⟶ X) :
      m • x = CategoryStruct.comp (CartesianMonoidalCategory.lift m x) ModObj.smul
      source
      @[instance_reducible]
      instance CategoryTheory.Hom.mulAction {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Z : C) :
      MulAction (Z ⟶ M) (Z ⟶ X)

      If M is a monoid object acting on X, then morphisms into M act on morphisms into X.

      Equations
      source
      @[instance_reducible]
      instance CategoryTheory.Hom.addAction {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] (Z : C) :
      AddAction (Z ⟶ M) (Z ⟶ X)

      If M is an additive monoid object acting on X, then morphisms into M act on morphisms into X.

      Equations
      source
      theorem CategoryTheory.ModObj.comp_smul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Z Z' : C} (g : Z' ⟶ Z) (m : Z ⟶ M) (x : Z ⟶ X) :
      CategoryStruct.comp g (m • x) = CategoryStruct.comp g m • CategoryStruct.comp g x
      source
      @[simp]
      theorem CategoryTheory.IsModHom.map_smul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Y : C} [ModObj M Y] (f : X ⟶ Y) [IsModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) :
      CategoryStruct.comp (m • x) f = m • CategoryStruct.comp x f
      source
      @[simp]
      theorem CategoryTheory.IsAddModHom.map_vadd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] {Y : C} [AddModObj M Y] (f : X ⟶ Y) [IsAddModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) :
      CategoryStruct.comp (m +ᵥ x) f = m +ᵥ CategoryStruct.comp x f
      source
      @[simp]
      theorem CategoryTheory.IsAddModHom.map_vadd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] {Y : C} [AddModObj M Y] (f : X ⟶ Y) [IsAddModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) {Z✝ : C} (h : Y ⟶ Z✝) :
      CategoryStruct.comp (m +ᵥ x) (CategoryStruct.comp f h) = CategoryStruct.comp (m +ᵥ CategoryStruct.comp x f) h
      source
      @[simp]
      theorem CategoryTheory.IsModHom.map_smul_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Y : C} [ModObj M Y] (f : X ⟶ Y) [IsModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) {Z✝ : C} (h : Y ⟶ Z✝) :
      CategoryStruct.comp (m • x) (CategoryStruct.comp f h) = CategoryStruct.comp (m • CategoryStruct.comp x f) h
      source
      def CategoryTheory.IsModHom.mulActionHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Y : C} [ModObj M Y] (f : X ⟶ Y) [IsModHom M f] (Z : C) :
      (Z ⟶ X) →ₑ[id] Z ⟶ Y

      An M-equivariant morphism induces an equivariant function on hom types.

      Equations
      Instances For
        source
        def CategoryTheory.IsAddModHom.addActionHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] {Y : C} [AddModObj M Y] (f : X ⟶ Y) [IsAddModHom M f] (Z : C) :
        (Z ⟶ X) →ₑ[id] Z ⟶ Y

        A φ-equivariant morphism induces an equivariant morphism on hom types.

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.IsAddModHom.addActionHom_apply {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] {Y : C} [AddModObj M Y] (f : X ⟶ Y) [IsAddModHom M f] (Z : C) (x✝ : Z ⟶ X) :
          (addActionHom f Z) x✝ = CategoryStruct.comp x✝ f
          source
          @[simp]
          theorem CategoryTheory.IsModHom.mulActionHom_apply {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Y : C} [ModObj M Y] (f : X ⟶ Y) [IsModHom M f] (Z : C) (x✝ : Z ⟶ X) :
          (mulActionHom f Z) x✝ = CategoryStruct.comp x✝ f
          source
          def CategoryTheory.ModObj.leftSMul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : C) [MonObj M] (X : C) [ModObj M X] :
          MonoidalCategoryStruct.tensorObj M X ⟶ MonoidalCategoryStruct.tensorObj X X

          The morphism (m, x) ↦ (m • x, x).

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.ModObj.leftSMul_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] :
            CategoryStruct.comp (leftSMul M X) (SemiCartesianMonoidalCategory.fst X X) = smul
            source
            @[simp]
            theorem CategoryTheory.ModObj.leftSMul_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Z : C} (h : X ⟶ Z) :
            CategoryStruct.comp (leftSMul M X) (CategoryStruct.comp (SemiCartesianMonoidalCategory.fst X X) h) = CategoryStruct.comp smul h
            source
            @[simp]
            theorem CategoryTheory.ModObj.leftSMul_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] :
            CategoryStruct.comp (leftSMul M X) (SemiCartesianMonoidalCategory.snd X X) = SemiCartesianMonoidalCategory.snd M X
            source
            @[simp]
            theorem CategoryTheory.ModObj.leftSMul_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Z : C} (h : X ⟶ Z) :
            CategoryStruct.comp (leftSMul M X) (CategoryStruct.comp (SemiCartesianMonoidalCategory.snd X X) h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.snd M X) h
            source
            theorem CategoryTheory.ModObj.lift_leftSMul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Z : C) (x : Z ⟶ X) (m : Z ⟶ M) :
            CategoryStruct.comp (CartesianMonoidalCategory.lift m x) (leftSMul M X) = CartesianMonoidalCategory.lift (m • x) x
            source
            theorem CategoryTheory.ModObj.lift_leftSMul_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Z : C) (x : Z ⟶ X) (m : Z ⟶ M) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj X X ⟶ Z✝) :
            CategoryStruct.comp (CartesianMonoidalCategory.lift m x) (CategoryStruct.comp (leftSMul M X) h) = CategoryStruct.comp (CartesianMonoidalCategory.lift (m • x) x) h
            source
            theorem CategoryTheory.ModObj.lift_leftSMul_eq_lift_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Z : C) (x y : Z ⟶ X) (m : Z ⟶ M) :
            CategoryStruct.comp (CartesianMonoidalCategory.lift m x) (leftSMul M X) = CartesianMonoidalCategory.lift y x ↔ m • x = y
            source
            theorem CategoryTheory.ModObj.isIso_leftSMul_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] :
            IsIso (leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y

            The morphism (m, x) ↦ (m • x, x) is an isomorphism if and only if the induced action is pointwise simply transitive.