Documentation

TauCeti.CategoryTheory.Exact.Resolution.OfChainComplex

Finite resolutions from bounded exact complexes #

A finite P-resolution of X in an exact category is recorded recursively, as a chain of conflations

K₁ ↪ Q₀ ↠ X,   K₂ ↪ Q₁ ↠ K₁,   …,   Kₙ ↪ Qₙ₋₁ ↠ Kₙ₋₁,

and TauCeti.ExactStructure.FiniteResolution.toChainComplex splices such a chain into a bounded augmented chain complex. This file goes the other way for the canonical exact structure of an abelian category. Let K be a chain complex with an augmentation ε : K₀ ⟶ X such that

0 = Kₙ₊₁ ⟶ Kₙ ⟶ ⋯ ⟶ K₁ ⟶ K₀ ⟶ X ⟶ 0

is exact and every Kᵢ with i ≤ n satisfies P. Cutting it at the kernels Zᵢ₊₁ = ker (Kᵢ ⟶ Zᵢ), starting from Z₀ = X, gives short exact sequences Zᵢ₊₁ ↪ Kᵢ ↠ Zᵢ, and Kₙ ⟶ Zₙ is an isomorphism, so Zₙ satisfies P once P is closed under isomorphisms. The result is a finite P-resolution of X of length n.

When K vanishes in all degrees above n, the complex of this resolution is isomorphic to K, compatibly with the augmentations, so passing from the complex to the recursive presentation loses nothing. Alternating sums along the resolution are alternating sums of the terms K₀, …, Kₙ.

Main definitions #

Main results #

Implementation notes #

The kernels Zᵢ are built by recursion from Z₀ = X, each together with the map Kᵢ ⟶ Zᵢ induced by the differential, so that no exactness is needed to define them. This recursion is reducible, so that Z₀ is X up to reducible unfolding and the resolution of Z₀ built below is literally a resolution of X for rw and simp. The resolution itself is assembled by a recursion on the number of remaining conflations, starting from the deep end Zₙ, as TauCeti.ExactStructure.FiniteResolution is. Only the exactness of the complex in degrees 0, …, n and the vanishing of Kₙ₊₁ are used; the terms above n + 1 are irrelevant to the construction.

References #

source
noncomputable def TauCeti.ExactStructure.FiniteResolution.ofChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} {K : ChainComplex C ℕ} {ε : K.X 0 ⟶ X} {hε : CategoryTheory.CategoryStruct.comp (K.d 1 0) ε = 0} {n : ℕ} (h₀ : { X₁ := K.X 1, X₂ := K.X 0, X₃ := X, f := K.d 1 0, g := ε, zero := hε }.Exact) (hK : ∀ i < n, { X₁ := K.X (i + 2), X₂ := K.X (i + 1), X₃ := K.X i, f := K.d (i + 2) (i + 1), g := K.d (i + 1) i, zero := ⋯ }.Exact) (hn : CategoryTheory.Limits.IsZero (K.X (n + 1))) [CategoryTheory.Epi ε] [P.IsClosedUnderIsomorphisms] (hP : ∀ i ≤ n, P (K.X i)) :
(abelian C).FiniteResolution P X

The finite resolution of a bounded exact augmented complex. If 0 ⟶ Kₙ ⟶ ⋯ ⟶ K₀ ⟶ X ⟶ 0 is exact, with Kₙ₊₁ = 0 and every Kᵢ for i ≤ n satisfying P, then cutting it at the kernels of its maps gives a finite P-resolution of X for the canonical exact structure, of length n.

Instances For
    source
    @[simp]
    theorem TauCeti.ExactStructure.FiniteResolution.length_ofChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} {K : ChainComplex C ℕ} {ε : K.X 0 ⟶ X} {hε : CategoryTheory.CategoryStruct.comp (K.d 1 0) ε = 0} {n : ℕ} (h₀ : { X₁ := K.X 1, X₂ := K.X 0, X₃ := X, f := K.d 1 0, g := ε, zero := hε }.Exact) (hK : ∀ i < n, { X₁ := K.X (i + 2), X₂ := K.X (i + 1), X₃ := K.X i, f := K.d (i + 2) (i + 1), g := K.d (i + 1) i, zero := ⋯ }.Exact) (hn : CategoryTheory.Limits.IsZero (K.X (n + 1))) [CategoryTheory.Epi ε] [P.IsClosedUnderIsomorphisms] (hP : ∀ i ≤ n, P (K.X i)) :
    (ofChainComplex h₀ hK hn hP).length = n

    The resolution of an exact augmented complex with Kₙ₊₁ = 0 has length n, the truncation degree; the terms of the complex above n + 1 play no role.

    source
    theorem TauCeti.ExactStructure.FiniteResolution.foldAlternating_ofChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} {K : ChainComplex C ℕ} {ε : K.X 0 ⟶ X} {hε : CategoryTheory.CategoryStruct.comp (K.d 1 0) ε = 0} {n : ℕ} (h₀ : { X₁ := K.X 1, X₂ := K.X 0, X₃ := X, f := K.d 1 0, g := ε, zero := hε }.Exact) (hK : ∀ i < n, { X₁ := K.X (i + 2), X₂ := K.X (i + 1), X₃ := K.X i, f := K.d (i + 2) (i + 1), g := K.d (i + 1) i, zero := ⋯ }.Exact) (hn : CategoryTheory.Limits.IsZero (K.X (n + 1))) [CategoryTheory.Epi ε] [P.IsClosedUnderIsomorphisms] (hP : ∀ i ≤ n, P (K.X i)) {A : Type u_1} [AddCommGroup A] (f : (Z : C) → P Z → A) (hf : ∀ {Y Z : C} (x : Y ≅ Z) (hY : P Y) (hZ : P Z), f Y hY = f Z hZ) :
    foldAlternating f (ofChainComplex h₀ hK hn hP) = ∑ i : Fin (n + 1), (-1) ^ ↑i • f (K.X ↑i) ⋯

    Alternating sums along the resolution of a bounded exact complex are the alternating sums f K₀ - f K₁ + ⋯ + (-1)ⁿ f Kₙ over the terms of the complex, for any f invariant under isomorphism.

    source
    noncomputable def TauCeti.ExactStructure.FiniteResolution.toChainComplexOfChainComplexIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} {K : ChainComplex C ℕ} {ε : K.X 0 ⟶ X} {hε : CategoryTheory.CategoryStruct.comp (K.d 1 0) ε = 0} {n : ℕ} (h₀ : { X₁ := K.X 1, X₂ := K.X 0, X₃ := X, f := K.d 1 0, g := ε, zero := hε }.Exact) (hK : ∀ i < n, { X₁ := K.X (i + 2), X₂ := K.X (i + 1), X₃ := K.X i, f := K.d (i + 2) (i + 1), g := K.d (i + 1) i, zero := ⋯ }.Exact) [CategoryTheory.Epi ε] [P.IsClosedUnderIsomorphisms] (hP : ∀ i ≤ n, P (K.X i)) (hzero : ∀ (i : ℕ), n < i → CategoryTheory.Limits.IsZero (K.X i)) :
    (ofChainComplex h₀ hK ⋯ hP).toChainComplex ≅ K

    The complex of the resolution of a bounded exact complex is that complex, when it vanishes in all degrees above the length: passing from the complex to the recursive presentation of the resolution loses nothing.

    Instances For
      source
      @[simp]
      theorem TauCeti.ExactStructure.FiniteResolution.toChainComplexOfChainComplexIso_hom_f_zero_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} {K : ChainComplex C ℕ} {ε : K.X 0 ⟶ X} {hε : CategoryTheory.CategoryStruct.comp (K.d 1 0) ε = 0} {n : ℕ} (h₀ : { X₁ := K.X 1, X₂ := K.X 0, X₃ := X, f := K.d 1 0, g := ε, zero := hε }.Exact) (hK : ∀ i < n, { X₁ := K.X (i + 2), X₂ := K.X (i + 1), X₃ := K.X i, f := K.d (i + 2) (i + 1), g := K.d (i + 1) i, zero := ⋯ }.Exact) [CategoryTheory.Epi ε] [P.IsClosedUnderIsomorphisms] (hP : ∀ i ≤ n, P (K.X i)) (hzero : ∀ (i : ℕ), n < i → CategoryTheory.Limits.IsZero (K.X i)) :
      CategoryTheory.CategoryStruct.comp ((toChainComplexOfChainComplexIso h₀ hK hP hzero).hom.f 0) ε = (ofChainComplex h₀ hK ⋯ hP).aug

      The identification of complexes carries the augmentation of the resolution to the augmentation ε of the complex.

      source
      @[simp]
      theorem TauCeti.ExactStructure.FiniteResolution.toChainComplexOfChainComplexIso_hom_f_zero_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} {K : ChainComplex C ℕ} {ε : K.X 0 ⟶ X} {hε : CategoryTheory.CategoryStruct.comp (K.d 1 0) ε = 0} {n : ℕ} (h₀ : { X₁ := K.X 1, X₂ := K.X 0, X₃ := X, f := K.d 1 0, g := ε, zero := hε }.Exact) (hK : ∀ i < n, { X₁ := K.X (i + 2), X₂ := K.X (i + 1), X₃ := K.X i, f := K.d (i + 2) (i + 1), g := K.d (i + 1) i, zero := ⋯ }.Exact) [CategoryTheory.Epi ε] [P.IsClosedUnderIsomorphisms] (hP : ∀ i ≤ n, P (K.X i)) (hzero : ∀ (i : ℕ), n < i → CategoryTheory.Limits.IsZero (K.X i)) {Z : C} (h : X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((toChainComplexOfChainComplexIso h₀ hK hP hzero).hom.f 0) (CategoryTheory.CategoryStruct.comp ε h) = CategoryTheory.CategoryStruct.comp (ofChainComplex h₀ hK ⋯ hP).aug h

      The identification of complexes carries the augmentation of the resolution to the augmentation ε of the complex.