δₗ_associativity_inv — Mathlib

English

For any iso f in D and any z in C, inv (f ⊵ᵣ z) = inv f ⊵ᵣ z.

Русский

Для любого изоморфизма f в D и любого z в C, обратный к действию слева равен действию слева на обратном f.

LaTeX

$$$inv(f \triangleleft_r z) = inv(f) \triangleleft_r z.$$$

Lean4

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

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