inv_actionHomLeft — Mathlib

English

For any morphisms f: x → y in D and g: x' → y' in C, if both f and g are isomorphisms, then the action morphism f ⊙ᵣₘ g is an isomorphism.

Русский

Для любых морфизмов f: x → y в D и g: x' → y' в C, если f и g — изоморфизмы, то отображение действия f ⊙ᵣₘ g является изоморфизмом.

LaTeX

$$$IsIso(f \odot_r^m g).$$$

Lean4

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

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