The index filtration of a twisted complex

The index filtration F_p consists of functions supported on generators of index at most p. For a finite generator set it is bounded below, exhaustive, and increasing. One-sidedness of the cocycle ensures that the twisted differential preserves it: the coefficient differential keeps the generator index, and every twisting term strictly lowers it.

Intersecting F_p with the total grading gives an actual cochain complex, with inclusion maps between its stages. The quotient F_p / F_{p-1} is identified with the copies of the coefficient module indexed by generators of index exactly p. Under this identification its induced differential acts coordinatewise by the coefficient differential. These are the filtered-complex and associated-graded inputs to the spectral sequence of a twisted complex. Restriction to the generators of a fixed index gives a short exact sequence of the filtration stages and the zero-cocycle complex, with the restriction map as cokernel of the stage inclusion.

References

• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, Definition 3.38.
• 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.

def TauCeti.twistedIndexFiltration {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] (ind : P → ℤ) (p : ℤ) : Submodule R (P → M)

The stage of the index filtration supported on generators of index at most p.

@[simp]

theorem TauCeti.mem_twistedIndexFiltration_iff {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] (ind : P → ℤ) {p : ℤ} {f : P → M} : f ∈ twistedIndexFiltration ind p ↔ ∀ (x : P), p < ind x → f x = 0

theorem TauCeti.twistedIndexFiltration_mono {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] (ind : P → ℤ) : Monotone (twistedIndexFiltration ind)

The index filtration is increasing.

theorem TauCeti.twistedIndexFiltration_eq_top {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] (ind : P → ℤ) {p : ℤ} (hp : ∀ (x : P), ind x ≤ p) : twistedIndexFiltration ind p = ⊤

Above every generator index the filtration stage is all of P → M.

theorem TauCeti.twistedIndexFiltration_eq_bot {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] (ind : P → ℤ) {p : ℤ} (hp : ∀ (x : P), p < ind x) : twistedIndexFiltration ind p = ⊥

Below every generator index the filtration vanishes.

theorem TauCeti.twistedIndexFiltration_bounded {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] (ind : P → ℤ) [Finite P] : ∃ (a : ℤ) (b : ℤ), twistedIndexFiltration ind a = ⊥ ∧ twistedIndexFiltration ind b = ⊤

A finite index filtration is bounded, including when there are no generators.

theorem TauCeti.iSup_twistedIndexFiltration_eq_top {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] (ind : P → ℤ) [Finite P] : ⨆ (p : ℤ), twistedIndexFiltration ind p = ⊤

Every element lies in some stage of a finite index filtration.

def TauCeti.twistedIndexGrading {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ℤ → Submodule R M) (ind : P → ℤ) (p n : ℤ) : Submodule R (P → M)

The degree-n part of F_p, in the total grading of the twisted complex.

@[simp]

theorem TauCeti.mem_twistedIndexGrading_iff {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] {ℳ : ℤ → Submodule R M} {ind : P → ℤ} {p n : ℤ} {f : P → M} : f ∈ twistedIndexGrading ℳ ind p n ↔ (∀ (x : P), p < ind x → f x = 0) ∧ ∀ (x : P), f x ∈ ℳ (n + ind x)

theorem TauCeti.twistedIndexGrading_mono {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] {ℳ : ℤ → Submodule R M} {ind : P → ℤ} {p q n : ℤ} (hpq : p ≤ q) : twistedIndexGrading ℳ ind p n ≤ twistedIndexGrading ℳ ind q n

The index filtration on each total degree is increasing.

theorem TauCeti.twistedIndexGrading_le_twistedTotalGrading {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] {ℳ : ℤ → Submodule R M} {ind : P → ℤ} (p n : ℤ) : twistedIndexGrading ℳ ind p n ≤ twistedTotalGrading ℳ ind n

A homogeneous filtration stage is contained in the corresponding total-degree piece.

noncomputable def TauCeti.indexExtend (R : Type uR) (M : Type uM) {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] (ind : P → ℤ) (p : ℤ) : ({ x : P // ind x = p } → M) →ₗ[R] P → M

The extension by zero of a family indexed by the generators of index p to all generators.

@[simp]

theorem TauCeti.indexExtend_apply_of_eq {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] {ind : P → ℤ} {p : ℤ} (f : { x : P // ind x = p } → M) {x : P} (hx : ind x = p) : (indexExtend R M ind p) f x = f ⟨x, hx⟩

The extension by zero takes the given value at a generator of index p.

@[simp]

theorem TauCeti.indexExtend_apply_of_ne {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] {ind : P → ℤ} {p : ℤ} (f : { x : P // ind x = p } → M) {x : P} (hx : ind x ≠ p) : (indexExtend R M ind p) f x = 0

The extension by zero vanishes at a generator of index different from p.

@[simp]

theorem TauCeti.funLeft_indexExtend {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] {ind : P → ℤ} {p : ℤ} (f : { x : P // ind x = p } → M) : (LinearMap.funLeft R M Subtype.val) ((indexExtend R M ind p) f) = f

Restricting a family extended by zero recovers the family.

theorem TauCeti.indexExtend_mem_twistedIndexFiltration {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] {ind : P → ℤ} {p : ℤ} (f : { x : P // ind x = p } → M) : (indexExtend R M ind p) f ∈ twistedIndexFiltration ind p

A family extended by zero from the generators of index p lies in the p-th piece of the index filtration.

theorem TauCeti.indexExtend_mem_twistedTotalGrading {R : Type uR} {M : Type uM} {P : Type uP} [Semiring R] [AddCommMonoid M] [Module R M] {ind : P → ℤ} {p : ℤ} {ℳ : ℤ → Submodule R M} {n : ℤ} {f : { x : P // ind x = p } → M} (hf : f ∈ twistedTotalGrading ℳ (fun (x : { x : P // ind x = p }) => ind ↑x) n) : (indexExtend R M ind p) f ∈ twistedTotalGrading ℳ ind n

A family of total degree n on the generators of index p, extended by zero, has total degree n.

theorem TauCeti.twistingSum_eq_zero_of_mem_twistedIndexFiltration {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Semiring A] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [Fintype P] {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (m : P → P → A) (hm : ∀ (x y : P), ind x ≤ ind y → m x y = 0) {p : ℤ} {f : P → M} (hf : f ∈ twistedIndexFiltration ind p) {y : P} (hy : p ≤ ind y) : ∑ x : P, MulOpposite.op (m x y) • ((InternalGrading.ofDecomposition ℳ).koszulTwist 1) (f x) = 0

Every twisting contribution from F_p vanishes at a generator of index at least p.

theorem TauCeti.twistedDifferential_mem_twistedIndexFiltration {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Semiring A] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (m : P → P → A) (hm : ∀ (x y : P), ind x ≤ ind y → m x y = 0) (dM : M →ₗ[R] M) {p : ℤ} {f : P → M} (hf : f ∈ twistedIndexFiltration ind p) : (twistedDifferential m ℳ dM) f ∈ twistedIndexFiltration ind p

One-sidedness makes the twisted differential preserve every index-filtration stage.

theorem TauCeti.twistedDifferential_apply_of_mem_twistedIndexFiltration {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Semiring A] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (m : P → P → A) (hm : ∀ (x y : P), ind x ≤ ind y → m x y = 0) (dM : M →ₗ[R] M) {p : ℤ} {f : P → M} (hf : f ∈ twistedIndexFiltration ind p) {y : P} (hy : ind y = p) : (twistedDifferential m ℳ dM) f y = dM (f y)

At index p, the differential of an element of F_p is its coefficient differential. Every twisting contribution has strictly smaller generator index.

theorem TauCeti.twistedDifferential_funLeft_val {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Semiring A] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (m : P → P → A) (hm : ∀ (x y : P), ind x ≤ ind y → m x y = 0) (dM : M →ₗ[R] M) {p : ℤ} {f : P → M} (hf : ∀ (x : P), p < ind x → f x = 0) : (twistedDifferential 0 ℳ dM) ((LinearMap.funLeft R M Subtype.val) f) = (LinearMap.funLeft R M Subtype.val) ((twistedDifferential m ℳ dM) f)

Restriction to generators of index p intertwines the differential on F_p with the coefficient differential, which is the twisted differential of the zero cocycle.

def TauCeti.twistedIndexLower {R : Type uR} {M : Type uM} {P : Type uP} [Ring R] [AddCommGroup M] [Module R M] (ind : P → ℤ) (p : ℤ) : Submodule R ↥(twistedIndexFiltration ind p)

The preceding filtration stage as a submodule of F_p.

@[simp]

theorem TauCeti.mem_twistedIndexLower_iff {R : Type uR} {M : Type uM} {P : Type uP} [Ring R] [AddCommGroup M] [Module R M] (ind : P → ℤ) (p : ℤ) {f : ↥(twistedIndexFiltration ind p)} : f ∈ twistedIndexLower ind p ↔ ∀ (x : P), p - 1 < ind x → ↑f x = 0

def TauCeti.twistedIndexProjection {R : Type uR} {M : Type uM} {P : Type uP} [Ring R] [AddCommGroup M] [Module R M] (ind : P → ℤ) (p : ℤ) : ↥(twistedIndexFiltration ind p) →ₗ[R] { x : P // ind x = p } → M

Projection from F_p to the generators of index exactly p.

@[simp]

theorem TauCeti.twistedIndexProjection_apply {R : Type uR} {M : Type uM} {P : Type uP} [Ring R] [AddCommGroup M] [Module R M] (ind : P → ℤ) (p : ℤ) (f : ↥(twistedIndexFiltration ind p)) (x : { x : P // ind x = p }) : (twistedIndexProjection ind p) f x = ↑f ↑x

theorem TauCeti.ker_twistedIndexProjection {R : Type uR} {M : Type uM} {P : Type uP} [Ring R] [AddCommGroup M] [Module R M] (ind : P → ℤ) (p : ℤ) : (twistedIndexProjection ind p).ker = twistedIndexLower ind p

The kernel of projection to index p is exactly F_{p-1} inside F_p.

theorem TauCeti.twistedIndexProjection_surjective {R : Type uR} {M : Type uM} {P : Type uP} [Ring R] [AddCommGroup M] [Module R M] (ind : P → ℤ) (p : ℤ) : Function.Surjective ⇑(twistedIndexProjection ind p)

Every family on the generators of index p is the projection of an element of F_p.

noncomputable def TauCeti.twistedIndexGradedEquiv {R : Type uR} {M : Type uM} {P : Type uP} [Ring R] [AddCommGroup M] [Module R M] (ind : P → ℤ) (p : ℤ) : (↥(twistedIndexFiltration ind p) ⧸ twistedIndexLower ind p) ≃ₗ[R] { x : P // ind x = p } → M

The associated graded module F_p / F_{p-1} is the family of coefficient modules on exactly the generators of index p.

@[simp]

theorem TauCeti.twistedIndexGradedEquiv_mk {R : Type uR} {M : Type uM} {P : Type uP} [Ring R] [AddCommGroup M] [Module R M] (ind : P → ℤ) (p : ℤ) (f : ↥(twistedIndexFiltration ind p)) (x : { x : P // ind x = p }) : (twistedIndexGradedEquiv ind p) (Submodule.Quotient.mk f) x = ↑f ↑x

noncomputable def TauCeti.twistedIndexDifferential {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Semiring A] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (m : P → P → A) (hm : ∀ (x y : P), ind x ≤ ind y → m x y = 0) (dM : M →ₗ[R] M) (p : ℤ) : ↥(twistedIndexFiltration ind p) →ₗ[R] ↥(twistedIndexFiltration ind p)

The restriction of the twisted differential to F_p.

@[simp]

theorem TauCeti.twistedIndexDifferential_apply {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Semiring A] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (m : P → P → A) (hm : ∀ (x y : P), ind x ≤ ind y → m x y = 0) (dM : M →ₗ[R] M) (p : ℤ) (f : ↥(twistedIndexFiltration ind p)) : ↑((twistedIndexDifferential m hm dM p) f) = (twistedDifferential m ℳ dM) ↑f

noncomputable def TauCeti.twistedIndexGradedDifferential {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Semiring A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (m : P → P → A) (hm : ∀ (x y : P), ind x ≤ ind y → m x y = 0) (dM : M →ₗ[R] M) (p : ℤ) : ↥(twistedIndexFiltration ind p) ⧸ twistedIndexLower ind p →ₗ[R] ↥(twistedIndexFiltration ind p) ⧸ twistedIndexLower ind p

The differential induced on F_p / F_{p-1} by the twisted differential.

@[simp]

theorem TauCeti.twistedIndexGradedDifferential_mk {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Semiring A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (m : P → P → A) (hm : ∀ (x y : P), ind x ≤ ind y → m x y = 0) (dM : M →ₗ[R] M) (p : ℤ) (f : ↥(twistedIndexFiltration ind p)) : (twistedIndexGradedDifferential m hm dM p) (Submodule.Quotient.mk f) = Submodule.Quotient.mk ((twistedIndexDifferential m hm dM p) f)

The quotient differential sends the class of f to the class of its twisted differential.

@[simp]

theorem TauCeti.twistedIndexGradedEquiv_d {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Semiring A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (m : P → P → A) (hm : ∀ (x y : P), ind x ≤ ind y → m x y = 0) (dM : M →ₗ[R] M) (p : ℤ) (f : ↥(twistedIndexFiltration ind p) ⧸ twistedIndexLower ind p) (x : { x : P // ind x = p }) : (twistedIndexGradedEquiv ind p) ((twistedIndexGradedDifferential m hm dM p) f) x = dM ((twistedIndexGradedEquiv ind p) f x)

Under the associated graded equivalence, the induced differential is the coefficient differential on each generator of index exactly p.

theorem TauCeti.twistedIndexGradedDifferential_sq_zero {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Semiring A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] (m : P → P → A) (hm : ∀ (x y : P), ind x ≤ ind y → m x y = 0) (dM : M →ₗ[R] M) (p : ℤ) (hdM : ∀ (x : M), dM (dM x) = 0) (f : ↥(twistedIndexFiltration ind p) ⧸ twistedIndexLower ind p) : (twistedIndexGradedDifferential m hm dM p) ((twistedIndexGradedDifferential m hm dM p) f) = 0

The induced associated graded differential squares to zero whenever the coefficient differential does.

theorem TauCeti.TwistingCocycle.twistedDifferential_mem_twistedIndexGrading {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hdM : LinearMap.IsHomogeneous dM ℳ ℳ 1) {p n : ℤ} {f : P → M} (hf : f ∈ twistedIndexGrading ℳ ind p n) : (twistedDifferential m.m ℳ dM) f ∈ twistedIndexGrading ℳ ind p (n + 1)

The twisted differential carries the degree-n part of F_p into degree n+1 in F_p.

noncomputable def TauCeti.TwistingCocycle.twistedIndexCochainComplex {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p : ℤ) : CochainComplex (ModuleCat R) ℤ

The pth stage of the index filtration as a cochain complex of modules.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexCochainComplex_X {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p n : ℤ) : (m.twistedIndexCochainComplex hM p).X n = ↧↥(twistedIndexGrading ℳ ind p n)

The degree terms of the filtered complex are the intersections of filtration and grading.

noncomputable def TauCeti.TwistingCocycle.twistedIndexCochainComplexXEquiv {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p n : ℤ) : ↑((m.twistedIndexCochainComplex hM p).X n) ≃ₗ[R] ↥(twistedIndexGrading ℳ ind p n)

Identify a term of the filtered complex with the intersection of index and total degree.

theorem TauCeti.TwistingCocycle.twistedIndexCochainComplexXEquiv_d {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p n : ℤ) (f : ↑((m.twistedIndexCochainComplex hM p).X n)) : ↑((m.twistedIndexCochainComplexXEquiv hM p (n + 1)) ((ModuleCat.Hom.hom ((m.twistedIndexCochainComplex hM p).d n (n + 1))) f)) = (twistedDifferential m.m ℳ dM) ↑((m.twistedIndexCochainComplexXEquiv hM p n) f)

The filtered cochain differential acts by the ambient twisted differential.

noncomputable def TauCeti.TwistingCocycle.twistedIndexCochainComplexMap {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) {p q : ℤ} (hpq : p ≤ q) : m.twistedIndexCochainComplex hM p ⟶ m.twistedIndexCochainComplex hM q

The canonical cochain inclusion of a filtration stage into a later stage.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexCochainComplexMap_apply {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) {p q : ℤ} (hpq : p ≤ q) (n : ℤ) (f : ↑((m.twistedIndexCochainComplex hM p).X n)) : ↑((m.twistedIndexCochainComplexXEquiv hM q n) ((ModuleCat.Hom.hom ((m.twistedIndexCochainComplexMap hM hpq).f n)) f)) = ↑((m.twistedIndexCochainComplexXEquiv hM p n) f)

The transition map is inclusion on the underlying homogeneous functions.

theorem TauCeti.TwistingCocycle.injective_twistedIndexCochainComplexMap_f {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) {p q : ℤ} (hpq : p ≤ q) (n : ℤ) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((m.twistedIndexCochainComplexMap hM hpq).f n))

The inclusion F_p ⟶ F_q is injective in each degree.

noncomputable def TauCeti.TwistingCocycle.twistedIndexCochainComplexι {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p : ℤ) : m.twistedIndexCochainComplex hM p ⟶ m.twistedCochainComplex dM hM

The canonical inclusion of an index-filtration stage into the twisted complex.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexCochainComplexι_apply {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p n : ℤ) (f : ↑((m.twistedIndexCochainComplex hM p).X n)) : ↑((twistedCochainComplexXEquiv ⋯ ⋯ hM n) ((ModuleCat.Hom.hom ((m.twistedIndexCochainComplexι hM p).f n)) f)) = ↑((m.twistedIndexCochainComplexXEquiv hM p n) f)

The stage inclusion preserves the underlying homogeneous function.

instance TauCeti.TwistingCocycle.mono_twistedIndexCochainComplexι {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p : ℤ) : CategoryTheory.Mono (m.twistedIndexCochainComplexι hM p)

Each filtration stage embeds as a subcomplex of the twisted complex.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexCochainComplexMap_ι {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) {p q : ℤ} (hpq : p ≤ q) : CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexMap hM hpq) (m.twistedIndexCochainComplexι hM q) = m.twistedIndexCochainComplexι hM p

Transition maps commute with the inclusions into the twisted complex.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexCochainComplexMap_ι_assoc {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) {p q : ℤ} (hpq : p ≤ q) {Z : CochainComplex (ModuleCat R) ℤ} (h✝ : m.twistedCochainComplex dM hM ⟶ Z) : CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexMap hM hpq) (CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexι hM q) h✝) = CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexι hM p) h✝

Transition maps commute with the inclusions into the twisted complex.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexCochainComplexMap_id {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p : ℤ) : m.twistedIndexCochainComplexMap hM ⋯ = CategoryTheory.CategoryStruct.id (m.twistedIndexCochainComplex hM p)

The transition map from a filtration stage to itself is the identity.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexCochainComplexMap_comp {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) {p q r : ℤ} (hpq : p ≤ q) (hqr : q ≤ r) : CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexMap hM hpq) (m.twistedIndexCochainComplexMap hM hqr) = m.twistedIndexCochainComplexMap hM ⋯

The transition maps of the index filtration compose.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexCochainComplexMap_comp_assoc {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) {p q r : ℤ} (hpq : p ≤ q) (hqr : q ≤ r) {Z : CochainComplex (ModuleCat R) ℤ} (h✝ : m.twistedIndexCochainComplex hM r ⟶ Z) : CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexMap hM hpq) (CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexMap hM hqr) h✝) = CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexMap hM ⋯) h✝

The transition maps of the index filtration compose.

noncomputable def TauCeti.TwistingCocycle.twistedIndexSubobject {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p : ℤ) : CategoryTheory.Subobject (m.twistedCochainComplex dM hM)

The index filtration as actual subobjects of the twisted cochain complex.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexSubobject_eq_mk {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p : ℤ) : m.twistedIndexSubobject hM p = CategoryTheory.Subobject.mk (m.twistedIndexCochainComplexι hM p)

The filtration subobject is represented by the canonical stage inclusion.

theorem TauCeti.TwistingCocycle.mem_range_twistedIndexSubobject_arrow_f_iff {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) (p n : ℤ) (f : ↑((m.twistedCochainComplex dM hM).X n)) : f ∈ (ModuleCat.Hom.hom ((m.twistedIndexSubobject hM p).arrow.f n)).range ↔ ∀ (x : P), p < ind x → ↑((twistedCochainComplexXEquiv ⋯ ⋯ hM n) f) x = 0

In degree n, the p-th filtration stage consists of the homogeneous families vanishing on generators of index greater than p.

theorem TauCeti.TwistingCocycle.twistedIndexSubobject_mono {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) : Monotone (m.twistedIndexSubobject hM)

The subobjects of the twisted complex form an increasing filtration.

theorem TauCeti.TwistingCocycle.twistedIndexSubobject_eq_top {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) {p : ℤ} (hp : ∀ (x : P), ind x ≤ p) : m.twistedIndexSubobject hM p = ⊤

Above all generator indices the subobject filtration is the whole twisted complex.

theorem TauCeti.TwistingCocycle.twistedIndexSubobject_eq_bot {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) {p : ℤ} (hp : ∀ (x : P), p < ind x) : m.twistedIndexSubobject hM p = ⊥

Below all generator indices the subobject filtration vanishes.

theorem TauCeti.TwistingCocycle.twistedIndexSubobject_bounded {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) {dM : M →ₗ[R] M} (hM : IsDGRightModule h ℳ dM) : ∃ (a : ℤ) (b : ℤ), m.twistedIndexSubobject hM a = ⊥ ∧ m.twistedIndexSubobject hM b = ⊤

The actual subcomplex filtration is bounded below and exhaustive for finite generators.

The graded pieces of the index filtration

noncomputable def TauCeti.TwistingCocycle.twistedIndexCochainComplexProj {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) : m.twistedIndexCochainComplex hM p ⟶ twistedCochainComplex 0 dM hM

The restriction F_p ⟶ ℳ ⊗ ⟨P_p⟩ from the pth step of the index filtration to the twisted complex of the zero cocycle on the generators P_p of index p.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexCochainComplexProj_f_apply {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p n : ℤ) (f : ↑((m.twistedIndexCochainComplex hM p).X n)) : ↑((twistedCochainComplexXEquiv ⋯ ⋯ hM n) ((ModuleCat.Hom.hom ((m.twistedIndexCochainComplexProj dM hM p).f n)) f)) = (LinearMap.funLeft R M Subtype.val) ↑((m.twistedIndexCochainComplexXEquiv hM p n) f)

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexMap_comp_proj {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) : CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexMap hM ⋯) (m.twistedIndexCochainComplexProj dM hM (p + 1)) = 0

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexMap_comp_proj_assoc {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) {Z : CochainComplex (ModuleCat R) ℤ} (h✝ : twistedCochainComplex 0 dM hM ⟶ Z) : CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexMap hM ⋯) (CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexProj dM hM (p + 1)) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

noncomputable def TauCeti.TwistingCocycle.twistedIndexShortComplex {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) : CategoryTheory.ShortComplex (CochainComplex (ModuleCat R) ℤ)

The short complex F_p ⟶ F_{p+1} ⟶ ℳ ⊗ ⟨P_{p+1}⟩ of the index filtration, whose second map restricts to the generators of index p + 1.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexShortComplex_X₁ {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) : (m.twistedIndexShortComplex dM hM p).X₁ = m.twistedIndexCochainComplex hM p

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexShortComplex_X₂ {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) : (m.twistedIndexShortComplex dM hM p).X₂ = m.twistedIndexCochainComplex hM (p + 1)

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexShortComplex_X₃ {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) : (m.twistedIndexShortComplex dM hM p).X₃ = twistedCochainComplex 0 dM hM

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexShortComplex_f {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) : (m.twistedIndexShortComplex dM hM p).f ≍ m.twistedIndexCochainComplexMap hM ⋯

The first map in twistedIndexShortComplex is the inclusion F_p ⟶ F_{p+1}.

@[simp]

theorem TauCeti.TwistingCocycle.twistedIndexShortComplex_g {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) : (m.twistedIndexShortComplex dM hM p).g ≍ m.twistedIndexCochainComplexProj dM hM (p + 1)

The second map in twistedIndexShortComplex is restriction to the generators of index p + 1.

theorem TauCeti.TwistingCocycle.surjective_twistedIndexCochainComplexProj_f {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p n : ℤ) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((m.twistedIndexCochainComplexProj dM hM p).f n))

The restriction F_p ⟶ ℳ ⊗ ⟨P_p⟩ is surjective in each degree: a function on the generators of index p extends by zero to a function supported on the generators of index at most p.

theorem TauCeti.TwistingCocycle.exists_twistedIndexCochainComplexMap_f_eq {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p n : ℤ) (g : ↑((m.twistedIndexCochainComplex hM (p + 1)).X n)) (hg : (CategoryTheory.ConcreteCategory.hom ((m.twistedIndexCochainComplexProj dM hM (p + 1)).f n)) g = 0) : ∃ (f : ↑((m.twistedIndexCochainComplex hM p).X n)), (CategoryTheory.ConcreteCategory.hom ((m.twistedIndexCochainComplexMap hM ⋯).f n)) f = g

An element of F_{p+1} whose restriction to the generators of index p + 1 vanishes comes from F_p.

theorem TauCeti.TwistingCocycle.twistedIndexShortComplex_shortExact {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) : (m.twistedIndexShortComplex dM hM p).ShortExact

The graded pieces of the index filtration. The sequence F_p ⟶ F_{p+1} ⟶ ℳ ⊗ ⟨P_{p+1}⟩ is short exact: the quotient F_{p+1} / F_p is the twisted complex of the zero cocycle on the generators of index p + 1.

noncomputable def TauCeti.TwistingCocycle.twistedIndexCochainComplexProjIsCokernel {R : Type uR} {A : Type uA} {M : Type uM} {P : Type uP} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] [Fintype P] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {ind : P → ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (dM : M →ₗ[R] M) (hM : IsDGRightModule h ℳ dM) (p : ℤ) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (m.twistedIndexCochainComplexProj dM hM (p + 1)) ⋯)

Restriction to the generators of index p + 1 is a cokernel of the inclusion F_p ⟶ F_{p+1}.