13.18 Injective resolutions to 13.37 Compact objects

Section13.18 Injective resolutions #

Section 13.18 of the Stacks Project, Tag 013G. 9 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 013I, a definition

Tag 013I in the Stacks Project.

CochainComplex.InjectiveResolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Defs/InjectiveResolution.lean, line 50. References: SGA 2 VIII (1.3); SGA 4½ Etat 0 (3.1.8), “injective case”.

An injective resolution of a cochain complex K in a category C: a bounded below cochain complex cocomplex of injective objects of C, together with a quasi-isomorphism ι : K ⟶ cocomplex.

public structure InjectiveResolution (K : CochainComplex C ℤ)

CategoryTheory.InjectiveResolution.toCochainComplexResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/NatIntBridge.lean, line 289. The attribute's comment: “the identification of the ℕ-graded half of the tag with the ℤ-graded one”.

An injective resolution of an object X, indexed by ℕ, read as an injective resolution of the cochain complex X[0], indexed by ℤ: the resolving complex is extended by zero in the negative degrees, which is Mathlib's CategoryTheory.InjectiveResolution.cochainComplex.

def toCochainComplexResolution (R : InjectiveResolution X) :
    CochainComplex.InjectiveResolution ((CochainComplex.singleFunctor C 0).obj X)

CochainComplex.InjectiveResolution.toNatResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/NatIntBridge.lean, line 325. The attribute's comment: “the identification of the ℤ-graded half of the tag with the ℕ-graded one, for a resolving complex vanishing in the negative degrees”.

An injective resolution of the cochain complex X[0], indexed by ℤ and vanishing in the negative degrees, read as an injective resolution of the object X, indexed by ℕ: the resolving complex is restricted along ComplexShape.embeddingUpNat.

The hypothesis that the resolving complex vanish in the negative degrees cannot be dropped; see the module docstring.

def toNatResolution
    (R : CochainComplex.InjectiveResolution ((CochainComplex.singleFunctor C 0).obj X))
    [R.cocomplex.IsStrictlyGE 0] : CategoryTheory.InjectiveResolution X

Tag 013J, a lemma

Tag 013J in the Stacks Project.

CochainComplex.isGE_iff_exists_quasiIso_isStrictlyGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 93.

Let C be a category with zero morphisms, a zero object and homology for every short complex, and let K be a cochain complex of C. The cohomology of K vanishes in all degrees < n if and only if there is a quasi-isomorphism f : K ⟶ L with L zero in all degrees < n.

public theorem isGE_iff_exists_quasiIso_isStrictlyGE {C : Type*} [Category C]
    [HasZeroMorphisms C] [HasZeroObject C] [CategoryWithHomology C]
    (K : CochainComplex C ℤ) (n : ℤ) :
    K.IsGE n ↔ ∃ (L : CochainComplex C ℤ) (f : K ⟶ L) (_ : QuasiIso f), L.IsStrictlyGE n

Tag 013K, a lemma

Tag 013K in the Stacks Project.

CochainComplex.exists_injectiveResolution_isStrictlyGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 110. References: SGA 4½ Etat 0 (3.2.3), “(4) existence”; SGA 4½ Etat 0 (4.2.3.1), “Corollary 1”.

Let A be an abelian category with enough injectives, let a : ℤ and let K be a cochain complex of A with H ^ n (K) = 0 for n < a. Then K has an injective resolution R whose resolving complex satisfies R.cocomplex.X n = 0 for n < a; and if moreover K.X n = 0 for n < a, then R can be chosen with all the components R.ι.f n : K.X n ⟶ R.cocomplex.X n monomorphisms.

public theorem exists_injectiveResolution_isStrictlyGE [EnoughInjectives A] (a : ℤ)
    (K : CochainComplex A ℤ) [K.IsGE a] :
    ∃ (R : K.InjectiveResolution) (_ : K.IsStrictlyGE a → ∀ n, Mono (R.ι.f n)),
      R.cocomplex.IsStrictlyGE a

Tag 013R, a lemma

Tag 013R in the Stacks Project.

Declarations registered for the tag:

CochainComplex.isKInjective_of_injective registered with add_to_stacks in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 464 (StacksFrontier): “the lemma's induction, with a supplied bound d for the boundedness below: a complex which is strictly bounded below by d and whose terms are injective objects is K-injective”.
CochainComplex.IsKInjective.nonempty_homotopy_zero registered with add_to_stacks in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 468 (StacksFrontier): “the conclusion at one morphism, the source's sentence: a morphism from an acyclic complex to a K-injective complex is homotopic to zero”.
CochainComplex.IsKInjective.rightOrthogonal registered with add_to_stacks in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 472 (StacksFrontier): “the conclusion in K(A): a K-injective complex is right orthogonal to the acyclic complexes, i.e. every morphism K ⟶ I of K(A) with K acyclic is zero”.

Tag 05TF, a remark

Tag 05TF in the Stacks Project.

CochainComplex.bijective_precomp_quotient_map, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 131.

If I is a K-injective cochain complex and α : K ⟶ L is a quasi-isomorphism, then precomposition with the image of α in the homotopy category K(A) is a bijection Hom_{K(A)}(L, I) → Hom_{K(A)}(K, I).

lemma bijective_precomp_quotient_map [I.IsKInjective] (α : K ⟶ L) [QuasiIso α] :
    Function.Bijective (fun β : (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj L ⟶
        (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj I =>
      (HomotopyCategory.quotient A (ComplexShape.up ℤ)).map α ≫ β)

Tag 013P, a lemma

Tag 013P in the Stacks Project.

CochainComplex.IsKInjective.exists_factorization_of_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 159. The attribute's comment: “for a K-injective target, which by 013R covers the source's hypothesis that the target be bounded below with injective terms; the extra hypotheses of part (2) are attached to its own conjunct”. References: SGA 2 VIII (1.4), “existence of Cu”.

Let A be an abelian category, let α : K ⟶ L be a quasi-isomorphism of cochain complexes of A, let I be a K-injective cochain complex of A and let γ : K ⟶ I. Then (1) there is a morphism of complexes β : L ⟶ I such that α ≫ β is homotopic to γ, and (2) if every term of I is an injective object and α is a monomorphism in every degree, then there is a β with α ≫ β = γ.

public theorem IsKInjective.exists_factorization_of_quasiIso [I.IsKInjective] (α : K ⟶ L)
    [QuasiIso α] (γ : K ⟶ I) :
    (∃ β : L ⟶ I, Nonempty (Homotopy (α ≫ β) γ)) ∧
      (∀ [∀ n, Injective (I.X n)] [∀ n, Mono (α.f n)], ∃ β : L ⟶ I, α ≫ β = γ)

CochainComplex.exists_desc_of_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/NatIntBridge.lean, line 438. The attribute's comment: “part (2), for ℕ-indexed complexes, with the source required only to be quasi-isomorphic to a complex concentrated in degree zero and the target only to have injective terms”. References: EGA 0 (12.1.4), “partial”.

Stacks 013P, part (2), for ℕ-indexed complexes: descent with minimal hypotheses. Let C be an abelian category, let ε : Z[0] ⟶ K be a quasi-isomorphism of cochain complexes of C indexed by ℕ, let L be a cochain complex of injective objects and let γ : Z[0] ⟶ L. Then γ = ε ≫ β for a (unique up to homotopy, see CochainComplex.nonempty_homotopy_of_precomp_quasiIso) morphism β : K ⟶ L.

Neither K nor L is required to be an injective resolution: the terms of K are arbitrary and L resolves nothing. Mathlib's CategoryTheory.InjectiveResolution.desc is the special case where both are the resolving complexes of injective resolutions.

theorem exists_desc_of_quasiIso [∀ n, Injective (L.X n)] (ε : (single₀ C).obj Z ⟶ K) [QuasiIso ε]
    (γ : (single₀ C).obj Z ⟶ L) : ∃ β : K ⟶ L, ε ≫ β = γ

Tag 013S, a lemma

Tag 013S in the Stacks Project.

CochainComplex.IsKInjective.nonempty_homotopy_of_precomp_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 174. The attribute's comment: “for a K-injective target, which by Tag 013R covers the source's bounded below complex of injective objects; the source's intermediary γ : K ⟶ I is eliminated by transitivity of homotopy”. References: SGA 2 VIII (1.4), “uniqueness of Cu”.

Let A be an abelian category, let α : K ⟶ L be a quasi-isomorphism of cochain complexes of A and let I be a K-injective cochain complex of A. Then two morphisms β₁, β₂ : L ⟶ I with α ≫ β₁ homotopic to α ≫ β₂ are homotopic.

public theorem IsKInjective.nonempty_homotopy_of_precomp_quasiIso [I.IsKInjective] (α : K ⟶ L)
    [QuasiIso α] {β₁ β₂ : L ⟶ I} (h : Homotopy (α ≫ β₁) (α ≫ β₂)) :
    Nonempty (Homotopy β₁ β₂)

CochainComplex.nonempty_homotopy_of_precomp_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/NatIntBridge.lean, line 468. The attribute's comment: “for ℕ-indexed complexes, with the source required only to be quasi-isomorphic to a complex concentrated in degree zero and the target only to have injective terms”. References: EGA 0 (12.1.4), “partial”; SGA 2 VIII (1.4), “special case”.

Stacks 013S, for ℕ-indexed complexes: uniqueness of the descent with minimal hypotheses. Two morphisms β₁, β₂ : K ⟶ L from a cochain complex quasi-isomorphic to Z[0] into a cochain complex of injective objects which agree, up to homotopy, after precomposition with a quasi-isomorphism ε : Z[0] ⟶ K, are homotopic.

As in CochainComplex.exists_desc_of_quasiIso, neither complex need be an injective resolution. Mathlib's CategoryTheory.InjectiveResolution.descHomotopy is the special case where both are; CategoryTheory.InjectiveResolution.descHomotopy' weakens the target alone.

theorem nonempty_homotopy_of_precomp_quasiIso [∀ n, Injective (L.X n)]
    (ε : (single₀ C).obj Z ⟶ K) [QuasiIso ε] {β₁ β₂ : K ⟶ L}
    (h : Homotopy (ε ≫ β₁) (ε ≫ β₂)) : Nonempty (Homotopy β₁ β₂)

Tag 05TG, a lemma

Tag 05TG in the Stacks Project.

Declarations registered for the tag:

CochainComplex.IsKInjective.Qh_map_bijective registered with add_to_stacks in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 184 (StacksFrontier): “the bijection Mor_{K(A)}(K, I) → Mor_{D(A)}(K, I) for a K-injective I”.
CochainComplex.isKInjective_of_injective registered with add_to_stacks in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 186 (StacksFrontier): “a complex strictly bounded below with injective terms is K-injective”.

Tag 013T, a lemma

Tag 013T in the Stacks Project.

CategoryTheory.ShortComplex.ShortExact.exists_shortExact_injectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/InjectiveResolution.lean, line 434. The attribute's comment: “parts (1)–(3); the given resolution of the first term is a hypothesis and the degree bound of parts (2) and (3) is an implication in the conclusion, so the source's plain assertion follows by resolving the first term with 013K”.

Let A be an abelian category with enough injectives, let S : 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 be a short exact sequence of cochain complexes of A with X₂ (hence X₁ and X₃) vanishing in the degrees < a, and let R₁ be any injective resolution of X₁. Then there are injective resolutions R₂ of X₂ and R₃ of X₃ and a short exact sequence 0 ⟶ I₁ ⟶ I₂ ⟶ I₃ ⟶ 0 of the resolving complexes making both squares commute; and if I₁ also vanishes in the degrees < a, then I₂ and I₃ may be chosen to do so as well.

public theorem exists_shortExact_injectiveResolution [EnoughInjectives A] (a : ℤ)
    {S : ShortComplex (CochainComplex A ℤ)} (hS : S.ShortExact) [S.X₂.IsStrictlyGE a]
    (R₁ : S.X₁.InjectiveResolution) :
    ∃ (R₂ : S.X₂.InjectiveResolution) (R₃ : S.X₃.InjectiveResolution)
      (f : R₁.cocomplex ⟶ R₂.cocomplex) (g : R₂.cocomplex ⟶ R₃.cocomplex)
      (w : f ≫ g = 0) (_ : (ShortComplex.mk f g w).ShortExact)
      (_ : R₁.cocomplex.IsStrictlyGE a →
        R₂.cocomplex.IsStrictlyGE a ∧ R₃.cocomplex.IsStrictlyGE a),
      R₁.ι ≫ f = S.f ≫ R₂.ι ∧ R₂.ι ≫ g = S.g ≫ R₃.ι

CategoryTheory.ShortComplex.ShortExact.exists_injectiveResolution_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/NatHorseshoe.lean, line 171. The attribute's comment: “the ℕ-graded form for a short exact sequence of objects, with the degreewise splitting of the resulting sequence of resolving complexes”.

The injective horseshoe for ℕ-indexed resolutions of objects. Let A be an abelian category with enough injectives and let 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 be a short exact sequence of objects of A. Then there are injective resolutions J₁, J₂, J₃ of the three terms and a short exact sequence 0 ⟶ J₁ ⟶ J₂ ⟶ J₃ ⟶ 0 of the resolving complexes over it: the two squares built from the augmentations commute in degree zero, and the sequence is split in every degree.

This is the ℕ-indexed form of Stacks 013T for a sequence of objects. It is deduced from the ℤ-indexed StacksDraft.CartanEilenbergResolutions.horseshoeProperty, with the two outer resolutions prescribed to be the extensions by zero of arbitrary ℕ-indexed ones, by restricting the resulting sequence of complexes back along ComplexShape.embeddingUpNat.

The degreewise splitting is what makes the sequence stay short exact under an arbitrary additive functor applied degreewise; it is not read off the twisted-biproduct construction of the horseshoe but recovered afterwards from CategoryTheory.ShortComplex.ShortExact.splittingOfInjective, the first term of the sequence in degree n being the injective object J₁.cocomplex.X n.

theorem exists_injectiveResolution_shortExact [EnoughInjectives A]
    {S : ShortComplex A} (hS : S.ShortExact) :
    ∃ (J₁ : InjectiveResolution S.X₁) (J₂ : InjectiveResolution S.X₂)
      (J₃ : InjectiveResolution S.X₃) (f : J₁.cocomplex ⟶ J₂.cocomplex)
      (g : J₂.cocomplex ⟶ J₃.cocomplex) (w : f ≫ g = 0),
      (ShortComplex.mk f g w).ShortExact ∧
      J₁.ι.f 0 ≫ f.f 0 = S.f ≫ J₂.ι.f 0 ∧ J₂.ι.f 0 ≫ g.f 0 = S.g ≫ J₃.ι.f 0 ∧
      ∀ n, ∃ _ : (ShortComplex.mk (f.f n) (g.f n)
        (congrFun (congrArg HomologicalComplex.Hom.f w) n)).Splitting, True

Sources

LeanCochainComplex.InjectiveResolution · CategoryTheory.InjectiveResolution.toCochainComplexResolution · CochainComplex.InjectiveResolution.toNatResolution · CochainComplex.isGE_iff_exists_quasiIso_isStrictlyGE · CochainComplex.exists_injectiveResolution_isStrictlyGE · CochainComplex.isKInjective_of_injective · CochainComplex.IsKInjective.nonempty_homotopy_zero · CochainComplex.IsKInjective.rightOrthogonal

Section13.19 Projective resolutions #

Section 13.19 of the Stacks Project, Tag 0643. 11 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0644, a definition

Tag 0644 in the Stacks Project.

CochainComplex.IsProjectiveResolution, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Defs/ProjectiveResolution.lean, line 112. The attribute's comment: “The case of a complex; for an object it is ProjectiveResolution.”. References: SGA 4½ Etat 0 (3.1.8), “projective case”.

A morphism of cochain complexes α : P ⟶ K in an abelian category is a projective resolution of K if P is bounded above, all the terms of P are projective objects, and α is a quasi-isomorphism.

public class IsProjectiveResolution {P K : CochainComplex C ℤ} (α : P ⟶ K) : Prop
    extends QuasiIso α

Tag 0645, a lemma

Tag 0645 in the Stacks Project.

Stacks.ProjectiveResolution.CohomologyVanishing.cohomology_vanishes_of_isProjectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/HomotopyLift.lean, line 125. The attribute's comment: “(1)”.

Stacks Tag 0645, Lemma 13.19.2, part (1). If K^• has a projective resolution, then H^n(K^•) = 0 for n ≫ 0.

theorem cohomology_vanishes_of_isProjectiveResolution
    (K : CochainComplex A ℤ) (h : IsProjectiveResolution K) :
    CohomologyVanishesForLargeN K

Stacks.ProjectiveResolution.CohomologyVanishing.exists_boundedAbove_quasiIso_of_cohomologyVanishes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/HomotopyLift.lean, line 147. The attribute's comment: “(2)”.

Stacks Tag 0645, Lemma 13.19.2, part (2). If H^n(K^•) = 0 for n ≫ 0, then there exists a quasi-isomorphism L^• → K^• with L^• bounded above.

theorem exists_boundedAbove_quasiIso_of_cohomologyVanishes
    (K : CochainComplex A ℤ) (h : CohomologyVanishesForLargeN K) :
    ∃ (L : CochainComplex A ℤ) (f : L ⟶ K), IsBoundedAboveComplex L ∧ QuasiIso f

Tag 0646, a lemma

Tag 0646 in the Stacks Project.

ProjectiveResolutionLemma.statement3, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/BoundedAbove.lean, line 280. The attribute's comment: “(3)”. References: SGA 4½ Etat 0 (3.1.9), “Part 1, special case”; SGA 4½ Etat 0 (3.2.3), “partial”; SGA 4½ Etat 0 (4.2.3.1), “Corollary 1”.

Statement 3. Assume A has enough projectives. Let K^• be a complex with K^n = 0 for n > a. Then there exists a projective resolution α : P^• → K^• (Definition 4) bounded above by a such that, additionally, each component α^n : P^n → K^n is an epimorphism.

alias statement3

ProjectiveResolutionLemma.statement2, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/BoundedAbove.lean, line 342. The attribute's comment: “(2)”. References: SGA 4½ Etat 0 (3.2.3), “partial”; SGA 4½ Etat 0 (4.2.3.1), “Corollary 1”.

Statement 2. Assume A has enough projectives. Let K^• be a complex with H^n(K^•) = 0 for all n ≫ 0. Then K^• has a projective resolution in the sense of Definition 4, i.e. there exists an upper bound N and a projective resolution of K^• bounded above by N.

theorem statement2 [EnoughProjectives C] (K : CochainComplex C ℤ)
    (hK : ∃ M : ℤ, ∀ n : ℤ, M ≤ n → IsZero (K.homology n)) :
    ∃ N : ℤ, Nonempty (ProjectiveResolutionComplex K N)

ProjectiveResolutionLemma.statement1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/EpiResData.lean, line 140. The attribute's comment: “(1)”. References: SGA 2 VIII (1.4), “special case”; SGA 4½ Etat 0 (3.1.9), “Part 1, special case”; SGA 4½ Etat 0 (3.2.3), “partial”.

Statement 1. If A has enough projectives, then every object A of A has a projective resolution in the sense of Definition 3: there is a complex P^• of projectives with P^n = 0 for n > 0 and a quasi-isomorphism P^• → A[0]. Viewing the resolution as a projective resolution (Definition 4) of the complex A[0] with upper bound 0 captures exactly conditions (1)–(4) of Definition 3.

theorem statement1 [EnoughProjectives C] (A : C) :
    Nonempty (ProjectiveResolutionComplex (single₀ A) 0)

Tag 0647, a lemma

Tag 0647 in the Stacks Project.

projective_into_acyclic_is_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/HomotopyLift.lean, line 309. References: SGA 6 I (4.1), “special case”; SGA 6 II (1.1), “c)”; SGA 6 II (1.2), “1.2 d), special case”.

Let K be an acyclic complex and P a bounded above complex of projective objects. Then every morphism of complexes f : P ⟶ K is homotopic to zero.

theorem projective_into_acyclic_is_zero
    {C : Type*} [CategoryTheory.Category C] [CategoryTheory.Abelian C]
    (P K : CochainComplex C ℤ)
    (n : ℤ) (hP : P.IsStrictlyLE n)
    (hProj : ∀ i : ℤ, CategoryTheory.Projective (P.X i))
    (hK : HomologicalComplex.Acyclic K)
    (f : P ⟶ K) : Nonempty (Homotopy f 0)

Tag 0648, a remark

Tag 0648 in the Stacks Project.

bijective_postcomp_quotient_map, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/KProjective.lean, line 247.

Remark [Stacks 0648] for a K-projective complex, the dual of [Stacks 05TF]. If P is a K-projective cochain complex and α : L ⟶ K is a quasi-isomorphism, then postcomposition with the image of α in the homotopy category is a bijection Hom_{K(A)}(P, L) → Hom_{K(A)}(P, K).

Its surjectivity is the first assertion of [Stacks 0649] and its injectivity is [Stacks 064A].

lemma bijective_postcomp_quotient_map {A : Type u} [Category.{v} A] [Abelian A]
    {P K L : CochainComplex A ℤ} [P.IsKProjective] (α : L ⟶ K) [QuasiIso α] :
    Function.Bijective (fun β : (HomotopyCategory.quotient A (.up ℤ)).obj P ⟶
        (HomotopyCategory.quotient A (.up ℤ)).obj L ↦
      β ≫ (HomotopyCategory.quotient A (.up ℤ)).map α)

Tag 0649, a lemma

Tag 0649 in the Stacks Project.

CochainComplex.IsKProjective.exists_lift_of_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/KProjective.lean, line 274.

Stacks 0649. Let A be an abelian category, let α : L ⟶ K be a quasi-isomorphism of cochain complexes in A and let P be a K-projective cochain complex — for instance one which is bounded above and consists of projective objects, by CochainComplex.isKProjective_of_projective. Then, given γ : P ⟶ K: (1) there is a β : P ⟶ L with β ≫ α homotopic to γ, and (2) if the terms of P are projective and α is epimorphic in every degree, there is a β : P ⟶ L with β ≫ α = γ.

public theorem CochainComplex.IsKProjective.exists_lift_of_quasiIso {A : Type u} [Category.{v} A]
    [Abelian A] {P K L : CochainComplex A ℤ} [P.IsKProjective] (α : L ⟶ K) [QuasiIso α]
    (γ : P ⟶ K) :
    (∃ β : P ⟶ L, Nonempty (Homotopy (β ≫ α) γ)) ∧
      ((∀ n : ℤ, Projective (P.X n)) → (∀ n : ℤ, Epi (α.f n)) → ∃ β : P ⟶ L, β ≫ α = γ)

Tag 064A, a lemma

Tag 064A in the Stacks Project.

CochainComplex.IsKProjective.nonempty_homotopy_of_comp_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/KProjective.lean, line 290.

Stacks 064A. Let A be an abelian category, let α : L ⟶ K be a quasi-isomorphism of cochain complexes in A and let P be a K-projective cochain complex — for instance one which is bounded above and consists of projective objects, by CochainComplex.isKProjective_of_projective. Then two morphisms β₁, β₂ : P ⟶ L whose composites with α are homotopic are themselves homotopic; in particular a lift of a given γ : P ⟶ K through α up to homotopy is unique up to homotopy.

public theorem CochainComplex.IsKProjective.nonempty_homotopy_of_comp_quasiIso {A : Type u}
    [Category.{v} A] [Abelian A] {P K L : CochainComplex A ℤ} [P.IsKProjective] (α : L ⟶ K)
    [QuasiIso α] {β₁ β₂ : P ⟶ L} (h : Homotopy (β₁ ≫ α) (β₂ ≫ α)) :
    Nonempty (Homotopy β₁ β₂)

Tag 064B, a lemma

Tag 064B in the Stacks Project.

CochainComplex.isKProjective_iff_Qh_map_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/KProjective.lean, line 324.

Stacks 064B. Let A be an abelian category and let P be a cochain complex in A. Then P is K-projective — which a bounded above complex of projective objects is, by CochainComplex.isKProjective_of_projective — if and only if for every object L of the homotopy category K(A) the localization functor Qh : K(A) ⥤ D(A) induces a bijection Mor_{K(A)}(P, L) → Mor_{D(A)}(P, L). The Stacks lemma is the forward implication.

public theorem CochainComplex.isKProjective_iff_Qh_map_bijective {A : Type u} [Category.{v} A]
    [Abelian A] [HasDerivedCategory.{w} A] (P : CochainComplex A ℤ) :
    P.IsKProjective ↔ ∀ L : HomotopyCategory A (ComplexShape.up ℤ),
      Function.Bijective (DerivedCategory.Qh.map :
        ((HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj P ⟶ L) → _)

Tag 064C, a lemma

Tag 064C in the Stacks Project.

CochainComplex.exists_shortExact_isProjectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/KProjective.lean, line 682.

Let C be an abelian category with enough projectives, let S : 0 ⟶ S.X₁ ⟶ S.X₂ ⟶ S.X₃ ⟶ 0 be a short exact sequence of cochain complexes of C with S.X₁ bounded above, and let π : P ⟶ S.X₃ be a projective resolution. Then there is a short exact sequence of complexes 0 ⟶ P₁ ⟶ P₂ ⟶ P ⟶ 0 mapping to S, with π as its third component, whose first two components π₁ : P₁ ⟶ S.X₁ and π₂ : P₂ ⟶ S.X₂ are projective resolutions as well.

public theorem exists_shortExact_isProjectiveResolution
    [EnoughProjectives C] (S : ShortComplex (CochainComplex C ℤ)) (hS : S.ShortExact)
    (n : ℤ) [S.X₁.IsStrictlyLE n] {P : CochainComplex C ℤ} (π : P ⟶ S.X₃)
    [IsProjectiveResolution π] :
    ∃ (P₁ P₂ : CochainComplex C ℤ) (i : P₁ ⟶ P₂) (p : P₂ ⟶ P) (hip : i ≫ p = 0)
      (π₁ : P₁ ⟶ S.X₁) (π₂ : P₂ ⟶ S.X₂),
      (ShortComplex.mk i p hip).ShortExact ∧ IsProjectiveResolution π₁ ∧
        IsProjectiveResolution π₂ ∧ i ≫ π₂ = π₁ ≫ S.f ∧ p ≫ π = π₂ ≫ S.g

Tag 064D, a lemma

Tag 064D in the Stacks Project.

CochainComplex.IsKProjective.hom_eq_zero_of_isStrictlyGE_of_isLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/KProjective.lean, line 423.

Stacks 064D. Let A be an abelian category, let P be a K-projective cochain complex of A with P^i = 0 for i < n — for instance a bounded complex of projective objects with that property, by CochainComplex.isKProjective_of_projective — and let K be a cochain complex with H^i(K) = 0 for i > m, where m < n. Then Mor_{K(A)}(P, K) = Mor_{D(A)}(P, K) = 0: every morphism from P to K in the homotopy category, and every morphism from P to K in the derived category, is zero.

public theorem CochainComplex.IsKProjective.hom_eq_zero_of_isStrictlyGE_of_isLE {A : Type u}
    [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A] (P K : CochainComplex A ℤ)
    [P.IsKProjective] (n : ℤ) [P.IsStrictlyGE n] (m : ℤ) (hmn : m < n) [K.IsLE m] :
    (∀ f : (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj P ⟶
      (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj K, f = 0) ∧
      (∀ f : DerivedCategory.Q.obj P ⟶ DerivedCategory.Q.obj K, f = 0)

Tag 064E, a lemma

Tag 064E in the Stacks Project.

exists_lift_homotopy_of_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/ProjectiveResolution/HomotopyLift.lean, line 592. References: SGA 6 II (1.1), “c), special case”.

Stacks Tag 064E. Let β : P^• → L^• and α : E^• → L^• be maps of cochain complexes in an abelian category A, and n : ℤ. Assume P^• is a bounded complex of projectives with P^i = 0 for i < n, and that H^i(α) is an isomorphism for i > n and an epimorphism for i = n. Then there is a chain map γ : P^• → E^• with α ∘ γ homotopic to β.

theorem exists_lift_homotopy_of_projective (P E L : CochainComplex A ℤ)
    (β : P ⟶ L) (α : E ⟶ L) (n : ℤ)
    (hProj : ∀ i, Projective (P.X i))
    (hBddAbove : ∃ b : ℤ, ∀ i, b < i → IsZero (P.X i))
    (hBelow : ∀ i, i < n → IsZero (P.X i))
    (hIso : ∀ i, n < i → IsIso (HomologicalComplex.homologyMap α i))
    (hEpi : Epi (HomologicalComplex.homologyMap α n)) :
    ∃ γ : P ⟶ E, Nonempty (Homotopy (γ ≫ α) β)

Sources

LeanCochainComplex.IsProjectiveResolution · Stacks.ProjectiveResolution.CohomologyVanishing.cohomology_vanishes_of_isProjectiveResolution · Stacks.ProjectiveResolution.CohomologyVanishing.exists_boundedAbove_quasiIso_of_cohomologyVanishes · ProjectiveResolutionLemma.statement3 · ProjectiveResolutionLemma.statement2 · ProjectiveResolutionLemma.statement1 · projective_into_acyclic_is_zero · bijective_postcomp_quotient_map

Section13.20 Right derived functors and injective resolutions #

Section 13.20 of the Stacks Project, Tag 0156. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05TH, a lemma

Tag 05TH in the Stacks Project.

HomotopyCategory.Plus.hasPointwiseRightDerivedFunctorAt_of_injective, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/RightDerivedFunctorInjective/Exactness.lean, line 277. The attribute's comment: “part (1): RF is defined at a bounded below complex of injectives”.

Stacks 05TH, part (1), first half. Let K be a bounded below complex of injective objects of an abelian category C. Then the right derived functor of any functor F : K⁺(C) ⥤ H relative to the quasi-isomorphisms of K⁺(C) is defined at K, i.e. the pointwise left Kan extension of F along a localization of K⁺(C) at the quasi-isomorphisms exists at the image of K.

If C has enough injectives, this holds for every K; the content here is that termwise injectivity of K suffices.

public instance hasPointwiseRightDerivedFunctorAt_of_injective {H : Type u₃} [Category.{v₃} H]
    (F : HomotopyCategory.Plus C ⥤ H) (K : HomotopyCategory.Plus C)
    [∀ n : ℤ, Injective (K.obj.as.X n)] :
    F.HasPointwiseRightDerivedFunctorAt (HomotopyCategory.Plus.quasiIso C) K

Tag 05TI, a lemma

Tag 05TI in the Stacks Project.

hasPointwiseRightDerivedFunctor_of_isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean, line 470. The attribute's comment: “(1)”. References: SGA 4 XVII (1.2.7), “enough injectives (RF)”.

Statement 1 (Stacks Tag 05TI, part 1). Let A be an abelian category with enough injectives. For every triangulated category D and every exact (triangulated) functor F : K^{+}(A) ⥤ D, the right derived functor RF : D^{+}(A) ⥤ D of F with respect to the quasi-isomorphisms is everywhere defined.

theorem hasPointwiseRightDerivedFunctor_of_isTriangulated {A : Type*} [Category A] [Abelian A]
  [EnoughInjectives A]
    {D : Type*} [Category D] [HasZeroObject D] [HasShift D ℤ] [Preadditive D]
    [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D]
    (F : HomotopyCategory.Plus A ⥤ D) [F.CommShift ℤ] [F.IsTriangulated] :
    F.HasPointwiseRightDerivedFunctor (HomotopyCategory.Plus.quasiIso A)

hasPointwiseRightDerivedFunctor_mapPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean, line 487. The attribute's comment: “(2)”. References: EGA 0 (13.6.1), “existence of R^pT”; SGA 4 XVII (1.2.7), “enough injectives (RF)”.

Statement 2 (Stacks Tag 05TI, part 2). Let A be an abelian category with enough injectives. For every abelian category B and every additive functor F : A ⥤ B, the right derived functor RF : D^{+}(A) ⥤ D^{+}(B) of the composite K^{+}(F) ⋙ Q^{+}_{B} : K^{+}(A) ⥤ D^{+}(B) is everywhere defined.

theorem hasPointwiseRightDerivedFunctor_mapPlus {A B : Type*} [Category A] [Abelian A]
  [EnoughInjectives A]
    [Category B] [Abelian B]
    (F : A ⥤ B) [F.Additive] :
    (mapPlus F ⋙ (HomotopyCategory.Plus.quasiIso B).Q).HasPointwiseRightDerivedFunctor
      (HomotopyCategory.Plus.quasiIso A)

Tag 0159, a lemma

Tag 0159 in the Stacks Project.

CategoryTheory.Functor.isTriangulated_of_isRightDerivedFunctor_mapHomotopyCategoryPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/RightDerivedFunctorInjective/Exactness.lean, line 347. The attribute's comment: “part (1)”. References: SGA 4 XVII (1.2.2), “(ii), special case”.

Stacks 0159, part (1). Let F : 𝒜 ⥤ ℬ be an additive functor between abelian categories, where 𝒜 has enough injectives. Then any right derived functor RF : D⁺(𝒜) ⥤ D⁺(ℬ) of K⁺(F) ⋙ Q⁺_ℬ along the localization Q⁺_𝒜 : K⁺(𝒜) ⥤ D⁺(𝒜) at the quasi-isomorphisms, with unit α, is an exact functor of triangulated categories.

The source's RF is the case RF := F.rightDerivedFunctorPlus and α := F.rightDerivedFunctorPlusUnith, with the commutation with the shift induced by the universal property. The induced exact functor K⁺(𝒜) ⥤ D⁺(ℬ) of part (2) is then DerivedCategory.Plus.Qh ⋙ RF.

public theorem isTriangulated_of_isRightDerivedFunctor_mapHomotopyCategoryPlus
    [RF.IsRightDerivedFunctor α (HomotopyCategory.Plus.quasiIso C)]
    [RF.CommShift ℤ] [NatTrans.CommShift α ℤ] :
    RF.IsTriangulated

Tag 015B, a lemma

Tag 015B in the Stacks Project.

CategoryTheory.Functor.isZero_rightDerivedPlus_obj_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/RightDerivedFunctorInjective/Exactness.lean, line 446. The attribute's comment: “part (3), for i ≠ 0 and an arbitrary additive functor”. References: EGA 0 (17.2.2), “(ii), special case”.

Injective objects are right acyclic, [Stacks, Tag 015B] part (3): if F : 𝒜 ⥤ ℬ is an additive functor between abelian categories, 𝒜 has enough injectives and I is an injective object of 𝒜, then the higher right derived functors of F vanish on I outside degree 0: R ⁱ F (I) = 0 for i ≠ 0.

The source states this for i > 0 and a left exact F; neither restriction is needed, as RF(I[0]) is F(I)[0].

public theorem isZero_rightDerivedPlus_obj_injective {A B : Type*} [Category* A] [Category* B]
    [Abelian A] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B]
    (F : A ⥤ B) [F.Additive] [EnoughInjectives A] (i : ℤ) (hi : i ≠ 0) (I : A) [Injective I] :
    IsZero ((F.rightDerivedPlus i).obj I)

Sources

LeanHomotopyCategory.Plus.hasPointwiseRightDerivedFunctorAt_of_injective · hasPointwiseRightDerivedFunctor_of_isTriangulated · hasPointwiseRightDerivedFunctor_mapPlus · CategoryTheory.Functor.isTriangulated_of_isRightDerivedFunctor_mapHomotopyCategoryPlus · CategoryTheory.Functor.isZero_rightDerivedPlus_obj_injective

Section13.21 Cartan-Eilenberg resolutions #

Section 13.21 of the Stacks Project, Tag 015G. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 015H, a definition

Tag 015H in the Stacks Project.

CochainComplex.CartanEilenbergResolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/CartanEilenbergResolutions/Basic.lean, line 52. References: EGA 0 (11.4.2), “injective, bdd below”.

A Cartan-Eilenberg resolution of a cochain complex K in an abelian category: a double complex I of injective objects, vanishing in first degrees ≪ 0 and in negative second degrees, together with an augmentation ε from K placed in second degree 0, such that the complexes I^{p,•}, Ker(d₁^{p,•}), Im(d₁^{p,•}) and H^p_I(I^{•,•}) are injective resolutions of K^p, Ker(d_K^p), Im(d_K^p) and H^p(K^•).

public structure CartanEilenbergResolution (K : CochainComplex C ℤ)

Tag 015I, a lemma

Tag 015I in the Stacks Project.

CochainComplex.exists_cartanEilenbergResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/CartanEilenbergResolutions/SpectralSequence.lean, line 749. References: EGA 0 (11.4.2), “bounded below case”; SGA 2 VIII (1.4), “existence of resolution”.

Existence of Cartan-Eilenberg resolutions. A cochain complex K over an abelian category with enough injectives which is strictly ≥ n admits a Cartan-Eilenberg resolution whose double complex is strictly ≥ n in the first direction.

public theorem _root_.CochainComplex.exists_cartanEilenbergResolution {C : Type u}
    [Category.{v} C] [Abelian C] [EnoughInjectives C] (K : CochainComplex C ℤ) (n : ℤ)
    [CochainComplex.IsStrictlyGE K n] :
    ∃ I : CochainComplex.CartanEilenbergResolution K,
      CochainComplex.IsStrictlyGE I.bicomplex n

Tag 015J, a lemma

Tag 015J in the Stacks Project.

CochainComplex.CartanEilenbergResolution.exists_homologyIso_rightDerivedPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/CartanEilenbergResolutions/SpectralSequence.lean, line 768. References: EGA 0 (11.4.3), “bounded below case”; EGA 0 (12.4.1), “bounded below complexes”; EGA 0 (12.1.7), “partial”.

The spectral sequences of a Cartan-Eilenberg resolution. Let F : 𝒜 ⥤ ℬ be an additive functor of abelian categories, with 𝒜 having enough injectives, let K be a bounded below cochain complex of 𝒜 and let I be a Cartan-Eilenberg resolution of K. For the double complex L = F(I): the 'E₁-page H^q(L^{p,•}) is the complex R^qF(K^p) in p, with differential induced by that of K; the ''E₂-page H^p_{II}(H^q_I(L^{•,•})) is R^pF(H^q(K^•)); and H^n(Tot(L)) is H^n(RF(K^•)), the abutment of both spectral sequences.

public theorem _root_.CochainComplex.CartanEilenbergResolution.exists_homologyIso_rightDerivedPlus
    {A : Type u} {B : Type u'} [Category.{v} A] [Category.{v'} B] [Abelian A] [Abelian B]
    [HasDerivedCategory.{w} A] [HasDerivedCategory.{w'} B] (F : A ⥤ B) [F.Additive]
    [EnoughInjectives A] {K : CochainComplex A ℤ} (hK : CochainComplex.plus A K)
    (I : K.CartanEilenbergResolution)
    [HomologicalComplex₂.HasTotal
      (((F.mapHomologicalComplex (ComplexShape.up ℤ)).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj I.bicomplex) (ComplexShape.up ℤ)] :
    (∀ q, ∃ e : ∀ p, ((((F.mapHomologicalComplex (ComplexShape.up ℤ)).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj I.bicomplex).X p).homology q ≅
          (F.rightDerivedPlus q).obj (K.X p),
      ∀ p p', homologyMap ((((F.mapHomologicalComplex (ComplexShape.up ℤ)).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj I.bicomplex).d p p') q ≫ (e p').hom =
          (e p).hom ≫ (F.rightDerivedPlus q).map (K.d p p')) ∧
    (∀ p q, Nonempty (((((F.mapHomologicalComplex (ComplexShape.up ℤ)).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj I.bicomplex).homology q).homology p ≅
          (F.rightDerivedPlus p).obj (K.homology q))) ∧
    (∀ n, Nonempty ((HomologicalComplex₂.total
        (((F.mapHomologicalComplex (ComplexShape.up ℤ)).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj I.bicomplex) (ComplexShape.up ℤ)).homology n ≅
          (DerivedCategory.Plus.homologyFunctor B n).obj
            (F.rightDerivedFunctorPlus.obj (DerivedCategory.Plus.Q.obj ⟨K, hK⟩))))

Sources

LeanCochainComplex.CartanEilenbergResolution · CochainComplex.exists_cartanEilenbergResolution · CochainComplex.CartanEilenbergResolution.exists_homologyIso_rightDerivedPlus

Section13.22 Composition of right derived functors #

Section 13.22 of the Stacks Project, Tag 015L. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 015M, a lemma

Tag 015M in the Stacks Project.

CategoryTheory.Functor.isIso_iff_rightAcyclic_obj_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/CompositionOfRightDerivedFunctors.lean, line 205. References: SGA 4½ Etat 0 (4.3.1), “enough injectives”.

Let F : 𝒜 ⥤ ℬ and G : ℬ ⥤ 𝒞 be additive functors between abelian categories, with 𝒜 and ℬ having enough injectives. The canonical transformation t : R(G ∘ F) ⟶ RG ∘ RF of functors D⁺(𝒜) ⥤ D⁺(𝒞), namely the unique one whose composite with the unit of R(G ∘ F) is the transformation G(F(K)) ⟶ RG(F(K)) ⟶ RG(RF(K)) built from the units of RG and of RF (the hypothesis ht), is an isomorphism if and only if F(I) is right acyclic for G for every injective object I of 𝒜.

public theorem isIso_iff_rightAcyclic_obj_injective (F : C ⥤ D) (G : D ⥤ E)
    [F.Additive] [G.Additive] [EnoughInjectives C] [EnoughInjectives D]
    (t : (F ⋙ G).rightDerivedFunctorPlus ⟶
      F.rightDerivedFunctorPlus ⋙ G.rightDerivedFunctorPlus)
    (ht : (F ⋙ G).rightDerivedFunctorPlusUnith ≫ whiskerLeft DerivedCategory.Plus.Qh t =
      whiskerRight (mapHomotopyCategoryPlusCompIso (Iso.refl (F ⋙ G))).inv
          DerivedCategory.Plus.Qh ≫
        whiskerLeft F.mapHomotopyCategoryPlus G.rightDerivedFunctorPlusUnith ≫
        whiskerRight F.rightDerivedFunctorPlusUnith G.rightDerivedFunctorPlus) :
    IsIso t ↔ ∀ I : C, Injective I → G.rightAcyclic (F.obj I)

Tag 015N, a lemma

Tag 015N in the Stacks Project.

CategoryTheory.Functor.exists_spectralSequence_rightDerivedFunctorPlus_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Grothendieck.lean, line 72. References: SGA 4 V (0.3), “(ii) ⇒ (i)”; SGA 4 VII (1.5), “more general”; SGA 4½ Arcata (2.3.3), “more general”; SGA 4½ Arcata (2.3.4), “more general”.

The Grothendieck spectral sequence. Let F : 𝒜 ⥤ ℬ and G : ℬ ⥤ 𝒞 be additive functors between abelian categories, with 𝒜 and ℬ having enough injectives, such that F(I) is right acyclic for G for every injective object I of 𝒜, and let X be an object of D⁺(𝒜). There is a filtered complex K of 𝒞 with H^n(K) ≅ H^n(R(G ∘ F)(X)) for all n, whose filtration is finite in each degree and whose spectral sequence E, presented by its pages Z_r^{p,q}/D_r^{p,q}, has E_2^{p,q} ≅ R^pG(H^q(RF(X))), is bounded, induces a finite filtration on each H^n(K), and converges to H^*(K).

theorem exists_spectralSequence_rightDerivedFunctorPlus_comp (F : A ⥤ B) (G : B ⥤ C)
    [F.Additive] [G.Additive] [EnoughInjectives A] [EnoughInjectives B]
    (hFG : ∀ I : A, Injective I → G.rightAcyclic (F.obj I)) (X : DerivedCategory.Plus A) :
    ∃ K : FilteredObject (CochainComplex C ℤ) ℤᵒᵖ,
      (∀ n : ℤ, Nonempty (K.X.homology n ≅
        (DerivedCategory.Plus.homologyFunctor C n).obj
          ((F ⋙ G).rightDerivedFunctorPlus.obj X))) ∧
      K.filtration.IsDegreewiseFinite ∧
      ∀ (Fil : ∀ (_p n : ℤ), Subobject (K.X.X n))
        (_ : ∀ p n : ℤ, Fil p n = Subobject.mk ((K.filtration.ι.app (op p)).f n))
        (Z : ∀ (_r _p n : ℤ), Subobject (K.X.X n))
        (_ : ∀ r p n : ℤ, Z r p n =
          Fil p n ⊓ (Subobject.pullback (K.X.d n (n + 1))).obj (Fil (p + r) (n + 1)))
        (D : ∀ (_r _p n : ℤ), Subobject (K.X.X n))
        (_ : ∀ r p n : ℤ, D r p n = Z (r - 1) (p + 1) n ⊔
          (Subobject.«exists» (K.X.d (n - 1) n)).obj (Z (r - 1) (p - r + 1) (n - 1)))
        (FH : ∀ (n _p : ℤ), Subobject (K.X.homology n))
        (_ : ∀ n p : ℤ, FH n p =
          imageSubobject (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n)),
      ∃ (E : CohomologicalSpectralSequence C 0)
        (_ : ∀ (r p q n : ℤ) (hr : 0 ≤ r) (_ : n = p + q), (E.page r hr).X (p, q) ≅
          cokernel (Subobject.ofLE _ _ (inf_le_right : D r p n ⊓ Z r p n ≤ Z r p n))),
        (∀ p q : ℤ, Nonempty ((E.page 2 zero_le_two).X (p, q) ≅
          (G.rightDerivedPlus p).obj
            ((DerivedCategory.Plus.homologyFunctor B q).obj (F.rightDerivedFunctorPlus.obj X)))) ∧
        (∀ n : ℤ, {p : ℤ | ¬ IsZero ((E.page 0).X (p, n - p))}.Finite) ∧
        (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ FH n a = ⊤ ∧ FH n b = ⊥) ∧
        (∀ p q : ℤ, ∃ b : ℤ, ∀ (r : ℤ) (hr : 0 ≤ r), b ≤ r →
          (E.page r hr).d (p, q) (p + r, q - r + 1) = 0) ∧
        (∀ p n : ℤ,
          IsGLB (Set.range fun r : ℕ =>
              Fil p n ⊓ (Subobject.pullback (K.X.d n (n + 1))).obj (Fil (p + r) (n + 1)) ⊔
                Fil (p + 1) n)
            (kernelSubobject (K.X.d n (n + 1)) ⊓ Fil p n ⊔ Fil (p + 1) n) ∧
          IsLUB (Set.range fun r : ℕ =>
              Fil p n ⊓ (Subobject.«exists» (K.X.d (n - 1) n)).obj (Fil (p - r) (n - 1)) ⊔
                Fil (p + 1) n)
            (imageSubobject (K.X.d (n - 1) n) ⊓ Fil p n ⊔ Fil (p + 1) n))

Sources

LeanCategoryTheory.Functor.isIso_iff_rightAcyclic_obj_injective · CategoryTheory.Functor.exists_spectralSequence_rightDerivedFunctorPlus_comp

Section13.23 Resolution functors #

Section 13.23 of the Stacks Project, Tag 013U. 6 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 013V, a proposition

Tag 013V in the Stacks Project.

qhPlus_isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 1031. The attribute's comment: “(exactness)”.

(Claim 1: Exactness.) The functor of Definition 6 is exact, i.e. it is a triangulated functor: it commutes with the shift (the CommShift ℤ structure on QhPlus A) and sends distinguished triangles of K^+(I) to distinguished triangles of D^+(A).

theorem qhPlus_isTriangulated [HasDerivedCategory A] :
    (QhPlus A).IsTriangulated

qhPlus_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 1195. References: SGA 4½ Etat 0 (3.1.4), “the equivalence”.

(Main theorem, Stacks 013V.) The canonical functor K^+(I) → D^+(A) of Definition 6 is an equivalence of categories. Combined with exactness (qhPlus_isTriangulated) this exhibits it as an equivalence of triangulated categories.

theorem qhPlus_isEquivalence [EnoughInjectives A] [HasDerivedCategory A] :
    (QhPlus A).IsEquivalence

Tag 013W, a definition

Tag 013W in the Stacks Project.

HomotopyCategory.Plus.ResolutionFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 187.

A resolution functor for an abelian category C is the data of a bounded below complex of injectives (j K).X₁, i.e. an object of K⁺(ℐ), for every object K of K⁺(C), together with a quasi-isomorphism (j K).w : K ⟶ (j K).X₁ in K⁺(C): that is, of a right resolution of every K for the inclusion K⁺(ℐ) ⥤ K⁺(C). (Functoriality of K ↦ (j K).X₁ is automatic, see [Stacks, Tag 05TJ].)

public abbrev ResolutionFunctor

Tag 05TJ, a lemma

Tag 05TJ in the Stacks Project.

HomotopyCategory.Plus.existsUnique_functor_of_resolutionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 395.

Let C be an abelian category, ℐ ⊆ C its full additive subcategory of injective objects, and let j be a resolution functor for C, i.e. a right resolution (j K).w : K ⟶ (j K).X₁ in K⁺(ℐ) of every object K of K⁺(C). Then there is a unique way to make K ↦ (j K).X₁ into a functor F : K⁺(C) ⥤ K⁺(ℐ) for which the comparison maps (j K).w form a natural transformation 𝟭 K⁺(C) ⟶ F ⋙ (K⁺(ℐ) ⥤ K⁺(C)); the latter is then a 2-isomorphism over D⁺(C), since its components are quasi-isomorphisms.

public theorem existsUnique_functor_of_resolutionFunctor (j : ResolutionFunctor C) :
    ∃! F : HomotopyCategory.Plus C ⥤ HomotopyCategory.Plus (InjectiveObject C),
      ∃ (α : 𝟭 (HomotopyCategory.Plus C) ⟶ F ⋙ (localizerMorphism C).functor)
        (hα : ∀ K, quasiIso C (α.app K)),
        ∀ K, LocalizerMorphism.RightResolution.mk (α.app K) (hα K) = j K

Tag 013X, a lemma

Tag 013X in the Stacks Project.

HomotopyCategory.Plus.nonempty_resolutionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 306. The attribute's comment: “T_013X, existence: a resolution functor exists when C has enough injectives”. References: SGA 4½ Etat 0 (3.2.3), “(4) existence”.

Let C be an abelian category with enough injectives. Then a resolution functor for C exists ([Stacks, Tag 013W]): every object K of K⁺(C) admits a bounded below complex of injectives (j K).X₁ together with a quasi-isomorphism (j K).w : K ⟶ (j K).X₁ in K⁺(C).

public theorem nonempty_resolutionFunctor (C : Type*) [Category C] [Abelian C]
    [EnoughInjectives C] :
    Nonempty (HomotopyCategory.Plus.ResolutionFunctor C)

HomotopyCategory.Plus.nonempty_isTerminal_rightResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 334. The attribute's comment: “T_013X, uniqueness up to unique isomorphism; no hypothesis on C”. References: SGA 4½ Etat 0 (3.2.3), “(4) uniqueness”.

Let C be an abelian category. A right resolution of an object K of K⁺(C) is unique up to unique isomorphism: every right resolution R of K is a terminal object of the category (localizerMorphism C).RightResolution K of right resolutions of K, in which a morphism R' ⟶ R is a morphism f : R'.X₁ ⟶ R.X₁ of K⁺(ℐ) with R'.w ≫ f = R.w in K⁺(C). So any two right resolutions of K are related by exactly one morphism compatible with their comparison maps, and every such morphism is an isomorphism; applied to two resolution functors this is the uniqueness up to unique isomorphism of [Stacks, Tag 013X], and it needs no hypothesis on C beyond Abelian C.

public theorem nonempty_isTerminal_rightResolution (C : Type*) [Category C] [Abelian C]
    {K : HomotopyCategory.Plus C} (R : (localizerMorphism C).RightResolution K) :
    Nonempty (IsTerminal R)

Tag 014W, a lemma

Tag 014W in the Stacks Project.

HomotopyCategory.Plus.commShiftOfQuasiIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 542. The attribute's comment: “the commutation with the shift itself; commShiftOfQuasiIso_compatibility is its compatibility with the comparison maps and eq_commShiftOfQuasiIso its uniqueness”.

The commutation of a resolution functor with the shift, the source's ξ: its component at a and K is the unique ξ_K : F(K⟦a⟧) ⟶ (F K)⟦a⟧ with α_{K⟦a⟧} ≫ ι ξ_K = (α_K)⟦a⟧. It is the only commutation compatible with α (commShiftOfQuasiIso_compatibility, eq_commShiftOfQuasiIso), and F is exact for it (isTriangulated_of_quasiIso).

noncomputable def commShiftOfQuasiIso : F.CommShift ℤ

HomotopyCategory.Plus.commShiftOfQuasiIso_compatibility, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 572. The attribute's comment: “the commutation is compatible with the comparison maps”.

commShiftOfQuasiIso is compatible with the comparison maps α: each of its components satisfies α_{K⟦a⟧} ≫ ι ξ_K = (α_K)⟦a⟧.

lemma commShiftOfQuasiIso_compatibility :
    letI := commShiftOfQuasiIso F α hα
    NatTrans.CommShift α ℤ

HomotopyCategory.Plus.eq_commShiftOfQuasiIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 582. The attribute's comment: “uniqueness of the commutation compatible with the comparison maps”.

Uniqueness of the source's ξ: a commutation of F with the shift which is compatible with the comparison maps α has ξ for each of its components, hence is commShiftOfQuasiIso.

lemma eq_commShiftOfQuasiIso :
    ∀ h : F.CommShift ℤ, (letI := h; NatTrans.CommShift α ℤ) →
      h = commShiftOfQuasiIso F α hα

HomotopyCategory.Plus.isTriangulated_of_quasiIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 594. The attribute's comment: “a resolution functor is exact”.

A resolution functor is exact: it carries distinguished triangles of K⁺(C) to distinguished triangles of K⁺(ℐ), for its commutation with the shift.

lemma isTriangulated_of_quasiIso :
    letI := commShiftOfQuasiIso F α hα
    F.IsTriangulated

Tag 05TK, a lemma

Tag 05TK in the Stacks Project.

HomotopyCategory.Plus.exists_equivalence_and_existsUnique_lift_of_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 729.

Let C be an abelian category, ℐ ⊆ C its full additive subcategory of injective objects, and let F : K⁺(C) ⥤ K⁺(ℐ) be a functor equipped with comparison maps α.app K : K ⟶ F K in K⁺(C) that are quasi-isomorphisms, i.e. the functorial form of a resolution functor ([Stacks, Tags 013W, 05TJ]). Then F factors through the localization Q : K⁺(C) ⥤ D⁺(C) by a functor which is quasi-inverse to the canonical functor K⁺(ℐ) ⥤ D⁺(C), and the factorization is unique up to a unique natural transformation over F.

public theorem exists_equivalence_and_existsUnique_lift_of_quasiIso
    (F : HomotopyCategory.Plus C ⥤ HomotopyCategory.Plus (InjectiveObject C))
    (α : 𝟭 (HomotopyCategory.Plus C) ⟶ F ⋙ (localizerMorphism C).functor)
    (hα : ∀ K, quasiIso C (α.app K)) :
    (∃ e : DerivedCategory.Plus C ≌ HomotopyCategory.Plus (InjectiveObject C),
      e.inverse = (localizerMorphism C).functor ⋙ DerivedCategory.Plus.Qh ∧
        Nonempty (DerivedCategory.Plus.Qh ⋙ e.functor ≅ F)) ∧
    ∀ (j₁ j₂ : DerivedCategory.Plus C ⥤ HomotopyCategory.Plus (InjectiveObject C))
      (e₁ : DerivedCategory.Plus.Qh ⋙ j₁ ≅ F) (e₂ : DerivedCategory.Plus.Qh ⋙ j₂ ≅ F),
      ∃! τ : j₁ ⟶ j₂,
        Functor.whiskerLeft DerivedCategory.Plus.Qh τ = e₁.hom ≫ e₂.inv

Sources

LeanqhPlus_isTriangulated · qhPlus_isEquivalence · HomotopyCategory.Plus.ResolutionFunctor · HomotopyCategory.Plus.existsUnique_functor_of_resolutionFunctor · HomotopyCategory.Plus.nonempty_resolutionFunctor · HomotopyCategory.Plus.nonempty_isTerminal_rightResolution · HomotopyCategory.Plus.commShiftOfQuasiIso · HomotopyCategory.Plus.commShiftOfQuasiIso_compatibility

Section13.24 Functorial injective embeddings and resolution functors #

Section 13.24 of the Stacks Project, Tag 0140. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0141, a lemma

Tag 0141 in the Stacks Project.

CochainComplex.Plus.exists_functorial_injective_resolution_and_exists_resolutionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/FunctorialInjectiveResolution.lean, line 1040.

Let C be an abelian category.

(1) If C has functorial injective embeddings, i.e. is equipped with a functor J : C ⥤ ℐ to the full subcategory of injective objects and a natural transformation η : 𝟭 C ⟶ J with monomorphic components ([Stacks, Tag 0139]), then there is a functor F : Comp⁺(C) ⥤ Comp⁺(ℐ) on bounded below cochain complexes and a natural transformation α : 𝟭 ⟶ F ⋙ ι whose components are quasi-isomorphisms, i.e. a functorial injective resolution of bounded below complexes.

(2) Any such pair (F, α) — over an arbitrary abelian C — induces a resolution functor for C ([Stacks, Tag 013W]), namely the one whose value at K is the image of F K in K⁺(ℐ) and whose comparison map is the homotopy class of α_K.

public theorem exists_functorial_injective_resolution_and_exists_resolutionFunctor :
    (∀ (J : C ⥤ InjectiveObject C) (η : 𝟭 C ⟶ J ⋙ InjectiveObject.ι C),
        (∀ A, Mono (η.app A)) →
        ∃ (F : CochainComplex.Plus C ⥤ CochainComplex.Plus (InjectiveObject C))
          (α : 𝟭 (CochainComplex.Plus C) ⟶ F ⋙ (InjectiveObject.ι C).mapCochainComplexPlus),
          ∀ K, CochainComplex.Plus.quasiIso C (α.app K)) ∧
      ∀ (F : CochainComplex.Plus C ⥤ CochainComplex.Plus (InjectiveObject C))
        (α : 𝟭 (CochainComplex.Plus C) ⟶ F ⋙ (InjectiveObject.ι C).mapCochainComplexPlus),
        (∀ K, CochainComplex.Plus.quasiIso C (α.app K)) →
        ∃ R : HomotopyCategory.Plus.ResolutionFunctor C,
          ∀ K : CochainComplex.Plus C,
            ∃ h : (R ((HomotopyCategory.Plus.quotient C).obj K)).X₁ =
                (HomotopyCategory.Plus.quotient (InjectiveObject C)).obj (F.obj K),
              (R ((HomotopyCategory.Plus.quotient C).obj K)).w =
                (HomotopyCategory.Plus.quotient C).map (α.app K) ≫
                  eqToHom (congrArg (InjectiveObject.ι C).mapHomotopyCategoryPlus.obj h.symm)

Sources

LeanCochainComplex.Plus.exists_functorial_injective_resolution_and_exists_resolutionFunctor

Section13.25 Right derived functors via resolution functors #

Section 13.25 of the Stacks Project, Tag 05TM. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05TN, a lemma

Tag 05TN in the Stacks Project.

CategoryTheory.Functor.exists_iso_rightDerivedFunctorPlus_of_comp_Qh_iso_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/ResolutionFunctor.lean, line 1292.

Let F : C ⥤ D be an additive functor between abelian categories with C having enough injectives, let ℐ ⊆ C be the subcategory of injective objects, and let j' : D⁺(C) ⥤ K⁺(ℐ) be a section up to isomorphism of the canonical functor K⁺(ℐ) ⥤ D⁺(C), i.e. the descent of a resolution functor ([Stacks, Tags 013W, 05TK]). Then the right derived functor RF of F is computed by F ∘ j': the triangle D⁺(C) ⥤ K⁺(ℐ) ⥤ D⁺(D), RF is 2-commutative, by the 2-isomorphism whose value at X is the unit of RF at the complex of injectives j' X followed by RF applied to ε.hom.app X.

public theorem exists_iso_rightDerivedFunctorPlus_of_comp_Qh_iso_id
    (F : C ⥤ D) [F.Additive] [EnoughInjectives C]
    (j' : DerivedCategory.Plus C ⥤ HomotopyCategory.Plus (InjectiveObject C))
    (ε : j' ⋙ (HomotopyCategory.Plus.localizerMorphism C).functor ⋙ DerivedCategory.Plus.Qh ≅
      𝟭 (DerivedCategory.Plus C)) :
    ∃ e : j' ⋙ (HomotopyCategory.Plus.localizerMorphism C).functor ⋙
        F.mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh ≅ F.rightDerivedFunctorPlus,
      ∀ X, e.hom.app X = F.rightDerivedFunctorPlusUnith.app
        ((HomotopyCategory.Plus.localizerMorphism C).functor.obj (j'.obj X)) ≫
          F.rightDerivedFunctorPlus.map (ε.hom.app X)

Sources

LeanCategoryTheory.Functor.exists_iso_rightDerivedFunctorPlus_of_comp_Qh_iso_id

Section13.26 Filtered derived category and injective resolutions #

Section 13.26 of the Stacks Project, Tag 015O. 15 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 015P, a definition

Tag 015P in the Stacks Project.

CategoryTheory.FilteredObject.IsFilteredInjective, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/Defs.lean, line 243.

An object I of Fil^f(C) is filtered injective if each graded piece gr^p(I) = F^p I / F^{p + 1} I is an injective object of C. As a property of a filtered object of C, it records that I lies in Fil^f(C), i.e. that its filtration is finite.

public structure FilteredObject.IsFilteredInjective {C : Type u} [Category.{v} C]
    [HasZeroMorphisms C] [HasCokernels C] (I : FilteredObject C ℤᵒᵖ) : Prop

Tag 05TP, a lemma

Tag 05TP in the Stacks Project.

CategoryTheory.FilteredObject.isFilteredInjective_iff_nonempty_iso_stdBiprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/InjectiveObject.lean, line 758.

Let 𝒜 be an abelian category. An object I of Fil^f(𝒜) is filtered injective if and only if there are integers a ≤ b, injective objects I_n of 𝒜 and an isomorphism I ≅ ⨁_{a ≤ n ≤ b} I_n of filtered objects, where the right-hand side carries the filtration F^p = ⨁_{n ≥ p} I_n (FilteredObject.stdBiprod). The finiteness of the filtration of I is part of both sides, and is not a hypothesis.

theorem isFilteredInjective_iff_nonempty_iso_stdBiprod (I : FilteredObject 𝒜 ℤᵒᵖ) :
    I.IsFilteredInjective ↔ ∃ a b : ℤ, a ≤ b ∧ ∃ Inj : ℤ → 𝒜, (∀ n, Injective (Inj n)) ∧
      Nonempty (I ≅ stdBiprod a b Inj)

Tag 05TQ, a lemma

Tag 05TQ in the Stacks Project.

CategoryTheory.FilteredObject.isSplitMono_of_isFilteredInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/InjectiveSplitting.lean, line 210.

Stacks 05TQ. Let 𝒜 be an abelian category. A strict monomorphism u : I ⟶ A of filtered objects of 𝒜 whose source I is a filtered injective object of Fil^f(𝒜) — its filtration is finite and every graded piece gr^p(I) = F^p I / F^{p + 1} I is an injective object of 𝒜 — is a split monomorphism: it admits a retraction in the category of filtered objects.

public theorem isSplitMono_of_isFilteredInjective {𝒜 : Type u} [Category.{v} 𝒜] [Abelian 𝒜]
    {I A : FilteredObject 𝒜 ℤᵒᵖ} (u : I ⟶ A) [IsStrictHom u] (hI : I.IsFilteredInjective) :
    IsSplitMono u

Tag 05TR, a lemma

Tag 05TR in the Stacks Project.

CategoryTheory.FilteredObject.factors_of_isFilteredInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/InjectiveExtension.lean, line 266.

Stacks 05TR. Let 𝒜 be an abelian category, let u : A ⟶ B be a strict morphism of filtered objects of 𝒜 and let f : A ⟶ I be a morphism into a filtered injective object I of Fil^f(𝒜): its filtration is finite and every graded piece gr^p(I) = F^p I / F^{p + 1} I is an injective object of 𝒜. Then f extends along u: there is a morphism g : B ⟶ I of filtered objects with f = u ≫ g. The source assumes u to be a strict monomorphism; monomorphy is not used, and is automatic on Fil^f(𝒜).

public theorem factors_of_isFilteredInjective {𝒜 : Type u} [Category.{v} 𝒜] [Abelian 𝒜]
    {A B I : FilteredObject 𝒜 ℤᵒᵖ} (f : A ⟶ I) (u : A ⟶ B) [IsStrictHom u]
    (hI : I.IsFilteredInjective) :
    ∃ g : B ⟶ I, u ≫ g = f

Tag 05TS, a lemma

Tag 05TS in the Stacks Project.

CategoryTheory.FilteredObject.exists_mono_isStrict_isFilteredInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/InjectiveResolutionDegreeZero/FilteredResolution.lean, line 66.

Stacks 05TS. Let 𝒜 be an abelian category with enough injectives. Every object A of Fil^f(𝒜) admits a strict monomorphism u : A ⟶ I into a filtered injective object I: the underlying morphism of u is a monomorphism of 𝒜 and u is strict.

public theorem _root_.CategoryTheory.FilteredObject.exists_mono_isStrict_isFilteredInjective
    [EnoughInjectives 𝒜] (A : FilteredObject 𝒜 ℤᵒᵖ) (hA : A.filtration.IsFinite) :
    ∃ (I : FilteredObject 𝒜 ℤᵒᵖ) (u : A ⟶ I), Mono u.hom ∧ IsStrict u ∧ I.IsFilteredInjective

Tag 05TT, a lemma

Tag 05TT in the Stacks Project.

CochainComplex.exists_filteredQuasiIso_isStrictlyGE_injective_gradedPiece, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/InjectiveResolutionDegreeZero/FilteredResolution.lean, line 248. References: EGA 0 (13.6.2), “existence of resolution”.

Stacks 05TT. Let 𝒜 be an abelian category with enough injectives and let K^• be a filtered cochain complex of 𝒜 concentrated in degree 0 with finite filtration, i.e. K^• is A[0] for an object A of Fil^f(𝒜). Then there is a filtered quasi-isomorphism α : K^• ⟶ I^•, that is, one whose graded pieces gr^p(α) are all quasi-isomorphisms, where I^• is a complex of filtered injective objects with I^n = 0 for n < 0: every term (I^n, F^• I^n) is a filtered injective object of Fil^f(𝒜).

public theorem exists_filteredQuasiIso_isStrictlyGE_injective_gradedPiece {𝒜 : Type u}
    [Category.{v} 𝒜] [Abelian 𝒜] [EnoughInjectives 𝒜]
    (K : FilteredObject (CochainComplex 𝒜 ℤ) ℤᵒᵖ) [K.X.IsStrictlyGE 0] [K.X.IsStrictlyLE 0]
    (hK : K.filtration.IsFinite) :
    ∃ (I : FilteredObject (CochainComplex 𝒜 ℤ) ℤᵒᵖ) (α : K ⟶ I)
      (_ : CochainComplex.filteredQuasiIso 𝒜 α) (_ : I.X.IsStrictlyGE 0),
      ∀ n : ℤ, (evalFil I n).IsFilteredInjective

Tag 05TU, a lemma

Tag 05TU in the Stacks Project.

CochainComplex.exists_hom_comp_eq_of_filteredQuasiIso_of_injective_gradedPiece, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/InjectiveHom.lean, line 1468. References: EGA 0 (13.6.3), “special case”.

Stacks 05TU. Let 𝒜 be an abelian category, let f : A ⟶ B be a morphism of filtered objects, placed in degree 0 by taking the filtered complexes A and B to be concentrated in degree 0, and let a : A[0] ⟶ I^• and b : B[0] ⟶ J^• be morphisms into filtered complexes with degreewise finite filtrations, where a is a filtered quasi-isomorphism and J^• vanishes in negative degrees and consists of filtered injective objects, i.e. every term (J^n, F^• J^n) is a filtered injective object of Fil^f(𝒜). Then f lifts to a morphism g : I^• ⟶ J^• with a ≫ g = f ≫ b on the nose.

This is the lift that CochainComplex.FilteredInjectiveResolution.exists_resolutionSystem needs.

Three of the source's hypotheses are unused here and dropped: that b be a filtered quasi-isomorphism, and that I^• vanish in negative degrees and have filtered injective graded pieces. The lift comes from the surjectivity half of [Stacks, Tag 05TY], which asks only that a be a filtered quasi-isomorphism into a complex of K(Fil^f(𝒜)) and that the target J^• be bounded below and filtered injective; the homotopy it produces is degenerate because A is concentrated in degree 0, which turns the commutation in K(Fil^f(𝒜)) into an equality of morphisms of filtered complexes.

public theorem exists_hom_comp_eq_of_filteredQuasiIso_of_injective_gradedPiece
    {𝒜 : Type u} [Category.{v} 𝒜] [Abelian 𝒜]
    {A B I J : FilteredObject (CochainComplex 𝒜 ℤ) ℤᵒᵖ}
    [A.X.IsStrictlyGE 0] [A.X.IsStrictlyLE 0] [J.X.IsStrictlyGE 0]
    (f : A ⟶ B) (a : A ⟶ I) (b : B ⟶ J) (ha : filteredQuasiIso 𝒜 a)
    (hAfin : ∀ n : ℤ, ∃ p q : ℤ, IsIso ((A.filtration.ι.app (op p)).f n) ∧
      IsZero ((A.filtration.obj (op q)).X n))
    (hIfin : ∀ n : ℤ, ∃ p q : ℤ, IsIso ((I.filtration.ι.app (op p)).f n) ∧
      IsZero ((I.filtration.obj (op q)).X n))
    (hJ : ∀ n : ℤ, (evalFil J n).IsFilteredInjective) :
    ∃ g : I ⟶ J, a ≫ g = f ≫ b

Tag 05TV, a lemma

Tag 05TV in the Stacks Project.

CochainComplex.exists_termwiseSplit_shortExact_of_filteredQuasiIso_of_injective_gr, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/TermwiseSplit/TwistedSum.lean, line 712.

Stacks 05TV. Let 𝒜 be an abelian category and let 0 → A → B → C → 0 be a short exact sequence of Fil^f(𝒜), i.e. morphisms α : A ⟶ B, β : B ⟶ C of filtered objects with finite filtrations whose composite vanishes and whose graded pieces form short exact sequences 0 → gr^p A → gr^p B → gr^p C → 0. Let a : A[0] ⟶ I^• and c : C[0] ⟶ J^• be filtered quasi-isomorphisms, where I^• and J^• are complexes of filtered objects with finite filtrations, vanishing in negative degrees, and where each I^n is a filtered injective object of Fil^f(𝒜). Then there are a complex M^• of filtered objects, morphisms u : I^• ⟶ M^•, v : M^• ⟶ J^• and b : B[0] ⟶ M^• such that 0 → I^• → M^• → J^• → 0 is short exact, α ≫ b = a ≫ u and b ≫ v = β ≫ c, and the sequence 0 → I^n → M^n → J^n → 0 splits in Fil(𝒜) in each degree n: there are a retraction r of u^n and a section s of v^n compatible with the filtrations. Filtered objects are placed in degree 0 by taking the filtered complexes A, B, C to be concentrated in degree 0.

public theorem exists_termwiseSplit_shortExact_of_filteredQuasiIso_of_injective_gr
    {𝒜 : Type u} [Category.{v} 𝒜] [Abelian 𝒜]
    {A B C I J : FilteredObject (CochainComplex 𝒜 ℤ) ℤᵒᵖ}
    [A.X.IsStrictlyGE 0] [A.X.IsStrictlyLE 0] [C.X.IsStrictlyGE 0] [C.X.IsStrictlyLE 0]
    [I.X.IsStrictlyGE 0] [J.X.IsStrictlyGE 0]
    (α : A ⟶ B) (β : B ⟶ C) (a : A ⟶ I) (c : C ⟶ J)
    (hcomp : α.hom ≫ β.hom = 0)
    (hgr : ∀ p : ℤ, (ShortComplex.mk ((gr p).map α)
      ((gr p).map β) (by
        have hz : ∀ q : ℤᵒᵖ, (α ≫ β).natTrans.app q = 0 := fun q =>
          zero_of_comp_mono (C.filtration.ι.app q) (by simp [hcomp])
        rw [← Functor.map_comp]
        apply coequalizer.hom_ext
        simp only [grMap_map, cokernel.π_desc, hz, zero_comp]
        exact comp_zero.symm)).ShortExact)
    (ha : filteredQuasiIso 𝒜 a) (hc : filteredQuasiIso 𝒜 c)
    (hA : ∀ n : ℤ, ∃ p q : ℤ, IsIso ((A.filtration.ι.app (op p)).f n) ∧
      IsZero ((A.filtration.obj (op q)).X n))
    (hB : ∀ n : ℤ, ∃ p q : ℤ, IsIso ((B.filtration.ι.app (op p)).f n) ∧
      IsZero ((B.filtration.obj (op q)).X n))
    (hC : ∀ n : ℤ, ∃ p q : ℤ, IsIso ((C.filtration.ι.app (op p)).f n) ∧
      IsZero ((C.filtration.obj (op q)).X n))
    (hJfin : ∀ n : ℤ, ∃ p q : ℤ, IsIso ((J.filtration.ι.app (op p)).f n) ∧
      IsZero ((J.filtration.obj (op q)).X n))
    (hI : ∀ n : ℤ, (evalFil I n).IsFilteredInjective) :
    ∃ (M : FilteredObject (CochainComplex 𝒜 ℤ) ℤᵒᵖ) (u : I ⟶ M) (v : M ⟶ J) (b : B ⟶ M)
      (huv : u.hom ≫ v.hom = 0), (ShortComplex.mk u.hom v.hom huv).ShortExact ∧
      α ≫ b = a ≫ u ∧ b ≫ v = β ≫ c ∧
      ∀ n : ℤ, ∃ (r : M.X.X n ⟶ I.X.X n) (s : J.X.X n ⟶ M.X.X n),
        u.hom.f n ≫ r = 𝟙 (I.X.X n) ∧ s ≫ v.hom.f n = 𝟙 (J.X.X n) ∧
        (∀ p : ℤ, ∃ rp : (M.filtration.obj (op p)).X n ⟶ (I.filtration.obj (op p)).X n,
          rp ≫ (I.filtration.ι.app (op p)).f n = (M.filtration.ι.app (op p)).f n ≫ r) ∧
        (∀ p : ℤ, ∃ sp : (J.filtration.obj (op p)).X n ⟶ (M.filtration.obj (op p)).X n,
          sp ≫ (M.filtration.ι.app (op p)).f n = (J.filtration.ι.app (op p)).f n ≫ s)

Tag 05TW, a lemma

Tag 05TW in the Stacks Project.

CochainComplex.exists_mono_isStrictHom_filteredQuasiIso_isStrictlyGE_injective_gradedPiece, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/InjectiveResolution.lean, line 1485. References: EGA 0 (13.6.2), “existence of resolution”.

Stacks 05TW. Let 𝒜 be an abelian category with enough injectives and let K^• be a filtered cochain complex of 𝒜 with K^n = 0 for n < a and with each K^n of finite filtration, i.e. an object of K^+(Fil^f(𝒜)). Then there is a filtered quasi-isomorphism α : K^• ⟶ I^•, that is, one whose graded pieces gr^p(α) are all quasi-isomorphisms, which is moreover a strict monomorphism — degreewise, each K^n ⟶ I^n is a monomorphism with F^p K^n = (K^n) ∩ F^p I^n — where I^• is a complex of filtered injective objects with I^n = 0 for n < a: every term (I^n, F^• I^n) is a filtered injective object of Fil^f(𝒜).

public theorem exists_mono_isStrictHom_filteredQuasiIso_isStrictlyGE_injective_gradedPiece
    (K : FilteredObject (CochainComplex 𝒜 ℤ) ℤᵒᵖ) (a : ℤ) [K.X.IsStrictlyGE a]
    (hK : ∀ n : ℤ, ∃ p q : ℤ, IsIso ((K.filtration.ι.app (op p)).f n) ∧
      IsZero ((K.filtration.obj (op q)).X n)) :
    ∃ (I : FilteredObject (CochainComplex 𝒜 ℤ) ℤᵒᵖ) (α : K ⟶ I)
      (_ : CochainComplex.filteredQuasiIso 𝒜 α) (_ : Mono α.hom)
      (_ : FilteredObject.IsStrictHom α) (_ : I.X.IsStrictlyGE a),
      ∀ n : ℤ, (evalFil I n).IsFilteredInjective

Tag 05TX, a lemma

Tag 05TX in the Stacks Project.

CochainComplex.exists_homotopy_zero_of_filteredAcyclic_of_injective_gradedPiece, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/AcyclicHomotopy.lean, line 599.

Stacks 05TX. Let 𝒜 be an abelian category and let K^•, I^• be filtered cochain complexes of 𝒜 whose terms have finite filtrations, i.e. objects of K(Fil^f(𝒜)). Assume K^• is filtered acyclic, that is every gr^p K^• = F^p K^•/F^{p + 1} K^• is acyclic, and that I^• is bounded below, I^n = 0 for n < n₀, and consists of filtered injective objects of Fil^f(𝒜): every term (I^n, F^• I^n) is filtered injective. Then every morphism α : K^• ⟶ I^• of filtered complexes is homotopic to zero by a filtered homotopy: there is a homotopy h from α to 0 on the underlying complexes each of whose components h^{i,j} : K^i ⟶ I^j carries F^p K^i into F^p I^j. Equivalently Hom_{K(Fil^f(𝒜))}(K^•, I^•) = 0.

public theorem exists_homotopy_zero_of_filteredAcyclic_of_injective_gradedPiece
    {𝒜 : Type u} [Category.{v} 𝒜] [Abelian 𝒜]
    {K I : FilteredObject (CochainComplex 𝒜 ℤ) ℤᵒᵖ} (α : K ⟶ I) (n₀ : ℤ) [I.X.IsStrictlyGE n₀]
    (hK : filteredAcyclic 𝒜 K)
    (hKfin : ∀ n : ℤ, ∃ p q : ℤ, IsIso ((K.filtration.ι.app (op p)).f n) ∧
      IsZero ((K.filtration.obj (op q)).X n))
    (hI : ∀ n : ℤ, (evalFil I n).IsFilteredInjective) :
    ∃ h : Homotopy α.hom 0, ∀ i j p : ℤ,
      ∃ hp : (K.filtration.obj (op p)).X i ⟶ (I.filtration.obj (op p)).X j,
        hp ≫ (I.filtration.ι.app (op p)).f j
          = (K.filtration.ι.app (op p)).f i ≫ h.hom i j

Tag 05TY, a lemma

Tag 05TY in the Stacks Project.

CochainComplex.bijective_precomp_full_and_map_eq_iff_filteredHomotopy_of_injective_gradedPiece, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/InjectiveHom.lean, line 1412.

Stacks 05TY. Let 𝒜 be an abelian category, let Filf be the class of filtered cochain complexes of 𝒜 whose filtration is finite in each degree — so that Filf.FullSubcategory is K(Fil^f(𝒜)) — and let Q be a localisation of it at the filtered quasi-isomorphisms, that is, the filtered derived category DF(𝒜) (Definition 05S2). Let I^• be a bounded below complex, I^n = 0 for n < n₀, consisting of filtered injective objects, that is with every gr^p(I^n) an injective object of 𝒜. Then:

for every filtered quasi-isomorphism α : K^• ⟶ L^• in K(Fil^f(𝒜)), precomposition with α is a bijection Hom_{K(Fil^f(𝒜))}(L^•, I^•) ⟶ Hom_{K(Fil^f(𝒜))}(K^•, I^•): every γ : K^• ⟶ I^• is filtered homotopic to α ≫ β for some β : L^• ⟶ I^•, and if α ≫ β and α ≫ β' are filtered homotopic then so are β and β';

for every M^• in K(Fil^f(𝒜)), Hom_{K(Fil^f(𝒜))}(M^•, I^•) = Hom_{DF(𝒜)}(M^•, I^•): every φ : Q.obj M^• ⟶ Q.obj I^• is Q.map f for a morphism of filtered complexes f : M^• ⟶ I^•, and Q.map f = Q.map g exactly when f and g are filtered homotopic.

Here a filtered homotopy between morphisms of filtered complexes is a homotopy h of the underlying complexes of 𝒜 each of whose components h^{i,j} carries F^p into F^p.

public theorem bijective_precomp_full_and_map_eq_iff_filteredHomotopy_of_injective_gradedPiece
    {𝒜 : Type u} [Category.{v} 𝒜] [Abelian 𝒜] {D : Type u'} [Category.{v'} D]
    (Filf : ObjectProperty (FilteredObject (CochainComplex 𝒜 ℤ) ℤᵒᵖ))
    (hFilf : ∀ K, Filf K ↔ ∀ n : ℤ, ∃ p q : ℤ,
      IsIso ((K.filtration.ι.app (op p)).f n) ∧ IsZero ((K.filtration.obj (op q)).X n))
    (Q : Filf.FullSubcategory ⥤ D)
    [Q.IsLocalization ((filteredQuasiIso 𝒜).inverseImage Filf.ι)]
    (I : Filf.FullSubcategory) (n₀ : ℤ) [I.obj.X.IsStrictlyGE n₀]
    (hI : ∀ p n : ℤ, Injective (((gr p).obj I.obj).X n)) :
    (∀ (K L : Filf.FullSubcategory) (α : K ⟶ L),
        (filteredQuasiIso 𝒜).inverseImage Filf.ι α →
        (∀ γ : K ⟶ I, ∃ β : L ⟶ I,
          ∃ h : Homotopy (Filf.ι.map (α ≫ β)).hom (Filf.ι.map γ).hom, ∀ i j p : ℤ,
            ∃ hp : (K.obj.filtration.obj (op p)).X i ⟶ (I.obj.filtration.obj (op p)).X j,
              hp ≫ (I.obj.filtration.ι.app (op p)).f j
                = (K.obj.filtration.ι.app (op p)).f i ≫ h.hom i j) ∧
        ∀ β β' : L ⟶ I,
          (∃ h : Homotopy (Filf.ι.map (α ≫ β)).hom (Filf.ι.map (α ≫ β')).hom, ∀ i j p : ℤ,
            ∃ hp : (K.obj.filtration.obj (op p)).X i ⟶ (I.obj.filtration.obj (op p)).X j,
              hp ≫ (I.obj.filtration.ι.app (op p)).f j
                = (K.obj.filtration.ι.app (op p)).f i ≫ h.hom i j) →
          ∃ h : Homotopy (Filf.ι.map β).hom (Filf.ι.map β').hom, ∀ i j p : ℤ,
            ∃ hp : (L.obj.filtration.obj (op p)).X i ⟶ (I.obj.filtration.obj (op p)).X j,
              hp ≫ (I.obj.filtration.ι.app (op p)).f j
                = (L.obj.filtration.ι.app (op p)).f i ≫ h.hom i j) ∧
      ∀ M : Filf.FullSubcategory,
        (∀ φ : Q.obj M ⟶ Q.obj I, ∃ f : M ⟶ I, Q.map f = φ) ∧
        ∀ f g : M ⟶ I, Q.map f = Q.map g ↔
          ∃ h : Homotopy (Filf.ι.map f).hom (Filf.ι.map g).hom, ∀ i j p : ℤ,
            ∃ hp : (M.obj.filtration.obj (op p)).X i ⟶ (I.obj.filtration.obj (op p)).X j,
              hp ≫ (I.obj.filtration.ι.app (op p)).f j
                = (M.obj.filtration.ι.app (op p)).f i ≫ h.hom i j

Tag 015Q, a lemma

Tag 015Q in the Stacks Project.

CochainComplex.FilteredDerivedCategory.isEquivalence_isTriangulated_toPlus_and_squares, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/FilteredDerivedCategory/Triangulated.lean, line 571.

Let 𝒜 be an abelian category with enough injectives, let I^f ⊂ Fil^f(𝒜) be the filtered injective objects and I ⊂ 𝒜 the injective objects. The canonical functor K⁺(I^f) ⥤ DF⁺(𝒜) is exact, fully faithful and essentially surjective, i.e. an equivalence of triangulated categories. Furthermore the squares
K⁺(I^f) ──→ DF⁺(𝒜)          K⁺(I^f) ──→ DF⁺(𝒜)
  │gr^p        │gr^p           │forget F    │forget F
  ↓            ↓               ↓            ↓
K⁺(I) ────→ D⁺(𝒜)           K⁺(I) ────→ D⁺(𝒜)
commute. Here gr^p, forget F : DF(𝒜) ⥤ D(𝒜) are the functors induced by gr^p, forget F : K(Fil^f(𝒜)) ⥤ K(𝒜), as recorded by the isomorphisms Qh ⋙ gr^p ≅ gr^p ⋙ Q and Qh ⋙ forget F ≅ forget F ⋙ Q.

theorem isEquivalence_isTriangulated_toPlus_and_squares [EnoughInjectives 𝒜] :
    (toPlus 𝒜).IsEquivalence ∧ (toPlus 𝒜).IsTriangulated ∧
      (∀ p : ℤ, Nonempty (Qh (𝒜 := 𝒜) ⋙ grDF p ≅
          (FiniteFilteredObject.grP p).mapHomotopyCategory _ ⋙ DerivedCategory.Qh) ∧
        Nonempty (toPlus 𝒜 ⋙ liftDFPlus (FiniteFilteredObject.grP p) (grP_inverts p) ≅
          (injectivePlus 𝒜).lift ((filteredInjectivePlus 𝒜).ι ⋙
              (FiniteFilteredObject.grP p).mapHomotopyCategory _)
            (fun X => injectivePlus_grP_obj p X.property) ⋙ injectivePlusQ 𝒜)) ∧
      Nonempty (Qh (𝒜 := 𝒜) ⋙ forgetDF ≅
        FiniteFilteredObject.forget.mapHomotopyCategory _ ⋙ DerivedCategory.Qh) ∧
      Nonempty (toPlus 𝒜 ⋙ liftDFPlus FiniteFilteredObject.forget forget_inverts ≅
        (injectivePlus 𝒜).lift ((filteredInjectivePlus 𝒜).ι ⋙
            FiniteFilteredObject.forget.mapHomotopyCategory _)
          (fun X => injectivePlus_forget_obj X.property) ⋙ injectivePlusQ 𝒜)

Tag 015U, an equation

Tag 015U in the Stacks Project.

CochainComplex.exists_iso_gradedPiece_rightDerivedFunctorPlus_of_filteredQuasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/DerivedFunctor.lean, line 253.

Stacks 015U. Let T : 𝒜 ⥤ ℬ be an additive functor of abelian categories with 𝒜 having enough injectives, and let RT : D⁺(𝒜) ⥤ D⁺(ℬ) be its right derived functor. Let α : K^• ⟶ I^• be a filtered quasi-isomorphism of filtered cochain complexes of 𝒜 with I^• filtered injective, i.e. every gr^p I^n injective — a filtered injective resolution of K^• — and let M^• be a filtered cochain complex of ℬ together with isomorphisms e p : gr^p M^• ≅ T(gr^p I^•) in the homotopy category, the datum of M^• = T_ext(I^•) out of which the filtered right derived functor is built, so that M^• presents RT(K^•) in DF⁺(ℬ); assume the graded pieces of K^•, I^• and M^• are bounded below. Then, for every p, there is an isomorphism gr^p(RT(K^•)) = gr^p M^• ≅ RT(gr^p K^•) in D⁺(ℬ) compatible with RT(gr^p α) and with the canonical map Q(T(gr^p I^•)) ⟶ RT(Q(gr^p I^•)) of the right derived functor; since the former is an isomorphism, the compatibility determines it uniquely. This is the isomorphism of functors gr^p ∘ RT ≅ RT ∘ gr^p on DF⁺(𝒜).

public theorem exists_iso_gradedPiece_rightDerivedFunctorPlus_of_filteredQuasiIso
    {A : Type u} {B : Type u'} [Category.{v} A] [Category.{v'} B] [Abelian A] [Abelian B]
    [HasDerivedCategory.{w} A] [HasDerivedCategory.{w'} B] [EnoughInjectives A]
    (T : A ⥤ B) [T.Additive]
    {K I : FilteredObject (CochainComplex A ℤ) ℤᵒᵖ} (α : K ⟶ I)
    (hα : filteredQuasiIso A α)
    (hinj : ∀ p n : ℤ, Injective (((gr p).obj I).X n))
    (M : FilteredObject (CochainComplex B ℤ) ℤᵒᵖ)
    (hK : ∀ p : ℤ, CochainComplex.plus A ((gr p).obj K))
    (hI : ∀ p : ℤ, CochainComplex.plus A ((gr p).obj I))
    (hM : ∀ p : ℤ, CochainComplex.plus B ((gr p).obj M))
    (e : ∀ p : ℤ, (HomotopyCategory.Plus.quotient B).obj ⟨_, hM p⟩ ≅
      T.mapHomotopyCategoryPlus.obj ((HomotopyCategory.Plus.quotient A).obj ⟨_, hI p⟩)) (p : ℤ) :
    ∃ Φ : DerivedCategory.Plus.Qh.obj ((HomotopyCategory.Plus.quotient B).obj ⟨_, hM p⟩) ≅
        T.rightDerivedFunctorPlus.obj (DerivedCategory.Plus.Qh.obj
          ((HomotopyCategory.Plus.quotient A).obj ⟨_, hK p⟩)),
      Φ.hom ≫ T.rightDerivedFunctorPlus.map (DerivedCategory.Plus.Qh.map
          ((HomotopyCategory.Plus.quotient A).map (ObjectProperty.homMk
            (X := ⟨_, hK p⟩) (Y := ⟨_, hI p⟩)
            ((gr p).map α)))) =
        DerivedCategory.Plus.Qh.map (e p).hom ≫
          T.rightDerivedFunctorPlusUnith.app
            ((HomotopyCategory.Plus.quotient A).obj ⟨_, hI p⟩)

Tag 015V, an equation

Tag 015V in the Stacks Project.

CochainComplex.isIso_rightDerivedFunctorPlusUnit_app_forget_of_injective_gradedPiece, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Filtered/DerivedFunctor.lean, line 576.

Stacks 015V. Let T : 𝒜 ⥤ ℬ be an additive functor of abelian categories with 𝒜 having enough injectives, and let I be a bounded below complex of filtered injective objects: a bounded below filtered cochain complex of 𝒜 every term (I^n, F^• I^n) of which is a filtered injective object of Fil^f(𝒜). Then the canonical map
Q(T((forget F) I)) ⟶ RT(Q((forget F) I))
in D⁺(ℬ) — the component at (forget F) I of the unit of the right derived functor RT : D⁺(𝒜) ⥤ D⁺(ℬ) — is an isomorphism. Since the left-hand side is (forget F)(RT(I)), RT here being the filtered right derived functor of [Stacks, Tag 05U2], and every object of DF⁺(𝒜) is isomorphic to such an I ([Stacks, Tag 015Q]), this is the source's isomorphism (forget F) ∘ RT ≅ RT ∘ (forget F) of functors DF⁺(𝒜) ⥤ D⁺(ℬ).

public theorem isIso_rightDerivedFunctorPlusUnit_app_forget_of_injective_gradedPiece
    {A : Type u} {B : Type u'} [Category.{v} A] [Category.{v'} B] [Abelian A] [Abelian B]
    [HasDerivedCategory.{w} A] [HasDerivedCategory.{w'} B] [EnoughInjectives A]
    (T : A ⥤ B) [T.Additive]
    (I : FilteredObject (CochainComplex A ℤ) ℤᵒᵖ) (a : ℤ) [I.X.IsStrictlyGE a]
    (hI : ∀ n : ℤ, (evalFil I n).IsFilteredInjective) :
    IsIso (T.rightDerivedFunctorPlusUnith.app ((HomotopyCategory.Plus.quotient A).obj
      ⟨FilteredObject.forget.obj I,
        (CochainComplex.plus_iff A _).2 ⟨a, ‹I.X.IsStrictlyGE a›⟩⟩))

Tag 015W, a lemma

Tag 015W in the Stacks Project.

CochainComplex.exists_spectralSequence_rightDerivedFunctorPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/FilteredDerivedCategory/InjectiveResolutions.lean, line 265. The attribute's comment: “the spectral sequence, its E_1 page, boundedness, convergence and finiteness of the induced filtration”. References: EGA 0 (13.6.4), “E_1, abutment, biregular”.

Stacks 015W. Let T : 𝒜 ⥤ ℬ be an additive functor of abelian categories, 𝒜 having enough injectives, and let (K^•, F) be an object of Comp⁺(Fil^f(𝒜)): a filtered complex with K^n = 0 for n < a whose filtration is finite in each degree. Let α : K^• ⟶ I^• be a filtered quasi-isomorphism to a bounded below complex of filtered injective objects — such a filtered injective resolution exists ([Stacks, Tag 05TW], exists_mono_isStrictHom_filteredQuasiIso_isStrictlyGE_injective_gradedPiece) and the statement holds for every choice of it. Let E be the spectral sequence of the filtered complex T(I^•) = RT(K^•) of ℬ, presented as in [Stacks, Tag 012M] by its pages E_r^{p,q} = Z_r^{p,q}/D_r^{p,q} and its differentials d_r of bidegree (r, -r + 1) induced by the differential of T(I^•). Then

E_1^{p,q} ≅ R^{p+q}T(gr^p K^•);

E is bounded: for each n only finitely many E_0^{p, n - p} are nonzero;

E converges to H^*(T(I^•)) = R^*T(K^•): d_r^{p,q} = 0 for r ≫ 0, and the stable cycles and boundaries exist and are those of (012S) and (012T) with equality;

the induced filtration on each R^nT(K^•) = H^n(T(I^•)) is finite;

H^n(T(I^•)) ≅ R^nT(K^•).

theorem exists_spectralSequence_rightDerivedFunctorPlus
    [HasDerivedCategory.{w} A] [EnoughInjectives A] (T : A ⥤ B) [T.Additive]
    {K I : FilteredObject (CochainComplex A ℤ) ℤᵒᵖ} (a b : ℤ) [K.X.IsStrictlyGE a]
    [I.X.IsStrictlyGE b] (hK : K.filtration.IsDegreewiseFinite) (α : K ⟶ I)
    (hα : filteredQuasiIso A α) (hI : ∀ n : ℤ, (evalFil I n).IsFilteredInjective)
    (F : ∀ (_p n : ℤ), Subobject ((mapFilteredInjective T I hI).X.X n))
    (hF : ∀ p n : ℤ, F p n =
      Subobject.mk (((mapFilteredInjective T I hI).filtration.ι.app (op p)).f n))
    (Z : ∀ (_r _p n : ℤ), Subobject ((mapFilteredInjective T I hI).X.X n))
    (hZ : ∀ r p n : ℤ, Z r p n = F p n ⊓
      (Subobject.pullback ((mapFilteredInjective T I hI).X.d n (n + 1))).obj (F (p + r) (n + 1)))
    (D : ∀ (_r _p n : ℤ), Subobject ((mapFilteredInjective T I hI).X.X n))
    (hD : ∀ r p n : ℤ, D r p n = Z (r - 1) (p + 1) n ⊔
      (Subobject.«exists» ((mapFilteredInjective T I hI).X.d (n - 1) n)).obj
        (Z (r - 1) (p - r + 1) (n - 1)))
    (FH : ∀ (n _p : ℤ), Subobject ((mapFilteredInjective T I hI).X.homology n))
    (hFH : ∀ n p : ℤ, FH n p = imageSubobject
      (HomologicalComplex.homologyMap ((mapFilteredInjective T I hI).filtration.ι.app (op p)) n)) :
    ∃ (e : ∀ (r p q n : ℤ) (hr : 0 ≤ r) (_ : n = p + q),
        ((spectralSequenceOf (mapFilteredInjective T I hI) F hF).page r hr).X (p, q) ≅
        cokernel (Subobject.ofLE _ _ (inf_le_right : D r p n ⊓ Z r p n ≤ Z r p n))),
      (∀ (r p q n : ℤ) (hr : 0 ≤ r) (hn : n = p + q),
        ∃ δ : (Z r p n : B) ⟶ (Z r (p + r) (n + 1) : B),
          δ ≫ (Z r (p + r) (n + 1)).arrow =
            (Z r p n).arrow ≫ (mapFilteredInjective T I hI).X.d n (n + 1) ∧
          cokernel.π (Subobject.ofLE _ _ (inf_le_right : D r p n ⊓ Z r p n ≤ Z r p n)) ≫
              (e r p q n hr hn).inv ≫
                ((spectralSequenceOf (mapFilteredInjective T I hI) F hF).page r hr).d
                  (p, q) (p + r, q - r + 1) =
            δ ≫ cokernel.π (Subobject.ofLE _ _ (inf_le_right :
                D r (p + r) (n + 1) ⊓ Z r (p + r) (n + 1) ≤ Z r (p + r) (n + 1))) ≫
              (e r (p + r) (q - r + 1) (n + 1) hr (by omega)).inv) ∧
      (∀ p q : ℤ, Nonempty
        (((spectralSequenceOf (mapFilteredInjective T I hI) F hF).page 1).X (p, q) ≅
        (DerivedCategory.Plus.homologyFunctor B (p + q)).obj
          (T.rightDerivedFunctorPlus.obj (DerivedCategory.Plus.Qh.obj
            ((HomotopyCategory.Plus.quotient A).obj
              ⟨(FilteredObject.gr p).obj K, ⟨a, isStrictlyGE_gr K a p⟩⟩))))) ∧
      (∀ n : ℤ, {p : ℤ | ¬ IsZero
        (((spectralSequenceOf (mapFilteredInjective T I hI) F hF).page 0).X (p, n - p))}.Finite) ∧
      (∀ p q : ℤ, ∃ b : ℤ, ∀ (r : ℤ) (hr : 0 ≤ r), b ≤ r →
        ((spectralSequenceOf (mapFilteredInjective T I hI) F hF).page r hr).d
          (p, q) (p + r, q - r + 1) = 0) ∧
      (∀ p n : ℤ,
        IsGLB (Set.range fun r : ℕ => F p n ⊓
            (Subobject.pullback ((mapFilteredInjective T I hI).X.d n (n + 1))).obj
              (F (p + r) (n + 1)) ⊔ F (p + 1) n)
          (kernelSubobject ((mapFilteredInjective T I hI).X.d n (n + 1)) ⊓ F p n ⊔
            F (p + 1) n) ∧
        IsLUB (Set.range fun r : ℕ => F p n ⊓
            (Subobject.«exists» ((mapFilteredInjective T I hI).X.d (n - 1) n)).obj
              (F (p - r) (n - 1)) ⊔ F (p + 1) n)
          (imageSubobject ((mapFilteredInjective T I hI).X.d (n - 1) n) ⊓ F p n ⊔
            F (p + 1) n)) ∧
      (∀ n : ℤ, ∃ p₀ p₁ : ℤ, p₀ ≤ p₁ ∧ FH n p₀ = ⊤ ∧ FH n p₁ = ⊥) ∧
      (∀ n : ℤ, Nonempty ((mapFilteredInjective T I hI).X.homology n ≅
        (DerivedCategory.Plus.homologyFunctor B n).obj
          (T.rightDerivedFunctorPlus.obj (DerivedCategory.Plus.Qh.obj
            ((HomotopyCategory.Plus.quotient A).obj ⟨K.X, ⟨a, inferInstance⟩⟩)))))

CochainComplex.exists_spectralSequenceMap_rightDerivedFunctorPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/FilteredDerivedCategory/InjectiveResolutions.lean, line 517. The attribute's comment: “functoriality in K^•: the induced morphism of spectral sequences, independent of choices on E_r for r ≥ 1”. References: EGA 0 (13.6.3), “existence of v”; EGA 0 (13.6.4), “E_r indep. of choices”.

Stacks 015W, functoriality. Let f : K^• ⟶ L^• be a morphism of Comp⁺(Fil^f(𝒜)) and let α : K^• ⟶ I^•, β : L^• ⟶ J^• be filtered injective resolutions. There is a morphism γ : I^• ⟶ J^• with α ≫ γ filtered homotopic to f ≫ β ([Stacks, Tag 05TY]); it induces a morphism of spectral sequences E_r(T(I^•)) ⟶ E_r(T(J^•)) ([Stacks, Tag 012O]), and on the pages E_r, r ≥ 1, this morphism does not depend on the choice of γ.

theorem exists_spectralSequenceMap_rightDerivedFunctorPlus
    {K L I J : FilteredObject (CochainComplex A ℤ) ℤᵒᵖ}
    (hK : K.filtration.IsDegreewiseFinite)
    (a b : ℤ) [I.X.IsStrictlyGE a] [J.X.IsStrictlyGE b]
    (hI : ∀ n : ℤ, (evalFil I n).IsFilteredInjective)
    (hJ : ∀ n : ℤ, (evalFil J n).IsFilteredInjective)
    (α : K ⟶ I) (hα : filteredQuasiIso A α) (β : L ⟶ J) (f : K ⟶ L) :
    (∃ γ : I ⟶ J, FilteredHomotopic (α ≫ γ) (f ≫ β)) ∧
      ∀ γ γ' : I ⟶ J, FilteredHomotopic (α ≫ γ) (f ≫ β) →
        FilteredHomotopic (α ≫ γ') (f ≫ β) → ∀ (r : ℤ) (hr : 1 ≤ r),
          (filteredSpectralSequenceMap (mapFilteredInjectiveMap T γ hI hJ)).hom r (by omega) =
            (filteredSpectralSequenceMap (mapFilteredInjectiveMap T γ' hI hJ)).hom r
              (by omega)

CochainComplex.filteredHomotopic_comp_and_spectralSequenceMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/FilteredDerivedCategory/InjectiveResolutions.lean, line 542. The attribute's comment: “the construction is compatible with composition”.

Stacks 015W, compatibility with composition. If γ lifts f : K^• ⟶ L^• and δ lifts g : L^• ⟶ M^• along filtered injective resolutions, then γ ≫ δ lifts f ≫ g, and the morphism of spectral sequences induced by γ ≫ δ is the composite of those induced by γ and δ.

theorem filteredHomotopic_comp_and_spectralSequenceMap_comp
    {K L M I J P : FilteredObject (CochainComplex A ℤ) ℤᵒᵖ}
    (hI : ∀ n : ℤ, (evalFil I n).IsFilteredInjective)
    (hJ : ∀ n : ℤ, (evalFil J n).IsFilteredInjective)
    (hP : ∀ n : ℤ, (evalFil P n).IsFilteredInjective)
    (α : K ⟶ I) (β : L ⟶ J) (ε : M ⟶ P) (f : K ⟶ L) (g : L ⟶ M) (γ : I ⟶ J) (δ : J ⟶ P)
    (hγ : FilteredHomotopic (α ≫ γ) (f ≫ β)) (hδ : FilteredHomotopic (β ≫ δ) (g ≫ ε)) :
    FilteredHomotopic (α ≫ γ ≫ δ) ((f ≫ g) ≫ ε) ∧
      filteredSpectralSequenceMap (mapFilteredInjectiveMap T (γ ≫ δ) hI hP) =
        filteredSpectralSequenceMap (mapFilteredInjectiveMap T γ hI hJ) ≫
          filteredSpectralSequenceMap (mapFilteredInjectiveMap T δ hJ hP)

CochainComplex.isIso_spectralSequenceMap_rightDerivedFunctorPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/FilteredDerivedCategory/InjectiveResolutions.lean, line 568. The attribute's comment: “the terms (E_r, d_r) for r ≥ 1 do not depend on any choices”. References: EGA 0 (13.6.4), “partial”.

Stacks 015W, independence of choices. For two filtered injective resolutions α : K^• ⟶ I^• and α' : K^• ⟶ I'^• of the same object, any γ : I^• ⟶ I'^• with α ≫ γ filtered homotopic to α' induces isomorphisms E_r(T(I^•)) ≅ E_r(T(I'^•)) on all pages r ≥ 1; when I'^• = I^• and α' = α the induced morphism is the identity on these pages. So the terms (E_r, d_r), r ≥ 1, do not depend on the choice of resolution.

theorem isIso_spectralSequenceMap_rightDerivedFunctorPlus
    {K I I' : FilteredObject (CochainComplex A ℤ) ℤᵒᵖ} (hK : K.filtration.IsDegreewiseFinite)
    (a a' : ℤ) [I.X.IsStrictlyGE a] [I'.X.IsStrictlyGE a']
    (hI : ∀ n : ℤ, (evalFil I n).IsFilteredInjective)
    (hI' : ∀ n : ℤ, (evalFil I' n).IsFilteredInjective)
    (α : K ⟶ I) (hα : filteredQuasiIso A α) (α' : K ⟶ I') (hα' : filteredQuasiIso A α')
    (γ : I ⟶ I') (hγ : FilteredHomotopic (α ≫ γ) α') :
    (∀ (r : ℤ) (hr : 1 ≤ r),
      IsIso ((filteredSpectralSequenceMap (mapFilteredInjectiveMap T γ hI hI')).hom r
        (by omega))) ∧
    ∀ γ₀ : I ⟶ I, FilteredHomotopic (α ≫ γ₀) α → ∀ (r : ℤ) (hr : 1 ≤ r),
      (filteredSpectralSequenceMap (mapFilteredInjectiveMap T γ₀ hI hI)).hom r (by omega) =
        𝟙 _

Sources

LeanCategoryTheory.FilteredObject.IsFilteredInjective · CategoryTheory.FilteredObject.isFilteredInjective_iff_nonempty_iso_stdBiprod · CategoryTheory.FilteredObject.isSplitMono_of_isFilteredInjective · CategoryTheory.FilteredObject.factors_of_isFilteredInjective · CategoryTheory.FilteredObject.exists_mono_isStrict_isFilteredInjective · CochainComplex.exists_filteredQuasiIso_isStrictlyGE_injective_gradedPiece · CochainComplex.exists_hom_comp_eq_of_filteredQuasiIso_of_injective_gradedPiece · CochainComplex.exists_termwiseSplit_shortExact_of_filteredQuasiIso_of_injective_gr

Section13.27 Ext groups #

Section 13.27 of the Stacks Project, Tag 06XP. 10 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06XQ, a definition

Tag 06XQ in the Stacks Project.

CategoryTheory.DerivedCategory.Ext, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/ExtAndYonedaExtensions.lean, line 51. References: SGA 4½ Etat 0 (3.2.1).

The i-th extension group Ext^i_𝒜(X, Y) = Hom_{D(𝒜)}(X, Y⟦i⟧) of an object X of the derived category D(𝒜) of an abelian category 𝒜 by an object Y, for i : ℤ. It is canonically identified with Hom_{D(𝒜)}(X⟦-i⟧, Y) via the adjunction between the shifts ⟦-i⟧ ⊣ ⟦i⟧.

public noncomputable abbrev DerivedCategory.Ext (X Y : DerivedCategory C) (i : ℤ) : Type _

CategoryTheory.Abelian.zExt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/ExtAndYonedaExtensions.lean, line 59. References: SGA 4½ Etat 0 (3.2.1), “degree-0 objects”.

The i-th extension group Ext^i_𝒜(A, B) = Ext^i_𝒜(A[0], B[0]) of an object A of an abelian category 𝒜 by an object B, for i : ℤ, where A[0] is the image of A under 𝒜 ⥤ D(𝒜), the complex concentrated in degree 0. For i = (n : ℕ) this is Mathlib's CategoryTheory.Abelian.Ext A B n, up to the equivalence Abelian.Ext.homEquiv.

public noncomputable abbrev Abelian.zExt (A B : C) (i : ℤ) : Type _

DerivedCategory.surjective_extZero_comp_iff_surjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/ZeroDegree.lean, line 40. The attribute's comment: “degree zero”.

Precomposition with ξ is surjective on degree-zero Ext groups into Y exactly when it is surjective on morphisms into Y. In degree 0 an Ext class is a morphism, by CategoryTheory.ShiftedHom.homEquiv, and the identification commutes with precomposition.

public theorem surjective_extZero_comp_iff_surjective_comp
    {E X : DerivedCategory C} (ξ : E ⟶ X) (Y : DerivedCategory C) :
    Function.Surjective (fun α : DerivedCategory.Ext X Y 0 => ξ ≫ α) ↔
      Function.Surjective (fun f : X ⟶ Y => ξ ≫ f)

Tag 06XR, a lemma

Tag 06XR in the Stacks Project.

ExtByResolutions.ext_via_injective_resolution_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/SplittingAndResolutions.lean, line 681. The attribute's comment: “(1)”.

Statement 1 (Stacks 06XR, part 1): computing Ext via an injective resolution. Given an injective resolution f : Y ⟶ I (Definition 2), the canonical map canMapOfInjectiveResolution (induced by f) is a bijection Hom_{K(A)}(X, I[i]) → Hom_{D(A)}(Q(X), Q(Y)[i]). This is the canonical identification Ext^i_A(X, Y) = Hom_{D(A)}(Q(X), Q(Y)[i]) ≅ Hom_{K(A)}(X, I[i]).

theorem ext_via_injective_resolution_bijective
    (X Y I : CochainComplex C ℤ) (i : ℤ)
    {f : Y ⟶ I} (hf : IsInjectiveResolution f) :
    haveI := hf.quasiIso
    Function.Bijective (canMapOfInjectiveResolution X Y I i f)

ExtByResolutions.ext_via_projective_resolution_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/SplittingAndResolutions.lean, line 724. The attribute's comment: “(2)”.

Statement 2 (Stacks 06XR, part 2): computing Ext via a projective resolution. Given a projective resolution g : P ⟶ X (Definition 3), the canonical map canMapOfProjectiveResolution (induced by g) is a bijection Hom_{K(A)}(P[-i], Y) → Hom_{D(A)}(Q(X), Q(Y)[i]). This is the canonical identification Ext^i_A(X, Y) = Hom_{D(A)}(Q(X), Q(Y)[i]) ≅ Hom_{K(A)}(P[-i], Y).

theorem ext_via_projective_resolution_bijective
    (X Y P : CochainComplex C ℤ) (i : ℤ)
    {g : P ⟶ X} (hg : IsProjectiveResolution g) :
    haveI := hg.quasiIso
    Function.Bijective (canMapOfProjectiveResolution X Y P i g)

Tag 06XS, a lemma

Tag 06XS in the Stacks Project.

DerivedCategory.bijective_homologyFunctor_shiftMap_of_isLE_of_isGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/ExtOneAndVanishing.lean, line 571.

Let 𝒜 be an abelian category and let X, Y be objects of D(𝒜) such that H^i(X) = 0 for i > a and H^j(Y) = 0 for j < b. If n + a = a' and a' ≤ b, then taking homology in degree a, Ext^n_𝒜(X, Y) = Hom_{D(𝒜)}(X, Y⟦n⟧) → Hom_𝒜(H^a(X), H^{a'}(Y)), is bijective. For a' < b the target is the zero group, so this says that Ext^n_𝒜(X, Y) = 0 for n < b - a; for a' = b it is the identification Ext^{b - a}_𝒜(X, Y) = Hom_𝒜(H^a(X), H^b(Y)).

public theorem bijective_homologyFunctor_shiftMap_of_isLE_of_isGE
    (X Y : DerivedCategory C) (a b n a' : ℤ) [X.IsLE a] [Y.IsGE b]
    (ha' : n + a = a') (hab : a' ≤ b) :
    Function.Bijective (fun f : DerivedCategory.Ext X Y n ↦
      ((homologyFunctor C 0).shiftMap f a a' ha' :
        (homologyFunctor C a).obj X ⟶ (homologyFunctor C a').obj Y))

Tag 06XT, a definition

Tag 06XT in the Stacks Project.

CategoryTheory.Abelian.YonedaExtension, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/ExtAndYonedaExtensions.lean, line 82.

A degree n + 1 Yoneda extension of B by A in an abelian category 𝒜 is an exact sequence 0 → A → Z_n → Z_{n - 1} → ⋯ → Z_0 → B → 0 in 𝒜. It is given by the sequence Z : Fin (n + 1) ⥤ 𝒜 of its middle terms, Z.obj' k = Z_{n - k}, together with the outer maps f : A ⟶ Z.left = Z_n and g : Z.right = Z_0 ⟶ B, and by the exactness of the sequence at each of A, Z_n, …, Z_0 and B. For n = 0 this is a short exact sequence 0 → A → Z_0 → B → 0.

public structure YonedaExtension (B A : 𝒜) (n : ℕ)

CategoryTheory.Abelian.YonedaExtension.Equivalent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/ExtAndYonedaExtensions.lean, line 109.

Two degree n + 1 Yoneda extensions E, E' of B by A in an abelian category are equivalent if there exists a degree n + 1 Yoneda extension E'' of B by A and maps φ : E''.Z ⟶ E.Z and ψ : E''.Z ⟶ E'.Z of the middle terms which are compatible with the maps from A and the maps to B, i.e. such that the two diagrams obtained by putting E'' between E and E' commute, with the identity on A and on B.

public def YonedaExtension.Equivalent (E E' : YonedaExtension B A n) : Prop

Tag 06XU, a lemma

Tag 06XU in the Stacks Project.

CategoryTheory.Abelian.eq_of_isExtClassMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/YonedaClassMap.lean, line 422. The attribute's comment: “uniqueness of the class map”.

There is at most one class map: the degree 1 values are prescribed, and cutting an extension at its left end computes the value in degree n + 2 from a value in degree n + 1.

lemma eq_of_isExtClassMap
    (δ₁ δ₂ : ∀ (B A : 𝒜) (n : ℕ), YonedaExtension B A n → Ext.{w} B A (n + 1))
    (h₁ : IsExtClassMap δ₁) (h₂ : IsExtClassMap δ₂) : δ₁ = δ₂

CategoryTheory.Abelian.extClassMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/YonedaClassMap.lean, line 442. The attribute's comment: “the class map δ itself; isExtClassMap_extClassMap is its two defining properties and eq_of_isExtClassMap their uniqueness”. References: EGA 0 (12.3.2), “canonical map δ”.

The class of a Yoneda extension. It is defined by recursion on the degree: in degree 1 it is the class CategoryTheory.ShortComplex.ShortExact.extClass of the short exact sequence the extension is, and in degree n + 2 it is the class of the extension cut at its left end (cut) composed with the class of the cutting short exact sequence (shortExact_cut). It is the unique such map: isExtClassMap_extClassMap is the pair of properties and eq_of_isExtClassMap their uniqueness.

noncomputable def extClassMap {B : 𝒜} :
    ∀ (n : ℕ) {A : 𝒜}, YonedaExtension B A n → Ext.{w} B A (n + 1)

CategoryTheory.Abelian.extClassMap_eq_of_equivalent, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/YonedaClassMap.lean, line 489. The attribute's comment: “equivalent Yoneda extensions have the same class”. References: EGA 0 (12.3.2), “E~E' ⇒ δE=δE'”; SGA 7 VII (3.2), “c(X, special case”.

Equivalent Yoneda extensions have the same class.

lemma extClassMap_eq_of_equivalent {B A : 𝒜} {n : ℕ} {E E' : YonedaExtension B A n}
    (h : E.Equivalent E') : extClassMap n E = extClassMap n E'

CategoryTheory.Abelian.isExtClassMap_extClassMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/YonedaClassMap.lean, line 523. The attribute's comment: “the two defining properties of the class map”.

The class map has the two properties which pin it down.

lemma isExtClassMap_extClassMap :
    IsExtClassMap (fun (_ _ : 𝒜) (n : ℕ) (E : YonedaExtension _ _ n) => extClassMap.{w} n E)

CategoryTheory.Abelian.surjective_extClassMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/YonedaClassMap.lean, line 608. The attribute's comment: “every element of Ext^{n + 1} is the class of a degree n + 1 Yoneda extension”. References: EGA 0 (12.3.2), “surjectivity of δ”; SGA 7 VII (3.2.5), “partial”.

The class map is surjective: every element of Ext^{n + 1}_𝒜(B, A) is the class of a degree n + 1 Yoneda extension of B by A. The induction is on the degree: an element ξ of Ext^{n + 1}_𝒜(B, A) is killed by a monomorphism A ⟶ Z (exists_shortExact_comp_mk₀_eq_zero), hence, by the covariant long exact sequence of the short exact sequence S : 0 → A → Z → C → 0, of the form ξ = η ∘ δ(S) with η ∈ Ext^n_𝒜(B, C). For n ≥ 1 the inductive hypothesis writes η = δ(E') for a degree n extension E' of B by C, and E' spliced with S is an extension of class ξ (extClassMap_splice). For n = 0, η is a map u : B ⟶ C and the pullback of S along u is a short exact sequence 0 → A → Z ×_C B → B → 0 of class ξ, by naturality of CategoryTheory.ShortComplex.ShortExact.extClass.

lemma surjective_extClassMap (B A : 𝒜) (n : ℕ) :
    Function.Surjective (fun E : YonedaExtension B A n => extClassMap.{w} n E)

CategoryTheory.Abelian.equivalent_of_extClassMap_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/YonedaClassMap.lean, line 880. The attribute's comment: “Yoneda extensions of the same degree with the same class are equivalent”. References: EGA 0 (12.3.2), “δE=δE' ⇒ E~E'”.

Two Yoneda extensions of the same degree with the same class are equivalent.

lemma equivalent_of_extClassMap_eq {B A : 𝒜} {n : ℕ} (E E' : YonedaExtension B A n)
    (h : extClassMap.{w} n E = extClassMap.{w} n E') : E.Equivalent E'

Tag 06XV, a lemma

Tag 06XV in the Stacks Project.

CategoryTheory.Abelian.Ext.extClass_surjective_and_eq_iff_iso_and_baerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/ExtOneAndVanishing.lean, line 247. References: EGA 0 (12.3.2); SGA 7 VII (3.2.5), “partial”.

Ext^1 is the Ext-group of extensions. Let 𝒜 be an abelian category and let A, B be objects of 𝒜. The class δ(E) ∈ Ext^1_𝒜(B, A) of an extension E : 0 → A → E → B → 0 of B by A, i.e. Mathlib's CategoryTheory.ShortComplex.ShortExact.extClass, has the following three properties:

every element of Ext^1_𝒜(B, A) is the class of an extension of B by A;

two extensions of B by A have the same class if and only if they are isomorphic, i.e. there is an isomorphism of their middle terms compatible with the maps from A and to B;

the class of a Baer sum is the sum of the classes: if 0 → A → T → B ⊕ B → 0 is an extension receiving a morphism from the direct sum extension 0 → A ⊕ A → E₁ ⊕ E₂ → B ⊕ B → 0 over the sum map Σ : A ⊕ A → A, and if 0 → A → E → B → 0 maps to it over the diagonal Δ : B → B ⊕ B, then δ(E) = δ(E₁) + δ(E₂).

Hence δ induces an isomorphism from the Ext-group Ext_𝒜(B, A) of isomorphism classes of extensions of B by A under Baer sum onto the group Ext^1_𝒜(B, A).

public theorem Ext.extClass_surjective_and_eq_iff_iso_and_baerSum (B A : 𝒜) :
    (∀ x : Ext.{w} B A 1, ∃ (E : 𝒜) (i : A ⟶ E) (p : E ⟶ B) (w : i ≫ p = 0)
        (h : (ShortComplex.mk i p w).ShortExact), h.extClass = x) ∧
    (∀ (E E' : 𝒜) (i : A ⟶ E) (p : E ⟶ B) (w : i ≫ p = 0) (i' : A ⟶ E') (p' : E' ⟶ B)
        (w' : i' ≫ p' = 0) (h : (ShortComplex.mk i p w).ShortExact)
        (h' : (ShortComplex.mk i' p' w').ShortExact),
        h.extClass = h'.extClass ↔ ∃ φ : E ≅ E', i ≫ φ.hom = i' ∧ φ.hom ≫ p' = p) ∧
    (∀ (E₁ E₂ E T : 𝒜) (i₁ : A ⟶ E₁) (p₁ : E₁ ⟶ B) (w₁ : i₁ ≫ p₁ = 0)
        (i₂ : A ⟶ E₂) (p₂ : E₂ ⟶ B) (w₂ : i₂ ≫ p₂ = 0)
        (i : A ⟶ E) (p : E ⟶ B) (w : i ≫ p = 0)
        (j : A ⟶ T) (q : T ⟶ B ⊞ B) (wT : j ≫ q = 0)
        (h₁ : (ShortComplex.mk i₁ p₁ w₁).ShortExact)
        (h₂ : (ShortComplex.mk i₂ p₂ w₂).ShortExact)
        (h : (ShortComplex.mk i p w).ShortExact)
        (_hT : (ShortComplex.mk j q wT).ShortExact)
        (u : E₁ ⊞ E₂ ⟶ T) (v : E ⟶ T),
        biprod.map i₁ i₂ ≫ u = biprod.desc (𝟙 A) (𝟙 A) ≫ j →
        u ≫ q = biprod.map p₁ p₂ →
        i ≫ v = j → v ≫ q = p ≫ biprod.lift (𝟙 B) (𝟙 B) →
          h.extClass = h₁.extClass + h₂.extClass)

Tag 0GSM, a lemma

Tag 0GSM in the Stacks Project.

CategoryTheory.ShortComplex.ShortExact.extClass_comp_extClass_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/ExtOneAndVanishing.lean, line 432.

Vanishing of a Yoneda product of two extension classes. Let 0 → A → Z → B → 0 and 0 → B → Z' → C → 0 be short exact sequences in an abelian category 𝒜, with classes [Z] ∈ Ext^1_𝒜(B, A) and [Z'] ∈ Ext^1_𝒜(C, B). Then the Yoneda product [Z] ∘ [Z'] ∈ Ext^2_𝒜(C, A) is zero if and only if there is a commutative diagram with exact rows and columns
                 0             0
                 ↓             ↓
  0 →   A   →    Z     →       B      →  0
      ‖ 1 ‖      ↓             ↓
  0 →   A   →    W     →       Z'     →  0
                 ↓             ↓
                 C   → ‖ 1 ‖ → C
                 ↓             ↓
                 0             0
in 𝒜, i.e. if and only if 0 → A → Z → B → 0 is the restriction along B → Z' of an extension 0 → A → W → Z' → 0 of Z' by A.

public theorem extClass_comp_extClass_eq_zero_iff {A Z B Z' C : 𝒜}
    {f : A ⟶ Z} {g : Z ⟶ B} {hfg : f ≫ g = 0}
    (hS : (ShortComplex.mk f g hfg).ShortExact)
    {f' : B ⟶ Z'} {g' : Z' ⟶ C} {hf'g' : f' ≫ g' = 0}
    (hS' : (ShortComplex.mk f' g' hf'g').ShortExact) :
    hS'.extClass.comp hS.extClass rfl = 0 ↔
      ∃ (W : 𝒜) (a : A ⟶ W) (q : W ⟶ Z') (i : Z ⟶ W) (p : W ⟶ C)
        (haq : a ≫ q = 0) (hip : i ≫ p = 0),
        (ShortComplex.mk a q haq).ShortExact ∧ (ShortComplex.mk i p hip).ShortExact ∧
          f ≫ i = a ∧ i ≫ q = g ≫ f' ∧ q ≫ g' = p

Tag 0EWW, a lemma

Tag 0EWW in the Stacks Project.

CategoryTheory.hasProjectiveDimensionLT_of_forall_ext_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/ExtOneAndVanishing.lean, line 324.

Vanishing of Ext^p_𝒜(X, -) forces projective dimension < p. If 𝒜 is an abelian category and Ext^p_𝒜(X, Y) = 0 for every object Y of 𝒜, then X has projective dimension < p, i.e. Ext^i_𝒜(X, Y) = 0 for every i ≥ p and every Y. This generalizes CategoryTheory.hasProjectiveDimensionLT_of_enoughInjectives by dropping the assumption [EnoughInjectives 𝒜]. [Stacks, Tag 0EWW] states the reading for all pairs of objects at once, which follows by applying this to every object of 𝒜.

public theorem hasProjectiveDimensionLT_of_forall_ext_eq_zero (X : 𝒜) (p : ℕ)
    (h : ∀ (Y : 𝒜) (e : Abelian.Ext.{w} X Y p), e = 0) : HasProjectiveDimensionLT X p

Tag 0GM4, a lemma

Tag 0GM4 in the Stacks Project.

DerivedCategory.nonempty_iso_biproduct_singleFunctor_obj_homology_of_forall_ext_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/SplittingAndResolutions.lean, line 365.

A bounded complex with no higher Ext between its cohomologies is the sum of them. Let 𝒜 be an abelian category and let K be an object of D(𝒜) whose cohomology vanishes outside [a, b]. If Ext^p_𝒜(H^i(K), H^j(K)) = 0 for all p ≥ 2 and all i > j, then K is isomorphic to the direct sum ⨁_{a ≤ i ≤ b} H^i(K)[-i] of its cohomologies. The isomorphism depends on choices of splittings, so only its existence is asserted. For a = b this is DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE.

public theorem nonempty_iso_biproduct_singleFunctor_obj_homology_of_forall_ext_eq_zero
    (K : DerivedCategory C) (a b : ℤ) [K.IsGE a] [K.IsLE b]
    (h : ∀ (i j : ℤ) (p : ℕ), j < i → 2 ≤ p →
      ∀ e : Abelian.Ext.{w'} ((homologyFunctor C i).obj K) ((homologyFunctor C j).obj K) p,
        e = 0) :
    Nonempty (K ≅ ⨁ fun i : Finset.Icc a b =>
      (singleFunctor C i.1).obj ((homologyFunctor C i.1).obj K))

Tag 0EWX, a lemma

Tag 0EWX in the Stacks Project.

DerivedCategory.nonempty_iso_biproduct_singleFunctor_obj_homology_of_forall_ext_two_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/Basic/SplittingAndResolutions.lean, line 413.

A bounded complex over a category with no Ext² is the sum of its cohomologies. Let 𝒜 be an abelian category with Ext²_𝒜(B, A) = 0 for every pair of objects A, B, and let K be an object of D(𝒜) whose cohomology vanishes outside [a, b]. Then K is isomorphic to the direct sum ⨁_{a ≤ i ≤ b} H^i(K)[-i] of its cohomologies. The isomorphism depends on choices of splittings, so only its existence is asserted. This is the special case of DerivedCategory.nonempty_iso_biproduct_singleFunctor_obj_homology_of_forall_ext_eq_zero ([Stacks, Tag 0GM4]) in which the vanishing of Ext^p, p ≥ 2, comes from the category rather than from K, via [Stacks, Tag 0EWW].

public theorem nonempty_iso_biproduct_singleFunctor_obj_homology_of_forall_ext_two_eq_zero
    (K : DerivedCategory C) (a b : ℤ) [K.IsGE a] [K.IsLE b]
    (h : ∀ (A B : C) (e : Abelian.Ext.{w'} B A 2), e = 0) :
    Nonempty (K ≅ ⨁ fun i : Finset.Icc a b =>
      (singleFunctor C i.1).obj ((homologyFunctor C i.1).obj K))

Sources

LeanCategoryTheory.DerivedCategory.Ext · CategoryTheory.Abelian.zExt · DerivedCategory.surjective_extZero_comp_iff_surjective_comp · ExtByResolutions.ext_via_injective_resolution_bijective · ExtByResolutions.ext_via_projective_resolution_bijective · DerivedCategory.bijective_homologyFunctor_shiftMap_of_isLE_of_isGE · CategoryTheory.Abelian.YonedaExtension · CategoryTheory.Abelian.YonedaExtension.Equivalent

Section13.28 K-groups #

Section 13.28 of the Stacks Project, Tag 0FCM. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FCN, a definition

Tag 0FCN in the Stacks Project.

CategoryTheory.Pretriangulated.K0, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/KGroup/Defs.lean, line 41. The attribute's comment: “stated for a pretriangulated category: the free abelian group and its relations use only the class of distinguished triangles, never the octahedron axiom”. References: SGA 6 I (6.3), “triangulated case”; SGA 6 IV (1.1), “the group k(C)”.

The zeroth K-group K₀(C) of a pretriangulated category C: the free abelian group on the objects of C modulo the subgroup generated by the elements [Y] - [X] - [Z], one for each distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧ of C. The class of an object X is QuotientAddGroup.mk (FreeAbelianGroup.of X).

abbrev K0 (C : Type u) [Category.{v} C] [HasZeroObject C] [HasShift C ℤ] [Preadditive C]
    [∀ n : ℤ, (CategoryTheory.shiftFunctor C n).Additive] [Pretriangulated C] : Type u

Tag 0FCP, a lemma

Tag 0FCP in the Stacks Project.

DerivedCategory.Bounded.exists_addEquiv_K0, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/KGroup.lean, line 658.

The zeroth K-group of D^b(A) is that of A: for an abelian category A there is a group isomorphism from the zeroth K-group of A (the free abelian group on the objects of A modulo [X₂] - [X₁] - [X₃] for every short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0) to the zeroth K-group of the bounded derived category of A, sending the class of X to the class of X viewed as a complex in degree 0. Such an isomorphism is unique, since the classes of objects generate K₀(A).

theorem DerivedCategory.Bounded.exists_addEquiv_K0 {A : Type u} [Category.{v} A]
    [Abelian A] [HasDerivedCategory.{w} A] :
    ∃ e : KZero A ≃+ Pretriangulated.K0 (DerivedCategory.Bounded A),
      ∀ X : A, e (KZero.mk A X) =
        QuotientAddGroup.mk (FreeAbelianGroup.of
          (⟨(DerivedCategory.singleFunctor A 0).obj X,
            ⟨⟨0, inferInstance⟩, ⟨0, inferInstance⟩⟩⟩ : DerivedCategory.Bounded A))

Tag 0FCQ, a lemma

Tag 0FCQ in the Stacks Project.

CategoryTheory.Pretriangulated.K0.map, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/KGroup/Basic.lean, line 112. The attribute's comment: “the homomorphism itself; map_cls is its defining property and map_unique is its uniqueness”. References: SGA 6 I (6.3), “triangulated case”.

The homomorphism K₀(F) : K₀(C) → K₀(D), [X] ↦ [F(X)], induced by an exact functor F : C ⥤ D: the image under F of a distinguished triangle is distinguished, so the lift of X ↦ [F(X)] to the free abelian group kills the defining relations.

noncomputable def map (F : C ⥤ D) [F.CommShift ℤ] [F.IsTriangulated] : K0 C →+ K0 D

CategoryTheory.Pretriangulated.K0.map_cls, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/KGroup/Basic.lean, line 123. The attribute's comment: “the defining property of map”.

K₀(F) sends the class of an object X of C to the class of F(X).

theorem map_cls (F : C ⥤ D) [F.CommShift ℤ] [F.IsTriangulated] (X : C) :
    map F (cls X) = cls (F.obj X)

CategoryTheory.Pretriangulated.K0.map_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/KGroup/Basic.lean, line 130. The attribute's comment: “uniqueness of map”.

K₀(F) is the only homomorphism K₀(C) → K₀(D) sending [X] to [F(X)] for every object X of C.

theorem map_unique (F : C ⥤ D) [F.CommShift ℤ] [F.IsTriangulated] (φ : K0 C →+ K0 D)
    (hφ : ∀ X : C, φ (cls X) = cls (F.obj X)) : φ = map F

Tag 0FCR, a lemma

Tag 0FCR in the Stacks Project.

K0_homomorphism_of_homological, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/KGroup/Basic.lean, line 570.

Stacks Lemma 13.28.4 (tag 0FCR). Let H : D → A be a homological functor from a triangulated category to an abelian category, such that for every object X of D only finitely many of the objects H(X[i]), i ∈ ℤ, are nonzero. Then there is a well-defined group homomorphism K_0(D) → K_0(A) characterized by [X] ↦ ∑_{i ∈ ℤ} (-1)^i [H(X[i])].

theorem K0_homomorphism_of_homological (H : D ⥤ A) (hH : H.IsHomological)
    (hfin : ∀ X : D, {i : ℤ | ¬ IsZero (H.obj ((shiftFunctor D i).obj X))}.Finite) :
    ∃ φ : K0 D →+ KZero A, ∀ X : D, φ (K0.cls X) = eulerClass D A H X

Tag 0FCS, a lemma

Tag 0FCS in the Stacks Project.

DerivedCategory.exists_addEquiv_K0_of_isWeakSerreClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/KGroup.lean, line 955.

The zeroth K-group of D^b_B(A) is that of B: for a weak Serre subcategory B of an abelian category A there is a group isomorphism from the zeroth K-group of B (the free abelian group on the objects of B modulo [X₂] - [X₁] - [X₃] for every short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of B) to the zeroth K-group of the triangulated subcategory D^b_B(A) ⊆ D(A) of bounded objects with all cohomology objects in B, sending the class of X to the class of X viewed as a complex in degree 0. Such an isomorphism is unique, since the classes of objects generate K₀(B).

theorem DerivedCategory.exists_addEquiv_K0_of_isWeakSerreClass
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    (B : ObjectProperty A) [B.IsWeakSerreClass]
    {P : ObjectProperty (DerivedCategory A)}
    (hP : P = (DerivedCategory.TStructure.t (C := A)).bounded ⊓
      fun X ↦ ∀ n : ℤ, B ((DerivedCategory.homologyFunctor A n).obj X))
    [P.IsTriangulated] :
    ∃ e : KZero B.FullSubcategory ≃+ Pretriangulated.K0 P.FullSubcategory,
      (∀ X : B.FullSubcategory, ∃ Y : P.FullSubcategory,
          Nonempty (P.ι.obj Y ≅ (DerivedCategory.singleFunctor A 0).obj (B.ι.obj X))) ∧
        ∀ (X : B.FullSubcategory) (Y : P.FullSubcategory),
          (P.ι.obj Y ≅ (DerivedCategory.singleFunctor A 0).obj (B.ι.obj X)) →
            e (KZero.mk B.FullSubcategory X) =
              QuotientAddGroup.mk (FreeAbelianGroup.of Y)

Tag 0FCT, a lemma

Tag 0FCT in the Stacks Project.

CategoryTheory.Pretriangulated.K0.exists_bilinear_of_bifunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/KGroup/Basic.lean, line 661.

Stacks Tag 0FCT (Lemma 13.28.6). Let D, D', D'' be triangulated categories and let F : D ⥤ (D' ⥤ D'') be a (curried) bifunctor ⊗ : D × D' → D''. Assume that

for each object X of D, the partial functor X ⊗ - = F.obj X : D' → D'' is an exact functor of triangulated categories (it admits a shift-commutation structure csR X and is triangulated for it), and

for each object X' of D', the partial functor - ⊗ X' = F.flip.obj X' : D → D'' is an exact functor of triangulated categories (it admits a shift-commutation structure csL X' and is triangulated for it).

Then ⊗ induces a bilinear map K_0(D) × K_0(D') → K_0(D'') sending the pair of classes ([X], [X']) to [X ⊗ X'].

The bilinear map is encoded as b : K0 D →+ (K0 D' →+ K0 D''): additivity of b in the second variable is built into the AddMonoidHom codomain, and additivity in the first variable is built into b itself being an AddMonoidHom.

theorem exists_bilinear_of_bifunctor
    (F : D ⥤ (D' ⥤ D''))
    (csR : ∀ X : D, (F.obj X).CommShift ℤ)
    (hR : ∀ X : D, letI := csR X; (F.obj X).IsTriangulated)
    (csL : ∀ X' : D', (F.flip.obj X').CommShift ℤ)
    (hL : ∀ X' : D', letI := csL X'; (F.flip.obj X').IsTriangulated) :
    ∃ b : K0 D →+ (K0 D' →+ K0 D''),
      ∀ (X : D) (X' : D'), b (cls X) (cls X') = cls ((F.obj X).obj X')

Sources

LeanCategoryTheory.Pretriangulated.K0 · DerivedCategory.Bounded.exists_addEquiv_K0 · CategoryTheory.Pretriangulated.K0.map · CategoryTheory.Pretriangulated.K0.map_cls · CategoryTheory.Pretriangulated.K0.map_unique · K0_homomorphism_of_homological · DerivedCategory.exists_addEquiv_K0_of_isWeakSerreClass · CategoryTheory.Pretriangulated.K0.exists_bilinear_of_bifunctor

Section13.29 Unbounded complexes #

Section 13.29 of the Stacks Project, Tag 06XW. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06XX, a lemma

Tag 06XX in the Stacks Project.

CochainComplex.exists_sequence_quasiIso_truncLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/UnboundedComplexes/TruncLEResolutions.lean, line 443.

Stacks 06XX. Let A be an abelian category and let P be a class of objects of A which contains a zero object, is closed under finite direct sums, and is such that every object of A is a quotient of an object satisfying P. Let K be a cochain complex. Then there are complexes Q n, quasi-isomorphisms f n : Q n ⟶ τ_{≤ n} K and morphisms g n : Q n ⟶ Q (n + 1) forming a commutative ladder over the canonical truncations of K, such that (1) each f n is degreewise epimorphic, (2) each Q n is bounded above with all terms satisfying P, and (3) each g n is degreewise a split injection whose cokernel satisfies P.

public theorem exists_sequence_quasiIso_truncLE (P : ObjectProperty A) [P.ContainsZero]
    (hsum : ∀ X Y : A, P X → P Y → P (X ⊞ Y))
    (hP : ∀ X : A, ∃ (Y : A) (_ : P Y) (p : Y ⟶ X), Epi p) (K : CochainComplex A ℤ) :
    ∃ (Q : ℕ → CochainComplex A ℤ) (f : ∀ n : ℕ, Q n ⟶ K.truncLE n)
      (g : ∀ n : ℕ, Q n ⟶ Q (n + 1)),
      (∀ n, QuasiIso (f n)) ∧ (∀ (n : ℕ) (i : ℤ), Epi ((f n).f i)) ∧
        (∀ n : ℕ, (Q n).IsStrictlyLE n) ∧ (∀ (n : ℕ) (i : ℤ), P ((Q n).X i)) ∧
        (∀ (n : ℕ) (i : ℤ), ∃ (C : A) (_ : P C) (e : (Q (n + 1)).X i ≅ (Q n).X i ⊞ C),
          (g n).f i ≫ e.hom = biprod.inl) ∧
        (∀ n : ℕ, g n ≫ f (n + 1) ≫ K.ιTruncLE ((n + 1 : ℕ) : ℤ)
          = f n ≫ K.ιTruncLE ((n : ℕ) : ℤ))

Tag 0794, a proposition

Tag 0794 in the Stacks Project.

CategoryTheory.Functor.hasPointwiseLeftDerivedFunctor_of_acyclic_mapHomologicalComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/UnboundedComplexes/LeftDerivedFunctor.lean, line 417.

Stacks 0794. Let F : 𝒜 ⥤ ℬ be a right exact functor of abelian categories and let P be a class of objects of 𝒜 which contains a zero object, is closed under finite direct sums, and is such that every object of 𝒜 is a quotient of an object satisfying P. Assume that

F turns every bounded above acyclic complex with all terms satisfying P into an acyclic complex,

𝒜 and ℬ have colimits of systems indexed by ℕ,

those colimits are exact in both 𝒜 and ℬ, and

F commutes with them.

Then the left derived functor LF of K(𝒜) ⥤ D(ℬ), K ↦ F(K), along the localization Qh : K(𝒜) ⥤ D(𝒜) at quasi-isomorphisms is defined at every object, i.e. LF is defined on all of D(𝒜).

public theorem hasPointwiseLeftDerivedFunctor_of_acyclic_mapHomologicalComplex
    (F : A ⥤ B) [F.Additive] [PreservesFiniteColimits F]
    (P : ObjectProperty A) [P.ContainsZero]
    (hsum : ∀ X Y : A, P X → P Y → P (X ⊞ Y))
    (hP : ∀ X : A, ∃ (Y : A) (_ : P Y) (p : Y ⟶ X), Epi p)
    (hFP : ∀ (a : ℤ) (L : CochainComplex A ℤ), L.IsStrictlyLE a → (∀ n, P (L.X n)) →
      L.Acyclic → ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj L).Acyclic)
    [HasColimitsOfShape ℕ A] [HasColimitsOfShape ℕ B]
    [HasExactColimitsOfShape ℕ A] [HasExactColimitsOfShape ℕ B]
    [PreservesColimitsOfShape ℕ F] :
    (F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).HasPointwiseLeftDerivedFunctor
      (HomotopyCategory.quasiIso A (ComplexShape.up ℤ))

Tag 070F, a lemma

Tag 070F in the Stacks Project.

CochainComplex.exists_sequence_quasiIso_truncGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/UnboundedComplexes/TruncGEResolutions.lean, line 468.

Stacks 070F. Let A be an abelian category and let P be a class of objects of A which contains a zero object, is closed under finite products, and is such that every object of A is a subobject of an object satisfying P. Let K be a cochain complex. Then there are complexes I n, quasi-isomorphisms f n : τ_{≥ -n} K ⟶ I n and morphisms g n : I (n + 1) ⟶ I n forming a commutative ladder under the canonical truncations of K, such that (1) each f n is degreewise monomorphic, (2) each I n is bounded below with all terms satisfying P, and (3) each g n is degreewise a split surjection whose kernel satisfies P. This is the dual of Stacks 06XX.

public theorem exists_sequence_quasiIso_truncGE (P : ObjectProperty A) [P.ContainsZero]
    (hprod : ∀ X Y : A, P X → P Y → P (X ⊞ Y))
    (hP : ∀ X : A, ∃ (Y : A) (_ : P Y) (i : X ⟶ Y), Mono i) (K : CochainComplex A ℤ) :
    ∃ (I : ℕ → CochainComplex A ℤ) (f : ∀ n : ℕ, K.truncGE (-(n : ℤ)) ⟶ I n)
      (g : ∀ n : ℕ, I (n + 1) ⟶ I n),
      (∀ n, QuasiIso (f n)) ∧ (∀ (n : ℕ) (i : ℤ), Mono ((f n).f i)) ∧
        (∀ n : ℕ, (I n).IsStrictlyGE (-(n : ℤ))) ∧ (∀ (n : ℕ) (i : ℤ), P ((I n).X i)) ∧
        (∀ (n : ℕ) (i : ℤ), ∃ (C : A) (_ : P C) (e : (I (n + 1)).X i ≅ (I n).X i ⊞ C),
          e.inv ≫ (g n).f i = biprod.fst) ∧
        (∀ n : ℕ, K.πTruncGE (-((n + 1 : ℕ) : ℤ)) ≫ f (n + 1) ≫ g n
          = K.πTruncGE (-(n : ℤ)) ≫ f n)

Sources

LeanCochainComplex.exists_sequence_quasiIso_truncLE · CategoryTheory.Functor.hasPointwiseLeftDerivedFunctor_of_acyclic_mapHomologicalComplex · CochainComplex.exists_sequence_quasiIso_truncGE

Section13.30 Deriving adjoints #

Section 13.30 of the Stacks Project, Tag 0FNC. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FND, a lemma

Tag 0FND in the Stacks Project.

CategoryTheory.Adjunction.existsUnique_homEquiv_of_isRightDerivedValueAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/DerivingAdjoints.lean, line 593. References: SGA 4 XVII (2.3.7), “outer Hom bijection”.

Stacks 0FND: deriving adjoints. Let F : 𝒟 ⥤ 𝒟' be right adjoint to G : 𝒟' ⥤ 𝒟, let S, S' be classes of morphisms of 𝒟, 𝒟' admitting left, resp. right fractions, and let Q : 𝒟 ⥤ S⁻¹𝒟 and Q' : 𝒟' ⥤ (S')⁻¹𝒟' be localization functors. Let K be an object of 𝒟 at which the right derived functor RF of Q' ∘ F is defined, with value RF(K) = c.pt, and let M be an object of 𝒟' at which the left derived functor LG of Q ∘ G is defined, with value LG(M) = d.pt.unop (the left derived value is the right derived value of the opposite functors, as in Stacks 05S9). Then there is a unique bijection Hom_{(S')⁻¹𝒟'}(M, RF(K)) ≃ Hom_{S⁻¹𝒟}(LG(M), K) compatible with the fractions computing the two sides: for every index s : K ⟶ I of the ind-object defining RF(K), every index t : P ⟶ M of the pro-object defining LG(M) and every f : P ⟶ F(I), a morphism ψ : M ⟶ RF(K) satisfies Q'(t) ≫ ψ = Q'(f) ≫ (coprojection at s) if and only if its image satisfies φ(ψ) ≫ Q(s) = (projection at t) ≫ Q(f^♯), where f^♯ : G(P) ⟶ I is adjoint to f.

theorem existsUnique_homEquiv_of_isRightDerivedValueAt
    {D : Type u₁} [Category.{v₁} D] {D' : Type u₂} [Category.{v₂} D']
    {SD : Type u₃} [Category.{v₃} SD] {SD' : Type u₄} [Category.{v₄} SD']
    {F : D ⥤ D'} {G : D' ⥤ D} (adj : G ⊣ F)
    (S : MorphismProperty D) (S' : MorphismProperty D')
    [S.HasLeftCalculusOfFractions] [S'.HasRightCalculusOfFractions]
    (Q : D ⥤ SD) [Q.IsLocalization S] (Q' : D' ⥤ SD') [Q'.IsLocalization S']
    (K : D) (M : D')
    (c : Cocone (MorphismProperty.Under.forget S ⊤ K ⋙ Under.forget K ⋙ F ⋙ Q'))
    (hc : (F ⋙ Q').IsRightDerivedValueAt S K c)
    (d : Cocone (MorphismProperty.Under.forget S'.op ⊤ (Opposite.op M) ⋙
      Under.forget (Opposite.op M) ⋙ (G ⋙ Q).op))
    (hd : (G ⋙ Q).op.IsRightDerivedValueAt S'.op (Opposite.op M) d) :
    ∃! φ : (Q'.obj M ⟶ c.pt) ≃ (d.pt.unop ⟶ Q.obj K),
      ∀ (s : S.Under ⊤ K) (t : S'.op.Under ⊤ (Opposite.op M))
        (f : t.right.unop ⟶ F.obj s.right) (ψ : Q'.obj M ⟶ c.pt),
        Q'.map t.hom.unop ≫ ψ = Q'.map f ≫ c.ι.app s ↔
          φ ψ ≫ Q.map s.hom = (d.ι.app t).unop ≫ Q.map ((adj.homEquiv _ _).symm f)

Tag 0DVC, a lemma

Tag 0DVC in the Stacks Project.

CategoryTheory.Adjunction.existsUnique_homEquiv_derivedCategory_of_isRightDerivedValueAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/DerivingAdjoints.lean, line 830.

Stacks 0DVC: deriving adjoints between derived categories. Let F : 𝒜 ⥤ ℬ be right adjoint to G : ℬ ⥤ 𝒜, functors of abelian categories, let K be a complex of 𝒜 and M a complex of ℬ, and let RF, resp. LG, be the right, resp. left, derived functor of K(𝒜) ⥤ K(ℬ) ⥤ D(ℬ), resp. K(ℬ) ⥤ K(𝒜) ⥤ D(𝒜), with respect to the quasi-isomorphisms. Assume RF is defined at K, with value RF(K) = c.pt, and LG is defined at M, with value LG(M) = d.pt (Stacks 05S9). Then there is a unique bijection Hom_{D(ℬ)}(M, RF(K)) ≃ Hom_{D(𝒜)}(LG(M), K) compatible with the fractions computing the two sides: for every index s : K ⟶ I of the ind-object defining RF(K), every index t : P ⟶ M of the pro-object defining LG(M) and every pair of chain maps f : P ⟶ F(I), g : G(P) ⟶ I that are adjoint to one another in each degree, a morphism ψ : M ⟶ RF(K) satisfies Qh(t) ≫ ψ = Qh(f) ≫ (coprojection at s) if and only if its image satisfies φ(ψ) ≫ Qh(s) = (projection at t) ≫ Qh(g).

theorem existsUnique_homEquiv_derivedCategory_of_isRightDerivedValueAt
    {A : Type u₁} [Category.{v₁} A] [Abelian A] [HasDerivedCategory.{w₁} A]
    {B : Type u₂} [Category.{v₂} B] [Abelian B] [HasDerivedCategory.{w₂} B]
    {F : A ⥤ B} {G : B ⥤ A} [F.Additive] [G.Additive] (adj : G ⊣ F)
    (K : HomotopyCategory A (ComplexShape.up ℤ)) (M : HomotopyCategory B (ComplexShape.up ℤ))
    (c : Cocone (MorphismProperty.Under.forget
        (HomotopyCategory.quasiIso A (ComplexShape.up ℤ)) ⊤ K ⋙
      Under.forget K ⋙ F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh))
    (hc : (F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).IsRightDerivedValueAt
      (HomotopyCategory.quasiIso A (ComplexShape.up ℤ)) K c)
    (d : Cone (MorphismProperty.Over.forget
        (HomotopyCategory.quasiIso B (ComplexShape.up ℤ)) ⊤ M ⋙
      Over.forget M ⋙ G.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh))
    (hd : (G.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).IsLeftDerivedValueAt
      (HomotopyCategory.quasiIso B (ComplexShape.up ℤ)) M d) :
    ∃! φ : (DerivedCategory.Qh.obj M ⟶ c.pt) ≃ (d.pt ⟶ DerivedCategory.Qh.obj K),
      ∀ (s : (HomotopyCategory.quasiIso A (ComplexShape.up ℤ)).Under ⊤ K)
        (t : (HomotopyCategory.quasiIso B (ComplexShape.up ℤ)).Over ⊤ M)
        (f : t.left.as ⟶ (F.mapHomologicalComplex (ComplexShape.up ℤ)).obj s.right.as)
        (g : (G.mapHomologicalComplex (ComplexShape.up ℤ)).obj t.left.as ⟶ s.right.as),
        (∀ n, f.f n = adj.homEquiv _ _ (g.f n)) →
        ∀ ψ : DerivedCategory.Qh.obj M ⟶ c.pt,
          DerivedCategory.Qh.map t.hom ≫ ψ =
              DerivedCategory.Qh.map
                ((HomotopyCategory.quotient B (ComplexShape.up ℤ)).map f) ≫ c.ι.app s ↔
            φ ψ ≫ DerivedCategory.Qh.map s.hom =
              d.π.app t ≫ DerivedCategory.Qh.map
                ((HomotopyCategory.quotient A (ComplexShape.up ℤ)).map g)

Tag 09T5, a lemma

Tag 09T5 in the Stacks Project.

CategoryTheory.Adjunction.exists_derived_of_isRightDerivedValueAt_of_isLeftDerivedValueAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/DerivingAdjoints.lean, line 1246.

Stacks 09T5: the derived functors of an adjoint pair are adjoint. Let F : 𝒟 ⥤ 𝒟' be right adjoint to G : 𝒟' ⥤ 𝒟, let S, S' be classes of morphisms of 𝒟, 𝒟' admitting left, resp. right fractions, and let Q : 𝒟 ⥤ S⁻¹𝒟, Q' : 𝒟' ⥤ (S')⁻¹𝒟' be localization functors. Let RF : S⁻¹𝒟 ⥤ (S')⁻¹𝒟' with β : F ⋙ Q' ⟶ Q ⋙ RF be the right derived functor of Q' ∘ F, in the sense that for every object K of 𝒟 the ind-object (s : K ⟶ I) ↦ Q'(F(I)) is essentially constant with value RF(Q(K)) and coprojections induced by β (Stacks 05S9), and let LG : (S')⁻¹𝒟' ⥤ S⁻¹𝒟 with α : Q' ⋙ LG ⟶ G ⋙ Q be the left derived functor of Q ∘ G, in the dual sense. Then LG is left adjoint to RF, by an adjunction whose unit and counit are compatible with α, β and the adjunction between F and G.

theorem exists_derived_of_isRightDerivedValueAt_of_isLeftDerivedValueAt
    {D : Type u₁} [Category.{v₁} D] {D' : Type u₂} [Category.{v₂} D']
    {SD : Type u₃} [Category.{v₃} SD] {SD' : Type u₄} [Category.{v₄} SD']
    {F : D ⥤ D'} {G : D' ⥤ D} (adj : G ⊣ F)
    (S : MorphismProperty D) (S' : MorphismProperty D')
    [S.HasLeftCalculusOfFractions] [S'.HasRightCalculusOfFractions]
    (Q : D ⥤ SD) [Q.IsLocalization S] (Q' : D' ⥤ SD') [Q'.IsLocalization S']
    (RF : SD ⥤ SD') (β : F ⋙ Q' ⟶ Q ⋙ RF)
    (LG : SD' ⥤ SD) (α : Q' ⋙ LG ⟶ G ⋙ Q)
    (hRF : ∀ K : D, ∃ (c : Cocone (MorphismProperty.Under.forget S ⊤ K ⋙
          Under.forget K ⋙ F ⋙ Q'))
        (_ : (F ⋙ Q').IsRightDerivedValueAt S K c) (e : c.pt ≅ RF.obj (Q.obj K)),
        ∀ s : S.Under ⊤ K, c.ι.app s ≫ e.hom ≫ RF.map (Q.map s.hom) = β.app s.right)
    (hLG : ∀ M : D', ∃ (d : Cone (MorphismProperty.Over.forget S' ⊤ M ⋙
          Over.forget M ⋙ G ⋙ Q))
        (_ : (G ⋙ Q).IsLeftDerivedValueAt S' M d) (e : LG.obj (Q'.obj M) ≅ d.pt),
        ∀ t : S'.Over ⊤ M, LG.map (Q'.map t.hom) ≫ e.hom ≫ d.π.app t = α.app t.left) :
    ∃ adj' : LG ⊣ RF,
      (∀ M : D', adj'.unit.app (Q'.obj M) ≫ RF.map (α.app M) =
          Q'.map (adj.unit.app M) ≫ β.app (G.obj M)) ∧
        (∀ K : D, LG.map (β.app K) ≫ adj'.counit.app (Q.obj K) =
          α.app (F.obj K) ≫ Q.map (adj.counit.app K))

Sources

LeanCategoryTheory.Adjunction.existsUnique_homEquiv_of_isRightDerivedValueAt · CategoryTheory.Adjunction.existsUnique_homEquiv_derivedCategory_of_isRightDerivedValueAt · CategoryTheory.Adjunction.exists_derived_of_isRightDerivedValueAt_of_isLeftDerivedValueAt

Section13.31 K-injective complexes #

Section 13.31 of the Stacks Project, Tag 070G. 9 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 070H, a definition

Tag 070H in the Stacks Project.

Declarations registered for the tag:

CochainComplex.IsKInjective registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch13.lean, line 15 (StacksFrontier): “definition: every chain map from an acyclic complex is null-homotopic”.
CochainComplex.isKInjective_iff_rightOrthogonal registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch13.lean, line 17 (StacksFrontier): “Hom_{K(A)}(M, I) = 0 for every acyclic M”.

Tag 070I, a lemma

Tag 070I in the Stacks Project.

CochainComplex.isKInjective_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/KInjective/Locality.lean, line 549.

Stacks 070I. Let A be an abelian category and I a cochain complex in A. The following are equivalent: (1) I is K-injective; (2) for every quasi-isomorphism M ⟶ N in K(A), precomposition Hom_{K(A)}(N, I) → Hom_{K(A)}(M, I) is bijective; (3) for every N in K(A), the localization map Hom_{K(A)}(N, I) → Hom_{D(A)}(N, I) is bijective.

public theorem isKInjective_tfae {A : Type u} [Category.{v} A] [Abelian A]
    [HasDerivedCategory.{w} A] (I : CochainComplex A ℤ) :
    List.TFAE
      [I.IsKInjective,
        (HomotopyCategory.quasiIso A (ComplexShape.up ℤ)).isLocal
          ((HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj I),
        ∀ N : HomotopyCategory A (ComplexShape.up ℤ),
          Function.Bijective (DerivedCategory.Qh.map :
            (N ⟶ (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj I) → _)]

Tag 090X, a lemma

Tag 090X in the Stacks Project.

CochainComplex.isKInjective_two_out_of_three_of_distTriang, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/KInjective/Locality.lean, line 569.

Stacks 090X. Let A be an abelian category and let (K, L, M, f, g, h) be a distinguished triangle of the homotopy category K(A) of cochain complexes in A, where K, L, M are cochain complexes. If two out of K, L, M are K-injective, then so is the third.

public theorem isKInjective_two_out_of_three_of_distTriang
    {A : Type u} [Category.{v} A] [Abelian A] {K L M : CochainComplex A ℤ}
    (f : (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj K ⟶
      (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj L)
    (g : (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj L ⟶
      (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj M)
    (h : (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj M ⟶
      ((HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj K)⟦(1 : ℤ)⟧)
    (hT : Triangle.mk f g h ∈ distTriang (HomotopyCategory A (ComplexShape.up ℤ))) :
    (L.IsKInjective → M.IsKInjective → K.IsKInjective) ∧
      (K.IsKInjective → M.IsKInjective → L.IsKInjective) ∧
      (K.IsKInjective → L.IsKInjective → M.IsKInjective)

Tag 070J, a lemma

Tag 070J in the Stacks Project.

Declarations registered for the tag:

CochainComplex.isKInjective_of_injective registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch13.lean, line 20 (StacksFrontier).

Tag 0BK6, a lemma

Tag 0BK6 in the Stacks Project.

Stacks.Injectives.KInjectiveProduct.product_isKInjective, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/KInjective/AdjointAndProducts.lean, line 345.

Statement 1. A product of K-injective complexes is K-injective.

alias product_isKInjective

Stacks.Injectives.KInjectiveProduct.product_repr_derived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/KInjective/AdjointAndProducts.lean, line 409.

Statement 2. The product complex ∏ᶜ X represents the product of the family (I_t) in the derived category D(A): for every complex K, the natural comparison map Hom_{D(A)}(K, ∏ᶜ X) → ∏ₜ Hom_{D(A)}(K, I_t) induced by the projections is a bijection (hence an isomorphism of abelian groups).

theorem product_repr_derived [HasDerivedCategory C]
    {T : Type} (X : T → CochainComplex C ℤ)
    [∀ n : ℤ, HasProduct fun t => (X t).X n] [HasProduct X]
    (hX : ∀ t, (X t).IsKInjective) (K : CochainComplex C ℤ) :
    Function.Bijective (derivedHomComparison X K)

Tag 070Y, a lemma

Tag 070Y in the Stacks Project.

CategoryTheory.Functor.exists_isRightDerivedValueAt_and_isIso_of_isKInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/KInjective/Locality.lean, line 386.

Stacks 070Y. Let A be an abelian category and F : K(A) ⥤ H a functor on the homotopy category of ℤ-indexed cochain complexes. Let I be a K-injective complex. Then:

I computes the right derived functor RF relative to the quasi-isomorphisms of K(A): the ind-object I/Qis(A) ⥤ H, (s : I ⟶ N) ↦ F(N), is essentially constant, and the canonical map F(I) ⟶ RF(I), i.e. the coprojection of its value cocone at the index 𝟙 I, is an isomorphism;

RF is defined at every object X of K(A) that is quasi-isomorphic to I, i.e. admits a quasi-isomorphism to or from I in K(A).

The source assumes F exact between triangulated categories; neither conclusion uses this.

public theorem exists_isRightDerivedValueAt_and_isIso_of_isKInjective
    {A : Type u₁} [Category.{v₁} A] [Abelian A] {H : Type u₂} [Category.{v₂} H]
    (F : HomotopyCategory A (ComplexShape.up ℤ) ⥤ H)
    (I : CochainComplex A ℤ) [I.IsKInjective] :
    (∃ c, F.IsRightDerivedValueAt (HomotopyCategory.quasiIso A (.up ℤ))
        ((HomotopyCategory.quotient A (.up ℤ)).obj I) c ∧
        IsIso (c.ι.app (MorphismProperty.Under.mk ⊤
          (𝟙 ((HomotopyCategory.quotient A (.up ℤ)).obj I))
          (MorphismProperty.id_mem _ _)))) ∧
      ∀ X : HomotopyCategory A (.up ℤ),
        ((∃ s : X ⟶ (HomotopyCategory.quotient A (.up ℤ)).obj I,
            HomotopyCategory.quasiIso A (.up ℤ) s) ∨
          (∃ s : (HomotopyCategory.quotient A (.up ℤ)).obj I ⟶ X,
            HomotopyCategory.quasiIso A (.up ℤ) s)) →
        ∃ c, F.IsRightDerivedValueAt (HomotopyCategory.quasiIso A (.up ℤ)) X c

Tag 070K, a lemma

Tag 070K in the Stacks Project.

CategoryTheory.Functor.hasPointwiseRightDerivedFunctor_and_isIso_app_of_exists_quasiIso_isKInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/KInjective/Locality.lean, line 423.

Stacks 070K. Let A be an abelian category such that every complex admits a quasi-isomorphism towards a K-injective complex, and let F : K(A) ⥤ D' be a functor on the homotopy category of ℤ-indexed cochain complexes. Then:

F has a pointwise right derived functor with respect to the quasi-isomorphisms Qis(A) of K(A); in particular F.HasRightDerivedFunctor Qis(A) holds, i.e. F has a right derived functor RF : D(A) ⥤ D', a left Kan extension of F along the localization K(A) ⥤ D(A);

every K-injective complex I computes RF: for any localization functor L for Qis(A) and any right derived functor RF of F with unit α : F ⟶ L ⋙ RF, the canonical map α.app I : F(I) ⟶ RF(I) is an isomorphism, which is the source's RF(I) = F(I).

The source assumes F exact between triangulated categories; neither conclusion uses this.

public theorem hasPointwiseRightDerivedFunctor_and_isIso_app_of_exists_quasiIso_isKInjective
    {A : Type u₁} [Category.{v₁} A] [Abelian A] {H : Type u₂} [Category.{v₂} H]
    (F : HomotopyCategory A (ComplexShape.up ℤ) ⥤ H)
    (hA : ∀ K : CochainComplex A ℤ, ∃ (I : CochainComplex A ℤ) (f : K ⟶ I),
      I.IsKInjective ∧ QuasiIso f) :
    F.HasPointwiseRightDerivedFunctor (HomotopyCategory.quasiIso A (ComplexShape.up ℤ)) ∧
      ∀ {D : Type u₃} [Category.{v₃} D] (L : HomotopyCategory A (ComplexShape.up ℤ) ⥤ D)
        [L.IsLocalization (HomotopyCategory.quasiIso A (ComplexShape.up ℤ))]
        (RF : D ⥤ H) (α : F ⟶ L ⋙ RF)
        [RF.IsRightDerivedFunctor α (HomotopyCategory.quasiIso A (ComplexShape.up ℤ))]
        (I : CochainComplex A ℤ), I.IsKInjective →
          IsIso (α.app ((HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj I))

Tag 070L, a lemma

Tag 070L in the Stacks Project.

isKInjective_limit_of_inverseSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/KInjective/InverseLimit.lean, line 533.

Stacks Tag 070L (Lemma 13.31.8). Let A be an abelian category and let F : ℕᵒᵖ ⥤ CochainComplex A ℤ be an inverse system of complexes (transition maps go from larger to smaller index). Assume: 1. each complex F.obj (op n) is K-injective; 2. each transition map F_{n+1} ⟶ F_n is a split surjection in every degree m; 3. the limit complex limit F exists (the degreewise limits exist in A). Then the limit complex limit F is K-injective.

The proof reduces (via exists_cylinder_extension_limit, then exists_compatible_homotopy_family) to the Mittag–Leffler construction of a compatible family of null-homotopies; the final step postcomposes the canonical cylinder homotopy cylinder.ι₀ ≃ cylinder.ι₁ with the assembled extension.

theorem isKInjective_limit_of_inverseSystem
    (F : ℕᵒᵖ ⥤ CochainComplex A ℤ) [HasLimit F]
    (hKInj : ∀ n : ℕ, (F.obj (op n)).IsKInjective)
    (hSplit : ∀ (n : ℕ) (m : ℤ),
      IsSplitEpi ((F.map (homOfLE (Nat.le_succ n)).op).f m)) :
    (limit F).IsKInjective

Tag 08BJ, a lemma

Tag 08BJ in the Stacks Project.

CochainComplex.isKInjective_mapHomologicalComplex_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/KInjective/AdjointAndProducts.lean, line 171.

Stacks 08BJ. Adjoint criterion for K-injectivity, exactness form: let u : A ⥤ B and v : B ⥤ A be additive functors between abelian categories such that u is right adjoint to v and v is exact. Then u carries K-injective cochain complexes to K-injective cochain complexes.

theorem isKInjective_mapHomologicalComplex_of_exact
    (u : A ⥤ B) (v : B ⥤ A) [u.Additive] [v.Additive] (adj : v ⊣ u)
    [PreservesFiniteLimits v] [PreservesFiniteColimits v]
    (I : CochainComplex A ℤ) [I.IsKInjective] :
    CochainComplex.IsKInjective ((u.mapHomologicalComplex (ComplexShape.up ℤ)).obj I)

Sources

LeanCochainComplex.IsKInjective · CochainComplex.isKInjective_iff_rightOrthogonal · CochainComplex.isKInjective_tfae · CochainComplex.isKInjective_two_out_of_three_of_distTriang · CochainComplex.isKInjective_of_injective · Stacks.Injectives.KInjectiveProduct.product_isKInjective · Stacks.Injectives.KInjectiveProduct.product_repr_derived · CategoryTheory.Functor.exists_isRightDerivedValueAt_and_isIso_of_isKInjective

Section13.32 Bounded cohomological dimension #

Section 13.32 of the Stacks Project, Tag 07K5. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07K6, a lemma

Tag 07K6 in the Stacks Project.

Stacks.BoundedCohomologicalDimension.main_theorem_07k6, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/BoundedCohomologicalDimension/Resolution/DescentAndFreeze.lean, line 828.

Let A be an abelian category and d : Ob(A) → ℕ∞ a function satisfying the bounded cohomological dimension hypotheses. Let K• be a cochain complex with n + d(K^n) → -∞ as n → -∞. Then there exists a complex L• together with a quasi-isomorphism K• → L• such that d(L^n) = 0 for all n ∈ ℤ.

alias main_theorem_07k6

Tag 07K7, a lemma

Tag 07K7 in the Stacks Project.

CategoryTheory.Functor.hasRightDerivedFunctor_of_isZero_rightDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/RightDerivedBoundedCohomologicalDimension.lean, line 1204. References: SGA 4½ Etat 0 (3.1.9), “(2) right, σ=F-acyclics”; SGA 4½ Etat 0 (4.2.3.2), “right case: Rf on D(A)”.

Stacks 07K7. Let F : 𝒜 ⥤ ℬ be a left exact functor of abelian categories, let P be the class of objects X which are right acyclic for F, i.e. such that X[0] computes the right derived functor of K⁺(𝒜) ⥤ D⁺(ℬ) in the sense of Stacks 05SX, and let RF⁺ : D⁺(𝒜) ⥤ D⁺(ℬ) be a right derived functor of F on the bounded below derived category. Assume that every object of 𝒜 is a subobject of an object of P, and that R ^ n F = H ^ n (RF⁺ (- [0])) = 0 for some n : ℕ. Then

the right derived functor RF : D(𝒜) ⥤ D(ℬ) exists,

every complex is the source of a quasi-isomorphism into a complex with terms in P,

every complex with terms in P computes RF, and

for every E in D(𝒜), H ^ i (RF (τ_{≤ a} E)) ⟶ H ^ i (RF E) is an isomorphism for i ≤ a, H ^ i (RF E) ⟶ H ^ i (RF (τ_{≥ b - n + 1} E)) is an isomorphism for i ≥ b, and RF shifts the range of degrees in which E lives by at most n - 1 on the right.

Right acyclicity is the source's notion (Stacks 0157(3) with 05SX); invertibility of the unit of RF⁺ at X[0] would be a weaker condition for a non-pointwise Kan extension (see the module documentation).

public theorem hasRightDerivedFunctor_of_isZero_rightDerived
    (F : A ⥤ B) [F.Additive] [PreservesFiniteLimits F]
    (RF' : DerivedCategory.Plus A ⥤ DerivedCategory.Plus B)
    (α' : F.mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh ⟶
      DerivedCategory.Plus.Qh ⋙ RF')
    [RF'.IsRightDerivedFunctor α' (HomotopyCategory.Plus.quasiIso A)]
    (P : ObjectProperty A)
    (hP : ∀ X : A, P X ↔ (F.mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh).ComputesRightDerived
      (HomotopyCategory.Plus.quasiIso A) ((HomotopyCategory.Plus.singleFunctor A 0).obj X))
    (hmono : ∀ X : A, ∃ (Y : A) (i : X ⟶ Y) (_ : Mono i), P Y)
    (n : ℕ) (hn : ∀ X : A, IsZero ((DerivedCategory.Plus.homologyFunctor B n).obj
      (RF'.obj ((DerivedCategory.Plus.singleFunctor A 0).obj X)))) :
    (F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).HasRightDerivedFunctor
        (HomotopyCategory.quasiIso A (ComplexShape.up ℤ)) ∧
      (∀ K : CochainComplex A ℤ, ∃ (L : CochainComplex A ℤ) (f : K ⟶ L) (_ : QuasiIso f),
        ∀ i : ℤ, P (L.X i)) ∧
      ∀ (RF : DerivedCategory A ⥤ DerivedCategory B)
        (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
          DerivedCategory.Qh ⋙ RF)
        [RF.IsRightDerivedFunctor α (HomotopyCategory.quasiIso A (ComplexShape.up ℤ))],
        (∀ L : CochainComplex A ℤ, (∀ i : ℤ, P (L.X i)) →
            IsIso (α.app ((HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj L))) ∧
          ∀ E : DerivedCategory A,
            (∀ a i : ℤ, i ≤ a → IsIso ((DerivedCategory.homologyFunctor B i).map
                (RF.map ((TStructure.t.truncLEι a).app E)))) ∧
              (∀ b i : ℤ, b ≤ i → IsIso ((DerivedCategory.homologyFunctor B i).map
                (RF.map ((TStructure.t.truncGEπ (b - (n : ℤ) + 1)).app E)))) ∧
                (∀ a : ℤ, E.IsGE a → (RF.obj E).IsGE a) ∧
                  ∀ b : ℤ, E.IsLE b → (RF.obj E).IsLE (b + (n : ℤ) - 1)

Tag 07K8, a lemma

Tag 07K8 in the Stacks Project.

CategoryTheory.Functor.hasLeftDerivedFunctor_of_isZero_leftDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/BoundedCohomologicalDimension.lean, line 452. References: SGA 4½ Etat 0 (3.1.9), “(2) left, σ=F-acyclics”; SGA 4½ Etat 0 (4.2.3.2), “left case: Lf on D(A)”.

Stacks 07K8. Let F : 𝒜 ⥤ ℬ be a right exact functor of abelian categories, let LF' : D⁺(𝒜ᵒᵖ) ⥤ D⁺(ℬᵒᵖ) be a right derived functor of F.op with unit α' — this is the left derived functor of F on the bounded above derived category D⁻(𝒜) — and let P be the class of objects which are left acyclic for F, i.e. of those X such that Xᵒᵖ[0] computes the right derived functor of F.op in the sense of Stacks 05SX. Assume that every object of 𝒜 is a quotient of an object of P, and that L ^ n F = H ^ (-n) (LF (- [0])) = 0 for some n : ℕ. Then

the left derived functor LF : D(𝒜) ⥤ D(ℬ) exists,

every complex is the target of a quasi-isomorphism from a complex with terms in P,

every complex with terms in P computes LF, and

for every E in D(𝒜), H ^ i (LF (τ_{≤ a + n - 1} E)) ⟶ H ^ i (LF E) is an isomorphism for i ≤ a, H ^ i (LF E) ⟶ H ^ i (LF (τ_{≥ b} E)) is an isomorphism for i ≥ b, and LF shifts the range of degrees in which E lives by at most n - 1 on the left.

public theorem hasLeftDerivedFunctor_of_isZero_leftDerived
    (F : A ⥤ B) [F.Additive] [PreservesFiniteColimits F]
    (LF' : DerivedCategory.Plus Aᵒᵖ ⥤ DerivedCategory.Plus Bᵒᵖ)
    (α' : F.op.mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh ⟶
      DerivedCategory.Plus.Qh ⋙ LF')
    [LF'.IsRightDerivedFunctor α' (HomotopyCategory.Plus.quasiIso Aᵒᵖ)]
    (P : ObjectProperty A)
    (hP : ∀ X : A, P X ↔
      (F.op.mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh).ComputesRightDerived
      (HomotopyCategory.Plus.quasiIso Aᵒᵖ)
      ((HomotopyCategory.Plus.singleFunctor Aᵒᵖ 0).obj (Opposite.op X)))
    (hepi : ∀ X : A, ∃ (Y : A) (p : Y ⟶ X) (_ : Epi p), P Y)
    (n : ℕ) (hn : ∀ X : A, IsZero ((DerivedCategory.Plus.homologyFunctor Bᵒᵖ n).obj
      (LF'.obj ((DerivedCategory.Plus.singleFunctor Aᵒᵖ 0).obj (Opposite.op X))))) :
    (F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).HasLeftDerivedFunctor
        (HomotopyCategory.quasiIso A (ComplexShape.up ℤ)) ∧
      (∀ K : CochainComplex A ℤ, ∃ (L : CochainComplex A ℤ) (f : L ⟶ K) (_ : QuasiIso f),
        ∀ i : ℤ, P (L.X i)) ∧
      ∀ (LF : DerivedCategory A ⥤ DerivedCategory B)
        (α : DerivedCategory.Qh ⋙ LF ⟶
          F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
        [LF.IsLeftDerivedFunctor α (HomotopyCategory.quasiIso A (ComplexShape.up ℤ))],
        (∀ L : CochainComplex A ℤ, (∀ i : ℤ, P (L.X i)) →
            IsIso (α.app ((HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj L))) ∧
          ∀ E : DerivedCategory A,
            (∀ a i : ℤ, i ≤ a → IsIso ((DerivedCategory.homologyFunctor B i).map
                (LF.map ((TStructure.t.truncLEι (a + (n : ℤ) - 1)).app E)))) ∧
              (∀ b i : ℤ, b ≤ i → IsIso ((DerivedCategory.homologyFunctor B i).map
                (LF.map ((TStructure.t.truncGEπ b).app E)))) ∧
                (∀ a : ℤ, E.IsGE a → (LF.obj E).IsGE (a - (n : ℤ) + 1)) ∧
                  ∀ b : ℤ, E.IsLE b → (LF.obj E).IsLE b

Sources

LeanStacks.BoundedCohomologicalDimension.main_theorem_07k6 · CategoryTheory.Functor.hasRightDerivedFunctor_of_isZero_rightDerived · CategoryTheory.Functor.hasLeftDerivedFunctor_of_isZero_leftDerived

Section13.33 Derived colimits #

Section 13.33 of the Stacks Project, Tag 0A5K. 9 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 090Z, a definition

Tag 090Z in the Stacks Project.

CategoryTheory.Pretriangulated.IsHomotopyColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/HomotopyColimit.lean, line 88.

An object K of a pre-triangulated category D is a derived colimit, or homotopy colimit, of a system of objects F : ℕ ⥤ D whose direct sum ∐ F.obj exists — written K = hocolim Kₙ — if there is a distinguished triangle ∐ F.obj ⟶ ∐ F.obj ⟶ K ⟶ (∐ F.obj)⟦1⟧ whose first map is 1 - fₙ on the n-th summand, i.e. Sigma.ι F.obj n - fₙ ≫ Sigma.ι F.obj (n + 1), where Kₙ = F.obj n and fₙ = F.map (homOfLE (Nat.le_succ n)) is the transition map Kₙ ⟶ Kₙ₊₁. Such a K is unique only up to non-unique isomorphism, which is why this is a predicate and not a construction.

public def IsHomotopyColimit (F : ℕ ⥤ D) [HasCoproduct F.obj] (K : D) : Prop

Tag 0CRH, a remark

Tag 0CRH in the Stacks Project.

CategoryTheory.Pretriangulated.exists_iso_of_isHomotopyColimitWithCoprojections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/HomotopyColimitCoprojections.lean, line 180.

[Stacks, Tag 0CRH]: a derived colimit datum is unique up to a compatible isomorphism. Let (Kₙ, fₙ) be a system of objects of a pre-triangulated category whose direct sum exists, and let (K, iₙ, c) and (K', i'ₙ, c') be two derived colimit data for it: objects endowed with coprojections satisfying iₙ₊₁ ∘ fₙ = iₙ and with a morphism to (∐ Kₙ)⟦1⟧ completing ∐ Kₙ --(1 - fₙ)--> ∐ Kₙ --(iₙ)--> · --c--> to a distinguished triangle. Then there is an isomorphism φ : K ≅ K' with φ ∘ iₙ = i'ₙ for every n and c' ∘ φ = c.

The existence of a morphism φ completing the identity of the first two terms to a morphism of the two triangles is TR3, and that it is invertible is the five lemma for distinguished triangles (Lemma 13.4.3). The isomorphism is not unique: nothing pins the completion TR3 produces.

theorem exists_iso_of_isHomotopyColimitWithCoprojections {F : ℕ ⥤ D} [HasCoproduct F.obj]
    {K : D} {i : ∀ n : ℕ, F.obj n ⟶ K} {c : K ⟶ (∐ F.obj)⟦(1 : ℤ)⟧}
    (h : IsHomotopyColimitWithCoprojections F K i c)
    {K' : D} {i' : ∀ n : ℕ, F.obj n ⟶ K'} {c' : K' ⟶ (∐ F.obj)⟦(1 : ℤ)⟧}
    (h' : IsHomotopyColimitWithCoprojections F K' i' c') :
    ∃ φ : K ≅ K', (∀ n : ℕ, i n ≫ φ.hom = i' n) ∧ φ.hom ≫ c' = c

Tag 0CRI, a remark

Tag 0CRI in the Stacks Project.

CategoryTheory.Pretriangulated.exists_hom_of_isHomotopyColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/DerivedColimits.lean, line 461.

Stacks 0CRI. A morphism of sequential systems induces a morphism between chosen homotopy colimits. It commutes with every canonical coprojection and completes the morphism of the two defining distinguished triangles.

public theorem exists_hom_of_isHomotopyColimit {F G : ℕ ⥤ D} [HasCoproduct F.obj]
    [HasCoproduct G.obj] (a : F ⟶ G) {K L : D}
    (p : ∐ F.obj ⟶ K) (q : K ⟶ (∐ F.obj)⟦(1 : ℤ)⟧)
    (hK : Triangle.mk (Stacks.CountableCoproducts.oneSubShift F) p q ∈ distTriang D)
    (p' : ∐ G.obj ⟶ L) (q' : L ⟶ (∐ G.obj)⟦(1 : ℤ)⟧)
    (hL : Triangle.mk (Stacks.CountableCoproducts.oneSubShift G) p' q' ∈ distTriang D) :
    ∃ b : K ⟶ L,
      (∀ n : ℕ, Sigma.ι F.obj n ≫ p ≫ b = a.app n ≫ Sigma.ι G.obj n ≫ p') ∧
      b ≫ q' = q ≫ (Limits.Sigma.map (fun n ↦ a.app n))⟦(1 : ℤ)⟧'

Tag 0CRJ, a lemma

Tag 0CRJ in the Stacks Project.

CategoryTheory.Pretriangulated.exists_iso_of_isHomotopyColimit_of_strictMono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/DerivedColimits.lean, line 831.

Stacks 0CRJ. Let F : ℕ ⥤ D be a system of objects K m = F.obj m of a pre-triangulated category, let n : ℕ → ℕ be strictly increasing, and assume the direct sums ∐ K m and ∐ K (n i) exist. If K is a derived colimit of the system with structure map p and K' is a derived colimit of the subsystem (K (n i)) with structure map p' (Definition 090Z), then there is an isomorphism e : K' ≅ K, i.e. hocolim K (n i) ⟶ hocolim K m, such that for every i the composition K (n i) ⟶ K' ⟶ K of the coprojection with e is the coprojection K (n i) ⟶ K.

public theorem exists_iso_of_isHomotopyColimit_of_strictMono
    (F : ℕ ⥤ D) [HasCoproduct F.obj] {n : ℕ → ℕ} (hn : StrictMono n)
    [HasCoproduct (hn.monotone.functor ⋙ F).obj]
    {K : D} (p : ∐ F.obj ⟶ K) (q : K ⟶ (∐ F.obj)⟦(1 : ℤ)⟧)
    (hK : Triangle.mk (Limits.Sigma.desc fun m ↦ Limits.Sigma.ι F.obj m -
        F.map (homOfLE (Nat.le_succ m)) ≫ Limits.Sigma.ι F.obj (m + 1)) p q ∈ distTriang D)
    {K' : D} (p' : ∐ (hn.monotone.functor ⋙ F).obj ⟶ K')
    (q' : K' ⟶ (∐ (hn.monotone.functor ⋙ F).obj)⟦(1 : ℤ)⟧)
    (hK' : Triangle.mk (Limits.Sigma.desc fun i ↦
      Limits.Sigma.ι (hn.monotone.functor ⋙ F).obj i -
        (hn.monotone.functor ⋙ F).map (homOfLE (Nat.le_succ i)) ≫
          Limits.Sigma.ι (hn.monotone.functor ⋙ F).obj (i + 1)) p' q' ∈ distTriang D) :
    ∃ e : K' ≅ K, ∀ i : ℕ,
      Limits.Sigma.ι (hn.monotone.functor ⋙ F).obj i ≫ p' ≫ e.hom =
        Limits.Sigma.ι F.obj (n i) ≫ p

Tag 0A5L, a lemma

Tag 0A5L in the Stacks Project.

derivedCategory_termwiseDirectSum_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Coproducts.lean, line 1015.

Stacks Tag 0A5L, the concrete identification of the coproduct in D(A): for a countable family K : J → CochainComplex A ℤ, the termwise direct sum ∐ K, with the images under Q of the canonical injections Sigma.ι K j, is a coproduct of (Q (K j))ⱼ in D(A).

[HasCoproduct K] records that the termwise direct sum exists in CochainComplex A ℤ; it follows from h.hasCoproducts and Countable J, but is assumed so that ∐ K and Sigma.ι K are well-formed in the statement.

theorem derivedCategory_termwiseDirectSum_isColimit
    (h : HasExactCountableDirectSums A) (J : Type) [Countable J]
    (K : J → CochainComplex A ℤ) [HasCoproduct K] :
    Nonempty (IsColimit
      ((DerivedCategory.Q (C := A)).mapCocone (Cofan.mk (∐ K) (Sigma.ι K))))

derivedCategory_hasCountableCoproducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Coproducts.lean, line 1029.

Stacks Tag 0A5L: if the abelian category A has exact countable direct sums then its derived category D(A) has countable direct sums.

A countable family in D(A) is, up to isomorphism, the image under Q of a family of complexes, by essential surjectivity of Q; the termwise direct sum of the latter is its coproduct.

theorem derivedCategory_hasCountableCoproducts
    (h : HasExactCountableDirectSums A) :
    HasCountableCoproducts (DerivedCategory A)

Tag 093W, a lemma

Tag 093W in the Stacks Project.

SheafOfModules.DifferentialGradedModule.shortExact_oneSubShift_piMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedDerivedColimits.lean, line 157. The attribute's comment: “sheaf differential graded modules”.

Lemma 093W for sheaf differential graded modules. For a system M₀ → M₁ → ⋯ of right differential graded A-modules over a sheaf of differential graded algebras, the sequence

0 → ⊕ₙ Mₙ --(1 - f)--> ⊕ₙ Mₙ --π--> colim Mₙ → 0

is short exact, where 1 - f is the morphism with σₙ ≫ (1 - f) = σₙ - fₙ ≫ σₙ₊₁ on the n-th coprojection and π is the morphism with σₙ ≫ π = ιₙ.

The general Lemma 093W applies verbatim: Mod(A, d) is abelian, it has colimits over ℕ and countable direct sums, and those colimits over ℕ are exact by Tag 0FRJ.

theorem shortExact_oneSubShift_piMap (F : ℕ ⥤ DifferentialGradedModule.{u, v, max u v w} A) :
    ∃ hw : oneSubShift F ≫ piMap F = 0,
      (ShortComplex.mk (oneSubShift F) (piMap F) hw).ShortExact

DifferentialGradedModule.shortExact_oneSubShift_piMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedColimits.lean, line 255. The attribute's comment: “differential graded modules”.

Lemma 093W for differential graded modules. For a system M₀ → M₁ → ⋯ of right differential graded A-modules the sequence 0 → ⊕ₙ Mₙ --(1 - f)--> ⊕ₙ Mₙ --π--> colim Mₙ → 0 is short exact.

theorem shortExact_oneSubShift_piMap :
    ∃ w : oneSubShift F ≫ piMap F = 0,
      (ShortComplex.mk (oneSubShift F) (piMap F) w).ShortExact

Stacks.CountableCoproducts.hasColimitsOfShape_discrete_of_hasColimitsOfShape_nat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/GrothendieckAxioms/CountableCoproducts.lean, line 182.

Countable direct sums exist. If colimits over ℕ exist in A, then every countable family of objects has a coproduct, i.e. A has colimits of shape Discrete ℕ.

theorem hasColimitsOfShape_discrete_of_hasColimitsOfShape_nat
    [HasColimitsOfShape ℕ A] :
    HasColimitsOfShape (Discrete ℕ) A

Stacks.CountableCoproducts.preservesFiniteLimits_colim_discrete_of_hasColimitsOfShape_nat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/GrothendieckAxioms/CountableCoproducts.lean, line 194.

Countable direct sums are exact. If colimits over ℕ exist and are exact in A, then the countable-coproduct functor colim : (Discrete ℕ ⥤ A) ⥤ A preserves finite limits — which, for a right-exact additive left adjoint, is exactness: it carries short exact sequences to short exact sequences.

theorem preservesFiniteLimits_colim_discrete_of_hasColimitsOfShape_nat
    [HasColimitsOfShape ℕ A] [HasColimitsOfShape (Discrete ℕ) A]
    (hexact : PreservesFiniteLimits (colim : (ℕ ⥤ A) ⥤ A)) :
    PreservesFiniteLimits (colim : (Discrete ℕ ⥤ A) ⥤ A)

Stacks.CountableCoproducts.shortExact_oneSubShift_piMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/GrothendieckAxioms/CountableCoproducts.lean, line 546.

The presentation of the colimit: Lemma 093W(2). For every system over ℕ in an abelian category with countable direct sums and colimits over ℕ that are exact, the sequence 0 ⟶ ∐ₙ Aₙ --(1 - f)--> ∐ₙ Aₙ --π--> colim Aₙ ⟶ 0 is short exact.

theorem shortExact_oneSubShift_piMap
    [HasColimitsOfShape ℕ A] [HasColimitsOfShape (Discrete ℕ) A]
    (hexact : PreservesFiniteLimits (colim : (ℕ ⥤ A) ⥤ A))
    (F : SystemOverNat A) :
    ∃ w : oneSubShift F ≫ piMap F = 0,
      (ShortComplex.mk (oneSubShift F) (piMap F) w).ShortExact

Tag 0949, a lemma

Tag 0949 in the Stacks Project.

DerivedCategory.isHomotopyColimit_Q_obj_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/DerivedColimits.lean, line 425.

Stacks 0949. Let A be an abelian category in which colimits over ℕ exist and are exact, and let L : ℕ ⥤ CochainComplex A ℤ be a system of complexes of A. Then the image under Q : CochainComplex A ℤ ⥤ D(A) of the termwise colimit colimit L is a derived colimit (homotopy colimit, Definition 090Z) of the system L ⋙ Q in D(A).

public theorem DerivedCategory.isHomotopyColimit_Q_obj_colimit {A : Type u} [Category.{v} A]
    [Abelian A] [HasDerivedCategory.{w} A] [HasColimitsOfShape ℕ A]
    [HasExactColimitsOfShape ℕ A] (L : ℕ ⥤ CochainComplex A ℤ)
    [HasCoproduct (L ⋙ DerivedCategory.Q).obj] :
    IsHomotopyColimit (L ⋙ DerivedCategory.Q) (DerivedCategory.Q.obj (colimit L))

Tag 0CRK, a lemma

Tag 0CRK in the Stacks Project.

CategoryTheory.Pretriangulated.exists_iso_colimit_of_isHomotopyColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/DerivedColimits.lean, line 243.

Stacks 0CRK. Let F : ℕ ⥤ D be a system of objects K n = F.obj n of a pre-triangulated category whose direct sum ∐ K n exists, let A be an abelian category in which colimits over ℕ exist and are exact, and let H : D ⥤ A be a homological functor commuting with countable direct sums. If K is a derived colimit of the system with structure map p : ∐ K n ⟶ K (Definition 090Z), then H K = colim H (K n): there is an isomorphism e : colim H (K n) ≅ H K such that for every n the n-th coprojection of the colimit followed by e is H applied to the coprojection K n ⟶ K of the derived colimit.

public theorem exists_iso_colimit_of_isHomotopyColimit
    (F : ℕ ⥤ D) [HasCoproduct F.obj] (H : D ⥤ A) [H.IsHomological]
    [PreservesColimitsOfShape (Discrete ℕ) H]
    {K : D} (p : ∐ F.obj ⟶ K) (q : K ⟶ (∐ F.obj)⟦(1 : ℤ)⟧)
    (hK : Triangle.mk (Limits.Sigma.desc fun n ↦ Limits.Sigma.ι F.obj n -
        F.map (homOfLE (Nat.le_succ n)) ≫ Limits.Sigma.ι F.obj (n + 1)) p q ∈ distTriang D) :
    ∃ e : colimit (F ⋙ H) ≅ H.obj K, ∀ n : ℕ,
      colimit.ι (F ⋙ H) n ≫ e.hom = H.map (Limits.Sigma.ι F.obj n ≫ p)

Tag 094A, a lemma

Tag 094A in the Stacks Project.

CategoryTheory.Pretriangulated.exists_iso_colimit_preadditiveCoyoneda_of_isHomotopyColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/DerivedColimits.lean, line 327.

Stacks 094A. Let F : ℕ ⥤ D be a system of objects L n = F.obj n of a pre-triangulated category whose direct sum ∐ L n exists, and let K be an object of D such that Hom(K, -) = preadditiveCoyoneda.obj (Opposite.op K) commutes with countable direct sums, i.e. for every countable family E : ℕ → D the canonical map ⨁ (K ⟶ E n) ⟶ (K ⟶ ∐ E) is bijective. If L is a derived colimit of the system with structure map p : ∐ L n ⟶ L (Definition 090Z), then Hom(K, L) = colim Hom(K, L n): there is an isomorphism of abelian groups e : colim Hom(K, L n) ≅ Hom(K, L) such that for every n the n-th coprojection of the colimit followed by e is composition with the coprojection L n ⟶ L of the derived colimit.

This is Lemma 0CRK for the homological functor H = Hom(K, -).

public theorem exists_iso_colimit_preadditiveCoyoneda_of_isHomotopyColimit
    (F : ℕ ⥤ D) [HasCoproduct F.obj] (K : D)
    [PreservesColimitsOfShape (Discrete ℕ) (preadditiveCoyoneda.obj (Opposite.op K))]
    {L : D} (p : ∐ F.obj ⟶ L) (q : L ⟶ (∐ F.obj)⟦(1 : ℤ)⟧)
    (hL : Triangle.mk (Limits.Sigma.desc fun n ↦ Limits.Sigma.ι F.obj n -
        F.map (homOfLE (Nat.le_succ n)) ≫ Limits.Sigma.ι F.obj (n + 1)) p q ∈ distTriang D) :
    ∃ e : colimit (F ⋙ preadditiveCoyoneda.obj (Opposite.op K)) ≅
        (preadditiveCoyoneda.obj (Opposite.op K)).obj L, ∀ n : ℕ,
      colimit.ι (F ⋙ preadditiveCoyoneda.obj (Opposite.op K)) n ≫ e.hom =
        (preadditiveCoyoneda.obj (Opposite.op K)).map (Limits.Sigma.ι F.obj n ≫ p)

Sources

LeanCategoryTheory.Pretriangulated.IsHomotopyColimit · CategoryTheory.Pretriangulated.exists_iso_of_isHomotopyColimitWithCoprojections · CategoryTheory.Pretriangulated.exists_hom_of_isHomotopyColimit · CategoryTheory.Pretriangulated.exists_iso_of_isHomotopyColimit_of_strictMono · derivedCategory_termwiseDirectSum_isColimit · derivedCategory_hasCountableCoproducts · SheafOfModules.DifferentialGradedModule.shortExact_oneSubShift_piMap · DifferentialGradedModule.shortExact_oneSubShift_piMap

Section13.34 Derived limits #

Section 13.34 of the Stacks Project, Tag 08TB. 5 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08TC, a definition

Tag 08TC in the Stacks Project.

CategoryTheory.Pretriangulated.IsDerivedLimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/HomotopyLimit.lean, line 72.

An object K of a pre-triangulated category D is a derived limit, or homotopy limit, of an inverse system F : ℕᵒᵖ ⥤ D of objects of D whose objects have a product — written K = R lim Kₙ — if there is a distinguished triangle K ⟶ ∏ Kₙ ⟶ ∏ Kₙ ⟶ K⟦1⟧ in which the middle map is the difference map (kₙ) ↦ (kₙ - fₙ₊₁(kₙ₊₁)), where Kₙ = F.obj ⟨n⟩ and fₙ₊₁ = F.map (homOfLE (Nat.le_succ n)).op is the transition map Kₙ₊₁ ⟶ Kₙ. Such a K is unique only up to non-unique isomorphism, which is why this is a predicate and not a construction.

public def IsDerivedLimit (F : ℕᵒᵖ ⥤ D) [HasProduct fun n : ℕ => F.obj ⟨n⟩] (K : D) : Prop

Tag 07KC, a lemma

Tag 07KC in the Stacks Project.

Stacks.DerivedProducts.hasProductsOfShape_derivedCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Products.lean, line 1170. The attribute's comment: “(1)”.

Statement 1 (Existence of products). The derived category D(A) has countable products (Definition 5).

INFORMAL ARGUMENT (sound, sanity-checked). Q is essentially surjective ((DerivedCategory.Q).EssSurj is an instance) and, by preservesLimitsOfShape_Q, preserves I-indexed products. Given any family X : I → D(A), choose for each i a complex K i with Q.obj (K i) ≅ X i (essential surjectivity). Then CochainComplex A ℤ has the product ∏ᶜ K (HasProductsOfShape I (CochainComplex A ℤ) infers), and Q carries its limit cone to a limit cone over i ↦ Q.obj (K i); transporting along the isos Q.obj (K i) ≅ X i (HasLimit.iso/Limits.HasLimit.ofIso-style transport, or hasLimitOfIso) yields a product of X. Hence D(A) has products of shape I.

PROOF STRATEGY (Lean). constructor; intro X (unfold HasProductsOfShape to ∀ family, HasProduct). Pick reps K i := (Q.objPreimage (X i)) with Q.objObjPreimageIso. Use preservesLimitsOfShape_Q to get the mapped cone of ∏ᶜ K is a limit (isLimitOfPreserves), giving HasProduct (fun i => Q.obj (K i)); then transport HasProduct along the natural iso Q.obj (K ·) ≅ X via hasProduct_of_iso/HasLimit.ofIso (Discrete.natIso of the objectwise isos).

theorem hasProductsOfShape_derivedCategory :
    HasProductsOfShape I (DerivedCategory A)

Stacks.DerivedProducts.isLimit_productFanInDerivedCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Products.lean, line 1204. The attribute's comment: “(2)”.

Statement 2 (Computation via termwise products). For any countable family K : I → CochainComplex A ℤ of complexes (representing objects of D(A)), the image under Q of the termwise product complex ∏ᶜ K, together with the projection chain maps Q.map (Pi.π K i), is a product of the family (Q.obj (K i)) in D(A), i.e. the corresponding fan is a limit cone. In particular the product is independent, up to canonical isomorphism in D(A), of the choice of representing complexes.

theorem isLimit_productFanInDerivedCategory (K : I → CochainComplex A ℤ) :
    Nonempty (IsLimit (productFanInDerivedCategory K))

Stacks.DerivedProducts.isIso_piComparison_homologyFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Products.lean, line 1236. The attribute's comment: “(3)”.

Statement 3 (Cohomology of the product). For every p ∈ ℤ and every countable family X : I → D(A), the canonical comparison morphism H^p(∏ X_i) → ∏ H^p(X_i) induced by the projections (piComparison of the homology functor) is an isomorphism in A. Equivalently H^p(∏ X_i) = ∏ H^p(X_i) (canonical iso).

theorem isIso_piComparison_homologyFunctor
    [HasProductsOfShape I (DerivedCategory A)]
    (X : I → DerivedCategory A) (p : ℤ) :
    IsIso (piComparison (DerivedCategory.homologyFunctor A p) X)

Tag 0BK7, a lemma

Tag 0BK7 in the Stacks Project.

DerivedCategory.exists_isDerivedLimit_of_forall_isGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/DerivedLimits.lean, line 273.

Let 𝒜 be an abelian category with countable products and enough injectives. Then any inverse system F : ℕᵒᵖ ⥤ D(𝒜) of objects of D⁺(𝒜), i.e. whose values Kₙ = F.obj ⟨n⟩ are bounded below, has a product ∏ Kₙ in D(𝒜) and a derived limit K = R lim Kₙ: an object sitting in a distinguished triangle K ⟶ ∏ Kₙ ⟶ ∏ Kₙ ⟶ K⟦1⟧ whose middle map is (kₙ) ↦ (kₙ - fₙ₊₁(kₙ₊₁)).

public theorem exists_isDerivedLimit_of_forall_isGE (F : ℕᵒᵖ ⥤ DerivedCategory 𝒜)
    (hF : ∀ n : ℕ, ∃ a : ℤ, (F.obj ⟨n⟩).IsGE a) :
    ∃ (_ : HasProduct fun n : ℕ => F.obj ⟨n⟩) (K : DerivedCategory 𝒜), IsDerivedLimit F K

Tag 070M, a lemma

Tag 070M in the Stacks Project.

CochainComplex.isKInjective_limit_and_isDerivedLimit_of_isSplitEpi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/DerivedLimits.lean, line 737.

Let A be an abelian category with countable products and let 𝓘 : ℕᵒᵖ ⥤ CochainComplex A ℤ be an inverse system of K-injective complexes whose transition maps are degreewise split epimorphisms. Then the limit I = lim 𝓘 exists, it is K-injective, and it represents the derived limit R lim 𝓘ₙ. Moreover, for every cochain complex K of A equipped with quasi-isomorphisms f n : τ_{≥ -n} K ⟶ 𝓘ₙ making the ladder over the canonical maps K.πTruncGE (-n) : K ⟶ τ_{≥ -n} K commute — the system produced by Stacks 070F, for which R lim 𝓘ₙ is R lim τ_{≥ -n} K, as the f n become isomorphisms in D(A) — the unique map γ : K ⟶ I compatible with the maps K ⟶ τ_{≥ -n} K ⟶ 𝓘ₙ is a quasi-isomorphism if and only if every map K ⟶ R lim τ_{≥ -n} K compatible with the projections, as in Stacks 0H72, is an isomorphism in D(A).

public theorem isKInjective_limit_and_isDerivedLimit_of_isSplitEpi
    (𝓘 : ℕᵒᵖ ⥤ CochainComplex A ℤ) (h𝓘 : ∀ n : ℕ, (𝓘.obj ⟨n⟩).IsKInjective)
    (hsplit : ∀ (n : ℕ) (i : ℤ), IsSplitEpi ((𝓘.map (homOfLE (Nat.le_succ n)).op).f i)) :
    ∃ (_ : HasLimit 𝓘) (_ : HasProduct fun n : ℕ => (𝓘 ⋙ Q).obj ⟨n⟩),
      (limit 𝓘).IsKInjective ∧ IsDerivedLimit (𝓘 ⋙ Q) (Q.obj (limit 𝓘)) ∧
        ∀ (K : CochainComplex A ℤ) (f : ∀ n : ℕ, K.truncGE (-(n : ℤ)) ⟶ 𝓘.obj ⟨n⟩),
          (∀ n : ℕ, QuasiIso (f n)) →
          (∀ n : ℕ, K.πTruncGE (-((n + 1 : ℕ) : ℤ)) ≫ f (n + 1) ≫
              𝓘.map (homOfLE (Nat.le_succ n)).op = K.πTruncGE (-(n : ℤ)) ≫ f n) →
          ∃ γ : K ⟶ limit 𝓘, (∀ n : ℕ, γ ≫ limit.π 𝓘 ⟨n⟩ = K.πTruncGE (-(n : ℤ)) ≫ f n) ∧
            (QuasiIso γ ↔ ∀ (L : DerivedCategory A) (c : Q.obj K ⟶ L)
              (p : L ⟶ ∏ᶜ fun n : ℕ => (𝓘 ⋙ Q).obj ⟨n⟩)
              (δ : (∏ᶜ fun n : ℕ => (𝓘 ⋙ Q).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧),
              Triangle.mk p (Pi.lift fun n : ℕ =>
                  Pi.π (fun n : ℕ => (𝓘 ⋙ Q).obj ⟨n⟩) n -
                    Pi.π (fun n : ℕ => (𝓘 ⋙ Q).obj ⟨n⟩) (n + 1) ≫
                      (𝓘 ⋙ Q).map (homOfLE (Nat.le_succ n)).op) δ ∈
                distTriang (DerivedCategory A) →
              (∀ n : ℕ, c ≫ p ≫ Pi.π (fun n : ℕ => (𝓘 ⋙ Q).obj ⟨n⟩) n =
                Q.map (K.πTruncGE (-(n : ℤ)) ≫ f n)) → IsIso c)

Tag 090Y, a lemma

Tag 090Y in the Stacks Project.

CochainComplex.exists_quasiIso_isKInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/DerivedLimits.lean, line 1063.

Let 𝒜 be an abelian category having enough injectives and exact countable products. Then every cochain complex K of objects of 𝒜 admits a quasi-isomorphism f : K ⟶ I to a K-injective complex I.

public theorem exists_quasiIso_isKInjective {𝒜 : Type u} [Category.{v} 𝒜] [Abelian 𝒜]
    [EnoughInjectives 𝒜] [HasProductsOfShape ℕ 𝒜] [HasExactLimitsOfShape (Discrete ℕ) 𝒜]
    (K : CochainComplex 𝒜 ℤ) :
    ∃ (I : CochainComplex 𝒜 ℤ) (f : K ⟶ I) (_ : QuasiIso f), I.IsKInjective

Sources

LeanCategoryTheory.Pretriangulated.IsDerivedLimit · Stacks.DerivedProducts.hasProductsOfShape_derivedCategory · Stacks.DerivedProducts.isLimit_productFanInDerivedCategory · Stacks.DerivedProducts.isIso_piComparison_homologyFunctor · DerivedCategory.exists_isDerivedLimit_of_forall_isGE · CochainComplex.isKInjective_limit_and_isDerivedLimit_of_isSplitEpi · CochainComplex.exists_quasiIso_isKInjective

Section13.35 Operations on full subcategories #

Section 13.35 of the Stacks Project, Tag 0FX0. 5 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FX3, a lemma

Tag 0FX3 in the Stacks Project.

closedUnderDirectSums_add_star_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/OperationsOnFullSubcategories.lean, line 859. The attribute's comment: “(1)”.

Stacks 0FX3 (1). add 𝒜 ⋆ add ℬ is closed under direct sums: for all X, X' ∈ add 𝒜 ⋆ add ℬ we have X ⊞ X' ∈ add 𝒜 ⋆ add ℬ.

Proof (as in the source): pick distinguished triangles T : A → X → B → A[1] and T' : A' → X' → B' → A'[1] with A, A' ∈ add 𝒜, B, B' ∈ add ℬ. The product triangle productTriangle ![T, T'] is distinguished (productTriangle_distinguished), its legs are the Fin 2-products of the legs of T, T', which via finProd2 are the binary biproducts A ⊞ A', X ⊞ X', B ⊞ B'. Since add is closed under ⊞ (add_closedUnderDirectSums) and under iso (add_iso), A ⊞ A' ∈ add 𝒜, B ⊞ B' ∈ add ℬ, and the middle object is iso to X ⊞ X'.

theorem closedUnderDirectSums_add_star_add (𝒜 ℬ : Set C) :
    ClosedUnderDirectSums (add 𝒜 ⋆ add ℬ)

closedUnderDirectSums_smd_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/OperationsOnFullSubcategories.lean, line 887. The attribute's comment: “(2)”.

Stacks 0FX3 (2). smd (add 𝒜) is closed under direct sums: for all X, X' ∈ smd (add 𝒜) we have X ⊞ X' ∈ smd (add 𝒜).

Proof (as in the source): write A ≅ X ⊞ Y, A' ≅ X' ⊞ Y' with A, A' ∈ add 𝒜. Then A ⊞ A' ∈ add 𝒜 (add_closedUnderDirectSums) and A ⊞ A' ≅ (X ⊞ Y) ⊞ (X' ⊞ Y') ≅ (X ⊞ X') ⊞ (Y ⊞ Y') (biprodRearrange), exhibiting X ⊞ X' as a direct summand of A ⊞ A' ∈ add 𝒜.

theorem closedUnderDirectSums_smd_add (𝒜 : Set C) :
    ClosedUnderDirectSums (smd (add 𝒜))

Tag 0FX4, a lemma

Tag 0FX4 in the Stacks Project.

CategoryTheory.ObjectProperty.retractClosure_extensionProductIter_isClosedUnderBinaryProducts_and_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/OperationsOnFullSubcategories.lean, line 202.

For a full subcategory P of a triangulated category which is closed under direct sums, the subcategory smd(P^{⋆ (n + 1)}) of direct summands of n-fold extensions of objects of P is strictly full, closed under direct sums and closed under direct summands, and these subcategories are additive in the number of factors: smd(P^{⋆ (n + m + 1)}) = smd(smd(P^{⋆ (n + 1)}) ⋆ smd(P^{⋆ (m + 1)})). Taking P = add(A) this is the Stacks project's Cₙ = smd(add(A)^{⋆ n}), strictly full, closed under direct sums and direct summands, with C_{n + m} = smd(Cₙ ⋆ C_m).

theorem retractClosure_extensionProductIter_isClosedUnderBinaryProducts_and_add
    (P : ObjectProperty C) [P.IsClosedUnderBinaryProducts] [IsTriangulated C] (n m : ℕ) :
    (P.extensionProductIter n).retractClosure.IsClosedUnderIsomorphisms ∧
      (P.extensionProductIter n).retractClosure.IsClosedUnderBinaryProducts ∧
      (P.extensionProductIter n).retractClosure.IsStableUnderRetracts ∧
      (P.extensionProductIter (n + m + 1)).retractClosure =
        (extensionProduct (P.extensionProductIter n).retractClosure
          (P.extensionProductIter m).retractClosure).retractClosure

Tag 0FX5, a remark

Tag 0FX5 in the Stacks Project.

Stacks.TriangulatedGenerators.retractClosure_extensionProductIter_biSup_shift_inverseImage_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/ExactFunctorBoundedOperations.lean, line 149. The attribute's comment: “for the bounded-shift form smd(add(P[c, d])^{⋆ n}), along an exact functor”.

The bounded-shift form of smd(add(P[c, d])^{⋆ n}) is functorial along an exact functor. Let F : C ⥤ D be an exact functor of pretriangulated categories, let P be a property of objects of C and Q one of D, and suppose F carries every object satisfying P to one satisfying Q. Then F carries smd(add(P[c, d])^{⋆ n}) into smd(add(Q[c, d])^{⋆ n}): the shift interval [c, d] and the number n of extensions are the same on both sides.

This is Derived Categories, Remark 13.35.5 ([Stacks, Tag 0FX5]) for this one of the section's constructions, namely the explicit subcategories Cₙ = smd(add(E[c, d])^{⋆ n}) built from a bounded range of shifts as in [Stacks, Tag 0FX9]. Tracking the interval is the content: the unbounded-shift form Stacks.TriangulatedGenerators.triangEnvelopeIter_inverseImage_of_le, stated with ObjectProperty.triangEnvelopeIter, gives no control on which shifts of Q the image uses.

theorem retractClosure_extensionProductIter_biSup_shift_inverseImage_of_le
    {P : ObjectProperty C} {Q : ObjectProperty D} (h : ∀ ⦃X : C⦄, P X → Q (F.obj X))
    (c d : ℤ) (n : ℕ) :
    ((⨆ i ∈ Set.Icc c d, P.isoClosure.shift i).binaryProductsClosure.extensionProductIter n
      ).retractClosure ≤
      ((((⨆ i ∈ Set.Icc c d, Q.isoClosure.shift i).binaryProductsClosure.extensionProductIter n
        ).retractClosure).inverseImage F)

Tag 0FX7, a lemma

Tag 0FX7 in the Stacks Project.

DerivedCategory.prop_retractClosure_extensionProductIter_of_prop_homology_and_of_prop_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/OperationsOnFullSubcategories.lean, line 541.

Let C be an abelian category and E a class of objects of C, viewed inside the derived category D(C). Let a ≤ b. (1) If the cohomology of K : D(C) vanishes outside [a, b] and each H^i(K) with i ∈ [a, b] is a direct summand of a finite direct sum of objects of E, then K is a direct summand of a (b - a)-fold extension of finite direct sums of objects of E placed in degrees [a, b], that is, K ∈ smd(add(E[a, b])^{⋆ (b - a + 1)}). (2) The same conclusion holds for K = Q.obj L when L is a cochain complex vanishing outside [a, b] whose terms L^i with i ∈ [a, b] are direct summands of finite direct sums of objects of E. The special cases where the objects H^i(K), resp. L^i, are themselves in E are parts (1) and (3) of [Stacks, Tag 0FX7].

theorem prop_retractClosure_extensionProductIter_of_prop_homology_and_of_prop_X
    (E : ObjectProperty C) {a b : ℤ} (hab : a ≤ b) :
    (∀ (K : DerivedCategory C) [K.IsGE a] [K.IsLE b],
        (∀ i ∈ Set.Icc a b,
          E.binaryProductsClosure.retractClosure ((homologyFunctor C i).obj K)) →
        ((⨆ i ∈ Set.Icc a b,
            E.map (singleFunctor C i)).binaryProductsClosure.extensionProductIter
          (b - a).toNat).retractClosure K) ∧
    (∀ (L : CochainComplex C ℤ) [L.IsStrictlyGE a] [L.IsStrictlyLE b],
        (∀ i ∈ Set.Icc a b, E.binaryProductsClosure.retractClosure (L.X i)) →
        ((⨆ i ∈ Set.Icc a b,
            E.map (singleFunctor C i)).binaryProductsClosure.extensionProductIter
          (b - a).toNat).retractClosure (Q.obj L))

Tag 0FX8, a lemma

Tag 0FX8 in the Stacks Project.

CategoryTheory.Functor.isZero_obj_shift_of_retractClosure_extensionProductIter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/OperationsOnFullSubcategories.lean, line 659.

Let H : C ⥤ A be a homological functor from a triangulated category to an abelian category, with H^i(X) = H(X⟦i⟧), and let E be a class of objects of C such that H^i(E) = 0 for E ∈ E and i ∉ [a, b]. Then every object X which is a direct summand of an n-fold extension of finite direct sums of objects E⟦-j⟧ with E ∈ E and j ∈ [c, d] satisfies H^i(X) = 0 for i ∉ [a + c, b + d]. In the notation of [Stacks, Tag 0FX0], for X ∈ smd(add(E[c, d])^{⋆ (n + 1)}) we have H^i(X) = 0 for i ∉ [a + c, b + d]; the window does not depend on the number of extensions, so it is sharper than the window [-m + na, m + nb] of [Stacks, Tag 0FX8], which it implies for a ≤ 0 ≤ b, c = -m, d = m.

theorem isZero_obj_shift_of_retractClosure_extensionProductIter
    (H : C ⥤ A) [H.IsHomological] (E : ObjectProperty C) {a b : ℤ}
    (hE : ∀ ⦃Y : C⦄, E Y → ∀ i ∉ Set.Icc a b, IsZero (H.obj (Y⟦i⟧)))
    (c d : ℤ) (n : ℕ) {X : C}
    (hX : ((⨆ j ∈ Set.Icc c d,
      E.isoClosure.shift j).binaryProductsClosure.extensionProductIter n).retractClosure X)
    {i : ℤ} (hi : i ∉ Set.Icc (a + c) (b + d)) :
    IsZero (H.obj (X⟦i⟧))

Sources

LeanclosedUnderDirectSums_add_star_add · closedUnderDirectSums_smd_add · CategoryTheory.ObjectProperty.retractClosure_extensionProductIter_isClosedUnderBinaryProducts_and_add · Stacks.TriangulatedGenerators.retractClosure_extensionProductIter_biSup_shift_inverseImage_of_le · DerivedCategory.prop_retractClosure_extensionProductIter_of_prop_homology_and_of_prop_X · CategoryTheory.Functor.isZero_obj_shift_of_retractClosure_extensionProductIter

Section13.36 Generators of triangulated categories #

Section 13.36 of the Stacks Project, Tag 09SI. 7 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FX9, a lemma

Tag 0FX9 in the Stacks Project.

CategoryTheory.ObjectProperty.triangEnvelopeIter_eq_iSup_retractClosure_extensionProductIter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/Generators.lean, line 376.

Only boundedly many shifts are needed in the triangulated envelope: the objects reachable from P by shifts, finite direct sums, retracts and at most n extensions form the increasing union, over m : ℕ, of the objects reachable in the same way but using only the shifts of P in the range [-m, m]. In the notation of the Stacks project, for n ≥ 1 we have ⟨E⟩ₙ = ⋃_{m ≥ 1} smd(add(E[-m, m])^{⋆ n}).

public theorem triangEnvelopeIter_eq_iSup_retractClosure_extensionProductIter
    (P : ObjectProperty C) (n : ℕ) :
    P.triangEnvelopeIter n =
      ⨆ m : ℕ, ((⨆ i ∈ Set.Icc (-(m : ℤ)) (m : ℤ),
        P.isoClosure.shift i).binaryProductsClosure.extensionProductIter n).retractClosure

Tag 0ATG, a lemma

Tag 0ATG in the Stacks Project.

CategoryTheory.ObjectProperty.triangEnvelope_eq_iSup_and_isSaturated_and_le_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/Generators.lean, line 438. References: SGA 4½ Etat 0 (2.3.3), “more general”.

The triangulated envelope ⟨P⟩ = ⋃ₙ ⟨P⟩ₙ of a nonempty object property P of a triangulated category is the union over n, m of the subcategories smd(add(P[-m, m])^{⋆ n}); it is closed under isomorphisms (strictly full), saturated (thick) and a triangulated subcategory; and it is contained in a strictly full, saturated triangulated subcategory Q exactly when P is, so that it is the smallest such subcategory containing P.

public theorem triangEnvelope_eq_iSup_and_isSaturated_and_le_iff
    (P : ObjectProperty C) [P.Nonempty] [IsTriangulated C] :
    (P.triangEnvelope = ⨆ n : ℕ, ⨆ m : ℕ,
        ((⨆ i ∈ Set.Icc (-(m : ℤ)) (m : ℤ),
          P.isoClosure.shift i).binaryProductsClosure.extensionProductIter n).retractClosure) ∧
      P.triangEnvelope.IsClosedUnderIsomorphisms ∧ P.triangEnvelope.IsSaturated ∧
      P.triangEnvelope.IsTriangulated ∧
      ∀ Q : ObjectProperty C, Q.IsClosedUnderIsomorphisms → Q.IsSaturated → Q.IsTriangulated →
        (P.triangEnvelope ≤ Q ↔ P ≤ Q)

Tag 09SJ, a definition

Tag 09SJ in the Stacks Project.

CategoryTheory.ObjectProperty.IsWeakTriangulatedGenerator, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/Generators.lean, line 468. The attribute's comment: “(3)”.

A property of objects P of a category C with zero morphisms and a shift by ℤ is a weak generator, or simply a generator, if every object K receiving only zero maps from the shifts of the objects satisfying P is zero; equivalently, if every nonzero object K admits an integer n and a nonzero map E ⟶ K⟦n⟧ from an object E satisfying P (isWeakTriangulatedGenerator_iff).

public def IsWeakTriangulatedGenerator (P : ObjectProperty C) : Prop

CategoryTheory.ObjectProperty.isWeakTriangulatedGenerator_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/Generators.lean, line 477. The attribute's comment: “(3), in the source's literal form: for every nonzero K an integer n and a nonzero map E ⟶ K⟦n⟧”.

A weak generator in the source's own words: P is a weak generator if and only if for every nonzero object K there are an object E satisfying P, an integer n and a nonzero map E ⟶ K⟦n⟧. For P = ObjectProperty.singleton E this is literally Definition [Stacks, Tag 09SJ](3).

public theorem isWeakTriangulatedGenerator_iff (P : ObjectProperty C) :
    P.IsWeakTriangulatedGenerator ↔
      ∀ K : C, ¬ IsZero K → ∃ E, P E ∧ ∃ (n : ℤ) (f : E ⟶ K⟦n⟧), f ≠ 0

Tag 09SK, a lemma

Tag 09SK in the Stacks Project.

Stacks.TriangulatedGenerators.hom_vanishing_iff_gen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/Generators.lean, line 861.

Stacks tag 09SK (Lemma 13.36.4). For objects E, K of a triangulated category D, the following are equivalent: 1. Hom(E, K[i]) = 0 for all i : ℤ; 2. Hom(E', K) = 0 for all E' ∈ ⟨E⟩.

theorem hom_vanishing_iff_gen (E K : D) :
    (∀ i : ℤ, ∀ f : E ⟶ (shiftFunctor D i).obj K, f = 0) ↔
      (∀ E' ∈ gen E, ∀ f : E' ⟶ K, f = 0)

Tag 09SL, a lemma

Tag 09SL in the Stacks Project.

CategoryTheory.ObjectProperty.IsClassicalTriangulatedGenerator.isZero_of_rightOrthogonal_shiftClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/Generators.lean, line 534.

Stacks 09SL: a classical generator of a (pre)triangulated category is a weak generator. If the triangulated envelope of an object property P is everything, then an object Y which receives only zero maps from the shifts of the objects of P — equivalently, an object Y with Hom(X, Y⟦n⟧) = 0 for every X satisfying P and every n : ℤ — is a zero object.

public theorem IsClassicalTriangulatedGenerator.isZero_of_rightOrthogonal_shiftClosure
    {P : ObjectProperty C} (hP : P.IsClassicalTriangulatedGenerator) {Y : C}
    (hY : (P.shiftClosure ℤ).rightOrthogonal Y) : IsZero Y

Tag 0FXA, a lemma

Tag 0FXA in the Stacks Project.

CategoryTheory.ObjectProperty.IsClassicalTriangulatedGenerator.isStrongTriangulatedGenerator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/Generators.lean, line 617.

Stacks 0FXA: in a triangulated category which has a strong generator, every classical generator is a strong generator. Here the ambient strong generator is a finite family of objects X : ι → C (the source's case is a single object, ι = Unit), and the classical generator is an object property P (the source's case is P = ObjectProperty.singleton E).

public theorem IsClassicalTriangulatedGenerator.isStrongTriangulatedGenerator [IsTriangulated C]
    {P : ObjectProperty C} (hP : P.IsClassicalTriangulatedGenerator)
    {ι : Type*} [Finite ι] {X : ι → C} (hX : (ofObj X).IsStrongTriangulatedGenerator) :
    P.IsStrongTriangulatedGenerator

Tag 0ATH, a remark

Tag 0ATH in the Stacks Project.

CategoryTheory.ObjectProperty.triangEnvelope_singleton_le_of_sums_of_extensions_of_summands, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/TriangulatedEnvelopeInduction.lean, line 57.

Let E be an object of a triangulated category and let T be a property of objects which is inherited by finite direct sums, satisfies the two-out-of-three property for distinguished triangles, is inherited by direct summands, and holds on all shifts of E. Then T holds on every object of the triangulated subcategory ⟨E⟩ generated by E.

theorem triangEnvelope_singleton_le_of_sums_of_extensions_of_summands
    [IsTriangulated C] (E : C) (T : ObjectProperty C)
    (_hsum : ∀ K L : C, T K → T L → T (K ⊞ L))
    (hext₁ : ∀ Tr ∈ distTriang C, T Tr.obj₂ → T Tr.obj₃ → T Tr.obj₁)
    (hext₂ : ∀ Tr ∈ distTriang C, T Tr.obj₁ → T Tr.obj₃ → T Tr.obj₂)
    (hext₃ : ∀ Tr ∈ distTriang C, T Tr.obj₁ → T Tr.obj₂ → T Tr.obj₃)
    (hsummand : ∀ K L : C, T (K ⊞ L) → T K ∧ T L)
    (hshift : ∀ n : ℤ, T ((CategoryTheory.shiftFunctor C n).obj E)) :
    (ObjectProperty.singleton E).triangEnvelope ≤ T

Sources

LeanCategoryTheory.ObjectProperty.triangEnvelopeIter_eq_iSup_retractClosure_extensionProductIter · CategoryTheory.ObjectProperty.triangEnvelope_eq_iSup_and_isSaturated_and_le_iff · CategoryTheory.ObjectProperty.IsWeakTriangulatedGenerator · CategoryTheory.ObjectProperty.isWeakTriangulatedGenerator_iff · Stacks.TriangulatedGenerators.hom_vanishing_iff_gen · CategoryTheory.ObjectProperty.IsClassicalTriangulatedGenerator.isZero_of_rightOrthogonal_shiftClosure · CategoryTheory.ObjectProperty.IsClassicalTriangulatedGenerator.isStrongTriangulatedGenerator · CategoryTheory.ObjectProperty.triangEnvelope_singleton_le_of_sums_of_extensions_of_summands

Section13.37 Compact objects #

Section 13.37 of the Stacks Project, Tag 09SM. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07LS, a definition

Tag 07LS in the Stacks Project.

CategoryTheory.IsCompactObject, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/CompactObjects/ThickSubcategory.lean, line 106.

An object K of a preadditive category is compact if for every family E : I → C whose direct sum exists, the map ⨁ i, (K ⟶ E i) → (K ⟶ ∐ E) sending a finitely supported family (f i) to ∑ i, f i ≫ Sigma.ι E i is bijective; that is, a morphism from K into a direct sum factors through a finite subsum in exactly one way.

public class IsCompactObject (K : C) : Prop

Tag 09QH, a lemma

Tag 09QH in the Stacks Project.

CategoryTheory.isClosedUnderIsomorphisms_isTriangulated_isSaturated_and_isIdempotentComplete_isCompactObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/CompactObjects/ThickSubcategory.lean, line 532.

The compact objects of a pre-triangulated category D with direct sums form the objects of a Karoubian, saturated, strictly full, pre-triangulated subcategory of D: the property of being compact is closed under isomorphisms, is a triangulated subcategory of D, is saturated (closed under direct summands), and idempotents split in the full subcategory it spans.

public theorem
    isClosedUnderIsomorphisms_isTriangulated_isSaturated_and_isIdempotentComplete_isCompactObject :
    ObjectProperty.IsClosedUnderIsomorphisms (IsCompactObject.{w, _, _} (C := D)) ∧
      ObjectProperty.IsTriangulated (IsCompactObject.{w, _, _} (C := D)) ∧
      ObjectProperty.IsSaturated (IsCompactObject.{w, _, _} (C := D)) ∧
      IsIdempotentComplete
        (ObjectProperty.FullSubcategory (IsCompactObject.{w, _, _} (C := D)))

Tag 09SN, a lemma

Tag 09SN in the Stacks Project.

CategoryTheory.Pretriangulated.exists_isHomotopyColimit_of_compactlyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/CompactObjects/CellStructure.lean, line 723.

Stacks 09SN. Let D be a pre-triangulated category with direct sums and let E : ι → D be a family of compact objects such that ⨁ E i generates D, i.e. the only objects right orthogonal to all shifts of the E i are the zero objects. Then every object X of D is a derived colimit X = hocolim Xₙ of a system F : ℕ ⥤ D whose first term F.obj 0 is a direct sum of shifts of the E i and each of whose transition morphisms Xₙ ⟶ Xₙ₊₁ fits into a distinguished triangle Yₙ ⟶ Xₙ ⟶ Xₙ₊₁ ⟶ Yₙ⟦1⟧ with Yₙ a direct sum of shifts of the E i.

public theorem exists_isHomotopyColimit_of_compactlyGenerated
    {ι : Type v} (E : ι → D) [∀ i, IsCompactObject.{v} (E i)]
    (hE : ∀ Y : D, ((ofObj E).shiftClosure ℤ).rightOrthogonal Y → IsZero Y) (X : D) :
    ∃ F : ℕ ⥤ D,
      IsHomotopyColimit F X ∧
      (⨆ J : Type v, ((ofObj E).shiftClosure ℤ).colimitsOfShape (Discrete J)) (F.obj 0) ∧
      ∀ n : ℕ, ∃ Y : D,
        (⨆ J : Type v, ((ofObj E).shiftClosure ℤ).colimitsOfShape (Discrete J)) Y ∧
        ∃ (f : Y ⟶ F.obj n) (g : F.obj (n + 1) ⟶ Y⟦(1 : ℤ)⟧),
          Triangle.mk f (F.map (homOfLE (Nat.le_succ n))) g ∈ distTriang D

Tag 09SP, a lemma

Tag 09SP in the Stacks Project.

CategoryTheory.Pretriangulated.exists_fac_triangEnvelope_of_isCompactObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/CompactObjects/CompactGenerators.lean, line 323.

Stacks 09SP. Let D be a triangulated category with direct sums, E : ι → D a family of compact objects, and X : ℕ → D a system of cell attachments as in [Stacks, Tag 09SN]: X 0 is a direct sum of shifts of the E i and each X (n + 1) fits into a distinguished triangle Yₙ ⟶ X n ⟶ X (n + 1) ⟶ Yₙ⟦1⟧ with Yₙ a direct sum of shifts of the E i. Then every morphism φ : C ⟶ X n from a compact object C factors as C ⟶ Z ⟶ X n with Z an object of the triangulated envelope ⟨E_{i₁} ⊕ … ⊕ E_{i_t}⟩ of a finite direct sum of the E i.

public theorem exists_fac_triangEnvelope_of_isCompactObject
    {ι : Type v} (E : ι → D) [∀ i, IsCompactObject.{v} (E i)] {X : ℕ → D}
    (hX₀ : (⨆ J : Type v, ((ofObj E).shiftClosure ℤ).colimitsOfShape (Discrete J)) (X 0))
    (hX : ∀ n : ℕ, ∃ Y : D,
      (⨆ J : Type v, ((ofObj E).shiftClosure ℤ).colimitsOfShape (Discrete J)) Y ∧
        ∃ (f : Y ⟶ X n) (g : X n ⟶ X (n + 1)) (h : X (n + 1) ⟶ Y⟦(1 : ℤ)⟧),
          Triangle.mk f g h ∈ distTriang D)
    {C : D} [IsCompactObject.{v} C] {n : ℕ} (φ : C ⟶ X n) :
    ∃ (s : Finset ι) (Z : D), (ObjectProperty.singleton (∐ fun i : s ↦ E i)).triangEnvelope Z ∧
      ∃ (a : C ⟶ Z) (b : Z ⟶ X n), a ≫ b = φ

Tag 09SQ, a definition

Tag 09SQ in the Stacks Project.

CategoryTheory.Pretriangulated.IsCompactlyGenerated, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/CompactObjects/CellStructure.lean, line 142.

A category D with a shift by ℤ is compactly generated if there is a family E : ι → D of compact objects, indexed by a type ι : Type w, which is a weak generator: the only objects of D receiving only zero maps from the shifts (E i)⟦n⟧ are the zero objects. When D has direct sums indexed by Type w this says that ⨁ E i generates D, as in Definition [Stacks, Tag 09SQ] — see ObjectProperty.isWeakTriangulatedGenerator_ofObj_iff.

public def IsCompactlyGenerated : Prop

CategoryTheory.ObjectProperty.isWeakTriangulatedGenerator_ofObj_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/CompactObjects/CompactGenerators.lean, line 396. The attribute's comment: “the source's form of the generation condition: the direct sum ∐ E is a weak generator”.

A family of objects is a weak generator if and only if its direct sum is one: for a family E : ι → C whose coproduct exists, the property of belonging to E is a weak generator exactly when the single object ∐ E is. This identifies the family-wise condition with the source's condition on ⨁ E i in Definition [Stacks, Tag 09SQ].

public theorem isWeakTriangulatedGenerator_ofObj_iff {C : Type u} [Category.{v} C]
    [HasZeroMorphisms C] [HasShift C ℤ] {ι : Type w} (E : ι → C) [HasCoproduct E] :
    (ofObj E).IsWeakTriangulatedGenerator ↔
      (ObjectProperty.singleton (∐ E)).IsWeakTriangulatedGenerator

Tag 09SR, a proposition

Tag 09SR in the Stacks Project.

CategoryTheory.ObjectProperty.isWeakTriangulatedGenerator_iff_triangEnvelope_eq_isCompactObject_and_isCompactlyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/CompactObjects/CompactGenerators.lean, line 714.

Stacks 09SR. Let D be a triangulated category with direct sums and let E be a compact object of D. Then E is a weak generator of D if and only if E is a classical generator of the subcategory D_c of compact objects, i.e. the triangulated envelope ⟨E⟩ is exactly the property of being a compact object, and D is compactly generated.

public theorem
    isWeakTriangulatedGenerator_iff_triangEnvelope_eq_isCompactObject_and_isCompactlyGenerated
    (E : D) [IsCompactObject.{v} E] :
    (ObjectProperty.singleton E).IsWeakTriangulatedGenerator ↔
      (ObjectProperty.singleton E).triangEnvelope = IsCompactObject.{v, _, _} (C := D) ∧
        IsCompactlyGenerated.{v} D

Sources

LeanCategoryTheory.IsCompactObject · CategoryTheory.isClosedUnderIsomorphisms_isTriangulated_isSaturated_and_isIdempotentComplete_isCompactObject · CategoryTheory.Pretriangulated.exists_isHomotopyColimit_of_compactlyGenerated · CategoryTheory.Pretriangulated.exists_fac_triangEnvelope_of_isCompactObject · CategoryTheory.Pretriangulated.IsCompactlyGenerated · CategoryTheory.ObjectProperty.isWeakTriangulatedGenerator_ofObj_iff · CategoryTheory.ObjectProperty.isWeakTriangulatedGenerator_iff_triangEnvelope_eq_isCompactObject_and_isCompactlyGenerated

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

13.18 Injective resolutions to 13.37 Compact objects

Section13.18 Injective resolutions#

Tag 013I, a definition

Tag 013J, a lemma

Tag 013K, a lemma

Tag 013R, a lemma

Tag 05TF, a remark

Tag 013P, a lemma

Tag 013S, a lemma

Tag 05TG, a lemma

Tag 013T, a lemma

Sources

Section13.19 Projective resolutions#

Tag 0644, a definition

Tag 0645, a lemma

Tag 0646, a lemma

Tag 0647, a lemma

Tag 0648, a remark

Tag 0649, a lemma

Tag 064A, a lemma

Tag 064B, a lemma

Tag 064C, a lemma

Tag 064D, a lemma

Tag 064E, a lemma

Sources

Section13.20 Right derived functors and injective resolutions#

Tag 05TH, a lemma

Tag 05TI, a lemma

Tag 0159, a lemma

Tag 015B, a lemma

Sources

Section13.21 Cartan-Eilenberg resolutions#

Tag 015H, a definition

Tag 015I, a lemma

Tag 015J, a lemma

Sources

Section13.22 Composition of right derived functors#

Tag 015M, a lemma

Tag 015N, a lemma

Sources

Section13.23 Resolution functors#

Tag 013V, a proposition

Tag 013W, a definition

Tag 05TJ, a lemma

Tag 013X, a lemma

Tag 014W, a lemma

Tag 05TK, a lemma

Sources

Section13.24 Functorial injective embeddings and resolution functors#

Tag 0141, a lemma

Sources

Section13.25 Right derived functors via resolution functors#

Tag 05TN, a lemma

Sources

Section13.26 Filtered derived category and injective resolutions#

Tag 015P, a definition

Tag 05TP, a lemma

Tag 05TQ, a lemma

Tag 05TR, a lemma

Tag 05TS, a lemma

Tag 05TT, a lemma

Tag 05TU, a lemma

Tag 05TV, a lemma

Tag 05TW, a lemma

Tag 05TX, a lemma

Tag 05TY, a lemma

Tag 015Q, a lemma

Tag 015U, an equation

Tag 015V, an equation

Tag 015W, a lemma

Sources

Section13.27 Ext groups#

Tag 06XQ, a definition

Tag 06XR, a lemma

Tag 06XS, a lemma

Tag 06XT, a definition

Tag 06XU, a lemma

Tag 06XV, a lemma

Tag 0GSM, a lemma

Tag 0EWW, a lemma

Section13.18 Injective resolutions #

Section13.19 Projective resolutions #

Section13.20 Right derived functors and injective resolutions #

Section13.21 Cartan-Eilenberg resolutions #

Section13.22 Composition of right derived functors #

Section13.23 Resolution functors #

Section13.24 Functorial injective embeddings and resolution functors #

Section13.25 Right derived functors via resolution functors #

Section13.26 Filtered derived category and injective resolutions #

Section13.27 Ext groups #

Section13.28 K-groups #

Section13.29 Unbounded complexes #

Section13.30 Deriving adjoints #

Section13.31 K-injective complexes #

Section13.32 Bounded cohomological dimension #

Section13.33 Derived colimits #

Section13.34 Derived limits #

Section13.35 Operations on full subcategories #

Section13.36 Generators of triangulated categories #