Classified residual projection objects

This file connects the generic right-adjoint projections of orthogonal exceptional blocks to the spherical and pseudoprojective classification interfaces. It isolates the formal content common to Paper I, Lemma 4.8 and Proposition 4.10, and Paper II, Lemma 2.4 and Theorem 2.7:

• the candidate attached to a block is the right projection of its first exceptional object;
• singleton blocks supply spherical candidates;
• longer blocks supply pseudoprojective candidates; and
• completeness and pairwise orthogonality promote these candidates to the existing classification packages.

The constructors below do not prove the geometric Ext calculations. Those remain explicit hypotheses, but the resulting classification data can no longer hide unrelated candidate objects behind an arbitrary function.

def CategoryTheory.SerreFunctor.SphericalClassificationData.ofResidualProjections {k : Type w} [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 : Triangulated.OrthogonalExceptionalBlocks k C ι) (Q : B.ResidualProjectionData) (D : SerreFunctorData k B.ResidualCategory) (n : ℕ) (candidate_spherical : ∀ (i : ι), IsSphericalObject D n (B.projectedObject Q i)) (pairwise_orthogonal : ∀ {i j : ι}, i ≠ j → IsGradedOrthogonal (B.projectedObject Q i) (B.projectedObject Q j)) (complete : ∀ (E : B.ResidualCategory), IsSphericalObject D n E ↔ ∃ (i : ι), IsShiftOf E (B.projectedObject Q i)) : SphericalClassificationData D n ι

Build a spherical classification whose candidates are the actual right projections of the first objects of exceptional blocks.

Equations

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

@[simp]

theorem CategoryTheory.SerreFunctor.SphericalClassificationData.ofResidualProjections_candidate {k : Type w} [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 : Triangulated.OrthogonalExceptionalBlocks k C ι) (Q : B.ResidualProjectionData) (D : SerreFunctorData k B.ResidualCategory) (n : ℕ) (candidate_spherical : ∀ (i : ι), IsSphericalObject D n (B.projectedObject Q i)) (pairwise_orthogonal : ∀ {i j : ι}, i ≠ j → IsGradedOrthogonal (B.projectedObject Q i) (B.projectedObject Q j)) (complete : ∀ (E : B.ResidualCategory), IsSphericalObject D n E ↔ ∃ (i : ι), IsShiftOf E (B.projectedObject Q i)) (i : ι) : (ofResidualProjections B Q D n candidate_spherical pairwise_orthogonal complete).candidate i = B.projectedObject Q i

def CategoryTheory.SerreFunctor.MixedClassificationData.ofResidualProjections {k : Type w} [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 : Triangulated.OrthogonalExceptionalBlocks k C ι) (Q : B.ResidualProjectionData) (D : SerreFunctorData k B.ResidualCategory) (n : ℕ) (spherical_of_length_one : ∀ (i : ι), B.length i = 1 → IsSphericalObject D n (B.projectedObject Q i)) (pseudoprojective_of_two_le : ∀ (i : ι), 2 ≤ B.length i → IsPseudoprojectiveObject D n (B.projectedObject Q i)) (pairwise_orthogonal : ∀ {i j : ι}, i ≠ j → IsGradedOrthogonal (B.projectedObject Q i) (B.projectedObject Q j)) (spherical_complete : ∀ (E : B.ResidualCategory), IsSphericalObject D n E ↔ ∃ (i : ι), B.length i = 1 ∧ IsShiftOf E (B.projectedObject Q i)) (pseudoprojective_complete : ∀ (E : B.ResidualCategory), IsPseudoprojectiveObject D n E ↔ ∃ (i : ι), 2 ≤ B.length i ∧ IsShiftOf E (B.projectedObject Q i)) : MixedClassificationData D n ι

Build the Paper II mixed classification with block lengths taken from the decomposition and candidates taken from its residual right projection.

Equations

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

@[simp]

theorem CategoryTheory.SerreFunctor.MixedClassificationData.ofResidualProjections_blockLength {k : Type w} [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 : Triangulated.OrthogonalExceptionalBlocks k C ι) (Q : B.ResidualProjectionData) (D : SerreFunctorData k B.ResidualCategory) (n : ℕ) (spherical_of_length_one : ∀ (i : ι), B.length i = 1 → IsSphericalObject D n (B.projectedObject Q i)) (pseudoprojective_of_two_le : ∀ (i : ι), 2 ≤ B.length i → IsPseudoprojectiveObject D n (B.projectedObject Q i)) (pairwise_orthogonal : ∀ {i j : ι}, i ≠ j → IsGradedOrthogonal (B.projectedObject Q i) (B.projectedObject Q j)) (spherical_complete : ∀ (E : B.ResidualCategory), IsSphericalObject D n E ↔ ∃ (i : ι), B.length i = 1 ∧ IsShiftOf E (B.projectedObject Q i)) (pseudoprojective_complete : ∀ (E : B.ResidualCategory), IsPseudoprojectiveObject D n E ↔ ∃ (i : ι), 2 ≤ B.length i ∧ IsShiftOf E (B.projectedObject Q i)) (i : ι) : (ofResidualProjections B Q D n spherical_of_length_one pseudoprojective_of_two_le pairwise_orthogonal spherical_complete pseudoprojective_complete).blockLength i = B.length i

@[simp]

theorem CategoryTheory.SerreFunctor.MixedClassificationData.ofResidualProjections_candidate {k : Type w} [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 : Triangulated.OrthogonalExceptionalBlocks k C ι) (Q : B.ResidualProjectionData) (D : SerreFunctorData k B.ResidualCategory) (n : ℕ) (spherical_of_length_one : ∀ (i : ι), B.length i = 1 → IsSphericalObject D n (B.projectedObject Q i)) (pseudoprojective_of_two_le : ∀ (i : ι), 2 ≤ B.length i → IsPseudoprojectiveObject D n (B.projectedObject Q i)) (pairwise_orthogonal : ∀ {i j : ι}, i ≠ j → IsGradedOrthogonal (B.projectedObject Q i) (B.projectedObject Q j)) (spherical_complete : ∀ (E : B.ResidualCategory), IsSphericalObject D n E ↔ ∃ (i : ι), B.length i = 1 ∧ IsShiftOf E (B.projectedObject Q i)) (pseudoprojective_complete : ∀ (E : B.ResidualCategory), IsPseudoprojectiveObject D n E ↔ ∃ (i : ι), 2 ≤ B.length i ∧ IsShiftOf E (B.projectedObject Q i)) (i : ι) : (ofResidualProjections B Q D n spherical_of_length_one pseudoprojective_of_two_le pairwise_orthogonal spherical_complete pseudoprojective_complete).candidate i = B.projectedObject Q i

theorem CategoryTheory.SerreFunctor.MixedClassificationData.residualProjection_candidate_dichotomy {k : Type w} [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 : Triangulated.OrthogonalExceptionalBlocks k C ι} {Q : B.ResidualProjectionData} {D : SerreFunctorData k B.ResidualCategory} {n : ℕ} (A : MixedClassificationData D n ι) (hlength : A.blockLength = B.length) (hcandidate : A.candidate = B.projectedObject Q) (i : ι) : IsSphericalObject D n (B.projectedObject Q i) ∨ IsPseudoprojectiveObject D n (B.projectedObject Q i)

Every residual projection candidate is spherical or pseudoprojective, according to the positive block-length dichotomy.