inv_actionHomRight — Mathlib

English

For any isomorphism f: y → z in D and any object z in C, the left action morphism inv (f ⊵ᵣ z) equals inv f ⊵ᵣ z.

Русский

Для любого изоморфизма f: y → z в D и любого объекта z в C, обратное к действию слева удовлетворяет inv (f ⊵ᵣ z) = inv f ⊵ᵣ z.

LaTeX

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

Lean4

@[simp]
theorem inv_actionHomRight (x : D) {y z : C} (f : y ⟶ z) [IsIso f] : inv (x ⊴ᵣ f) = x ⊴ᵣ inv f :=
  IsIso.inv_eq_of_hom_inv_id <| actionHomRight_hom_inv' x f

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