algebraFunctorOfMonadHom

Mathlib.CategoryTheory.Monad.Algebra

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Monad.algebraFunctorOfMonadHom

Lean4

/-- Given a monad morphism from `T₂` to `T₁`, we get a functor from the algebras of `T₁` to algebras of
`T₂`.
-/
@[simps]
def algebraFunctorOfMonadHom {T₁ T₂ : Monad C} (h : T₂ ⟶ T₁) : Algebra T₁ ⥤ Algebra T₂
    where
  obj
    A :=
    { A := A.A
      a := h.app A.A ≫ A.a
      unit := by simp [A.unit]
      assoc := by simp [A.assoc] }
  map f := { f := f.f }

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

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

Разделы

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

Аффилиация

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