isIso_inl_iff_isZero — Mathlib

English

In a preadditive category with binary biproducts, biprod.inl is an isomorphism iff the second summand is zero.

Русский

В прецидивной категории с двоичным бикопродуктом biprod.inl является изоморфизмом тогда и только тогда, когда второй суммант равен нулю.

LaTeX

$$$ IsIso(biprod.inl) \iff IsZero Y. $$$

Lean4

theorem isIso_inl_iff_isZero (X Y : C) : IsIso (biprod.inl : X ⟶ X ⊞ Y) ↔ IsZero Y :=
  by
  rw [biprod.isIso_inl_iff_id_eq_fst_comp_inl, ← biprod.total, add_eq_left]
  constructor
  · intro h
    replace h := h =≫ biprod.snd
    simpa [← IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] using h
  · intro h
    rw [IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] at h
    rw [h, zero_comp]

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