Documentation

TauCeti.Algebra.Homology.DG.Twisted.Equivalence

Homologous twisting cocycles give homotopy equivalent twisted complexes #

This file bundles the continuation maps and the chain homotopies of TauCeti.Algebra.Homology.DG.Twisted.Continuation and TauCeti.Algebra.Homology.DG.Twisted.Homotopy as morphisms and homotopies of the cochain complexes TwistingCocycle.twistedCochainComplex, and deduces that homologous twisting cocycles (the source's Β§1.4, Definitions 1.10 and 1.11) give homotopy equivalent twisted complexes.

Fix a differential graded algebra (π’œ, d), a differential graded right module (β„³, dM) and twisting cocycles mP on (P, ind) and mQ on (Q, indQ).

Main definitions #

References #

Morphisms between terms of the twisted complexes #

source
noncomputable def TauCeti.termHom {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} (mP : TwistingCocycle π’œ d P ind) (mQ : TwistingCocycle π’œ d Q indQ) (hM : IsDGRightModule h β„³ dM) (Ξ¦ : (P β†’ M) β†’β‚—[R] Q β†’ M) (i j : β„€) (hΞ¦ : βˆ€ f ∈ twistedTotalGrading β„³ ind i, Ξ¦ f ∈ twistedTotalGrading β„³ indQ j) :
(mP.twistedCochainComplex dM hM).X i ⟢ (mQ.twistedCochainComplex dM hM).X j

A linear map Ξ¦ : (P β†’ M) β†’ (Q β†’ M) which sends total degree i into total degree j, as a morphism between the degree-i term of the twisted complex of mP and the degree-j term of the twisted complex of mQ.

Instances For
    source
    @[simp]
    theorem TauCeti.termHom_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} (mP : TwistingCocycle π’œ d P ind) (mQ : TwistingCocycle π’œ d Q indQ) (hM : IsDGRightModule h β„³ dM) (Ξ¦ : (P β†’ M) β†’β‚—[R] Q β†’ M) (i j : β„€) (hΞ¦ : βˆ€ f ∈ twistedTotalGrading β„³ ind i, Ξ¦ f ∈ twistedTotalGrading β„³ indQ j) (x : ↑((mP.twistedCochainComplex dM hM).X i)) :
    ↑((twistedCochainComplexXEquiv β‹― β‹― hM j) ((ModuleCat.Hom.hom (termHom mP mQ hM Ξ¦ i j hΞ¦)) x)) = Ξ¦ ↑((twistedCochainComplexXEquiv β‹― β‹― hM i) x)
    source
    theorem TauCeti.termHom_ext {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} {hM : IsDGRightModule h β„³ dM} {i j : β„€} {a b : (mP.twistedCochainComplex dM hM).X i ⟢ (mQ.twistedCochainComplex dM hM).X j} (hab : βˆ€ (x : ↑((mP.twistedCochainComplex dM hM).X i)), ↑((twistedCochainComplexXEquiv β‹― β‹― hM j) ((ModuleCat.Hom.hom a) x)) = ↑((twistedCochainComplexXEquiv β‹― β‹― hM j) ((ModuleCat.Hom.hom b) x))) :
    a = b

    Two morphisms between terms of twisted complexes are equal when they agree on the underlying functions.

    The morphism of a continuation cocycle #

    source
    noncomputable def TauCeti.ContinuationCocycle.continuationHom {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} (Ξ½ : ContinuationCocycle mP mQ) (hM : IsDGRightModule h β„³ dM) :
    mP.twistedCochainComplex dM hM ⟢ mQ.twistedCochainComplex dM hM

    The continuation map of a continuation cocycle Ξ½ : mP β†’ mQ, as a morphism of cochain complexes between the twisted complexes of a differential graded right module.

    Instances For
      source
      @[simp]
      theorem TauCeti.ContinuationCocycle.continuationHom_f_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} (Ξ½ : ContinuationCocycle mP mQ) (hM : IsDGRightModule h β„³ dM) (n : β„€) (x : ↑((mP.twistedCochainComplex dM hM).X n)) :
      ↑((twistedCochainComplexXEquiv β‹― β‹― hM n) ((ModuleCat.Hom.hom ((Ξ½.continuationHom hM).f n)) x)) = (continuationMap R M Ξ½.Ξ½) ↑((twistedCochainComplexXEquiv β‹― β‹― hM n) x)
      source
      @[simp]
      theorem TauCeti.ContinuationCocycle.continuationHom_refl {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P : Type uP} {ind : P β†’ β„€} [Fintype P] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} [DecidableEq P] (hM : IsDGRightModule h β„³ dM) :
      (refl β‹― mP).continuationHom hM = CategoryTheory.CategoryStruct.id (mP.twistedCochainComplex dM hM)

      The Kronecker continuation cocycle induces the identity morphism.

      source
      @[simp]
      theorem TauCeti.ContinuationCocycle.continuationHom_comp {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q S : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} {indS : S β†’ β„€} [Fintype P] [Fintype Q] [Fintype S] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} {mS : TwistingCocycle π’œ d S indS} (ν₁ : ContinuationCocycle mP mQ) (Ξ½β‚‚ : ContinuationCocycle mQ mS) (hM : IsDGRightModule h β„³ dM) :
      (comp h ν₁ Ξ½β‚‚).continuationHom hM = CategoryTheory.CategoryStruct.comp (ν₁.continuationHom hM) (Ξ½β‚‚.continuationHom hM)

      The composite of continuation cocycles induces the composite of the morphisms.

      source
      theorem TauCeti.ContinuationCocycle.factors_twistedIndexSubobject {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} (Ξ½ : ContinuationCocycle mP mQ) (hM : IsDGRightModule h β„³ dM) (hΞ½ : βˆ€ (x : P) (y : Q), ind x < indQ y β†’ Ξ½.Ξ½ x y = 0) (p : β„€) :
      (mQ.twistedIndexSubobject hM p).Factors (CategoryTheory.CategoryStruct.comp (mP.twistedIndexSubobject hM p).arrow (Ξ½.continuationHom hM))

      A continuation cocycle with no entries strictly increasing the index sends each piece of the index filtration into the corresponding piece.

      The homotopy of a parametrized cocycle #

      source
      noncomputable def TauCeti.ParametrizedCocycle.homotopy {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} {Ξ½β‚€ ν₁ : ContinuationCocycle mP mQ} (Ξ· : ParametrizedCocycle Ξ½β‚€ ν₁) (hM : IsDGRightModule h β„³ dM) :
      Homotopy (ν₁.continuationHom hM) (Ξ½β‚€.continuationHom hM)

      A parametrized cocycle Ξ· between continuation cocycles Ξ½β‚€ and ν₁ is a homotopy between their morphisms of twisted complexes, whose component X i ⟢ X (i - 1) is the homotopy map.

      Instances For
        source
        @[simp]
        theorem TauCeti.ParametrizedCocycle.homotopy_hom_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} {Ξ½β‚€ ν₁ : ContinuationCocycle mP mQ} (Ξ· : ParametrizedCocycle Ξ½β‚€ ν₁) (hM : IsDGRightModule h β„³ dM) (j : β„€) (x : ↑((mP.twistedCochainComplex dM hM).X (j + 1))) :
        ↑((twistedCochainComplexXEquiv β‹― β‹― hM j) ((ModuleCat.Hom.hom ((Ξ·.homotopy hM).hom (j + 1) j)) x)) = (homotopyMap Ξ·.h β„³) ↑((twistedCochainComplexXEquiv β‹― β‹― hM (j + 1)) x)

        The component X (j + 1) ⟢ X j of the homotopy of a parametrized cocycle is its homotopy map.

        source
        theorem TauCeti.ParametrizedCocycle.homotopy_hom_eq_zero {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} {Ξ½β‚€ ν₁ : ContinuationCocycle mP mQ} (Ξ· : ParametrizedCocycle Ξ½β‚€ ν₁) (hM : IsDGRightModule h β„³ dM) {i j : β„€} (hij : j + 1 β‰  i) :
        (Ξ·.homotopy hM).hom i j = 0

        The components of the homotopy of a parametrized cocycle vanish outside adjacent degrees.

        Homologous twisting cocycles #

        source
        structure TauCeti.Homologous {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} [DecidableEq P] [DecidableEq Q] (h : IsDGAlgebra π’œ d) (mP : TwistingCocycle π’œ d P ind) (mQ : TwistingCocycle π’œ d Q indQ) :
        Type (max uA uP)

        Two twisting cocycles mP and mQ are homologous when there are continuation cocycles Ξ½ : mP β†’ mQ and Ξ½' : mQ β†’ mP whose two composites are joined to the Kronecker cocycles by parametrized cocycles.

        Instances For
          source
          noncomputable def TauCeti.Homologous.homotopyEquiv {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} [DecidableEq P] [DecidableEq Q] (H : Homologous h mP mQ) (hM : IsDGRightModule h β„³ dM) :
          HomotopyEquiv (mP.twistedCochainComplex dM hM) (mQ.twistedCochainComplex dM hM)

          Homologous twisting cocycles give homotopy equivalent twisted complexes: for every differential graded right module (β„³, dM), the twisted complexes of mP and mQ are homotopy equivalent.

          Instances For
            source
            @[simp]
            theorem TauCeti.Homologous.homotopyEquiv_hom {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} [DecidableEq P] [DecidableEq Q] (H : Homologous h mP mQ) (hM : IsDGRightModule h β„³ dM) :
            (H.homotopyEquiv hM).hom = H.Ξ½.continuationHom hM
            source
            @[simp]
            theorem TauCeti.Homologous.homotopyEquiv_inv {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P Q : Type uP} {ind : P β†’ β„€} {indQ : Q β†’ β„€} [Fintype P] [Fintype Q] [Module Aᡐᡒᡖ M] [IsScalarTower R Aᡐᡒᡖ M] [SMulCommClass R Aᡐᡒᡖ M] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {β„³ : β„€ β†’ Submodule R M} [DirectSum.Decomposition β„³] [SetLike.GradedSMul ((InternalGrading.ofDecomposition π’œ).opposite.piece β„€) β„³] {dM : M β†’β‚—[R] M} {mP : TwistingCocycle π’œ d P ind} {mQ : TwistingCocycle π’œ d Q indQ} [DecidableEq P] [DecidableEq Q] (H : Homologous h mP mQ) (hM : IsDGRightModule h β„³ dM) :
            (H.homotopyEquiv hM).inv = H.Ξ½'.continuationHom hM