Classification of spherical and pseudoprojective objects up to shift

The classification theorems in the two Enriques papers have a common logical shape. A finite family of candidates is constructed, distinct candidates are graded-orthogonal, and every spherical or pseudoprojective object is isomorphic to a shift of the appropriate candidate.

This file isolates that shape. It proves the formal consequences of graded orthogonality and packages the conclusions of arXiv:1912.04332v2 Proposition 4.10 and arXiv:2104.13610v2 Theorem 2.7 as explicit supplied classification data. It does not claim the deep geometric hypotheses needed by those papers: mutations, admissible projection functors, and the Enriques-surface Ext calculations are not yet constructed in this repository.

def CategoryTheory.SerreFunctor.IsShiftOf {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (E F : C) : Prop

E is isomorphic to some integral shift of F.

Equations

• CategoryTheory.SerreFunctor.IsShiftOf E F = ∃ (p : ℤ), Nonempty (E ≅ (CategoryTheory.shiftFunctor C p).obj F)

theorem CategoryTheory.SerreFunctor.IsShiftOf.refl {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (E : C) : IsShiftOf E E

Every object is a shift of itself, with shift zero.

theorem CategoryTheory.SerreFunctor.IsShiftOf.symm {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {E F : C} (h : IsShiftOf E F) : IsShiftOf F E

Being isomorphic up to an integral shift is symmetric.

theorem CategoryTheory.SerreFunctor.IsShiftOf.trans {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {E F G : C} (hEF : IsShiftOf E F) (hFG : IsShiftOf F G) : IsShiftOf E G

Integral shifts compose, so IsShiftOf is transitive.

theorem CategoryTheory.SerreFunctor.IsShiftOf.of_iso_left {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {E E' F : C} (e : E ≅ E') (h : IsShiftOf E' F) : IsShiftOf E F

Replacing the left object by an isomorphic object preserves IsShiftOf.

theorem CategoryTheory.SerreFunctor.IsShiftOf.of_iso_right {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {E F F' : C} (h : IsShiftOf E F) (e : F ≅ F') : IsShiftOf E F'

Replacing the right object by an isomorphic object preserves IsShiftOf.

def CategoryTheory.SerreFunctor.IsGradedOrthogonal {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (E F : C) : Prop

All shifted Homs from E to F vanish.

Equations

• CategoryTheory.SerreFunctor.IsGradedOrthogonal E F = ∀ (p : ℤ) (f : E ⟶ (CategoryTheory.shiftFunctor C p).obj F), f = 0

theorem CategoryTheory.SerreFunctor.not_isShiftOf_of_isGradedOrthogonal {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {E F : C} (hE : ¬Limits.IsZero E) (horth : IsGradedOrthogonal E F) : ¬IsShiftOf E F

A nonzero object cannot be a shift of an object to which it is graded orthogonal.

structure CategoryTheory.SerreFunctor.SphericalClassificationData {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (D : SerreFunctorData k C) (n : ℕ) (ι : Type t) : Type (max t u)

A family of spherical candidates with the completeness and separation conclusions of Paper I, Proposition 4.10. The fields are supplied because the mutation argument proving them is not generic category theory.

• candidate : ι → C

  The classified candidate family.

• candidate_spherical (i : ι) : IsSphericalObject D n (self.candidate i)

  Every candidate is spherical.

• pairwise_orthogonal {i j : ι} : i ≠ j → IsGradedOrthogonal (self.candidate i) (self.candidate j)

  Distinct candidates are graded-orthogonal.

• complete (E : C) : IsSphericalObject D n E ↔ ∃ (i : ι), IsShiftOf E (self.candidate i)

  Every spherical object is, and only is, a shift of a candidate.

theorem CategoryTheory.SerreFunctor.SphericalClassificationData.candidate_not_isShiftOf {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {ι : Type t} (A : SphericalClassificationData D n ι) {i j : ι} (hij : i ≠ j) : ¬IsShiftOf (A.candidate i) (A.candidate j)

Distinct candidates are not isomorphic up to any shift.

theorem CategoryTheory.SerreFunctor.SphericalClassificationData.exists_candidate_shift {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {ι : Type t} (A : SphericalClassificationData D n ι) {E : C} (hE : IsSphericalObject D n E) : ∃ (i : ι) (p : ℤ), Nonempty (E ≅ (shiftFunctor C p).obj (A.candidate i))

Find a candidate and shift representing a spherical object.

structure CategoryTheory.SerreFunctor.MixedClassificationData {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (D : SerreFunctorData k C) (n : ℕ) (ι : Type t) : Type (max t u)

The mixed classification pattern of Paper II, Theorem 2.7.

blockLength i = 1 marks the spherical candidates and 2 ≤ blockLength i marks the pseudoprojective candidates. The intended paper specialization is n = 3.

• blockLength : ι → ℕ

  The length of the exceptional block producing a candidate.

• candidate : ι → C

  The projected candidate object.

• spherical_of_length_one (i : ι) : self.blockLength i = 1 → IsSphericalObject D n (self.candidate i)

  Length-one blocks produce spherical candidates.

• pseudoprojective_of_two_le (i : ι) : 2 ≤ self.blockLength i → IsPseudoprojectiveObject D n (self.candidate i)

  Longer blocks produce pseudoprojective candidates.

• pairwise_orthogonal {i j : ι} : i ≠ j → IsGradedOrthogonal (self.candidate i) (self.candidate j)

  Distinct candidates are graded-orthogonal.

• spherical_complete (E : C) : IsSphericalObject D n E ↔ ∃ (i : ι), self.blockLength i = 1 ∧ IsShiftOf E (self.candidate i)

  Classification of all spherical objects.

• pseudoprojective_complete (E : C) : IsPseudoprojectiveObject D n E ↔ ∃ (i : ι), 2 ≤ self.blockLength i ∧ IsShiftOf E (self.candidate i)

  Classification of all pseudoprojective objects.

theorem CategoryTheory.SerreFunctor.MixedClassificationData.candidate_spherical {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {ι : Type t} (A : MixedClassificationData D n ι) {i : ι} (hi : A.blockLength i = 1) : IsSphericalObject D n (A.candidate i)

A length-one candidate is spherical.

theorem CategoryTheory.SerreFunctor.MixedClassificationData.candidate_pseudoprojective {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {ι : Type t} (A : MixedClassificationData D n ι) {i : ι} (hi : 2 ≤ A.blockLength i) : IsPseudoprojectiveObject D n (A.candidate i)

A longer-block candidate is pseudoprojective.

theorem CategoryTheory.SerreFunctor.MixedClassificationData.spherical_candidate_not_isShiftOf {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {ι : Type t} (A : MixedClassificationData D n ι) {i j : ι} (hi : A.blockLength i = 1) (hij : i ≠ j) : ¬IsShiftOf (A.candidate i) (A.candidate j)

Distinct spherical candidates are not isomorphic up to shift.

theorem CategoryTheory.SerreFunctor.MixedClassificationData.pseudoprojective_candidate_not_isShiftOf {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {ι : Type t} (A : MixedClassificationData D n ι) {i j : ι} (hi : 2 ≤ A.blockLength i) (hij : i ≠ j) : ¬IsShiftOf (A.candidate i) (A.candidate j)

Distinct pseudoprojective candidates are not isomorphic up to shift.

theorem CategoryTheory.SerreFunctor.MixedClassificationData.spherical_iff {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {ι : Type t} (A : MixedClassificationData D n ι) (E : C) : IsSphericalObject D n E ↔ ∃ (i : ι), A.blockLength i = 1 ∧ IsShiftOf E (A.candidate i)

Exact spherical half of the Paper II classification.

theorem CategoryTheory.SerreFunctor.MixedClassificationData.pseudoprojective_iff {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {ι : Type t} (A : MixedClassificationData D n ι) (E : C) : IsPseudoprojectiveObject D n E ↔ ∃ (i : ι), 2 ≤ A.blockLength i ∧ IsShiftOf E (A.candidate i)

Exact pseudoprojective half of the Paper II classification.