isIso_actionHomLeft — Mathlib

English

Let C and D be categories with a monoidal left action of C on D. If f is an isomorphism in C and z is an object of D, then the induced left-action morphism f ⊵ₗ z is an isomorphism in D with inverse inv f ⊵ₗ z.

Русский

Пусть C и D — категории, на которых действует моноидальное слева соотношение; если f является изоморфизмом в C, а z ∈ D, то отображение действия слева f ⊵ₗ z является изоморфизмом в D, обратное равно inv f ⊵ₗ z.

LaTeX

$$$\operatorname{inv}(f \;⊵_\ell\; z) = \operatorname{inv}f \;⊵_\ell\; z$$$

Lean4

instance isIso_actionHomLeft {x y : C} (f : x ⟶ y) [IsIso f] (z : D) : IsIso (f ⊵ₗ z) :=
  ⟨inv f ⊵ₗ z, by simp⟩

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