Functors between exact categories

An additive functor between categories with chosen exact structures is conflation-exact when it maps every distinguished kernel--cokernel pair to a distinguished kernel--cokernel pair. The name distinguishes this relative notion from Mathlib's CategoryTheory.exactFunctor, which means preservation of finite limits and finite colimits.

This file develops the functorial interface needed by exact Grothendieck groups. Conflation-exact functors preserve inflations and deflations, compose, and are invariant under natural isomorphism. Every additive functor is conflation-exact for the split exact structures. For the canonical exact structures on abelian categories, conflation-exactness is equivalent to Mathlib's finite-limit and finite-colimit exactness.

Main definitions and results

• TauCeti.ExactStructure.IsConflationExact: an additive functor preserves the distinguished conflations.
• TauCeti.ExactStructure.IsConflationExact.map_isInflation and TauCeti.ExactStructure.IsConflationExact.map_isDeflation: the induced preservation results for admissible morphisms.
• TauCeti.ExactStructure.IsConflationExact.id, .comp, and .of_iso: identity, composition, and natural-isomorphism invariance.
• TauCeti.ExactStructure.IsConflationExact.op: opposite-category duality.
• TauCeti.ExactStructure.ReflectsConflations: a functor detects the distinguished conflations, with the corresponding composition and natural-isomorphism API.
• TauCeti.ExactStructure.essSurj_of_lift_conflation: a functor along which every conflation lifts, up to isomorphism of the middle term, is essentially surjective.
• TauCeti.ExactStructure.isConflationExact_split: every additive functor preserves split conflations.
• TauCeti.ExactStructure.isConflationExact_abelian_iff: for canonical abelian exact structures, conflation-exactness agrees with Mathlib's exact-functor predicate.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, https://arxiv.org/abs/0811.1480, Section 5.
• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 7.

structure TauCeti.ExactStructure.IsConflationExact {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) (F : CategoryTheory.Functor C D) [F.Additive] : Prop

An additive functor is conflation-exact when it maps every conflation of the source exact structure to a conflation of the target exact structure.

This is exactness relative to two chosen Quillen exact structures. It is deliberately distinct from CategoryTheory.exactFunctor, the property of preserving finite limits and finite colimits.

• map_conflation {S : CategoryTheory.ShortComplex C} : E.Conflation S → E'.Conflation (S.map F)

  The image under F of a distinguished conflation is distinguished.

theorem TauCeti.ExactStructure.IsConflationExact.map_isKernelCokernelPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) : IsKernelCokernelPair (S.map F)

A conflation-exact functor sends a conflation to a kernel--cokernel pair.

theorem TauCeti.ExactStructure.IsConflationExact.map_isInflation {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) {X Y : C} {i : X ⟶ Y} (hi : E.IsInflation i) : E'.IsInflation (F.map i)

A conflation-exact functor preserves inflations.

theorem TauCeti.ExactStructure.IsConflationExact.map_isDeflation {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) {Y Z : C} {p : Y ⟶ Z} (hp : E.IsDeflation p) : E'.IsDeflation (F.map p)

A conflation-exact functor preserves deflations.

theorem TauCeti.ExactStructure.IsConflationExact.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} : E.IsConflationExact E (CategoryTheory.Functor.id C)

The identity functor is conflation-exact.

theorem TauCeti.ExactStructure.IsConflationExact.comp {C : Type u₁} {D : Type u₂} {K : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Category.{v₃, u₃} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.Limits.HasBinaryBiproducts K] {E : ExactStructure C} {E' : ExactStructure D} {E'' : ExactStructure K} {F : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D K} [F.Additive] [H.Additive] (hF : E.IsConflationExact E' F) (hH : E'.IsConflationExact E'' H) : E.IsConflationExact E'' (F.comp H)

A composite of conflation-exact functors is conflation-exact.

theorem TauCeti.ExactStructure.IsConflationExact.of_iso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : E.IsConflationExact E' F) (e : F ≅ G) : E.IsConflationExact E' G

Conflation-exactness is preserved by replacing a functor with a naturally isomorphic additive functor.

theorem TauCeti.ExactStructure.IsConflationExact.iff_of_iso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (e : F ≅ G) : E.IsConflationExact E' F ↔ E.IsConflationExact E' G

Naturally isomorphic additive functors are conflation-exact together.

theorem TauCeti.ExactStructure.IsConflationExact.op {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) : E.op.IsConflationExact E'.op F.op

Passing to opposite categories preserves conflation-exactness.

structure TauCeti.ExactStructure.ReflectsConflations {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) (F : CategoryTheory.Functor C D) [F.Additive] : Prop

An additive functor reflects conflations when a short complex is a source conflation whenever its image is a target conflation. Together with IsConflationExact, this says that the chosen exact structures agree along the functor.

• reflects_conflation {S : CategoryTheory.ShortComplex C} : E'.Conflation (S.map F) → E.Conflation S

  A short complex whose image is a conflation was already a conflation.

theorem TauCeti.ExactStructure.ReflectsConflations.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} : E.ReflectsConflations E (CategoryTheory.Functor.id C)

The identity functor reflects conflations.

theorem TauCeti.ExactStructure.ReflectsConflations.comp {C : Type u₁} {D : Type u₂} {K : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Category.{v₃, u₃} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.Limits.HasBinaryBiproducts K] {E : ExactStructure C} {E' : ExactStructure D} {E'' : ExactStructure K} {F : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D K} [F.Additive] [H.Additive] (hF : E.ReflectsConflations E' F) (hH : E'.ReflectsConflations E'' H) : E.ReflectsConflations E'' (F.comp H)

A composite of functors which reflect conflations reflects conflations.

theorem TauCeti.ExactStructure.ReflectsConflations.of_iso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : E.ReflectsConflations E' F) (e : F ≅ G) : E.ReflectsConflations E' G

Reflection of conflations is preserved by replacing a functor with a naturally isomorphic additive functor.

theorem TauCeti.ExactStructure.ReflectsConflations.iff_of_iso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (e : F ≅ G) : E.ReflectsConflations E' F ↔ E.ReflectsConflations E' G

Naturally isomorphic additive functors reflect conflations together.

theorem TauCeti.ExactStructure.conflation_map_iff {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hF' : E.ReflectsConflations E' F) (S : CategoryTheory.ShortComplex C) : E'.Conflation (S.map F) ↔ E.Conflation S

If a functor both preserves and reflects conflations, a short complex is distinguished exactly when its image is distinguished.

theorem TauCeti.ExactStructure.isConflationExact_split {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] : (split C).IsConflationExact (split D) F

Every additive functor preserves split conflations.

theorem TauCeti.ExactStructure.essSurj_of_lift_conflation {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {F : CategoryTheory.Functor C D} (hlift : ∀ (S : CategoryTheory.ShortComplex D), E'.Conflation S → ∃ (X : C), Nonempty (F.obj X ≅ S.X₂)) : F.EssSurj

A functor is essentially surjective when the middle term of every target conflation has a preimage up to isomorphism.

theorem TauCeti.ExactStructure.isConflationExact_abelian_iff {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Abelian A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Abelian B] (F : CategoryTheory.Functor A B) [F.Additive] : (abelian A).IsConflationExact (abelian B) F ↔ CategoryTheory.Limits.PreservesFiniteLimits F ∧ CategoryTheory.Limits.PreservesFiniteColimits F

For the canonical exact structures on abelian categories, conflation-exactness is precisely Mathlib's exactness condition: preservation of finite limits and finite colimits.

theorem TauCeti.ExactStructure.isConflationExact_abelian {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Abelian A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Abelian B] (F : CategoryTheory.Functor A B) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (abelian A).IsConflationExact (abelian B) F

An additive functor which is exact in Mathlib's finite-limit and finite-colimit sense is conflation-exact for the canonical exact structures.

theorem TauCeti.ExactStructure.reflectsConflations_abelian_of_faithful {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Abelian A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Abelian B] (F : CategoryTheory.Functor A B) [F.Additive] [F.Faithful] : (abelian A).ReflectsConflations (abelian B) F

A faithful additive functor between abelian categories reflects conflations of the canonical exact structures. No exactness assumption is needed for this direction.