14.5. Deformation: FiniteLengthHN
14.5.1. hn_exists_in_thin_interval_of_quotientLowerBound
Given a thin finite-length interval \mathcal{P}((a,b)) and a nonzero interval object X, if every proper strict quotient of X has W-phase strictly greater than a given lower bound t, then X admits an HN filtration with \operatorname{ssf}-semistable factors whose phases all lie in (t, U). This is the faithful Bridgeland S7 recursion with the paper's G/H-style input exposed: the lower phase bound for quotients is propagated through the recursive kernel step to smaller strict subobjects.
Proof: By well-founded induction on the strict-subobject poset of X. If X is already W-semistable, a single-factor filtration suffices. Otherwise, extract a strict MDQ q : X \twoheadrightarrow B and its kernel K = \ker(q). Lift K to a strict subobject T < X, recurse on T with the MDQ phase \psi(B) as the new lower bound, then assemble the resulting filtration by appending B as the last factor.
theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.hn_exists_in_thin_interval_of_quotientLowerBound.{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] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) {a b : ℝ} {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a b} [Fact (a < b)] [Fact (b - a ≤ 1)] (hFiniteLength : CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b) (hW_interval : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) {L U : ℝ} (hWindow : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → L < ssf.wPhase F ∧ ssf.wPhase F < U) (hWidth : U - L < 1) {U_hom : ℝ} (hHom : ∀ {E F : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E.obj (ssf.wPhase E.obj) → CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf F.obj (ssf.wPhase F.obj) → ssf.wPhase F.obj < ssf.wPhase E.obj → ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0) (hDestabBound : ∀ {Y : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, ¬CategoryTheory.Limits.IsZero Y → ∀ {A : CategoryTheory.Subobject Y}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf (CategoryTheory.Subobject.underlying.obj A).obj (ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj) → CategoryTheory.IsStrictMono A.arrow → ssf.wPhase Y.obj < ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj → ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj < U_hom) (t : ℝ) (X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b) (hX : ¬CategoryTheory.Limits.IsZero X) : (∀ (A : CategoryTheory.Subobject X), A ≠ ⊤ → CategoryTheory.IsStrictMono A.arrow → t < ssf.wPhase (CategoryTheory.Limits.cokernel A.arrow).obj) → have Psem := fun ψ E => CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E ψ; ∃ G, ∀ (j : Fin G.n), t < G.φ j ∧ G.φ j < UCategoryTheory.Triangulated.SkewedStabilityFunction.hn_exists_in_thin_interval_of_quotientLowerBound.{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] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) {a b : ℝ} {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a b} [Fact (a < b)] [Fact (b - a ≤ 1)] (hFiniteLength : CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b) (hW_interval : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) {L U : ℝ} (hWindow : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → L < ssf.wPhase F ∧ ssf.wPhase F < U) (hWidth : U - L < 1) {U_hom : ℝ} (hHom : ∀ {E F : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E.obj (ssf.wPhase E.obj) → CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf F.obj (ssf.wPhase F.obj) → ssf.wPhase F.obj < ssf.wPhase E.obj → ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0) (hDestabBound : ∀ {Y : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, ¬CategoryTheory.Limits.IsZero Y → ∀ {A : CategoryTheory.Subobject Y}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf (CategoryTheory.Subobject.underlying.obj A).obj (ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj) → CategoryTheory.IsStrictMono A.arrow → ssf.wPhase Y.obj < ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj → ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj < U_hom) (t : ℝ) (X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b) (hX : ¬CategoryTheory.Limits.IsZero X) : (∀ (A : CategoryTheory.Subobject X), A ≠ ⊤ → CategoryTheory.IsStrictMono A.arrow → t < ssf.wPhase (CategoryTheory.Limits.cokernel A.arrow).obj) → have Psem := fun ψ E => CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E ψ; ∃ G, ∀ (j : Fin G.n), t < G.φ j ∧ G.φ j < U
Something wrong, better idea? Suggest a change
14.5.2. hn_exists_in_thin_interval
Every nonzero object in a thin finite-length interval \mathcal{P}((a,b)) admits an HN filtration with \operatorname{ssf}-semistable factors whose phases lie in (L, U), given a global W-phase window (L, U) of width < 1, Hom vanishing for semistable objects, and a destabilizing phase bound. This is the legacy interface to hn_exists_in_thin_interval_of_quotientLowerBound obtained by feeding in the global lower window bound L.
Proof: Derives the quotient lower bound from the global window: every proper strict quotient is nonzero, hence its W-phase is > L by the window hypothesis. Then delegates to hn_exists_in_thin_interval_of_quotientLowerBound.
theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.hn_exists_in_thin_interval.{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] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) {a b : ℝ} {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a b} [Fact (a < b)] [Fact (b - a ≤ 1)] (hFiniteLength : CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b) (hW_interval : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) {L U : ℝ} (hWindow : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → L < ssf.wPhase F ∧ ssf.wPhase F < U) (hWidth : U - L < 1) {U_hom : ℝ} (hHom : ∀ {E F : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E.obj (ssf.wPhase E.obj) → CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf F.obj (ssf.wPhase F.obj) → ssf.wPhase F.obj < ssf.wPhase E.obj → ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0) (hDestabBound : ∀ {Y : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, ¬CategoryTheory.Limits.IsZero Y → ∀ {A : CategoryTheory.Subobject Y}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf (CategoryTheory.Subobject.underlying.obj A).obj (ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj) → CategoryTheory.IsStrictMono A.arrow → ssf.wPhase Y.obj < ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj → ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj < U_hom) (X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b) (hX : ¬CategoryTheory.Limits.IsZero X) : have Psem := fun ψ E => CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E ψ; ∃ G, ∀ (j : Fin G.n), L < G.φ j ∧ G.φ j < UCategoryTheory.Triangulated.SkewedStabilityFunction.hn_exists_in_thin_interval.{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] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) {a b : ℝ} {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a b} [Fact (a < b)] [Fact (b - a ≤ 1)] (hFiniteLength : CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b) (hW_interval : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) {L U : ℝ} (hWindow : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → L < ssf.wPhase F ∧ ssf.wPhase F < U) (hWidth : U - L < 1) {U_hom : ℝ} (hHom : ∀ {E F : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E.obj (ssf.wPhase E.obj) → CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf F.obj (ssf.wPhase F.obj) → ssf.wPhase F.obj < ssf.wPhase E.obj → ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0) (hDestabBound : ∀ {Y : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, ¬CategoryTheory.Limits.IsZero Y → ∀ {A : CategoryTheory.Subobject Y}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf (CategoryTheory.Subobject.underlying.obj A).obj (ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj) → CategoryTheory.IsStrictMono A.arrow → ssf.wPhase Y.obj < ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj → ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj < U_hom) (X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b) (hX : ¬CategoryTheory.Limits.IsZero X) : have Psem := fun ψ E => CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E ψ; ∃ G, ∀ (j : Fin G.n), L < G.φ j ∧ G.φ j < U
Something wrong, better idea? Suggest a change
14.5.3. hn_exists_in_thin_interval_of_strictQuotientLowerBound
Quotient-form wrapper for the faithful S7 HN recursion: the lower phase bound is stated for nonzero strict quotients X \twoheadrightarrow B rather than cokernel subobjects. This is the interface closest to Bridgeland's classes G and H, converted internally to the kernel/cokernel subobject language used by the recursion.
Proof: Translates the strict-quotient lower bound into the cokernel-subobject language (each strict quotient corresponds to a cokernel of a strict mono), then delegates to hn_exists_in_thin_interval_of_quotientLowerBound.
theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.hn_exists_in_thin_interval_of_strictQuotientLowerBound.{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] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) {a b : ℝ} {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a b} [Fact (a < b)] [Fact (b - a ≤ 1)] (hFiniteLength : CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b) (hW_interval : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) {L U : ℝ} (hWindow : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → L < ssf.wPhase F ∧ ssf.wPhase F < U) (hWidth : U - L < 1) {U_hom : ℝ} (hHom : ∀ {E F : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E.obj (ssf.wPhase E.obj) → CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf F.obj (ssf.wPhase F.obj) → ssf.wPhase F.obj < ssf.wPhase E.obj → ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0) (hDestabBound : ∀ {Y : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, ¬CategoryTheory.Limits.IsZero Y → ∀ {A : CategoryTheory.Subobject Y}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf (CategoryTheory.Subobject.underlying.obj A).obj (ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj) → CategoryTheory.IsStrictMono A.arrow → ssf.wPhase Y.obj < ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj → ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj < U_hom) (t : ℝ) (X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b) (hX : ¬CategoryTheory.Limits.IsZero X) (hquot : ∀ {B : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b} (q : X ⟶ B), CategoryTheory.IsStrictEpi q → ¬CategoryTheory.Limits.IsZero B.obj → t < ssf.wPhase B.obj) : have Psem := fun ψ E => CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E ψ; ∃ G, ∀ (j : Fin G.n), t < G.φ j ∧ G.φ j < UCategoryTheory.Triangulated.SkewedStabilityFunction.hn_exists_in_thin_interval_of_strictQuotientLowerBound.{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] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) {a b : ℝ} {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a b} [Fact (a < b)] [Fact (b - a ≤ 1)] (hFiniteLength : CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b) (hW_interval : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) {L U : ℝ} (hWindow : ∀ {F : C}, CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b F → ¬CategoryTheory.Limits.IsZero F → L < ssf.wPhase F ∧ ssf.wPhase F < U) (hWidth : U - L < 1) {U_hom : ℝ} (hHom : ∀ {E F : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E.obj (ssf.wPhase E.obj) → CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf F.obj (ssf.wPhase F.obj) → ssf.wPhase F.obj < ssf.wPhase E.obj → ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0) (hDestabBound : ∀ {Y : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}, ¬CategoryTheory.Limits.IsZero Y → ∀ {A : CategoryTheory.Subobject Y}, CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf (CategoryTheory.Subobject.underlying.obj A).obj (ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj) → CategoryTheory.IsStrictMono A.arrow → ssf.wPhase Y.obj < ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj → ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj < U_hom) (t : ℝ) (X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b) (hX : ¬CategoryTheory.Limits.IsZero X) (hquot : ∀ {B : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b} (q : X ⟶ B), CategoryTheory.IsStrictEpi q → ¬CategoryTheory.Limits.IsZero B.obj → t < ssf.wPhase B.obj) : have Psem := fun ψ E => CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf E ψ; ∃ G, ∀ (j : Fin G.n), t < G.φ j ∧ G.φ j < U
Something wrong, better idea? Suggest a change
14.5.4. intervalProp_chain_of_postnikovTower
If all factors of a Postnikov tower lie in \mathcal{P}((a,b)), then every intermediate chain object of the tower also lies in \mathcal{P}((a,b)).
Proof: By induction on k: the base object is zero (hence in \mathcal{P}((a,b))), and each step applies intervalProp_of_triangle to the distinguished triangle connecting the k-th chain object, its successor, and the corresponding factor.
theorem
CategoryTheory.Triangulated.intervalProp_chain_of_postnikovTower.{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] (s : CategoryTheory.Triangulated.Slicing C) {E : C} {a b : ℝ} (P : CategoryTheory.Triangulated.PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), CategoryTheory.Triangulated.Slicing.intervalProp C s a b (P.factor i)) (k : ℕ) (hk : k ≤ P.n) : CategoryTheory.Triangulated.Slicing.intervalProp C s a b (P.chain.obj' k ⋯)CategoryTheory.Triangulated.intervalProp_chain_of_postnikovTower.{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] (s : CategoryTheory.Triangulated.Slicing C) {E : C} {a b : ℝ} (P : CategoryTheory.Triangulated.PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), CategoryTheory.Triangulated.Slicing.intervalProp C s a b (P.factor i)) (k : ℕ) (hk : k ≤ P.n) : CategoryTheory.Triangulated.Slicing.intervalProp C s a b (P.chain.obj' k ⋯)
Something wrong, better idea? Suggest a change
14.5.5. intervalProp_of_postnikovTower
If all factors of a Postnikov tower lie in \mathcal{P}((a,b)), then the total object also lies in \mathcal{P}((a,b)).
Proof: This follows immediately from intervalProp_chain_of_postnikovTower applied at the top of the tower, using the isomorphism between the top chain object and the total object.
theorem
CategoryTheory.Triangulated.intervalProp_of_postnikovTower.{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] (s : CategoryTheory.Triangulated.Slicing C) {E : C} {a b : ℝ} (P : CategoryTheory.Triangulated.PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), CategoryTheory.Triangulated.Slicing.intervalProp C s a b (P.factor i)) : CategoryTheory.Triangulated.Slicing.intervalProp C s a b ECategoryTheory.Triangulated.intervalProp_of_postnikovTower.{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] (s : CategoryTheory.Triangulated.Slicing C) {E : C} {a b : ℝ} (P : CategoryTheory.Triangulated.PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), CategoryTheory.Triangulated.Slicing.intervalProp C s a b (P.factor i)) : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E
Something wrong, better idea? Suggest a change
14.5.6. gtProp_of_postnikovTower
If all factors of a Postnikov tower have phases strictly greater than t (i.e., lie in \mathcal{P}(>t)), then the total object also lies in \mathcal{P}(>t).
Proof: By induction on the tower length: the base is the zero object (which trivially satisfies \mathcal{P}(>t)), and each extension step uses gtProp_of_triangle applied to the distinguished triangle at the next level.
theorem
CategoryTheory.Triangulated.gtProp_of_postnikovTower.{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] (s : CategoryTheory.Triangulated.Slicing C) {E : C} {t : ℝ} (P : CategoryTheory.Triangulated.PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), CategoryTheory.Triangulated.Slicing.gtProp C s t (P.factor i)) : CategoryTheory.Triangulated.Slicing.gtProp C s t ECategoryTheory.Triangulated.gtProp_of_postnikovTower.{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] (s : CategoryTheory.Triangulated.Slicing C) {E : C} {t : ℝ} (P : CategoryTheory.Triangulated.PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), CategoryTheory.Triangulated.Slicing.gtProp C s t (P.factor i)) : CategoryTheory.Triangulated.Slicing.gtProp C s t E
Something wrong, better idea? Suggest a change
14.5.7. ltProp_of_postnikovTower
If all factors of a Postnikov tower have phases strictly less than t (i.e., lie in \mathcal{P}(<t)), then the total object also lies in \mathcal{P}(<t).
Proof: By induction on the tower length, applying ltProp_of_triangle at each extension step, analogously to gtProp_of_postnikovTower.
theorem
CategoryTheory.Triangulated.ltProp_of_postnikovTower.{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] (s : CategoryTheory.Triangulated.Slicing C) {E : C} {t : ℝ} (P : CategoryTheory.Triangulated.PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), CategoryTheory.Triangulated.Slicing.ltProp C s t (P.factor i)) : CategoryTheory.Triangulated.Slicing.ltProp C s t ECategoryTheory.Triangulated.ltProp_of_postnikovTower.{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] (s : CategoryTheory.Triangulated.Slicing C) {E : C} {t : ℝ} (P : CategoryTheory.Triangulated.PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), CategoryTheory.Triangulated.Slicing.ltProp C s t (P.factor i)) : CategoryTheory.Triangulated.Slicing.ltProp C s t E
Something wrong, better idea? Suggest a change