inv_δₗ — Mathlib

English

In the left-linear action, the inverse associativity relation between μℓ, the tensor product, and αℓ holds as a coherence identity.

Русский

Во левостороннем линейном действии идентичности совместимости μℓ, тензора и αℓ сохраняют когерентность в виде обратного равенства.

LaTeX

$$$ c \triangleright_\ell μ_\ell F c' d \;\;≫\; μ_\ell F c (c' \triangleleft_\ell d) \;\;≫\; F.map (α_ℓ^{-1}) = (α_ℓ c c' (F.obj d))^{-1} \;≫ μ_ℓ F (c \otimes c') d. $$$

Lean4

@[simp]
theorem inv_δₗ : CategoryTheory.inv (δₗ F c d) = μₗ F c d :=
  Eq.symm <| IsIso.eq_inv_of_hom_inv_id <| δₗ_comp_μₗ F c d

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