degreewiseEpiWithInjectiveKernel — Mathlib

English

A morphism between cochain complexes is degreewise epi with injective kernels if and only if each component morphism is epi with injective kernel.

Русский

Гомоморфизм между коцепентными (cochain) комплексами задается как по каждому степени компонентам эпи с инъективными ядрами.

LaTeX

$$$\deg(\varphi)\;\text{holds if}\; \forall i \in \mathbb{Z},\; epiWithInjectiveKernel(\varphi.f_i)$$$

Lean4

/-- A morphism of cochain complexes `φ` in an abelian category satisfies
`degreewiseEpiWithInjectiveKernel φ` if for any `i : ℤ`, the morphism
`φ.f i` is an epimorphism with an injective kernel. -/
def degreewiseEpiWithInjectiveKernel : MorphismProperty (CochainComplex C ℤ) := fun _ _ φ =>
  ∀ (i : ℤ), epiWithInjectiveKernel (φ.f i)

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