Ambient weak Harder--Narasimhan filtrations from a bounded heart

This file extends weak HN filtrations from the heart of a bounded t-structure to every ambient object. The construction follows the canonical t-cohomological filtration. An object with amplitude [b, a] receives an HN tower whose phases lie in (-a, 1-b].

The key point is strict separation between adjacent cohomological degrees. A pure degree-a object has phases in (-a, 1-a], while the truncation below degree a has phases strictly above 1-a. The generic Postnikov-splicing operation can therefore concatenate their HN towers across the truncation triangle.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.HNFiltration.shiftWeakAmbient {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {W : WeakStabilityFunction t} {E : C} (F : HNFiltration C W.ambientPhasePredicate E) (a : ℤ) : HNFiltration C W.ambientPhasePredicate ((shiftFunctor C a).obj E)

Shift an HN filtration for an induced ambient weak phase family by an integer. This is the non-circular analogue of HNFiltration.shiftHN: it uses the shift law already proved directly for ambientPhasePredicate, before a slicing has been assembled.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.HNFiltration.shiftWeakAmbient_phase {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {W : WeakStabilityFunction t} {E : C} (F : HNFiltration C W.ambientPhasePredicate E) (a : ℤ) (j : Fin F.n) : (shiftWeakAmbient F a).φ j = F.φ j + ↑a

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientHN_exists_of_mem_heart_with_phase_bounds {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (hHN : W.HasHNProperty) (E : t.heart.FullSubcategory) : ∃ (F : HNFiltration C W.ambientPhasePredicate E.obj), ∀ (j : Fin F.n), F.φ j ∈ Set.Ioc 0 1

Heart-level HN existence supplies an ambient HN tower whose phases lie in the standard interval (0, 1]. Recording the bounds together with the tower avoids making later amplitude arguments depend on a particular choice.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientHN_exists_of_pure {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (hHN : W.HasHNProperty) {E : C} (a : ℤ) (hLE : t.IsLE E a) (hGE : t.IsGE E a) : ∃ (F : HNFiltration C W.ambientPhasePredicate E), (∀ (j : Fin F.n), -↑a < F.φ j) ∧ ∀ (j : Fin F.n), F.φ j ≤ 1 - ↑a

A pure object concentrated in t-degree a has an ambient weak HN tower with phases in (-a, 1-a].

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientHN_exists_of_width {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (hHN : W.HasHNProperty) (b : ℤ) (n : ℕ) (E : C) : t.IsLE E (b + ↑n) → t.IsGE E b → ∃ (F : HNFiltration C W.ambientPhasePredicate E), (∀ (j : Fin F.n), -(↑b + ↑n) < F.φ j) ∧ ∀ (j : Fin F.n), F.φ j ≤ 1 - ↑b

Objects whose t-cohomology is supported in degrees [b, b+n] admit an ambient weak HN tower with all phases in (-(b+n), 1-b]. The phase bounds are the induction invariant that makes successive truncation triangles strictly spliceable.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientHN_exists_of_bounded {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (hbounded : t.IsBounded) (hHN : W.HasHNProperty) (E : C) : Nonempty (HNFiltration C W.ambientPhasePredicate E)

A bounded t-structure and weak HN filtrations on its heart determine HN filtrations for the integer-normalized ambient weak phase family on every object.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientHN_of_bounded {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (hbounded : t.IsBounded) (hHN : W.HasHNProperty) (E : C) : Nonempty (HNFiltration C W.ambientPhasePredicate E)

Global form of ambientHN_exists_of_bounded.

Boundedness of a heart tilt

theorem CategoryTheory.Triangulated.WeakStabilityCondition.heartTorsionPair_tilt_isBounded {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : Tilting.HeartTorsionPair t) (hbounded : t.IsBounded) : P.tilt.IsBounded

A Happel--Reiten--Smalø tilt of a bounded t-structure is bounded. In the aisle convention used by HeartTorsionPair.tilt, an original amplitude interval [b, a] becomes the tilted interval [b, a+1].