Parametrized cocycles and the chain homotopy between continuation maps #

A parametrized cocycle between two continuation cocycles ν₀ ν₁ : mP → mQ (the source's Definition 1.11) is a matrix h x y ∈ 𝒜 (indQ y - ind x - 1) with `d (h x y) = ν₁ x y - ν₀ x y + Σ_z (-1) ^ (ind x - ind z) • (mP x z * h z y)

Σ_z (-1) ^ (ind x - indQ z) • (h x z * mQ z y). It induces, for every differential graded right module (ℳ, dM), the map homotopyMap h ℳ : ℳ ⊗ ⟨P⟩ → ℳ ⊗ ⟨Q⟩, 𝔥 (α ⊗ x) = (-1) ^ |α| Σ_y (α · h x y) ⊗ y, which lowers the total degree by one and is a **chain homotopy** between the two continuation maps: Ψ¹ - Ψ⁰ = D⁻ ∘ 𝔥 + 𝔥 ∘ D⁺ (homotopyMap_twistedDifferential`). So homotopic continuation cocycles induce chain homotopic continuation maps.

As in TauCeti.Algebra.Homology.DG.Twisted.Continuation, the map is defined for any matrix, the theorems take the degree and parametrized equations as hypotheses, and the bundled ParametrizedCocycle comes last. The Koszul sign (-1) ^ |α| is the Koszul twist of parameter one of TauCeti.Algebra.Homology.DG.Twisted.Complex.

Main definitions #

TauCeti.homotopyMap h ℳ: the map (P → M) →ₗ[R] (Q → M) of a matrix h.
TauCeti.ParametrizedCocycle ν₀ ν₁: parametrized cocycles between continuation cocycles.

Main results #

TauCeti.homotopyMap_mem_twistedTotalGrading: the homotopy map lowers the total degree by one.
TauCeti.homotopyMap_twistedDifferential: the chain homotopy identity Ψ¹ - Ψ⁰ = D⁻ ∘ 𝔥 + 𝔥 ∘ D⁺ for a differential graded right module.

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.11.
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.

source

noncomputable def TauCeti.homotopyMap {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Semiring A] {P : Type uP} {Q : Type uQ} [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (h : P → Q → A) (ℳ : ℤ → Submodule R M) [DirectSum.Decomposition ℳ] :

(P → M) →ₗ[R] Q → M

The map ℳ ⊗ ⟨P⟩ → ℳ ⊗ ⟨Q⟩ of a matrix h : P → Q → A with the Koszul sign, on the models P → M and Q → M: its y-component is (𝔥 f) y = Σ_x op (h x y) • ε (f x), where ε is the Koszul twist of parameter one, so that on a homogeneous elementary tensor 𝔥 (α ⊗ x) = (-1) ^ |α| Σ_y (α · h x y) ⊗ y (homotopyMap_single).

Instances For

source

@[simp]

theorem TauCeti.homotopyMap_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Semiring A] {P : Type uP} {Q : Type uQ} [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (h : P → Q → A) {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (f : P → M) (y : Q) :

(homotopyMap h ℳ) f y = ∑ x : P, MulOpposite.op (h x y) • ((InternalGrading.ofDecomposition ℳ).koszulTwist 1) (f x)

source

theorem TauCeti.homotopyMap_single_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Semiring A] {P : Type uP} {Q : Type uQ} [Fintype P] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (h : P → Q → A) {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [DecidableEq P] (x : P) {q : ℤ} {α : M} (hα : α ∈ ℳ q) (y : Q) :

(homotopyMap h ℳ) (Pi.single x α) y = q.negOnePow • MulOpposite.op (h x y) • α

The y-component of the homotopy map of a homogeneous elementary tensor α ⊗ x, with α of degree q.

source

theorem TauCeti.homotopyMap_single {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Semiring A] {P : Type uP} {Q : Type uQ} [Fintype P] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] (h : P → Q → A) {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [Fintype Q] [DecidableEq P] [DecidableEq Q] (x : P) {q : ℤ} {α : M} (hα : α ∈ ℳ q) :

(homotopyMap h ℳ) (Pi.single x α) = ∑ y : Q, Pi.single y (q.negOnePow • MulOpposite.op (h x y) • α)

The homotopy map of a homogeneous elementary tensor: 𝔥 (α ⊗ x) = (-1) ^ |α| Σ_y (α · h x y) ⊗ y.

source

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

(homotopyMap h ℳ) f ∈ twistedTotalGrading ℳ indQ (n - 1)

The homotopy map of a matrix with homogeneous entries of degree indQ y - ind x - 1 lowers the total degree by one.

source

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

(continuationMap R M ν₁) f - (continuationMap R M ν₀) f = (twistedDifferential mQ ℳ dM) ((homotopyMap h ℳ) f) + (homotopyMap h ℳ) ((twistedDifferential mP ℳ dM) f)

The chain homotopy identity: for a matrix h with homogeneous entries which satisfies the parametrized equation between the continuation cocycles ν₀ and ν₁, and a differential graded right module (ℳ, dM), Ψ¹ - Ψ⁰ = D⁻ ∘ 𝔥 + 𝔥 ∘ D⁺.