μₗ_associativity_inv — Mathlib

English

In a monoidal left action setting, the associativity constraint μℓ has a coherent inverse relation with the tensor product and the associator αℓ: the appropriate composite relations hold with inverses.

Русский

В обстановке левого моноидального действия существует когерентное обратное отношение между μℓ, тензором и ассоциатором αℓ: выполняются соответствующие равенства, включающие инверсы.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem μₗ_associativity_inv (c c' : C) (d : D) :
    c ⊴ₗ μₗ F c' d ≫ μₗ F c (c' ⊙ₗ d) ≫ F.map (αₗ _ _ _).inv = (αₗ c c' (F.obj d)).inv ≫ μₗ F (c ⊗ c') d := by
  simpa [-μₗ_associativity, -μₗ_associativity_assoc] using
    (αₗ _ _ _).inv ≫= (μₗ_associativity F c c' d).symm =≫ F.map (αₗ _ _ _).inv

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