Transporting strict finite length along functors

The reusable centrepiece of the third piece the Aut action on stability conditions needs.

CategoryTheory/Triangulated/QuasiAbelian.lean has a general transfer lemma, isStrictArtinianObject_of_fullFaithful_map_strictMono, for any full+faithful strict-mono-preserving functor — but it assumes ordinary IsArtinianObject of the image (DCC on all subobjects), which is strictly stronger than what Slicing.IsLocallyFinite supplies. A version assuming only strict finite length has to hand-roll a StrictSubobject order-embedding, and doing that per functor is what this file removes.

The argument is extracted here once, for an arbitrary functor; the interval inclusion lemma interval_thinFiniteLength_of_inclusion_strict below is an instance of it.

The extra hypothesis, and why it is unavoidable here

harr says the arrow of the subobject generated by a strict mono is again a strict mono. It cannot be dropped: proving it needs strict monos to be closed under composition (with Subobject.underlyingIso), and strict-mono composition is not available in general — it is proved only for interval categories (Slicing.IntervalCat.comp_strictMono, WeakStabilityCondition/StabilityCondition/Foundation/Slicing/IntervalStrictness.lean). Callers whose target is an interval category discharge harr with intervalSubobject_arrow_strictMono (WeakStabilityCondition/StabilityCondition/Foundation/Slicing/IntervalFiniteTransfer.lean).

Also here

mapEquiv_intervalProp_iff: under the Aut action the interval endpoints do not move — only the objects do. That is the structural difference from step 3c, where the endpoints moved and exists_radius was needed. It is why interval_thinFiniteLength_of_inclusion_strict below cannot be reused for Aut: it compares two intervalProps on the same object.

The general transfer

theorem CategoryTheory.Triangulated.isStrictArtinian_of_faithful_strict {A : Type u} [Category.{w, u} A] [Preadditive A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u} [Category.{w, u} D] [Preadditive D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) [F.Full] [F.Faithful] (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) (harr : ∀ {Y Z : D} (f : Y ⟶ Z) [inst : Mono f], IsStrictMono f → IsStrictMono (Subobject.mk f).arrow) {E : A} [IsStrictArtinianObject (F.obj E)] : IsStrictArtinianObject E

Strict-Artinian transfers, from a strict hypothesis. isStrictArtinianObject_of_fullFaithful_map_strictMono needs ordinary IsArtinianObject of the image; this needs only the strict version.

theorem CategoryTheory.Triangulated.isStrictNoetherian_of_faithful_strict {A : Type u} [Category.{w, u} A] [Preadditive A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u} [Category.{w, u} D] [Preadditive D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) [F.Full] [F.Faithful] (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) (harr : ∀ {Y Z : D} (f : Y ⟶ Z) [inst : Mono f], IsStrictMono f → IsStrictMono (Subobject.mk f).arrow) {E : A} [IsStrictNoetherianObject (F.obj E)] : IsStrictNoetherianObject E

Strict-Noetherian, the same route with the order reversed.

Strict finite length along inclusions of thin interval categories

theorem CategoryTheory.Triangulated.interval_thinFiniteLength_of_inclusion_strict {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {s₁ s₂ : Slicing C} {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)] [Fact (b₂ - a₂ ≤ 1)] (h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂) (hFinite : ∀ (Y : Slicing.IntervalCat C s₂ a₂ b₂), IsStrictArtinianObject Y ∧ IsStrictNoetherianObject Y) (X : Slicing.IntervalCat C s₁ a₁ b₁) : IsStrictArtinianObject X ∧ IsStrictNoetherianObject X

Strict Artinian and Noetherian conditions pull back from a containing thin interval.

theorem CategoryTheory.Triangulated.intervalInclusion_isAdmissibleSubobject {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {s₁ s₂ : Slicing C} {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)] [Fact (b₂ - a₂ ≤ 1)] (h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂) {E : Slicing.IntervalCat C s₁ a₁ b₁} (A : Subobject E) (hA : Slicing.IsAdmissibleSubobject C s₁ A) : Slicing.IsAdmissibleSubobject C s₂ (strictSubobjectImageOfFullFaithful (ObjectProperty.ιOfLE h) ⋯ ⟨A, ⋯⟩)

An admissible subobject stays admissible when its thin interval is included in another thin interval.

theorem CategoryTheory.Triangulated.interval_finiteLength_of_inclusion {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {s₁ s₂ : Slicing C} {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)] [Fact (b₂ - a₂ ≤ 1)] (h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂) (hFinite : ∀ (Y : Slicing.IntervalCat C s₂ a₂ b₂), Slicing.IsFiniteLength C s₂ Y) (X : Slicing.IntervalCat C s₁ a₁ b₁) : Slicing.IsFiniteLength C s₁ X

Intrinsic admissible finite length pulls back along an inclusion of thin interval categories.

Interval properties under the Aut action

theorem CategoryTheory.Triangulated.mapEquiv_intervalProp_iff {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ : C ≌ C) [Φ.functor.Additive] [Φ.inverse.Additive] [Φ.functor.CommShift ℤ] [Φ.inverse.CommShift ℤ] [Φ.functor.IsTriangulated] [Φ.inverse.IsTriangulated] (s : Slicing C) (a b : ℝ) (E : C) : Slicing.intervalProp C (s.mapEquiv Φ) a b E ↔ Slicing.intervalProp C s a b (Φ.inverse.obj E)

The endpoints do not move. An autoequivalence relabels objects, so E lies in the (a, b) window of Φ • s exactly when Φ⁻¹ E lies in the same (a, b) window of s.

Contrast relabel_intervalProp, where phase relabelling moves the endpoints and requires a uniform-continuity argument.