μₗ_unitality_inv — Mathlib

English

In a monoidal left action, the unitality constraint μℓ has an inverse relation with the unit λℓ and the functor F, giving the equation involving F.map and inverse of λℓ.

Русский

При моноидальном левом действии неравенство единицы λ и μℓ взаимно согласованы через μℓ и F, выражающееся обратной формулой.

LaTeX

$$$ (λ_\ell^F d)^{-1} ≫ μ_\ell F (𝟙_C) d = F.map (λ_\ell d)^{-1}. $$$

Lean4

@[reassoc (attr := simp)]
theorem μₗ_unitality_inv (d : D) : (λₗ (F.obj d)).inv ≫ μₗ F (𝟙_ C) d = F.map (λₗ d).inv := by
  simpa [-μₗ_unitality] using (λₗ[C] (F.obj d)).inv ≫= (μₗ_unitality F d).symm =≫ F.map (λₗ[C] d).inv

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