mathlib docs: category_theory.monoidal.Mod

structure Mod {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) :

Type (max u₁ v₁)

X : C
act : A.X ⊗ c.X ⟶ c.X
one_act' : (A.one ⊗ 𝟙 c.X) ≫ c.act = (λ_ c.X).hom . "obviously"
assoc' : (A.mul ⊗ 𝟙 c.X) ≫ c.act = (α_ A.X A.X c.X).hom ≫ (𝟙 A.X ⊗ c.act) ≫ c.act . "obviously"

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

theorem Mod.assoc_flip {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M : Mod A) :

(𝟙 A.X ⊗ M.act) ≫ M.act = (α_ A.X A.X M.X).inv ≫ (A.mul ⊗ 𝟙 M.X) ≫ M.act

source

theorem Mod.hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {A : Mon_ C} {M N : Mod A} (x y : M.hom N) :

x = y ↔ x.hom = y.hom

source

theorem Mod.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {A : Mon_ C} {M N : Mod A} (x y : M.hom N) (h : x.hom = y.hom) :

x = y

source

@[ext]

structure Mod.hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M N : Mod A) :

Type v₁

hom : M.X ⟶ N.X
act_hom' : M.act ≫ c.hom = (𝟙 A.X ⊗ c.hom) ≫ N.act . "obviously"

A morphism of module objects.

source

@[simp]

theorem Mod.id_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M : Mod A) :

M.id.hom = 𝟙 M.X

source

def Mod.id {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M : Mod A) :

M.hom M

The identity morphism on a module object.

Equations

M.id = {hom := 𝟙 M.X, act_hom' := _}

source

@[instance]

def Mod.hom_inhabited {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M : Mod A) :

inhabited (M.hom M)

Equations

M.hom_inhabited = {default := M.id}

source

def Mod.comp {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category 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 := f.hom ≫ g.hom, act_hom' := _}

source

@[simp]

theorem Mod.comp_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} {M N O : Mod A} (f : M.hom N) (g : N.hom O) :

(Mod.comp f g).hom = f.hom ≫ g.hom

source

@[instance]

def Mod.category_theory.category {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} :

category_theory.category (Mod A)

Equations

Mod.category_theory.category = {to_category_struct := {to_has_hom := {hom := λ (M N : Mod A), M.hom N}, id := Mod.id A, comp := λ (M N O : Mod A) (f : M ⟶ N) (g : N ⟶ O), Mod.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}

source

@[simp]

theorem Mod.id_hom' {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M : Mod A) :

(𝟙 M).hom = 𝟙 M.X

source

@[simp]

theorem Mod.comp_hom' {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} {M N K : Mod A} (f : M ⟶ N) (g : N ⟶ K) :

(f ≫ g).hom = f.hom ≫ g.hom

source

@[simp]

theorem Mod.regular_act {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) :

(Mod.regular A).act = A.mul

source

def Mod.regular {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) :

Mod A

A monoid object as a module over itself.

Equations

Mod.regular A = {X := A.X, act := A.mul, one_act' := _, assoc' := _}

source

@[simp]

theorem Mod.regular_X {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) :

(Mod.regular A).X = A.X

source

@[instance]

def Mod.inhabited {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) :

inhabited (Mod A)

Equations

Mod.inhabited A = {default := Mod.regular A}

source

def Mod.forget {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) :

Mod A ⥤ C

The forgetful functor from module objects to the ambient category.

Equations

Mod.forget A = {obj := λ (A_1 : Mod A), A_1.X, map := λ (A_1 B : Mod A) (f : A_1 ⟶ B), f.hom, map_id' := _, map_comp' := _}

source

def Mod.comap {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A B : Mon_ C} (f : A ⟶ B) :

Mod B ⥤ Mod A

A morphism of monoid objects induces a "restriction" or "comap" functor between the categories of module objects.

Equations

Mod.comap f = {obj := λ (M : Mod B), {X := M.X, act := (f.hom ⊗ 𝟙 M.X) ≫ M.act, one_act' := _, assoc' := _}, map := λ (M N : Mod B) (g : M ⟶ N), {hom := g.hom, act_hom' := _}, map_id' := _, map_comp' := _}

source

@[simp]

theorem Mod.comap_map_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A B : Mon_ C} (f : A ⟶ B) (M N : Mod B) (g : M ⟶ N) :

((Mod.comap f).map g).hom = g.hom

source

@[simp]

theorem Mod.comap_obj_X {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A B : Mon_ C} (f : A ⟶ B) (M : Mod B) :

((Mod.comap f).obj M).X = M.X

source

@[simp]

theorem Mod.comap_obj_act {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A B : Mon_ C} (f : A ⟶ B) (M : Mod B) :

((Mod.comap f).obj M).act = (f.hom ⊗ 𝟙 M.X) ≫ M.act

mathlib documentation

The category of module objects over a monoid object.