Standard triangles in the stable category

This file gives the standard Happel triangles in the projective stable quotient of a Frobenius exact category. A conflation is sent to a triangle in the stable category by the quotient functor, its connecting map, and the comparison between the chosen suspension object and the stable suspension. The cone of an arbitrary morphism is identified with the standard triangle of its cone conflation, and the cone triangle on the inflation of any conflation is identified with that conflation's stable triangle. This construction follows Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2. Morphisms between objects in the stable category are handled by choosing a representative in the exact category.

The isomorphism-closed class of distinguished triangles records the triangles arising from conflations. The cone construction shows that the standard cone triangles belong to this class.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableConflationTriangle {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) (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S) : CategoryTheory.Pretriangulated.Triangle E.ProjectiveStableCategory

The stable image of a conflation, with its connecting map transported to the suspension shift.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.ExactStructure.IsFrobenius.stableConflationTriangle_eq_mk {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) (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S) : hE.stableConflationTriangle S hS = CategoryTheory.Pretriangulated.Triangle.mk (E.projectiveStableFunctor.map S.f) (E.projectiveStableFunctor.map S.g) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.connectingMap hS)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (hE.stableShiftFunctorOneIso.inv.app (E.projectiveStableFunctor.obj S.X₁))))

The stable conflation triangle written with its three explicit arrows.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConflationTriangle_obj₁ {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) (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S) : (hE.stableConflationTriangle S hS).obj₁ = E.projectiveStableFunctor.obj S.X₁

The first object of the stable conflation triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConflationTriangle_obj₂ {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) (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S) : (hE.stableConflationTriangle S hS).obj₂ = E.projectiveStableFunctor.obj S.X₂

The second object of the stable conflation triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConflationTriangle_obj₃ {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) (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S) : (hE.stableConflationTriangle S hS).obj₃ = E.projectiveStableFunctor.obj S.X₃

The third object of the stable conflation triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConflationTriangle_mor₁ {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) (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S) : (hE.stableConflationTriangle S hS).mor₁ ≍ E.projectiveStableFunctor.map S.f

The first morphism of the stable conflation triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConflationTriangle_mor₂ {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) (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S) : (hE.stableConflationTriangle S hS).mor₂ ≍ E.projectiveStableFunctor.map S.g

The second morphism of the stable conflation triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConflationTriangle_mor₃ {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) (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S) : (hE.stableConflationTriangle S hS).mor₃ ≍ CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.connectingMap hS)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (hE.stableShiftFunctorOneIso.inv.app (E.projectiveStableFunctor.obj S.X₁)))

The third morphism of the stable conflation triangle.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableDistinguishedTriangles {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) : Set (CategoryTheory.Pretriangulated.Triangle E.ProjectiveStableCategory)

The distinguished triangles generated by conflations, up to isomorphism.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.ExactStructure.IsFrobenius.mem_stableDistinguishedTriangles_iff {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) (T : CategoryTheory.Pretriangulated.Triangle E.ProjectiveStableCategory) : T ∈ hE.stableDistinguishedTriangles ↔ ∃ (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S), Nonempty (T ≅ hE.stableConflationTriangle S hS)

Membership in the distinguished stable triangles means being isomorphic to a conflation triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConflationTriangle_mem {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) (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S) : hE.stableConflationTriangle S hS ∈ hE.stableDistinguishedTriangles

A standard conflation triangle is distinguished.

theorem TauCeti.ExactStructure.IsFrobenius.stableDistinguishedTriangles_isomorphic {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) {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle E.ProjectiveStableCategory} (hT₁ : T₁ ∈ hE.stableDistinguishedTriangles) (e : T₁ ≅ T₂) : T₂ ∈ hE.stableDistinguishedTriangles

Distinguished triangles are closed under isomorphism in the stable category.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableConeTriangle {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) {X Y : C} (f : X ⟶ Y) : CategoryTheory.Pretriangulated.Triangle E.ProjectiveStableCategory

The stable triangle associated to an arbitrary morphism through its cone.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangle_eq_mk {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) {X Y : C} (f : X ⟶ Y) : hE.stableConeTriangle f = CategoryTheory.Pretriangulated.Triangle.mk (E.projectiveStableFunctor.map f) (E.projectiveStableFunctor.map (hE.coneInclusion f)) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.coneConnectingMap f)) (hE.stableSuspensionObjIsoShift X).hom)

The stable cone triangle written using the canonical comparison from the chosen suspension object to the shift.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangle_obj₁ {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) {X Y : C} (f : X ⟶ Y) : (hE.stableConeTriangle f).obj₁ = E.projectiveStableFunctor.obj X

The first object of the stable cone triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangle_obj₂ {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) {X Y : C} (f : X ⟶ Y) : (hE.stableConeTriangle f).obj₂ = E.projectiveStableFunctor.obj Y

The second object of the stable cone triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangle_obj₃ {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) {X Y : C} (f : X ⟶ Y) : (hE.stableConeTriangle f).obj₃ = E.projectiveStableFunctor.obj (hE.coneObj f)

The third object of the stable cone triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangle_mor₁ {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) {X Y : C} (f : X ⟶ Y) : (hE.stableConeTriangle f).mor₁ ≍ E.projectiveStableFunctor.map f

The first morphism of the stable cone triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangle_mor₂ {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) {X Y : C} (f : X ⟶ Y) : (hE.stableConeTriangle f).mor₂ ≍ E.projectiveStableFunctor.map (hE.coneInclusion f)

The second morphism of the stable cone triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangle_mor₃ {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) {X Y : C} (f : X ⟶ Y) : (hE.stableConeTriangle f).mor₃ ≍ CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.coneConnectingMap f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (hE.stableShiftFunctorOneIso.inv.app (E.projectiveStableFunctor.obj X)))

The third morphism of the stable cone triangle.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableConeTriangleIsoConflation {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) {X Y : C} (f : X ⟶ Y) : hE.stableConeTriangle f ≅ hE.stableConflationTriangle { X₁ := X, X₂ := hE.suspensionInjective X ⊞ Y, X₃ := hE.coneObj f, f := hE.coneInflation f, g := hE.coneDeflation f, zero := ⋯ } ⋯

The cone triangle is isomorphic to the standard triangle of the cone conflation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableConeTriangleIsoStableConflation {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) (S : CategoryTheory.ShortComplex C) (hS : E.Conflation S) : hE.stableConeTriangle S.f ≅ hE.stableConflationTriangle S hS

The cone triangle on the inflation of a conflation is isomorphic to that conflation's stable triangle. The third component is the stable isomorphism from the cone to the cokernel.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangle_mem {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) {X Y : C} (f : X ⟶ Y) : hE.stableConeTriangle f ∈ hE.stableDistinguishedTriangles

The cone triangle is distinguished.

noncomputable def TauCeti.ExactStructure.IsFrobenius.stableConeTriangleOf {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) {X Y : C} (f : E.projectiveStableFunctor.obj X ⟶ E.projectiveStableFunctor.obj Y) : CategoryTheory.Pretriangulated.Triangle E.ProjectiveStableCategory

A cone triangle for a morphism between objects in the projective stable category, represented by a morphism in the Frobenius exact category.

Equations

• hE.stableConeTriangleOf f = hE.stableConeTriangle (Classical.choose ⋯)

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangleOf_exists_rep {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) {X Y : C} (f : E.projectiveStableFunctor.obj X ⟶ E.projectiveStableFunctor.obj Y) : ∃ (g : X ⟶ Y), E.projectiveStableFunctor.map g = f ∧ hE.stableConeTriangleOf f = hE.stableConeTriangle g

A chosen stable cone triangle is the cone triangle of a representative of its morphism.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangleOf_mor₁ {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) {X Y : C} (f : E.projectiveStableFunctor.obj X ⟶ E.projectiveStableFunctor.obj Y) : (hE.stableConeTriangleOf f).mor₁ ≍ f

The first morphism of the chosen stable cone triangle is the given stable-category morphism.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangleOf_obj₁ {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) {X Y : C} (f : E.projectiveStableFunctor.obj X ⟶ E.projectiveStableFunctor.obj Y) : (hE.stableConeTriangleOf f).obj₁ = E.projectiveStableFunctor.obj X

The first object of the chosen stable cone triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangleOf_obj₂ {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) {X Y : C} (f : E.projectiveStableFunctor.obj X ⟶ E.projectiveStableFunctor.obj Y) : (hE.stableConeTriangleOf f).obj₂ = E.projectiveStableFunctor.obj Y

The second object of the chosen stable cone triangle.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.stableConeTriangleOf_mem {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) {X Y : C} (f : E.projectiveStableFunctor.obj X ⟶ E.projectiveStableFunctor.obj Y) : hE.stableConeTriangleOf f ∈ hE.stableDistinguishedTriangles

The cone triangle of any stable-category morphism is distinguished.