instIsMultiplicativeMonoModSerre — Mathlib

English

The property monoModSerre is multiplicative: it is closed under composition and interacts with exactness in a coherent way.

Русский

Свойство monoModSerre является мультипликативным: оно замкнуто относительно композиции и согласуется с точностью.

LaTeX

$$$P.monoModSerre.IsMultiplicative$$$

Lean4

instance : P.monoModSerre.IsMultiplicative
    where
  id_mem _ := P.monoModSerre_of_mono _
  comp_mem f g hf hg := P.prop_X₂_of_exact ((kernelCokernelCompSequence_exact f g).exact 0) hf hg

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