isIso_actionHom — Mathlib

English

Let f: x → y be an isomorphism in D and g: x' → y' be an isomorphism in C. Then the composite action morphism f ⊙ᵣₘ g is an isomorphism in D, with inverse inv f ⊙ᵣₘ inv g.

Русский

Пусть f: x → y — изоморфизм в D и g: x' → y' — изоморфизм в C. Тогда композиционный отображение действия f ⊙ᵣₘ g есть изоморфизм и имеет обратное inv f ⊙ᵣₘ inv g.

LaTeX

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

Lean4

instance isIso_actionHom {x y : D} {x' y' : C} (f : x ⟶ y) (g : x' ⟶ y') [IsIso f] [IsIso g] : IsIso (f ⊙ᵣₘ g) :=
  ⟨(inv f) ⊙ᵣₘ (inv g), by simp [← actionHom_comp]⟩

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