Mapping telescopes in triangulated categories #
This file supplies the first missing categorical ingredient in the Brown-style construction behind Theorem A.13 of arXiv:2607.28411v1. For a sequence
X₀ ⟶ X₁ ⟶ X₂ ⟶ ⋯,
its mapping telescope is the cone of 1 - shift on the countable coproduct of
the Xₙ. The construction is deliberately triangulated rather than derived:
it only uses a countable coproduct and the axiom completing a morphism to a
distinguished triangle.
The compact-source theorems below prove the two sequential-colimit properties needed when the Brown approximation tower is assembled: every map into the telescope factors through a finite stage, and equality in the telescope is witnessed at a finite later stage. They do not assert Brown representability.
noncomputable def
CategoryTheory.Triangulated.MappingTelescope.shiftMap
{C : Type u}
[Category.{v, u} C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
:
The endomorphism of the countable coproduct induced by the transition maps of a sequence.
Equations
- CategoryTheory.Triangulated.MappingTelescope.shiftMap X f = CategoryTheory.Limits.Sigma.desc fun (n : ℕ) => CategoryTheory.CategoryStruct.comp (f n) (CategoryTheory.Limits.Sigma.ι X (n + 1))
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.MappingTelescope.ι_shiftMap
{C : Type u}
[Category.{v, u} C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
(n : ℕ)
:
CategoryStruct.comp (Limits.Sigma.ι X n) (shiftMap X f) = CategoryStruct.comp (f n) (Limits.Sigma.ι X (n + 1))
@[simp]
theorem
CategoryTheory.Triangulated.MappingTelescope.ι_shiftMap_assoc
{C : Type u}
[Category.{v, u} C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
(n : ℕ)
{Z : C}
(h : ∐ X ⟶ Z)
:
CategoryStruct.comp (Limits.Sigma.ι X n) (CategoryStruct.comp (shiftMap X f) h) = CategoryStruct.comp (f n) (CategoryStruct.comp (Limits.Sigma.ι X (n + 1)) h)
noncomputable def
CategoryTheory.Triangulated.MappingTelescope.map
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
:
The morphism whose cone defines the mapping telescope.
Equations
Instances For
theorem
CategoryTheory.Triangulated.MappingTelescope.ι_map
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
(n : ℕ)
:
CategoryStruct.comp (Limits.Sigma.ι X n) (map X f) = Limits.Sigma.ι X n - CategoryStruct.comp (f n) (Limits.Sigma.ι X (n + 1))
theorem
CategoryTheory.Triangulated.MappingTelescope.ι_map_assoc
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
(n : ℕ)
{Z : C}
(h : ∐ X ⟶ Z)
:
CategoryStruct.comp (Limits.Sigma.ι X n) (CategoryStruct.comp (map X f) h) = CategoryStruct.comp (Limits.Sigma.ι X n - CategoryStruct.comp (f n) (Limits.Sigma.ι X (n + 1))) h
noncomputable def
CategoryTheory.Triangulated.MappingTelescope.projection
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
[Limits.HasCoproduct X]
(n : ℕ)
:
The projection from a coproduct onto one summand, using zero maps on all other summands.
Equations
- CategoryTheory.Triangulated.MappingTelescope.projection X n = CategoryTheory.Limits.Sigma.desc fun (i : ℕ) => if h : i = n then CategoryTheory.eqToHom ⋯ else 0
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.MappingTelescope.ι_projection
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
[Limits.HasCoproduct X]
(i n : ℕ)
:
theorem
CategoryTheory.Triangulated.MappingTelescope.ι_projection_self
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
[Limits.HasCoproduct X]
(n : ℕ)
:
theorem
CategoryTheory.Triangulated.MappingTelescope.shiftMap_projection_zero
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
:
theorem
CategoryTheory.Triangulated.MappingTelescope.shiftMap_projection_succ
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
(n : ℕ)
:
CategoryStruct.comp (shiftMap X f) (projection X (n + 1)) = CategoryStruct.comp (projection X n) (f n)
theorem
CategoryTheory.Triangulated.MappingTelescope.map_projection_zero
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
:
theorem
CategoryTheory.Triangulated.MappingTelescope.map_projection_succ
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
(n : ℕ)
:
CategoryStruct.comp (map X f) (projection X (n + 1)) = projection X (n + 1) - CategoryStruct.comp (projection X n) (f n)
theorem
CategoryTheory.Triangulated.MappingTelescope.comp_projection_eq_zero_of_comp_map_eq_zero
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
{K : C}
(a : K ⟶ ∐ X)
(ha : CategoryStruct.comp a (map X f) = 0)
(n : ℕ)
:
theorem
CategoryTheory.Triangulated.MappingTelescope.eq_zero_of_comp_map_eq_zero
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
{K : C}
(hK : IsCompactObject K)
(a : K ⟶ ∐ X)
(ha : CategoryStruct.comp a (map X f) = 0)
:
theorem
CategoryTheory.Triangulated.MappingTelescope.hom_map_injective
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
{K : C}
(hK : IsCompactObject K)
:
Function.Injective fun (a : K ⟶ ∐ X) => CategoryStruct.comp a (map X f)
The 1 - shift map is injective on morphisms from a compact object.
noncomputable def
CategoryTheory.Triangulated.MappingTelescope.transition
{C : Type u}
[Category.{v, u} C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
(i j : ℕ)
(h : i ≤ j)
:
The composite transition map between two stages of the sequence.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.MappingTelescope.transition_self
{C : Type u}
[Category.{v, u} C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
(i : ℕ)
:
theorem
CategoryTheory.Triangulated.MappingTelescope.transition_succ
{C : Type u}
[Category.{v, u} C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
(i j : ℕ)
(hij : i ≤ j)
:
structure
CategoryTheory.Triangulated.MappingTelescope.Data
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
:
Type (max u v)
A mapping telescope for a sequence, presented as a chosen distinguished
cone of 1 - shift. Different choices are noncanonically isomorphic; the
Brown construction only uses the distinguished-triangle interface.
- obj : C
The telescope object.
The coproduct-to-telescope morphism.
The connecting morphism.
- distinguished : Pretriangulated.Triangle.mk (map X f) self.hom self.connecting ∈ Pretriangulated.distinguishedTriangles
The defining triangle is distinguished.
Instances For
noncomputable def
CategoryTheory.Triangulated.MappingTelescope.chosen
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(X : ℕ → C)
(f : (n : ℕ) → X n ⟶ X (n + 1))
[Limits.HasCoproduct X]
:
Data X f
Every sequence with a countable coproduct admits a mapping telescope.
Equations
Instances For
theorem
CategoryTheory.Triangulated.MappingTelescope.Data.exists_desc
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{X : ℕ → C}
{f : (n : ℕ) → X n ⟶ X (n + 1)}
[Limits.HasCoproduct X]
(T : Data X f)
{Z : C}
(g : (n : ℕ) → X n ⟶ Z)
(hcompat : ∀ (n : ℕ), CategoryStruct.comp (f n) (g (n + 1)) = g n)
:
∃ (k : T.obj ⟶ Z), Limits.Sigma.desc g = CategoryStruct.comp T.hom k
Compatible maps out of a sequence factor through its mapping telescope.
This is the Hom(-, Z) exactness statement for the distinguished triangle
defining the telescope.
theorem
CategoryTheory.Triangulated.MappingTelescope.Data.exists_desc_comp_ι
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{X : ℕ → C}
{f : (n : ℕ) → X n ⟶ X (n + 1)}
[Limits.HasCoproduct X]
(T : Data X f)
{Z : C}
(g : (n : ℕ) → X n ⟶ Z)
(hcompat : ∀ (n : ℕ), CategoryStruct.comp (f n) (g (n + 1)) = g n)
:
∃ (k : T.obj ⟶ Z), ∀ (n : ℕ), CategoryStruct.comp (Limits.Sigma.ι X n) (CategoryStruct.comp T.hom k) = g n
The factorization through a telescope restricts to the original compatible family on each coproduct summand.
noncomputable def
CategoryTheory.Triangulated.MappingTelescope.Data.inclusion
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{X : ℕ → C}
{f : (n : ℕ) → X n ⟶ X (n + 1)}
[Limits.HasCoproduct X]
(T : Data X f)
(n : ℕ)
:
The canonical map from a stage into the mapping telescope.
Equations
Instances For
theorem
CategoryTheory.Triangulated.MappingTelescope.Data.f_comp_inclusion
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{X : ℕ → C}
{f : (n : ℕ) → X n ⟶ X (n + 1)}
[Limits.HasCoproduct X]
(T : Data X f)
(n : ℕ)
:
theorem
CategoryTheory.Triangulated.MappingTelescope.Data.transition_comp_inclusion
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{X : ℕ → C}
{f : (n : ℕ) → X n ⟶ X (n + 1)}
[Limits.HasCoproduct X]
(T : Data X f)
(i j : ℕ)
(hij : i ≤ j)
:
theorem
CategoryTheory.Triangulated.MappingTelescope.Data.comp_connecting_eq_zero
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{X : ℕ → C}
{f : (n : ℕ) → X n ⟶ X (n + 1)}
[Limits.HasCoproduct X]
{K : C}
(hK : IsCompactObject K)
(T : Data X f)
(a : K ⟶ T.obj)
:
A compact source has zero composite with the connecting morphism of a mapping telescope.
theorem
CategoryTheory.Triangulated.MappingTelescope.Data.exists_lift_coproduct
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{X : ℕ → C}
{f : (n : ℕ) → X n ⟶ X (n + 1)}
[Limits.HasCoproduct X]
{K : C}
(hK : IsCompactObject K)
(T : Data X f)
(a : K ⟶ T.obj)
:
∃ (b : K ⟶ ∐ X), a = CategoryStruct.comp b T.hom
A map from a compact object into a telescope lifts to the defining coproduct.
theorem
CategoryTheory.Triangulated.MappingTelescope.Data.exists_factor_stage
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{X : ℕ → C}
{f : (n : ℕ) → X n ⟶ X (n + 1)}
[Limits.HasCoproduct X]
{K : C}
(hK : IsCompactObject K)
(T : Data X f)
(a : K ⟶ T.obj)
:
∃ (n : ℕ) (b : K ⟶ X n), a = CategoryStruct.comp b (T.inclusion n)
Every map from a compact object into the telescope factors through one finite stage of the sequence.
theorem
CategoryTheory.Triangulated.MappingTelescope.Data.exists_transition_comp_eq_zero
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{X : ℕ → C}
{f : (n : ℕ) → X n ⟶ X (n + 1)}
[Limits.HasCoproduct X]
{K : C}
(hK : IsCompactObject K)
(T : Data X f)
(n : ℕ)
(b : K ⟶ X n)
(hb : CategoryStruct.comp b (T.inclusion n) = 0)
:
∃ (m : ℕ) (hnm : n ≤ m), CategoryStruct.comp b (transition X f n m hnm) = 0
If a map from a compact object becomes zero in the telescope, then it is already killed by a finite transition map.
theorem
CategoryTheory.Triangulated.MappingTelescope.Data.exists_transition_comp_eq
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{X : ℕ → C}
{f : (n : ℕ) → X n ⟶ X (n + 1)}
[Limits.HasCoproduct X]
{K : C}
(hK : IsCompactObject K)
(T : Data X f)
(n : ℕ)
(a b : K ⟶ X n)
(hab : CategoryStruct.comp a (T.inclusion n) = CategoryStruct.comp b (T.inclusion n))
:
∃ (m : ℕ) (hnm : n ≤ m), CategoryStruct.comp a (transition X f n m hnm) = CategoryStruct.comp b (transition X f n m hnm)
Equality after mapping into the telescope is witnessed at a finite later stage.