Enriques categories

Definition 4.2 of arXiv:1912.04332v2 calls a linear triangulated category m-Enriques when its Serre functor satisfies S² ≅ [2m], with m ∈ (1/2)ℤ. The integral parameter twiceDimension used here is exactly 2m; it avoids introducing a rational index for a shift that is intrinsically integer-valued.

The Serre functor is required to be an autoequivalence as part of the package. SerreFunctorData alone does not assert essential surjectivity at this level of generality, so that fact is an explicit field rather than an invalid theorem.

The file also proves Remark 4.3(iii): if a positive-dimensional Serre functor is itself a shift, the category contains no exceptional objects. This is a genuine consequence of Serre duality and the exceptional-object vanishing clause; no geometry enters.

structure CategoryTheory.SerreFunctor.EnriquesCategoryData (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (twiceDimension : ℤ) extends CategoryTheory.SerreFunctor.SerreCategoryData k C : Type (max (max u v) w)

An Enriques-category structure of half-integral dimension twiceDimension / 2.

• serre : SerreFunctorData k C
• serreIsEquivalence : self.serre.S.IsEquivalence
• squareShift : Nonempty (self.serre.S.comp self.serre.S ≅ shiftFunctor C twiceDimension)

  The square of the Serre functor is the indicated shift.

@[reducible, inline]

abbrev CategoryTheory.SerreFunctor.TwoEnriquesCategoryData (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] : Type (max (max u v) w)

The paper's 2-Enriques categories, for which S² ≅ [4].

Equations

• CategoryTheory.SerreFunctor.TwoEnriquesCategoryData k C = CategoryTheory.SerreFunctor.EnriquesCategoryData k C 4

def CategoryTheory.SerreFunctor.EnriquesCategoryData.dimension {twiceDimension : ℤ} : ℚ

The half-integral Enriques dimension, retained as a readable invariant.

Equations

• CategoryTheory.SerreFunctor.EnriquesCategoryData.dimension = ↑twiceDimension / 2

noncomputable def CategoryTheory.SerreFunctor.EnriquesCategoryData.serreSquareIso {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {twiceDimension : ℤ} (A : EnriquesCategoryData k C twiceDimension) : A.serre.S.comp A.serre.S ≅ shiftFunctor C twiceDimension

A selected square-to-shift isomorphism from the property-valued field.

Equations

• A.serreSquareIso = ⋯.some

noncomputable def CategoryTheory.SerreFunctor.EnriquesCategoryData.serreSquareObjIso {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {twiceDimension : ℤ} (A : EnriquesCategoryData k C twiceDimension) (E : C) : A.serre.S.obj (A.serre.S.obj E) ≅ (shiftFunctor C twiceDimension).obj E

Objectwise form of S² ≅ [2m].

Equations

• A.serreSquareObjIso E = A.serreSquareIso.app E

theorem CategoryTheory.SerreFunctor.EnriquesCategoryData.hasSerreEquivalence {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {twiceDimension : ℤ} (A : EnriquesCategoryData k C twiceDimension) : A.serre.S.IsEquivalence

The chosen Serre functor can be used as an equivalence by instance search inside a consumer without making equivalence a global instance.

theorem CategoryTheory.SerreFunctor.no_exceptional_of_serre_iso_shift {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [HomFinite k C] (D : SerreFunctorData k C) (n : ℤ) (hn : n ≠ 0) (hS : Nonempty (D.S ≅ shiftFunctor C n)) (E : C) : ¬Triangulated.IsExceptional k E

If a nonzero shift is a Serre functor, no object can be exceptional.

This is Remark 4.3(iii) of arXiv:1912.04332v2. The proof compares dimensions: Serre duality identifies End(E) with the dual of Hom(E,S E), the displayed Serre/shift isomorphism identifies the latter with Hom(E,E[n]), and exceptionality makes the first one-dimensional and the last zero.