μ_δ_app — Mathlib

English

The μ and δ components at an object X satisfy the unit-counit compatibility: (μ F i j).app X ; (δ F i j).app X = id_X.

Русский

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

LaTeX

$$$ (\\mu F i j).app X \\circ (\\delta 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).hom_inv_id_app X

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