δ_μ_app — Mathlib

English

The δ and μ components satisfy the opposite compatibility: (δ F i j).app X ; (μ F i j).app X = id_X.

Русский

δ и μ компоненты удовлетворяют обратной совместимости: (δ F i j).app X ; (μ F i j).app X = id_X.

LaTeX

$$$ (\\delta F i j).app X \\circ (\\mu F i j).app X = \\mathrm{id}_X $$$

Lean4

@[reassoc (attr := simp)]
theorem δ_μ_app (i j : M) (X : C) [F.Monoidal] : (δ F i j).app X ≫ (μ F i j).app X = 𝟙 _ :=
  (μIso F i j).inv_hom_id_app X

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