13.38 Brown representability to 13.42 Essentially constant…

Section13.38 Brown representability #

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

Tag 0A8F, a lemma

Tag 0A8F in the Stacks Project.

CategoryTheory.Pretriangulated.exists_iso_preadditiveYoneda_of_compactlyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/BrownRepresentability.lean, line 322.

Brown representability: let D be a triangulated category with arbitrary direct sums which is compactly generated, i.e. there is a family E : ι → D of compact objects (each preadditiveCoyoneda.obj (op (E i)) preserves direct sums) whose direct sum generates D (the only objects right orthogonal to all shifts of the E i are the zero objects). Then every contravariant cohomological functor H : Dᵒᵖ ⥤ AddCommGrpCat which transforms direct sums into products is representable: H ≅ Hom(-, X) for some X : D.

public theorem exists_iso_preadditiveYoneda_of_compactlyGenerated
    {ι : Type v} (E : ι → D)
    [∀ (i : ι) (α : Type v),
      PreservesColimitsOfShape (Discrete α) (preadditiveCoyoneda.obj (op (E i)))]
    (hE : ∀ Y : D, ((ofObj E).shiftClosure ℤ).rightOrthogonal Y → IsZero Y)
    (H : Dᵒᵖ ⥤ AddCommGrpCat.{v}) [H.IsHomological]
    [∀ α : Type v, PreservesLimitsOfShape (Discrete α) H] :
    ∃ X : D, Nonempty (H ≅ preadditiveYoneda.obj X)

Tag 0A8G, a proposition

Tag 0A8G in the Stacks Project.

CategoryTheory.Pretriangulated.exists_isTriangulated_rightAdjoint_of_compactlyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/BrownRepresentability.lean, line 415. References: SGA 4 XVII (2.2.13.1), “Triangulated case”.

Let D be a triangulated category with arbitrary direct sums which is compactly generated, i.e. there is a family E : ι → D of compact objects (each preadditiveCoyoneda.obj (op (E i)) preserves direct sums) whose direct sum generates D (the only objects right orthogonal to all shifts of the E i are the zero objects). Let F : D ⥤ D' be an exact functor of triangulated categories which transforms direct sums into direct sums. Then F has a right adjoint G, which is again exact: the adjunction F ⊣ G is a triangulated adjunction for a (unique) Functor.CommShift ℤ structure on G.

public theorem exists_isTriangulated_rightAdjoint_of_compactlyGenerated
    (F : D ⥤ D') [F.CommShift ℤ] [F.IsTriangulated]
    [∀ α : Type v, PreservesColimitsOfShape (Discrete α) F]
    {ι : Type v} (E : ι → D)
    [∀ (i : ι) (α : Type v),
      PreservesColimitsOfShape (Discrete α) (preadditiveCoyoneda.obj (op (E i)))]
    (hE : ∀ Y : D, ((ofObj E).shiftClosure ℤ).rightOrthogonal Y → IsZero Y) :
    ∃ (G : D' ⥤ D) (adj : F ⊣ G) (_ : G.CommShift ℤ), adj.IsTriangulated

Sources

LeanCategoryTheory.Pretriangulated.exists_iso_preadditiveYoneda_of_compactlyGenerated · CategoryTheory.Pretriangulated.exists_isTriangulated_rightAdjoint_of_compactlyGenerated

Section13.39 Brown representability, bis #

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

Tag 0GYG, a lemma

Tag 0GYG in the Stacks Project.

CategoryTheory.Pretriangulated.exists_iso_preadditiveYoneda_of_generating_of_factorsThroughSigma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/WeakBrownRepresentability.lean, line 803.

Brown representability, weak version: let 𝒟 be a triangulated category with direct sums and let E : ι → 𝒟 be a family of objects such that every nonzero object of 𝒟 receives a nonzero morphism from some E i, and such that every morphism from some E i to a countable direct sum ∐ X, X : ℕ → 𝒟, factors through a direct sum ∐ fun n ↦ E (j n) of members of the family via a direct sum of morphisms E (j n) ⟶ X n. Then a contravariant cohomological functor H : 𝒟ᵒᵖ ⥤ AddCommGrpCat which transforms direct sums into products is representable.

public theorem exists_iso_preadditiveYoneda_of_generating_of_factorsThroughSigma
    {D : Type u} [Category.{v} D] [Preadditive D] [HasZeroObject D] [HasShift D ℤ]
    [∀ n : ℤ, (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D]
    [HasCoproducts.{max w v} D] {ι : Type w} (E : ι → D)
    (hE : ∀ X : D, ¬ IsZero X → ∃ (i : ι) (f : E i ⟶ X), f ≠ 0)
    (hE' : ∀ (X : ℕ → D) (i : ι) (α : E i ⟶ ∐ X), ∃ (j : ℕ → ι) (β : ∀ n, E (j n) ⟶ X n)
      (γ : E i ⟶ ∐ fun n ↦ E (j n)), α = γ ≫ Limits.Sigma.map β)
    (H : Dᵒᵖ ⥤ AddCommGrpCat.{v}) [H.IsHomological]
    [∀ J : Type (max w v), PreservesLimitsOfShape (Discrete J) H] :
    ∃ X : D, Nonempty (preadditiveYoneda.obj X ≅ H)

Tag 0GYH, a proposition

Tag 0GYH in the Stacks Project.

CategoryTheory.Pretriangulated.exists_isTriangulated_rightAdjoint_of_generating_of_factorsThroughSigma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/BrownRepresentability.lean, line 636. References: SGA 4 XVII (2.2.13.1), “Triangulated case”.

Let D be a triangulated category with direct sums and let E : ι → D be a family of objects satisfying conditions (1) and (2) of weak Brown representability [Stacks, Tag 0GYG]: every nonzero object of D receives a nonzero morphism from some E i, and every morphism from some E i to a countable direct sum ∐ X, X : ℕ → D, factors through a direct sum ∐ fun n ↦ E (j n) of members of the family via a direct sum of morphisms E (j n) ⟶ X n. Let F : D ⥤ D' be an exact functor of triangulated categories which transforms direct sums into direct sums. Then F has a right adjoint G, which is again exact: the adjunction F ⊣ G is a triangulated adjunction for a (unique) Functor.CommShift ℤ structure on G.

public theorem exists_isTriangulated_rightAdjoint_of_generating_of_factorsThroughSigma
    (F : D ⥤ D') [F.CommShift ℤ] [F.IsTriangulated]
    [∀ α : Type (max w v), PreservesColimitsOfShape (Discrete α) F]
    {ι : Type w} (E : ι → D)
    (hE : ∀ X : D, ¬ IsZero X → ∃ (i : ι) (f : E i ⟶ X), f ≠ 0)
    (hE' : ∀ (X : ℕ → D) (i : ι) (α : E i ⟶ ∐ X), ∃ (j : ℕ → ι) (β : ∀ n, E (j n) ⟶ X n)
      (γ : E i ⟶ ∐ fun n ↦ E (j n)), α = γ ≫ Limits.Sigma.map β) :
    ∃ (G : D' ⥤ D) (adj : F ⊣ G) (_ : G.CommShift ℤ), adj.IsTriangulated

Sources

LeanCategoryTheory.Pretriangulated.exists_iso_preadditiveYoneda_of_generating_of_factorsThroughSigma · CategoryTheory.Pretriangulated.exists_isTriangulated_rightAdjoint_of_generating_of_factorsThroughSigma

Section13.40 Admissible subcategories #

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

Tag 0CQQ, a lemma

Tag 0CQQ in the Stacks Project.

Stacks.Triangulated.RightOrthogonal.inRightOrthogonal_iff_postcomp_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 1012.

Stacks Tag 0CQQ / Lemma 13.40.2.

Let A ⊆ D (described by P) be a full subcategory invariant under all shifts (up to isomorphism), and let X --f--> Y --g--> Z --h--> X[1] be a distinguished triangle. Then Z is in the right orthogonal Aᗮ if and only if, for every object A of A, the map f_* : Hom(A, X) → Hom(A, Y), g ↦ g ≫ f, is an isomorphism of abelian groups (here expressed as a bijection).

Proof outline (as in the source), applying the homological functor Hom(A,-): * (1) ⇒ (2): injectivity of f_* uses the inverse-rotated triangle Z⟦-1⟧ → X → Y and coyoneda_exact₂: a kernel element factors through Z⟦-1⟧, which vanishes by hom_to_shift_eq_zero; surjectivity uses coyoneda_exact₂ on T since u ≫ g = 0 for any u : A ⟶ Y (as Z ∈ Aᗮ). * (2) ⇒ (1): for u : A ⟶ Z, first u ≫ h = 0 by injectivity of · ≫ f⟦1⟧ (Helper 3 and bijective_postcomp_shift transport bijectivity to Hom(A, X⟦1⟧)) together with comp_distTriang_mor_zero₂₃ on the rotated triangle; then coyoneda_exact₂ on the rotated triangle factors u = v ≫ g, surjectivity of f_* gives v = w ≫ f, and f ≫ g = 0 yields u = w ≫ (f ≫ g) = 0.

theorem inRightOrthogonal_iff_postcomp_bijective
    (P : C → Prop) (hP : InvariantUnderAllShifts P)
    (T : Triangle C) (hT : T ∈ distinguishedTriangles) :
    InRightOrthogonal P T.obj₃ ↔
      ∀ (A : C), P A → Function.Bijective (fun g : A ⟶ T.obj₁ => g ≫ T.mor₁)

Tag 0H0M, a lemma

Tag 0H0M in the Stacks Project.

Stacks.Triangulated.AdmissibleSubcategories.isLeftOrthogonal_iff_bijective_precompMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 1245.

Theorem (Stacks Tag 0H0M, Lemma 13.40.3). Let B ⊂ D be a full subcategory invariant under all shifts, and let X --f--> Y --g--> Z --h--> X[1] be a distinguished triangle. Then X lies in the left orthogonal ᗮB if and only if, for every object B of B, the precomposition map g* : Hom_D(Z, B) → Hom_D(Y, B) is bijective.

theorem isLeftOrthogonal_iff_bijective_precompMap
    (B : D → Prop) (hB : ShiftInvariant B)
    (T : Triangle D) (hT : T ∈ distinguishedTriangles) :
    IsLeftOrthogonal B T.obj₁ ↔
      ∀ (b : D), B b → Function.Bijective (precompMap T b)

Tag 0FXC, a lemma

Tag 0FXC in the Stacks Project.

CategoryTheory.ObjectProperty.isStableUnderRetracts_rightOrthogonal_and_leftOrthogonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 158. References: SGA 4½ Etat 0 (2.6.2), “thickness”.

Let C be a category with zero morphisms and P : ObjectProperty C a property of its objects. Then both the right orthogonal P.rightOrthogonal and the left orthogonal P.leftOrthogonal are stable under retracts; in particular they are saturated, i.e. thick, and strictly full subcategories of C.

theorem isStableUnderRetracts_rightOrthogonal_and_leftOrthogonal (P : ObjectProperty C) :
    P.rightOrthogonal.IsStableUnderRetracts ∧ P.leftOrthogonal.IsStableUnderRetracts

Tag 0CQR, a lemma

Tag 0CQR in the Stacks Project.

CategoryTheory.ObjectProperty.isTriangulated_extensionProduct_of_le_rightOrthogonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 580.

Let C be a triangulated category, let A and B be triangulated subcategories of C with B contained in the right orthogonal of A. Then the objects X of C that fit in a distinguished triangle A' ⟶ X ⟶ B' ⟶ A'⟦1⟧ with A' in A and B' in B form a triangulated subcategory of C: they are stable under shifts, two out of three of them in a distinguished triangle forces the third, and they are stable under direct sums. For B = A.rightOrthogonal this is the property P of [Stacks, Tag 0CQR].

theorem isTriangulated_extensionProduct_of_le_rightOrthogonal
    (A B : ObjectProperty C) [A.IsTriangulated] [B.IsTriangulated]
    (hB : B ≤ A.rightOrthogonal) :
    (A.extensionProduct B).IsTriangulated

Tag 0H0N, a lemma

Tag 0H0N in the Stacks Project.

CategoryTheory.ObjectProperty.isTriangulated_extensionProduct_leftOrthogonal_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 599.

Let C be a triangulated category and let B be a triangulated subcategory of C. Then the objects X of C that fit in a distinguished triangle A ⟶ X ⟶ B' ⟶ A⟦1⟧ with A in the left orthogonal of B and B' in B form a triangulated subcategory of C: they are stable under shifts, two out of three of them in a distinguished triangle forces the third, and they are stable under direct sums. This is the property P of [Stacks, Tag 0H0N].

theorem isTriangulated_extensionProduct_leftOrthogonal_self (B : ObjectProperty C)
    [B.IsTriangulated] :
    (B.leftOrthogonal.extensionProduct B).IsTriangulated

Tag 0CQS, a lemma

Tag 0CQS in the Stacks Project.

CategoryTheory.ObjectProperty.isLeftAdjoint_ι_iff_extensionProduct_rightOrthogonal_eq_top_and_isSaturated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 342.

Let C be a pretriangulated category and let A : ObjectProperty C be invariant under all shifts, for instance a triangulated subcategory of C. Then the inclusion A.ι : A.FullSubcategory ⥤ C has a right adjoint if and only if every object X of C fits in a distinguished triangle A' ⟶ X ⟶ B ⟶ A'⟦1⟧ with A' satisfying A and B in the right orthogonal of A, i.e. if and only if A.extensionProduct A.rightOrthogonal = ⊤; and in that case A is saturated, i.e. thick ([Stacks, Tag 05RB]), and the objects isomorphic to an object satisfying A are exactly the objects of the left orthogonal of A.rightOrthogonal, so a strictly full such A satisfies A = ᗮ(Aᗮ).

theorem isLeftAdjoint_ι_iff_extensionProduct_rightOrthogonal_eq_top_and_isSaturated
    (A : ObjectProperty C) [A.IsStableUnderShift ℤ] :
    (A.ι.IsLeftAdjoint ↔ A.extensionProduct A.rightOrthogonal = ⊤) ∧
      (A.extensionProduct A.rightOrthogonal = ⊤ →
        A.IsSaturated ∧ A.isoClosure = A.rightOrthogonal.leftOrthogonal)

Tag 0CQT, a lemma

Tag 0CQT in the Stacks Project.

CategoryTheory.ObjectProperty.isRightAdjoint_ι_iff_extensionProduct_leftOrthogonal_self_eq_top_and_isSaturated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 484.

Let C be a pretriangulated category and let B : ObjectProperty C be invariant under all shifts, for instance a triangulated subcategory of C. Then the inclusion B.ι : B.FullSubcategory ⥤ C has a left adjoint if and only if every object X of C fits in a distinguished triangle A ⟶ X ⟶ B' ⟶ A⟦1⟧ with A in the left orthogonal of B and B' satisfying B, i.e. if and only if B.leftOrthogonal.extensionProduct B = ⊤; and in that case B is saturated, i.e. thick ([Stacks, Tag 05RB]), and the objects isomorphic to an object satisfying B are exactly the objects of the right orthogonal of B.leftOrthogonal, so a strictly full such B satisfies B = (ᗮB)ᗮ.

theorem isRightAdjoint_ι_iff_extensionProduct_leftOrthogonal_self_eq_top_and_isSaturated
    (B : ObjectProperty C) [B.IsStableUnderShift ℤ] :
    (B.ι.IsRightAdjoint ↔ B.leftOrthogonal.extensionProduct B = ⊤) ∧
      (B.leftOrthogonal.extensionProduct B = ⊤ →
        B.IsSaturated ∧ B.isoClosure = B.leftOrthogonal.rightOrthogonal)

Tag 0FXD, a definition

Tag 0FXD in the Stacks Project.

CategoryTheory.ObjectProperty.IsRightAdmissible, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 271.

A property A of the objects of a pretriangulated category C is right admissible if it is strictly full (closed under isomorphisms) and triangulated, and the inclusion A.ι : A.FullSubcategory ⥤ C has a right adjoint. By [Stacks, Tag 0CQS] the last condition holds if and only if every object X of C fits in a distinguished triangle A' ⟶ X ⟶ B ⟶ A'⟦1⟧ with A' satisfying A and B in the right orthogonal of A, and it then forces A = ᗮ(Aᗮ).

public class IsRightAdmissible (A : ObjectProperty C) : Prop extends
  A.IsClosedUnderIsomorphisms, A.IsTriangulated, A.ι.IsLeftAdjoint

CategoryTheory.ObjectProperty.IsLeftAdmissible, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 280.

A property A of the objects of a pretriangulated category C is left admissible if it is strictly full (closed under isomorphisms) and triangulated, and the inclusion A.ι : A.FullSubcategory ⥤ C has a left adjoint. By [Stacks, Tag 0CQT] the last condition holds if and only if every object X of C fits in a distinguished triangle A' ⟶ X ⟶ B ⟶ A'⟦1⟧ with A' in the left orthogonal of A and B satisfying A, and it then forces A = (ᗮA)ᗮ.

public class IsLeftAdmissible (A : ObjectProperty C) : Prop extends
  A.IsClosedUnderIsomorphisms, A.IsTriangulated, A.ι.IsRightAdjoint

CategoryTheory.ObjectProperty.IsTwoSidedAdmissible, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 287.

A property A of the objects of a pretriangulated category C is two-sided admissible if it is both right and left admissible, i.e. A is a strictly full triangulated subcategory whose inclusion A.ι : A.FullSubcategory ⥤ C has both a right and a left adjoint.

public class IsTwoSidedAdmissible (A : ObjectProperty C) : Prop extends
  A.IsRightAdmissible, A.IsLeftAdmissible

Tag 0H0P, a proposition

Tag 0H0P in the Stacks Project.

CategoryTheory.ObjectProperty.tfae_isRightAdmissible_isLeftAdmissible_extensionProduct_and_isEquivalence_ι_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/AdmissibleSubcategories.lean, line 820. References: SGA 4½ Etat 0 (2.6.6).

Let C be a triangulated category and let A B : ObjectProperty C be strictly full and invariant under all shifts. Then: A is right admissible with B = Aᗮ if and only if B is left admissible with A = ᗮB if and only if Hom(A', B') = 0 for A' in A and B' in B and every object X of C fits in a distinguished triangle A' ⟶ X ⟶ B' ⟶ A'⟦1⟧ with A' ∈ A, B' ∈ B. If this holds, then for every Verdier quotient L : C ⥤ Q of C by B, i.e. every localization of C at B.trW, the composite A.ι ⋙ L : A ⥤ Q is an equivalence and a right adjoint of the inclusion A.ι is L ⋙ G for some G : Q ⥤ A, necessarily a quasi-inverse of A.ι ⋙ L; and dually for the Verdier quotient of C by A, the inclusion B.ι and its left adjoint.

theorem tfae_isRightAdmissible_isLeftAdmissible_extensionProduct_and_isEquivalence_ι_comp
    (A B : ObjectProperty C) [A.IsClosedUnderIsomorphisms] [B.IsClosedUnderIsomorphisms]
    [A.IsStableUnderShift ℤ] [B.IsStableUnderShift ℤ] :
    [A.IsRightAdmissible ∧ B = A.rightOrthogonal,
      B.IsLeftAdmissible ∧ A = B.leftOrthogonal,
      A ≤ B.leftOrthogonal ∧ A.extensionProduct B = ⊤].TFAE ∧
    (A ≤ B.leftOrthogonal → A.extensionProduct B = ⊤ →
      (∀ {Q : Type w} [Category.{w'} Q] (L : C ⥤ Q) [L.IsLocalization B.trW],
          (A.ι ⋙ L).IsEquivalence ∧
            ∃ G : Q ⥤ A.FullSubcategory, Nonempty (A.ι ⊣ L ⋙ G)) ∧
      (∀ {Q : Type w} [Category.{w'} Q] (L : C ⥤ Q) [L.IsLocalization A.trW],
          (B.ι ⋙ L).IsEquivalence ∧
            ∃ G : Q ⥤ B.FullSubcategory, Nonempty (L ⋙ G ⊣ B.ι)))

Sources

LeanStacks.Triangulated.RightOrthogonal.inRightOrthogonal_iff_postcomp_bijective · Stacks.Triangulated.AdmissibleSubcategories.isLeftOrthogonal_iff_bijective_precompMap · CategoryTheory.ObjectProperty.isStableUnderRetracts_rightOrthogonal_and_leftOrthogonal · CategoryTheory.ObjectProperty.isTriangulated_extensionProduct_of_le_rightOrthogonal · CategoryTheory.ObjectProperty.isTriangulated_extensionProduct_leftOrthogonal_self · CategoryTheory.ObjectProperty.isLeftAdjoint_ι_iff_extensionProduct_rightOrthogonal_eq_top_and_isSaturated · CategoryTheory.ObjectProperty.isRightAdjoint_ι_iff_extensionProduct_leftOrthogonal_self_eq_top_and_isSaturated · CategoryTheory.ObjectProperty.IsRightAdmissible

Section13.41 Postnikov systems #

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

Tag 0D7Z, a definition

Tag 0D7Z in the Stacks Project.

CategoryTheory.Triangulated.PostnikovSystem, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/PostnikovSystems.lean, line 84.

A Postnikov system for a complex Xₙ ⟶ Xₙ₋₁ ⟶ ⋯ ⟶ X₀ in a pretriangulated category, the morphisms of the complex being d i : X i.succ ⟶ X i.castSucc: objects Y₀, …, Yₙ together with an isomorphism Y₀ ⟶ X₀ and distinguished triangles Yᵢ₊₁ ⟶ Xᵢ₊₁ ⟶ Yᵢ ⟶ Yᵢ₊₁⟦1⟧ in which the composition Xᵢ₊₁ ⟶ Yᵢ ⟶ Xᵢ is the given morphism Xᵢ₊₁ ⟶ Xᵢ.

public structure PostnikovSystem {n : ℕ} (X : Fin (n + 1) → D)
    (d : ∀ i : Fin n, X i.succ ⟶ X i.castSucc)

Tag 0D81, a lemma

Tag 0D81 in the Stacks Project.

CategoryTheory.Triangulated.nonempty_postnikovSystem_of_length_le_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/PostnikovSystems.lean, line 299.

A complex Xₙ ⟶ Xₙ₋₁ ⟶ ⋯ ⟶ X₀ of length n ≤ 2 in a pretriangulated category admits a Postnikov system. The bound is sharp: for n > 2 Postnikov systems do not always exist.

theorem nonempty_postnikovSystem_of_length_le_two {n : ℕ}
    (hn : n ≤ 2) (X : Fin (n + 1) → D) (d : ∀ i : Fin n, X i.succ ⟶ X i.castSucc)
    (hd : ∀ (i : Fin n) (h : (i : ℕ) + 1 < n), d ⟨(i : ℕ) + 1, h⟩ ≫ d i = 0) :
    Nonempty (PostnikovSystem X d)

Tag 0D82, a lemma

Tag 0D82 in the Stacks Project.

CategoryTheory.Triangulated.PostnikovSystem.hom_shift_obj_eq_zero_and_exists_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/PostnikovSystems.lean, line 453.

Let Xₙ ⟶ ⋯ ⟶ X₀ and X'ₙ ⟶ ⋯ ⟶ X'₀ be complexes in a pretriangulated category, let S' be a Postnikov system for the second one, and assume that every morphism Xᵢ⟦i - j - 1⟧ ⟶ X'ⱼ with i > j + 1 is zero. Then

every morphism Xᵢ⟦i - j - 1⟧ ⟶ Y'ⱼ with i > j + 1 is zero, and

for every Postnikov system S for the first complex, every morphism of complexes f i : Xᵢ ⟶ X'ᵢ extends to a (nonunique) morphism of Postnikov systems S ⟶ S', i.e. to a family g i : Yᵢ ⟶ Y'ᵢ compatible with the morphisms Yᵢ ⟶ Xᵢ, Xᵢ₊₁ ⟶ Yᵢ and Yᵢ ⟶ Yᵢ₊₁⟦1⟧ of the two systems.

theorem PostnikovSystem.hom_shift_obj_eq_zero_and_exists_hom {n : ℕ}
    (X : Fin (n + 1) → D) (d : ∀ i : Fin n, X i.succ ⟶ X i.castSucc)
    {X' : Fin (n + 1) → D} {d' : ∀ i : Fin n, X' i.succ ⟶ X' i.castSucc}
    (S' : PostnikovSystem X' d')
    (h : ∀ i j : Fin (n + 1), (j : ℕ) + 1 < (i : ℕ) →
      ∀ f : (X i)⟦((i : ℕ) : ℤ) - ((j : ℕ) : ℤ) - 1⟧ ⟶ X' j, f = 0) :
    (∀ i j : Fin (n + 1), (j : ℕ) + 1 < (i : ℕ) →
        ∀ f : (X i)⟦((i : ℕ) : ℤ) - ((j : ℕ) : ℤ) - 1⟧ ⟶ S'.obj j, f = 0) ∧
      ∀ (S : PostnikovSystem X d) (f : ∀ i, X i ⟶ X' i),
        (∀ i : Fin n, d i ≫ f i.castSucc = f i.succ ≫ d' i) →
        ∃ g : ∀ i, S.obj i ⟶ S'.obj i,
          (∀ i, g i ≫ S'.π i = S.π i ≫ f i) ∧
          (∀ i : Fin n, S.p i ≫ g i.castSucc = f i.succ ≫ S'.p i) ∧
          (∀ i : Fin n, S.δ i ≫ (g i.succ)⟦(1 : ℤ)⟧' = g i.castSucc ≫ S'.δ i)

Tag 0FXE, a lemma

Tag 0FXE in the Stacks Project.

CategoryTheory.Triangulated.PostnikovSystem.subsingleton_hom_last, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/PostnikovSystems.lean, line 870.

Let Xₙ ⟶ ⋯ ⟶ X₀ and X'ₙ ⟶ ⋯ ⟶ X'₀ be complexes in a pretriangulated category, let f i : Xᵢ ⟶ X'ᵢ be a family of morphisms, and let S, S' be Postnikov systems for the two complexes, with objects Yᵢ, Y'ᵢ. If

every morphism Xᵢ⟦i⟧ ⟶ Y'ₙ⟦n⟧ with i ≥ 1 is zero, or

every morphism Yₙ⟦n⟧ ⟶ X'ⱼ⟦j⟧ with j < n is zero, or

every morphism Xᵢ⟦i - j + 1⟧ ⟶ X'ⱼ and every morphism Xⱼ ⟶ X'ᵢ⟦i - j⟧ with i < j is zero,

then any two morphisms of Postnikov systems S ⟶ S' over f — families g i : Yᵢ ⟶ Y'ᵢ compatible with the morphisms Yᵢ ⟶ Xᵢ, Xᵢ₊₁ ⟶ Yᵢ and Yᵢ ⟶ Yᵢ₊₁⟦1⟧ of the two systems — induce the same morphism Yₙ ⟶ Y'ₙ on the totalizations.

theorem PostnikovSystem.subsingleton_hom_last {n : ℕ}
    {X X' : Fin (n + 1) → D} {d : ∀ i : Fin n, X i.succ ⟶ X i.castSucc}
    {d' : ∀ i : Fin n, X' i.succ ⟶ X' i.castSucc}
    (S : PostnikovSystem X d) (S' : PostnikovSystem X' d') (f : ∀ i, X i ⟶ X' i)
    (h : (∀ i : Fin (n + 1), 0 < (i : ℕ) →
            ∀ u : (X i)⟦((i : ℕ) : ℤ)⟧ ⟶ (S'.obj (Fin.last n))⟦(n : ℤ)⟧, u = 0) ∨
         (∀ j : Fin (n + 1), (j : ℕ) < n →
            ∀ u : (S.obj (Fin.last n))⟦(n : ℤ)⟧ ⟶ (X' j)⟦((j : ℕ) : ℤ)⟧, u = 0) ∨
         ((∀ i j : Fin (n + 1), (i : ℕ) < (j : ℕ) →
            ∀ u : (X i)⟦((i : ℕ) : ℤ) - ((j : ℕ) : ℤ) + 1⟧ ⟶ X' j, u = 0) ∧
          (∀ i j : Fin (n + 1), (i : ℕ) < (j : ℕ) →
            ∀ u : X j ⟶ (X' i)⟦((i : ℕ) : ℤ) - ((j : ℕ) : ℤ)⟧, u = 0))) :
    ((fun g : ∀ i, S.obj i ⟶ S'.obj i => g (Fin.last n)) ''
      {g : ∀ i, S.obj i ⟶ S'.obj i |
        (∀ i, g i ≫ S'.π i = S.π i ≫ f i) ∧
        (∀ i : Fin n, S.p i ≫ g i.castSucc = f i.succ ≫ S'.p i) ∧
        (∀ i : Fin n, S.δ i ≫ (g i.succ)⟦(1 : ℤ)⟧' = g i.castSucc ≫ S'.δ i)}).Subsingleton

Tag 0D83, a lemma

Tag 0D83 in the Stacks Project.

CategoryTheory.Triangulated.nonempty_postnikovSystem_of_hom_shift_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/PostnikovSystems.lean, line 589.

A complex Xₙ ⟶ ⋯ ⟶ X₀ in a pretriangulated category, with morphisms d i : Xᵢ₊₁ ⟶ Xᵢ, admits a Postnikov system as soon as every morphism Xᵢ⟦i - j - 2⟧ ⟶ Xⱼ with i > j + 2 is zero. Without that vanishing condition Postnikov systems need not exist once n > 2; for n ≤ 2 the condition is vacuous and this is CategoryTheory.Triangulated.nonempty_postnikovSystem_of_length_le_two.

theorem nonempty_postnikovSystem_of_hom_shift_eq_zero {n : ℕ} (X : Fin (n + 1) → D)
    (d : ∀ i : Fin n, X i.succ ⟶ X i.castSucc)
    (hd : ∀ (i : Fin n) (h : (i : ℕ) + 1 < n), d ⟨(i : ℕ) + 1, h⟩ ≫ d i = 0)
    (h : ∀ i j : Fin (n + 1), (j : ℕ) + 2 < (i : ℕ) →
      ∀ u : (X i)⟦((i : ℕ) : ℤ) - ((j : ℕ) : ℤ) - 2⟧ ⟶ X j, u = 0) :
    Nonempty (PostnikovSystem X d)

CategoryTheory.Triangulated.PostnikovSystem.exists_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/PostnikovSystems.lean, line 654.

Let Xₙ ⟶ ⋯ ⟶ X₀ be a diagram in a pretriangulated category, with morphisms d i : Xᵢ₊₁ ⟶ Xᵢ, such that every morphism Xᵢ⟦i - j - 1⟧ ⟶ Xⱼ with i > j + 1 is zero. Then for every diagram X'ₙ ⟶ ⋯ ⟶ X'₀ and every isomorphism f i : Xᵢ ≅ X'ᵢ of diagrams, any Postnikov systems S, S' for the two are isomorphic over f: there is a family of isomorphisms g i : Yᵢ ≅ Y'ᵢ compatible with the morphisms Yᵢ ⟶ Xᵢ, Xᵢ₊₁ ⟶ Yᵢ and Yᵢ ⟶ Yᵢ₊₁⟦1⟧ of the two systems. In particular, at X' = X, d' = d and f = 𝟙, any two Postnikov systems for Xₙ ⟶ ⋯ ⟶ X₀ are isomorphic.

theorem PostnikovSystem.exists_iso {n : ℕ} {X X' : Fin (n + 1) → D}
    {d : ∀ i : Fin n, X i.succ ⟶ X i.castSucc} {d' : ∀ i : Fin n, X' i.succ ⟶ X' i.castSucc}
    (h : ∀ i j : Fin (n + 1), (j : ℕ) + 1 < (i : ℕ) →
      ∀ u : (X i)⟦((i : ℕ) : ℤ) - ((j : ℕ) : ℤ) - 1⟧ ⟶ X j, u = 0)
    (S : PostnikovSystem X d) (S' : PostnikovSystem X' d') (f : ∀ i, X i ≅ X' i)
    (hf : ∀ i : Fin n, d i ≫ (f i.castSucc).hom = (f i.succ).hom ≫ d' i) :
    ∃ g : ∀ i, S.obj i ≅ S'.obj i,
      (∀ i, (g i).hom ≫ S'.π i = S.π i ≫ (f i).hom) ∧
      (∀ i : Fin n, S.p i ≫ (g i.castSucc).hom = (f i.succ).hom ≫ S'.p i) ∧
      (∀ i : Fin n, S.δ i ≫ ((g i.succ).hom)⟦(1 : ℤ)⟧' =
        (g i.castSucc).hom ≫ S'.δ i)

Sources

LeanCategoryTheory.Triangulated.PostnikovSystem · CategoryTheory.Triangulated.nonempty_postnikovSystem_of_length_le_two · CategoryTheory.Triangulated.PostnikovSystem.hom_shift_obj_eq_zero_and_exists_hom · CategoryTheory.Triangulated.PostnikovSystem.subsingleton_hom_last · CategoryTheory.Triangulated.nonempty_postnikovSystem_of_hom_shift_eq_zero · CategoryTheory.Triangulated.PostnikovSystem.exists_iso

Section13.42 Essentially constant systems #

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

Tag 0G39, a lemma

Tag 0G39 in the Stacks Project.

CategoryTheory.Pretriangulated.isEssentiallyConstant_op_iff_exists_iso_const_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/EssentiallyConstant.lean, line 745.

Stacks 0G39. An inverse system A : J ⥤ 𝒟 in a pre-triangulated category, indexed by a cofiltered category J, is essentially constant as a pro-object (Stacks 05PU for A.op) if and only if there are an index i, an object X and an inverse system Z : Over i ⥤ 𝒟 on the indices j ≥ i such that

A_j ≅ X ⊞ Z_j naturally in j ≥ i — so the transition morphisms respect the decomposition and are the identity on X — and

for every j ≥ i there are j' ≥ j and a transition morphism Z_{j'} ⟶ Z_j equal to zero.

The value of the essentially constant system is then X.

public theorem isEssentiallyConstant_op_iff_exists_iso_const_biprod [IsCofiltered J] (A : J ⥤ D) :
    IsEssentiallyConstantInd A.op ↔
      ∃ (i : J) (X : D) (Z : Over i ⥤ D)
        (_ : Over.forget i ⋙ A ≅ (Functor.const (Over i)).obj X ⊞ Z),
        ∀ j : Over i, ∃ (j' : Over i) (u : j' ⟶ j), Z.map u = 0

Tag 0G3A, a lemma

Tag 0G3A in the Stacks Project.

CategoryTheory.Pretriangulated.isEssentiallyConstant_op_π₂_and_exists_limit_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/EssentiallyConstant.lean, line 983.

Stacks 0G3A. Let T : J ⥤ Triangle 𝒟 be an inverse system of distinguished triangles A_j ⟶ B_j ⟶ C_j ⟶ A_j[1] in a pre-triangulated category, indexed by a cofiltered category J. If (A_j) and (C_j) are essentially constant as pro-objects (Stacks 05PU for the opposite diagrams), then so is (B_j), and there are an index n, a distinguished triangle S = (A ⟶ B ⟶ C ⟶ A[1]) of the values and a morphism of triangles φ : T_n ⟶ S which induces an isomorphism lim_{j ≥ n} A_j ⟶ A, and similarly for B and C: for each of the three terms there is a limit cone on the system restricted to the indices j ≥ n (the objects of Over n) whose apex is that term of S and whose leg at n is split by the corresponding component of φ.

public theorem isEssentiallyConstant_op_π₂_and_exists_limit_triangle [IsCofiltered J]
    (T : J ⥤ Triangle D) (hT : ∀ j, T.obj j ∈ distTriang D)
    (h₁ : IsEssentiallyConstantInd (T ⋙ Triangle.π₁).op)
    (h₃ : IsEssentiallyConstantInd (T ⋙ Triangle.π₃).op) :
    IsEssentiallyConstantInd (T ⋙ Triangle.π₂).op ∧
      ∃ (n : J) (S : Triangle D) (_ : S ∈ distTriang D) (φ : T.obj n ⟶ S)
        (πA : (Functor.const (Over n)).obj S.obj₁ ⟶ Over.forget n ⋙ T ⋙ Triangle.π₁)
        (πB : (Functor.const (Over n)).obj S.obj₂ ⟶ Over.forget n ⋙ T ⋙ Triangle.π₂)
        (πC : (Functor.const (Over n)).obj S.obj₃ ⟶ Over.forget n ⋙ T ⋙ Triangle.π₃),
        (πA.app (Over.mk (𝟙 n)) ≫ φ.hom₁ = 𝟙 S.obj₁ ∧ Nonempty (IsLimit (Cone.mk _ πA))) ∧
        (πB.app (Over.mk (𝟙 n)) ≫ φ.hom₂ = 𝟙 S.obj₂ ∧ Nonempty (IsLimit (Cone.mk _ πB))) ∧
        (πC.app (Over.mk (𝟙 n)) ≫ φ.hom₃ = 𝟙 S.obj₃ ∧ Nonempty (IsLimit (Cone.mk _ πC)))

Tag 0G3B, a lemma

Tag 0G3B in the Stacks Project.

DerivedCategory.isEssentiallyConstant_op_and_exists_limit_cone_of_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/EssentiallyConstant.lean, line 1210.

Let A : J ⥤ D(𝒜) be an inverse system in the derived category of an abelian category, indexed by a cofiltered category J. Assume H^i(A_j) = 0 for every j and every i outside an interval [a, b], and that each inverse system (H^i(A_j))_j of 𝒜 is essentially constant (Stacks 05PU for the opposite diagram). Then (A_j) is essentially constant: besides IsEssentiallyConstantInd A.op, there are an index n, an object X, a morphism φ : A_n ⟶ X and a limit cone with apex X on the system restricted to the indices j ≥ n (the objects of Over n) whose leg at n is split by φ; and for every i the image of that cone under H^i is again a limit cone, i.e. H^i(X) is the value of the essentially constant system (H^i(A_j))_j.

public theorem isEssentiallyConstant_op_and_exists_limit_cone_of_homology
    [IsCofiltered J] (A : J ⥤ DerivedCategory 𝒜) (a b : ℤ)
    (hA : ∀ (i : ℤ), i < a ∨ b < i → ∀ j : J, IsZero ((homologyFunctor 𝒜 i).obj (A.obj j)))
    (hH : ∀ i : ℤ, IsEssentiallyConstantInd (A ⋙ homologyFunctor 𝒜 i).op) :
    IsEssentiallyConstantInd A.op ∧
      ∃ (n : J) (X : DerivedCategory 𝒜) (φ : A.obj n ⟶ X)
        (π : (Functor.const (Over n)).obj X ⟶ Over.forget n ⋙ A),
        π.app (Over.mk (𝟙 n)) ≫ φ = 𝟙 X ∧ Nonempty (IsLimit (Cone.mk X π)) ∧
        ∀ i : ℤ, Nonempty (IsLimit ((homologyFunctor 𝒜 i).mapCone (Cone.mk X π)))

Tag 0G3C, a lemma

Tag 0G3C in the Stacks Project.

CategoryTheory.Pretriangulated.exists_proInverse_mor₁_of_proZero_π₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/EssentiallyConstant.lean, line 1060.

Stacks 0G3C. Let T : J ⥤ Triangle 𝒟 be an inverse system of distinguished triangles A_j ⟶ B_j ⟶ C_j ⟶ A_j[1] in a pre-triangulated category, indexed by a cofiltered category J. If the inverse system (C_j) of third terms is pro-zero, i.e. every index admits an arrow along which the transition morphism of third terms vanishes, then the morphisms A_j ⟶ B_j determine an isomorphism of pro-objects between (A_j) and (B_j): for every index j there are an arrow f : k ⟶ j and a morphism s : B_k ⟶ A_j such that A_k ⟶ B_k ⟶ A_j is the transition morphism A_k ⟶ A_j and B_k ⟶ A_j ⟶ B_j is the transition morphism B_k ⟶ B_j.

public theorem exists_proInverse_mor₁_of_proZero_π₃ [IsCofiltered J]
    (T : J ⥤ Triangle D) (hT : ∀ j, T.obj j ∈ distTriang D)
    (h₃ : ∀ j : J, ∃ (k : J) (f : k ⟶ j), (T.map f).hom₃ = 0) (j : J) :
    ∃ (k : J) (f : k ⟶ j) (s : (T.obj k).obj₂ ⟶ (T.obj j).obj₁),
      (T.obj k).mor₁ ≫ s = (T.map f).hom₁ ∧ s ≫ (T.obj j).mor₁ = (T.map f).hom₂

Tag 0G3D, a lemma

Tag 0G3D in the Stacks Project.

DerivedCategory.exists_proInverse_of_proInverse_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/EssentiallyConstant.lean, line 1452.

Stacks 0G3D. Let α : A ⟶ B be an inverse system of maps A_j ⟶ B_j of the derived category of an abelian category, indexed by a cofiltered category J. Assume H^i(A_j) = 0 and H^i(B_j) = 0 for every j and every i outside an interval [a, b], and that for every i the maps H^i(A_j) ⟶ H^i(B_j) are an isomorphism of pro-objects of 𝒜, i.e. every index j admits an arrow f : k ⟶ j and a morphism H^i(B_k) ⟶ H^i(A_j) whose two round trips are the transition morphisms. Then the maps A_j ⟶ B_j determine an isomorphism of pro-objects between (A_j) and (B_j): for every index j there are an arrow f : k ⟶ j and a morphism s : B_k ⟶ A_j such that A_k ⟶ B_k ⟶ A_j is the transition morphism A_k ⟶ A_j and B_k ⟶ A_j ⟶ B_j is the transition morphism B_k ⟶ B_j.

public theorem exists_proInverse_of_proInverse_homology [IsCofiltered J]
    {A B : J ⥤ DerivedCategory 𝒜} (α : A ⟶ B) (a b : ℤ)
    (hA : ∀ i : ℤ, i < a ∨ b < i → ∀ j : J, IsZero ((homologyFunctor 𝒜 i).obj (A.obj j)))
    (hB : ∀ i : ℤ, i < a ∨ b < i → ∀ j : J, IsZero ((homologyFunctor 𝒜 i).obj (B.obj j)))
    (hH : ∀ (i : ℤ) (j : J), ∃ (k : J) (f : k ⟶ j)
      (s : (homologyFunctor 𝒜 i).obj (B.obj k) ⟶ (homologyFunctor 𝒜 i).obj (A.obj j)),
      (homologyFunctor 𝒜 i).map (α.app k) ≫ s = (homologyFunctor 𝒜 i).map (A.map f) ∧
        s ≫ (homologyFunctor 𝒜 i).map (α.app j) = (homologyFunctor 𝒜 i).map (B.map f))
    (j : J) :
    ∃ (k : J) (f : k ⟶ j) (s : B.obj k ⟶ A.obj j),
      α.app k ≫ s = A.map f ∧ s ≫ α.app j = B.map f

Sources

LeanCategoryTheory.Pretriangulated.isEssentiallyConstant_op_iff_exists_iso_const_biprod · CategoryTheory.Pretriangulated.isEssentiallyConstant_op_π₂_and_exists_limit_triangle · DerivedCategory.isEssentiallyConstant_op_and_exists_limit_cone_of_homology · CategoryTheory.Pretriangulated.exists_proInverse_mor₁_of_proZero_π₃ · DerivedCategory.exists_proInverse_of_proInverse_homology

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

13.38 Brown representability to 13.42 Essentially constant…

Section13.38 Brown representability#

Tag 0A8F, a lemma

Tag 0A8G, a proposition

Sources

Section13.39 Brown representability, bis#

Tag 0GYG, a lemma

Tag 0GYH, a proposition

Sources

Section13.40 Admissible subcategories#

Tag 0CQQ, a lemma

Tag 0H0M, a lemma

Tag 0FXC, a lemma

Tag 0CQR, a lemma

Tag 0H0N, a lemma

Tag 0CQS, a lemma

Tag 0CQT, a lemma

Tag 0FXD, a definition

Tag 0H0P, a proposition

Sources

Section13.41 Postnikov systems#

Tag 0D7Z, a definition

Tag 0D81, a lemma

Tag 0D82, a lemma

Tag 0FXE, a lemma

Tag 0D83, a lemma

Sources

Section13.42 Essentially constant systems#

Tag 0G39, a lemma

Tag 0G3A, a lemma

Tag 0G3B, a lemma

Tag 0G3C, a lemma

Tag 0G3D, a lemma

Sources

Section13.38 Brown representability #

Section13.39 Brown representability, bis #

Section13.40 Admissible subcategories #

Section13.41 Postnikov systems #

Section13.42 Essentially constant systems #