Mapping cones of X - a on a polynomial extension of a complex

Let K be a complex of modules over a commutative ring A. Its polynomial extension K[X] = A[X] ⊗[A] K is again a complex of A-modules, and multiplication by any polynomial p : A[X] is a chain endomorphism of it. For a : A, the mapping cone of multiplication by X - a on K[X] is homotopy equivalent to K.

The reason is that the short exact sequence of A-modules

0 ⟶ A[X] ⟶ A[X] ⟶ A ⟶ 0,

given by multiplication by X - a followed by evaluation at a, is split by division by X - a and by the inclusion of constants. Tensoring with K keeps it split in the category of complexes, so CategoryTheory.ShortComplex.Splitting.homotopyCofiberHomotopyEquiv applies.

This is the algebra behind the stabilization invariance of grid homology: the complex of a stabilized grid diagram is identified with the mapping cone of V₁ - V₂ on the polynomial extension GC⁻(G)[V₁] of the complex of the original diagram, and the homotopy equivalence here compares that cone with GC⁻(G) itself.

Main definitions

• HomologicalComplex.polynomialExtension: the complex A[X] ⊗[A] K.
• HomologicalComplex.polynomialExtensionMul: multiplication by a polynomial on A[X] ⊗[A] K.
• HomologicalComplex.polynomialExtensionEval: evaluation at a, a chain map A[X] ⊗[A] K ⟶ K.
• HomologicalComplex.polynomialExtensionConst: the inclusion K ⟶ A[X] ⊗[A] K of constants.
• HomologicalComplex.polynomialExtensionMulXSubCHomotopyEquiv: the homotopy equivalence between the mapping cone of multiplication by X - C a and K.

References

• P. Ozsváth, A. Stipsicz, Z. Szabó, Grid Homology for Knots and Links, Section 5.2.

@[reducible, inline]

noncomputable abbrev HomologicalComplex.polynomialExtension {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) : HomologicalComplex (ModuleCat A) c

The polynomial extension A[X] ⊗[A] K of a complex K of A-modules: its terms are A[X] ⊗[A] K.X i and its differentials are A[X] ⊗ K.d i j.

Equations

• K.polynomialExtension = ((CategoryTheory.MonoidalCategory.tensorLeft ↧(Polynomial A)).mapHomologicalComplex c).obj K

noncomputable def HomologicalComplex.polynomialExtensionMul {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (p : Polynomial A) : K.polynomialExtension ⟶ K.polynomialExtension

Multiplication by a polynomial p : A[X] on the polynomial extension A[X] ⊗[A] K.

Equations

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

@[simp]

theorem HomologicalComplex.polynomialExtensionMul_f {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (p : Polynomial A) (i : ι) : (K.polynomialExtensionMul p).f i = CategoryTheory.MonoidalCategoryStruct.whiskerRight (ModuleCat.ofHom (LinearMap.mulLeft A p)) (K.X i)

Multiplication by p acts on A[X] ⊗ K.X i through the first factor.

@[simp]

theorem HomologicalComplex.polynomialExtensionMul_zero {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) : K.polynomialExtensionMul 0 = 0

Multiplication by the zero polynomial is the zero chain map.

@[simp]

theorem HomologicalComplex.polynomialExtensionMul_one {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) : K.polynomialExtensionMul 1 = CategoryTheory.CategoryStruct.id K.polynomialExtension

Multiplication by the constant polynomial 1 is the identity chain map.

@[simp]

theorem HomologicalComplex.polynomialExtensionMul_add {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (p q : Polynomial A) : K.polynomialExtensionMul (p + q) = K.polynomialExtensionMul p + K.polynomialExtensionMul q

Multiplication by a sum of polynomials is the sum of their multiplication chain maps.

@[simp]

theorem HomologicalComplex.polynomialExtensionMul_neg {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (p : Polynomial A) : K.polynomialExtensionMul (-p) = -K.polynomialExtensionMul p

Multiplication by the negative of a polynomial is the negative multiplication chain map.

@[simp]

theorem HomologicalComplex.polynomialExtensionMul_comp {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (p q : Polynomial A) : CategoryTheory.CategoryStruct.comp (K.polynomialExtensionMul p) (K.polynomialExtensionMul q) = K.polynomialExtensionMul (p * q)

Composing multiplication by two polynomials is multiplication by their product.

noncomputable def HomologicalComplex.polynomialExtensionEval {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (a : A) : K.polynomialExtension ⟶ K

Evaluation at a : A, as the chain map A[X] ⊗[A] K ⟶ K.

Equations

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

@[simp]

theorem HomologicalComplex.polynomialExtensionEval_f {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (a : A) (i : ι) : (K.polynomialExtensionEval a).f i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ModuleCat.ofHom (Polynomial.leval a)) (K.X i)) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (K.X i)).hom

Evaluation at a evaluates the first tensor factor of A[X] ⊗ K.X i.

noncomputable def HomologicalComplex.polynomialExtensionConst {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) : K ⟶ K.polynomialExtension

The inclusion of K into A[X] ⊗[A] K as the constant polynomials.

Equations

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

@[simp]

theorem HomologicalComplex.polynomialExtensionConst_f {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (i : ι) : K.polynomialExtensionConst.f i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (K.X i)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ModuleCat.ofHom (Algebra.linearMap A (Polynomial A))) (K.X i))

The inclusion of constants sends x : K.X i to 1 ⊗ x.

@[simp]

theorem HomologicalComplex.polynomialExtensionMul_X_sub_C_comp_polynomialExtensionEval {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (a : A) : CategoryTheory.CategoryStruct.comp (K.polynomialExtensionMul (Polynomial.X - Polynomial.C a)) (K.polynomialExtensionEval a) = 0

Evaluation at a kills the multiples of X - C a.

@[simp]

theorem HomologicalComplex.polynomialExtensionMul_X_sub_C_comp_polynomialExtensionEval_assoc {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (a : A) {Z : HomologicalComplex (ModuleCat A) c} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.polynomialExtensionMul (Polynomial.X - Polynomial.C a)) (CategoryTheory.CategoryStruct.comp (K.polynomialExtensionEval a) h) = CategoryTheory.CategoryStruct.comp 0 h

Evaluation at a kills the multiples of X - C a.

@[simp]

theorem HomologicalComplex.polynomialExtensionConst_comp_polynomialExtensionEval {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (a : A) : CategoryTheory.CategoryStruct.comp K.polynomialExtensionConst (K.polynomialExtensionEval a) = CategoryTheory.CategoryStruct.id K

A constant polynomial evaluates to itself.

@[simp]

theorem HomologicalComplex.polynomialExtensionConst_comp_polynomialExtensionEval_assoc {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) (a : A) {Z : HomologicalComplex (ModuleCat A) c} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp K.polynomialExtensionConst (CategoryTheory.CategoryStruct.comp (K.polynomialExtensionEval a) h) = h

A constant polynomial evaluates to itself.

noncomputable def HomologicalComplex.polynomialExtensionMulXSubCHomotopyEquiv {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) [DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (a : A) : HomotopyEquiv (homotopyCofiber (K.polynomialExtensionMul (Polynomial.X - Polynomial.C a))) K

The mapping cone of multiplication by X - C a on the polynomial extension A[X] ⊗[A] K is homotopy equivalent to K, provided every index of the complex shape is the target of a relation. The map from the cone is induced by evaluation at a, and its homotopy inverse is the inclusion of the constant polynomials.

Equations

• K.polynomialExtensionMulXSubCHomotopyEquiv hc a = (HomologicalComplex.evalShortComplexSplitting✝ K a).homotopyCofiberHomotopyEquiv hc

@[simp]

theorem HomologicalComplex.polynomialExtensionMulXSubCHomotopyEquiv_hom {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) [DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (a : A) : (K.polynomialExtensionMulXSubCHomotopyEquiv hc a).hom = homotopyCofiber.desc (K.polynomialExtensionMul (Polynomial.X - Polynomial.C a)) (K.polynomialExtensionEval a) (Homotopy.ofEq ⋯)

The map from the mapping cone in polynomialExtensionMulXSubCHomotopyEquiv is induced by evaluation at a.

@[simp]

theorem HomologicalComplex.polynomialExtensionMulXSubCHomotopyEquiv_inv {A : Type u} [CommRing A] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat A) c) [DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (a : A) : (K.polynomialExtensionMulXSubCHomotopyEquiv hc a).inv = CategoryTheory.CategoryStruct.comp K.polynomialExtensionConst (homotopyCofiber.inr (K.polynomialExtensionMul (Polynomial.X - Polynomial.C a)))

The homotopy inverse in polynomialExtensionMulXSubCHomotopyEquiv is the inclusion of the constant polynomials into the A[X] ⊗[A] K-summand of the mapping cone.