Local finiteness under transfer, and transfer of stability conditions

Bridgeland's stability conditions are the locally finite pre-stability conditions. This file shows that local finiteness survives transfer along a phase-detecting functor, and therefore upgrades PreStabilityCondition.WithClassMap.preimage to StabilityCondition.WithClassMap.preimage.

Main definitions

• Slicing.PreimageData.intervalFunctor: the detecting functor restricted to a thin phase window, the carrier of the whole finite-length argument.
• Slicing.PreimageData.strictImage: the induced map on strict subobjects, an instance of the Foundation-level strictImage.
• StabilityCondition.WithClassMap.preimage: the transported stability condition, with its source-facing names pullback and pushforward.

Main results

• Slicing.PreimageData.reflectsIsomorphisms: a functor carrying slicing-lifting data reflects isomorphisms. The cone of a morphism is killed by the functor exactly when the morphism becomes invertible, and the functor reflects zero objects.
• Slicing.preimage_intervalProp_iff: thin-interval membership for the preimage slicing is detected by the functor, because both extreme phases are.
• Slicing.PreimageData.strictImage_strictMono: the image map on strict subobjects is strictly monotone, without fullness or faithfulness.
• Slicing.PreimageData.isLocallyFinite: the preimage of a locally finite slicing is locally finite, with the same radius.

Implementation notes

The proof follows mapEquiv_isLocallyFinite in Symmetry/Autoequivalence/Stability/Transport.lean, with one genuine difference. There the functor was an equivalence, so the image map on strict subobjects was injective by fullness (strictImage_injective). A phase-detecting functor need not be full or faithful, so injectivity is replaced by the argument that a strictly smaller subobject stays strictly smaller: if the images of B₁ < B₂ agreed, the comparison B₁ ⟶ B₂ would become invertible, and a functor that reflects isomorphisms would make it invertible already, contradicting B₁ ≠ B₂. This is exactly the place where the Hom-vanishing half of Slicing.PreimageData is used, through reflectsZeroObjects. The image map itself and its monotonicity are the Foundation-level strictImage and strictImage_monotone, which need only preservation of strict monos; the well-foundedness transfer is isStrictArtinianObject_of_strictMono and its Noetherian twin.

The image map is built on strict subobjects rather than on the intrinsic admissible subobjects. The two orders agree in a thin interval by admissibleStrictSubobjectOrderIso, and strict subobjects are the ones for which the functor's action on canonical arrows is available.

References

• arXiv:2607.28411v1, Remarks 3.2 and 3.7, which take conservativity as an input; here it is derived.

theorem CategoryTheory.Triangulated.Slicing.preimage_intervalProp_iff {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (s : Slicing D) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) (a b : ℝ) (E : C) : intervalProp C (s.preimage F h) a b E ↔ intervalProp D s a b (F.obj E)

Thin-interval membership for the preimage slicing is detected by the functor: both extreme phases are computed on the image (Slicing.preimage_phiPlus, Slicing.preimage_phiMinus), and zero objects are reflected by the lifting witness. The direct analogue of Slicing.preimage_ltProp_iff for the two-sided window.

Reflecting isomorphisms

theorem CategoryTheory.Triangulated.Slicing.PreimageData.reflectsIsomorphisms {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {s : Slicing D} {F : Functor C D} [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) : F.ReflectsIsomorphisms

A functor carrying slicing-lifting data reflects isomorphisms. Complete f to a distinguished triangle; its image is distinguished with first map F.map f, so the image of the cone is zero, so the cone is zero by reflectsZeroObjects, so f is an isomorphism.

Thin intervals

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.PreimageData.intervalFunctor {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {s : Slicing D} {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) (a b : ℝ) : Functor (IntervalCat C (s.preimage F h) a b) (IntervalCat D s a b)

The detecting functor restricted to a thin interval of the preimage slicing, landing in the same thin interval of the target slicing.

An abbrev, as autIntervalFunctor is, so that instance search sees the underlying ObjectProperty.lift.

Equations

• h.intervalFunctor a b = (CategoryTheory.Triangulated.Slicing.intervalProp D s a b).lift ((CategoryTheory.Triangulated.Slicing.intervalProp C (s.preimage F h) a b).ι.comp F) ⋯

theorem CategoryTheory.Triangulated.Slicing.PreimageData.intervalFunctor_map_strictMono {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {s : Slicing D} {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) [IsTriangulated C] [IsTriangulated D] (a b : ℝ) [Fact (a < b)] [Fact (b - a ≤ 1)] {X Y : IntervalCat C (s.preimage F h) a b} (f : X ⟶ Y) (hf : IsStrictMono f) : IsStrictMono ((h.intervalFunctor a b).map f)

The restricted functor preserves strict monomorphisms, by the cone route: a strict mono and its cokernel extend to an ambient distinguished triangle, the functor keeps it distinguished with all three vertices in the target interval, and a distinguished triangle on a thin interval is a strict short exact sequence there.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.Slicing.PreimageData.strictImage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {s : Slicing D} {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) [IsTriangulated C] [IsTriangulated D] (a b : ℝ) [Fact (a < b)] [Fact (b - a ≤ 1)] {E : IntervalCat C (s.preimage F h) a b} : StrictSubobject E → StrictSubobject ((h.intervalFunctor a b).obj E)

The image of a strict subobject under the restricted functor, taken as a strict subobject rather than a bare Subobject: intervalFunctor_map_strictMono is what makes the canonical representative arrow strict, and strictness is what the finite-length orders are stated about. This is the Foundation-level strictImage at the restricted functor, so strictImage_monotone applies verbatim. Unlike strictSubobjectImageOfFullFaithful, this map is not injective in general, since the detecting functor need not be faithful; that is why strictImage_strictMono below goes through reflection of isomorphisms instead.

Equations

• h.strictImage a b = CategoryTheory.Triangulated.strictImage (h.intervalFunctor a b) ⋯ ⋯

theorem CategoryTheory.Triangulated.Slicing.PreimageData.strictImage_strictMono {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {s : Slicing D} {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) [IsTriangulated C] [IsTriangulated D] (a b : ℝ) [Fact (a < b)] [Fact (b - a ≤ 1)] {E : IntervalCat C (s.preimage F h) a b} : StrictMono (h.strictImage a b)

The image map on strict subobjects is strictly monotone. Monotonicity gives ≤; if the images of B₁ < B₂ were equal, the comparison morphism B₁ ⟶ B₂ would map to an isomorphism, hence be an isomorphism because the functor reflects them, hence identify B₁ with B₂.

theorem CategoryTheory.Triangulated.Slicing.PreimageData.isStrictFiniteLengthObject_of_intervalFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {s : Slicing D} {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) [IsTriangulated C] [IsTriangulated D] (a b : ℝ) [Fact (a < b)] [Fact (b - a ≤ 1)] {E : IntervalCat C (s.preimage F h) a b} (hE : IsStrictFiniteLengthObject ((h.intervalFunctor a b).obj E)) : IsStrictFiniteLengthObject E

Strict finite length descends along the restricted functor: both chain conditions on strict subobjects of the image pull back through the strictly monotone image map, by isStrictArtinianObject_of_strictMono and its Noetherian twin.

theorem CategoryTheory.Triangulated.Slicing.PreimageData.isLocallyFinite {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {s : Slicing D} {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) [IsTriangulated C] [IsTriangulated D] (hs : IsLocallyFinite D s) : IsLocallyFinite C (s.preimage F h)

Local finiteness survives transfer, with the same radius. The interval windows do not move, so the radius of the target slicing works verbatim; the content is the descent of strict finite length along the restricted functor, converted to and from the intrinsic admissible-subobject formulation by admissibleStrictSubobjectOrderIso.

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated C] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ : WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : σ.slicing.PreimageData F) : WithClassMap C (v.comp (K₀.map F))

The stability condition transported along a phase-detecting functor. The pre-stability data is PreStabilityCondition.WithClassMap.preimage; local finiteness is Slicing.PreimageData.isLocallyFinite. This is the Bridgeland-definition form of Remarks 3.2 and 3.7 of arXiv:2607.28411v1: once the preimage collection is a slicing, transfer produces a stability condition with respect to (Λ, v ∘ K₀(F)).

Equations

• σ.preimage F h = { toWithClassMap := σ.preimage F h, locallyFinite := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.preimage_toWithClassMap {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated C] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ : WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : σ.slicing.PreimageData F) : (σ.preimage F h).toWithClassMap = σ.preimage F h

Forgetting local finiteness commutes with transfer. Definitional; recorded so that every pre-stability result about preimage applies to the stability-level construction through one simp step.

@[simp]

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.preimage_slicing {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated C] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ : WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : σ.slicing.PreimageData F) : (σ.preimage F h).slicing = σ.slicing.preimage F h

The slicing of the transported stability condition is the preimage slicing. Restated at the stability-condition level so callers need not go through preimage_toWithClassMap.

@[simp]

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.preimage_Z {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated C] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ : WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : σ.slicing.PreimageData F) : (σ.preimage F h).Z = σ.Z

Transfer leaves the central charge on Λ untouched. Restated at the stability-condition level so callers need not go through preimage_toWithClassMap.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.preimage_charge {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated C] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ : WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : σ.slicing.PreimageData F) (E : C) : (σ.preimage F h).charge E = σ.charge (F.obj E)

The transported central charge of an object is the original charge of its image. Not a simp lemma: simp already derives it from preimage_toWithClassMap and the pre-stability preimage_charge, so it is recorded only as the direct restatement a caller can rw with.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.StabilityCondition.WithClassMap.pullback {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated C] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ : WithClassMap D v) (push : Functor C D) [push.Additive] [push.CommShift ℤ] [push.IsTriangulated] (h : σ.slicing.PreimageData push) : WithClassMap C (v.comp (K₀.map push))

Definition 3.1(3) of arXiv:2607.28411v1 for stability conditions: the pullback f^♯σ is computed through the direct image push = f_*. The name follows Slicing.pullback in Phase.Transfer.Basic.

Equations

• σ.pullback push h = σ.preimage push h

@[reducible, inline]

abbrev CategoryTheory.Triangulated.StabilityCondition.WithClassMap.pushforward {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated C] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ : WithClassMap D v) (pull : Functor C D) [pull.Additive] [pull.CommShift ℤ] [pull.IsTriangulated] (h : σ.slicing.PreimageData pull) : WithClassMap C (v.comp (K₀.map pull))

Definition 3.6(3) of arXiv:2607.28411v1 for stability conditions: the pushforward f_♯σ is computed through the inverse image pull = f^*. The name follows Slicing.pushforward in Phase.Transfer.Basic.

Equations

• σ.pushforward pull h = σ.preimage pull h