Differential modules

A differential module in a category C with zero morphisms is an object X together with an endomorphism d : X ⟶ X such that d ≫ d = 0. For C = ModuleCat Rᵐᵒᵖ this is a right R-module with a square-zero right-linear endomorphism, in the sense of Avramov, Buchweitz and Iyengar. A differential module is a one-periodic object: there is a single object and a single differential, with no grading.

This file builds the category of differential modules, with its preadditive and linear structures and its forgetful functor, and relates it to the neighbouring notions without identifying them:

• DifferentialModule.onePeriodicComplexEquivalence: differential modules are equivalent to homological complexes of shape ComplexShape.up (ZMod 1), the one-periodic complexes, so that Mathlib's homotopies, homotopy category and homology of complexes, and the periodic shift of TauCeti.PeriodicComplex, apply to differential modules through this equivalence (the one-object complex TauCeti.oneObjectHomologicalComplex uses the shape ComplexShape.refl Unit instead, which carries no periodic shift); in particular a homotopy between the one-periodic complexes of φ ψ : M ⟶ N is a single h : M.X ⟶ N.X with φ - ψ = d h + h d (DifferentialModule.nonempty_homotopy_toOnePeriodicComplex_map_iff), and the zero object and binary biproducts of differential modules are obtained through it;
• DifferentialModule.differentialObjectEquivalence: for a shift on C together with a natural isomorphism e : shiftFunctor C 1 ≅ 𝟭 C, differential modules are equivalent to Mathlib's differential objects DifferentialObject S C, whose differentials are d : X ⟶ X⟦1⟧ with d ≫ d⟦1⟧' = 0; the shifted-square law is derived from d ≫ d = 0 using naturality of e;
• DifferentialModule.forgetParity: forgetting the parity of a two-periodic complex X₀ ⇄ X₁ gives the differential module X₀ ⊞ X₁ whose differential has off-diagonal components the two differentials of the complex.

A two-periodic complex is a different object from a differential module: forgetParity forgets the decomposition of the underlying object into its even and odd parts, which a differential module does not carry.

Main definitions

• TauCeti.DifferentialModule: an object with a square-zero endomorphism.
• TauCeti.DifferentialModule.forget: the underlying object.
• TauCeti.DifferentialModule.onePeriodicComplexEquivalence: the equivalence with one-periodic complexes.
• TauCeti.DifferentialModule.differentialObjectEquivalence: the equivalence with differential objects for a shift whose shift by 1 is identified with the identity.
• TauCeti.DifferentialModule.forgetParity: the differential module of a two-periodic complex.

References

• Luchezar L. Avramov, Ragnar-Olaf Buchweitz and Srikanth Iyengar, Class and rank of differential modules, Invent. Math. 169 (2007), 1–35, Section 1.
• Torkil Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.
• The category structure follows Kim Morrison's CategoryTheory.DifferentialObject in Mathlib.CategoryTheory.DifferentialObject.

structure TauCeti.DifferentialModule (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : Type (max u v)

A differential module in a category C with zero morphisms: an object X with an endomorphism d : X ⟶ X such that d ≫ d = 0.

• X : C

  The underlying object.

• d : self.X ⟶ self.X

  The differential.

• d_comp_d : CategoryTheory.CategoryStruct.comp self.d self.d = 0

  The differential squares to zero.

@[simp]

theorem TauCeti.DifferentialModule.d_comp_d_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (self : DifferentialModule C) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.d (CategoryTheory.CategoryStruct.comp self.d h) = CategoryTheory.CategoryStruct.comp 0 h

The differential squares to zero.

structure TauCeti.DifferentialModule.Hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (M N : DifferentialModule C) : Type v

A morphism of differential modules: a morphism of the underlying objects commuting with the differentials.

• f : M.X ⟶ N.X

  The morphism of underlying objects.

• comm : CategoryTheory.CategoryStruct.comp self.f N.d = CategoryTheory.CategoryStruct.comp M.d self.f

  The morphism commutes with the differentials.

theorem TauCeti.DifferentialModule.Hom.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {M N : DifferentialModule C} {x y : M.Hom N} : x = y ↔ x.f = y.f

theorem TauCeti.DifferentialModule.Hom.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {M N : DifferentialModule C} {x y : M.Hom N} (f : x.f = y.f) : x = y

@[simp]

theorem TauCeti.DifferentialModule.Hom.comm_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} (self : M.Hom N) {Z : C} (h : N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp N.d h) = CategoryTheory.CategoryStruct.comp M.d (CategoryTheory.CategoryStruct.comp self.f h)

The morphism commutes with the differentials.

def TauCeti.DifferentialModule.Hom.id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (M : DifferentialModule C) : M.Hom M

The identity morphism of a differential module.

def TauCeti.DifferentialModule.Hom.comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N P : DifferentialModule C} (φ : M.Hom N) (ψ : N.Hom P) : M.Hom P

The composition of morphisms of differential modules.

@[instance_reducible]

instance TauCeti.DifferentialModule.instCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Category.{v, max u v} (DifferentialModule C)

theorem TauCeti.DifferentialModule.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} {φ ψ : M ⟶ N} (h : φ.f = ψ.f) : φ = ψ

theorem TauCeti.DifferentialModule.hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} {φ ψ : M ⟶ N} : φ = ψ ↔ φ.f = ψ.f

@[simp]

theorem TauCeti.DifferentialModule.id_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (M : DifferentialModule C) : (CategoryTheory.CategoryStruct.id M).f = CategoryTheory.CategoryStruct.id M.X

@[simp]

theorem TauCeti.DifferentialModule.comp_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N P : DifferentialModule C} (φ : M ⟶ N) (ψ : N ⟶ P) : (CategoryTheory.CategoryStruct.comp φ ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f

theorem TauCeti.DifferentialModule.comp_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N P : DifferentialModule C} (φ : M ⟶ N) (ψ : N ⟶ P) {Z : C} (h : P.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ ψ).f h = CategoryTheory.CategoryStruct.comp φ.f (CategoryTheory.CategoryStruct.comp ψ.f h)

@[simp]

theorem TauCeti.DifferentialModule.eqToHom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} (h : M = N) : (CategoryTheory.eqToHom h).f = CategoryTheory.eqToHom ⋯

The underlying morphism of an equality transport is the transport of underlying objects.

@[instance_reducible]

instance TauCeti.DifferentialModule.instZeroHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} : Zero (M ⟶ N)

@[simp]

theorem TauCeti.DifferentialModule.zero_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} : Hom.f 0 = 0

@[instance_reducible]

instance TauCeti.DifferentialModule.instHasZeroMorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Limits.HasZeroMorphisms (DifferentialModule C)

def TauCeti.DifferentialModule.forget (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (DifferentialModule C) C

The forgetful functor sending a differential module to its underlying object.

@[simp]

theorem TauCeti.DifferentialModule.forget_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (M : DifferentialModule C) : (forget C).obj M = M.X

@[simp]

theorem TauCeti.DifferentialModule.forget_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X✝ Y✝ : DifferentialModule C} (φ : X✝ ⟶ Y✝) : (forget C).map φ = φ.f

instance TauCeti.DifferentialModule.instFaithfulForget {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (forget C).Faithful

instance TauCeti.DifferentialModule.instIsIsoF {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} (φ : M ⟶ N) [CategoryTheory.IsIso φ] : CategoryTheory.IsIso φ.f

def TauCeti.DifferentialModule.isoMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} (e : M.X ≅ N.X) (comm : CategoryTheory.CategoryStruct.comp e.hom N.d = CategoryTheory.CategoryStruct.comp M.d e.hom) : M ≅ N

A constructor for isomorphisms of differential modules from an isomorphism of the underlying objects commuting with the differentials.

@[simp]

theorem TauCeti.DifferentialModule.isoMk_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} (e : M.X ≅ N.X) (comm : CategoryTheory.CategoryStruct.comp e.hom N.d = CategoryTheory.CategoryStruct.comp M.d e.hom) : (isoMk e comm).hom = { f := e.hom, comm := comm }

@[simp]

theorem TauCeti.DifferentialModule.isoMk_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} (e : M.X ≅ N.X) (comm : CategoryTheory.CategoryStruct.comp e.hom N.d = CategoryTheory.CategoryStruct.comp M.d e.hom) : (isoMk e comm).inv = { f := e.inv, comm := ⋯ }

theorem TauCeti.DifferentialModule.isIso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {M N : DifferentialModule C} (φ : M ⟶ N) : CategoryTheory.IsIso φ ↔ CategoryTheory.IsIso φ.f

A morphism of differential modules is an isomorphism exactly when its underlying morphism is.

The preadditive and linear structures

@[instance_reducible]

instance TauCeti.DifferentialModule.instAddHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} : Add (M ⟶ N)

@[instance_reducible]

instance TauCeti.DifferentialModule.instSubHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} : Sub (M ⟶ N)

@[instance_reducible]

instance TauCeti.DifferentialModule.instNegHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} : Neg (M ⟶ N)

@[simp]

theorem TauCeti.DifferentialModule.add_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} (φ ψ : M ⟶ N) : (φ + ψ).f = φ.f + ψ.f

@[simp]

theorem TauCeti.DifferentialModule.sub_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} (φ ψ : M ⟶ N) : (φ - ψ).f = φ.f - ψ.f

@[simp]

theorem TauCeti.DifferentialModule.neg_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} (φ : M ⟶ N) : (-φ).f = -φ.f

@[instance_reducible]

instance TauCeti.DifferentialModule.instAddCommGroupHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} : AddCommGroup (M ⟶ N)

@[instance_reducible]

instance TauCeti.DifferentialModule.instPreadditive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.Preadditive (DifferentialModule C)

instance TauCeti.DifferentialModule.instAdditiveForget {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (forget C).Additive

@[instance_reducible]

instance TauCeti.DifferentialModule.instSMulHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : SMul R (M ⟶ N)

@[simp]

theorem TauCeti.DifferentialModule.smul_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (a : R) (φ : M ⟶ N) : (a • φ).f = a • φ.f

@[instance_reducible]

instance TauCeti.DifferentialModule.instModuleHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : Module R (M ⟶ N)

@[instance_reducible]

instance TauCeti.DifferentialModule.instLinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Linear R (DifferentialModule C)

instance TauCeti.DifferentialModule.instLinearForget {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (forget C)

One-periodic complexes

@[implicit_reducible]

def TauCeti.DifferentialModule.toOnePeriodicComplex (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (DifferentialModule C) (HomologicalComplex C (ComplexShape.up (ZMod 1)))

The one-periodic complex of a differential module: the object and the differential in the unique degree of ZMod 1.

@[simp]

theorem TauCeti.DifferentialModule.toOnePeriodicComplex_obj_d (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (M : DifferentialModule C) (x✝ x✝¹ : ZMod 1) : ((toOnePeriodicComplex C).obj M).d x✝ x✝¹ = M.d

@[simp]

theorem TauCeti.DifferentialModule.toOnePeriodicComplex_obj_X (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (M : DifferentialModule C) (x✝ : ZMod 1) : ((toOnePeriodicComplex C).obj M).X x✝ = M.X

@[simp]

theorem TauCeti.DifferentialModule.toOnePeriodicComplex_map_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X✝ Y✝ : DifferentialModule C} (φ : X✝ ⟶ Y✝) (x✝ : ZMod 1) : ((toOnePeriodicComplex C).map φ).f x✝ = φ.f

@[implicit_reducible]

def TauCeti.DifferentialModule.ofOnePeriodicComplex (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (HomologicalComplex C (ComplexShape.up (ZMod 1))) (DifferentialModule C)

The differential module of a one-periodic complex K: the object K.X 0 with the differential K.d 0 0.

@[simp]

theorem TauCeti.DifferentialModule.ofOnePeriodicComplex_obj_X (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C (ComplexShape.up (ZMod 1))) : ((ofOnePeriodicComplex C).obj K).X = K.X 0

@[simp]

theorem TauCeti.DifferentialModule.ofOnePeriodicComplex_map_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X✝ Y✝ : HomologicalComplex C (ComplexShape.up (ZMod 1))} (φ : X✝ ⟶ Y✝) : ((ofOnePeriodicComplex C).map φ).f = φ.f 0

@[simp]

theorem TauCeti.DifferentialModule.ofOnePeriodicComplex_obj_d (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C (ComplexShape.up (ZMod 1))) : ((ofOnePeriodicComplex C).obj K).d = K.d 0 0

def TauCeti.DifferentialModule.onePeriodicComplexEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : DifferentialModule C ≌ HomologicalComplex C (ComplexShape.up (ZMod 1))

Differential modules are equivalent to one-periodic complexes, that is to homological complexes of shape ComplexShape.up (ZMod 1).

@[simp]

theorem TauCeti.DifferentialModule.onePeriodicComplexEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (onePeriodicComplexEquivalence C).functor = toOnePeriodicComplex C

@[simp]

theorem TauCeti.DifferentialModule.onePeriodicComplexEquivalence_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (onePeriodicComplexEquivalence C).inverse = ofOnePeriodicComplex C

instance TauCeti.DifferentialModule.instAdditiveHomologicalComplexZModOfNatNatUpToOnePeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (toOnePeriodicComplex C).Additive

instance TauCeti.DifferentialModule.instAdditiveHomologicalComplexZModOfNatNatUpOfOnePeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (ofOnePeriodicComplex C).Additive

instance TauCeti.DifferentialModule.instLinearHomologicalComplexZModOfNatNatUpToOnePeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (toOnePeriodicComplex C)

instance TauCeti.DifferentialModule.instLinearHomologicalComplexZModOfNatNatUpOfOnePeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (ofOnePeriodicComplex C)

instance TauCeti.DifferentialModule.instAdditiveHomologicalComplexZModOfNatNatUpFunctorOnePeriodicComplexEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (onePeriodicComplexEquivalence C).functor.Additive

instance TauCeti.DifferentialModule.instHasZeroObject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasZeroObject (DifferentialModule C)

Differential modules have a zero object when the underlying category does: it is the image of the zero one-periodic complex.

instance TauCeti.DifferentialModule.instHasBinaryBiproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Limits.HasBinaryBiproducts (DifferentialModule C)

Differential modules have binary biproducts when the underlying category does, since they are equivalent to one-periodic complexes.

theorem TauCeti.DifferentialModule.nonempty_homotopy_toOnePeriodicComplex_map_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : DifferentialModule C} (φ ψ : M ⟶ N) : Nonempty (Homotopy ((toOnePeriodicComplex C).map φ) ((toOnePeriodicComplex C).map ψ)) ↔ ∃ (h : M.X ⟶ N.X), φ.f = CategoryTheory.CategoryStruct.comp M.d h + CategoryTheory.CategoryStruct.comp h N.d + ψ.f

A homotopy between the one-periodic complexes of two morphisms φ ψ : M ⟶ N of differential modules is a single morphism h : M.X ⟶ N.X with φ - ψ = d h + h d.

Differential objects for a shift identified with the identity

@[implicit_reducible]

def TauCeti.DifferentialModule.toDifferentialObject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) : CategoryTheory.Functor (DifferentialModule C) (CategoryTheory.DifferentialObject S C)

The differential object of a differential module M, for a natural isomorphism e : shiftFunctor C 1 ≅ 𝟭 C: the differential is M.d ≫ e.inv.app M.X : M.X ⟶ M.X⟦1⟧, and its shifted square vanishes because M.d ≫ M.d = 0.

@[simp]

theorem TauCeti.DifferentialModule.toDifferentialObject_obj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) (M : DifferentialModule C) : ((toDifferentialObject e).obj M).obj = M.X

@[simp]

theorem TauCeti.DifferentialModule.toDifferentialObject_obj_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) (M : DifferentialModule C) : ((toDifferentialObject e).obj M).d = CategoryTheory.CategoryStruct.comp M.d (e.inv.app M.X)

@[simp]

theorem TauCeti.DifferentialModule.toDifferentialObject_map_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) {X✝ Y✝ : DifferentialModule C} (φ : X✝ ⟶ Y✝) : ((toDifferentialObject e).map φ).f = φ.f

@[implicit_reducible]

def TauCeti.DifferentialModule.ofDifferentialObject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) : CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (DifferentialModule C)

The differential module of a differential object Y, for a natural isomorphism e : shiftFunctor C 1 ≅ 𝟭 C: the differential is Y.d ≫ e.hom.app Y.obj : Y.obj ⟶ Y.obj.

@[simp]

theorem TauCeti.DifferentialModule.ofDifferentialObject_map_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) {X✝ Y✝ : CategoryTheory.DifferentialObject S C} (φ : X✝ ⟶ Y✝) : ((ofDifferentialObject e).map φ).f = φ.f

@[simp]

theorem TauCeti.DifferentialModule.ofDifferentialObject_obj_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) (Y : CategoryTheory.DifferentialObject S C) : ((ofDifferentialObject e).obj Y).d = CategoryTheory.CategoryStruct.comp Y.d (e.hom.app Y.obj)

@[simp]

theorem TauCeti.DifferentialModule.ofDifferentialObject_obj_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) (Y : CategoryTheory.DifferentialObject S C) : ((ofDifferentialObject e).obj Y).X = Y.obj

def TauCeti.DifferentialModule.differentialObjectEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) : DifferentialModule C ≌ CategoryTheory.DifferentialObject S C

For a natural isomorphism e : shiftFunctor C 1 ≅ 𝟭 C, differential modules are equivalent to Mathlib's differential objects DifferentialObject S C.

@[simp]

theorem TauCeti.DifferentialModule.differentialObjectEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) : (differentialObjectEquivalence e).functor = toDifferentialObject e

@[simp]

theorem TauCeti.DifferentialModule.differentialObjectEquivalence_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : Type u_1} [AddMonoidWithOne S] [CategoryTheory.HasShift C S] (e : CategoryTheory.shiftFunctor C 1 ≅ CategoryTheory.Functor.id C) : (differentialObjectEquivalence e).inverse = ofDifferentialObject e

Forgetting the parity of a two-periodic complex

@[implicit_reducible]

noncomputable def TauCeti.DifferentialModule.forgetParity (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Functor (HomologicalComplex C (ComplexShape.up (ZMod 2))) (DifferentialModule C)

The differential module obtained by forgetting the parity of a two-periodic complex K: the object K.X 0 ⊞ K.X 1, with the differential whose components are K.d 0 1 : K.X 0 ⟶ K.X 1 and K.d 1 0 : K.X 1 ⟶ K.X 0.

@[simp]

theorem TauCeti.DifferentialModule.forgetParity_obj_X (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : ((forgetParity C).obj K).X = (K.X 0 ⊞ K.X 1)

@[simp]

theorem TauCeti.DifferentialModule.forgetParity_map_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X✝ Y✝ : HomologicalComplex C (ComplexShape.up (ZMod 2))} (φ : X✝ ⟶ Y✝) : ((forgetParity C).map φ).f = CategoryTheory.Limits.biprod.map (φ.f 0) (φ.f 1)

@[simp]

theorem TauCeti.DifferentialModule.inl_forgetParity_obj_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl ((forgetParity C).obj K).d = CategoryTheory.CategoryStruct.comp (K.d 0 1) CategoryTheory.Limits.biprod.inr

Precomposing the differential after forgetting parity with the left inclusion recovers the differential from degree zero to degree one.

@[simp]

theorem TauCeti.DifferentialModule.inl_forgetParity_obj_d_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) {Z : C} (h : ((forgetParity C).obj K).X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp ((forgetParity C).obj K).d h) = CategoryTheory.CategoryStruct.comp (K.d 0 1) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h)

Precomposing the differential after forgetting parity with the left inclusion recovers the differential from degree zero to degree one.

@[simp]

theorem TauCeti.DifferentialModule.inr_forgetParity_obj_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr ((forgetParity C).obj K).d = CategoryTheory.CategoryStruct.comp (K.d 1 0) CategoryTheory.Limits.biprod.inl

Precomposing the differential after forgetting parity with the right inclusion recovers the differential from degree one to degree zero.

@[simp]

theorem TauCeti.DifferentialModule.inr_forgetParity_obj_d_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) {Z : C} (h : ((forgetParity C).obj K).X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp ((forgetParity C).obj K).d h) = CategoryTheory.CategoryStruct.comp (K.d 1 0) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h)

Precomposing the differential after forgetting parity with the right inclusion recovers the differential from degree one to degree zero.

instance TauCeti.DifferentialModule.instAdditiveHomologicalComplexZModOfNatNatUpForgetParity {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (forgetParity C).Additive

instance TauCeti.DifferentialModule.instLinearHomologicalComplexZModOfNatNatUpForgetParity {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (forgetParity C)