One-object homological complexes

A square-zero endomorphism of an object in a category with zero morphisms determines a homological complex indexed by Unit, using the circular shape ComplexShape.refl Unit. This file provides that construction and records its unique object and differential.

Main definitions

• TauCeti.oneObjectHomologicalComplex: the homological complex associated to a square-zero endomorphism.

@[instance_reducible]

instance ComplexShape.refl.decidableRel {ι : Type u_1} [DecidableEq ι] : DecidableRel (refl ι).Rel

Membership in the relation of the one-object-per-index shape ComplexShape.refl ι is decidable when equality of indices is.

Equations

• ComplexShape.refl.decidableRel i j = ComplexShape.refl.decidableRel._aux_1 i j

theorem ComplexShape.refl_rel {ι : Type u_1} (i : ι) : (refl ι).Rel i i

Every index of ComplexShape.refl ι is related to itself.

def TauCeti.oneObjectHomologicalComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (d : X ⟶ X) (d_comp_d : CategoryTheory.CategoryStruct.comp d d = 0) : HomologicalComplex C (ComplexShape.refl Unit)

The one-object homological complex associated to a square-zero endomorphism.

Equations

• TauCeti.oneObjectHomologicalComplex X d d_comp_d = { X := fun (x : Unit) => X, d := fun (x x_1 : Unit) => d, shape := ⋯, d_comp_d' := ⋯ }

@[simp]

theorem TauCeti.oneObjectHomologicalComplex_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (d : X ⟶ X) (d_comp_d : CategoryTheory.CategoryStruct.comp d d = 0) (i : Unit) : (oneObjectHomologicalComplex X d d_comp_d).X i = X

The unique object of the one-object homological complex is its defining object.

@[simp]

theorem TauCeti.oneObjectHomologicalComplex_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (d : X ⟶ X) (d_comp_d : CategoryTheory.CategoryStruct.comp d d = 0) : (oneObjectHomologicalComplex X d d_comp_d).d () () = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp d (CategoryTheory.eqToHom ⋯))

The unique differential of the one-object homological complex is its defining endomorphism, transported across the canonical object equation.