# Documentation

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

# The short complexes attached to homological complexes #

In this file, we define a functor shortComplexFunctor C c i : HomologicalComplex C c ⥤ ShortComplex C. By definition, the image of a homological complex K by this functor is the short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

When the homology refactor is completed (TODO @joelriou), the homology of a homological complex K in degree i shall be the homology of the short complex (shortComplexFunctor C c i).obj K, which can be abbreviated as K.sc i.

@[simp]
theorem HomologicalComplex.shortComplexFunctor'_obj_f (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (K : ) :
(().obj K).f =
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_map_τ₁ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) :
∀ {X Y : } (f : X Y), (().map f).τ₁ =
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_obj_X₂ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (K : ) :
(().obj K).X₂ =
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_obj_X₁ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (K : ) :
(().obj K).X₁ =
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_map_τ₂ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) :
∀ {X Y : } (f : X Y), (().map f).τ₂ =
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_obj_g (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (K : ) :
(().obj K).g =
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_map_τ₃ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) :
∀ {X Y : } (f : X Y), (().map f).τ₃ =
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_obj_X₃ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (K : ) :
(().obj K).X₃ =
def HomologicalComplex.shortComplexFunctor' (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) :

The functor HomologicalComplex C c ⥤ ShortComplex C which sends a homological complex K to the short complex K.X i ⟶ K.X j ⟶ K.X k for arbitrary indices i, j and k.

Instances For
@[simp]
theorem HomologicalComplex.shortComplexFunctor_obj_f (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (K : ) :
(().obj K).f =
@[simp]
theorem HomologicalComplex.shortComplexFunctor_map_τ₃ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) :
∀ {X Y : } (f : X Y), (().map f).τ₃ =
@[simp]
theorem HomologicalComplex.shortComplexFunctor_obj_X₁ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (K : ) :
(().obj K).X₁ =
@[simp]
theorem HomologicalComplex.shortComplexFunctor_obj_g (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (K : ) :
(().obj K).g =
@[simp]
theorem HomologicalComplex.shortComplexFunctor_obj_X₃ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (K : ) :
(().obj K).X₃ =
@[simp]
theorem HomologicalComplex.shortComplexFunctor_map_τ₁ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) :
∀ {X Y : } (f : X Y), (().map f).τ₁ =
@[simp]
theorem HomologicalComplex.shortComplexFunctor_obj_X₂ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (K : ) :
(().obj K).X₂ =
@[simp]
theorem HomologicalComplex.shortComplexFunctor_map_τ₂ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) :
∀ {X Y : } (f : X Y), (().map f).τ₂ =
noncomputable def HomologicalComplex.shortComplexFunctor (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) :

The functor HomologicalComplex C c ⥤ ShortComplex C which sends a homological complex K to the short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

Instances For
@[simp]
theorem HomologicalComplex.natIsoSc'_hom_app_τ₂ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (hi : = i) (hk : = k) (X : ) :
((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₂ =
@[simp]
theorem HomologicalComplex.natIsoSc'_inv_app_τ₃ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (hi : = i) (hk : = k) (X : ) :
((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₃ = ().inv
@[simp]
theorem HomologicalComplex.natIsoSc'_hom_app_τ₁ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (hi : = i) (hk : = k) (X : ) :
((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₁ = ().hom
@[simp]
theorem HomologicalComplex.natIsoSc'_inv_app_τ₁ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (hi : = i) (hk : = k) (X : ) :
((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₁ = ().inv
@[simp]
theorem HomologicalComplex.natIsoSc'_inv_app_τ₂ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (hi : = i) (hk : = k) (X : ) :
((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₂ =
@[simp]
theorem HomologicalComplex.natIsoSc'_hom_app_τ₃ (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (hi : = i) (hk : = k) (X : ) :
((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₃ = ().hom
noncomputable def HomologicalComplex.natIsoSc' (C : Type u_1) [] {ι : Type u_2} (c : ) (i : ι) (j : ι) (k : ι) (hi : = i) (hk : = k) :

The natural isomorphism shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k when c.prev j = i and c.next j = k.

Instances For
@[inline, reducible]
abbrev HomologicalComplex.sc' {C : Type u_1} [] {ι : Type u_2} {c : } (K : ) (i : ι) (j : ι) (k : ι) :

The short complex K.X i ⟶ K.X j ⟶ K.X k for arbitrary indices i, j and k.

Instances For
@[inline, reducible]
noncomputable abbrev HomologicalComplex.sc {C : Type u_1} [] {ι : Type u_2} {c : } (K : ) (i : ι) :

The short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

Instances For
@[inline, reducible]
noncomputable abbrev HomologicalComplex.isoSc' {C : Type u_1} [] {ι : Type u_2} {c : } (K : ) (i : ι) (j : ι) (k : ι) (hi : = i) (hk : = k) :

The canonical isomorphism K.sc j ≅ K.sc' i j k when c.prev j = i and c.next j = k.

Instances For