Right projections onto t-structure aisles

The nonpositive truncation of a t-structure is the canonical right adjoint to the inclusion of its aisle. Mathlib constructs the ambient truncation functor and proves its universal mapping property; this file packages that property as the chosen right projection used by the semiorthogonal-decomposition API.

The ambient projector is naturally isomorphic to truncLE. Consequently any coproduct-preservation theorem for truncation transfers directly to the chosen projection.

instance CategoryTheory.Triangulated.TStructure.aisleInclusionIsLE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : (t.le n).FullSubcategory) : t.IsLE ((t.le n).ι.obj X) n

noncomputable def CategoryTheory.Triangulated.TStructure.aisleProjection {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : Functor C (t.le n).FullSubcategory

The truncation functor with its codomain restricted to the aisle.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.aisleProjection_obj_obj {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : ((t.aisleProjection n).obj X).obj = (t.truncLE n).obj X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.aisleProjection_map_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) {X Y : C} (f : X ⟶ Y) : ((t.aisleProjection n).map f).hom = (t.truncLE n).map f

noncomputable def CategoryTheory.Triangulated.TStructure.aisleProjectionHomEquiv {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : (t.le n).FullSubcategory) (Y : C) : ((t.le n).ι.obj X ⟶ Y) ≃ (X ⟶ (t.aisleProjection n).obj Y)

The universal Hom equivalence for the aisle truncation.

Equations

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

theorem CategoryTheory.Triangulated.TStructure.aisleProjectionHomEquiv_apply {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : (t.le n).FullSubcategory) (Y : C) (f : (t.le n).ι.obj X ⟶ Y) : (t.aisleProjectionHomEquiv n X Y) f = ObjectProperty.homMk (t.liftTruncLE f n)

Not a simp lemma: ObjectProperty.ι_obj rewrites the source type of f, so simp's normal form for this left-hand side is one this statement does not have and the rewrite could never fire. aisleProjectionAdjunction uses it through rw, where that does not matter.

theorem CategoryTheory.Triangulated.TStructure.aisleProjectionHomEquiv_symm_apply {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : (t.le n).FullSubcategory) (Y : C) (f : X ⟶ (t.aisleProjection n).obj Y) : (t.aisleProjectionHomEquiv n X Y).symm f = CategoryStruct.comp f.hom ((t.truncLEι n).app Y)

Not a simp lemma, for the reason given on aisleProjectionHomEquiv_apply.

noncomputable def CategoryTheory.Triangulated.TStructure.aisleProjectionAdjunction {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : (t.le n).ι ⊣ t.aisleProjection n

The inclusion of a t-structure aisle is left adjoint to truncation into that aisle.

Equations

• t.aisleProjectionAdjunction n = CategoryTheory.Adjunction.mkOfHomEquiv { homEquiv := t.aisleProjectionHomEquiv n, homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }

noncomputable def CategoryTheory.Triangulated.TStructure.aisleRightProjectionData {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : (t.le n).RightProjectionData

The canonical chosen right projection onto an aisle.

Equations

• t.aisleRightProjectionData n = { projection := t.aisleProjection n, adjunction := t.aisleProjectionAdjunction n }

noncomputable def CategoryTheory.Triangulated.TStructure.aisleRightProjectionDataAmbientIso {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : (t.aisleRightProjectionData n).ambientProjection ≅ t.truncLE n

The ambient endofunctor of the aisle projection is naturally isomorphic to the ordinary truncation functor.

Equations

• t.aisleRightProjectionDataAmbientIso n = CategoryTheory.Iso.refl (t.aisleRightProjectionData n).ambientProjection

theorem CategoryTheory.Triangulated.TStructure.aisleRightProjectionData_preservesSmallCoproducts {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (h : (t.truncLE n).PreservesSmallCoproducts) : (t.aisleRightProjectionData n).ambientProjection.PreservesSmallCoproducts

Coproduct preservation of truncation transfers to the ambient aisle projector.

theorem CategoryTheory.Triangulated.TStructure.le_isRightAdmissible {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (h : (t.le n).IsTriangulated) : (t.le n).IsRightAdmissible

An aisle which is also triangulated is right admissible. The extra triangulatedness does not hold for an arbitrary t-structure aisle, but does hold when the aisle is a coproduct closure of a triangulated property.