The category of module objects over a monoid object.

structure Mod_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : Type (max u₁ v₁)

A module object for a monoid object, all internal to some monoidal category.

• X : C

  The underlying object in the ambient monoidal category

• smul : CategoryTheory.MonoidalCategoryStruct.tensorObj A.X self.X ⟶ self.X

  The action morphism of the module object

• one_smul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.one self.X) self.smul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor self.X).hom
• assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.mul self.X) self.smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.smul) self.smul)

@[simp]

theorem Mod_.assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (self : Mod_ A) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.mul self.X) (CategoryTheory.CategoryStruct.comp self.smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.smul) (CategoryTheory.CategoryStruct.comp self.smul h))

@[simp]

theorem Mod_.one_smul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (self : Mod_ A) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.one self.X) (CategoryTheory.CategoryStruct.comp self.smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor self.X).hom h

theorem Mod_.assoc_flip {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (M : Mod_ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X M.smul) M.smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.mul M.X) M.smul)

structure Mod_.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (M N : Mod_ A) : Type v₁

A morphism of module objects.

• hom : M.X ⟶ N.X

  The underlying morphism

• smul_hom : CategoryTheory.CategoryStruct.comp M.smul self.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.hom) N.smul

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

theorem Mod_.Hom.ext_iff {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} : x = y ↔ x.hom = y.hom

@[simp]

theorem Mod_.Hom.smul_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M N : Mod_ A} (self : M.Hom N) {Z : C} (h : N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.smul (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.hom) (CategoryTheory.CategoryStruct.comp N.smul h)

def Mod_.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (M : Mod_ A) : M.Hom M

The identity morphism on a module object.

Equations

• M.id = { hom := CategoryTheory.CategoryStruct.id M.X, smul_hom := ⋯ }

@[simp]

theorem Mod_.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (M : Mod_ A) : M.id.hom = CategoryTheory.CategoryStruct.id M.X

instance Mod_.homInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (M : Mod_ A) : Inhabited (M.Hom M)

Equations

• M.homInhabited = { default := M.id }

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

• Mod_.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, smul_hom := ⋯ }

@[simp]

theorem Mod_.comp_hom {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) : (comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

instance Mod_.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} : CategoryTheory.Category.{v₁, max u₁ v₁} (Mod_ A)

Equations

• Mod_.instCategory = { Hom := fun (M N : Mod_ A) => M.Hom N, id := Mod_.id, comp := fun {X Y Z : Mod_ A} (f : X.Hom Y) (g : Y.Hom Z) => Mod_.comp f g, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

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₂

theorem Mod_.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M N : Mod_ A} {f₁ f₂ : M ⟶ N} : f₁ = f₂ ↔ f₁.hom = f₂.hom

@[simp]

theorem Mod_.id_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (M : Mod_ A) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X

@[simp]

theorem Mod_.comp_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M N K : Mod_ A} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

def Mod_.regular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : Mod_ A

A monoid object as a module over itself.

Equations

• Mod_.regular A = { X := A.X, smul := Mon_Class.mul, one_smul := ⋯, assoc := ⋯ }

@[simp]

theorem Mod_.regular_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : (regular A).smul = Mon_Class.mul

@[simp]

theorem Mod_.regular_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : (regular A).X = A.X

instance Mod_.instInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : Inhabited (Mod_ A)

Equations

• Mod_.instInhabited A = { default := Mod_.regular A }

def Mod_.forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : CategoryTheory.Functor (Mod_ A) C

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 := ⋯ }

def Mod_.comap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : Mon_ C} (f : A ⟶ B) : CategoryTheory.Functor (Mod_ B) (Mod_ A)

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.

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

theorem Mod_.comap_obj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : Mon_ C} (f : A ⟶ B) (M : Mod_ B) : ((comap f).obj M).X = M.X

@[simp]

theorem Mod_.comap_obj_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : Mon_ C} (f : A ⟶ B) (M : Mod_ B) : ((comap f).obj M).smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom M.X) M.smul

class Mod_Class {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [Mon_Class M] (X : C) : Type v₁

An action of a monoid object M on an object X is the data of a map smul : M ⊗ X ⟶ X that satisfies unitality and associativity with multiplication.

See MulAction for the non-categorical version.

• smul : CategoryTheory.MonoidalCategoryStruct.tensorObj M X ⟶ X

  The action map

• one_smul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.one X) smul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom

  The identity acts trivially.

• mul_smul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.mul X) smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M smul) smul)

  The action map is compatible with multiplication.

@[simp]

theorem Mod_Class.one_smul_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M : C} {inst✝² : Mon_Class M} (X : C) [self : Mod_Class M X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.one X) (CategoryTheory.CategoryStruct.comp smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h

@[simp]

theorem Mod_Class.mul_smul_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M : C} {inst✝² : Mon_Class M} (X : C) [self : Mod_Class M X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.mul X) (CategoryTheory.CategoryStruct.comp smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M smul) (CategoryTheory.CategoryStruct.comp smul h))

def Mon_Class.termγ : Lean.ParserDescr

The action map

Equations

• Mon_Class.termγ = Lean.ParserDescr.node `Mon_Class.termγ 1024 (Lean.ParserDescr.symbol "γ")

def Mon_Class.«termγ[_]» : Lean.ParserDescr

The action map

Equations

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

theorem Mod_Class.assoc_flip {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [Mon_Class M] (X : C) [Mod_Class M X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M smul) smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.mul X) smul)

@[reducible, inline]

abbrev Mod_Class.regular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [Mon_Class M] : Mod_Class M M

The action of a monoid object on itself.

Equations

• Mod_Class.regular M = { smul := Mon_Class.mul, one_smul := ⋯, mul_smul := ⋯ }

instance Mod_Class.instXX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (M : Mod_ A) : Mod_Class A.X M.X

Equations

• Mod_Class.instXX M = { smul := M.smul, one_smul := ⋯, mul_smul := ⋯ }

def Mod_.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [Mon_Class M] (X : C) [Mod_Class M X] : Mod_ { X := M, mon := inst✝ }

Construct an object of Mod_ (Mon_.mk' M) from an object X : C and a Mod_Class M X instance.

Equations

• Mod_.mk' M X = { X := X, smul := Mod_Class.smul, one_smul := ⋯, assoc := ⋯ }

@[simp]

theorem Mod_.mk'_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [Mon_Class M] (X : C) [Mod_Class M X] : (mk' M X).smul = Mod_Class.smul

@[simp]

theorem Mod_.mk'_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [Mon_Class M] (X : C) [Mod_Class M X] : (mk' M X).X = X