isIso_hom_mk — Mathlib

English

If a morphism f: M.V → N.V is an isomorphism and the coherence condition holds, then the constructed Action.Hom using f is an isomorphism.

Русский

Если отображение f между базовыми объектами является изоморфизмом и выполняется условие согласованности, то конструированный morphism является изоморфизмом.

LaTeX

$$Given $f: M.V \\to N.V$ iso and coherence $w$, then $\\mathrm{Hom.mk}\; f\; w$ is iso$$

Lean4

instance isIso_hom_mk {M N : Action V G} (f : M.V ⟶ N.V) [IsIso f] (w) : @IsIso _ _ M N (Hom.mk f w) :=
  (mkIso (asIso f) w).isIso_hom

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