Epimorphisms with an injective kernel

In this file, we define the class of morphisms epiWithInjectiveKernel in an abelian category. We show that this property of morphisms is multiplicative.

This shall be used in the file Mathlib/Algebra/Homology/Factorizations/Basic.lean in order to define morphisms of cochain complexes which satisfy this property degreewise.

def CategoryTheory.Abelian.epiWithInjectiveKernel {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] : MorphismProperty C

The class of morphisms in an abelian category that are epimorphisms and have an injective kernel.

Equations

• CategoryTheory.Abelian.epiWithInjectiveKernel f = (CategoryTheory.Epi f ∧ CategoryTheory.Injective (CategoryTheory.Limits.kernel f))

theorem CategoryTheory.Abelian.epiWithInjectiveKernel_iff {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] {X Y : C} (g : X ⟶ Y) : epiWithInjectiveKernel g ↔ ∃ (I : C) (_ : Injective I) (f : I ⟶ X) (w : CategoryStruct.comp f g = 0), Nonempty { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting

A morphism g : X ⟶ Y is epi with an injective kernel iff there exists a morphism f : I ⟶ X with I injective such that f ≫ g = 0 and the short complex I ⟶ X ⟶ Y has a splitting.

theorem CategoryTheory.Abelian.epiWithInjectiveKernel_of_iso {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) [IsIso f] : epiWithInjectiveKernel f

instance CategoryTheory.Abelian.instIsMultiplicativeEpiWithInjectiveKernel {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] : epiWithInjectiveKernel.IsMultiplicative