Documentation

TauCeti.CategoryTheory.Exact.Abelian

The canonical exact structure on an abelian category #

Every abelian category C carries a canonical Quillen exact structure ExactStructure.abelian C whose conflations are the short exact short complexes S : X ⟶ Y ⟶ Z (in the sense of CategoryTheory.ShortComplex.ShortExact).

In this exact structure:

The Quillen axioms E0/E0op, E1/E1op, and E2/E2op translate directly to standard properties of abelian categories:

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.ExactStructure.abelian (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] :
ExactStructure C

The canonical exact structure on an abelian category C, whose conflations are the short exact short complexes.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.ExactStructure.abelian_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
    (abelian C).Conflation S ↔ S.ShortExact

    The conflations of the canonical exact structure on an abelian category are the short exact short complexes.

    source
    theorem TauCeti.ExactStructure.abelian_conflation_iff_isKernelCokernelPair {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
    (abelian C).Conflation S ↔ IsKernelCokernelPair S

    In an abelian category, conflations of the canonical exact structure are precisely the kernel–cokernel pairs.

    source
    @[simp]
    theorem TauCeti.ExactStructure.abelian_isInflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (i : X ⟶ Y) :
    (abelian C).IsInflation i ↔ CategoryTheory.Mono i

    A morphism in an abelian category is an inflation of the canonical exact structure if and only if it is a monomorphism.

    source
    @[simp]
    theorem TauCeti.ExactStructure.abelian_isDeflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} (p : Y ⟶ Z) :
    (abelian C).IsDeflation p ↔ CategoryTheory.Epi p

    A morphism in an abelian category is a deflation of the canonical exact structure if and only if it is an epimorphism.

    source
    theorem TauCeti.ExactStructure.abelian_inflations_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] :
    (abelian C).inflations = CategoryTheory.MorphismProperty.monomorphisms C

    The inflations of the canonical exact structure are precisely the monomorphisms.

    source
    theorem TauCeti.ExactStructure.abelian_deflations_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] :
    (abelian C).deflations = CategoryTheory.MorphismProperty.epimorphisms C

    The deflations of the canonical exact structure are precisely the epimorphisms.

    source
    theorem TauCeti.ExactStructure.abelian_conflation_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (i : X ⟶ Y) [CategoryTheory.Mono i] :
    (abelian C).Conflation { X₁ := X, X₂ := Y, X₃ := CategoryTheory.Limits.cokernel i, f := i, g := CategoryTheory.Limits.cokernel.π i, zero := ⋯ }

    In an abelian category, every monomorphism i : X ⟶ Y yields a canonical conflation X ⟶ Y ⟶ cokernel i.

    source
    theorem TauCeti.ExactStructure.abelian_conflation_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} (p : Y ⟶ Z) [CategoryTheory.Epi p] :
    (abelian C).Conflation { X₁ := CategoryTheory.Limits.kernel p, X₂ := Y, X₃ := Z, f := CategoryTheory.Limits.kernel.ι p, g := p, zero := ⋯ }

    In an abelian category, every epimorphism p : Y ⟶ Z yields a canonical conflation kernel p ⟶ Y ⟶ Z.

    source
    theorem TauCeti.ExactStructure.abelian_conflation_op_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
    (abelian Cᵒᵖ).Conflation S.op ↔ (abelian C).Conflation S

    Duality for canonical conflations: the opposite of a short complex in C is a conflation in Cᵒᵖ if and only if the original complex is a conflation in C.

    source
    theorem TauCeti.ExactStructure.abelian_conflation_unop_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex Cᵒᵖ) :
    (abelian C).Conflation S.unop ↔ (abelian Cᵒᵖ).Conflation S

    Duality for canonical conflations: the un-opposite of a short complex in Cᵒᵖ is a conflation in C if and only if the original complex is a conflation in Cᵒᵖ.