Categorical base change for triangulated fibers

The numerical family interfaces initially indexed unrelated triangulated categories by a type. This file records the next layer needed for families: a contravariant Cat-valued pseudofunctor, triangulated pullback functors, and their induced action on the repository-owned triangulated Grothendieck group.

The pseudofunctor supplies identity and composition coherence by natural isomorphisms. An ordinary strict functor is admitted through ofFunctor; it is a specialization, not the general root. No geometric origin is asserted: the base is an abstract category, not a scheme, and this file constructs neither derived pullback nor transport of slicings. Relative Harder--Narasimhan structures, openness, and boundedness remain separate geometric obligations.

structure CategoryTheory.Triangulated.Families.TriangulatedFiberFamily {B : Type u} [Category.{v, u} B] : Type (max (max u v) (w + 1))

A contravariant category-valued family whose fibers and transition functors carry the structures used by ordinary stability conditions.

For f : s ⟶ t, the pseudofunctorial map of fibers is interpreted as pullback from the fiber over t to the fiber over s.

• fibers : Pseudofunctor (LocallyDiscrete Bᵒᵖ) Cat

  The underlying contravariant category-valued family.

• fiberPreadditive (b : B) : Preadditive ↑(self.fibers.obj { as := Opposite.op b })

  Every fiber is preadditive.

• fiberZero (b : B) : Limits.HasZeroObject ↑(self.fibers.obj { as := Opposite.op b })

  Every fiber has a zero object.

• fiberShift (b : B) : HasShift ↑(self.fibers.obj { as := Opposite.op b }) ℤ

  Every fiber has an integer shift.

• fiberShiftAdditive (b : B) (n : ℤ) : (shiftFunctor (↑(self.fibers.obj { as := Opposite.op b })) n).Additive

  Every shift functor is additive.

• fiberPretriangulated (b : B) : Pretriangulated ↑(self.fibers.obj { as := Opposite.op b })

  Every fiber is pretriangulated.

• pullAdditive {s t : B} (f : s ⟶ t) : (self.fibers.map f.op.toLoc).toFunctor.Additive

  Every pullback functor is additive.

• pullCommShift {s t : B} (f : s ⟶ t) : (self.fibers.map f.op.toLoc).toFunctor.CommShift ℤ

  Every pullback functor commutes with the integer shift.

• pullTriangulated {s t : B} (f : s ⟶ t) : (self.fibers.map f.op.toLoc).toFunctor.IsTriangulated

  Every pullback functor preserves distinguished triangles.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber {B : Type u} [Category.{v, u} B] (F : TriangulatedFiberFamily) (b : B) : Type w

The triangulated category over one object of the base.

Equations

• F.Fiber b = ↑(F.fibers.obj { as := Opposite.op b })

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pull {B : Type u} [Category.{v, u} B] (F : TriangulatedFiberFamily) {s t : B} (f : s ⟶ t) : Functor (F.Fiber t) (F.Fiber s)

The pullback functor attached to a base morphism.

Equations

• F.pull f = (F.fibers.map f.op.toLoc).toFunctor

def CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pullIdIso {B : Type u} [Category.{v, u} B] (F : TriangulatedFiberFamily) (b : B) : F.pull (CategoryStruct.id b) ≅ Functor.id (F.Fiber b)

The pseudofunctorial unit identifying pullback along an identity with the identity functor on the fiber.

Equations

• F.pullIdIso b = id (CategoryTheory.Cat.Hom.toNatIso (F.fibers.mapId { as := Opposite.op b }))

def CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pullCompIso {B : Type u} [Category.{v, u} B] (F : TriangulatedFiberFamily) {r s t : B} (f : r ⟶ s) (g : s ⟶ t) : F.pull (CategoryStruct.comp f g) ≅ (F.pull g).comp (F.pull f)

The pseudofunctorial compositor identifying pullback along a composite with the corresponding iterated pullback.

Equations

• F.pullCompIso f g = id (CategoryTheory.Cat.Hom.toNatIso (F.fibers.mapComp g.op.toLoc f.op.toLoc))

def CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pullK₀ {B : Type u} [Category.{v, u} B] (F : TriangulatedFiberFamily) {s t : B} (f : s ⟶ t) : K₀ (F.Fiber t) →+ K₀ (F.Fiber s)

Pullback on the repository-owned triangulated Grothendieck groups.

Equations

• F.pullK₀ f = CategoryTheory.Triangulated.K₀.map (F.pull f)

@[simp]

theorem CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pullK₀_of {B : Type u} [Category.{v, u} B] (F : TriangulatedFiberFamily) {s t : B} (f : s ⟶ t) (E : F.Fiber t) : (F.pullK₀ f) (K₀.of (F.Fiber t) E) = K₀.of (F.Fiber s) ((F.pull f).obj E)

@[simp]

theorem CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pullK₀_id {B : Type u} [Category.{v, u} B] (F : TriangulatedFiberFamily) (b : B) : F.pullK₀ (CategoryStruct.id b) = AddMonoidHom.id (K₀ (F.Fiber b))

@[simp]

theorem CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pullK₀_comp {B : Type u} [Category.{v, u} B] (F : TriangulatedFiberFamily) {r s t : B} (f : r ⟶ s) (g : s ⟶ t) : F.pullK₀ (CategoryStruct.comp f g) = (F.pullK₀ f).comp (F.pullK₀ g)

def CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.ofFunctor {B : Type u} [Category.{v, u} B] (fibers : Functor Bᵒᵖ Cat) (fiberPreadditive : (b : B) → Preadditive ↑(fibers.obj (Opposite.op b))) (fiberZero : ∀ (b : B), Limits.HasZeroObject ↑(fibers.obj (Opposite.op b))) (fiberShift : (b : B) → HasShift ↑(fibers.obj (Opposite.op b)) ℤ) (fiberShiftAdditive : ∀ (b : B) (n : ℤ), (shiftFunctor (↑(fibers.obj (Opposite.op b))) n).Additive) (fiberPretriangulated : (b : B) → Pretriangulated ↑(fibers.obj (Opposite.op b))) (pullAdditive : ∀ {s t : B} (f : s ⟶ t), (fibers.map f.op).toFunctor.Additive) (pullCommShift : {s t : B} → (f : s ⟶ t) → (fibers.map f.op).toFunctor.CommShift ℤ) (pullTriangulated : ∀ {s t : B} (f : s ⟶ t), (fibers.map f.op).toFunctor.IsTriangulated) : TriangulatedFiberFamily

Promote an ordinary strict contravariant functor to a triangulated fiber family. The resulting pseudofunctor has equality-induced unit and compositor isomorphisms.

Equations

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

def CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.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] : TriangulatedFiberFamily

The constant category-valued family.

Equations

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

structure CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.CompatibleClassMaps {B : Type u} [Category.{v, u} B] (F : TriangulatedFiberFamily) (V : Type u_1) [AddCommGroup V] (classMap : (b : B) → K₀ (F.Fiber b) →+ V) : Prop

Class maps to one common group which are invariant under every categorical pullback.

• pull_compatible {s t : B} (f : s ⟶ t) (x : K₀ (F.Fiber t)) : (classMap s) ((F.pullK₀ f) x) = (classMap t) x

  Pullback does not change the common numerical class.

theorem CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.CompatibleClassMaps.class_pull {B : Type u} [Category.{v, u} B] {F : TriangulatedFiberFamily} {V : Type u_1} [AddCommGroup V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} (h : F.CompatibleClassMaps V classMap) {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)

Compatibility on Grothendieck groups specializes to the class of an actual pulled-back object.

theorem CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.CompatibleClassMaps.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_2) [AddCommGroup V] (v₀ : K₀ C →+ V) : (TriangulatedFiberFamily.constant B C).CompatibleClassMaps V fun (x : B) => v₀

A single class map gives compatible maps on the constant family.