Documentation

Mathlib.Algebra.Homology.Functor

Complexes in functor categories #

We can view a complex valued in a functor category T ⥤ V as a functor from T to complexes valued in V.

When V is abelian, a morphism of short complexes or homological complexes in the category T ⥤ V is a quasi-isomorphism iff it is so after evaluation at any t : T.

Future work #

In fact there is an equivalence of categories HomologicalComplex (T ⥤ V) c ≌ T ⥤ HomologicalComplex V c.

source
def HomologicalComplex.asFunctor {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2} [CategoryTheory.Category.{v_2, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3} {c : ComplexShape ι} (C : HomologicalComplex (CategoryTheory.Functor T V) c) :
CategoryTheory.Functor T (HomologicalComplex V c)

A complex of functors gives a functor to complexes.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HomologicalComplex.asFunctor_obj_X {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2} [CategoryTheory.Category.{v_2, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3} {c : ComplexShape ι} (C : HomologicalComplex (CategoryTheory.Functor T V) c) (t : T) (i : ι) :
    (C.asFunctor.obj t).X i = (C.X i).obj t
    source
    @[simp]
    theorem HomologicalComplex.asFunctor_obj_d {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2} [CategoryTheory.Category.{v_2, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3} {c : ComplexShape ι} (C : HomologicalComplex (CategoryTheory.Functor T V) c) (t : T) (i j : ι) :
    (C.asFunctor.obj t).d i j = (C.d i j).app t
    source
    @[simp]
    theorem HomologicalComplex.asFunctor_map_f {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2} [CategoryTheory.Category.{v_2, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3} {c : ComplexShape ι} (C : HomologicalComplex (CategoryTheory.Functor T V) c) {X✝ Y✝ : T} (h : X✝ ⟶ Y✝) (i : ι) :
    (C.asFunctor.map h).f i = (C.X i).map h
    source
    def HomologicalComplex.complexOfFunctorsToFunctorToComplex {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2} [CategoryTheory.Category.{v_2, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3} {c : ComplexShape ι} :
    CategoryTheory.Functor (HomologicalComplex (CategoryTheory.Functor T V) c) (CategoryTheory.Functor T (HomologicalComplex V c))

    The functorial version of HomologicalComplex.asFunctor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem HomologicalComplex.complexOfFunctorsToFunctorToComplex_obj {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2} [CategoryTheory.Category.{v_2, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3} {c : ComplexShape ι} (C : HomologicalComplex (CategoryTheory.Functor T V) c) :
      complexOfFunctorsToFunctorToComplex.obj C = C.asFunctor
      source
      @[simp]
      theorem HomologicalComplex.complexOfFunctorsToFunctorToComplex_map_app_f {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2} [CategoryTheory.Category.{v_2, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3} {c : ComplexShape ι} {X✝ Y✝ : HomologicalComplex (CategoryTheory.Functor T V) c} (f : X✝ ⟶ Y✝) (t : T) (i : ι) :
      ((complexOfFunctorsToFunctorToComplex.map f).app t).f i = (f.f i).app t
      source
      theorem CategoryTheory.ShortComplex.quasiIso_iff_evaluation {T : Type u_1} [Category.{v_1, u_1} T] {V : Type u_2} [Category.{v_2, u_2} V] [Abelian V] {S₁ S₂ : ShortComplex (Functor T V)} (f : S₁ ⟶ S₂) :
      QuasiIso f ↔ ∀ (j : T), QuasiIso (((evaluation T V).obj j).mapShortComplex.map f)
      source
      theorem HomologicalComplex.quasiIsoAt_iff_evaluation {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2} [CategoryTheory.Category.{v_2, u_2} V] [CategoryTheory.Abelian V] {ι : Type u_3} {c : ComplexShape ι} {K₁ K₂ : HomologicalComplex (CategoryTheory.Functor T V) c} (f : K₁ ⟶ K₂) (i : ι) :
      QuasiIsoAt f i ↔ ∀ (t : T), QuasiIsoAt ((((CategoryTheory.evaluation T V).obj t).mapHomologicalComplex c).map f) i
      source
      theorem HomologicalComplex.quasiIso_iff_evaluation {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2} [CategoryTheory.Category.{v_2, u_2} V] [CategoryTheory.Abelian V] {ι : Type u_3} {c : ComplexShape ι} {K₁ K₂ : HomologicalComplex (CategoryTheory.Functor T V) c} (f : K₁ ⟶ K₂) :
      QuasiIso f ↔ ∀ (t : T), QuasiIso ((((CategoryTheory.evaluation T V).obj t).mapHomologicalComplex c).map f)