The category of module objects over a monoid object. #
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' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.one X) smul = (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom
The identity acts trivially.
- mul_smul' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.mul X) smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) smul)
The action map is compatible with multiplication.
Instances
The action map
Equations
- Mon_Class.termγ = Lean.ParserDescr.node `Mon_Class.termγ 1024 (Lean.ParserDescr.symbol "γ")
Instances For
The action map
Equations
- One or more equations did not get rendered due to their size.
Instances For
The action map
Equations
- One or more equations did not get rendered due to their size.
Instances For
The action of a monoid object on itself.
Equations
- Mod_Class.regular M = { smul := Mon_Class.mul, one_smul' := ⋯, mul_smul' := ⋯ }
Instances For
If C
acts monoidally on D
, then every object of D
is canonically a
module over the trivial monoid.
Equations
- Mod_Class.instTensorUnit X = { smul := (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom, one_smul' := ⋯, mul_smul' := ⋯ }
A morphism in D
is a morphism of A
-module objects if it commutes with
the action maps
Instances
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
A morphism of module objects.
The underlying morphism
Instances For
An alternative constructor for Hom
,
taking a morphism without a [isMod_Hom] instance, as well as the relevant
equality to put such an instance.
Equations
- Mod_.Hom.mk' f smul_hom = { hom := f, isMod_Hom := ⋯ }
Instances For
An alternative constructor for Hom
,
taking a morphism without a [isMod_Hom] instance, between objects with
a Mod_Class
instance (rather than bundled as Mod_
),
as well as the relevant equality to put such an instance.
Equations
- Mod_.Hom.mk'' f smul_hom = { hom := f, isMod_Hom := ⋯ }
Instances For
The identity morphism on a module object.
Instances For
Equations
- M.homInhabited = { default := M.id }
Composition of module object morphisms.
Instances For
Equations
- One or more equations did not get rendered due to their size.
A monoid object as a module over itself.
Equations
- Mod_.regular A = { X := A, mod := Mod_Class.regular A }
Instances For
Equations
- Mod_.instInhabited A = { default := Mod_.regular A }
The forgetful functor from module objects to the ambient category.
Equations
Instances For
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]
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
.
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.