instIsIdempotentCompleteHomologicalComplex

English

Another extensionality lemma for Karoubi objects: equality is determined by X and p-part as in the first ext.

Русский

Другая лемма экстендирования для объектов Karoubi: равенство определяется X и p-частью так же, как и в первом ext.

LaTeX

$$ext (h_X : Eq P.X Q.X) (h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p) → P = Q$$

Lean4

instance [IsIdempotentComplete C] : IsIdempotentComplete (HomologicalComplex C c) :=
  by
  rw [isIdempotentComplete_iff_of_equivalence ((toKaroubiEquivalence C).mapHomologicalComplex c), ←
    isIdempotentComplete_iff_of_equivalence (karoubiHomologicalComplexEquivalence C c)]
  infer_instance

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