# The category of module objects over a monoid object. #

structure Mod_ {C : Type u₁} [] (A : Mon_ C) :
Type (max u₁ v₁)

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

Instances For
@[simp]
theorem Mod_.one_act {C : Type u₁} [] {A : Mon_ C} (self : Mod_ A) :
@[simp]
theorem Mod_.one_act_assoc {C : Type u₁} [] {A : Mon_ C} (self : Mod_ A) {Z : C} (h : self.X Z) :
theorem Mod_.assoc_flip {C : Type u₁} [] {A : Mon_ C} (M : Mod_ A) :
theorem Mod_.Hom.ext {C : Type u₁} :
∀ {inst : } {inst_1 : } {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 : } {inst_1 : } {A : Mon_ C} {M N : Mod_ A} (x y : M.Hom N), x = y x.hom = y.hom
structure Mod_.Hom {C : Type u₁} [] {A : Mon_ C} (M : Mod_ A) (N : Mod_ A) :
Type v₁

A morphism of module objects.

Instances For
@[simp]
theorem Mod_.Hom.act_hom {C : Type u₁} [] {A : Mon_ C} {M : Mod_ A} {N : Mod_ A} (self : M.Hom N) :
@[simp]
theorem Mod_.Hom.act_hom_assoc {C : Type u₁} [] {A : Mon_ C} {M : Mod_ A} {N : Mod_ A} (self : M.Hom N) {Z : C} (h : N.X Z) :
@[simp]
theorem Mod_.id_hom {C : Type u₁} [] {A : Mon_ C} (M : Mod_ A) :
M.id.hom =
def Mod_.id {C : Type u₁} [] {A : Mon_ C} (M : Mod_ A) :
M.Hom M

The identity morphism on a module object.

Equations
• M.id = { hom := , act_hom := }
Instances For
instance Mod_.homInhabited {C : Type u₁} [] {A : Mon_ C} (M : Mod_ A) :
Inhabited (M.Hom M)
Equations
• M.homInhabited = { default := M.id }
@[simp]
theorem Mod_.comp_hom {C : Type u₁} [] {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₁} [] {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
instance Mod_.instCategory {C : Type u₁} [] {A : Mon_ C} :
Equations
• Mod_.instCategory =
theorem Mod_.hom_ext {C : Type u₁} [] {A : Mon_ C} {M : Mod_ A} {N : Mod_ A} (f₁ : M N) (f₂ : M N) (h : f₁.hom = f₂.hom) :
f₁ = f₂
@[simp]
theorem Mod_.id_hom' {C : Type u₁} [] {A : Mon_ C} (M : Mod_ A) :
@[simp]
theorem Mod_.comp_hom' {C : Type u₁} [] {A : Mon_ C} {M : Mod_ A} {N : Mod_ A} {K : Mod_ A} (f : M N) (g : N K) :
@[simp]
theorem Mod_.regular_X {C : Type u₁} [] (A : Mon_ C) :
().X = A.X
@[simp]
theorem Mod_.regular_act {C : Type u₁} [] (A : Mon_ C) :
().act = A.mul
def Mod_.regular {C : Type u₁} [] (A : Mon_ C) :

A monoid object as a module over itself.

Equations
• = { X := A.X, act := A.mul, one_act := , assoc := }
Instances For
instance Mod_.instInhabited {C : Type u₁} [] (A : Mon_ C) :
Equations
• = { default := }
def Mod_.forget {C : Type u₁} [] (A : Mon_ C) :

The forgetful functor from module objects to the ambient category.

Equations
• = { 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_map_hom {C : Type u₁} [] {A : Mon_ C} {B : Mon_ C} (f : A B) :
∀ {X Y : Mod_ B} (g : X Y), (().map g).hom = g.hom
@[simp]
theorem Mod_.comap_obj_X {C : Type u₁} [] {A : Mon_ C} {B : Mon_ C} (f : A B) (M : Mod_ B) :
(().obj M).X = M.X
@[simp]
theorem Mod_.comap_obj_act {C : Type u₁} [] {A : Mon_ C} {B : Mon_ C} (f : A B) (M : Mod_ B) :
(().obj M).act =
def Mod_.comap {C : Type u₁} [] {A : Mon_ C} {B : Mon_ C} (f : 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