Documentation

TauCeti.Algebra.Homology.Periodic.Examples

Acyclic differential modules need not be contractible #

Over the dual numbers over any commutative ring k, multiplication by ε gives a differential module whose one-periodic complex is exact and whose underlying module is free. When k is nontrivial, no linear homotopy contracts the differential. This example separates acyclicity from contractibility at the boundary between homotopy and derived categories: the one-periodic complex is nonzero in the periodic homotopy category but zero in the periodic derived category. Since it is acyclic and not contractible, it is not homotopically projective, although its unique term is projective (dualNumberDifferentialModule_projective). Thus acyclicity does not imply contractibility, and projectivity of the terms does not imply homotopical projectivity. For the same reason the complex has no projective flag (not_hasProjectiveFlag_dualNumberPeriodicComplex).

References #

source
@[reducible, inline]
abbrev TauCeti.DualNumbers (k : Type u_1) :
Type u_1

The algebra of dual numbers over k.

Instances For
    source
    def TauCeti.dualNumberDifferentialModule {k : Type u_1} [CommRing k] :
    DifferentialModule (ModuleCat (DualNumbers k))

    The differential module on the regular dual-number module with differential multiplication by ε.

    Instances For
      source
      @[simp]
      theorem TauCeti.dualNumberDifferentialModule_X {k : Type u_1} [CommRing k] :
      dualNumberDifferentialModule.X = ↧(DualNumbers k)

      The underlying object of the dual-number differential module is the regular module.

      source
      @[simp]
      theorem TauCeti.dualNumberDifferentialModule_d {k : Type u_1} [CommRing k] :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp dualNumberDifferentialModule.d (CategoryTheory.eqToHom ⋯)) = ModuleCat.ofHom (LinearMap.toSpanSingleton (DualNumbers k) (DualNumbers k) DualNumber.eps)

      Transported to the regular module, the differential is multiplication by ε.

      source
      theorem TauCeti.dualNumberDifferentialModule_d_apply {k : Type u_1} [CommRing k] (x : DualNumbers k) :
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp dualNumberDifferentialModule.d (CategoryTheory.eqToHom ⋯)))) x = x * DualNumber.eps

      The differential sends x to x * ε.

      source
      theorem TauCeti.dualNumberDifferentialModule_projective {k : Type u_1} [CommRing k] :
      CategoryTheory.Projective dualNumberDifferentialModule.X

      The underlying module of dualNumberDifferentialModule is projective.

      source
      @[reducible, inline]
      abbrev TauCeti.dualNumberPeriodicComplex {k : Type u_1} [CommRing k] :
      HomologicalComplex (ModuleCat (DualNumbers k)) (ComplexShape.up (ZMod 1))

      The one-periodic complex associated to multiplication by ε on the dual numbers.

      Instances For
        source
        theorem TauCeti.dualNumberPeriodicComplex_acyclic {k : Type u_1} [CommRing k] :
        dualNumberPeriodicComplex.Acyclic

        The one-periodic complex of the dual-number differential module is acyclic.

        source
        theorem TauCeti.dualNumberDifferentialModule_not_contractible {k : Type u_1} [CommRing k] [Nontrivial k] :
        ¬∃ (h : DualNumbers k →ₗ[DualNumbers k] DualNumbers k), LinearMap.id = LinearMap.toSpanSingleton (DualNumbers k) (DualNumbers k) DualNumber.eps ∘ₗ h + h ∘ₗ LinearMap.toSpanSingleton (DualNumbers k) (DualNumbers k) DualNumber.eps

        Multiplication by ε on the regular module admits no contracting homotopy: there is no linear map h with d h + h d = 1.

        source
        theorem TauCeti.not_isZero_quotient_obj_dualNumberPeriodicComplex {k : Type u_1} [CommRing k] [Nontrivial k] :
        ¬CategoryTheory.Limits.IsZero ((HomotopyCategory.quotient (ModuleCat (DualNumbers k)) (ComplexShape.up (ZMod 1))).obj dualNumberPeriodicComplex)

        The dual-number periodic complex is nonzero in the periodic homotopy category.

        source
        theorem TauCeti.isZero_Q_obj_dualNumberPeriodicComplex {k : Type u_1} [CommRing k] :
        CategoryTheory.Limits.IsZero ((PeriodicComplex.DerivedCategory.Q (ModuleCat (DualNumbers k)) 1).obj dualNumberPeriodicComplex)

        The dual-number periodic complex is zero in the periodic derived category.

        source
        theorem TauCeti.not_isHomotopicallyProjective_dualNumberPeriodicComplex {k : Type u_1} [CommRing k] [Nontrivial k] :
        ¬PeriodicComplex.IsHomotopicallyProjective dualNumberPeriodicComplex

        The dual-number periodic complex is not homotopically projective, although its unique term is projective by dualNumberDifferentialModule_projective.

        source
        theorem TauCeti.not_hasProjectiveFlag_dualNumberPeriodicComplex {k : Type u_1} [CommRing k] [Nontrivial k] :
        ¬PeriodicComplex.HasProjectiveFlag dualNumberPeriodicComplex

        The dual-number periodic complex has no projective flag, although its unique term is projective by dualNumberDifferentialModule_projective.