Right-adjoint projections onto admissible components

For a full subcategory cut out by an object property P, a right projection is a chosen right adjoint to the inclusion P.ι. The distinction between existence and chosen data is intentional: P.IsRightAdmissible is a proposition, while the Enriques papers form concrete objects such as ζ_K^!(L) and therefore need an actual projection functor.

This file packages only the adjunction. It does not call a cone functor or construct mutations: functorial cones are unavailable in a bare triangulated category. The adjunction nevertheless gives the universal Hom equivalence used in Paper I, Remark 4.9, and in Paper II's definition of the residual projection objects.

structure CategoryTheory.ObjectProperty.RightProjectionData {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Type (max u v)

A chosen right-adjoint projection onto the full subcategory defined by P.

• projection : Functor C P.FullSubcategory

  The right projection functor.

• adjunction : P.ι ⊣ self.projection

  The inclusion is left adjoint to the projection.

def CategoryTheory.ObjectProperty.RightProjectionData.ofEq {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) {P' : ObjectProperty C} (h : P = P') : P'.RightProjectionData

Transport chosen right-projection data across an equality of object properties.

Equations

• Q.ofEq h = h ▸ Q

noncomputable def CategoryTheory.ObjectProperty.RightProjectionData.ofIsRightAdmissible {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (hP : P.IsRightAdmissible) : P.RightProjectionData

Extract a chosen right projection from proposition-valued right admissibility. This is noncomputable because admissibility only asserts that the adjoint exists.

Equations

• CategoryTheory.ObjectProperty.RightProjectionData.ofIsRightAdmissible hP = { projection := ⋯.choose, adjunction := ⋯.some }

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.RightProjectionData.project {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) (X : C) : P.FullSubcategory

The projected object, as an object of the full subcategory.

Equations

• Q.project X = Q.projection.obj X

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.RightProjectionData.projectObj {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) (X : C) : C

The underlying ambient object of a projection.

Equations

• Q.projectObj X = P.ι.obj (Q.project X)

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.RightProjectionData.ambientProjection {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) : Functor C C

The ambient endofunctor underlying a right projection.

Equations

• Q.ambientProjection = Q.projection.comp P.ι

def CategoryTheory.ObjectProperty.RightProjectionData.ofEqAmbientIso {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) {P' : ObjectProperty C} (h : P = P') : (Q.ofEq h).ambientProjection ≅ Q.ambientProjection

Equality transport does not change the underlying ambient projection.

Equations

• Q.ofEqAmbientIso h = h ▸ CategoryTheory.Iso.refl (Q.ofEq ⋯).ambientProjection

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.RightProjectionData.counitApp {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) (X : C) : Q.projectObj X ⟶ X

The counit map from the projected ambient object to its source.

Equations

• Q.counitApp X = Q.adjunction.counit.app X

def CategoryTheory.ObjectProperty.RightProjectionData.homEquiv {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) (R : P.FullSubcategory) (X : C) : (P.ι.obj R ⟶ X) ≃ (R ⟶ Q.project X)

The universal property of the right projection.

Equations

• Q.homEquiv R X = Q.adjunction.homEquiv R X

def CategoryTheory.ObjectProperty.RightProjectionData.homEquivFromProject {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) (R : P.FullSubcategory) (X : C) : (R ⟶ Q.project X) ≃ (P.ι.obj R ⟶ X)

The universal property in the direction used by residual-category consumers: maps from a residual object to the projected object are exactly ambient maps to the original object.

Equations

• Q.homEquivFromProject R X = (Q.adjunction.homEquiv R X).symm

theorem CategoryTheory.ObjectProperty.RightProjectionData.homEquivFromProject_id {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) (X : C) : (Q.homEquivFromProject (Q.project X) X) (CategoryStruct.id (Q.project X)) = Q.counitApp X

Under the universal Hom equivalence, the identity of a projected object corresponds to the counit map.

theorem CategoryTheory.ObjectProperty.RightProjectionData.isRightAdmissible {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (hP : P.IsTriangulated) : P.IsRightAdmissible

Chosen projection data witnesses proposition-valued right admissibility once triangulated closure of the component is known.

theorem CategoryTheory.ObjectProperty.RightProjectionData.project_isZero_iff {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (Q : P.RightProjectionData) [Preadditive C] (X : C) : Limits.IsZero (Q.project X) ↔ ∀ (R : P.FullSubcategory) (f : P.ι.obj R ⟶ X), f = 0

The projection of X is zero exactly when every ambient map from a P-object to X vanishes.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.ResidualProjectionData {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type t} (B : OrthogonalExceptionalBlocks k C ι) : Type (max u v)

A chosen right projection onto the residual category of an exceptional block decomposition.

Equations

• B.ResidualProjectionData = B.residual.RightProjectionData

@[reducible, inline]

abbrev CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.projectedObject {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type t} (B : OrthogonalExceptionalBlocks k C ι) (Q : B.ResidualProjectionData) (i : ι) : B.ResidualCategory

The residual projection of the first exceptional object in block i. This is the common categorical shape of the objects S_i in both Enriques papers.

Equations

• B.projectedObject Q i = CategoryTheory.ObjectProperty.RightProjectionData.project Q (B.firstObject i)

def CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.projectedObjectHomEquiv {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type t} (B : OrthogonalExceptionalBlocks k C ι) (Q : B.ResidualProjectionData) (R : B.ResidualCategory) (i : ι) : (R ⟶ B.projectedObject Q i) ≃ (B.residual.ι.obj R ⟶ B.firstObject i)

Universal property of a residual projection object.

Equations

• B.projectedObjectHomEquiv Q R i = CategoryTheory.ObjectProperty.RightProjectionData.homEquivFromProject Q R (B.firstObject i)

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.projectedObjectHomEquiv_id {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type t} (B : OrthogonalExceptionalBlocks k C ι) (Q : B.ResidualProjectionData) (i : ι) : (B.projectedObjectHomEquiv Q (B.projectedObject Q i) i) (CategoryStruct.id (B.projectedObject Q i)) = ObjectProperty.RightProjectionData.counitApp Q (B.firstObject i)

The identity of a residual projection object corresponds to its counit map into the first exceptional object of the block.