The model category structure on bounded below complexes

Let C be an abelian category with enough injectives. In this file, we define a model category structure on the category CochainComplex.Plus C of bounded below cochain complexes in C. The cofibrations are monomorphisms, the weak equivalences are quasi-isomorphisms and the fibrations are those morphisms that are degreewise epimorphisms with an injective kernel. The ModelCategory instance is scoped in the namespace CochainComplex.Plus.modelCategoryQuillen.

References

• Daniel G. Quillen, Homotopical algebra, §I.1, Example B

@[implicit_reducible]

def CochainComplex.Plus.modelCategoryQuillen.instCategoryWithWeakEquivalences {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : HomotopicalAlgebra.CategoryWithWeakEquivalences (Plus C)

The weak equivalences in the category CochainComplex.Plus C of bounded below cochain complexes are quasi-isomorphisms.

Equations

• CochainComplex.Plus.modelCategoryQuillen.instCategoryWithWeakEquivalences = { weakEquivalences := CochainComplex.Plus.quasiIso C }

@[implicit_reducible]

def CochainComplex.Plus.modelCategoryQuillen.instCategoryWithCofibrations {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : HomotopicalAlgebra.CategoryWithCofibrations (Plus C)

The cofibrations in the category CochainComplex.Plus C of bounded below cochain complexes are monomorphisms.

Equations

• CochainComplex.Plus.modelCategoryQuillen.instCategoryWithCofibrations = { cofibrations := CategoryTheory.MorphismProperty.monomorphisms (CochainComplex.Plus C) }

@[implicit_reducible]

def CochainComplex.Plus.modelCategoryQuillen.instCategoryWithFibrations {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : HomotopicalAlgebra.CategoryWithFibrations (Plus C)

The fibrations in the category CochainComplex.Plus C of bounded below cochain complexes are the morphisms that are degreewise epi with an injective kernel.

Equations

• CochainComplex.Plus.modelCategoryQuillen.instCategoryWithFibrations = { fibrations := CochainComplex.degreewiseEpiWithInjectiveKernel.inverseImage (CochainComplex.Plus.ι C) }

instance CochainComplex.Plus.modelCategoryQuillen.instHasTwoOutOfThreePropertyWeakEquivalences {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : (HomotopicalAlgebra.weakEquivalences (Plus C)).HasTwoOutOfThreeProperty

instance CochainComplex.Plus.modelCategoryQuillen.instIsStableUnderRetractsWeakEquivalences {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : (HomotopicalAlgebra.weakEquivalences (Plus C)).IsStableUnderRetracts

instance CochainComplex.Plus.modelCategoryQuillen.instIsStableUnderRetractsCofibrations {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : (HomotopicalAlgebra.cofibrations (Plus C)).IsStableUnderRetracts

instance CochainComplex.Plus.modelCategoryQuillen.instIsStableUnderRetractsFibrations {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : (HomotopicalAlgebra.fibrations (Plus C)).IsStableUnderRetracts

theorem CochainComplex.Plus.modelCategoryQuillen.cofibration_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X Y : Plus C} (f : X ⟶ Y) : HomotopicalAlgebra.Cofibration f ↔ CategoryTheory.Mono f

theorem CochainComplex.Plus.modelCategoryQuillen.fibration_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X Y : Plus C} (f : X ⟶ Y) : HomotopicalAlgebra.Fibration f ↔ degreewiseEpiWithInjectiveKernel f.hom

theorem CochainComplex.Plus.modelCategoryQuillen.isFibrant_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : Plus C) : HomotopicalAlgebra.IsFibrant X ↔ ∀ (n : ℤ), CategoryTheory.Injective (X.obj.X n)

theorem CochainComplex.Plus.modelCategoryQuillen.weakEquivalence_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X Y : Plus C} (f : X ⟶ Y) : HomotopicalAlgebra.WeakEquivalence f ↔ QuasiIso f.hom

instance CochainComplex.Plus.modelCategoryQuillen.instMonoOfCofibration {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A B : Plus C} (i : A ⟶ B) [HomotopicalAlgebra.Cofibration i] : CategoryTheory.Mono i

instance CochainComplex.Plus.modelCategoryQuillen.instHasLiftingPropertyOfMonoOfWeakEquivalenceOfFibration {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A B X Y : Plus C} (i : A ⟶ B) (p : X ⟶ Y) [CategoryTheory.Mono i] [HomotopicalAlgebra.WeakEquivalence i] [HomotopicalAlgebra.Fibration p] : CategoryTheory.HasLiftingProperty i p

instance CochainComplex.Plus.modelCategoryQuillen.instHasLiftingPropertyOfMonoOfFibrationOfWeakEquivalence {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A B X Y : Plus C} (i : A ⟶ B) (p : X ⟶ Y) [CategoryTheory.Mono i] [HomotopicalAlgebra.Fibration p] [HomotopicalAlgebra.WeakEquivalence p] : CategoryTheory.HasLiftingProperty i p

instance CochainComplex.Plus.modelCategoryQuillen.instHasFactorizationTrivialCofibrationsFibrations {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : (HomotopicalAlgebra.trivialCofibrations (Plus C)).HasFactorization (HomotopicalAlgebra.fibrations (Plus C))

instance CochainComplex.Plus.modelCategoryQuillen.instHasFactorizationCofibrationsTrivialFibrations {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : (HomotopicalAlgebra.cofibrations (Plus C)).HasFactorization (HomotopicalAlgebra.trivialFibrations (Plus C))

@[implicit_reducible]

def CochainComplex.Plus.modelCategoryQuillen.instModelCategory {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : HomotopicalAlgebra.ModelCategory (Plus C)

The Quillen model category structure on the category CochainComplex.Plus C of bounded below cochain complexes in an abelian category C with enough injectives.

Equations

• One or more equations did not get rendered due to their size.