isIso_inl_iff_id_eq_fst_comp_inl — Mathlib

English

In a category with binary biproducts X ⊞ Y, the morphism biprod.inl is an isomorphism if and only if id_{X⊞Y} = fst ∘ inl.

Русский

В категории с бинарными биобразованиями X ⊞ Y морфизм biprod.inl является изоморфизмом тогда и только тогда, когда выполняется id_{X⊞Y} = fst ∘ inl.

LaTeX

$$$\mathrm{IsIso}(\mathrm{biprod.inl}) \;\iff\; \mathrm{id}_{X \oplus Y} = \mathrm{biprod.fst} \circ \mathrm{biprod.inl}$$$

Lean4

theorem isIso_inl_iff_id_eq_fst_comp_inl (X Y : C) [HasBinaryBiproduct X Y] :
    IsIso (biprod.inl : X ⟶ X ⊞ Y) ↔ 𝟙 (X ⊞ Y) = biprod.fst ≫ biprod.inl :=
  by
  constructor
  · intro h
    have := (cancel_epi (inv biprod.inl : X ⊞ Y ⟶ X)).2 <| @biprod.inl_fst _ _ _ X Y _
    rw [IsIso.inv_hom_id_assoc, Category.comp_id] at this
    rw [this, IsIso.inv_hom_id]
  · intro h
    exact ⟨⟨biprod.fst, biprod.inl_fst, h.symm⟩⟩

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