δᵣ_associativity_inv — Mathlib

English

For a right oplax linear functor, the associativity constraint δℓ satisfies an inverse associativity identity with αℓ and μℓ.

Русский

Для правой опласной линейной функтории ограничение ассоциативности δℓ удовлетворяет обратной ассоциативности с αℓ и μℓ.

LaTeX

$$$δ_ℓ F c (c' ⊗ d) \;⟶\; c ⊴_ℓ δ_ℓ F c' d \;⟶\; α_ℓ^{-1} = F.map (α_ℓ)^{-1} ∘ δ_ℓ F (c ⊗ c') d.$$$

Lean4

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

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