instIsNormalMonoCategory — Mathlib

English

The opposite construction yields a normal mono category structure on HomologicalComplex.

Русский

Обратное построение даёт структуру нормальной моно-категории на HomologicalComplex.

LaTeX

$$$\\text{IsNormalMonoCategory}(\\mathrm{HomologicalComplex}\\; C\\; c)$$$

Lean4

noncomputable instance : IsNormalMonoCategory (HomologicalComplex C c) :=
  ⟨fun p _ =>
    ⟨NormalMono.mk _ (cokernel.π p) (cokernel.condition _)
        (isLimitOfEval _ _ (fun _ => Abelian.isLimitMapConeOfKernelForkOfι _ _))⟩⟩

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