Ext profiles and transport by Serre-compatible equivalences

The special objects in the two Enriques papers have two logically separate ingredients: a computation of all shifted self-Hom spaces and an isomorphism between the Serre image and the appropriate shift. SphericalExtProfile and PseudoprojectiveExtProfile isolate the computation; their constructors add the Serre isomorphism to recover IsSphericalObject and IsPseudoprojectiveObject.

The second part proves the equivalence-transport step used in both refined Torelli arguments. A SerreCompatibleEquivalence is an equivalence equipped with the linear, additive, shift, and Serre comparison data that the proof actually consumes. These fields are explicit because the general Serre uniqueness/conjugation lane (#896--#898) has not yet produced them automatically.

structure CategoryTheory.SerreFunctor.SphericalExtProfile {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (n : ℕ) (E : C) : Prop

The shifted self-Hom computation for an n-spherical object, before the Serre-action statement is added.

• vanishing (i : ℤ) : i ≠ 0 → i ≠ ↑n → ∀ (f : E ⟶ (shiftFunctor C i).obj E), f = 0

  Self-Homs vanish away from degrees zero and n.

• end_one : Nonempty ((E ⟶ E) ≃ₗ[k] k)

  The degree-zero self-Hom is one-dimensional.

• top_one : Nonempty ((E ⟶ (shiftFunctor C ↑n).obj E) ≃ₗ[k] k)

  The degree-n self-Hom is one-dimensional.

structure CategoryTheory.SerreFunctor.PseudoprojectiveExtProfile {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (n : ℕ) (E : C) : Prop

The shifted self-Hom computation for an n-pseudoprojective object, before the Serre-action statement is added.

• inRange_one (i : ℕ) : i ≤ n → Nonempty ((E ⟶ (shiftFunctor C ↑i).obj E) ≃ₗ[k] k)

  Every self-Hom in degrees zero through n is one-dimensional.

• vanishing (i : ℤ) : i < 0 ∨ ↑n < i → ∀ (f : E ⟶ (shiftFunctor C i).obj E), f = 0

  Self-Homs vanish outside degrees zero through n.

theorem CategoryTheory.SerreFunctor.SphericalExtProfile.toIsSphericalObject {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {n : ℕ} {E : C} (h : SphericalExtProfile n E) (D : SerreFunctorData k C) (serreShift : Nonempty (D.S.obj E ≅ (shiftFunctor C ↑n).obj E)) : IsSphericalObject D n E

Add the Serre-shift identification to an Ext computation.

theorem CategoryTheory.SerreFunctor.PseudoprojectiveExtProfile.toIsPseudoprojectiveObject {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {n : ℕ} {E : C} (h : PseudoprojectiveExtProfile n E) (D : SerreFunctorData k C) (serreShift : Nonempty (D.S.obj E ≅ (shiftFunctor C ↑n).obj E)) : IsPseudoprojectiveObject D n E

Add the Serre-shift identification to an Ext computation.

theorem CategoryTheory.SerreFunctor.SphericalExtProfile.map {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {n : ℕ} {E : C} (h : SphericalExtProfile n E) (F : Functor C D) [F.Additive] [Functor.Linear k F] [F.CommShift ℤ] (hF : F.FullyFaithful) : SphericalExtProfile n (F.obj E)

Spherical Ext computations transport through a fully faithful linear shift-compatible functor.

theorem CategoryTheory.SerreFunctor.PseudoprojectiveExtProfile.map {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {n : ℕ} {E : C} (h : PseudoprojectiveExtProfile n E) (F : Functor C D) [F.Additive] [Functor.Linear k F] [F.CommShift ℤ] (hF : F.FullyFaithful) : PseudoprojectiveExtProfile n (F.obj E)

Pseudoprojective Ext computations transport through a fully faithful linear shift-compatible functor.

structure CategoryTheory.SerreFunctor.SerreCompatibleEquivalence {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] (S_C : SerreFunctorData k C) (S_D : SerreFunctorData k D) : Type (max (max (max u u') v) v')

An equivalence together with the exact comparison data needed to transport Serre-theoretic objects.

The functor is already fully faithful and essentially surjective because it is an equivalence. Additivity, linearity, shift compatibility, and the intertwining of the two chosen Serre functors are kept as visible fields.

• equiv : C ≌ D

  The underlying equivalence.

• functorAdditive : self.equiv.functor.Additive

  The forward functor is additive.

• functorLinear : Functor.Linear k self.equiv.functor

  The forward functor is k-linear.

• functorCommShift : self.equiv.functor.CommShift ℤ

  The forward functor commutes coherently with integral shifts.

• serreIso : S_C.S.comp self.equiv.functor ≅ self.equiv.functor.comp S_D.S

  The forward functor intertwines the chosen Serre functors.

• inverseAdditive : self.equiv.inverse.Additive

  The inverse functor is additive.

• inverseLinear : Functor.Linear k self.equiv.inverse

  The inverse functor is k-linear.

• inverseCommShift : self.equiv.inverse.CommShift ℤ

  The inverse functor commutes coherently with integral shifts.

• inverseSerreIso : S_D.S.comp self.equiv.inverse ≅ self.equiv.inverse.comp S_C.S

  The inverse functor intertwines the chosen Serre functors.

def CategoryTheory.SerreFunctor.SerreCompatibleEquivalence.symm {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {S_C : SerreFunctorData k C} {S_D : SerreFunctorData k D} (F : SerreCompatibleEquivalence S_C S_D) : SerreCompatibleEquivalence S_D S_C

Reverse a Serre-compatible equivalence, retaining all of its linear and shift comparison data.

Equations

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

theorem CategoryTheory.SerreFunctor.SerreCompatibleEquivalence.mapSpherical {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {S_C : SerreFunctorData k C} {S_D : SerreFunctorData k D} (F : SerreCompatibleEquivalence S_C S_D) {n : ℕ} {E : C} (h : IsSphericalObject S_C n E) : IsSphericalObject S_D n (F.equiv.functor.obj E)

A spherical object remains spherical under a Serre-compatible equivalence.

theorem CategoryTheory.SerreFunctor.SerreCompatibleEquivalence.mapPseudoprojective {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {S_C : SerreFunctorData k C} {S_D : SerreFunctorData k D} (F : SerreCompatibleEquivalence S_C S_D) {n : ℕ} {E : C} (h : IsPseudoprojectiveObject S_C n E) : IsPseudoprojectiveObject S_D n (F.equiv.functor.obj E)

A pseudoprojective object remains pseudoprojective under a Serre-compatible equivalence.

theorem CategoryTheory.SerreFunctor.SerreCompatibleEquivalence.spherical_iff {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {S_C : SerreFunctorData k C} {S_D : SerreFunctorData k D} (F : SerreCompatibleEquivalence S_C S_D) {n : ℕ} {E : C} : IsSphericalObject S_D n (F.equiv.functor.obj E) ↔ IsSphericalObject S_C n E

A Serre-compatible equivalence preserves and reflects spherical objects.

theorem CategoryTheory.SerreFunctor.SerreCompatibleEquivalence.pseudoprojective_iff {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {S_C : SerreFunctorData k C} {S_D : SerreFunctorData k D} (F : SerreCompatibleEquivalence S_C S_D) {n : ℕ} {E : C} : IsPseudoprojectiveObject S_D n (F.equiv.functor.obj E) ↔ IsPseudoprojectiveObject S_C n E

A Serre-compatible equivalence preserves and reflects pseudoprojective objects.

theorem CategoryTheory.SerreFunctor.SerreCompatibleEquivalence.mapIsShiftOf {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {S_C : SerreFunctorData k C} {S_D : SerreFunctorData k D} (F : SerreCompatibleEquivalence S_C S_D) {E E' : C} (h : IsShiftOf E E') : IsShiftOf (F.equiv.functor.obj E) (F.equiv.functor.obj E')

Being a shift of an object is preserved by a shift-compatible equivalence.

theorem CategoryTheory.SerreFunctor.SerreCompatibleEquivalence.isShiftOf_iff {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {S_C : SerreFunctorData k C} {S_D : SerreFunctorData k D} (F : SerreCompatibleEquivalence S_C S_D) {E E' : C} : IsShiftOf (F.equiv.functor.obj E) (F.equiv.functor.obj E') ↔ IsShiftOf E E'

A Serre-compatible equivalence preserves and reflects the relation of being an integral shift.

theorem CategoryTheory.SerreFunctor.SerreCompatibleEquivalence.mapIsGradedOrthogonal {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {S_C : SerreFunctorData k C} {S_D : SerreFunctorData k D} (F : SerreCompatibleEquivalence S_C S_D) {E E' : C} (h : IsGradedOrthogonal E E') : IsGradedOrthogonal (F.equiv.functor.obj E) (F.equiv.functor.obj E')

Graded orthogonality is preserved by a shift-compatible equivalence.

theorem CategoryTheory.SerreFunctor.SerreCompatibleEquivalence.isGradedOrthogonal_iff {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {S_C : SerreFunctorData k C} {S_D : SerreFunctorData k D} (F : SerreCompatibleEquivalence S_C S_D) {E E' : C} : IsGradedOrthogonal (F.equiv.functor.obj E) (F.equiv.functor.obj E') ↔ IsGradedOrthogonal E E'

A Serre-compatible equivalence preserves and reflects graded orthogonality.