comul_assoc_flip — Mathlib

English

In a bicategory with a comonad t, the comultiplication followed by whiskering with t satisfies a coassociative relation with the associator, i.e., Δ ≫ Δ ▷ t = Δ ≫ t ◁ Δ ≫ α_{t t t}^{-1}. This is a structural coherence condition for comonads in bicategories.

Русский

В бикатегории с когомонадой t слагаемая Δ, затем обрамление (whiskering) с t, удовлетворяет когоссоциативному соотношению с ассоциатором α, то есть Δ ≫ Δ ▷ t = Δ ≫ t ◁ Δ ≫ α_{t t t}^{-1}. Это условие когерентности для когомонад в бикатегории.

LaTeX

$$$Δ ≫ Δ \triangleright t = Δ ≫ t \triangleleft Δ ≫ (α_{t t t})^{-1}$$$

Lean4

@[reassoc]
theorem comul_assoc_flip : Δ ≫ Δ ▷ t = Δ ≫ t ◁ Δ ≫ (α_ t t t).inv :=
  ComonObj.comul_assoc_flip t

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