uniqueHomFromTrivial

Mathlib.CategoryTheory.Monoidal.Mon_

URI: https://scilib.ai/kg/mathlib#Mon.uniqueHomFromTrivial

Lean4

@[simps]
instance uniqueHomFromTrivial (A : Mon C) : Unique (trivial C ⟶ A)
    where
  default.hom := η[A.X]
  default.isMonHom_hom.mul_hom := by simp [unitors_equal]
  uniq
    f := by
    ext
    rw [← Category.id_comp f.hom]
    dsimp only [trivial_X]
    rw [← trivial_mon_one, IsMonHom.one_hom]

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

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

Разделы

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

Аффилиация

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