isIso_right_of_isIso_biprod_map — Mathlib

English

If biprod.map f g is an iso, then g is iso.

Русский

Если biprod.map f g является изоморфизмом, то g также изоморфен.

LaTeX

$$$\mathrm{IsIso}(\mathrm{biprod.map} f g) \Rightarrow \mathrm{IsIso}(g)$$$

Lean4

/-- If
```
(f 0)
(0 g)
```
is invertible, then `g` is invertible.
-/
theorem isIso_right_of_isIso_biprod_map {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [IsIso (biprod.map f g)] : IsIso g :=
  letI : IsIso (biprod.map g f) := by
    rw [← biprod.braiding_map_braiding]
    infer_instance
  isIso_left_of_isIso_biprod_map g f

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