Stable categories of products

The projective stable category of a product of exact categories is additively equivalent to the product of their projective stable categories. The comparison sends a pair to the pair of its stable classes and acts componentwise on morphisms. No Frobenius hypothesis is needed for this additive equivalence: a pair of maps factors through a relative projective exactly when both maps do.

For Frobenius exact categories the product exact structure is Frobenius, and the two projections preserve projective-injectives. Their stable functors therefore admit the suspension comparisons and triangle-functor structures of StableConflationExact.stableFunctorIsTriangulated. The comparison here concerns the additive categories; it does not identify their triangulations.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2 (stable quotients of Frobenius categories).

@[simp]

theorem TauCeti.ExactStructure.mem_prod_projectiveStableIdeal_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) {X Y : C × D} (f : X ⟶ Y) : f ∈ (E.prod E').projectiveStableIdeal.hom X Y ↔ f.1 ∈ E.projectiveStableIdeal.hom X.1 Y.1 ∧ f.2 ∈ E'.projectiveStableIdeal.hom X.2 Y.2

A map in the product is projectively trivial precisely when both components are projectively trivial. Two component factorizations combine through the pair of projectives.

noncomputable def TauCeti.ExactStructure.projectiveStableProdFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : CategoryTheory.Functor (E.prod E').ProjectiveStableCategory (E.ProjectiveStableCategory × E'.ProjectiveStableCategory)

The componentwise comparison from the stable category of a product to the product of stable categories.

Equations

• E.projectiveStableProdFunctor E' = (E.prod E').projectiveStableIdeal.lift (E.projectiveStableFunctor.prod E'.projectiveStableFunctor) ⋯

@[simp]

theorem TauCeti.ExactStructure.projectiveStableProdFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) (X : C × D) : (E.projectiveStableProdFunctor E').obj ((E.prod E').projectiveStableFunctor.obj X) = (E.projectiveStableFunctor.obj X.1, E'.projectiveStableFunctor.obj X.2)

The product comparison sends the class of a pair to the pair of its classes.

@[simp]

theorem TauCeti.ExactStructure.projectiveStableProdFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) {X Y : C × D} (f : X ⟶ Y) : (E.projectiveStableProdFunctor E').map ((E.prod E').projectiveStableFunctor.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map f.1, E'.projectiveStableFunctor.map f.2) (CategoryTheory.eqToHom ⋯))

The product comparison acts componentwise on representatives of stable morphisms.

@[simp]

theorem TauCeti.ExactStructure.projectiveStableFunctor_prod_comp_projectiveStableProdFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : (E.prod E').projectiveStableFunctor.comp (E.projectiveStableProdFunctor E') = E.projectiveStableFunctor.prod E'.projectiveStableFunctor

The product comparison commutes with the quotient functors.

instance TauCeti.ExactStructure.instAdditiveProjectiveStableCategoryProdProdProjectiveStableProdFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : (E.projectiveStableProdFunctor E').Additive

instance TauCeti.ExactStructure.instFaithfulProjectiveStableCategoryProdProdProjectiveStableProdFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : (E.projectiveStableProdFunctor E').Faithful

instance TauCeti.ExactStructure.instFullProjectiveStableCategoryProdProdProjectiveStableProdFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : (E.projectiveStableProdFunctor E').Full

instance TauCeti.ExactStructure.instEssSurjProjectiveStableCategoryProdProdProjectiveStableProdFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : (E.projectiveStableProdFunctor E').EssSurj

instance TauCeti.ExactStructure.instIsEquivalenceProjectiveStableCategoryProdProdProjectiveStableProdFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : (E.projectiveStableProdFunctor E').IsEquivalence

noncomputable def TauCeti.ExactStructure.projectiveStableProdEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : (E.prod E').ProjectiveStableCategory ≌ E.ProjectiveStableCategory × E'.ProjectiveStableCategory

The projective stable category of a product is additively equivalent to the product of the projective stable categories, without an enough-projectives or Frobenius hypothesis.

Equations

• E.projectiveStableProdEquivalence E' = (E.projectiveStableProdFunctor E').asEquivalence

@[simp]

theorem TauCeti.ExactStructure.projectiveStableProdEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : (E.projectiveStableProdEquivalence E').functor = E.projectiveStableProdFunctor E'

The forward functor of the product equivalence is the componentwise comparison.

instance TauCeti.ExactStructure.instAdditiveProjectiveStableCategoryProdProdFunctorProjectiveStableProdEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : (E.projectiveStableProdEquivalence E').functor.Additive

theorem TauCeti.ExactStructure.stableConflationExact_fst_prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : StableConflationExact (E.prod E') E (CategoryTheory.Prod.fst C D)

The first projection of exact categories preserves projective-injectives, and hence induces a stable triangle functor when the exact structures are Frobenius.

theorem TauCeti.ExactStructure.stableConflationExact_snd_prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) : StableConflationExact (E.prod E') E' (CategoryTheory.Prod.snd C D)

The second projection of exact categories preserves projective-injectives, and hence induces a stable triangle functor when the exact structures are Frobenius.

@[simp]

theorem TauCeti.ExactStructure.projectiveStableProdFunctor_comp_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) : (E.projectiveStableProdFunctor E').comp (CategoryTheory.Prod.fst E.ProjectiveStableCategory E'.ProjectiveStableCategory) = ⋯.stableFunctor ⋯

The first component of the product comparison is the stable functor induced by the first projection. Thus its suspension comparison and triangle-functor structure are those already constructed for stable conflation-exact functors.

@[simp]

theorem TauCeti.ExactStructure.projectiveStableProdFunctor_comp_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) : (E.projectiveStableProdFunctor E').comp (CategoryTheory.Prod.snd E.ProjectiveStableCategory E'.ProjectiveStableCategory) = ⋯.stableFunctor ⋯

The second component of the product comparison is the stable functor induced by the second projection, with its existing suspension and triangle-functor structures.