The cone of a morphism in a Frobenius exact category

Let E be a Frobenius exact structure with chosen conflations X ⟶ I(X) ⟶ ΣX. The cone of a morphism f : X ⟶ Y is the pushout

X  --i(X)-->  I(X)
|               |
-f              |
v               v
Y  ------->  cone f

of the chosen inflation of X along -f. The sign is what makes the associated conflation of the pushout square read

X --(i(X), f)--> I(X) ⊞ Y --> cone f,

so that the cone is the cokernel of (i(X), f).

That conflation is the point of the construction. Since I(X) is projective-injective, the biproduct inclusion Y ⟶ I(X) ⊞ Y becomes an isomorphism in the projective stable category and carries f to the inflation of the conflation. Thus every morphism of the underlying category is, up to a canonical isomorphism of its target in the stable category, the inflation of a conflation, and f acquires the standard sequence

X ⟶ Y ⟶ cone f ⟶ ΣX

whose last map is the connecting morphism of the cone conflation. This file constructs the cone together with that sequence, proves that consecutive composites vanish in the stable category, and makes the cone act on commutative squares.

The cone extends the construction it is modelled on. When f is already the inflation of a conflation X ⟶ Y ⟶ Z, the cone of f is an extension of Z by the projective-injective I(X), so it represents Z in the stable category.

Main definitions

• TauCeti.ExactStructure.IsFrobenius.coneObj: the cone cone f of f : X ⟶ Y.
• TauCeti.ExactStructure.IsFrobenius.coneInclusion: the map Y ⟶ cone f.
• TauCeti.ExactStructure.IsFrobenius.coneInjectiveMap: the map I(X) ⟶ cone f.
• TauCeti.ExactStructure.IsFrobenius.coneConnectingMap: the map cone f ⟶ ΣX.
• TauCeti.ExactStructure.IsFrobenius.coneSequence: the conflation Y ⟶ cone(f) ⟶ ΣX.
• TauCeti.ExactStructure.IsFrobenius.coneMap: the map of cones induced by a commutative square.
• TauCeti.ExactStructure.IsFrobenius.coneComparison: the map from the cone of the first map of a short complex to its third term.

Main results

• TauCeti.ExactStructure.IsFrobenius.isPushout_cone: the defining pushout square, which supplies the universal property of the cone.
• TauCeti.ExactStructure.IsFrobenius.conflation_cone: the conflation X ⟶ I(X) ⊞ Y ⟶ cone f.
• TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_coneInflation: in the stable category, the inflation of the cone conflation is f followed by the isomorphism Y ≅ I(X) ⊞ Y.
• TauCeti.ExactStructure.IsFrobenius.conflation_coneSequence: the cone sequence is the cobase change of the chosen suspension conflation.
• TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_comp_coneInclusion, TauCeti.ExactStructure.IsFrobenius.coneInclusion_comp_coneConnectingMap and projectiveStableFunctor_map_coneConnectingMap_comp_cokernelMap: consecutive composites of X ⟶ Y ⟶ cone f ⟶ ΣX ⟶ ΣY vanish in the stable category.
• TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_connectingMap_cone: the connecting morphism of the cone conflation is coneConnectingMap f.
• TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_coneMap_id and TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_coneMap_comp: cone maps preserve identities and composition in the stable category.
• TauCeti.ExactStructure.IsFrobenius.conflation_coneComparison and TauCeti.ExactStructure.IsFrobenius.isIso_projectiveStableFunctor_map_coneComparison: the cone of the inflation of a conflation is an extension of its third term by I(X), and represents that third term in the stable category.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.
• Bernhard Keller, Chain complexes and stable categories, Manuscripta Mathematica 67 (1990), 379–417, Section 1.
• Theo Bühler, Exact Categories, Expositiones Mathematicae 28 (2010), 1–69, Proposition 2.12.

noncomputable def TauCeti.ExactStructure.IsFrobenius.coneObj {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) : C

The cone of f : X ⟶ Y: the pushout of the chosen inflation X ⟶ I(X) along -f.

Equations

• hE.coneObj f = CategoryTheory.Limits.pushout (hE.suspensionInflation X) (-f)

noncomputable def TauCeti.ExactStructure.IsFrobenius.coneInjectiveMap {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.suspensionInjective X ⟶ hE.coneObj f

The map from the chosen injective object of X to the cone of f : X ⟶ Y.

Equations

• hE.coneInjectiveMap f = CategoryTheory.Limits.pushout.inl (hE.suspensionInflation X) (-f)

noncomputable def TauCeti.ExactStructure.IsFrobenius.coneInclusion {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) : Y ⟶ hE.coneObj f

The map from the target of f : X ⟶ Y to its cone.

Equations

• hE.coneInclusion f = CategoryTheory.Limits.pushout.inr (hE.suspensionInflation X) (-f)

theorem TauCeti.ExactStructure.IsFrobenius.isPushout_cone {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.IsPushout (hE.suspensionInflation X) (-f) (hE.coneInjectiveMap f) (hE.coneInclusion f)

The cone of f is the pushout of the chosen inflation X ⟶ I(X) along -f. This is the universal property of the cone.

theorem TauCeti.ExactStructure.IsFrobenius.suspensionInflation_comp_coneInjectiveMap {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.CategoryStruct.comp (hE.suspensionInflation X) (hE.coneInjectiveMap f) = -CategoryTheory.CategoryStruct.comp f (hE.coneInclusion f)

The defining square of the cone, with the sign moved onto the injective side.

theorem TauCeti.ExactStructure.IsFrobenius.suspensionInflation_comp_coneInjectiveMap_assoc {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) {Z : C} (h : hE.coneObj f ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.suspensionInflation X) (CategoryTheory.CategoryStruct.comp (hE.coneInjectiveMap f) h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp f (hE.coneInclusion f)) h

The defining square of the cone, with the sign moved onto the injective side.

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.IsFrobenius.coneInflation {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) : X ⟶ hE.suspensionInjective X ⊞ Y

The inflation (i(X), f) : X ⟶ I(X) ⊞ Y of the cone conflation of f.

Equations

• hE.coneInflation f = CategoryTheory.Limits.biprod.lift (hE.suspensionInflation X) f

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.IsFrobenius.coneDeflation {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.suspensionInjective X ⊞ Y ⟶ hE.coneObj f

The deflation I(X) ⊞ Y ⟶ cone f of the cone conflation of f.

Equations

• hE.coneDeflation f = CategoryTheory.Limits.biprod.desc (hE.coneInjectiveMap f) (hE.coneInclusion f)

theorem TauCeti.ExactStructure.IsFrobenius.coneInflation_comp_coneDeflation {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.CategoryStruct.comp (hE.coneInflation f) (hE.coneDeflation f) = 0

The two maps of the cone conflation compose to zero.

theorem TauCeti.ExactStructure.IsFrobenius.coneInflation_comp_coneDeflation_assoc {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) {Z : C} (h : hE.coneObj f ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.coneInflation f) (CategoryTheory.CategoryStruct.comp (hE.coneDeflation f) h) = CategoryTheory.CategoryStruct.comp 0 h

The two maps of the cone conflation compose to zero.

theorem TauCeti.ExactStructure.IsFrobenius.conflation_cone {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) : E.Conflation { X₁ := X, X₂ := hE.suspensionInjective X ⊞ Y, X₃ := hE.coneObj f, f := hE.coneInflation f, g := hE.coneDeflation f, zero := ⋯ }

The cone conflation of f : X ⟶ Y: the cone is the cokernel of the inflation (i(X), f) : X ⟶ I(X) ⊞ Y.

noncomputable def TauCeti.ExactStructure.IsFrobenius.coneConnectingMap {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.coneObj f ⟶ hE.suspensionObj X

The connecting map cone f ⟶ ΣX of the cone of f : X ⟶ Y, induced by the chosen deflation I(X) ⟶ ΣX and the zero map on Y.

Equations

• hE.coneConnectingMap f = ⋯.desc (hE.suspensionDeflation X) 0 ⋯

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInjectiveMap_comp_coneConnectingMap {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.CategoryStruct.comp (hE.coneInjectiveMap f) (hE.coneConnectingMap f) = hE.suspensionDeflation X

The connecting map of the cone restricts on the injective object to the chosen suspension deflation.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInjectiveMap_comp_coneConnectingMap_assoc {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) {Z : C} (h : hE.suspensionObj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.coneInjectiveMap f) (CategoryTheory.CategoryStruct.comp (hE.coneConnectingMap f) h) = CategoryTheory.CategoryStruct.comp (hE.suspensionDeflation X) h

The connecting map of the cone restricts on the injective object to the chosen suspension deflation.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInclusion_comp_coneConnectingMap {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.CategoryStruct.comp (hE.coneInclusion f) (hE.coneConnectingMap f) = 0

The composite Y ⟶ cone f ⟶ ΣX of the cone sequence vanishes.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInclusion_comp_coneConnectingMap_assoc {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) {Z : C} (h : hE.suspensionObj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.coneInclusion f) (CategoryTheory.CategoryStruct.comp (hE.coneConnectingMap f) h) = CategoryTheory.CategoryStruct.comp 0 h

The composite Y ⟶ cone f ⟶ ΣX of the cone sequence vanishes.

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.IsFrobenius.coneSequence {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.ShortComplex C

The cone sequence Y ⟶ cone(f) ⟶ ΣX. It is the cobase change of the chosen suspension presentation of X along -f.

Equations

• hE.coneSequence f = { X₁ := Y, X₂ := hE.coneObj f, X₃ := hE.suspensionObj X, f := hE.coneInclusion f, g := hE.coneConnectingMap f, zero := ⋯ }

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneSequence_X₁ {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.coneSequence f).X₁ = Y

The first object of the cone sequence is its codomain.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneSequence_X₂ {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.coneSequence f).X₂ = hE.coneObj f

The middle object of the cone sequence is the cone.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneSequence_X₃ {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.coneSequence f).X₃ = hE.suspensionObj X

The last object of the cone sequence is the chosen suspension.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneSequence_f {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.coneSequence f).f = hE.coneInclusion f

The first map of the cone sequence is the cone inclusion.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneSequence_g {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.coneSequence f).g = hE.coneConnectingMap f

The second map of the cone sequence is the cone connecting map.

theorem TauCeti.ExactStructure.IsFrobenius.conflation_coneSequence {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) : E.Conflation (hE.coneSequence f)

The cone sequence is a conflation.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_coneInflation {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) : E.projectiveStableFunctor.map (hE.coneInflation f) = CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map f) (E.projectiveStableIsoBiprod ⋯ Y).hom

In the projective stable category, the inflation of the cone conflation of f is f followed by the isomorphism Y ≅ I(X) ⊞ Y.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_comp_coneInclusion {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.CategoryStruct.comp (E.projectiveStableFunctor.map f) (E.projectiveStableFunctor.map (hE.coneInclusion f)) = 0

The composite X ⟶ Y ⟶ cone f of the cone sequence vanishes in the projective stable category: it factors through the injective I(X).

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_connectingMap_cone {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) : E.projectiveStableFunctor.map (hE.connectingMap ⋯) = E.projectiveStableFunctor.map (hE.coneConnectingMap f)

The connecting morphism of the cone conflation is the connecting map of the cone.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_coneConnectingMap_comp_cokernelMap {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.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.coneConnectingMap f)) (E.projectiveStableFunctor.map ((hE.suspensionPresentation X).cokernelMap (hE.suspensionPresentation Y) f)) = 0

The composite cone f ⟶ ΣX ⟶ ΣY of the cone sequence vanishes in the projective stable category: it factors through the injective I(Y).

noncomputable def TauCeti.ExactStructure.IsFrobenius.coneMap {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 X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'} (a : X ⟶ X') (b : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') : hE.coneObj f ⟶ hE.coneObj f'

The map of cones induced by a commutative square f ≫ b = a ≫ f'.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInjectiveMap_comp_coneMap {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 X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'} (a : X ⟶ X') (b : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') : CategoryTheory.CategoryStruct.comp (hE.coneInjectiveMap f) (hE.coneMap a b w) = CategoryTheory.CategoryStruct.comp ((hE.suspensionPresentation X).middleMap (hE.suspensionPresentation X') a) (hE.coneInjectiveMap f')

The cone map restricts on the injective objects to the map induced by a on the chosen injective presentations.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInjectiveMap_comp_coneMap_assoc {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 X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'} (a : X ⟶ X') (b : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') {Z : C} (h : hE.coneObj f' ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.coneInjectiveMap f) (CategoryTheory.CategoryStruct.comp (hE.coneMap a b w) h) = CategoryTheory.CategoryStruct.comp ((hE.suspensionPresentation X).middleMap (hE.suspensionPresentation X') a) (CategoryTheory.CategoryStruct.comp (hE.coneInjectiveMap f') h)

The cone map restricts on the injective objects to the map induced by a on the chosen injective presentations.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInclusion_comp_coneMap {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 X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'} (a : X ⟶ X') (b : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') : CategoryTheory.CategoryStruct.comp (hE.coneInclusion f) (hE.coneMap a b w) = CategoryTheory.CategoryStruct.comp b (hE.coneInclusion f')

The cone map commutes with the cone inclusions.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInclusion_comp_coneMap_assoc {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 X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'} (a : X ⟶ X') (b : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') {Z : C} (h : hE.coneObj f' ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.coneInclusion f) (CategoryTheory.CategoryStruct.comp (hE.coneMap a b w) h) = CategoryTheory.CategoryStruct.comp b (CategoryTheory.CategoryStruct.comp (hE.coneInclusion f') h)

The cone map commutes with the cone inclusions.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_coneMap_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) {X Y : C} (f : X ⟶ Y) : E.projectiveStableFunctor.map (hE.coneMap (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) ⋯) = CategoryTheory.CategoryStruct.id (E.projectiveStableFunctor.obj (hE.coneObj f))

Cone maps preserve identities in the projective stable category. The equality need not hold before passing to the stable category because the chosen maps between injective presentations need not preserve identities strictly.

theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_coneMap_comp {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 X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'} {X'' Y'' : C} {f'' : X'' ⟶ Y''} (a : X ⟶ X') (b : Y ⟶ Y') (a' : X' ⟶ X'') (b' : Y' ⟶ Y'') (w : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') (w' : CategoryTheory.CategoryStruct.comp f' b' = CategoryTheory.CategoryStruct.comp a' f'') : E.projectiveStableFunctor.map (hE.coneMap (CategoryTheory.CategoryStruct.comp a a') (CategoryTheory.CategoryStruct.comp b b') ⋯) = CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.coneMap a b w)) (E.projectiveStableFunctor.map (hE.coneMap a' b' w'))

Cone maps preserve composition in the projective stable category. The equality need not hold before passing to the stable category because the chosen maps between injective presentations need not preserve composition strictly.

This is not a simp lemma: the left-hand side mentions neither the intermediate morphism f' nor the two squares w and w', so simp could never instantiate them.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneMap_comp_coneConnectingMap {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 X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'} (a : X ⟶ X') (b : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') : CategoryTheory.CategoryStruct.comp (hE.coneMap a b w) (hE.coneConnectingMap f') = CategoryTheory.CategoryStruct.comp (hE.coneConnectingMap f) ((hE.suspensionPresentation X).cokernelMap (hE.suspensionPresentation X') a)

The cone map commutes with the connecting maps and the map induced by a on the cokernel terms of the chosen injective presentations.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneMap_comp_coneConnectingMap_assoc {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 X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'} (a : X ⟶ X') (b : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') {Z : C} (h : hE.suspensionObj X' ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.coneMap a b w) (CategoryTheory.CategoryStruct.comp (hE.coneConnectingMap f') h) = CategoryTheory.CategoryStruct.comp (hE.coneConnectingMap f) (CategoryTheory.CategoryStruct.comp ((hE.suspensionPresentation X).cokernelMap (hE.suspensionPresentation X') a) h)

The cone map commutes with the connecting maps and the map induced by a on the cokernel terms of the chosen injective presentations.

noncomputable def TauCeti.ExactStructure.IsFrobenius.coneComparison {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) : hE.coneObj S.f ⟶ S.X₃

The comparison from the cone of the first map of a short complex X ⟶ Y ⟶ Z to its third term Z, induced by the zero map on I(X) and by the second map on Y.

Equations

• hE.coneComparison S = ⋯.desc 0 S.g ⋯

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInjectiveMap_comp_coneComparison {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) : CategoryTheory.CategoryStruct.comp (hE.coneInjectiveMap S.f) (hE.coneComparison S) = 0

The comparison kills the injective object of the cone.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInjectiveMap_comp_coneComparison_assoc {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) {Z : C} (h : S.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.coneInjectiveMap S.f) (CategoryTheory.CategoryStruct.comp (hE.coneComparison S) h) = CategoryTheory.CategoryStruct.comp 0 h

The comparison kills the injective object of the cone.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInclusion_comp_coneComparison {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) : CategoryTheory.CategoryStruct.comp (hE.coneInclusion S.f) (hE.coneComparison S) = S.g

The comparison carries the cone inclusion to the second map of the short complex.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.coneInclusion_comp_coneComparison_assoc {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) {Z : C} (h : S.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.coneInclusion S.f) (CategoryTheory.CategoryStruct.comp (hE.coneComparison S) h) = CategoryTheory.CategoryStruct.comp S.g h

The comparison carries the cone inclusion to the second map of the short complex.

noncomputable def TauCeti.ExactStructure.IsFrobenius.isColimitConeComparison {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} (hkc : IsKernelCokernelPair S) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (hE.coneComparison S) ⋯)

The third term of a kernel–cokernel pair is the cokernel of the injective object inside the cone of its first map.

Equations

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

theorem TauCeti.ExactStructure.IsFrobenius.conflation_coneComparison {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) : E.Conflation { X₁ := hE.suspensionInjective S.X₁, X₂ := hE.coneObj S.f, X₃ := S.X₃, f := hE.coneInjectiveMap S.f, g := hE.coneComparison S, zero := ⋯ }

The cone of the inflation of a conflation differs from its third term by the chosen injective object: I(X) ⟶ cone S.f ⟶ Z is a conflation.

theorem TauCeti.ExactStructure.IsFrobenius.isIso_projectiveStableFunctor_map_coneComparison {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.IsIso (E.projectiveStableFunctor.map (hE.coneComparison S))

The cone of the inflation of a conflation represents its third term in the projective stable category, because it differs from it by a projective-injective summand.