Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.Families.PreStabilityBaseChange

Fiber pre-stability conditions and categorical base change #

This file binds actual pre-stability conditions on the fibers of a TriangulatedFiberFamily to its pullback functors. The compatibility package requires the precise non-formal witness which turns the inverse-image phase collection into a slicing, equality with the target-fiber slicing, and compatibility of both numerical class maps and central charges.

The package does not construct the Slicing.PreimageData witnesses from geometry. In particular, it supplies no family of schemes, derived pullback construction, relative Harder--Narasimhan theorem, openness, or boundedness.

source
structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData {B : Type u} [Category.{v, u} B] (F : Families.TriangulatedFiberFamily) {V : Type uV} [AddCommGroup V] (classMap : (b : B) → K₀ (F.Fiber b) →+ V) (sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)) :
Prop

Fiber pre-stability conditions whose slicings and common numerical data are compatible with every categorical pullback functor.

  • classMap_compatible : F.CompatibleClassMaps V classMap

    The common numerical class is invariant under pullback.

  • charge_compatible {s t : B} : ∀ (x : s ⟶ t), (sigma s).Z = (sigma t).Z

    Every fiber uses the same central charge on the common class group.

  • preimageData {s t : B} (f : s ⟶ t) : (sigma s).slicing.PreimageData (F.pull f)

    Pullback admits the non-formal Hom-vanishing and HN data needed to construct the inverse-image slicing.

  • slicing_compatible {s t : B} (f : s ⟶ t) : (sigma t).slicing = (sigma s).slicing.preimage (F.pull f) ⋯

    The target-fiber slicing is exactly the inverse image of the source-fiber slicing along pullback.

Instances For
    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.phase_iff {B : Type u} [Category.{v, u} B] {F : Families.TriangulatedFiberFamily} {V : Type uV} [AddCommGroup V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} (h : FiberPreStabilityBaseChangeData F classMap sigma) {s t : B} (f : s ⟶ t) (phi : ℝ) (E : F.Fiber t) :
    (sigma t).slicing.P phi E ↔ (sigma s).slicing.P phi ((F.pull f).obj E)

    An object lies in a target-fiber phase exactly when its pullback lies in the corresponding source-fiber phase.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.preimageData_comp {B : Type u} [Category.{v, u} B] {F : Families.TriangulatedFiberFamily} {V : Type uV} [AddCommGroup V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} (h : FiberPreStabilityBaseChangeData F classMap sigma) {r s t : B} (f : r ⟶ s) (g : s ⟶ t) :
    (sigma r).slicing.PreimageData ((F.pull g).comp (F.pull f))

    The witnesses attached to two successive base changes compose on the iterated pullback functor. Comparison with pullback along the composite is supplied by the pseudofunctor compositor.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.preimageData_pullComp {B : Type u} [Category.{v, u} B] {F : Families.TriangulatedFiberFamily} {V : Type uV} [AddCommGroup V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} (h : FiberPreStabilityBaseChangeData F classMap sigma) {r s t : B} (f : r ⟶ s) (g : s ⟶ t) :
    (sigma r).slicing.PreimageData (F.pull (CategoryStruct.comp f g))

    Transport the iterated preimage witness to pullback along the composite using the pseudofunctor compositor.

    source
    @[simp]
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.preimage_pullComp {B : Type u} [Category.{v, u} B] {F : Families.TriangulatedFiberFamily} {V : Type uV} [AddCommGroup V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} (h : FiberPreStabilityBaseChangeData F classMap sigma) {r s t : B} (f : r ⟶ s) (g : s ⟶ t) :
    (sigma r).slicing.preimage (F.pull (CategoryStruct.comp f g)) ⋯ = (sigma r).slicing.preimage ((F.pull g).comp (F.pull f)) ⋯

    Preimage slicing along a composite pullback agrees with preimage slicing along the two pullback stages.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.slicing_compatible_comp {B : Type u} [Category.{v, u} B] {F : Families.TriangulatedFiberFamily} {V : Type uV} [AddCommGroup V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} (h : FiberPreStabilityBaseChangeData F classMap sigma) {r s t : B} (f : r ⟶ s) (g : s ⟶ t) :
    (sigma t).slicing = (sigma r).slicing.preimage ((F.pull g).comp (F.pull f)) ⋯

    The slicing over the target of two successive base changes can be constructed in one step along the composite pullback functor.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.slicing_compatible_pullComp {B : Type u} [Category.{v, u} B] {F : Families.TriangulatedFiberFamily} {V : Type uV} [AddCommGroup V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} (h : FiberPreStabilityBaseChangeData F classMap sigma) {r s t : B} (f : r ⟶ s) (g : s ⟶ t) :
    (sigma t).slicing = (sigma r).slicing.preimage (F.pull (CategoryStruct.comp f g)) ⋯

    The target slicing is also the preimage along pullback by the composite, with the witness transported through the pseudofunctor compositor.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.phase_iff_comp {B : Type u} [Category.{v, u} B] {F : Families.TriangulatedFiberFamily} {V : Type uV} [AddCommGroup V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} (h : FiberPreStabilityBaseChangeData F classMap sigma) {r s t : B} (f : r ⟶ s) (g : s ⟶ t) (phi : ℝ) (E : F.Fiber t) :
    (sigma t).slicing.P phi E ↔ (sigma r).slicing.P phi ((F.pull f).obj ((F.pull g).obj E))

    Phase membership transported through a composite base change agrees with transport through its two stages.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.class_pull {B : Type u} [Category.{v, u} B] {F : Families.TriangulatedFiberFamily} {V : Type uV} [AddCommGroup V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} (h : FiberPreStabilityBaseChangeData F classMap sigma) {s t : B} (f : s ⟶ t) (E : F.Fiber t) :
    (classMap s) (K₀.of (F.Fiber s) ((F.pull f).obj E)) = (classMap t) (K₀.of (F.Fiber t) E)

    Pullback preserves the common numerical class of an object.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.charge_pull {B : Type u} [Category.{v, u} B] {F : Families.TriangulatedFiberFamily} {V : Type uV} [AddCommGroup V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} (h : FiberPreStabilityBaseChangeData F classMap sigma) {s t : B} (f : s ⟶ t) (E : F.Fiber t) :
    (sigma s).charge ((F.pull f).obj E) = (sigma t).charge E

    Pullback preserves the central charge of an object.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.constant {B : Type u} [Category.{v, u} B] (C : Type w) [Category.{w, w} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (V : Type u_1) [AddCommGroup V] (v₀ : K₀ C →+ V) (sigma₀ : PreStabilityCondition.WithClassMap C v₀) :
    FiberPreStabilityBaseChangeData (Families.TriangulatedFiberFamily.constant B C) (fun (x : B) => v₀) fun (x : B) => sigma₀

    One pre-stability condition supplies the constant base-change model.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData.class_mem_semistableClasses_pull {B : Type u} [Category.{v, u} B] {F : Families.TriangulatedFiberFamily} {W : Type uV} [NormedAddCommGroup W] {classMap' : (b : B) → K₀ (F.Fiber b) →+ W} {sigma' : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap' b)} (h : FiberPreStabilityBaseChangeData F classMap' sigma') {s t : B} (f : s ⟶ t) {phi : ℝ} {E : F.Fiber t} (hP : (sigma' t).slicing.P phi E) (hE : ¬Limits.IsZero ((F.pull f).obj E)) :
    (classMap' t) (K₀.of (F.Fiber t) E) ∈ (sigma' s).semistableClasses

    A target-fiber semistable object whose pullback remains nonzero contributes the same common class to the source-fiber semistable locus.