Opposite stable categories

When relative projectives and injectives coincide, the projective stable category of the opposite exact category is additively equivalent to the opposite projective stable category. In particular this applies to every Frobenius exact category. The comparison sends an opposite object to the opposite of its stable class, and does the same on morphisms.

Projectives in the opposite are injectives in the original category. Equality of projectives and injectives identifies the two ideals that must be killed. The quotient comparison then comes from MorphismIdeal.opQuotientFunctor, rather than a second construction of opposite ideal quotients. Enough projectives or injectives are not needed for this additive comparison.

This file constructs the equivalence and its compatibility with the quotient functors. It does not assert compatibility with the shifts or distinguished triangles.

References

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

@[simp]

theorem TauCeti.ExactStructure.projectiveStableIdeal_op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) : E.op.projectiveStableIdeal = E.projectiveStableIdeal.op

If relative projectives and injectives coincide, the projective stable ideal of the opposite exact structure is the opposite projective stable ideal.

noncomputable def TauCeti.ExactStructure.projectiveStableOpFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) : CategoryTheory.Functor E.op.ProjectiveStableCategory E.ProjectiveStableCategoryᵒᵖ

The comparison from the stable category of the opposite to the opposite stable category. It is the lift of the opposite quotient functor.

Equations

• E.projectiveStableOpFunctor hPI = E.op.projectiveStableIdeal.lift E.projectiveStableFunctor.op ⋯

@[simp]

theorem TauCeti.ExactStructure.projectiveStableOpFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) (X : Cᵒᵖ) : (E.projectiveStableOpFunctor hPI).obj (E.op.projectiveStableFunctor.obj X) = Opposite.op (E.projectiveStableFunctor.obj (Opposite.unop X))

The opposite stable comparison has the expected object formula.

@[simp]

theorem TauCeti.ExactStructure.projectiveStableOpFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) {X Y : Cᵒᵖ} (f : X ⟶ Y) : (E.projectiveStableOpFunctor hPI).map (E.op.projectiveStableFunctor.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map f.unop).op (CategoryTheory.eqToHom ⋯))

The opposite stable comparison sends the class of a map to the opposite class of its unopposite. The transports identify the objects using the object formula.

@[simp]

theorem TauCeti.ExactStructure.projectiveStableFunctor_op_comp_projectiveStableOpFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) : E.op.projectiveStableFunctor.comp (E.projectiveStableOpFunctor hPI) = E.projectiveStableFunctor.op

The comparison commutes with taking stable classes and opposites.

instance TauCeti.ExactStructure.instAdditiveProjectiveStableCategoryOppositeOpProjectiveStableOpFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) : (E.projectiveStableOpFunctor hPI).Additive

instance TauCeti.ExactStructure.instIsEquivalenceProjectiveStableCategoryOppositeOpProjectiveStableOpFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) : (E.projectiveStableOpFunctor hPI).IsEquivalence

noncomputable def TauCeti.ExactStructure.projectiveStableOpEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) : E.op.ProjectiveStableCategory ≌ E.ProjectiveStableCategoryᵒᵖ

When relative projectives and injectives coincide, the projective stable category of the opposite is additively equivalent to the opposite projective stable category. No choice of suspension presentations enters this comparison. For a Frobenius structure, take hPI := hE.projective_iff_injective.

Equations

• E.projectiveStableOpEquivalence hPI = (E.projectiveStableOpFunctor hPI).asEquivalence

@[simp]

theorem TauCeti.ExactStructure.projectiveStableOpEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) : (E.projectiveStableOpEquivalence hPI).functor = E.projectiveStableOpFunctor hPI

The forward direction of the opposite stable equivalence is the comparison functor.

instance TauCeti.ExactStructure.instAdditiveProjectiveStableCategoryOppositeOpFunctorProjectiveStableOpEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) : (E.projectiveStableOpEquivalence hPI).functor.Additive

noncomputable def TauCeti.ExactStructure.projectiveStableFunctorOpCompInverseIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hPI : ∀ (X : C), E.isProjective X ↔ E.isInjective X) : E.projectiveStableFunctor.op.comp (E.projectiveStableOpEquivalence hPI).inverse ≅ E.op.projectiveStableFunctor

The inverse comparison carries the opposite stable class of an object back to the stable class of its opposite, naturally in objects of the original opposite category.

Equations

• E.projectiveStableFunctorOpCompInverseIso hPI = (CategoryTheory.eqToIso ⋯).compInverseIso