unmopMonObj

Mathlib.CategoryTheory.Monoidal.Opposite.Mon_

URI: https://scilib.ai/kg/mathlib#MonObj.unmopMonObj

Lean4

/-- If `M : Cᴹᵒᵖ` is a monoid object, then `unmop M : C` too. -/
@[simps -isSimp] -- not making them simp because it causes a loop.

instance unmopMonObj : MonObj (unmop M) where
  mul := MonObj.mul.unmop
  one := MonObj.one.unmop
  mul_one := by
    apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
    simp
  one_mul := by
    apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
    simp
  mul_assoc := by
    apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
    simp

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru