7.2. IntervalCategory: FiniteLength🔗

7.2.1. toLeftHeart_additive🔗

The left heart embedding F_L : \mathcal{P}((a,b)) \to \mathcal{P}((a, a+1]) is an additive functor.

Proof: The functor acts as the identity on morphisms, so additivity is immediate.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_additive.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) (a b : ℝ)
  (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C s a b
      hab).Additive
CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_additive.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (a b : ℝ) (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
      C s a b hab).Additive

Something wrong, better idea? Suggest a change

7.2.2. toRightHeart_additive🔗

The right heart embedding F_R : \mathcal{P}((a,b)) \to \mathcal{P}([b-1, b)) is an additive functor.

Proof: The functor acts as the identity on morphisms, so additivity is immediate.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_additive.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) (a b : ℝ)
  (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart C s a b
      hab).Additive
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_additive.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (a b : ℝ) (hab : b - a ≤ 1) :
  (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart
      C s a b hab).Additive

Something wrong, better idea? Suggest a change

7.2.3. toLeftHeart_preservesKernel🔗

The left heart embedding F_L : \mathcal{P}((a,b)) \to \mathcal{P}((a, a+1]) preserves kernels.

Proof: The kernel of f in \mathcal{P}((a,b)) maps to the kernel of F_L(f) in the left heart via the comparison isomorphism toLeftHeartKernelIso. Transporting the limit cone through this isomorphism shows F_L preserves the kernel.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_preservesKernel.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (f : X ⟶ Y) :
  CategoryTheory.Limits.PreservesLimit
    (CategoryTheory.Limits.parallelPair f 0)
    (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C s a b
      ⋯)
CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_preservesKernel.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (f : X ⟶ Y) :
  CategoryTheory.Limits.PreservesLimit
    (CategoryTheory.Limits.parallelPair f
      0)
    (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
      C s a b ⋯)

Something wrong, better idea? Suggest a change

7.2.4. toRightHeart_preservesCokernel🔗

The right heart embedding F_R : \mathcal{P}((a,b)) \to \mathcal{P}([b-1, b)) preserves cokernels.

Proof: The cokernel of f in \mathcal{P}((a,b)) maps to the cokernel of F_R(f) in the right heart via the comparison isomorphism toRightHeartCokernelIso. Transporting the colimit cocone through this isomorphism shows F_R preserves the cokernel.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_preservesCokernel.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (f : X ⟶ Y) :
  CategoryTheory.Limits.PreservesColimit
    (CategoryTheory.Limits.parallelPair f 0)
    (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart C s a
      b ⋯)
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_preservesCokernel.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (f : X ⟶ Y) :
  CategoryTheory.Limits.PreservesColimit
    (CategoryTheory.Limits.parallelPair f
      0)
    (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart
      C s a b ⋯)

Something wrong, better idea? Suggest a change

7.2.5. intervalCat_hasBinaryBiproducts🔗

The thin interval category \mathcal{P}((a, b)) has binary biproducts.

Proof: Follows from having binary products (proved earlier) and the additive/preadditive structure.

theorem

CategoryTheory.Triangulated.Slicing.intervalCat_hasBinaryBiproducts.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] {a b : ℝ}
  (s : CategoryTheory.Triangulated.Slicing C) :
  CategoryTheory.Limits.HasBinaryBiproducts
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)
CategoryTheory.Triangulated.Slicing.intervalCat_hasBinaryBiproducts.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {a b : ℝ}
  (s :
    CategoryTheory.Triangulated.Slicing
      C) :
  CategoryTheory.Limits.HasBinaryBiproducts
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)

Something wrong, better idea? Suggest a change

7.2.6. intervalCat_hasEqualizers🔗

The thin interval category \mathcal{P}((a, b)) has equalizers.

Proof: In a preadditive category, equalizers follow from the existence of kernels.

theorem

CategoryTheory.Triangulated.Slicing.intervalCat_hasEqualizers.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)]
  (s : CategoryTheory.Triangulated.Slicing C) :
  CategoryTheory.Limits.HasEqualizers
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)
CategoryTheory.Triangulated.Slicing.intervalCat_hasEqualizers.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  (s :
    CategoryTheory.Triangulated.Slicing
      C) :
  CategoryTheory.Limits.HasEqualizers
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)

Something wrong, better idea? Suggest a change

7.2.7. intervalCat_hasCoequalizers🔗

The thin interval category \mathcal{P}((a, b)) has coequalizers.

Proof: In a preadditive category, coequalizers follow from the existence of cokernels.

theorem

CategoryTheory.Triangulated.Slicing.intervalCat_hasCoequalizers.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)]
  (s : CategoryTheory.Triangulated.Slicing C) :
  CategoryTheory.Limits.HasCoequalizers
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)
CategoryTheory.Triangulated.Slicing.intervalCat_hasCoequalizers.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  (s :
    CategoryTheory.Triangulated.Slicing
      C) :
  CategoryTheory.Limits.HasCoequalizers
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)

Something wrong, better idea? Suggest a change

7.2.8. intervalCat_hasFiniteCoproducts🔗

The thin interval category \mathcal{P}((a, b)) has finite coproducts.

Proof: Follows from having binary coproducts and an initial object.

theorem

CategoryTheory.Triangulated.Slicing.intervalCat_hasFiniteCoproducts.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] {a b : ℝ}
  (s : CategoryTheory.Triangulated.Slicing C) :
  CategoryTheory.Limits.HasFiniteCoproducts
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)
CategoryTheory.Triangulated.Slicing.intervalCat_hasFiniteCoproducts.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {a b : ℝ}
  (s :
    CategoryTheory.Triangulated.Slicing
      C) :
  CategoryTheory.Limits.HasFiniteCoproducts
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)

Something wrong, better idea? Suggest a change

7.2.9. intervalCat_hasPullbacks🔗

The thin interval category \mathcal{P}((a, b)) has pullbacks.

Proof: Follows from having binary products and equalizers.

theorem

CategoryTheory.Triangulated.Slicing.intervalCat_hasPullbacks.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)]
  (s : CategoryTheory.Triangulated.Slicing C) :
  CategoryTheory.Limits.HasPullbacks
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)
CategoryTheory.Triangulated.Slicing.intervalCat_hasPullbacks.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  (s :
    CategoryTheory.Triangulated.Slicing
      C) :
  CategoryTheory.Limits.HasPullbacks
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)

Something wrong, better idea? Suggest a change

7.2.10. intervalCat_hasPushouts🔗

The thin interval category \mathcal{P}((a, b)) has pushouts.

Proof: Follows from having binary coproducts and coequalizers.

theorem

CategoryTheory.Triangulated.Slicing.intervalCat_hasPushouts.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)]
  (s : CategoryTheory.Triangulated.Slicing C) :
  CategoryTheory.Limits.HasPushouts
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)
CategoryTheory.Triangulated.Slicing.intervalCat_hasPushouts.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  (s :
    CategoryTheory.Triangulated.Slicing
      C) :
  CategoryTheory.Limits.HasPushouts
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)

Something wrong, better idea? Suggest a change

7.2.11. toLeftHeart_preservesFiniteLimits🔗

The left heart embedding F_L : \mathcal{P}((a,b)) \to \mathcal{P}((a, a+1]) preserves all finite limits.

Proof: Since F_L is additive and preserves kernels, it preserves all finite limits by the general criterion for additive functors between preadditive categories.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_preservesFiniteLimits.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)] :
  CategoryTheory.Limits.PreservesFiniteLimits
    (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C s a b
      ⋯)
CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_preservesFiniteLimits.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)] :
  CategoryTheory.Limits.PreservesFiniteLimits
    (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
      C s a b ⋯)

Something wrong, better idea? Suggest a change

7.2.12. toRightHeart_preservesFiniteColimits🔗

The right heart embedding F_R : \mathcal{P}((a,b)) \to \mathcal{P}([b-1, b)) preserves all finite colimits.

Proof: Since F_R is additive and preserves cokernels, it preserves all finite colimits by the general criterion for additive functors between preadditive categories.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_preservesFiniteColimits.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)] :
  CategoryTheory.Limits.PreservesFiniteColimits
    (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart C s a
      b ⋯)
CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_preservesFiniteColimits.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)] :
  CategoryTheory.Limits.PreservesFiniteColimits
    (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart
      C s a b ⋯)

Something wrong, better idea? Suggest a change

7.2.13. finite_subobject_of_leftHeart🔗

Finite subobjects in the left heart transfer to finite subobjects in \mathcal{P}((a,b)): if F_L(X) has finitely many subobjects, then X has finitely many subobjects.

Proof: The left heart embedding is faithful and preserves monomorphisms (it preserves finite limits). Faithful functors that preserve monos reflect the finiteness of the subobject poset.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.finite_subobject_of_leftHeart.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (hX :
    Finite
      (CategoryTheory.Subobject
        ((CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C
              s a b ⋯).obj
          X))) :
  Finite (CategoryTheory.Subobject X)
CategoryTheory.Triangulated.Slicing.IntervalCat.finite_subobject_of_leftHeart.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (hX :
    Finite
      (CategoryTheory.Subobject
        ((CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
              C s a b ⋯).obj
          X))) :
  Finite (CategoryTheory.Subobject X)

Something wrong, better idea? Suggest a change

7.2.14. comp_strictEpi🔗

Strict epimorphisms in \mathcal{P}((a,b)) are closed under composition: if f and g are strict epimorphisms, then f \circ g is a strict epimorphism.

Proof: Both f and g map to epimorphisms in the left heart by epi_toLeftHeart_of_strictEpi. Their composition F_L(f \circ g) = F_L(f) \circ F_L(g) is therefore epi in the abelian heart. Then strictEpi_of_epi_toLeftHeart recovers strictness.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.comp_strictEpi.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y Z : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (f : X ⟶ Y) (g : Y ⟶ Z) (hf : CategoryTheory.IsStrictEpi f)
  (hg : CategoryTheory.IsStrictEpi g) :
  CategoryTheory.IsStrictEpi (CategoryTheory.CategoryStruct.comp f g)
CategoryTheory.Triangulated.Slicing.IntervalCat.comp_strictEpi.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y Z :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (f : X ⟶ Y) (g : Y ⟶ Z)
  (hf : CategoryTheory.IsStrictEpi f)
  (hg : CategoryTheory.IsStrictEpi g) :
  CategoryTheory.IsStrictEpi
    (CategoryTheory.CategoryStruct.comp f
      g)

Something wrong, better idea? Suggest a change

7.2.15. comp_strictMono🔗

Strict monomorphisms in \mathcal{P}((a,b)) are closed under composition: if f and g are strict monomorphisms, then f \circ g is a strict monomorphism.

Proof: Both f and g map to monomorphisms in the right heart by mono_toRightHeart_of_strictMono. Their composition F_R(f \circ g) = F_R(f) \circ F_R(g) is therefore mono in the abelian heart. Then strictMono_of_mono_toRightHeart recovers strictness.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.comp_strictMono.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y Z : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (f : X ⟶ Y) (g : Y ⟶ Z) (hf : CategoryTheory.IsStrictMono f)
  (hg : CategoryTheory.IsStrictMono g) :
  CategoryTheory.IsStrictMono (CategoryTheory.CategoryStruct.comp f g)
CategoryTheory.Triangulated.Slicing.IntervalCat.comp_strictMono.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y Z :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (f : X ⟶ Y) (g : Y ⟶ Z)
  (hf : CategoryTheory.IsStrictMono f)
  (hg : CategoryTheory.IsStrictMono g) :
  CategoryTheory.IsStrictMono
    (CategoryTheory.CategoryStruct.comp f
      g)

Something wrong, better idea? Suggest a change

7.2.16. intervalCat_quasiAbelian🔗

The thin interval category \mathcal{P}((a, b)) with a < b and b - a \le 1 is quasi-abelian.

Proof: The two quasi-abelian axioms are: (1) pullbacks of strict epimorphisms are strict epi, and (2) pushouts of strict monomorphisms are strict mono. For (1): a strict epi g maps to an epi in the left heart; the left heart is abelian, so the pullback of an epi is epi; the left heart embedding preserves pullbacks (it preserves finite limits); reflecting back gives a strict epi. For (2): dual argument using the right heart and pushouts.

theorem

CategoryTheory.Triangulated.Slicing.intervalCat_quasiAbelian.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)] :
  CategoryTheory.QuasiAbelian
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)
CategoryTheory.Triangulated.Slicing.intervalCat_quasiAbelian.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)] :
  CategoryTheory.QuasiAbelian
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)

Something wrong, better idea? Suggest a change

7.2.17. IsLocallyFinite🔗

[Definition 5.7] per-object strict finite length is weaker than finite length of all chains (paper's assumption)

A slicing \mathcal{P} is locally finite if there exists \eta > 0 with \eta < 1/2 such that every object in each thin interval category \mathcal{P}((t - \eta, t + \eta)) has finite length in the quasi-abelian sense (i.e., satisfies both ACC and DCC on strict subobjects).

Construction: The structure witnesses \eta, the positivity bound, the normalization \eta < 1/2 (ensuring width 2\eta \le 1 for the quasi-abelian structure), and for each center t \in \mathbb{R}, the strict Artinian and strict Noetherian conditions on every object.

structure

CategoryTheory.Triangulated.Slicing.IsLocallyFinite.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) : Prop
CategoryTheory.Triangulated.Slicing.IsLocallyFinite.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing
      C) :
  Prop

Constructor

CategoryTheory.Triangulated.Slicing.IsLocallyFinite.mk.{v, u}

Fields

intervalFinite : ∃ η,
  ∃ (hη : 0 < η) (hη' : η < 1 / 2),
    ∀ (t : ℝ),
      let a := t - η;
      let b := t + η;
      ∀ (E : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b),
        CategoryTheory.IsStrictArtinianObject E ∧ CategoryTheory.IsStrictNoetherianObject E

Something wrong, better idea? Suggest a change

7.2.18. strictMono_strictEpi_of_shortExact_toLeftRightHearts🔗

If a short complex in \mathcal{P}((a,b)) is short exact in both the left heart \mathcal{P}((a, a+1]) and the right heart \mathcal{P}([b-1, b)), then its left map is a strict monomorphism and its right map is a strict epimorphism.

Proof: Short exactness in the right heart gives mono on f (reflecting through the right heart gives strict mono). Short exactness in the left heart gives epi on g (reflecting through the left heart gives strict epi).

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.strictMono_strictEpi_of_shortExact_toLeftRightHearts.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)}
  (hL :
    (S.map
        (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C s
          a b ⋯)).ShortExact)
  (hR :
    (S.map
        (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart C
          s a b ⋯)).ShortExact) :
  CategoryTheory.IsStrictMono S.f ∧ CategoryTheory.IsStrictEpi S.g
CategoryTheory.Triangulated.Slicing.IntervalCat.strictMono_strictEpi_of_shortExact_toLeftRightHearts.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b)}
  (hL :
    (S.map
        (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
          C s a b ⋯)).ShortExact)
  (hR :
    (S.map
        (CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart
          C s a b ⋯)).ShortExact) :
  CategoryTheory.IsStrictMono S.f ∧
    CategoryTheory.IsStrictEpi S.g

Something wrong, better idea? Suggest a change

7.2.19. strictMono_strictEpi_of_distTriang🔗

A distinguished triangle in \mathcal{C} whose three vertices lie in \mathcal{P}((a,b)) forces the first map to be a strict monomorphism and the second to be a strict epimorphism in \mathcal{P}((a,b)).

Proof: The triangle lifts to short exact sequences in both hearts via the abelian subcategory theory. Apply strictMono_strictEpi_of_shortExact_toLeftRightHearts.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.strictMono_strictEpi_of_distTriang.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)}
  {δ : S.X₃.obj ⟶ (CategoryTheory.shiftFunctor C 1).obj S.X₁.obj}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.IsStrictMono S.f ∧ CategoryTheory.IsStrictEpi S.g
CategoryTheory.Triangulated.Slicing.IntervalCat.strictMono_strictEpi_of_distTriang.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b)}
  {δ :
    S.X₃.obj ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        S.X₁.obj}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        S.f.hom S.g.hom δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.IsStrictMono S.f ∧
    CategoryTheory.IsStrictEpi S.g

Something wrong, better idea? Suggest a change

7.2.20. exists_distTriang_of_shortExact_toLeftHeart🔗

A short exact sequence in the left heart \mathcal{P}((a,a+1]) with vertices in \mathcal{P}((a,b)) extends to a distinguished triangle in \mathcal{C}.

Proof: In the abelian heart, the epi g lifts to a distinguished triangle via the admissible subcategory structure. The kernel comparison isomorphism identifies the first vertex with S.X_1, giving a distinguished triangle on the original objects.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.exists_distTriang_of_shortExact_toLeftHeart.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (b - a ≤ 1)]
  (s : CategoryTheory.Triangulated.Slicing C)
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)}
  (hL :
    (S.map
        (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C s
          a b ⋯)).ShortExact) :
  ∃ δ,
    CategoryTheory.Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles
CategoryTheory.Triangulated.Slicing.IntervalCat.exists_distTriang_of_shortExact_toLeftHeart.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (b - a ≤ 1)]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b)}
  (hL :
    (S.map
        (CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
          C s a b ⋯)).ShortExact) :
  ∃ δ,
    CategoryTheory.Pretriangulated.Triangle.mk
        S.f.hom S.g.hom δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles

Something wrong, better idea? Suggest a change

7.2.21. exists_distTriang_of_strictShortExact🔗

A strict short exact sequence in \mathcal{P}((a,b)) extends to a distinguished triangle in \mathcal{C}.

Proof: The strict mono S.f maps to a mono in the right heart, and the strict epi S.g maps to an epi in the left heart. The homology data from the strict short exact sequence gives a short exact sequence in the left heart, from which exists_distTriang_of_shortExact_toLeftHeart produces the distinguished triangle.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.exists_distTriang_of_strictShortExact.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)}
  (hS : CategoryTheory.StrictShortExact S) :
  ∃ δ,
    CategoryTheory.Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles
CategoryTheory.Triangulated.Slicing.IntervalCat.exists_distTriang_of_strictShortExact.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b)}
  (hS :
    CategoryTheory.StrictShortExact S) :
  ∃ δ,
    CategoryTheory.Pretriangulated.Triangle.mk
        S.f.hom S.g.hom δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles

Something wrong, better idea? Suggest a change

7.2.22. strictShortExact_of_distTriang🔗

A distinguished triangle in \mathcal{C} whose three vertices lie in \mathcal{P}((a,b)) defines a strict short exact sequence in \mathcal{P}((a,b)).

Proof: From strictMono_strictEpi_of_distTriang, the first map is strict mono and the second is strict epi. Exactness follows from the abelian heart SES: the triangle gives kernel and cokernel limit cones in both hearts, reflecting through the faithful embeddings yields exactness in \mathcal{P}((a,b)).

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.strictShortExact_of_distTriang.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)}
  {δ : S.X₃.obj ⟶ (CategoryTheory.shiftFunctor C 1).obj S.X₁.obj}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.StrictShortExact S
CategoryTheory.Triangulated.Slicing.IntervalCat.strictShortExact_of_distTriang.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b)}
  {δ :
    S.X₃.obj ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        S.X₁.obj}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        S.f.hom S.g.hom δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.StrictShortExact S

Something wrong, better idea? Suggest a change

7.2.23. strictShortExact_inclusion🔗

A strict short exact sequence in a smaller thin interval \mathcal{P}((a_1, b_1)) remains strict in any larger thin interval \mathcal{P}((a_2, b_2)) containing it.

Proof: Lift the strict SES to a distinguished triangle via exists_distTriang_of_strictShortExact. The triangle's vertices lie in the larger interval by intervalProp_mono. Apply strictShortExact_of_distTriang in the larger interval.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.strictShortExact_inclusion.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a₁ b₁ a₂ b₂ : ℝ}
  [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)] (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂)
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a₁ b₁)}
  (hS : CategoryTheory.StrictShortExact S) :
  CategoryTheory.StrictShortExact
    (S.map
      (CategoryTheory.Triangulated.Slicing.IntervalCat.inclusion C s ha
        hb))
CategoryTheory.Triangulated.Slicing.IntervalCat.strictShortExact_inclusion.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)]
  [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)] (ha : a₂ ≤ a₁)
  (hb : b₁ ≤ b₂)
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a₁ b₁)}
  (hS :
    CategoryTheory.StrictShortExact S) :
  CategoryTheory.StrictShortExact
    (S.map
      (CategoryTheory.Triangulated.Slicing.IntervalCat.inclusion
        C s ha hb))

Something wrong, better idea? Suggest a change

7.2.24. strictShortExact_iff_exists_distTriang🔗

Strict short exact sequences in \mathcal{P}((a,b)) are in bijection with distinguished triangles in \mathcal{C} whose three vertices lie in \mathcal{P}((a,b)).

Proof: Forward: exists_distTriang_of_strictShortExact. Backward: strictShortExact_of_distTriang.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.strictShortExact_iff_exists_distTriang.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)} :
  CategoryTheory.StrictShortExact S ↔
    ∃ δ,
      CategoryTheory.Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles
CategoryTheory.Triangulated.Slicing.IntervalCat.strictShortExact_iff_exists_distTriang.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b)} :
  CategoryTheory.StrictShortExact S ↔
    ∃ δ,
      CategoryTheory.Pretriangulated.Triangle.mk
          S.f.hom S.g.hom δ ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles

Something wrong, better idea? Suggest a change

7.2.25. K0_of_strictShortExact🔗

A strict short exact sequence X_1 \hookrightarrow X_2 \twoheadrightarrow X_3 in \mathcal{P}((a,b)) yields the K_0 relation [X_2] = [X_1] + [X_3] in the Grothendieck group of \mathcal{C}.

Proof: Lift the strict SES to a distinguished triangle in \mathcal{C}. The K_0 additivity on distinguished triangles gives the relation.

theorem

CategoryTheory.Triangulated.Slicing.IntervalCat.K0_of_strictShortExact.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)}
  (hS : CategoryTheory.StrictShortExact S) :
  CategoryTheory.Triangulated.K₀.of C S.X₂.obj =
    CategoryTheory.Triangulated.K₀.of C S.X₁.obj +
      CategoryTheory.Triangulated.K₀.of C S.X₃.obj
CategoryTheory.Triangulated.Slicing.IntervalCat.K0_of_strictShortExact.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b)}
  (hS :
    CategoryTheory.StrictShortExact S) :
  CategoryTheory.Triangulated.K₀.of C
      S.X₂.obj =
    CategoryTheory.Triangulated.K₀.of C
        S.X₁.obj +
      CategoryTheory.Triangulated.K₀.of C
        S.X₃.obj

Something wrong, better idea? Suggest a change

7.2.26. appendStrictFactor🔗

Append a semistable strict quotient in \mathcal{P}((a,b)) to an HN filtration of the kernel. Given an HN filtration G of S.X_1 and a strict short exact sequence S.X_1 \hookrightarrow S.X_2 \twoheadrightarrow S.X_3 with S.X_3 \in \mathcal{P}(\psi) and \psi below all phases of G, this produces an HN filtration of S.X_2.

Construction: Lifts the strict SES to a distinguished triangle and applies HNFiltration.appendFactor with identity isomorphisms.

def

CategoryTheory.Triangulated.HNFiltration.appendStrictFactor.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)}
  (G : CategoryTheory.Triangulated.HNFiltration C P S.X₁.obj)
  (hS : CategoryTheory.StrictShortExact S) (ψ : ℝ) (hψ : P ψ S.X₃.obj)
  (hψ_lt : ∀ (j : Fin G.n), ψ < G.φ j) :
  CategoryTheory.Triangulated.HNFiltration C P S.X₂.obj
CategoryTheory.Triangulated.HNFiltration.appendStrictFactor.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b)}
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C P S.X₁.obj)
  (hS : CategoryTheory.StrictShortExact S)
  (ψ : ℝ) (hψ : P ψ S.X₃.obj)
  (hψ_lt : ∀ (j : Fin G.n), ψ < G.φ j) :
  CategoryTheory.Triangulated.HNFiltration
    C P S.X₂.obj

Something wrong, better idea? Suggest a change

7.2.27. SkewedStabilityFunction🔗

[Definition 4.4] weaker: only σ-semistable nonvanishing, not all nonzero objects

A skewed stability function on a thin subcategory \mathcal{P}((a, b)) consists of a group homomorphism W : \Lambda \to \mathbb{C} (the charge), a class map v : K_0(\mathcal{C}) \to \Lambda, and a skewing parameter \alpha \in (a, b), such that W(v[E]) \ne 0 for every nonzero \sigma-semistable object E with phase in (a, b). In the deformation theorem, W is a perturbation of the central charge Z of a stability condition.

Construction: The structure bundles the homomorphism W, the parameter \alpha with its interval membership proof, and the non-vanishing condition on semistable objects.

structure

CategoryTheory.Triangulated.SkewedStabilityFunction.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ]
  (v : CategoryTheory.Triangulated.K₀ C →+ Λ)
  (s : CategoryTheory.Triangulated.Slicing C) (a b : ℝ) : Type u'
CategoryTheory.Triangulated.SkewedStabilityFunction.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  (v :
    CategoryTheory.Triangulated.K₀ C →+ Λ)
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (a b : ℝ) : Type u'

Constructor

CategoryTheory.Triangulated.SkewedStabilityFunction.mk.{v, u, u'}

Fields

W : Λ →+ ℂ

The group homomorphism (typically a perturbation of the central charge).

α : ℝ

The skewing parameter, lying in the interval (a, b).

hα_mem : a < self.α ∧ self.α < b

The skewing parameter lies in the interval.

nonzero : ∀ (E : C) (φ : ℝ),
  a < φ → φ < b → s.P φ E → ¬CategoryTheory.Limits.IsZero E → self.W (CategoryTheory.Triangulated.cl C v E) ≠ 0

For every nonzero semistable object of phase φ ∈ (a, b), the central charge W(v[E]) is nonzero.

Something wrong, better idea? Suggest a change

7.2.28. strict_additive🔗

The central charge of a skewed stability function is additive on strict short exact sequences: W(v[X_2]) = W(v[X_1]) + W(v[X_3]) for a strict SES X_1 \hookrightarrow X_2 \twoheadrightarrow X_3 in \mathcal{P}((a,b)).

Proof: The K_0 relation from K0_of_strictShortExact gives [X_2] = [X_1] + [X_3] in K_0(\mathcal{C}), and W \circ v is a group homomorphism, so it respects the sum.

theorem

CategoryTheory.Triangulated.SkewedStabilityFunction.strict_additive.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C] {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)] {s : CategoryTheory.Triangulated.Slicing C}
  (ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b)
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)}
  (hS : CategoryTheory.StrictShortExact S) :
  ssf.W (CategoryTheory.Triangulated.cl C v S.X₂.obj) =
    ssf.W (CategoryTheory.Triangulated.cl C v S.X₁.obj) +
      ssf.W (CategoryTheory.Triangulated.cl C v S.X₃.obj)
CategoryTheory.Triangulated.SkewedStabilityFunction.strict_additive.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b)
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b)}
  (hS :
    CategoryTheory.StrictShortExact S) :
  ssf.W
      (CategoryTheory.Triangulated.cl C v
        S.X₂.obj) =
    ssf.W
        (CategoryTheory.Triangulated.cl C
          v S.X₁.obj) +
      ssf.W
        (CategoryTheory.Triangulated.cl C
          v S.X₃.obj)

Something wrong, better idea? Suggest a change