μᵣ_associativity_inv — Mathlib

English

The unitality constraint μℓ interacts with the unit object via F.map and inverse of the left unit iso.

Русский

Единичность μℓ взаимодействует с единицей через отображение F и обратную единичную изоморфность.

LaTeX

$$$ (μ_ℓ F c d)^{-1} = δ_ℓ F c d.$$$

Lean4

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

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