instHasBinaryBiproductComplement — Mathlib

English

In Karoubi(C), for every P, the binary biproduct P with its complement P.complement exists.

Русский

В Karoubi(C) для каждого P существует двоичное биобразное произведение P и его дополнение P.complement.

LaTeX

$$\\operatorname{HasBinaryBiproduct}(P, P.complement)$$

Lean4

instance (P : Karoubi C) : HasBinaryBiproduct P P.complement :=
  hasBinaryBiproduct_of_total
    { pt := P.X
      fst := P.decompId_p
      snd := P.complement.decompId_p
      inl := P.decompId_i
      inr := P.complement.decompId_i
      inl_fst := P.decompId.symm
      inl_snd := by
        simp only [zero_def, hom_ext_iff, complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p, comp_sub,
          comp_id, idem, sub_self]
      inr_fst := by
        simp only [zero_def, hom_ext_iff, complement_X, comp_f, decompId_i_f, complement_p, decompId_p_f, sub_comp,
          id_comp, idem, sub_self]
      inr_snd := P.complement.decompId.symm }
    (by
      ext
      simp only [complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p, add_def, idem, comp_sub, comp_id,
        sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel, id_f])

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