The category of module objects over a monoid object. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 ⊗ self.X ⟶ self.X
- one_act' : (A.one ⊗ 𝟙 self.X) ≫ self.act = (λ_ self.X).hom . "obviously"
- assoc' : (A.mul ⊗ 𝟙 self.X) ≫ self.act = (α_ A.X A.X self.X).hom ≫ (𝟙 A.X ⊗ self.act) ≫ self.act . "obviously"
A module object for a monoid object, all internal to some monoidal category.
Instances for Mod_
- Mod_.has_sizeof_inst
- Mod_.category_theory.category
- Mod_.inhabited
@[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₁
A morphism of module objects.
Instances for Mod_.hom
- Mod_.hom.has_sizeof_inst
- Mod_.hom_inhabited
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) :
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
@[simp]
theorem
Mod_.id_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A : Mon_ C}
(M : Mod_ A) :
@[protected, instance]
def
Mod_.hom_inhabited
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A : Mon_ C}
(M : Mod_ A) :
Equations
- M.hom_inhabited = {default := M.id}
@[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) :
@[protected, instance]
def
Mod_.category_theory.category
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A : Mon_ C} :
@[simp]
theorem
Mod_.id_hom'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A : Mon_ C}
(M : Mod_ A) :
@[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) :
@[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
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.
@[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
@[protected, instance]
def
Mod_.inhabited
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
Equations
- Mod_.inhabited A = {default := Mod_.regular A}
def
Mod_.forget
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
The forgetful functor from module objects to the ambient category.
@[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
@[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
def
Mod_.comap
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
(f : A ⟶ B) :
A morphism of monoid objects induces a "restriction" or "comap" functor between the categories of module objects.
@[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) :