instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel

English

The degreewise property of being epi with injective kernels in cochain complexes is closed under composition and includes identities.

Русский

Свойство по степеням быть эпиморфизмом с инъективными ядрами в коцепентном комплексе сохраняется под композициями и содержит тождественные отображения.

LaTeX

$$$\text{IsMultiplicative}(\deg(\cdot))\;:\; \forall \varphi,\psi,\; (\varphi\circ \psi)\in \deg(\cdot)$$$

Lean4

instance : (degreewiseEpiWithInjectiveKernel (C := C)).IsMultiplicative
    where
  id_mem _ _ := MorphismProperty.id_mem _ _
  comp_mem _ _ hf hg n := MorphismProperty.comp_mem _ _ _ (hf n) (hg n)

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