strInv

Mathlib.CategoryTheory.Endofunctor.Algebra

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Endofunctor.Algebra.Initial.strInv

Lean4

/-- The inverse of the structure map of an initial algebra -/
@[simp]
def strInv : A.1 ⟶ F.obj A.1 :=
  (h.to ⟨F.obj A.a, F.map A.str⟩).f

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

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

Разделы

Аффилиация

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