δₗ_unitality_hom — Mathlib

English

If f: x → y and g: x' → y' are isomorphisms, then inv (f ⊙ᵣₘ g) = inv f ⊙ᵣₘ inv g.

Русский

Если f и g — изоморфизмы, то обратное к их совместному действию равно их обратным поодиночному действию.

LaTeX

$$$inv(f \odot_r^m g) = inv(f) \odot_r^m inv(g).$$$

Lean4

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

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