12.24 Spectral sequences… to 12.32 Exactness of products

Section12.24 Spectral sequences: filtered complexes#

Section 12.24 of the Stacks Project, Tag 012K. 15 tags here are carried by 33 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 012L, a definition

Tag 012L in the Stacks Project.

CochainComplex.Filtered, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex/Defs.lean, line 49. The attribute's comment: “as a complex filtered by subcomplexes, the same datum as a complex of Fil(𝒜)”. References: EGA 0 (11.2.2).

A filtered complex of C: a cochain complex K^• together with a decreasing filtration F^pK^• of it by subcomplexes, i.e. a filtered object of CochainComplex C ℤ indexed by ℤᵒᵖ.

abbrev Filtered (C : Type u) [Category.{v} C] [HasZeroMorphisms C] : Type _

CochainComplex.ImageSystem.filtered, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex/ImageFiltration.lean, line 130. The attribute's comment: “a complex filtered by the images of a system of complexes mapping into it”.

The filtration of X^• by the images of a system, as a filtered complex in the sense of [Stacks, Tag 012L].

public def filtered : CochainComplex.Filtered C
Tag 012M, a lemma

Tag 012M in the Stacks Project.

CochainComplex.exists_cohomologicalSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex/Basic/Convergence.lean, line 775.

The spectral sequence of a filtered complex. For a filtered complex (K^•, F) of an abelian category, with Z_r^{p, q} = F^p K^n ⊓ (d^n)⁻¹(F^{p + r}K^{n + 1}) and D_r^{p, q} = Z_{r - 1}^{p + 1, q - 1} ⊔ d^{n - 1}(Z_{r - 1}^{p - r + 1, q + r - 2}) as subobjects of K^n, the quotients E_r^{p, q} = Z_r^{p, q} / (D_r^{p, q} ⊓ Z_r^{p, q}) are the pages of a cohomological spectral sequence whose differential is induced by d, whose zeroth page is gr^p K^•, and whose first page is therefore H^n(gr^p K^•).

public theorem exists_cohomologicalSpectralSequence
    {A : Type u} [Category.{v} A] [Abelian A]
    (K : FilteredObject (CochainComplex A ℤ) ℤᵒᵖ)
    (F : ∀ (_p n : ℤ), Subobject (K.X.X n))
    (hF : ∀ p n : ℤ, F p n = Subobject.mk ((K.filtration.ι.app (op p)).f n))
    (Z : ∀ (_r _p n : ℤ), Subobject (K.X.X n))
    (hZ : ∀ r p n : ℤ, Z r p n =
      F p n ⊓ (Subobject.pullback (K.X.d n (n + 1))).obj (F (p + r) (n + 1)))
    (D : ∀ (_r _p n : ℤ), Subobject (K.X.X n))
    (hD : ∀ 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))) :
    ∃ (E : CohomologicalSpectralSequence A 0)
      (e : ∀ (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 n : ℤ), n = p + q → ((E.page 0 le_rfl).X (p, q) ≅
        ((FilteredObject.gr p).obj K).X n)),
      (∀ (r p q n : ℤ) (hr : 0 ≤ r) (hn : n = p + q),
        ∃ δ : (Z r p n : A) ⟶ (Z r (p + r) (n + 1) : A),
          δ ≫ (Z r (p + r) (n + 1)).arrow = (Z r p n).arrow ≫ K.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 ≫ (E.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 n : ℤ) (hn : n = p + q) (u : (Z 0 p n : A) ⟶ (K.filtration.obj (op p)).X n),
        u ≫ (K.filtration.ι.app (op p)).f n = (Z 0 p n).arrow →
        cokernel.π (Subobject.ofLE _ _ (inf_le_right : D 0 p n ⊓ Z 0 p n ≤ Z 0 p n)) ≫
            (e 0 p q n le_rfl hn).inv ≫ (α p q n hn).hom =
          u ≫ (FilteredObject.grMapπ (FilteredObject.succHom p) K).f n) ∧
      (∀ (p q n : ℤ) (hn : n = p + q),
        (E.page 0 le_rfl).d (p, q) (p, q + 1) ≫ (α p (q + 1) (n + 1) (by omega)).hom =
          (α p q n hn).hom ≫
            ((FilteredObject.gr p).obj K).d n (n + 1)) ∧
      (∀ p q n : ℤ, n = p + q → Nonempty ((E.page 1).X (p, q) ≅
        ((FilteredObject.gr p).obj K).homology n))
Tag 012N, a lemma

Tag 012N in the Stacks Project.

CochainComplex.Filtered.exists_iso_firstPage_homology_d_eq_δ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex.lean, line 750. The attribute's comment: “(1)”.

Stacks 012N (1). Let E be the spectral sequence of the filtered complex K, presented on its first page as in [Stacks, Tag 012M]: E_1^{p, q} = Z_1^{p, q}/(D_1^{p, q} ∩ Z_1^{p, q}), with d_1 induced by d. Then E_1^{p, q} = H^{p + q}(gr^pK^•), the class of x ∈ Z_1^{p, q} ⊆ F^pK^{p + q} going to the class of its image in gr^pK^{p + q}, and under these identifications d_1^{p, q} is the boundary map in cohomology of the short exact sequence of complexes 0 → gr^{p + 1}K^• → F^pK^•/F^{p + 2}K^• → gr^pK^• → 0.

theorem exists_iso_firstPage_homology_d_eq_δ :
    ∃ ε : ∀ (p q n : ℤ) (_ : n = p + q),
        (E.page 1).X (p, q) ≅ ((gr p).obj K).homology n,
      (∀ (p q n : ℤ) (hn : n = p + q)
          (u : (cycles K.X K.step 1 p n : C) ⟶ (K.filtration.obj (op p)).X n)
          (_ : u ≫ (K.filtration.ι.app (op p)).f n = (cycles K.X K.step 1 p n).arrow)
          (hc : (u ≫ (grMapπ (succHom p) K).f n) ≫ ((gr p).obj K).d n (n + 1) = 0),
        cokernel.π (Subobject.ofLE _ _ (inf_le_right : boundaries K.X K.step 1 p n ⊓
            cycles K.X K.step 1 p n ≤ cycles K.X K.step 1 p n)) ≫
            (e p q n hn).inv ≫ (ε p q n hn).hom =
          ((gr p).obj K).liftCycles (u ≫ (grMapπ (succHom p) K).f n) (n + 1) (by simp) hc ≫
            ((gr p).obj K).homologyπ n) ∧
      ∀ (p q n : ℤ) (hn : n = p + q),
        (E.page 1).d (p, q) (p + 1, q) ≫ (ε (p + 1) q (n + 1) (by omega)).hom =
          (ε p q n hn).hom ≫
            (grMapCompShortComplex_shortExact (succHom (p + 1)) (succHom p) K).δ n (n + 1)
              (by simp)

CochainComplex.Filtered.d_gr_eq_zero_and_exists_iso_firstPage_d_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex.lean, line 802. The attribute's comment: “(2)”.

Stacks 012N (2). If d(F^pK) ⊆ F^{p + 1}K for all p, then d induces the zero differential on every gr^pK^•, so that E_1^{p, q} = gr^pK^{p + q}, the class of x ∈ Z_1^{p, q} = F^pK^{p + q} going to its image; and under these identifications d_1^{p, q} is the morphism gr^pK^{p + q} → gr^{p + 1}K^{p + q + 1} induced by d.

theorem d_gr_eq_zero_and_exists_iso_firstPage_d_eq
    (hd : ∀ p n : ℤ, (K.step (p + 1) (n + 1)).Factors ((K.step p n).arrow ≫ K.X.d n (n + 1))) :
    (∀ p i j : ℤ, ((gr p).obj K).d i j = 0) ∧
    ∃ ε : ∀ (p q n : ℤ) (_ : n = p + q), (E.page 1).X (p, q) ≅ ((gr p).obj K).X n,
      (∀ (p q n : ℤ) (hn : n = p + q)
          (u : (cycles K.X K.step 1 p n : C) ⟶ (K.filtration.obj (op p)).X n)
          (_ : u ≫ (K.filtration.ι.app (op p)).f n = (cycles K.X K.step 1 p n).arrow),
        cokernel.π (Subobject.ofLE _ _ (inf_le_right : boundaries K.X K.step 1 p n ⊓
            cycles K.X K.step 1 p n ≤ cycles K.X K.step 1 p n)) ≫
            (e p q n hn).inv ≫ (ε p q n hn).hom =
          u ≫ (grMapπ (succHom p) K).f n) ∧
      ∀ (p q n : ℤ) (hn : n = p + q), ∃ μ : ((gr p).obj K).X n ⟶ ((gr (p + 1)).obj K).X (n + 1),
        (∀ (v : (K.filtration.obj (op p)).X n ⟶ (K.filtration.obj (op (p + 1))).X (n + 1)),
          v ≫ (K.filtration.ι.app (op (p + 1))).f (n + 1) =
              (K.filtration.ι.app (op p)).f n ≫ K.X.d n (n + 1) →
            (grMapπ (succHom p) K).f n ≫ μ = v ≫ (grMapπ (succHom (p + 1)) K).f (n + 1)) ∧
        (E.page 1).d (p, q) (p + 1, q) ≫ (ε (p + 1) q (n + 1) (by omega)).hom =
          (ε p q n hn).hom ≫ μ
Tag 012O, a lemma

Tag 012O in the Stacks Project.

FilteredComplexSpectralSequence.spectralSequenceMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex/Functoriality.lean, line 204. References: EGA 0 (11.2.3), “existence of E(u)”; EGA 0 (11.2.2), “functoriality”.

A morphism φ : K ⟶ L of filtered complexes, i.e. carrying each F^p K^n into F^p L^n, induces a morphism of spectral sequences E_r(K) ⟶ E_r(L): on the r-th pages it is the map Z_r^{p,q}(K)/D_r^{p,q}(K) ⟶ Z_r^{p,q}(L)/D_r^{p,q}(L) induced by φ, and these maps commute with the differentials d_r and the identifications H(E_r) = E_{r+1}.

noncomputable def spectralSequenceMap :
    spectralSequence K FK hantiK ⟶ spectralSequence L FL hantiL
Tag 012P, a definition

Tag 012P in the Stacks Project.

CochainComplex.Filtered.inducedFilteredObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Convergence.lean, line 271. The attribute's comment: “the induced filtration of H^n(K^•), bundled as an object of Fil(𝒜)”. References: EGA 0 (11.2.2).

The cohomology of a filtered complex, filtered. H^n(K^•) together with the filtration F^pH^n(K^•) = Im(H^n(F^pK^•) ⟶ H^n(K^•)) induced on it by (K^•, F) ([Stacks, Tag 012P]), as an object of Fil(C) = CategoryTheory.FilteredObject C ℤᵒᵖ. Packaging the induced filtration this way is what lets CategoryTheory.FilteredObject.gr p be applied to it, so that the graded pieces gr^pH^n(K^•) are the values of a functor.

noncomputable def inducedFilteredObject (K : Filtered C) (n : ℤ) : FilteredObject C ℤᵒᵖ

CochainComplex.Filtered.inducedFiltration, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex/Defs.lean, line 72.

The filtration of H^n(K^•) induced by a filtered complex K^•, with steps F^pH^n(K^•) = Im(H^n(F^pK^•) ⟶ H^n(K^•)).

noncomputable def inducedFiltration : Filtration (K.X.homology n) ℤᵒᵖ

CochainComplex.Filtered.inducedFilteredObjectFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Leray/FunctorialFilteredAbutment.lean, line 118. The attribute's comment: “the induced filtration of H^n, functorially in the filtered complex”.

The cohomology H^n of a functorial filtered complex, with its induced filtration, as a functor to Fil(𝒜).

def inducedFilteredObjectFunctor (G : D ⥤ Filtered C) (n : ℤ) : D ⥤ FilteredObject C ℤᵒᵖ
Tag 012R, an equation

Tag 012R in the Stacks Project.

sub_image_homologyMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex/Basic/InducedFiltration.lean, line 601.

Stacks 012R. The step F^{p'}H^n(K^•) of the induced filtration on cohomology, read as a subobject of K^n, is Ker(d^n) ∩ F^{p'}K^n + Im(d^{n-1}).

lemma sub_image_homologyMap (F : ℤ → ∀ m : ℤ, Subobject (K.X.X m))
    (hF : ∀ p' m : ℤ, F p' m = Subobject.mk ((K.filtration.ι.app (op p')).f m)) (p' : ℤ) :
    (Subobject.exists (K.X.iCycles n)).obj ((Subobject.pullback (K.X.homologyπ n)).obj
        (Subobject.mk (image.ι (HomologicalComplex.homologyMap
          (K.filtration.ι.app (op p')) n))))
      = kernelSubobject (K.X.d n (n + 1)) ⊓ F p' n ⊔ imageSubobject (K.X.d (n - 1) n)
Tag 0BDT, an equation

Tag 0BDT in the Stacks Project.

CochainComplex.Filtered.exists_iso_gradedHomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex.lean, line 419.

Stacks 0BDT. The graded piece gr^pH^n(K^•) = F^pH^n(K^•)/F^{p + 1}H^n(K^•) of the filtration induced on cohomology is (Ker(d) ∩ F^pK^n)/(Ker(d) ∩ F^{p + 1}K^n + Im(d) ∩ F^pK^n): there is an isomorphism between the two compatible with the canonical maps to both from the cycles of K^• lying in F^pK^n.

theorem exists_iso_gradedHomology (p n : ℤ) :
    ∃ (a : (K.cyclesInStep p n : C) ⟶
        (kernelSubobject (K.X.d n (n + 1)) ⊓ K.step p n : Subobject (K.X.X n)))
      (b : (K.cyclesInStep p n : C) ⟶
        image (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n))
      (e : cokernel (Subobject.ofLE _ _ (K.kernel_inf_step_succ_sup_image_inf_step_le p n)) ≅
        K.gradedHomology p n),
      a ≫ (kernelSubobject (K.X.d n (n + 1)) ⊓ K.step p n).arrow =
        (K.cyclesInStep p n).arrow ≫ K.X.iCycles n ∧
      b ≫ image.ι (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n) =
        (K.cyclesInStep p n).arrow ≫ K.X.homologyπ n ∧
      a ≫ cokernel.π (Subobject.ofLE _ _ (K.kernel_inf_step_succ_sup_image_inf_step_le p n)) ≫
          e.hom =
        b ≫ cokernel.π (image.preComp
          (HomologicalComplex.homologyMap (K.filtration.diagram.map
            (homOfLE (Int.le_add_one le_rfl) : (p : ℤ) ⟶ p + 1).op) n)
          (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n))
Tag 012Q, a lemma

Tag 012Q in the Stacks Project.

CochainComplex.exists_epi_gradedPiece_homology_of_isGLB_isLUB, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex/Basic/StablePage.lean, line 569.

Stacks 012Q. Let 𝒜 be an abelian category and let (K^•, F) be a filtered complex of 𝒜, with degreewise filtration subobjects F^p K^n. Fix p, n : ℤ and write q = n - p. Assume the stable cycles Z_∞^{p, q} and the stable boundaries B_∞^{p, q} exist, i.e. that Z is the greatest lower bound of the subobjects F^p K^n ∩ (d^n)⁻¹(F^\{p + r}K^\{n + 1}) + F^\{p + 1}K^n and B the least upper bound of the subobjects F^p K^n ∩ d^{n - 1}(F^{p - r}K^{n - 1}) + F^{p + 1}K^n of K^n. Then B_∞^{p, q} ≤ Z_∞^{p, q}, so the limit E_∞^{p, q} = Z_∞^{p, q}/B_∞^{p, q} exists, and the graded piece gr^p H^n(K^•) of the induced filtration on cohomology is a subquotient of it: the object A = Ker(d^n) ∩ F^p K^n maps to Z_∞^{p, q} and to F^p H^n(K^•), its image S in E_∞^{p, q} is a subobject of E_∞^{p, q}, and the induced map S ⟶ gr^p H^n(K^•) is an epimorphism.

public theorem exists_epi_gradedPiece_homology_of_isGLB_isLUB
    {C : Type u} [Category.{v} C] [Abelian C]
    (K : FilteredObject (CochainComplex C ℤ) ℤᵒᵖ) (p n : ℤ)
    (F : ℤ → ∀ m : ℤ, Subobject (K.X.X m))
    (hF : ∀ p' m : ℤ, F p' m = Subobject.mk ((K.filtration.ι.app (op p')).f m))
    (A : Subobject (K.X.cycles n)) (hA : A = (Subobject.pullback (K.X.iCycles n)).obj (F p n))
    (Z B : Subobject (K.X.X n))
    (hZ : IsGLB (Set.range fun r : ℕ =>
      F p n ⊓ (Subobject.pullback (K.X.d n (n + 1))).obj (F (p + r) (n + 1)) ⊔ F (p + 1) n) Z)
    (hB : IsLUB (Set.range fun r : ℕ =>
      F p n ⊓ (Subobject.«exists» (K.X.d (n - 1) n)).obj (F (p - r) (n - 1)) ⊔ F (p + 1) n) B) :
    B ≤ Z ∧
    ∃ (a : (A : C) ⟶ (Z : C))
      (b : (A : C) ⟶ image (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n))
      (S : Subobject (cokernel (Subobject.ofLE (B ⊓ Z) Z inf_le_right)))
      (g : (A : C) ⟶ (S : C))
      (e : (S : C) ⟶ cokernel (image.preComp
        (HomologicalComplex.homologyMap (K.filtration.diagram.map
          (homOfLE (Int.le_add_one le_rfl) : (p : ℤ) ⟶ p + 1).op) n)
        (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n))),
      A.arrow ≫ K.X.iCycles n = a ≫ Z.arrow ∧
      A.arrow ≫ K.X.homologyπ n =
        b ≫ image.ι (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n) ∧
      Epi g ∧ Epi e ∧
      g ≫ S.arrow = a ≫ cokernel.π (Subobject.ofLE (B ⊓ Z) Z inf_le_right) ∧
      g ≫ e = b ≫ cokernel.π (image.preComp
        (HomologicalComplex.homologyMap (K.filtration.diagram.map
          (homOfLE (Int.le_add_one le_rfl) : (p : ℤ) ⟶ p + 1).op) n)
        (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n))
Tag 0BDU, a definition

Tag 0BDU in the Stacks Project.

IsRegularChainComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Boundedness.lean, line 45. The attribute's comment: “regular”.

A cohomological spectral sequence E (with d_r of bidegree (r, 1 - r)) is regular if for every (p, q) : ℤ × ℤ there exists b : ℤ such that the differential d_r^{p,q} : E_r^{p,q} → E_r^{p + r, q - r + 1} is zero for all r ≥ b (with r₀ ≤ r).

def IsRegularChainComplex (E : CohomologicalSpectralSequence C r₀) : Prop

IsCoregular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Boundedness.lean, line 54. The attribute's comment: “coregular”.

A cohomological spectral sequence E (with d_r of bidegree (r, 1 - r)) is coregular if for every (p, q) : ℤ × ℤ there exists b : ℤ such that the differential d_r^{p - r, q + r - 1} : E_r^{p-r, q+r-1} → E_r^{p, q} is zero for all r ≥ b (with r₀ ≤ r).

def IsCoregular (E : CohomologicalSpectralSequence C r₀) : Prop

IsBounded, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Boundedness.lean, line 62. The attribute's comment: “bounded”. References: EGA 0 (11.1.1), “partial”.

A cohomological spectral sequence E is bounded if for every total degree n : ℤ there are only finitely many pairs p : ℤ such that E_{r₀}^{p, n - p} is nonzero.

def IsBounded (E : CohomologicalSpectralSequence C r₀) : Prop

IsBoundedBelow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Boundedness.lean, line 69. The attribute's comment: “bounded below”.

A cohomological spectral sequence E is bounded below if for every total degree n : ℤ there exists b : ℤ such that E_{r₀}^{p, n - p} = 0 for all p ≥ b.

def IsBoundedBelow (E : CohomologicalSpectralSequence C r₀) : Prop

IsBoundedAbove, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Boundedness.lean, line 76. The attribute's comment: “bounded above”.

A cohomological spectral sequence E is bounded above if for every total degree n : ℤ there exists b : ℤ such that E_{r₀}^{p, n - p} = 0 for all p ≤ b.

def IsBoundedAbove (E : CohomologicalSpectralSequence C r₀) : Prop
Tag 0BDV, a lemma

Tag 0BDV in the Stacks Project.

CohomologicalSpectralSequence.isRegularChainComplex_iff_Z_eventually_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Boundedness.lean, line 175. The attribute's comment: “(1)”.

Part (1): the spectral sequence is regular iff for all p, q the cycles Z_r^{p,q} are eventually constant.

theorem isRegularChainComplex_iff_Z_eventually_constant :
    IsRegularChainComplex E ↔ ∀ p q : ℤ, ∃ b : ℤ, ∀ r, b ≤ r → E.Z (p, q) r = E.Z (p, q) b

CohomologicalSpectralSequence.isCoregular_iff_B_eventually_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Boundedness.lean, line 192. The attribute's comment: “(2)”.

Part (2): the spectral sequence is coregular iff for all p, q the boundaries B_r^{p,q} are eventually constant.

theorem isCoregular_iff_B_eventually_constant :
    IsCoregular E ↔ ∀ p q : ℤ, ∃ b : ℤ, ∀ r, b ≤ r → E.B (p, q) r = E.B (p, q) b

CohomologicalSpectralSequence.isBounded_iff_isBoundedBelow_and_isBoundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Boundedness.lean, line 206. The attribute's comment: “(3)”.

Part (3): the spectral sequence is bounded iff it is both bounded below and bounded above.

theorem isBounded_iff_isBoundedBelow_and_isBoundedAbove :
    IsBounded E ↔ IsBoundedBelow E ∧ IsBoundedAbove E

CohomologicalSpectralSequence.isRegularChainComplex_of_isBoundedBelow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Boundedness.lean, line 224. The attribute's comment: “(4)”.

Part (4): if the spectral sequence is bounded below, then it is regular.

theorem isRegularChainComplex_of_isBoundedBelow (h : IsBoundedBelow E) :
    IsRegularChainComplex E

CohomologicalSpectralSequence.isCoregular_of_isBoundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Boundedness.lean, line 234. The attribute's comment: “(5)”.

Part (5): if the spectral sequence is bounded above, then it is coregular.

theorem isCoregular_of_isBoundedAbove (h : IsBoundedAbove E) : IsCoregular E
Tag 012U, a definition

Tag 012U in the Stacks Project.

CochainComplex.Filtered.WeaklyConverges, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Defs/FilteredComplex.lean, line 211. The attribute's comment: “(1)”. References: EGA 0 (11.1.3), “special case”.

Stacks 012U (1). The spectral sequence of a filtered complex K weakly converges to H^*(K^•) if for all p, n the stable cycles Z_∞^{p, n - p} and boundaries B_∞^{p, n - p} exist and gr^p H^n(K^•) = E_∞^{p, n - p} via [Stacks, Tag 012Q]: there is an isomorphism E_∞^{p, n - p} = Z_∞^{p, n - p}/B_∞^{p, n - p} ≅ gr^p H^n(K^•) compatible with the canonical maps to both from Ker(d^n) ∩ F^p K^n.

def WeaklyConverges : Prop

CochainComplex.Filtered.Abuts, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Defs/FilteredComplex.lean, line 231. The attribute's comment: “(2)”.

Stacks 012U (2). The spectral sequence of a filtered complex K abuts to H^*(K^•) if it weakly converges to H^*(K^•) and for all n the induced filtration on H^n(K^•) is separated, ⋂_p F^p H^n(K^•) = 0, and exhaustive, ⋃_p F^p H^n(K^•) = H^n(K^•).

def Abuts : Prop

CochainComplex.Filtered.Converges, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Defs/FilteredComplex.lean, line 239. The attribute's comment: “(3)”.

Stacks 012U (3). The spectral sequence of a filtered complex K converges to H^*(K^•) if it is regular, abuts to H^*(K^•), and H^n(K^•) = lim_p H^n(K^•)/F^p H^n(K^•) for all n.

def Converges : Prop
Tag 012V, a lemma

Tag 012V in the Stacks Project.

CochainComplex.exists_iso_stablePage_iff_and_isGLB_isLUB_inducedFiltration_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex/Basic/StablePage.lean, line 648.

Stacks 012V. Let 𝒜 be an abelian category, let (K^•, F) be a filtered complex of 𝒜 with degreewise filtration subobjects F p n = F^p K^n, and fix p n : ℤ; write q = n - p, A = Ker(d^n) ∩ F^p K^n, N = Ker(d^n) ∩ F^p K^n + F^{p + 1}K^n (the left-hand side of the inclusion (012S)), D = Im(d^{n - 1}) ∩ F^p K^n + F^{p + 1}K^n (the right-hand side of the inclusion (012T)), and FH p' = F^{p'} H^n(K^•) for the induced filtration on cohomology. Then:

  1. whenever Z = Z_∞^{p, q} and B = B_∞^{p, q} exist, the graded piece gr^p H^n(K^•) is the whole of the limit E_∞^{p, q} = Z/B — that is, there is an isomorphism between them compatible with the two canonical maps out of A — if and only if Z = N and B = D, i.e. if and only if (012S) and (012T) are equalities;
  2. the induced filtration on H^n(K^•) is separated, ⋂_{p'} F^{p'} H^n(K^•) = 0, if and only if ⋂_{p'} (Ker(d^n) ∩ F^{p'}K^n + Im(d^{n - 1})) = Im(d^{n - 1}), and it is exhaustive, ⋃_{p'} F^{p'}H^n(K^•) = H^n(K^•), if and only if ⋃_{p'} (Ker(d^n) ∩ F^{p'}K^n + Im(d^{n - 1})) = Ker(d^n).

Weak convergence to H^*(K^•) is (1) for all p, n, and abutment is weak convergence together with (2) for all n.

public theorem exists_iso_stablePage_iff_and_isGLB_isLUB_inducedFiltration_iff
    {C : Type u} [Category.{v} C] [Abelian C]
    (K : FilteredObject (CochainComplex C ℤ) ℤᵒᵖ) (p n : ℤ)
    (F : ℤ → ∀ m : ℤ, Subobject (K.X.X m))
    (hF : ∀ p' m : ℤ, F p' m = Subobject.mk ((K.filtration.ι.app (op p')).f m))
    (A : Subobject (K.X.cycles n))
    (hA : A = (Subobject.pullback (K.X.iCycles n)).obj (F p n))
    (N D : Subobject (K.X.X n))
    (hN : N = kernelSubobject (K.X.d n (n + 1)) ⊓ F p n ⊔ F (p + 1) n)
    (hD : D = imageSubobject (K.X.d (n - 1) n) ⊓ F p n ⊔ F (p + 1) n)
    (FH : ℤ → Subobject (K.X.homology n))
    (hFH : ∀ p' : ℤ, FH p' =
      Subobject.mk (image.ι (HomologicalComplex.homologyMap (K.filtration.ι.app (op p')) n))) :
    (∀ Z B : Subobject (K.X.X n),
        IsGLB (Set.range fun r : ℕ =>
          F p n ⊓ (Subobject.pullback (K.X.d n (n + 1))).obj (F (p + r) (n + 1)) ⊔ F (p + 1) n) Z →
        IsLUB (Set.range fun r : ℕ =>
          F p n ⊓ (Subobject.«exists» (K.X.d (n - 1) n)).obj (F (p - r) (n - 1)) ⊔
            F (p + 1) n) B →
        ∀ a : (A : C) ⟶ (Z : C), a ≫ Z.arrow = A.arrow ≫ K.X.iCycles n →
        ∀ b : (A : C) ⟶ image (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n),
          b ≫ image.ι (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n) =
            A.arrow ≫ K.X.homologyπ n →
        ((∃ e : cokernel (Subobject.ofLE (B ⊓ Z) Z inf_le_right) ≅
              cokernel (image.preComp
                (HomologicalComplex.homologyMap (K.filtration.diagram.map
                  (homOfLE (Int.le_add_one le_rfl) : (p : ℤ) ⟶ p + 1).op) n)
                (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n)),
            a ≫ cokernel.π (Subobject.ofLE (B ⊓ Z) Z inf_le_right) ≫ e.hom =
              b ≫ cokernel.π (image.preComp
                (HomologicalComplex.homologyMap (K.filtration.diagram.map
                  (homOfLE (Int.le_add_one le_rfl) : (p : ℤ) ⟶ p + 1).op) n)
                (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n))) ↔
          Z = N ∧ B = D)) ∧
      (IsGLB (Set.range FH) ⊥ ↔
        IsGLB (Set.range fun p' : ℤ => kernelSubobject (K.X.d n (n + 1)) ⊓ F p' n ⊔
          imageSubobject (K.X.d (n - 1) n)) (imageSubobject (K.X.d (n - 1) n))) ∧
      (IsLUB (Set.range FH) ⊤ ↔
        IsLUB (Set.range fun p' : ℤ => kernelSubobject (K.X.d n (n + 1)) ⊓ F p' n ⊔
          imageSubobject (K.X.d (n - 1) n)) (kernelSubobject (K.X.d n (n + 1))))
Tag 012W, a lemma

Tag 012W in the Stacks Project.

CochainComplex.Filtered.abutsTo_of_isDegreewiseFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/AbutsTo.lean, line 132. The attribute's comment: “(2) and (3) together, in the form E abuts to H^*(K^•)”.

The spectral sequence of a degreewise finite filtered complex abuts to its cohomology.

The spectral sequence is presented as in [Stacks, Tag 012W]: by an isomorphism hE of each page with the subquotient Z_r^{p,q}/(D_r^{p,q} ⊓ Z_r^{p,q}) of K^n. This is the presentation in which [Stacks, Tag 012M], [Stacks, Tag 012W], [Stacks, Tag 0132] and [Stacks, Tag 015N] all state their conclusions, so a consumer which has invoked one of those already has the data to hand.

The filtration witnessing the abutment is the one [Stacks, Tag 012P] induces on H^n(K^•), and degreewise finiteness of the filtration of K^• is the only hypothesis.

theorem abutsTo_of_isDegreewiseFinite (K : Filtered C) (F : ∀ (_p n : ℤ), Subobject (K.X.X n))
    (hF : ∀ p n : ℤ, F p n = Subobject.mk ((K.filtration.ι.app (op p)).f n))
    (Z : ∀ (_r _p n : ℤ), Subobject (K.X.X n))
    (hZ : ∀ r p n : ℤ, Z r p n =
      F p n ⊓ (Subobject.pullback (K.X.d n (n + 1))).obj (F (p + r) (n + 1)))
    (D : ∀ (_r _p n : ℤ), Subobject (K.X.X n))
    (hD : ∀ 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)))
    (E : CohomologicalSpectralSequence C 0)
    (hE : ∀ (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)))
    (hK : K.filtration.IsDegreewiseFinite) :
    SpectralSequence.AbutsTo E (fun n => K.X.homology n)

CochainComplex.Filtered.abutsTo_of_isDegreewiseFinite', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/AbutsTo.lean, line 161. The attribute's comment: “(2) and (3), for the canonical spectral sequence of a filtered complex”. References: SGA 4 Vbis (2.5.2), “partial”.

The canonical spectral sequence of a degreewise finite filtered complex abuts to its cohomology. abutsTo_of_isDegreewiseFinite for CochainComplex.Filtered.spectralSequenceFunctor, whose pages are the subquotients Z_r^{p,q}/(D_r^{p,q} ⊓ Z_r^{p,q}) on the nose, so that the presentation hypotheses are discharged and degreewise finiteness is the only one left.

theorem abutsTo_of_isDegreewiseFinite' (K : Filtered C)
    (hK : K.filtration.IsDegreewiseFinite) :
    SpectralSequence.AbutsTo (spectralSequenceFunctor.obj K) (fun n => K.X.homology n)

CochainComplex.Filtered.nonempty_pageInfinityIso_gr', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Convergence.lean, line 801. The attribute's comment: “(3), the comparison E_∞^{p,q} ≅ gr^pH^n(K^•) of (012V) is an isomorphism”.

E_∞^{p,q} ≅ gr^p H^{p+q}(K^•). For a filtered complex (K^•, F) of an abelian category whose filtration is finite in each degree, the infinity page of its spectral sequence at the bidegree (p, q) is the p-th graded piece of the filtration induced on H^{p+q}(K^•).

This is the convergence datum of [Stacks, Tag 012W](3): the spectral sequence converges to H^*(K^•). Degreewise finiteness of the filtration is the only hypothesis; the boundedness, the finiteness of the induced filtration, the regularity and the two equalities (012S), (012T) that the statement of 012W lists separately are all consequences of it, and are discharged here.

The isomorphism is pageInfinityIsoGrAt at a stable page chosen by exists_isStableFrom; only its existence is asserted, because a page chosen here is not a page chosen anywhere else.

theorem nonempty_pageInfinityIso_gr' (hK : K.filtration.IsDegreewiseFinite) (p q : ℤ) :
    Nonempty (E.pageInfinity (p, q) ≅
      (FilteredObject.gr p).obj (K.inducedFilteredObject (p + q)))

CochainComplex.Filtered.nonempty_pageInfinityIso_gr, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Convergence.lean, line 832. The attribute's comment: “(3), for the canonical spectral sequence of a filtered complex”. References: SGA 4 Vbis (2.5.2), “partial”.

E_∞^{p,q} ≅ gr^p H^{p+q}(K^•) for the canonical spectral sequence of a filtered complex. nonempty_pageInfinityIso_gr' for CochainComplex.Filtered.spectralSequenceFunctor, whose pages are the subquotients Z_r^{p,q}/(D_r^{p,q} ⊓ Z_r^{p,q}) on the nose.

theorem nonempty_pageInfinityIso_gr (K : Filtered C)
    (hK : K.filtration.IsDegreewiseFinite) (p q : ℤ) :
    Nonempty ((spectralSequenceFunctor.obj K).pageInfinity (p, q) ≅
      (FilteredObject.gr p).obj (K.inducedFilteredObject (p + q)))

CochainComplex.isBounded_and_converges_of_isDegreewiseFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex/Basic/Convergence.lean, line 378. References: EGA 0 (11.2.4), “special case”.

Stacks 012W. Let 𝒜 be an abelian category and let (K^•, F) be a filtered complex of 𝒜 whose filtration is finite in each degree. Let E be the spectral sequence of (K^•, F), so that its page at (r, p, q) is Z_r^{p,q}/D_r^{p,q} for n = p + q, where Z_r^{p,q} = F^p K^n ⊓ (d^n)⁻¹(F^{p+r}K^{n+1}) and D_r^{p,q} = Z_{r-1}^{p+1,q-1} ⊔ d^{n-1}(Z_{r-1}^{p-r+1,q+r-2}), and let F^p H^n(K^•) = Im(H^n(F^pK^•) ⟶ H^n(K^•)) be the induced filtration on cohomology. Then:

  1. E is bounded: for every n only finitely many E_0^{p, n-p} are nonzero;
  2. the induced filtration on each H^n(K^•) is finite;
  3. E converges to H^*(K^•): it is regular, d_r^{p,q} = 0 for r ≫ 0, and it converges weakly, the stable cycles and boundaries Z_∞^{p,q} and B_∞^{p,q} existing and being equal to Ker(d^n) ⊓ F^p K^n ⊔ F^{p+1}K^n and Im(d^{n-1}) ⊓ F^p K^n ⊔ F^{p+1}K^n, i.e. equality holding in (012S) and (012T);
  4. if 𝒞 ⊆ 𝒜 is a weak Serre subcategory with E_r^{p,q} in 𝒞 for all p, q and some r ≥ 0, then every H^n(K^•) is in 𝒞.
public theorem isBounded_and_converges_of_isDegreewiseFinite
    {A : Type u} [Category.{v} A] [Abelian A]
    (K : FilteredObject (CochainComplex A ℤ) ℤᵒᵖ)
    (hK : K.filtration.IsDegreewiseFinite)
    (F : ∀ (_p n : ℤ), Subobject (K.X.X n))
    (hF : ∀ p n : ℤ, F p n = Subobject.mk ((K.filtration.ι.app (op p)).f n))
    (Z : ∀ (_r _p n : ℤ), Subobject (K.X.X n))
    (hZ : ∀ r p n : ℤ, Z r p n =
      F p n ⊓ (Subobject.pullback (K.X.d n (n + 1))).obj (F (p + r) (n + 1)))
    (D : ∀ (_r _p n : ℤ), Subobject (K.X.X n))
    (hD : ∀ 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))
    (hFH : ∀ n p : ℤ, FH n p =
      imageSubobject (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n))
    (E : CohomologicalSpectralSequence A 0)
    (hE : ∀ (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))) :
    (∀ 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 : ℕ =>
          F p n ⊓ (Subobject.pullback (K.X.d n (n + 1))).obj (F (p + r) (n + 1)) ⊔ F (p + 1) n)
        (kernelSubobject (K.X.d n (n + 1)) ⊓ F p n ⊔ F (p + 1) n) ∧
      IsLUB (Set.range fun r : ℕ =>
          F p n ⊓ (Subobject.«exists» (K.X.d (n - 1) n)).obj (F (p - r) (n - 1)) ⊔ F (p + 1) n)
        (imageSubobject (K.X.d (n - 1) n) ⊓ F p n ⊔ F (p + 1) n)) ∧
    (∀ (P : ObjectProperty A) [P.IsWeakSerreClass] (r : ℤ) (hr : 0 ≤ r),
      (∀ p q : ℤ, P ((E.page r hr).X (p, q))) → ∀ n : ℤ, P (K.X.homology n))
Tag 0BDW, a lemma

Tag 0BDW in the Stacks Project.

CochainComplex.Filtered.finite_homology_and_sum_negOnePow_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex.lean, line 1212.

Stacks 0BDW. Let (K^•, F) be a filtered complex of C whose filtration is finite in each degree, and let E be its spectral sequence, presented by the identification of its pages with Z_s^{p, q}/(D_s^{p, q} ∩ Z_s^{p, q}) of [Stacks, Tag 012M]. If some page E_r has only finitely many nonzero terms, then only finitely many H^n(K^•) are nonzero, and for every weak Serre subcategory P of C containing the terms of E_r (for instance the smallest one) the H^n(K^•) lie in P and ∑ (-1)^n [H^n(K^•)] = ∑ (-1)^{p + q} [E_r^{p, q}] in K₀(P).

theorem finite_homology_and_sum_negOnePow_eq (hK : K.filtration.IsDegreewiseFinite)
    (E : CohomologicalSpectralSequence C 0)
    (e : ∀ (r p q n : ℤ) (hr : 0 ≤ r) (_ : n = p + q), (E.page r hr).X (p, q) ≅
      cokernel (Subobject.ofLE _ _ (inf_le_right : boundaries K.X K.step r p n ⊓
        cycles K.X K.step r p n ≤ cycles K.X K.step r p n)))
    (r : ℤ) (hr : 0 ≤ r) (hfin : {pq : ℤ × ℤ | ¬ IsZero ((E.page r hr).X pq)}.Finite)
    (P : ObjectProperty C) [P.IsWeakSerreClass] (hP : ∀ pq : ℤ × ℤ, P ((E.page r hr).X pq)) :
    {n : ℤ | ¬ IsZero (K.X.homology n)}.Finite ∧
    ∃ hH : ∀ n : ℤ, P (K.X.homology n),
      ∑ᶠ n : ℤ, (n.negOnePow : ℤ) • KZero.mk P.FullSubcategory ⟨K.X.homology n, hH n⟩ =
        ∑ᶠ pq : ℤ × ℤ, ((pq.1 + pq.2).negOnePow : ℤ) •
          KZero.mk P.FullSubcategory ⟨(E.page r hr).X pq, hP pq⟩
Tag 0BK5, a lemma

Tag 0BK5 in the Stacks Project.

CochainComplex.isBounded_and_converges_of_eventually_isZero_of_eventually_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/FilteredComplex/Basic/Convergence.lean, line 677. References: EGA 0 (13.6.4), “partial”.

Stacks 0BK5. Let 𝒜 be an abelian category and let (K^•, F) be a filtered complex of 𝒜 such that, for every n, H^n(F^pK^•) = 0 for p ≫ 0 and H^n(F^pK^•) ⟶ H^n(K^•) is an isomorphism for p ≪ 0. Let E be the spectral sequence of (K^•, F), presented as in isBounded_and_converges_of_isDegreewiseFinite by its pages Z_r^{p,q}/D_r^{p,q}, and let F^p H^n(K^•) = Im(H^n(F^pK^•) ⟶ H^n(K^•)). Then:

  1. E is bounded: for every n only finitely many E_1^{p, n-p} are nonzero;
  2. the induced filtration on each H^n(K^•) is finite;
  3. E converges to H^*(K^•): it is regular, the stable cycles and boundaries exist and equality holds in (012S) and (012T), and the resulting canonical comparison E_∞^{p, n-p} ≅ gr^p H^n(K^•) of [Stacks, Tag 012V] is an isomorphism.

Boundedness is stated on the first page, where the source's proof establishes it: under these hypotheses E_0^{p, q} = gr^p K^{p+q} need not vanish for |p| ≫ 0 (take any acyclic complex with a nowhere-stationary filtration by acyclic subcomplexes), so the source's spectral sequence is bounded as a spectral sequence starting at r = 1.

public theorem isBounded_and_converges_of_eventually_isZero_of_eventually_isIso
    {A : Type u} [Category.{v} A] [Abelian A]
    (K : FilteredObject (CochainComplex A ℤ) ℤᵒᵖ)
    (F : ∀ (_p n : ℤ), Subobject (K.X.X n))
    (hF : ∀ p n : ℤ, F p n = Subobject.mk ((K.filtration.ι.app (op p)).f n))
    (Z : ∀ (_r _p n : ℤ), Subobject (K.X.X n))
    (hZ : ∀ r p n : ℤ, Z r p n =
      F p n ⊓ (Subobject.pullback (K.X.d n (n + 1))).obj (F (p + r) (n + 1)))
    (D : ∀ (_r _p n : ℤ), Subobject (K.X.X n))
    (hD : ∀ 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))
    (hFH : ∀ n p : ℤ, FH n p =
      imageSubobject (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n))
    (E : CohomologicalSpectralSequence A 0)
    (hE : ∀ (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)))
    (hzero : ∀ n : ℤ, ∃ p₀ : ℤ, ∀ p : ℤ, p₀ ≤ p →
      IsZero ((K.filtration.obj (op p)).homology n))
    (hiso : ∀ n : ℤ, ∃ p₁ : ℤ, ∀ p : ℤ, p ≤ p₁ →
      IsIso (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n)) :
    (∀ n : ℤ, {p : ℤ | ¬ IsZero ((E.page 1 (by omega)).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 : ℕ =>
          F p n ⊓ (Subobject.pullback (K.X.d n (n + 1))).obj (F (p + r) (n + 1)) ⊔
            F (p + 1) n)
        (kernelSubobject (K.X.d n (n + 1)) ⊓ F p n ⊔ F (p + 1) n) ∧
      IsLUB (Set.range fun r : ℕ =>
          F p n ⊓ (Subobject.«exists» (K.X.d (n - 1) n)).obj (F (p - r) (n - 1)) ⊔
            F (p + 1) n)
        (imageSubobject (K.X.d (n - 1) n) ⊓ F p n ⊔ F (p + 1) n)) ∧
    (∀ p n : ℤ,
      let C := (Subobject.pullback (K.X.iCycles n)).obj (F p n)
      let N := kernelSubobject (K.X.d n (n + 1)) ⊓ F p n ⊔ F (p + 1) n
      let B := imageSubobject (K.X.d (n - 1) n) ⊓ F p n ⊔ F (p + 1) n
      ∃ (a : (C : A) ⟶ (N : A))
        (b : (C : A) ⟶ image (HomologicalComplex.homologyMap
          (K.filtration.ι.app (op p)) n))
        (e : cokernel (Subobject.ofLE (B ⊓ N) N inf_le_right) ≅
          cokernel (image.preComp
            (HomologicalComplex.homologyMap (K.filtration.diagram.map
              (homOfLE (Int.le_add_one le_rfl) : (p : ℤ) ⟶ p + 1).op) n)
            (HomologicalComplex.homologyMap (K.filtration.ι.app (op p)) n))),
        C.arrow ≫ K.X.iCycles n = a ≫ N.arrow ∧
        C.arrow ≫ K.X.homologyπ n =
          b ≫ image.ι (HomologicalComplex.homologyMap
            (K.filtration.ι.app (op p)) n) ∧
        a ≫ cokernel.π (Subobject.ofLE (B ⊓ N) N inf_le_right) ≫ e.hom =
          b ≫ cokernel.π (image.preComp
            (HomologicalComplex.homologyMap (K.filtration.diagram.map
              (homOfLE (Int.le_add_one le_rfl) : (p : ℤ) ⟶ p + 1).op) n)
            (HomologicalComplex.homologyMap
              (K.filtration.ι.app (op p)) n)))
Sources
LeanCochainComplex.Filtered · CochainComplex.ImageSystem.filtered · CochainComplex.exists_cohomologicalSpectralSequence · CochainComplex.Filtered.exists_iso_firstPage_homology_d_eq_δ · CochainComplex.Filtered.d_gr_eq_zero_and_exists_iso_firstPage_d_eq · FilteredComplexSpectralSequence.spectralSequenceMap · CochainComplex.Filtered.inducedFilteredObject · CochainComplex.Filtered.inducedFiltration

Section12.25 Spectral sequences: double complexes#

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

Tag 0130, a lemma

Tag 0130 in the Stacks Project.

HomologicalComplex₂.exists_iso_pages_totalFiltration₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/DoubleComplex/Convergence.lean, line 47. The attribute's comment: “(2), (4) and (6)”.

Stacks 0130, the second filtration. Let (''E_r, ''d_r) be the spectral sequence of the total complex of a double complex K^{•,•} filtered by the second coordinate, presented as in [Stacks, Tag 012M] by its pages Z_r^{p,q}/D_r^{p,q} and its differentials induced by d. Then 2. ''E_0^{p,q} = K^{q,p} with ''d_0^{p,q} = d_1^{q,p}; 4. ''E_1^{p,q} = H^q(K^{•,p}) with ''d_1^{p,q} = (-1)^q H^q(d_2^{•,p}); here H^q(K^{•,p}) is written as the p-th term of H^q_I(K^{•,•}), whose differential is induced by d_2; 6. ''E_2^{p,q} = H^p_{II}(H^q_I(K^{•,•})).

That the filtration F this is stated for really is F_{II}^p Tot^n = ⨁_{i + j = n, j ≥ p} K^{i,j} is the companion statement isLeast_totalFiltration₂, which shares the parameters F and hF with this one; the two together are the content of [Stacks, Tag 0130] for the second filtration.

public theorem exists_iso_pages_totalFiltration₂
    (F : ∀ (_p n : ℤ), Subobject ((K.total (ComplexShape.up ℤ)).X n))
    (hF : ∀ p n : ℤ, F p n = Subobject.mk ((K.totalFiltration₂.filtration.ι.app (op p)).f n))
    (Z : ∀ (_r _p n : ℤ), Subobject ((K.total (ComplexShape.up ℤ)).X n))
    (hZ : ∀ r p n : ℤ, Z r p n = F p n ⊓
      (Subobject.pullback ((K.total (ComplexShape.up ℤ)).d n (n + 1))).obj (F (p + r) (n + 1)))
    (D : ∀ (_r _p n : ℤ), Subobject ((K.total (ComplexShape.up ℤ)).X n))
    (hD : ∀ r p n : ℤ, D r p n = Z (r - 1) (p + 1) n ⊔
      (Subobject.«exists» ((K.total (ComplexShape.up ℤ)).d (n - 1) n)).obj
        (Z (r - 1) (p - r + 1) (n - 1)))
    (E : CohomologicalSpectralSequence C 0)
    (e : ∀ (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)))
    (hδ : ∀ (r p q n : ℤ) (hr : 0 ≤ r) (hn : n = p + q),
      ∃ δ : (Z r p n : C) ⟶ (Z r (p + r) (n + 1) : C),
        δ ≫ (Z r (p + r) (n + 1)).arrow =
          (Z r p n).arrow ≫ (K.total (ComplexShape.up ℤ)).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 ≫ (E.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 : ℤ, (E.page 0 le_rfl).X (p, q) ≅ (K.X q).X p,
      ∀ p q : ℤ, (E.page 0 le_rfl).d (p, q) (p, q + 1) ≫ (α p (q + 1)).hom =
        (α p q).hom ≫ (K.d q (q + 1)).f p) ∧
    (∃ β : ∀ p q : ℤ, (E.page 1 zero_le_one).X (p, q) ≅ (K.homology q).X p,
      ∀ p q : ℤ, (E.page 1 zero_le_one).d (p, q) (p + 1, q) ≫ (β (p + 1) q).hom =
        (β p q).hom ≫ (q.negOnePow • (K.homology q).d p (p + 1))) ∧
    ∀ p q : ℤ, Nonempty ((E.page 2 zero_le_two).X (p, q) ≅ (K.homology q).homology p)

HomologicalComplex₂.isLeast_totalFiltration₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/DoubleComplex/Filtration.lean, line 288. The attribute's comment: “the first filtration is ⨁_{i ≥ p} K^{i,j}”.

Stacks 0130, the first filtration is the one intended. The degreewise steps F p n of the filtration of Tot(K^{•,•}) by the first coordinate are F\_I^p Tot^n = ⨁\_\{i + j = n, i ≥ p} K^\{i,j}, characterized without arbitrary suprema of subobjects: F p n contains the image of every summand inclusion K^{i,j} ⟶ Tot^n with i ≥ p, and it is the least subobject of Tot^n that does. Consequently the filtration is decreasing in p. Together with exists_iso_pages_totalFiltration₁, which is stated for the same F under the same hypothesis hF, this is the content of [Stacks, Tag 0130] for the first filtration: the identifications of the pages there are identifications for this filtration.

public theorem isLeast_totalFiltration₁
    (F : ∀ (_p n : ℤ), Subobject ((K.total (ComplexShape.up ℤ)).X n))
    (hF : ∀ p n : ℤ, F p n = Subobject.mk ((K.totalFiltration₁.filtration.ι.app (op p)).f n)) :
    (∀ (p i j n : ℤ) (hij : i + j = n), p ≤ i →
      imageSubobject (K.ιTotal (ComplexShape.up ℤ) i j n hij) ≤ F p n) ∧
    (∀ (p n : ℤ) (W : Subobject ((K.total (ComplexShape.up ℤ)).X n)),
      (∀ (i j : ℤ) (hij : i + j = n), p ≤ i →
        imageSubobject (K.ιTotal (ComplexShape.up ℤ) i j n hij) ≤ W) → F p n ≤ W) ∧
    (∀ p p' n : ℤ, p ≤ p' → F p' n ≤ F p n)

HomologicalComplex₂.isLeast_totalFiltration₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/DoubleComplex/Filtration.lean, line 308. The attribute's comment: “the second filtration is ⨁_{j ≥ p} K^{i,j}”.

Stacks 0130, the second filtration is the one intended. The degreewise steps F p n of the filtration of Tot(K^{•,•}) by the second coordinate are F\_\{II}^p Tot^n = ⨁\_\{i + j = n, j ≥ p} K^\{i,j}, characterized without arbitrary suprema of subobjects: F p n contains the image of every summand inclusion K^{i,j} ⟶ Tot^n with j ≥ p, and it is the least subobject of Tot^n that does. Consequently the filtration is decreasing in p. Together with exists_iso_pages_totalFiltration₂, which is stated for the same F under the same hypothesis hF, this is the content of [Stacks, Tag 0130] for the second filtration: the identifications of the pages there are identifications for this filtration.

public theorem isLeast_totalFiltration₂
    (F : ∀ (_p n : ℤ), Subobject ((K.total (ComplexShape.up ℤ)).X n))
    (hF : ∀ p n : ℤ, F p n = Subobject.mk ((K.totalFiltration₂.filtration.ι.app (op p)).f n)) :
    (∀ (p i j n : ℤ) (hij : i + j = n), p ≤ j →
      imageSubobject (K.ιTotal (ComplexShape.up ℤ) i j n hij) ≤ F p n) ∧
    (∀ (p n : ℤ) (W : Subobject ((K.total (ComplexShape.up ℤ)).X n)),
      (∀ (i j : ℤ) (hij : i + j = n), p ≤ j →
        imageSubobject (K.ιTotal (ComplexShape.up ℤ) i j n hij) ≤ W) → F p n ≤ W) ∧
    (∀ p p' n : ℤ, p ≤ p' → F p' n ≤ F p n)

HomologicalComplex₂.exists_iso_pages_totalFiltration₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/DoubleComplex/Pages.lean, line 497. The attribute's comment: “(1), (3) and (5)”.

Stacks 0130, the first filtration. Let ('E_r, 'd_r) be the spectral sequence of the total complex of a double complex K^{•,•} filtered by the first coordinate, presented as in [Stacks, Tag 012M] by its pages Z_r^{p,q}/D_r^{p,q} and its differentials induced by d. Then 1. 'E_0^{p,q} = K^{p,q} with 'd_0^{p,q} = (-1)^p d_2^{p,q}; 3. 'E_1^{p,q} = H^q(K^{p,•}) with 'd_1^{p,q} = H^q(d_1^{p,•}); 5. 'E_2^{p,q} = H^p_I(H^q_{II}(K^{•,•})), the cohomology in degree p of the complex p ↦ H^q(K^{p,•}).

That the filtration F this is stated for really is F_I^p Tot^n = ⨁_{i + j = n, i ≥ p} K^{i,j} is the companion statement isLeast_totalFiltration₁, which shares the parameters F and hF with this one; the two together are the content of [Stacks, Tag 0130] for the first filtration.

public theorem exists_iso_pages_totalFiltration₁
    (F : ∀ (_p n : ℤ), Subobject ((K.total (ComplexShape.up ℤ)).X n))
    (hF : ∀ p n : ℤ, F p n = Subobject.mk ((K.totalFiltration₁.filtration.ι.app (op p)).f n))
    (Z : ∀ (_r _p n : ℤ), Subobject ((K.total (ComplexShape.up ℤ)).X n))
    (hZ : ∀ r p n : ℤ, Z r p n = F p n ⊓
      (Subobject.pullback ((K.total (ComplexShape.up ℤ)).d n (n + 1))).obj (F (p + r) (n + 1)))
    (D : ∀ (_r _p n : ℤ), Subobject ((K.total (ComplexShape.up ℤ)).X n))
    (hD : ∀ r p n : ℤ, D r p n = Z (r - 1) (p + 1) n ⊔
      (Subobject.«exists» ((K.total (ComplexShape.up ℤ)).d (n - 1) n)).obj
        (Z (r - 1) (p - r + 1) (n - 1)))
    (E : CohomologicalSpectralSequence C 0)
    (e : ∀ (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)))
    (hδ : ∀ (r p q n : ℤ) (hr : 0 ≤ r) (hn : n = p + q),
      ∃ δ : (Z r p n : C) ⟶ (Z r (p + r) (n + 1) : C),
        δ ≫ (Z r (p + r) (n + 1)).arrow =
          (Z r p n).arrow ≫ (K.total (ComplexShape.up ℤ)).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 ≫ (E.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 : ℤ, (E.page 0 le_rfl).X (p, q) ≅ (K.X p).X q,
      ∀ p q : ℤ, (E.page 0 le_rfl).d (p, q) (p, q + 1) ≫ (α p (q + 1)).hom =
        (α p q).hom ≫ (p.negOnePow • (K.X p).d q (q + 1))) ∧
    (∃ β : ∀ p q : ℤ, (E.page 1 zero_le_one).X (p, q) ≅ (K.X p).homology q,
      ∀ p q : ℤ, (E.page 1 zero_le_one).d (p, q) (p + 1, q) ≫ (β (p + 1) q).hom =
        (β p q).hom ≫ HomologicalComplex.homologyMap (K.d p (p + 1)) q) ∧
    ∀ p q : ℤ, Nonempty ((E.page 2 zero_le_two).X (p, q) ≅
      (((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) q).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj K).homology p)
Tag 0131, a definition

Tag 0131 in the Stacks Project.

HomologicalComplex₂.WeaklyConvergesToTotalHomology₁, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Defs/FilteredComplex.lean, line 345. The attribute's comment: “('E_r, 'd_r) weakly converges”.

Stacks 0131, the first spectral sequence, weak convergence. The spectral sequence ('E_r, 'd_r) of Tot(K^{•,•}) filtered by the first coordinate weakly converges to H^n(Tot(K^{•,•})).

abbrev WeaklyConvergesToTotalHomology₁ : Prop

HomologicalComplex₂.AbutsToTotalHomology₁, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Defs/FilteredComplex.lean, line 352. The attribute's comment: “('E_r, 'd_r) abuts”.

Stacks 0131, the first spectral sequence, abutment. The spectral sequence ('E_r, 'd_r) of Tot(K^{•,•}) filtered by the first coordinate abuts to H^n(Tot(K^{•,•})).

abbrev AbutsToTotalHomology₁ : Prop

HomologicalComplex₂.ConvergesToTotalHomology₁, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Defs/FilteredComplex.lean, line 359. The attribute's comment: “('E_r, 'd_r) converges”.

Stacks 0131, the first spectral sequence, convergence. The spectral sequence ('E_r, 'd_r) of Tot(K^{•,•}) filtered by the first coordinate converges to H^n(Tot(K^{•,•})).

abbrev ConvergesToTotalHomology₁ : Prop

HomologicalComplex₂.WeaklyConvergesToTotalHomology₂, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Defs/FilteredComplex.lean, line 366. The attribute's comment: “(''E_r, ''d_r) weakly converges”.

Stacks 0131, the second spectral sequence, weak convergence. The spectral sequence (''E_r, ''d_r) of Tot(K^{•,•}) filtered by the second coordinate weakly converges to H^n(Tot(K^{•,•})).

abbrev WeaklyConvergesToTotalHomology₂ : Prop

HomologicalComplex₂.AbutsToTotalHomology₂, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Defs/FilteredComplex.lean, line 373. The attribute's comment: “(''E_r, ''d_r) abuts”.

Stacks 0131, the second spectral sequence, abutment. The spectral sequence (''E_r, ''d_r) of Tot(K^{•,•}) filtered by the second coordinate abuts to H^n(Tot(K^{•,•})).

abbrev AbutsToTotalHomology₂ : Prop

HomologicalComplex₂.ConvergesToTotalHomology₂, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Defs/FilteredComplex.lean, line 380. The attribute's comment: “(''E_r, ''d_r) converges”.

Stacks 0131, the second spectral sequence, convergence. The spectral sequence (''E_r, ''d_r) of Tot(K^{•,•}) filtered by the second coordinate converges to H^n(Tot(K^{•,•})).

abbrev ConvergesToTotalHomology₂ : Prop
Tag 0132, a lemma

Tag 0132 in the Stacks Project.

CategoryTheory.SpectralSequence.AbutsTo.prop_of_prop_page_firstQuadrant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/AbutsToWeakSerreFirstQuadrant.lean, line 66. The attribute's comment: “part (4), for a first-quadrant CohomologicalSpectralSequence presented by SpectralSequence.AbutsTo, with the page hypothesis split into vanishing outside the first quadrant and membership at the nonnegative bidegrees”.

Stacks 0132 part (4) for a first quadrant spectral sequence. Let E be a cohomological spectral sequence of an abelian category which abuts to a graded object H, let P be a weak Serre subcategory, and let r be a page of E. If the terms of E_r vanish outside the first quadrant and those at the nonnegative bidegrees lie in P, then every H n lies in P.

This is CategoryTheory.SpectralSequence.AbutsTo.prop_of_prop_page with its hypothesis on the page split into the two clauses a first quadrant spectral sequence provides: P contains the zero object and is closed under isomorphisms, so the vanishing clause gives P at the bidegrees the other clause does not reach.

theorem AbutsTo.prop_of_prop_page_firstQuadrant {r₀ : ℤ}
    {E : CohomologicalSpectralSequence C r₀} {H : ℤ → C} (hE : AbutsTo E H)
    (P : ObjectProperty C) [P.IsWeakSerreClass] {r : ℤ} (hr : r₀ ≤ r)
    (hzero : ∀ p q : ℤ, p < 0 ∨ q < 0 → IsZero ((E.page r hr).X (p, q)))
    (hP : ∀ p q : ℕ, P ((E.page r hr).X ((p : ℤ), (q : ℤ)))) (n : ℤ) : P (H n)

HomologicalComplex₂.isBounded_and_converges_totalFiltration₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/DoubleComplex/Convergence.lean, line 205.

Stacks 0132, the first filtration. If every diagonal of the double complex K^{•,•} has only finitely many nonzero terms, then the spectral sequence E of Tot(K^{•,•}) filtered by the first coordinate, presented as in CochainComplex.isBounded_and_converges_of_isDegreewiseFinite, is bounded, the filtration it induces on each H^n(Tot(K^{•,•})) is finite, E converges to H^*(Tot(K^{•,•})), and a weak Serre subcategory containing one whole page of E contains every H^n(Tot(K^{•,•})).

public theorem isBounded_and_converges_totalFiltration₁
    (hK : ∀ n : ℤ, {pq : ℤ × ℤ | pq.1 + pq.2 = n ∧ ¬ IsZero ((K.X pq.1).X pq.2)}.Finite)
    (F : ∀ (_p n : ℤ), Subobject (K.totalFiltration₁.X.X n))
    (hF : ∀ p n : ℤ, F p n = Subobject.mk ((K.totalFiltration₁.filtration.ι.app (op p)).f n))
    (Z : ∀ (_r _p n : ℤ), Subobject (K.totalFiltration₁.X.X n))
    (hZ : ∀ r p n : ℤ, Z r p n =
      F p n ⊓ (Subobject.pullback (K.totalFiltration₁.X.d n (n + 1))).obj (F (p + r) (n + 1)))
    (D : ∀ (_r _p n : ℤ), Subobject (K.totalFiltration₁.X.X n))
    (hD : ∀ r p n : ℤ, D r p n = Z (r - 1) (p + 1) n ⊔
      (Subobject.«exists» (K.totalFiltration₁.X.d (n - 1) n)).obj (Z (r - 1) (p - r + 1) (n - 1)))
    (FH : ∀ (n _p : ℤ), Subobject (K.totalFiltration₁.X.homology n))
    (hFH : ∀ n p : ℤ, FH n p =
      imageSubobject
        (HomologicalComplex.homologyMap (K.totalFiltration₁.filtration.ι.app (op p)) n))
    (E : CohomologicalSpectralSequence C 0)
    (hE : ∀ (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))) :
    (∀ n : ℤ, {p : ℤ | ¬ IsZero ((E.page 0 le_rfl).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 : ℕ =>
          F p n ⊓ (Subobject.pullback (K.totalFiltration₁.X.d n (n + 1))).obj (F (p + r) (n + 1))
            ⊔ F (p + 1) n)
        (kernelSubobject (K.totalFiltration₁.X.d n (n + 1)) ⊓ F p n ⊔ F (p + 1) n) ∧
      IsLUB (Set.range fun r : ℕ =>
          F p n ⊓ (Subobject.«exists» (K.totalFiltration₁.X.d (n - 1) n)).obj (F (p - r) (n - 1))
            ⊔ F (p + 1) n)
        (imageSubobject (K.totalFiltration₁.X.d (n - 1) n) ⊓ F p n ⊔ F (p + 1) n)) ∧
    (∀ (P : ObjectProperty C) [P.IsWeakSerreClass] (r : ℤ) (hr : 0 ≤ r),
      (∀ p q : ℤ, P ((E.page r hr).X (p, q))) → ∀ n : ℤ, P (K.totalFiltration₁.X.homology n))

HomologicalComplex₂.isBounded_and_converges_totalFiltration₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/DoubleComplex/Convergence.lean, line 247.

Stacks 0132, the second filtration. If every diagonal of the double complex K^{•,•} has only finitely many nonzero terms, then the spectral sequence E of Tot(K^{•,•}) filtered by the second coordinate, presented as in CochainComplex.isBounded_and_converges_of_isDegreewiseFinite, is bounded, the filtration it induces on each H^n(Tot(K^{•,•})) is finite, E converges to H^*(Tot(K^{•,•})), and a weak Serre subcategory containing one whole page of E contains every H^n(Tot(K^{•,•})).

public theorem isBounded_and_converges_totalFiltration₂
    (hK : ∀ n : ℤ, {pq : ℤ × ℤ | pq.1 + pq.2 = n ∧ ¬ IsZero ((K.X pq.1).X pq.2)}.Finite)
    (F : ∀ (_p n : ℤ), Subobject (K.totalFiltration₂.X.X n))
    (hF : ∀ p n : ℤ, F p n = Subobject.mk ((K.totalFiltration₂.filtration.ι.app (op p)).f n))
    (Z : ∀ (_r _p n : ℤ), Subobject (K.totalFiltration₂.X.X n))
    (hZ : ∀ r p n : ℤ, Z r p n =
      F p n ⊓ (Subobject.pullback (K.totalFiltration₂.X.d n (n + 1))).obj (F (p + r) (n + 1)))
    (D : ∀ (_r _p n : ℤ), Subobject (K.totalFiltration₂.X.X n))
    (hD : ∀ r p n : ℤ, D r p n = Z (r - 1) (p + 1) n ⊔
      (Subobject.«exists» (K.totalFiltration₂.X.d (n - 1) n)).obj (Z (r - 1) (p - r + 1) (n - 1)))
    (FH : ∀ (n _p : ℤ), Subobject (K.totalFiltration₂.X.homology n))
    (hFH : ∀ n p : ℤ, FH n p =
      imageSubobject
        (HomologicalComplex.homologyMap (K.totalFiltration₂.filtration.ι.app (op p)) n))
    (E : CohomologicalSpectralSequence C 0)
    (hE : ∀ (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))) :
    (∀ n : ℤ, {p : ℤ | ¬ IsZero ((E.page 0 le_rfl).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 : ℕ =>
          F p n ⊓ (Subobject.pullback (K.totalFiltration₂.X.d n (n + 1))).obj (F (p + r) (n + 1))
            ⊔ F (p + 1) n)
        (kernelSubobject (K.totalFiltration₂.X.d n (n + 1)) ⊓ F p n ⊔ F (p + 1) n) ∧
      IsLUB (Set.range fun r : ℕ =>
          F p n ⊓ (Subobject.«exists» (K.totalFiltration₂.X.d (n - 1) n)).obj (F (p - r) (n - 1))
            ⊔ F (p + 1) n)
        (imageSubobject (K.totalFiltration₂.X.d (n - 1) n) ⊓ F p n ⊔ F (p + 1) n)) ∧
    (∀ (P : ObjectProperty C) [P.IsWeakSerreClass] (r : ℤ) (hr : 0 ≤ r),
      (∀ p q : ℤ, P ((E.page r hr).X (p, q))) → ∀ n : ℤ, P (K.totalFiltration₂.X.homology n))
Tag 0133, a lemma

Tag 0133 in the Stacks Project.

quasiIso_total_of_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/TotalComplexQuasiIso.lean, line 1431. The attribute's comment: “p”.

Under the hypotheses, the total complex of DA exists and the induced map K^• → Tot(A^{•,•}) is a quasi-isomorphism (variant in the first variable p).

theorem quasiIso_total_of_resolution
    (K : HomologicalComplex A (ComplexShape.up ℤ))
    (DA : HomologicalComplex₂ A (ComplexShape.up ℤ) (ComplexShape.up ℤ))
    (α : K ⟶ rowZero DA)
    (h : Hypotheses K DA α) :
    ∃ _ : DA.HasTotal (ComplexShape.up ℤ),
      ∃ (f : K ⟶ DA.total (ComplexShape.up ℤ)),
        (∀ n : ℤ, f.f n =
          α.f n ≫ DA.ιTotal (ComplexShape.up ℤ) n 0 n (by simp)) ∧
          QuasiIso f

quasiIso_total_of_resolution_flip, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/TotalComplexQuasiIso.lean, line 1446. The attribute's comment: “q”.

Under the hypotheses for DA.flip, the total complex of DA exists and the induced map K^• → Tot(A^{•,•}) is a quasi-isomorphism (variant in the second variable q).

theorem quasiIso_total_of_resolution_flip
    (K : HomologicalComplex A (ComplexShape.up ℤ))
    (DA : HomologicalComplex₂ A (ComplexShape.up ℤ) (ComplexShape.up ℤ))
    (α : K ⟶ rowZero DA.flip)
    (h : Hypotheses K DA.flip α) :
    ∃ _ : DA.HasTotal (ComplexShape.up ℤ),
      ∃ (f : K ⟶ DA.total (ComplexShape.up ℤ)),
        (∀ n : ℤ, f.f n =
          α.f n ≫ DA.ιTotal (ComplexShape.up ℤ) 0 n n (by simp)) ∧
          QuasiIso f
Tag 0FKH, a lemma

Tag 0FKH in the Stacks Project.

isHomotopyEquiv_total_of_isHomotopyEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/TotalComplexQuasiIso.lean, line 1737.

Let M^• be a complex of an abelian category and A^{•,•} a complex of complexes. If a : M^•[0] ⟶ A^{•,•} is part of a homotopy equivalence in the category of complexes of complexes, then the canonical induced map α : M^• ⟶ Tot(A^{•,•}) is a homotopy equivalence.

theorem isHomotopyEquiv_total_of_isHomotopyEquiv
    {V : Type*} [Category V] [Abelian V]
    (M : HomologicalComplex V (ComplexShape.up ℤ))
    (A : HomologicalComplex₂ V (ComplexShape.up ℤ) (ComplexShape.up ℤ))
    [A.HasTotal (ComplexShape.up ℤ)]
    (a : HomotopyEquiv (singleObjComplex M) A) :
    Nonempty {e : HomotopyEquiv M (A.total (ComplexShape.up ℤ)) //
        e.hom = totalAlpha M A a.hom}
Sources
LeanHomologicalComplex₂.exists_iso_pages_totalFiltration₂ · HomologicalComplex₂.isLeast_totalFiltration₁ · HomologicalComplex₂.isLeast_totalFiltration₂ · HomologicalComplex₂.exists_iso_pages_totalFiltration₁ · HomologicalComplex₂.WeaklyConvergesToTotalHomology₁ · HomologicalComplex₂.AbutsToTotalHomology₁ · HomologicalComplex₂.ConvergesToTotalHomology₁ · HomologicalComplex₂.WeaklyConvergesToTotalHomology₂

Section12.26 Double complexes of abelian groups#

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

Tag 0E1Q, a lemma

Tag 0E1Q in the Stacks Project.

quasiIso_of_isRightResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Grp/TotalComplex.lean, line 550.

Let M^• be a cochain complex of abelian groups and let 0 → M^• → A_0^• → A_1^• → … be an exact complex of complexes of abelian groups (encoded as a half-plane double complex with augmentation f). Then the induced map g : M^• → Tot(A^{•,•}) is a quasi-isomorphism.

theorem quasiIso_of_isRightResolution
    (M : CochainComplex AddCommGrpCat ℤ)
    (A : HomologicalComplex₂ AddCommGrpCat 𝕀 𝕀) [A.HasTotal 𝕀]
    (f : M ⟶ A.X 0)
    (hA_vanish : ∀ p : ℤ, p < 0 → IsZero (A.X p))
    (hExact : IsRightResolution M A f)
    (g : M ⟶ A.total 𝕀) (hg : InducedFromColumnZero f g) :
    QuasiIso g
Tag 09IZ, a lemma

Tag 09IZ in the Stacks Project.

quasiIso_of_goodResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Grp/TotalComplex.lean, line 940.

A good resolution A → M yields a chain map A.total shZ ⟶ M whose per-degree components agree with canonicalMapF, and this chain map is a quasi-isomorphism.

theorem quasiIso_of_goodResolution
    (M : HomologicalComplex Ab shZ)
    (A : HomologicalComplex₂ Ab shZ shZ)
    [A.HasTotal shZ]
    (f : A.X 0 ⟶ M)
    (_h : GoodResolution M A f) :
    ∃ φ : A.total shZ ⟶ M,
      (∀ n : ℤ, φ.f n = canonicalMapF M A f n) ∧ QuasiIso φ
Tag 09J0, a lemma

Tag 09J0 in the Stacks Project.

HomologicalComplex₂.quasiIso_toProductTotal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/AbelianGroupComplexResolutions.lean, line 631.

Let 0 → M^• → A_0^• → A_1^• → ⋯ be an exact complex of complexes of abelian groups such that for every p the induced complex 0 → Coker(d_M^p) → Coker(d_{A_0}^p) → ⋯ is exact. Then the map M^• → Tot_π(A^{•, •}) induced by M^• → A_0^• is a quasi-isomorphism. Here K is the double complex A^{p, q} = A_p^q, ε is the map M^• → A_0^•, the exact complex of complexes is the augmentation of K by ε, and Coker(d^p) is the object of opcycles in degree p + 1.

theorem quasiIso_toProductTotal (ε : M ⟶ K.X 0) (w : ε ≫ K.d 0 1 = 0)
    (hA : (CochainComplex.augment K ε w).Acyclic)
    (hC : ∀ q : ℤ, (((HomologicalComplex.opcyclesFunctor AddCommGrpCat.{u} (ComplexShape.up ℤ)
      q).mapHomologicalComplex (ComplexShape.up ℕ)).obj (CochainComplex.augment K ε w)).Acyclic) :
    QuasiIso (toProductTotal ε w)
Tag 0E1R, a lemma

Tag 0E1R in the Stacks Project.

quasiIso_productTotalAug, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Grp/TotalComplex.lean, line 1289.

The natural map from the product total complex of an exact left resolution by complexes to M is a quasi-isomorphism.

alias quasiIso_productTotalAug
Sources
LeanquasiIso_of_isRightResolution · quasiIso_of_goodResolution · HomologicalComplex₂.quasiIso_toProductTotal · quasiIso_productTotalAug

Section12.27 Injectives#

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

Tag 0135, a definition

Tag 0135 in the Stacks Project.

Declarations registered for the tag:

Tag 0136, a lemma

Tag 0136 in the Stacks Project.

injective_iff_everySES_splits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/Basic.lean, line 83. The attribute's comment: “(1)⇔(3)”.

I is injective iff every short exact sequence 0 ⟶ I ⟶ A ⟶ B ⟶ 0 is split.

theorem injective_iff_everySES_splits (I : 𝒜) :
    Injective I ↔ EverySESStartingAtSplits I

subsingleton_ext_one_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/Basic.lean, line 90. The attribute's comment: “(1)⇒(4)”.

If I is injective then Ext¹(B, I) = 0 (encoded as Subsingleton (Ext B I 1)) for every object B.

theorem subsingleton_ext_one_of_injective [HasExt 𝒜]
    (I : 𝒜) (hI : Injective I) (B : 𝒜) :
    Subsingleton (Abelian.Ext B I 1)
Tag 0137, a lemma

Tag 0137 in the Stacks Project.

Declarations registered for the tag:

Tag 0138, a definition

Tag 0138 in the Stacks Project.

Declarations registered for the tag:

Tag 0139, a definition

Tag 0139 in the Stacks Project.

HasFunctorialInjectiveEmbeddings, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/Basic.lean, line 135.

The notion of functorial injective embeddings for an abelian category 𝒜: there exists a functor J : 𝒜 ⥤ Arrow 𝒜 satisfying the three conditions IsFunctorialInjectiveEmbeddings₁, IsFunctorialInjectiveEmbeddings₂, and IsFunctorialInjectiveEmbeddings₃.

def HasFunctorialInjectiveEmbeddings : Prop
Sources
LeanCategoryTheory.Injective · injective_iff_everySES_splits · subsingleton_ext_one_of_injective · CategoryTheory.Injective.instPiObj · CategoryTheory.EnoughInjectives · HasFunctorialInjectiveEmbeddings

Section12.28 Projectives#

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

Tag 013B, a definition

Tag 013B in the Stacks Project.

Declarations registered for the tag:

Tag 013C, a lemma

Tag 013C in the Stacks Project.

homFunctor_shortExact_of_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Projective/Basic.lean, line 98. The attribute's comment: “(1)⇒(2)”.

(1) → (2): if P is projective then Hom(P, -) is exact.

theorem homFunctor_shortExact_of_projective {P : 𝒜} [hP : Projective P]
    (S : ShortComplex 𝒜) (hS : S.ShortExact) :
    ((homFunctor P).mapShortComplex.obj S).ShortExact

projective_iff_every_ses_splits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Projective/Basic.lean, line 156. The attribute's comment: “(1)⇔(3)”. References: SGA 3 VIIB (1.4.3), “more general”; SGA 6 I (1.3.1), “(i) ⇔ (ii), special case”; SGA 6 V (2.2.1), “special case”.

Stacks 013C (narrowed). (1) ↔ (3): P is projective iff every short exact sequence ending in P splits.

The Stacks lemma states the equivalence of four conditions; this records the equivalence between projectivity and the splitting property. The forward implications to the other two conditions are given by homFunctor_shortExact_of_projective and ext_one_eq_zero_of_projective.

theorem projective_iff_every_ses_splits (P : 𝒜) :
    Projective P ↔ EverySESEndingInPSplits P

ext_one_eq_zero_of_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Projective/Basic.lean, line 163. The attribute's comment: “(1)⇒(4)”.

(1) → (4): if P is projective then Ext^1(P, A) = 0 for every A. We use the standard HasExt instance from HasExt.standard 𝒜.

theorem ext_one_eq_zero_of_projective {P : 𝒜} [Projective P] (A : 𝒜) :
    haveI : HasExt.{max u v} 𝒜 := HasExt.standard 𝒜
    ∀ (e : Abelian.Ext.{max u v} P A 1), e = 0
Tag 013D, a lemma

Tag 013D in the Stacks Project.

Declarations registered for the tag:

Tag 013E, a definition

Tag 013E in the Stacks Project.

Declarations registered for the tag:

Tag 013F, a definition

Tag 013F in the Stacks Project.

HasFunctorialProjectiveSurjections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Projective/Basic.lean, line 215.

An abelian category 𝒜 has functorial projective surjections if there exists a functor P : 𝒜 ⥤ Arrow 𝒜 satisfying conditions (1), (2) and (3) above.

def HasFunctorialProjectiveSurjections : Prop
Sources
LeanCategoryTheory.Projective · homFunctor_shortExact_of_projective · projective_iff_every_ses_splits · ext_one_eq_zero_of_projective · CategoryTheory.Projective.instSigmaObj · CategoryTheory.EnoughProjectives · HasFunctorialProjectiveSurjections

Section12.29 Injectives and adjoint functors#

Section 12.29 of the Stacks Project, Tag 015Y. 5 tags here are carried by 5 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 015Z, a lemma

Tag 015Z in the Stacks Project.

preservesInjectiveObjects_of_exact_of_adjunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/Adjunction.lean, line 76. The attribute's comment: “first part”. References: SGA 4 V (0.2), “1) (i) ⇒ (ii)”.

Conjunction of (a) ⇔ (b) and (b) ⇒ (c).

theorem preservesInjectiveObjects_of_exact_of_adjunction
    (u : A ⥤ B) (v : B ⥤ A) [u.Additive] [v.Additive] (adj : v ⊣ u) :
    (v.PreservesMonomorphisms ↔ (PreservesFiniteLimits v ∧ PreservesFiniteColimits v)) ∧
      ((PreservesFiniteLimits v ∧ PreservesFiniteColimits v) → u.PreservesInjectiveObjects)

exact_iff_preservesInjectiveObjects_of_adjunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/Adjunction.lean, line 86. The attribute's comment: “full statement”. References: SGA 4 V (0.2), “1) (i)⇔(ii)”.

Assuming A has enough injectives, the three conditions are equivalent.

theorem exact_iff_preservesInjectiveObjects_of_adjunction
    [EnoughInjectives A]
    (u : A ⥤ B) (v : B ⥤ A) [u.Additive] [v.Additive] (adj : v ⊣ u) :
    (v.PreservesMonomorphisms ↔ (PreservesFiniteLimits v ∧ PreservesFiniteColimits v)) ∧
      ((PreservesFiniteLimits v ∧ PreservesFiniteColimits v) ↔ u.PreservesInjectiveObjects)
Tag 03B8, a remark

Tag 03B8 in the Stacks Project.

ModuleCat.flat_iff_restrictScalars_preservesInjectiveObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/ChangeOfRings.lean, line 32. The attribute's comment: “flatness criterion”.

Stacks Project, Tag 03B8. Every injective S-module remains injective after restriction of scalars along f : R →+* S if and only if f is flat.

The forward implication uses that extension of scalars along a flat map is exact. Conversely, if restriction of scalars preserves injectives, its left adjoint preserves monomorphisms; since extension of scalars already preserves colimits, it is exact, and hence S is flat over R.

theorem ModuleCat.flat_iff_restrictScalars_preservesInjectiveObjects
    {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) :
    f.Flat ↔ (ModuleCat.restrictScalars.{u} f).PreservesInjectiveObjects
Tag 0160, a lemma

Tag 0160 in the Stacks Project.

Declarations registered for the tag:

Tag 0161, a lemma

Tag 0161 in the Stacks Project.

hasFunctorialInjectiveEmbeddings_of_adjunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/Adjunction.lean, line 168.

Let A and B be abelian categories, u : A ⥤ B and v : B ⥤ A additive functors. Assume u is right adjoint to v, v transforms injective maps into injective maps, A has enough injectives, v B = 0 implies B = 0, and A has functorial injective embeddings. Then B has functorial injective embeddings.

theorem hasFunctorialInjectiveEmbeddings_of_adjunction
    (A : Type*) [Category A] [Abelian A]
    (B : Type*) [Category B] [Abelian B]
    (u : A ⥤ B) (v : B ⥤ A)
    [u.Additive] [v.Additive]
    (adj : v ⊣ u)
    (hv_mono : ∀ {X Y : B} (f : X ⟶ Y) [Mono f], Mono (v.map f))
    [EnoughInjectives A]
    (h_reflectZero : ∀ (X : B), IsZero (v.obj X) → IsZero X)
    (hA : HasFunctorialInjectiveEmbeddings A) :
    HasFunctorialInjectiveEmbeddings B
Tag 0793, a lemma

Tag 0793 in the Stacks Project.

isRightAdjoint_of_partialAdjointData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/Adjunction.lean, line 293.

Let 𝒜 and 𝓑 be abelian categories, u : 𝒜 ⥤ 𝓑 a functor, and suppose there is S ⊆ Ob(𝓑) such that every object of 𝓑 is a quotient of some object of S and, for every P ∈ S, the functor A ↦ Hom_𝓑(P, u A) is corepresentable. Then u admits a left adjoint.

theorem isRightAdjoint_of_partialAdjointData
    {A B : Type*} [Category A] [Category B] [Abelian A] [Abelian B]
    (u : A ⥤ B) (S : Set B)
    (h1 : QuotientOfFamily S)
    (h2 : PartialAdjointData u S) :
    u.IsRightAdjoint
Sources
LeanpreservesInjectiveObjects_of_exact_of_adjunction · exact_iff_preservesInjectiveObjects_of_adjunction · ModuleCat.flat_iff_restrictScalars_preservesInjectiveObjects · CategoryTheory.EnoughInjectives.of_adjunction · hasFunctorialInjectiveEmbeddings_of_adjunction · isRightAdjoint_of_partialAdjointData

Section12.30 Essentially constant systems#

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

Tag 0A2E, a lemma

Tag 0A2E in the Stacks Project.

CategoryTheory.EssentiallyConstantInd.isEssentiallyConstantInd_iff_exists_biproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/EssentiallyConstant/Karoubian.lean, line 204. The attribute's comment: “(1)”.

Stacks 0A2E (1). Let M : I ⥤ A be a diagram over a filtered category in a preadditive Karoubian category. Then M is essentially constant if and only if colim M exists and there are a filtered category I' with a fully faithful cofinal functor H : I' ⥤ I (a cofinal filtered full subcategory) and, for each i' : I', a direct sum decomposition M (H i') ≅ X_{i'} ⊕ Z_{i'} such that X_{i'} maps isomorphically to colim M and Z_{i'} maps to zero in M (H i'') for some i' ⟶ i'' in I'.

theorem isEssentiallyConstantInd_iff_exists_biproduct [IsFiltered I] [IsIdempotentComplete A]
    (M : I ⥤ A) :
    IsEssentiallyConstantInd M ↔
      ∃ (_ : HasColimit M) (I' : Type u') (_ : Category.{v'} I') (_ : IsFiltered I')
        (H : I' ⥤ I) (_ : H.Full) (_ : H.Faithful) (_ : H.Final), ∀ i' : I',
          ∃ (X' Z' : A) (b : BinaryBicone X' Z') (_ : b.IsBilimit) (e : b.pt ≅ M.obj (H.obj i')),
            IsIso (b.inl ≫ e.hom ≫ colimit.ι M (H.obj i')) ∧
            ∃ (i'' : I') (f : i' ⟶ i''), b.inr ≫ e.hom ≫ M.map (H.map f) = 0

CategoryTheory.EssentiallyConstantPro.isEssentiallyConstantPro_iff_exists_biproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/EssentiallyConstant/Karoubian.lean, line 334. The attribute's comment: “(2)”.

Stacks 0A2E (2). Let M : I ⥤ A be a diagram over a cofiltered category in a preadditive Karoubian category. Then M is essentially constant if and only if lim M exists and there are a cofiltered category I' with a fully faithful initial functor H : I' ⥤ I (an initial cofiltered full subcategory) and, for each i' : I', a direct sum decomposition M (H i') ≅ X_{i'} ⊕ Z_{i'} such that lim M maps isomorphically to X_{i'} and M (H i'') ⟶ Z_{i'} is zero for some i'' ⟶ i' in I'.

theorem isEssentiallyConstantPro_iff_exists_biproduct [IsCofiltered I] [IsIdempotentComplete A]
    (M : I ⥤ A) :
    IsEssentiallyConstantPro M ↔
      ∃ (_ : HasLimit M) (I' : Type u') (_ : Category.{v'} I') (_ : IsCofiltered I')
        (H : I' ⥤ I) (_ : H.Full) (_ : H.Faithful) (_ : H.Initial), ∀ i' : I',
          ∃ (X' Z' : A) (b : BinaryBicone X' Z') (_ : b.IsBilimit) (e : b.pt ≅ M.obj (H.obj i')),
            IsIso (limit.π M (H.obj i') ≫ e.inv ≫ b.fst) ∧
            ∃ (i'' : I') (f : i'' ⟶ i'), M.map (H.map f) ≫ e.inv ≫ b.snd = 0
Tag 0A2F, a lemma

Tag 0A2F in the Stacks Project.

hasColimit_biprod_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/EssentiallyConstant/Biproducts.lean, line 186. The attribute's comment: “iff”.

In a Karoubian additive category, the pointwise biproduct functor F ⊞ G has a colimit iff both F and G do.

theorem hasColimit_biprod_iff
    {I C : Type*} [Category I] [Category C]
    [Preadditive C] [HasBinaryBiproducts C] [IsIdempotentComplete C]
    (F G : I ⥤ C) :
    HasColimit (F ⊞ G) ↔ HasColimit F ∧ HasColimit G

colimitBiprodIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/EssentiallyConstant/Biproducts.lean, line 213. The attribute's comment: “iso”.

In a Karoubian additive category, if both F and G have colimits, then the colimit of the pointwise biproduct is canonically isomorphic to the biproduct of the colimits.

noncomputable def colimitBiprodIso
    {I C : Type*} [Category I] [Category C]
    [Preadditive C] [HasBinaryBiproducts C] [IsIdempotentComplete C]
    (F G : I ⥤ C) [HasColimit F] [HasColimit G] :
    haveI := hasColimit_biprod_of_hasColimit F G
    colimit (F ⊞ G) ≅ colimit F ⊞ colimit G

colimitBiprodIso_of_hasColimit_biprod, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/EssentiallyConstant/Biproducts.lean, line 226. The attribute's comment: “iso_from_biprod”.

In a Karoubian additive category, if F ⊞ G has a colimit, then it is canonically isomorphic to the biproduct of the colimits of F and G.

noncomputable def colimitBiprodIso_of_hasColimit_biprod
    {I C : Type*} [Category I] [Category C]
    [Preadditive C] [HasBinaryBiproducts C] [IsIdempotentComplete C]
    (F G : I ⥤ C) [HasColimit (F ⊞ G)] :
    haveI := hasColimit_of_hasColimit_biprod_left F G
    haveI := hasColimit_of_hasColimit_biprod_right F G
    colimit (F ⊞ G) ≅ colimit F ⊞ colimit G
Tag 0A2G, a lemma

Tag 0A2G in the Stacks Project.

isEssentiallyConstantInd_biprod_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/EssentiallyConstant/Biproducts.lean, line 385.

Let I be a filtered category and C an additive Karoubian category. For two functors F, G : I ⥤ C, the direct sum F ⊞ G is essentially constant iff both F and G are essentially constant.

theorem isEssentiallyConstantInd_biprod_iff
    {I : Type u} [Category.{v} I] [IsFiltered I]
    {C : Type u'} [Category.{v'} C] [Preadditive C]
    [HasFiniteBiproducts C] [IsIdempotentComplete C]
    (F G : I ⥤ C) :
    haveI : HasBinaryBiproducts C := hasBinaryBiproducts_of_finite_biproducts C
    IsEssentiallyConstantInd (F ⊞ G) ↔
      IsEssentiallyConstantInd F ∧ IsEssentiallyConstantInd G
Sources
LeanCategoryTheory.EssentiallyConstantInd.isEssentiallyConstantInd_iff_exists_biproduct · CategoryTheory.EssentiallyConstantPro.isEssentiallyConstantPro_iff_exists_biproduct · hasColimit_biprod_iff · colimitBiprodIso · colimitBiprodIso_of_hasColimit_biprod · isEssentiallyConstantInd_biprod_iff

Section12.31 Inverse systems#

Section 12.31 of the Stacks Project, Tag 02MY. 8 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02MZ, a lemma

Tag 02MZ in the Stacks Project.

inverseSystem_preadditive, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/InverseSystem.lean, line 46. The attribute's comment: “(1) preadditive”.

Stacks 02MZ (1), preadditive. If C is preadditive, then so is the category of inverse systems in C.

noncomputable def inverseSystem_preadditive
    (C : Type*) [Category C] [Preadditive C] : Preadditive (InverseSystemCategoricalFunctorial C)

inverseSystem_hasFiniteBiproducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/InverseSystem.lean, line 53. The attribute's comment: “(1) biproducts”.

Stacks 02MZ (1), biproducts. If C is preadditive with finite biproducts, then the category of inverse systems in C has finite biproducts.

theorem inverseSystem_hasFiniteBiproducts
    (C : Type*) [Category C] [Preadditive C] [HasFiniteBiproducts C] :
    HasFiniteBiproducts (InverseSystemCategoricalFunctorial C)

inverseSystem_abelian, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/InverseSystem.lean, line 61. The attribute's comment: “(2) abelian”.

Stacks 02MZ (2), abelian. If C is an abelian category, then the category of inverse systems in C is abelian.

noncomputable def inverseSystem_abelian
    (C : Type*) [Category C] [Abelian C] : Abelian (InverseSystemCategoricalFunctorial C)

inverseSystem_shortComplex_exact_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/InverseSystem.lean, line 69. The attribute's comment: “(2) exactness”. References: SGA 3 I (5.2), “partial”.

Stacks 02MZ (2), exactness. A short complex (Kᵢ) → (Lᵢ) → (Mᵢ) of inverse systems over an abelian category is exact if and only if its evaluation at every index i (i.e. Kᵢ → Lᵢ → Mᵢ) is exact.

theorem inverseSystem_shortComplex_exact_iff
    (C : Type*) [Category C] [Abelian C] (S : ShortComplex (InverseSystemCategoricalFunctorial C)) :
    S.Exact ↔ ∀ (i : ℕᵒᵖ), (S.map ((evaluation ℕᵒᵖ C).obj i)).Exact
Tag 02N0, a definition

Tag 02N0 in the Stacks Project.

IsMittagLefflerCategorical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/InverseSystem.lean, line 107. References: EGA 0 (13.1.2), “ℕ-indexed systems”; EGA III (4.1.7); SGA 4½ Rapport (4.11).

Stacks Tag 02N0. The inverse system F : ℕᵒᵖ ⥤ C over an abelian category satisfies the Mittag-Leffler condition if for every i there exists c = c(i) ≥ i such that Im(A_k → A_i) = Im(A_c → A_i) for all k ≥ c.

def IsMittagLefflerCategorical (F : ℕᵒᵖ ⥤ C) : Prop
Tag 02N1, a lemma

Tag 02N1 in the Stacks Project.

Ab.mono_lim_map_and_exact_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ShortComplex/InverseLimit.lean, line 379. The attribute's comment: “left_exact”.

Part (1): for any short exact sequence of inverse systems, the limit sequence 0 → lim A → lim B → lim C is exact.

theorem Ab.mono_lim_map_and_exact_of_shortExact
    (S : ShortComplex (ℕᵒᵖ ⥤ Ab.{u})) (h : S.ShortExact) :
    Mono (S.map (lim : (ℕᵒᵖ ⥤ Ab.{u}) ⥤ Ab.{u})).f ∧
      (S.map (lim : (ℕᵒᵖ ⥤ Ab.{u}) ⥤ Ab.{u})).Exact

Ab.isMittagLeffler_X₃_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ShortComplex/InverseLimit.lean, line 389. The attribute's comment: “ML_quotient”. References: EGA 0 (13.2.1), “(i), systems over ℕ”; SGA 5 V (2.1.2), “(i)”.

Part (2): a quotient of a Mittag-Leffler inverse system is Mittag-Leffler.

theorem Ab.isMittagLeffler_X₃_of_shortExact
    (S : ShortComplex (ℕᵒᵖ ⥤ Ab.{u})) (h : S.ShortExact)
    (hB : (S.X₂ ⋙ forget Ab).IsMittagLeffler) : (S.X₃ ⋙ forget Ab).IsMittagLeffler

Ab.shortExact_lim_of_isMittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ShortComplex/InverseLimit.lean, line 399. The attribute's comment: “ML_short_exact”. References: EGA 0 (13.2.2), “systems over ℕ”.

Part (3): if the kernel system is Mittag-Leffler, then the limit sequence 0 → lim A → lim B → lim C → 0 is short exact.

theorem Ab.shortExact_lim_of_isMittagLeffler
    (S : ShortComplex (ℕᵒᵖ ⥤ Ab.{u})) (h : S.ShortExact)
    (hA : (S.X₁ ⋙ forget Ab).IsMittagLeffler) :
    (S.map (lim : (ℕᵒᵖ ⥤ Ab.{u}) ⥤ Ab.{u})).ShortExact

ModuleCat.shortExact_lim_of_isMittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ShortComplex/InverseLimit.lean, line 490. The attribute's comment: “ML_short_exact, for towers of modules”. References: EGA 0 (13.2.2), “ℕ-indexed systems”; EGA III (4.1.7.21), “more general”.

Stacks 02N1 part (3) for towers of modules: if the kernel system is Mittag-Leffler, then the limit sequence 0 → lim A → lim B → lim C → 0 is short exact. This is CategoryTheory.ShortComplex.shortExact_map_lim_of_isMittagLeffler with the pointwise short exactness obtained from short exactness in the functor category, evaluation being exact.

theorem ModuleCat.shortExact_lim_of_isMittagLeffler {R : Type u} [Ring R]
    (S : ShortComplex (ℕᵒᵖ ⥤ ModuleCat.{v} R)) (h : S.ShortExact)
    (hA : (S.X₁ ⋙ forget (ModuleCat.{v} R)).IsMittagLeffler) :
    (S.map (lim : (ℕᵒᵖ ⥤ ModuleCat.{v} R) ⥤ ModuleCat.{v} R)).ShortExact

ModuleCat.isMittagLeffler_X₃_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ShortComplex/InverseLimit.lean, line 500. The attribute's comment: “ML_quotient, for towers of modules”.

Stacks 02N1 part (2) for towers of modules: a quotient of a Mittag-Leffler inverse system is Mittag-Leffler.

theorem ModuleCat.isMittagLeffler_X₃_of_shortExact {R : Type u} [Ring R]
    (S : ShortComplex (ℕᵒᵖ ⥤ ModuleCat.{v} R)) (h : S.ShortExact)
    (hB : (S.X₂ ⋙ forget (ModuleCat.{v} R)).IsMittagLeffler) :
    (S.X₃ ⋙ forget (ModuleCat.{v} R)).IsMittagLeffler
Tag 070B, a lemma

Tag 070B in the Stacks Project.

Ab.exact_lim_map_of_isMittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ShortComplex/InverseLimit.lean, line 472. References: EGA 0 (13.2.2), “partial”.

Let A → B → C → D be an exact sequence of inverse systems of abelian groups indexed by ℕ. If A satisfies the Mittag-Leffler condition, then the induced sequence on inverse limits lim B → lim C → lim D is exact at lim C.

The proof is the source's: ψ factors through K = Ker(χ) by an epimorphism ψ', whose kernel is a quotient of A, hence Mittag-Leffler (02N1); so lim B → lim K is onto (02N1), and lim K = Ker(lim χ) because lim preserves kernels.

theorem Ab.exact_lim_map_of_isMittagLeffler {A B C D : ℕᵒᵖ ⥤ Ab.{u}} (φ : A ⟶ B) (ψ : B ⟶ C)
    (χ : C ⟶ D)
    (hφψ : φ ≫ ψ = 0) (hψχ : ψ ≫ χ = 0)
    (hAB : (ShortComplex.mk φ ψ hφψ).Exact) (hBC : (ShortComplex.mk ψ χ hψχ).Exact)
    (hML : (A ⋙ forget Ab).IsMittagLeffler) :
    (ShortComplex.mk (lim.map ψ) (lim.map χ)
      (by rw [← lim.map_comp, hψχ, Functor.map_zero])).Exact

ModuleCat.exact_lim_map_of_isMittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ShortComplex/InverseLimit.lean, line 518. The attribute's comment: “for towers of modules”. References: EGA 0 (13.2.2), “partial”.

Stacks 070B for towers of modules. Let A → B → C → D be an exact sequence of inverse systems of R-modules indexed by ℕ. If A satisfies the Mittag-Leffler condition, then the induced sequence on inverse limits lim B → lim C → lim D is exact at lim C.

This is the same argument as Ab.exact_lim_map_of_isMittagLeffler, run with the two inputs for towers of modules: ψ factors through K = Ker(χ) by an epimorphism ψ', whose kernel is a quotient of A, hence Mittag-Leffler; so lim B → lim K is onto, and lim K = Ker(lim χ) because lim preserves kernels.

theorem ModuleCat.exact_lim_map_of_isMittagLeffler {R : Type u} [Ring R]
    {A B C D : ℕᵒᵖ ⥤ ModuleCat.{v} R} (φ : A ⟶ B) (ψ : B ⟶ C) (χ : C ⟶ D)
    (hφψ : φ ≫ ψ = 0) (hψχ : ψ ≫ χ = 0)
    (hAB : (ShortComplex.mk φ ψ hφψ).Exact) (hBC : (ShortComplex.mk ψ χ hψχ).Exact)
    (hML : (A ⋙ forget (ModuleCat.{v} R)).IsMittagLeffler) :
    (ShortComplex.mk (lim.map ψ) (lim.map χ)
      (by rw [← lim.map_comp, hψχ, Functor.map_zero])).Exact
Tag 070C, a lemma

Tag 070C in the Stacks Project.

essentially_constant_iff_direct_sum_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/EssentiallyConstant/Biproducts.lean, line 562.

For a directed preorder ι and an inverse system F : ιᵒᵖ ⥤ 𝓐 in an abelian category with a limit cone c, the system is essentially constant if and only if there is an index i₀ admitting a compatible direct-sum decomposition with eventually-vanishing Z-summand.

theorem essentially_constant_iff_direct_sum_decomposition
    [IsDirected ι (· ≤ ·)]
    (F : ιᵒᵖ ⥤ 𝓐) (c : Cone F) (_hc : IsLimit c) :
    (∃ (i : ιᵒᵖ) (s : F.obj i ⟶ c.pt),
        EssentiallyConstantPro.IsEssentiallyConstantWith F c i s) ↔
      HasDirectSumDecomposition F c
Tag 070D, a lemma

Tag 070D in the Stacks Project.

isMittagLeffler_forget_iff_of_isEssentiallyConstantPro, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ShortComplex/InverseLimit.lean, line 707.

Let 0 → (A_i) → (B_i) → (C_i) → 0 be a short exact sequence of inverse systems of abelian groups indexed by a cofiltered category J. If (C_i) is essentially constant, then (A_i) has the Mittag-Leffler property iff (B_i) does.

theorem isMittagLeffler_forget_iff_of_isEssentiallyConstantPro
    {J : Type*} [Category J] [IsCofiltered J]
    (S : ShortComplex (J ⥤ Ab))
    (hS : S.ShortExact)
    (hC : EssentiallyConstantPro.IsEssentiallyConstantPro S.X₃) :
    (S.X₁ ⋙ forget Ab).IsMittagLeffler ↔ (S.X₂ ⋙ forget Ab).IsMittagLeffler
Tag 070E, a lemma

Tag 070E in the Stacks Project.

isIso_comparisonHomologyLimit_of_isMittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/InverseLimit.lean, line 534. References: EGA 0 (13.2.3), “special case”.

For a countable inverse system of 4-term complexes of abelian groups, if (A^{-2}_i) and (A^{-1}_i) are Mittag-Leffler and (H^{-1}_i) is essentially constant, then the comparison morphism from the 0-cohomology of the limit complex to the limit of the 0-cohomologies is an isomorphism.

theorem isIso_comparisonHomologyLimit_of_isMittagLeffler
    (A_neg2 A_neg1 A_0 A_1 : ℕᵒᵖ ⥤ Ab.{v})
    (d_neg2 : A_neg2 ⟶ A_neg1) (d_neg1 : A_neg1 ⟶ A_0) (d_0 : A_0 ⟶ A_1)
    (h_neg1 : ∀ i, d_neg2.app i ≫ d_neg1.app i = 0)
    (h_0 : ∀ i, d_neg1.app i ≫ d_0.app i = 0)
    (hML_neg2 : (A_neg2 ⋙ forget Ab).IsMittagLeffler)
    (hML_neg1 : (A_neg1 ⋙ forget Ab).IsMittagLeffler)
    (hEC : EssentiallyConstantPro.IsEssentiallyConstantPro
      (homologyInvSystem d_neg2 d_neg1 h_neg1)) :
    IsIso (comparisonHomologyLimit d_neg1 d_0 h_0)
Tag 0AAT, a lemma

Tag 0AAT in the Stacks Project.

acyclic_limit_of_acyclic_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/InverseLimit.lean, line 922.

Let α be an ordinal and K an inverse system of cochain complexes of abelian groups over α. If every K_β is acyclic and the comparison map K^n_β → lim_{γ < β} K^n_γ is surjective for every β and n, then the limit complex lim_{β < α} K_β is acyclic.

theorem acyclic_limit_of_acyclic_of_surjective (α : Ordinal.{u})
    (K : (α.ToType)ᵒᵖ ⥤ CochainComplex AddCommGrpCat.{u} ℤ)
    (hAcyclic : ∀ β : α.ToType, (K.obj (op β)).Acyclic)
    (hSurj : ∀ (β : α.ToType) (n : ℤ),
      Function.Surjective
        (ConcreteCategory.hom (comparisonMap α K β n))) :
    (limit K).Acyclic
Sources
LeaninverseSystem_preadditive · inverseSystem_hasFiniteBiproducts · inverseSystem_abelian · inverseSystem_shortComplex_exact_iff · IsMittagLefflerCategorical · Ab.mono_lim_map_and_exact_of_shortExact · Ab.isMittagLeffler_X₃_of_shortExact · Ab.shortExact_lim_of_isMittagLeffler

Section12.32 Exactness of products#

Section 12.32 of the Stacks Project, Tag 060J. 1 tag here is carried by 3 declarations of the repository (all in StacksCore) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 060K, a lemma

Tag 060K in the Stacks Project.

CategoryTheory.ShortComplex.pi, a def in StacksCore (human-reviewed), declared in StacksCore/Algebra/Homology/ShortComplex/Products.lean, line 78. The attribute's comment: “The product ∏ L_i ⟶ ∏ M_i ⟶ ∏ N_i is a complex (the zero field)”.

The product short complex ∏ (S i).X₁ ⟶ ∏ (S i).X₂ ⟶ ∏ (S i).X₃ of a family of short complexes, with the differentials Pi.map. Its zero field is the clause of Stacks 060K that ∏ L_i ⟶ ∏ M_i ⟶ ∏ N_i is again a complex.

noncomputable def pi : ShortComplex C

CategoryTheory.ShortComplex.piHomologyIso, a def in StacksCore (human-reviewed), declared in StacksCore/Algebra/Homology/ShortComplex/Products.lean, line 143. The attribute's comment: “General version: exact products of short complexes in an abelian category”.

Exactness of products (Stacks 060K, general version): when I-indexed products are exact in the abelian category C, the homology of the product short complex pi S is the product of the homologies of the S i.

noncomputable def piHomologyIso : (pi S).homology ≅ ∏ᶜ fun i ↦ (S i).homology

CategoryTheory.ShortComplex.piHomologyIsoAddCommGrpCat, a def in StacksCore (human-reviewed), declared in StacksCore/Algebra/Homology/ShortComplex/Products.lean, line 194. The attribute's comment: “The Stacks statement: products of complexes of abelian groups”.

Exactness of products (Stacks 060K): for a family L_i ⟶ M_i ⟶ N_i of complexes of abelian groups with cohomology H_i, the complex ∏ L_i ⟶ ∏ M_i ⟶ ∏ N_i (pi S) has homology ∏ H_i. Products of abelian groups are exact by Mathlib's AB4Star AddCommGrpCat.

noncomputable def piHomologyIsoAddCommGrpCat :
    (pi S).homology ≅ ∏ᶜ fun i ↦ (S i).homology

Declarations registered for the tag:

Sources
LeanCategoryTheory.ShortComplex.pi · CategoryTheory.ShortComplex.piHomologyIso · CategoryTheory.ShortComplex.piHomologyIsoAddCommGrpCat · instHasExactLimitsOfShapeDiscreteAddCommGrpCat · instAB4StarAddCommGrpCat

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.