Continuation cocycles and the chain maps they induce

A continuation cocycle from a twisting cocycle mP on (P, ind) to a twisting cocycle mQ on (Q, indQ), over a differential graded algebra (𝒜, d), is a matrix ν x y ∈ 𝒜 (indQ y - ind x) with d (ν x y) = Σ_z mP x z * ν z y + Σ_z (-1) ^ (ind x - indQ z - 1) • (ν x z * mQ z y) (the source's Definition 1.10, transcribed to the cohomological grading C^{-n} = C_n of TauCeti.Algebra.Homology.DG.Twisted.Cocycle). It induces, for every differential graded right module (ℳ, dM), the degree-zero map continuationMap ν : ℳ ⊗ ⟨P⟩ → ℳ ⊗ ⟨Q⟩, Ψ (α ⊗ x) = Σ_y (α · ν x y) ⊗ y, which preserves the total grading and commutes with the twisted differentials: this is the continuation map.

The Kronecker matrix is a continuation cocycle from m to itself, inducing the identity, and the matrix product of continuation cocycles m¹ → m² and m² → m³ is a continuation cocycle m¹ → m³, inducing the composite of the continuation maps.

As in TauCeti.Algebra.Homology.DG.Twisted.Complex, the map is defined for any matrix ν, the theorems take the degree and continuation equations as hypotheses, and the bundled ContinuationCocycle comes last.

Main definitions

• TauCeti.continuationMap R M ν: the map (P → M) →ₗ[R] (Q → M) of a matrix ν.
• TauCeti.ContinuationCocycle mP mQ: continuation cocycles between twisting cocycles, with refl and comp.

Main results

• TauCeti.continuationMap_mem_twistedTotalGrading: the continuation map has total degree zero.
• TauCeti.continuationMap_twistedDifferential: the continuation map is a chain map, Ψ ∘ D_P = D_Q ∘ Ψ, for a differential graded right module.
• TauCeti.continuationMap_kronecker, TauCeti.continuationMap_matMul: the Kronecker matrix induces the identity and the matrix product induces the composite.
• TauCeti.continuation_kronecker, TauCeti.continuation_matMul: the Kronecker matrix and the matrix product satisfy the continuation equation.

References

• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, §1.4, Definition 1.10.
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Morse homology with differential graded coefficients, Progress in Mathematics 360, Birkhäuser, 2025, Chapters 3–4.

noncomputable def TauCeti.continuationMap (R : Type uR) {A : Type uA} (M : Type uM) [CommSemiring R] [Semiring A] {P : Type uP} {Q : Type uQ} [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (ν : P → Q → A) : (P → M) →ₗ[R] Q → M

The map ℳ ⊗ ⟨P⟩ → ℳ ⊗ ⟨Q⟩ of a matrix ν : P → Q → A, on the models P → M and Q → M: its y-component is (Ψ f) y = Σ_x op (ν x y) • f x, so that on an elementary tensor Ψ (α ⊗ x) = Σ_y (α · ν x y) ⊗ y (continuationMap_single), with no Koszul sign.

theorem TauCeti.continuationMap_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommSemiring R] [Semiring A] {P : Type uP} {Q : Type uQ} [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (ν : P → Q → A) (f : P → M) (y : Q) : (continuationMap R M ν) f y = ∑ x : P, MulOpposite.op (ν x y) • f x

The y-component of the continuation map; not @[simp], so that the elementary-tensor normal form continuationMap_single_apply is reached first.

theorem TauCeti.continuationMap_add {R : Type uR} {A : Type uA} {M : Type uM} [CommSemiring R] [Semiring A] {P : Type uP} {Q : Type uQ} [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (F G : Matrix P Q A) : continuationMap R M (F + G) = continuationMap R M F + continuationMap R M G

The continuation map is additive in the matrix.

@[simp]

theorem TauCeti.continuationMap_zero (R : Type uR) {A : Type uA} (M : Type uM) [CommSemiring R] [Semiring A] (P : Type uP) (Q : Type uQ) [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] : continuationMap R M 0 = 0

The zero matrix induces the zero map.

@[simp]

theorem TauCeti.continuationMap_single_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommSemiring R] [Semiring A] {P : Type uP} {Q : Type uQ} [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (ν : P → Q → A) [DecidableEq P] (x : P) (α : M) (y : Q) : (continuationMap R M ν) (Pi.single x α) y = MulOpposite.op (ν x y) • α

The y-component of the continuation map of an elementary tensor α ⊗ x.

theorem TauCeti.continuationMap_single {R : Type uR} {A : Type uA} {M : Type uM} [CommSemiring R] [Semiring A] {P : Type uP} {Q : Type uQ} [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (ν : P → Q → A) [Fintype Q] [DecidableEq P] [DecidableEq Q] (x : P) (α : M) : (continuationMap R M ν) (Pi.single x α) = ∑ y : Q, Pi.single y (MulOpposite.op (ν x y) • α)

The continuation map of an elementary tensor: Ψ (α ⊗ x) = Σ_y (α · ν x y) ⊗ y.

The maps of the Kronecker matrix and of a matrix product

@[simp]

theorem TauCeti.continuationMap_kronecker {R : Type uR} {A : Type uA} {M : Type uM} [CommSemiring R] [Semiring A] {P : Type uP} [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [DecidableEq P] : continuationMap R M 1 = LinearMap.id

The Kronecker matrix induces the identity.

theorem TauCeti.continuationMap_matMul {R : Type uR} {A : Type uA} {M : Type uM} [CommSemiring R] [Semiring A] {P : Type uP} {Q : Type uQ} {S : Type uS} [Fintype P] [Fintype Q] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (F : Matrix P Q A) (G : Matrix Q S A) : continuationMap R M (F * G) = continuationMap R M G ∘ₗ continuationMap R M F

The matrix product induces the composite of the continuation maps.

theorem TauCeti.continuationMap_mem_twistedIndexFiltration {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] (ν : P → Q → A) [CommSemiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (hν : ∀ (x : P) (y : Q), ind x < indQ y → ν x y = 0) {p : ℤ} {f : P → M} (hf : f ∈ twistedIndexFiltration ind p) : (continuationMap R M ν) f ∈ twistedIndexFiltration indQ p

The continuation map of a matrix with no entries strictly increasing the index preserves the index filtration.

theorem TauCeti.continuationMap_mem_twistedTotalGrading {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] (ν : P → Q → A) [CommSemiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {ℳ : ℤ → Submodule R M} [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (hν : ∀ (x : P) (y : Q), ν x y ∈ 𝒜 (indQ y - ind x)) {n : ℤ} {f : P → M} (hf : f ∈ twistedTotalGrading ℳ ind n) : (continuationMap R M ν) f ∈ twistedTotalGrading ℳ indQ n

The continuation map of a matrix with homogeneous entries of degree indQ y - ind x preserves the total degree.

theorem TauCeti.continuationMap_twistedDifferential {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] (ν : P → Q → A) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype Q] [IsScalarTower R Aᵐᵒᵖ M] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} (mP : P → P → A) (mQ : Q → Q → A) (dM : M →ₗ[R] M) (hν : ∀ (x : P) (y : Q), ν x y ∈ 𝒜 (indQ y - ind x)) (hc : ∀ (x : P) (y : Q), d (ν x y) = ∑ z : P, mP x z * ν z y + ∑ z : Q, (ind x - indQ z - 1).negOnePow • (ν x z * mQ z y)) (hM : IsDGRightModule h ℳ dM) (f : P → M) : (continuationMap R M ν) ((twistedDifferential mP ℳ dM) f) = (twistedDifferential mQ ℳ dM) ((continuationMap R M ν) f)

The continuation map is a chain map: for a matrix ν with homogeneous entries which satisfies the continuation equation between mP and mQ, and a differential graded right module (ℳ, dM), Ψ ∘ D_P = D_Q ∘ Ψ.

The Kronecker matrix and the matrix product

theorem TauCeti.kronecker_mem_graded {R : Type uR} {A : Type uA} {P : Type uP} {ind : P → ℤ} [DecidableEq P] [CommSemiring R] [Semiring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] (x y : P) : 1 x y ∈ 𝒜 (ind y - ind x)

The Kronecker matrix has entries of degree ind y - ind x.

theorem TauCeti.continuation_kronecker {R : Type uR} {A : Type uA} {P : Type uP} {ind : P → ℤ} [DecidableEq P] [CommRing R] [Ring A] [Algebra R A] [Fintype P] {d : A →ₗ[R] A} (m : P → P → A) (hd : d 1 = 0) (x y : P) : d (1 x y) = ∑ z : P, m x z * 1 z y + ∑ z : P, (ind x - ind z - 1).negOnePow • (1 x z * m z y)

The Kronecker matrix satisfies the continuation equation from m to m, for any matrix m, as soon as d 1 = 0.

theorem TauCeti.matMul_mem_graded {R : Type uR} {A : Type uA} {P : Type uP} {Q : Type uQ} {S : Type uS} {ind : P → ℤ} {indQ : Q → ℤ} {indS : S → ℤ} [Fintype Q] (ν₁ : P → Q → A) (ν₂ : Q → S → A) [CommSemiring R] [Semiring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] (hν₁ : ∀ (x : P) (y : Q), ν₁ x y ∈ 𝒜 (indQ y - ind x)) (hν₂ : ∀ (y : Q) (z : S), ν₂ y z ∈ 𝒜 (indS z - indQ y)) (x : P) (z : S) : (Matrix.of ν₁ * Matrix.of ν₂) x z ∈ 𝒜 (indS z - ind x)

The matrix product of matrices with entries of degrees indQ y - ind x and indS z - indQ y has entries of degree indS z - ind x.

theorem TauCeti.continuation_matMul {R : Type uR} {A : Type uA} {P : Type uP} {Q : Type uQ} {S : Type uS} {ind : P → ℤ} {indQ : Q → ℤ} {indS : S → ℤ} [Fintype Q] (ν₁ : P → Q → A) (ν₂ : Q → S → A) [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] [Fintype P] [Fintype S] {d : A →ₗ[R] A} (h : IsDGAlgebra 𝒜 d) (m₁ : P → P → A) (m₂ : Q → Q → A) (m₃ : S → S → A) (hν₁ : ∀ (x : P) (y : Q), ν₁ x y ∈ 𝒜 (indQ y - ind x)) (hc₁ : ∀ (x : P) (y : Q), d (ν₁ x y) = ∑ z : P, m₁ x z * ν₁ z y + ∑ z : Q, (ind x - indQ z - 1).negOnePow • (ν₁ x z * m₂ z y)) (hc₂ : ∀ (y : Q) (w : S), d (ν₂ y w) = ∑ z : Q, m₂ y z * ν₂ z w + ∑ z : S, (indQ y - indS z - 1).negOnePow • (ν₂ y z * m₃ z w)) (x : P) (y : S) : d ((Matrix.of ν₁ * Matrix.of ν₂) x y) = ∑ w : P, m₁ x w * (Matrix.of ν₁ * Matrix.of ν₂) w y + ∑ w : S, (ind x - indS w - 1).negOnePow • ((Matrix.of ν₁ * Matrix.of ν₂) x w * m₃ w y)

The matrix product of continuation cocycles m₁ → m₂ and m₂ → m₃ satisfies the continuation equation from m₁ to m₃.

Continuation cocycles

structure TauCeti.ContinuationCocycle {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] [Fintype Q] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} (mP : TwistingCocycle 𝒜 d P ind) (mQ : TwistingCocycle 𝒜 d Q indQ) : Type (max (max uA uP) uQ)

A continuation cocycle from the twisting cocycle mP on (P, ind) to the twisting cocycle mQ on (Q, indQ) (the source's Definition 1.10): a matrix ν x y ∈ 𝒜 (indQ y - ind x) with d (ν x y) = Σ_z mP x z * ν z y + Σ_z (-1) ^ (ind x - indQ z - 1) • (ν x z * mQ z y).

• ν : P → Q → A

  The entries of the continuation cocycle.

• mem_graded (x : P) (y : Q) : self.ν x y ∈ 𝒜 (indQ y - ind x)

  The entry ν x y has cohomological degree indQ y - ind x.

• continuation (x : P) (y : Q) : d (self.ν x y) = ∑ z : P, mP.m x z * self.ν z y + ∑ z : Q, (ind x - indQ z - 1).negOnePow • (self.ν x z * mQ.m z y)

  The continuation equation.

theorem TauCeti.ContinuationCocycle.ext {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] [Fintype Q] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} {ν₁ ν₂ : ContinuationCocycle mP mQ} (h : ∀ (x : P) (y : Q), ν₁.ν x y = ν₂.ν x y) : ν₁ = ν₂

theorem TauCeti.ContinuationCocycle.ext_iff {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] [Fintype Q] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} {ν₁ ν₂ : ContinuationCocycle mP mQ} : ν₁ = ν₂ ↔ ∀ (x : P) (y : Q), ν₁.ν x y = ν₂.ν x y

theorem TauCeti.ContinuationCocycle.ν_eq_zero_of_lt_of_nonpos {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] [Fintype Q] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} (ν : ContinuationCocycle mP mQ) (h𝒜 : ∀ (n : ℤ), 0 < n → 𝒜 n = ⊥) {x : P} {y : Q} (hxy : ind x < indQ y) : ν.ν x y = 0

Over an algebra concentrated in cohomological degrees ≤ 0, a continuation cocycle has no entries strictly increasing the index: ν x y has degree indQ y - ind x.

def TauCeti.ContinuationCocycle.refl {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {ind : P → ℤ} [Fintype P] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} [GradedAlgebra 𝒜] [DecidableEq P] (hd : d 1 = 0) (m : TwistingCocycle 𝒜 d P ind) : ContinuationCocycle m m

The Kronecker matrix, as a continuation cocycle from m to itself, for a differential with d 1 = 0.

@[simp]

theorem TauCeti.ContinuationCocycle.refl_ν {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {ind : P → ℤ} [Fintype P] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} [GradedAlgebra 𝒜] [DecidableEq P] (hd : d 1 = 0) (m : TwistingCocycle 𝒜 d P ind) : (refl hd m).ν = 1

def TauCeti.ContinuationCocycle.comp {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {S : Type uS} {ind : P → ℤ} {indQ : Q → ℤ} {indS : S → ℤ} [Fintype P] [Fintype Q] [Fintype S] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} {mS : TwistingCocycle 𝒜 d S indS} [GradedAlgebra 𝒜] (h : IsDGAlgebra 𝒜 d) (ν₁ : ContinuationCocycle mP mQ) (ν₂ : ContinuationCocycle mQ mS) : ContinuationCocycle mP mS

The matrix product of continuation cocycles mP → mQ and mQ → mS, a continuation cocycle mP → mS.

@[simp]

theorem TauCeti.ContinuationCocycle.comp_ν {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {S : Type uS} {ind : P → ℤ} {indQ : Q → ℤ} {indS : S → ℤ} [Fintype P] [Fintype Q] [Fintype S] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} {mS : TwistingCocycle 𝒜 d S indS} [GradedAlgebra 𝒜] (h : IsDGAlgebra 𝒜 d) (ν₁ : ContinuationCocycle mP mQ) (ν₂ : ContinuationCocycle mQ mS) : (comp h ν₁ ν₂).ν = Matrix.of ν₁.ν * Matrix.of ν₂.ν

@[simp]

theorem TauCeti.ContinuationCocycle.refl_comp {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] [Fintype Q] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} [GradedAlgebra 𝒜] [DecidableEq P] (h : IsDGAlgebra 𝒜 d) (ν : ContinuationCocycle mP mQ) : comp h (refl ⋯ mP) ν = ν

The Kronecker continuation cocycle is a left identity for the composition.

@[simp]

theorem TauCeti.ContinuationCocycle.comp_refl {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] [Fintype Q] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} [GradedAlgebra 𝒜] [DecidableEq Q] (h : IsDGAlgebra 𝒜 d) (ν : ContinuationCocycle mP mQ) : comp h ν (refl ⋯ mQ) = ν

The Kronecker continuation cocycle is a right identity for the composition.

theorem TauCeti.ContinuationCocycle.comp_assoc {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {S : Type uS} {ind : P → ℤ} {indQ : Q → ℤ} {indS : S → ℤ} [Fintype P] [Fintype Q] [Fintype S] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} {mS : TwistingCocycle 𝒜 d S indS} [GradedAlgebra 𝒜] {T : Type uT} {indT : T → ℤ} [Fintype T] {mT : TwistingCocycle 𝒜 d T indT} (h : IsDGAlgebra 𝒜 d) (ν₁ : ContinuationCocycle mP mQ) (ν₂ : ContinuationCocycle mQ mS) (ν₃ : ContinuationCocycle mS mT) : comp h (comp h ν₁ ν₂) ν₃ = comp h ν₁ (comp h ν₂ ν₃)

The composition of continuation cocycles is associative.

theorem TauCeti.ContinuationCocycle.refl_ν_eq_zero_of_lt {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {ind : P → ℤ} [Fintype P] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} [GradedAlgebra 𝒜] [DecidableEq P] (hd : d 1 = 0) (m : TwistingCocycle 𝒜 d P ind) {x y : P} (hxy : ind x < ind y) : (refl hd m).ν x y = 0

The Kronecker continuation cocycle has no entries strictly increasing the index.

theorem TauCeti.ContinuationCocycle.comp_ν_eq_zero_of_lt {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {S : Type uS} {ind : P → ℤ} {indQ : Q → ℤ} {indS : S → ℤ} [Fintype P] [Fintype Q] [Fintype S] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} {mS : TwistingCocycle 𝒜 d S indS} [GradedAlgebra 𝒜] (h : IsDGAlgebra 𝒜 d) (ν₁ : ContinuationCocycle mP mQ) (ν₂ : ContinuationCocycle mQ mS) (hν₁ : ∀ (x : P) (y : Q), ind x < indQ y → ν₁.ν x y = 0) (hν₂ : ∀ (x : Q) (y : S), indQ x < indS y → ν₂.ν x y = 0) {x : P} {y : S} (hxy : ind x < indS y) : (comp h ν₁ ν₂).ν x y = 0

A composite of continuation cocycles with no entries strictly increasing the index has no such entries.

theorem TauCeti.ContinuationCocycle.continuationMap_refl {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {ind : P → ℤ} [Fintype P] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} [GradedAlgebra 𝒜] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [DecidableEq P] (hd : d 1 = 0) (m : TwistingCocycle 𝒜 d P ind) : continuationMap R M (refl hd m).ν = LinearMap.id

The Kronecker continuation cocycle induces the identity.

theorem TauCeti.ContinuationCocycle.continuationMap_comp {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {S : Type uS} {ind : P → ℤ} {indQ : Q → ℤ} {indS : S → ℤ} [Fintype P] [Fintype Q] [Fintype S] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} {mS : TwistingCocycle 𝒜 d S indS} [GradedAlgebra 𝒜] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (h : IsDGAlgebra 𝒜 d) (ν₁ : ContinuationCocycle mP mQ) (ν₂ : ContinuationCocycle mQ mS) : continuationMap R M (comp h ν₁ ν₂).ν = continuationMap R M ν₂.ν ∘ₗ continuationMap R M ν₁.ν

The composite continuation cocycle induces the composite of the continuation maps.

theorem TauCeti.ContinuationCocycle.continuationMap_mem_twistedTotalGrading {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] [Fintype Q] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} [GradedAlgebra 𝒜] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] {ℳ : ℤ → Submodule R M} [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (ν : ContinuationCocycle mP mQ) {n : ℤ} {f : P → M} (hf : f ∈ twistedTotalGrading ℳ ind n) : (continuationMap R M ν.ν) f ∈ twistedTotalGrading ℳ indQ n

The continuation map of a continuation cocycle preserves the total degree.

theorem TauCeti.ContinuationCocycle.continuationMap_twistedDifferential {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] {P : Type uP} {Q : Type uQ} {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] [Fintype Q] {𝒜 : ℤ → Submodule R A} {d : A →ₗ[R] A} {mP : TwistingCocycle 𝒜 d P ind} {mQ : TwistingCocycle 𝒜 d Q indQ} [GradedAlgebra 𝒜] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] {dM : M →ₗ[R] M} {h : IsDGAlgebra 𝒜 d} (ν : ContinuationCocycle mP mQ) (hM : IsDGRightModule h ℳ dM) (f : P → M) : (continuationMap R M ν.ν) ((twistedDifferential mP.m ℳ dM) f) = (twistedDifferential mQ.m ℳ dM) ((continuationMap R M ν.ν) f)

The continuation map of a continuation cocycle is a chain map between the twisted complexes of a differential graded right module.