Documentation

Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

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.

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

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

Equations
Instances For
    source
    theorem CategoryTheory.Abelian.epiWithInjectiveKernel_iff {C : Type u_1} [Category.{v_1, 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.

    source
    theorem CategoryTheory.Abelian.epiWithInjectiveKernel_of_iso {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) [IsIso f] :
    epiWithInjectiveKernel f
    source
    theorem CategoryTheory.Abelian.epiWithInjectiveKernel_iff_of_isZero {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) (hY : Limits.IsZero Y) :
    epiWithInjectiveKernel f ↔ Injective X
    source
    instance CategoryTheory.Abelian.instIsMultiplicativeEpiWithInjectiveKernel {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] :
    epiWithInjectiveKernel.IsMultiplicative
    source
    instance CategoryTheory.Abelian.instIsStableUnderRetractsEpiWithInjectiveKernel {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] :
    epiWithInjectiveKernel.IsStableUnderRetracts
    source
    theorem CategoryTheory.Abelian.epiWithInjectiveKernel.hasLiftingProperty {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} {p : X ⟶ Y} (hp : epiWithInjectiveKernel p) {A B : C} (i : A ⟶ B) [Mono i] :
    HasLiftingProperty i p