Documentation

TauCeti.Algebra.Homology.DG.Twisted.Complex

The twisted complex of a twisting cocycle #

Let m : P β†’ P β†’ A be a matrix of coefficients in the differential graded algebra (π’œ, d), indexed by the finite set P graded by ind, and let (β„³, dM) be a differential graded right module over (π’œ, d). The twisted complex β„³ βŠ— ⟨P⟩ has underlying module P β†’ M, the direct sum of one copy of M for each generator, and differential

D (Ξ± βŠ— x) = dM Ξ± βŠ— x + (-1) ^ |Ξ±| Ξ£_y (Ξ± Β· m x y) βŠ— y

on a homogeneous elementary tensor Ξ± βŠ— x, written Pi.single x Ξ±. The Koszul sign is carried by the Koszul twist of parameter one, (InternalGrading.ofDecomposition β„³).koszulTwist 1, which is Ξ± ↦ (-1) ^ |Ξ±| Ξ± on M. The total degree of Ξ± βŠ— x is |Ξ±| - ind x, so a generator of index k sits in cohomological degree -k.

The differential is defined for any matrix. It raises the total degree by one when the entries are homogeneous of degree ind y - ind x + 1, and it squares to zero when in addition m satisfies the twisting equation; the one-sidedness of a TauCeti.TwistingCocycle plays no role, and the results for a twisting cocycle are the specializations to its matrix. The twisted complex is packaged as a cochain complex of R-modules through TauCeti.gradedCochainComplex. Right modules are represented as left modules over Aᡐᡒᡖ, so Ξ± Β· a is written MulOpposite.op a β€’ Ξ±.

Main definitions #

Main results #

References #

source
def TauCeti.twistedTotalGrading {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {P : Type uP} (β„³ : β„€ β†’ Submodule R M) (ind : P β†’ β„€) (n : β„€) :
Submodule R (P β†’ M)

The twisted complex β„³ βŠ— ⟨P⟩, identified with P β†’ M, is graded in total degree n by f x ∈ β„³ (n + ind x): the generator x sits in cohomological degree -ind x.

Instances For
    source
    @[simp]
    theorem TauCeti.mem_twistedTotalGrading_iff {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {P : Type uP} {ind : P β†’ β„€} {β„³ : β„€ β†’ Submodule R M} {n : β„€} {f : P β†’ M} :
    f ∈ twistedTotalGrading β„³ ind n ↔ βˆ€ (x : P), f x ∈ β„³ (n + ind x)
    source
    instance TauCeti.instGradedSMulTwistedTotalGrading {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {P : Type uP} {ind : P β†’ β„€} {A : Type uA} [AddCommMonoid A] [Module R A] [SMul A M] {π’œ : β„€ β†’ Submodule R A} {β„³ : β„€ β†’ Submodule R M} [SetLike.GradedSMul π’œ β„³] :
    SetLike.GradedSMul π’œ (twistedTotalGrading β„³ ind)

    The pointwise left action on P β†’ M adds degrees in the total grading, as soon as the action on M does.

    source
    theorem TauCeti.iSupIndep_twistedTotalGrading {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {P : Type uP} {ind : P β†’ β„€} (β„³ : β„€ β†’ Submodule R M) [DirectSum.Decomposition β„³] :
    iSupIndep (twistedTotalGrading β„³ ind)

    The pieces of the total grading are independent.

    source
    theorem TauCeti.iSup_twistedTotalGrading_eq_top {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {P : Type uP} {ind : P β†’ β„€} (β„³ : β„€ β†’ Submodule R M) [DirectSum.Decomposition β„³] [Finite P] :
    ⨆ (n : β„€), twistedTotalGrading β„³ ind n = ⊀

    The pieces of the total grading span P β†’ M when P is finite.

    source
    @[instance_reducible]
    noncomputable instance TauCeti.instDecompositionTwistedTotalGrading {R : Type uR} {M : Type uM} [Ring R] [AddCommGroup M] [Module R M] {P : Type uP} [Finite P] {ind : P β†’ β„€} (β„³ : β„€ β†’ Submodule R M) [DirectSum.Decomposition β„³] :
    DirectSum.Decomposition (twistedTotalGrading β„³ ind)

    The total grading is an internal direct sum decomposition of P β†’ M for finite P. Over a semiring, independence and spanning do not give an internal direct sum (see DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top), so the instance is stated over a ring.

    source
    noncomputable def TauCeti.twistedDifferential {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Semiring A] {P : Type uP} [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] (m : P β†’ P β†’ A) (β„³ : β„€ β†’ Submodule R M) [DirectSum.Decomposition β„³] (dM : M β†’β‚—[R] M) :
    (P β†’ M) β†’β‚—[R] P β†’ M

    The twisted differential on β„³ βŠ— ⟨P⟩, identified with P β†’ M, of a matrix m. Its y-component is (D f) y = dM (f y) + Ξ£_x op (m x y) β€’ Ξ΅ (f x), where Ξ΅ is the Koszul twist of parameter one; on a homogeneous elementary tensor this is D (Ξ± βŠ— x) = dM Ξ± βŠ— x + (-1) ^ |Ξ±| Ξ£_y (Ξ± Β· m x y) βŠ— y (twistedDifferential_single). The right A-action on M and its commutation with the R-scalars are parameters of the definition: the map depends on the action, and R-linearity needs the commutation.

    Instances For
      source
      @[simp]
      theorem TauCeti.twistedDifferential_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Semiring A] {P : Type uP} [Fintype P] [AddCommMonoid M] [Module R M] [Module Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] (m : P β†’ P β†’ A) {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] (dM : M β†’β‚—[R] M) (f : P β†’ M) (y : P) :
      (twistedDifferential m β„³ dM) f y = dM (f y) + βˆ‘ x : P, MulOpposite.op (m x y) β€’ ((InternalGrading.ofDecomposition β„³).koszulTwist 1) (f x)
      source
      theorem TauCeti.koszulTwist_one_eq_negOnePow_smul {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] {q : β„€} {Ξ± : M} (hΞ± : Ξ± ∈ β„³ q) :
      ((InternalGrading.ofDecomposition β„³).koszulTwist 1) Ξ± = q.negOnePow β€’ Ξ±

      The Koszul twist of parameter one acts on a homogeneous element of degree q by the sign (-1) ^ q.

      source
      theorem TauCeti.twistedDifferential_single {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Semiring A] {P : Type uP} [Fintype P] [AddCommGroup M] [Module R M] [Module Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] (m : P β†’ P β†’ A) {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] (dM : M β†’β‚—[R] M) [DecidableEq P] (x : P) {q : β„€} {Ξ± : M} (hΞ± : Ξ± ∈ β„³ q) :
      (twistedDifferential m β„³ dM) (Pi.single x Ξ±) = Pi.single x (dM Ξ±) + βˆ‘ y : P, Pi.single y (q.negOnePow β€’ MulOpposite.op (m x y) β€’ Ξ±)

      Evaluation on a homogeneous elementary tensor Ξ± βŠ— x, with Ξ± of degree q.

      source
      theorem TauCeti.twistedDifferential_single_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Semiring A] {P : Type uP} [Fintype P] [AddCommGroup M] [Module R M] [Module Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] (m : P β†’ P β†’ A) {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] (dM : M β†’β‚—[R] M) [DecidableEq P] (x z : P) {q : β„€} {Ξ± : M} (hΞ± : Ξ± ∈ β„³ q) :
      (twistedDifferential m β„³ dM) (Pi.single x Ξ±) z = Pi.single x (dM Ξ±) z + q.negOnePow β€’ MulOpposite.op (m x z) β€’ Ξ±

      The z-component of the twisted differential of a homogeneous elementary tensor Ξ± βŠ— x.

      source
      theorem TauCeti.twistedDifferential_mem_twistedTotalGrading {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] {P : Type uP} {ind : P β†’ β„€} [Fintype P] [Module Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] (m : P β†’ P β†’ A) {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] (dM : M β†’β‚—[R] M) {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] (hm : βˆ€ (x y : P), m x y ∈ π’œ (ind y - ind x + 1)) (hdM : LinearMap.IsHomogeneous dM β„³ β„³ 1) {n : β„€} {f : P β†’ M} (hf : f ∈ twistedTotalGrading β„³ ind n) :
      (twistedDifferential m β„³ dM) f ∈ twistedTotalGrading β„³ ind (n + 1)

      The twisted differential of a matrix with homogeneous entries of degree ind y - ind x + 1 raises the total degree by one, for any homogeneous dM of degree one.

      source
      theorem TauCeti.twistedDifferential_sq_zero {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} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} [AddCommGroup M] [Module R M] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] (m : P β†’ P β†’ A) {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] (dM : M β†’β‚—[R] M) [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] (hm : βˆ€ (x y : P), m x y ∈ π’œ (ind y - ind x + 1)) (htw : βˆ€ (x y : P), d (m x y) = βˆ‘ z : P, (ind x - ind z).negOnePow β€’ (m x z * m z y)) (hM : IsDGRightModule h β„³ dM) (f : P β†’ M) :
      (twistedDifferential m β„³ dM) ((twistedDifferential m β„³ dM) f) = 0

      The twisted differential of a matrix with homogeneous entries which satisfies the twisting equation squares to zero, when (β„³, dM) is a differential graded right module over (π’œ, d).

      source
      noncomputable def TauCeti.twistedCochainComplex {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} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} [AddCommGroup M] [Module R M] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {m : P β†’ P β†’ A} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] {dM : M β†’β‚—[R] M} [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] (hm : βˆ€ (x y : P), m x y ∈ π’œ (ind y - ind x + 1)) (htw : βˆ€ (x y : P), d (m x y) = βˆ‘ z : P, (ind x - ind z).negOnePow β€’ (m x z * m z y)) (hM : IsDGRightModule h β„³ dM) :
      CochainComplex (ModuleCat R) β„€

      The twisted complex β„³ βŠ— ⟨P⟩ of a matrix with homogeneous entries which satisfies the twisting equation, as a cochain complex of R-modules: the degree-n term is twistedTotalGrading β„³ ind n and the differential is the restriction of twistedDifferential.

      Instances For
        source
        @[simp]
        theorem TauCeti.twistedCochainComplex_X {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} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} [AddCommGroup M] [Module R M] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {m : P β†’ P β†’ A} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] {dM : M β†’β‚—[R] M} [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] (hm : βˆ€ (x y : P), m x y ∈ π’œ (ind y - ind x + 1)) (htw : βˆ€ (x y : P), d (m x y) = βˆ‘ z : P, (ind x - ind z).negOnePow β€’ (m x z * m z y)) (hM : IsDGRightModule h β„³ dM) (n : β„€) :
        (twistedCochainComplex hm htw hM).X n = ↧β†₯(twistedTotalGrading β„³ ind n)
        source
        noncomputable def TauCeti.twistedCochainComplexXEquiv {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} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} [AddCommGroup M] [Module R M] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {m : P β†’ P β†’ A} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] {dM : M β†’β‚—[R] M} [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] (hm : βˆ€ (x y : P), m x y ∈ π’œ (ind y - ind x + 1)) (htw : βˆ€ (x y : P), d (m x y) = βˆ‘ z : P, (ind x - ind z).negOnePow β€’ (m x z * m z y)) (hM : IsDGRightModule h β„³ dM) (n : β„€) :
        ↑((twistedCochainComplex hm htw hM).X n) ≃ₗ[R] β†₯(twistedTotalGrading β„³ ind n)

        The degree-n term of the twisted complex is the total-degree-n submodule of P β†’ M, as a linear equivalence.

        Instances For
          source
          theorem TauCeti.twistedCochainComplexXEquiv_d {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} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} [AddCommGroup M] [Module R M] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {m : P β†’ P β†’ A} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] {dM : M β†’β‚—[R] M} [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] (hm : βˆ€ (x y : P), m x y ∈ π’œ (ind y - ind x + 1)) (htw : βˆ€ (x y : P), d (m x y) = βˆ‘ z : P, (ind x - ind z).negOnePow β€’ (m x z * m z y)) (hM : IsDGRightModule h β„³ dM) (n : β„€) (f : ↑((twistedCochainComplex hm htw hM).X n)) :
          ↑((twistedCochainComplexXEquiv hm htw hM (n + 1)) ((ModuleCat.Hom.hom ((twistedCochainComplex hm htw hM).d n (n + 1))) f)) = (twistedDifferential m β„³ dM) ↑((twistedCochainComplexXEquiv hm htw hM n) f)

          Under twistedCochainComplexXEquiv, the differential of the twisted complex is the twisted differential.

          source
          theorem TauCeti.TwistingCocycle.twistedDifferential_mem_twistedTotalGrading {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} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} (m : TwistingCocycle π’œ d P ind) [AddCommMonoid M] [Module R M] [Module Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] (dM : M β†’β‚—[R] M) [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] (hdM : LinearMap.IsHomogeneous dM β„³ β„³ 1) {n : β„€} {f : P β†’ M} (hf : f ∈ twistedTotalGrading β„³ ind n) :
          (twistedDifferential m.m β„³ dM) f ∈ twistedTotalGrading β„³ ind (n + 1)

          The twisted differential of a twisting cocycle raises the total degree by one, for any homogeneous dM of degree one.

          source
          theorem TauCeti.TwistingCocycle.twistedDifferential_sq_zero {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} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} (m : TwistingCocycle π’œ d P ind) [AddCommGroup M] [Module R M] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] (dM : M β†’β‚—[R] M) [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] (hM : IsDGRightModule h β„³ dM) (f : P β†’ M) :
          (twistedDifferential m.m β„³ dM) ((twistedDifferential m.m β„³ dM) f) = 0

          The twisted differential of a twisting cocycle squares to zero when (β„³, dM) is a differential graded right module over (π’œ, d).

          source
          @[reducible, inline]
          noncomputable abbrev TauCeti.TwistingCocycle.twistedCochainComplex {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} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} (m : TwistingCocycle π’œ d P ind) [AddCommGroup M] [Module R M] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] (dM : M β†’β‚—[R] M) [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] (hM : IsDGRightModule h β„³ dM) :
          CochainComplex (ModuleCat R) β„€

          The twisted complex β„³ βŠ— ⟨P⟩ of a twisting cocycle, as a cochain complex of R-modules.

          Instances For