Theorems · Definition · category theory
CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
{C : Type u_1} →
{D : Type u_2} →
{inst : CategoryTheory.Category.{v_1, u_1} C} →
{inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
{inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
[self : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] →
(d : D) →
CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
(CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅
dThe structural isomorphism between d ⊙ᵣ 𝟙_ C and d.
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Isostatement · cited by 3,963
- CategoryTheory.MonoidalCategoryStruct.tensorUnitstatement · cited by 1,384
- CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObjstatement · cited by 146
- CategoryTheory.MonoidalCategoryStructstatement and proof · cited by 26
- CategoryTheory.MonoidalCategory.MonoidalRightActionStructstatement and proof · cited by 0
Cited by48
Results whose statement or proof uses this declaration.
- CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturalitystatement · cited by 3
- CategoryTheory.Functor.LaxRightLinear.μᵣ_unitalitystatement · cited by 2
- CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIsoproof · cited by 2
- CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_invstatement · cited by 2
- CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_invstatement and proof · cited by 1
- CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitorstatement · cited by 1
- CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitorstatement · cited by 1
- CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturalitystatement and proof · cited by 1
- CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_homstatement and proof · cited by 1
- CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRightstatement and proof · cited by 1
- CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIsostatement and proof · cited by 0