associator

Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

URI: https://scilib.ai/kg/mathlib#AugmentedSimplexCategory.associator

Lean4

/-- The associator isomorphism for the monoidal structure on `AugmentedSimplexCategory` -/
def associator (x y z : AugmentedSimplexCategory) : tensorObj (tensorObj x y) z ≅ tensorObj x (tensorObj y z) :=
  match x, y, z with
  | .of x, .of y, .of z => eqToIso (congrArg (fun j ↦ WithInitial.of <| SimplexCategory.mk j) (by simp +arith))
  | .star, .star, .star => Iso.refl _
  | .star, .of _, .star => Iso.refl _
  | .star, .star, .of _ => Iso.refl _
  | .star, .of _, .of _ => Iso.refl _
  | .of _, .star, .star => Iso.refl _
  | .of _, .star, .of _ => Iso.refl _
  | .of _, .of _, .star => Iso.refl _

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

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

Разделы

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

Аффилиация

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