The category of module objects over a monoid object. #
class
CategoryTheory.ModObj
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(M : C)
[MonObj M]
(X : D)
:
Type v₂
Given an action of a monoidal category C on a category D,
an action of a monoid object M in C on an object X in D is the data of a
map smul : M ⊙ₗ X ⟶ X that satisfies unitality and associativity with
multiplication.
See MulAction for the non-categorical version.
The action map
- one_smul' : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.one X) smul = (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom
The identity acts trivially.
- mul_smul' : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.mul X) smul = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) smul)
The action map is compatible with multiplication.
Instances
theorem
CategoryTheory.ModObj.mul_smul'_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory.MonoidalLeftAction C D}
{M : C}
{inst✝⁴ : MonObj M}
(X : D)
[self : ModObj M X]
{Z : D}
(h : X ⟶ Z)
:
CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.mul X)
(CategoryStruct.comp smul h) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom
(CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) (CategoryStruct.comp smul h))
The action map is compatible with multiplication.
theorem
CategoryTheory.ModObj.one_smul'_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory.MonoidalLeftAction C D}
{M : C}
{inst✝⁴ : MonObj M}
(X : D)
[self : ModObj M X]
{Z : D}
(h : X ⟶ Z)
:
The identity acts trivially.
@[simp]
theorem
CategoryTheory.ModObj.one_smul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{M : C}
[MonObj M]
(X : D)
[ModObj M X]
:
@[simp]
theorem
CategoryTheory.ModObj.one_smul_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{M : C}
[MonObj M]
(X : D)
[ModObj M X]
{Z : D}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ModObj.mul_smul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{M : C}
[MonObj M]
(X : D)
[ModObj M X]
:
@[simp]
theorem
CategoryTheory.ModObj.mul_smul_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{M : C}
[MonObj M]
(X : D)
[ModObj M X]
{Z : D}
(h : X ⟶ Z)
:
CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.mul X)
(CategoryStruct.comp smul h) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom
(CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) (CategoryStruct.comp smul h))
theorem
CategoryTheory.ModObj.assoc_flip
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{M : C}
[MonObj M]
(X : D)
[ModObj M X]
:
@[reducible, inline]
abbrev
CategoryTheory.ModObj.regular
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(M : C)
[MonObj M]
:
ModObj M M
The action of a monoid object on itself.
Instances For
@[simp]
theorem
CategoryTheory.ModObj.smul_eq_mul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(M : C)
[MonObj M]
:
@[implicit_reducible]
instance
CategoryTheory.ModObj.instTensorUnit
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(X : D)
:
If C acts monoidally on D, then every object of D is canonically a
module over the trivial monoid.
@[simp]
theorem
CategoryTheory.ModObj.smul_def
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(X : D)
:
theorem
CategoryTheory.ModObj.ext
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{M : C}
[MonObj M]
{X : C}
(h₁ h₂ : ModObj M X)
(H : smul = smul)
:
theorem
CategoryTheory.ModObj.ext_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{M : C}
[MonObj M]
{X : C}
{h₁ h₂ : ModObj M X}
:
class
CategoryTheory.IsMod_Hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(A : C)
[MonObj A]
{M N : D}
[ModObj A M]
[ModObj A N]
(f : M ⟶ N)
:
A morphism in D is a morphism of A-module objects if it commutes with
the action maps
Instances
@[simp]
theorem
CategoryTheory.IsMod_Hom.smul_hom_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory.MonoidalLeftAction C D}
{A : C}
{inst✝⁴ : MonObj A}
{M N : D}
{inst✝⁵ : ModObj A M}
{inst✝⁶ : ModObj A N}
{f : M ⟶ N}
[self : IsMod_Hom A f]
{Z : D}
(h : N ⟶ Z)
:
instance
CategoryTheory.instIsMod_HomId
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(A : C)
[MonObj A]
{M : D}
[ModObj A M]
:
IsMod_Hom A (CategoryStruct.id M)
instance
CategoryTheory.instIsMod_HomComp
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(A : C)
[MonObj A]
{M N O : D}
[ModObj A M]
[ModObj A N]
[ModObj A O]
(f : M ⟶ N)
(g : N ⟶ O)
[IsMod_Hom A f]
[IsMod_Hom A g]
:
IsMod_Hom A (CategoryStruct.comp f g)
instance
CategoryTheory.instIsMod_HomInvOfHom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(A : C)
[MonObj A]
{M N : D}
[ModObj A M]
[ModObj A N]
(f : M ≅ N)
[IsMod_Hom A f.hom]
:
structure
CategoryTheory.Mod_
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(A : C)
[MonObj A]
:
Type (max u₂ v₂)
A module object for a monoid object in a monoidal category acting on the ambient category.
- X : D
The underlying object in the ambient category
Instances For
theorem
CategoryTheory.Mod_.assoc_flip
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
(M : Mod_ D A)
:
CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A ModObj.smul) ModObj.smul = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso A A M.X).inv
(CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.mul M.X) ModObj.smul)
structure
CategoryTheory.Mod_.Hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
(M N : Mod_ D A)
:
Type v₂
A morphism of module objects.
The underlying morphism
Instances For
theorem
CategoryTheory.Mod_.Hom.ext
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory.MonoidalLeftAction C D}
{A : C}
{inst✝⁴ : MonObj A}
{M N : Mod_ D A}
{x y : M.Hom N}
(hom : x.hom = y.hom)
:
theorem
CategoryTheory.Mod_.Hom.ext_iff
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory.MonoidalLeftAction C D}
{A : C}
{inst✝⁴ : MonObj A}
{M N : Mod_ D A}
{x y : M.Hom N}
:
def
CategoryTheory.Mod_.Hom.mk'
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
{M N : Mod_ D A}
(f : M.X ⟶ N.X)
(smul_hom :
CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul := by
cat_disch)
:
M.Hom N
An alternative constructor for Hom,
taking a morphism without a [isMod_Hom] instance, as well as the relevant
equality to put such an instance.
Instances For
@[simp]
theorem
CategoryTheory.Mod_.Hom.mk'_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
{M N : Mod_ D A}
(f : M.X ⟶ N.X)
(smul_hom :
CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul := by
cat_disch)
:
def
CategoryTheory.Mod_.Hom.mk''
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
{M N : D}
[ModObj A M]
[ModObj A N]
(f : M ⟶ N)
(smul_hom :
CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul := by
cat_disch)
:
An alternative constructor for Hom,
taking a morphism without a [isMod_Hom] instance, between objects with
a ModObj instance (rather than bundled as Mod_),
as well as the relevant equality to put such an instance.
Instances For
@[simp]
theorem
CategoryTheory.Mod_.Hom.mk''_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
{M N : D}
[ModObj A M]
[ModObj A N]
(f : M ⟶ N)
(smul_hom :
CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul := by
cat_disch)
:
def
CategoryTheory.Mod_.id
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
(M : Mod_ D A)
:
M.Hom M
The identity morphism on a module object.
Instances For
@[simp]
theorem
CategoryTheory.Mod_.id_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
(M : Mod_ D A)
:
@[implicit_reducible]
instance
CategoryTheory.Mod_.homInhabited
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
(M : Mod_ D A)
:
def
CategoryTheory.Mod_.comp
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
{M N O : Mod_ D A}
(f : M.Hom N)
(g : N.Hom O)
:
M.Hom O
Composition of module object morphisms.
Instances For
@[simp]
theorem
CategoryTheory.Mod_.comp_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
{M N O : Mod_ D A}
(f : M.Hom N)
(g : N.Hom O)
:
@[implicit_reducible]
instance
CategoryTheory.Mod_.instCategory
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
:
Category.{v₂, max u₂ v₂} (Mod_ D A)
theorem
CategoryTheory.Mod_.hom_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
{M N : Mod_ D A}
(f₁ f₂ : M ⟶ N)
(h : f₁.hom = f₂.hom)
:
theorem
CategoryTheory.Mod_.hom_ext_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
{M N : Mod_ D A}
{f₁ f₂ : M ⟶ N}
:
@[simp]
theorem
CategoryTheory.Mod_.id_hom'
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
(M : Mod_ D A)
:
@[simp]
theorem
CategoryTheory.Mod_.comp_hom'
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A : C}
[MonObj A]
{M N K : Mod_ D A}
(f : M ⟶ N)
(g : N ⟶ K)
:
def
CategoryTheory.Mod_.regular
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(A : C)
[MonObj A]
:
Mod_ C A
A monoid object as a module over itself.
Instances For
@[simp]
theorem
CategoryTheory.Mod_.regular_mod_smul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(A : C)
[MonObj A]
:
@[simp]
theorem
CategoryTheory.Mod_.regular_X
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(A : C)
[MonObj A]
:
@[implicit_reducible]
instance
CategoryTheory.Mod_.instInhabited
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(A : C)
[MonObj A]
:
def
CategoryTheory.Mod_.forget
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(A : C)
[MonObj A]
:
The forgetful functor from module objects to the ambient category.
Instances For
@[simp]
theorem
CategoryTheory.Mod_.forget_map
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(A : C)
[MonObj A]
{X✝ Y✝ : Mod_ D A}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Mod_.forget_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
(A : C)
[MonObj A]
(A✝ : Mod_ D A)
:
@[implicit_reducible]
def
CategoryTheory.Mod_.scalarRestriction
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A B : C}
[MonObj A]
[MonObj B]
(f : A ⟶ B)
[IsMonHom f]
(M : D)
[ModObj B M]
:
ModObj A M
When M is a B-module in D and f : A ⟶ B is a morphism of internal
monoid objects, M inherits an A-module structure via
"restriction of scalars", i.e γ[A, M] = f.hom ⊵ₗ M ≫ γ[B, M].
Instances For
@[simp]
theorem
CategoryTheory.Mod_.scalarRestriction_smul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A B : C}
[MonObj A]
[MonObj B]
(f : A ⟶ B)
[IsMonHom f]
(M : D)
[ModObj B M]
:
theorem
CategoryTheory.Mod_.scalarRestriction_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A B : C}
[MonObj A]
[MonObj B]
(f : A ⟶ B)
[IsMonHom f]
(M N : D)
[ModObj B M]
[ModObj B N]
(g : M ⟶ N)
[IsMod_Hom B g]
:
IsMod_Hom A g
If g : M ⟶ N is a B-linear morphisms of B-modules, then it induces an
A-linear morphism when M and N have an A-module structure obtained
by restricting scalars along a monoid morphism A ⟶ B.
def
CategoryTheory.Mod_.comap
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A B : C}
[MonObj A]
[MonObj B]
(f : A ⟶ B)
[IsMonHom f]
:
A morphism of monoid objects induces a "restriction" or "comap" functor between the categories of module objects.
Instances For
@[simp]
theorem
CategoryTheory.Mod_.comap_obj_X
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A B : C}
[MonObj A]
[MonObj B]
(f : A ⟶ B)
[IsMonHom f]
(M : Mod_ D B)
:
@[simp]
theorem
CategoryTheory.Mod_.comap_obj_mod
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A B : C}
[MonObj A]
[MonObj B]
(f : A ⟶ B)
[IsMonHom f]
(M : Mod_ D B)
:
@[simp]
theorem
CategoryTheory.Mod_.comap_map_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory.MonoidalLeftAction C D]
{A B : C}
[MonObj A]
[MonObj B]
(f : A ⟶ B)
[IsMonHom f]
{M N : Mod_ D B}
(g : M ⟶ N)
: