Functors between projective stable categories

An additive functor between exact categories is stable conflation-exact when it preserves conflations and projective-injective objects. Between Frobenius exact categories, such a functor carries every morphism factoring through a projective to one factoring through a projective. It therefore descends to an additive functor between the projective stable categories.

The construction is functorial: natural transformations and natural isomorphisms descend, identity and composition are preserved, and an equivalence whose two directions are stable conflation-exact induces an equivalence of stable categories.

Main definitions

• TauCeti.StableConflationExact: a conflation-exact additive functor preserving projective-injective objects.
• TauCeti.StableConflationExact.stableFunctor: its induced functor between projective stable categories.
• TauCeti.StableConflationExact.stableNatTrans and .stableNatIso: descent of natural transformations and natural isomorphisms.
• TauCeti.StableConflationExact.stableEquivalence: the stable equivalence induced by an equivalence that is stable conflation-exact in both directions.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.

structure TauCeti.StableConflationExact {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

A conflation-exact functor is stable conflation-exact when it also sends projective-injective objects to projective-injective objects.

• isConflationExact : E.IsConflationExact E' F

  The underlying functor preserves conflations.

• map_projectiveInjective {X : C} : E.projectiveInjective X → E'.projectiveInjective (F.obj X)

  The underlying functor preserves projective-injective objects.

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

The identity functor is stable conflation-exact.

theorem TauCeti.StableConflationExact.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} {G : CategoryTheory.Functor D K} [F.Additive] [G.Additive] (hF : StableConflationExact E E' F) (hG : StableConflationExact E' E'' G) : StableConflationExact E E'' (F.comp G)

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

theorem TauCeti.StableConflationExact.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 : StableConflationExact E E' F) (e : F ≅ G) : StableConflationExact E E' G

Stable conflation-exactness is preserved by replacing a functor by a naturally isomorphic additive functor.

theorem TauCeti.StableConflationExact.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) : StableConflationExact E E' F ↔ StableConflationExact E E' G

Naturally isomorphic additive functors are stable conflation-exact together.

theorem TauCeti.StableConflationExact.projectiveStableIdeal_le_comap {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 : StableConflationExact E E' F) (hE : E.IsFrobenius) : E.projectiveStableIdeal ≤ E'.projectiveStableIdeal.comap F

Between Frobenius exact categories, a stable conflation-exact functor carries the projective stable ideal of the source into the projective stable ideal of the target.

noncomputable def TauCeti.StableConflationExact.stableFunctor {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 : StableConflationExact E E' F) (hE : E.IsFrobenius) : CategoryTheory.Functor E.ProjectiveStableCategory E'.ProjectiveStableCategory

A stable conflation-exact functor between Frobenius exact categories descends to their projective stable categories.

Equations

• hF.stableFunctor hE = E.projectiveStableIdeal.map E'.projectiveStableIdeal F ⋯

theorem TauCeti.StableConflationExact.stableFunctor_eq_map {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 : StableConflationExact E E' F) (hE : E.IsFrobenius) : hF.stableFunctor hE = E.projectiveStableIdeal.map E'.projectiveStableIdeal F ⋯

The stable functor is the map on ideal quotients induced by the original functor.

instance TauCeti.StableConflationExact.stableFunctor_full {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] [F.Full] (hF : StableConflationExact E E' F) (hE : E.IsFrobenius) : (hF.stableFunctor hE).Full

A full stable conflation-exact functor induces a full functor on stable categories.

@[simp]

theorem TauCeti.StableConflationExact.stableFunctor_obj_projectiveStableFunctor_obj {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 : StableConflationExact E E' F) (hE : E.IsFrobenius) (X : C) : (hF.stableFunctor hE).obj (E.projectiveStableFunctor.obj X) = E'.projectiveStableFunctor.obj (F.obj X)

The stable functor applies the original functor on objects from the exact category.

@[simp]

theorem TauCeti.StableConflationExact.stableFunctor_map_projectiveStableFunctor_map {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 : StableConflationExact E E' F) (hE : E.IsFrobenius) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((hF.stableFunctor hE).map (E.projectiveStableFunctor.map f)) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (E'.projectiveStableFunctor.map (F.map f))

The stable functor applies the original functor to representatives of stable morphisms.

@[simp]

theorem TauCeti.StableConflationExact.stableFunctor_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) : ⋯.stableFunctor hE = CategoryTheory.Functor.id E.ProjectiveStableCategory

Descent sends the identity stable conflation-exact functor to the identity functor.

theorem TauCeti.StableConflationExact.stableFunctor_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} {G : CategoryTheory.Functor D K} [F.Additive] [G.Additive] (hF : StableConflationExact E E' F) (hG : StableConflationExact E' E'' G) (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) : ⋯.stableFunctor hE = (hF.stableFunctor hE).comp (hG.stableFunctor hE')

Descent carries a composite of stable conflation-exact functors to the composite of their stable functors.

noncomputable def TauCeti.StableConflationExact.stableNatTrans {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 : StableConflationExact E E' F) (hG : StableConflationExact E E' G) (hE : E.IsFrobenius) (α : F ⟶ G) : hF.stableFunctor hE ⟶ hG.stableFunctor hE

A natural transformation between stable conflation-exact functors descends to a natural transformation between their stable functors.

Equations

• hF.stableNatTrans hG hE α = E.projectiveStableIdeal.mapNatTrans E'.projectiveStableIdeal ⋯ ⋯ α

@[simp]

theorem TauCeti.StableConflationExact.stableNatTrans_app_projectiveStableFunctor_obj {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 : StableConflationExact E E' F) (hG : StableConflationExact E E' G) (hE : E.IsFrobenius) (α : F ⟶ G) (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((hF.stableNatTrans hG hE α).app (E.projectiveStableFunctor.obj X)) (CategoryTheory.eqToHom ⋯)) = E'.projectiveStableFunctor.map (α.app X)

On objects from the exact category, a descended natural transformation is represented by the corresponding component of the original transformation.

@[simp]

theorem TauCeti.StableConflationExact.stableNatTrans_id {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 : StableConflationExact E E' F) (hE : E.IsFrobenius) : hF.stableNatTrans hF hE (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (hF.stableFunctor hE)

Descent sends the identity natural transformation to the identity.

@[simp]

theorem TauCeti.StableConflationExact.stableNatTrans_comp {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 H : CategoryTheory.Functor C D} [F.Additive] [G.Additive] [H.Additive] (hF : StableConflationExact E E' F) (hG : StableConflationExact E E' G) (hH : StableConflationExact E E' H) (hE : E.IsFrobenius) (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.CategoryStruct.comp (hF.stableNatTrans hG hE α) (hG.stableNatTrans hH hE β) = hF.stableNatTrans hH hE (CategoryTheory.CategoryStruct.comp α β)

Descent preserves vertical composition of natural transformations.

noncomputable def TauCeti.StableConflationExact.stableNatIso {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 : StableConflationExact E E' F) (hG : StableConflationExact E E' G) (hE : E.IsFrobenius) (α : F ≅ G) : hF.stableFunctor hE ≅ hG.stableFunctor hE

A natural isomorphism between stable conflation-exact functors descends to a natural isomorphism between their stable functors.

Equations

• hF.stableNatIso hG hE α = E.projectiveStableIdeal.mapNatIso E'.projectiveStableIdeal ⋯ ⋯ α

@[simp]

theorem TauCeti.StableConflationExact.stableNatIso_hom {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 : StableConflationExact E E' F) (hG : StableConflationExact E E' G) (hE : E.IsFrobenius) (α : F ≅ G) : (hF.stableNatIso hG hE α).hom = hF.stableNatTrans hG hE α.hom

The forward component of a descended natural isomorphism is the descended transformation.

@[simp]

theorem TauCeti.StableConflationExact.stableNatIso_inv {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 : StableConflationExact E E' F) (hG : StableConflationExact E E' G) (hE : E.IsFrobenius) (α : F ≅ G) : (hF.stableNatIso hG hE α).inv = hG.stableNatTrans hF hE α.inv

The inverse component of a descended natural isomorphism is the descended inverse.

noncomputable def TauCeti.StableConflationExact.stableEquivalence {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} (e : C ≌ D) [e.functor.Additive] [e.inverse.Additive] (hF : StableConflationExact E E' e.functor) (hG : StableConflationExact E' E e.inverse) (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) : E.ProjectiveStableCategory ≌ E'.ProjectiveStableCategory

An equivalence which is stable conflation-exact in both directions induces an equivalence of projective stable categories.

Equations

• TauCeti.StableConflationExact.stableEquivalence e hF hG hE hE' = TauCeti.MorphismIdeal.mapEquivalence e E.projectiveStableIdeal E'.projectiveStableIdeal ⋯

@[simp]

theorem TauCeti.StableConflationExact.stableEquivalence_functor {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} (e : C ≌ D) [e.functor.Additive] [e.inverse.Additive] (hF : StableConflationExact E E' e.functor) (hG : StableConflationExact E' E e.inverse) (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) : (stableEquivalence e hF hG hE hE').functor = hF.stableFunctor hE

The functor of the induced stable equivalence is the descended forward functor.

@[simp]

theorem TauCeti.StableConflationExact.stableEquivalence_inverse {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} (e : C ≌ D) [e.functor.Additive] [e.inverse.Additive] (hF : StableConflationExact E E' e.functor) (hG : StableConflationExact E' E e.inverse) (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) : (stableEquivalence e hF hG hE hE').inverse = hG.stableFunctor hE'

The inverse of the induced stable equivalence is the descended inverse functor.