Structures · Category theory
CategoryTheory.ModObj
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.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Mod
- Shape
- 2 explicit arguments · adds smul, one_smul, mul_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by43
- CategoryTheory.ModObj.smul
- CategoryTheory.ModObj.leftSMul
- CategoryTheory.Mod.scalarRestriction
- CategoryTheory.ModObj.mul_smul
- CategoryTheory.ModObj.leftSMul_snd
- CategoryTheory.ModObj.leftSMul_fst
- CategoryTheory.ModObj.one_smul
- CategoryTheory.ModObj.mul_smul_self
- CategoryTheory.ModObj.mul_smul_self_flip
- CategoryTheory.Hom.smul_def
- CategoryTheory.ModObj.ofIso
- CategoryTheory.Mod.scalarRestriction_hom
- CategoryTheory.Mod.scalarRestriction_smul
- CategoryTheory.ModObj.lift_leftSMul
- CategoryTheory.IsModHom.map_smul
- CategoryTheory.Mod.Hom.mk''
- CategoryTheory.ModObj.one_smul_self
- CategoryTheory.IsModHom.mulActionHom
- CategoryTheory.IsModHom.map_smul_assoc
- CategoryTheory.ModObj.one_smul_self_assoc
- CategoryTheory.Mod.Hom.mk''_hom
- CategoryTheory.ModObj.one_smul_assoc
- CategoryTheory.IsModHom.mulActionHom_apply
- CategoryTheory.ModObj.mul_smul_self_assoc
- CategoryTheory.ModObj.isIso_leftSMul_iff
- CategoryTheory.instIsModHomId
- CategoryTheory.IsMod_Hom
- CategoryTheory.ModObj.comp_smul
- CategoryTheory.Mod_.scalarRestriction
- CategoryTheory.Mod_.scalarRestriction_hom
- CategoryTheory.ModObj.assoc_flip
- CategoryTheory.Hom.instSMulHom
- CategoryTheory.instIsModHomInvOfHom
- CategoryTheory.ModObj.lift_leftSMul_eq_lift_iff
- CategoryTheory.ModObj.lift_leftSMul_assoc
- CategoryTheory.instIsModHomComp
- CategoryTheory.ModObj.leftSMul_snd_assoc
- CategoryTheory.Mod_.Hom.mk''
- CategoryTheory.ModObj.leftSMul_fst_assoc
- CategoryTheory.ModObj.mul_smul_assoc
- CategoryTheory.ModObj.ofIso_smul
- CategoryTheory.ModObj.mul_smul_self_flip_assoc
- CategoryTheory.Hom.mulAction
Ancestors0
No ancestors.