Spherical and pseudoprojective objects

This file formalizes Definitions 4.1 of arXiv:1912.04332v2 and 2.1 of arXiv:2104.13610v2 in a generic k-linear category with a chosen Serre functor.

An n-spherical object has one-dimensional self-Hom in degrees 0 and n, vanishing in every other degree, and is carried to its n-shift by the Serre functor. An n-pseudoprojective object has one-dimensional self-Hom in every degree from 0 through n, vanishing outside that interval, and satisfies the same Serre condition.

For pseudoprojective objects the paper asserts an isomorphism of graded vector spaces only. No multiplication or truncated-polynomial algebra structure is part of the definition here.

As throughout the repository, vanishing is stated as ∀ f, f = 0; applying IsZero to the bare type of morphisms would make the predicate uninhabitable.

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

An n-spherical object relative to a chosen Serre functor.

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

  Self-Homs vanish away from degrees 0 and n.

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

  The endomorphism space is the base field.

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

  The top self-Hom is the base field.

• serre_shift : Nonempty (D.S.obj E ≅ (shiftFunctor C ↑n).obj E)

  The Serre functor carries the object to its n-shift.

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

An n-pseudoprojective object relative to a chosen Serre functor.

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

  Every self-Hom from degree 0 through degree n is the base field.

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

  Self-Homs vanish outside the interval [0,n].

• serre_shift : Nonempty (D.S.obj E ≅ (shiftFunctor C ↑n).obj E)

  The Serre functor carries the object to its n-shift.

theorem CategoryTheory.SerreFunctor.IsSphericalObject.not_isZero {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {E : C} (h : IsSphericalObject D n E) : ¬Limits.IsZero E

A spherical object is nonzero.

theorem CategoryTheory.SerreFunctor.IsSphericalObject.finrank_end {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {E : C} (h : IsSphericalObject D n E) : Module.finrank k (E ⟶ E) = 1

The endomorphism space of a spherical object is one-dimensional.

theorem CategoryTheory.SerreFunctor.IsSphericalObject.finrank_top {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {E : C} (h : IsSphericalObject D n E) : Module.finrank k (E ⟶ (shiftFunctor C ↑n).obj E) = 1

The top self-Hom of a spherical object is one-dimensional.

theorem CategoryTheory.SerreFunctor.IsSphericalObject.finrank_hom_eq_zero {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {E : C} (h : IsSphericalObject D n E) (i : ℤ) (hi₀ : i ≠ 0) (hin : i ≠ ↑n) : Module.finrank k (E ⟶ (shiftFunctor C i).obj E) = 0

Every other self-Hom has dimension zero.

theorem CategoryTheory.SerreFunctor.IsSphericalObject.of_iso {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {E F : C} (h : IsSphericalObject D n E) (e : E ≅ F) : IsSphericalObject D n F

Sphericity is invariant under isomorphism.

theorem CategoryTheory.SerreFunctor.IsPseudoprojectiveObject.not_isZero {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {E : C} (h : IsPseudoprojectiveObject D n E) : ¬Limits.IsZero E

A pseudoprojective object is nonzero.

theorem CategoryTheory.SerreFunctor.IsPseudoprojectiveObject.finrank_inRange {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {E : C} (h : IsPseudoprojectiveObject D n E) (i : ℕ) (hi : i ≤ n) : Module.finrank k (E ⟶ (shiftFunctor C ↑i).obj E) = 1

Every in-range self-Hom is one-dimensional.

theorem CategoryTheory.SerreFunctor.IsPseudoprojectiveObject.finrank_hom_eq_zero {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {E : C} (h : IsPseudoprojectiveObject D n E) (i : ℤ) (hi : i < 0 ∨ ↑n < i) : Module.finrank k (E ⟶ (shiftFunctor C i).obj E) = 0

Every out-of-range self-Hom has dimension zero.

theorem CategoryTheory.SerreFunctor.IsPseudoprojectiveObject.of_iso {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {E F : C} (h : IsPseudoprojectiveObject D n E) (e : E ≅ F) : IsPseudoprojectiveObject D n F

Pseudoprojectivity is invariant under isomorphism.

theorem CategoryTheory.SerreFunctor.IsPseudoprojectiveObject.not_isSphericalObject {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctorData k C} {n : ℕ} {E : C} (h : IsPseudoprojectiveObject D n E) (hn : 2 ≤ n) : ¬IsSphericalObject D n E

For n ≥ 2, a pseudoprojective object cannot be spherical: degree one is nonzero for the former and vanishes for the latter.

theorem CategoryTheory.SerreFunctor.isSphericalObject_one_iff_isPseudoprojectiveObject_one {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (D : SerreFunctorData k C) (E : C) : IsSphericalObject D 1 E ↔ IsPseudoprojectiveObject D 1 E

In dimension one, the spherical and pseudoprojective profiles coincide.