Spherical objects without a Serre functor, and their Euler characteristic

IsSphericalObject k n E says Hom(E, E⟦i⟧) vanishes off {0, n} and is the base field at both. From it, chiHom_self_eq computes χ(E,E) = 1 + (-1)ⁿ, and at n = 2 that discharges the hypothesis χ(E,E) = 2 which the spherical twist's involutivity consumes — so a caller holding a spherical object no longer supplies it by hand.

Why a second sphericity predicate, and how it relates to the first

SerreFunctor/Objects.lean already has SerreFunctor.IsSphericalObject D n E, relative to a chosen Serre functor, carrying a fourth clause S(E) ≅ E⟦n⟧. This one is deliberately weaker: a general k-linear pretriangulated category has no Serre functor at all, and the Euler computation needs none. Rather than leave two parallel predicates, of_serreFunctor projects the Serre-relative one onto this one, so the Euler computation proved here is available there too. The projection is one-way and must stay so: nothing here reconstructs a Serre functor.

Trap: n = 0 makes the Euler computation false, not vacuous

The structure is perfectly inhabitable at n = 0 — vanishing's two side conditions collapse into one, the support is {0}, and end_one and top_one say the same thing up to shiftFunctor 0. There χ(E,E) = 1, while 1 + (-1)⁰ = 2. So chiHom_self_eq without hn : n ≠ 0 is false rather than vacuous, and an implementer who drops the hypothesis is left with an unprovable goal — or closes it by silently strengthening the structure, which is worse. The hypothesis is what makes {0, n} a two-element set so the sum splits. The degenerate value is recorded separately as chiHom_self_eq_one_of_zero.

Trap: the spelling of the vanishing clause

vanishing reads ∀ f : E ⟶ E⟦i⟧, f = 0, and must not read IsZero (E ⟶ E⟦i⟧). That Hom is a bare Type; IsZero there demands an object both initial and terminal, and Type has none, so the field would be unsatisfiable, the structure uninhabitable, and every theorem below vacuously true — while compiling and passing every gate. AlgebraicGeometry/Surface/Spherical.lean records the same trap; the spelling is copied from it deliberately.

What is not here

No Serre-duality argument deriving top_one from end_one: the two clauses stay independent, as they do in the K3-specific profile. The twist itself, the Mukai lattice and the braid relation are their own files.

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

An n-spherical object, with no Serre functor in sight.

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

  Hom(E, E⟦i⟧) = 0 away from degrees 0 and n. Stated as "every morphism is zero"; see the trap in the module docstring.

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

  End(E) ≅ k: the object is simple.

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

  Hom(E, E⟦n⟧) ≅ k. Independent of end_one at this generality.

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

A spherical object is nonzero: a zero object has a subsingleton endomorphism space, and end_one would make the field one too.

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

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

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

theorem CategoryTheory.Triangulated.SphericalTwist.IsSphericalObject.finrank_shift_zero {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {n : ℤ} {E : C} (h : IsSphericalObject k n E) : Module.finrank k (E ⟶ (shiftFunctor C 0).obj E) = 1

Hom(E, E⟦0⟧) is the base field too. The zero shift is not syntactically the identity, so the endomorphism statement does not apply to it directly.

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

Sphericity transports along an isomorphism.

theorem CategoryTheory.Triangulated.SphericalTwist.chiHom_self_eq {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {n : ℤ} {E : C} (h : IsSphericalObject k n E) (hn : n ≠ 0) : chiHom k C E E = 1 + ↑n.negOnePow

The Euler characteristic of a spherical object, χ(E,E) = 1 + (-1)ⁿ.

The support of i ↦ (-1)ⁱ · dim Hom(E, E⟦i⟧) sits inside {0, n}, so the finsum is a two-term sum — and it is two terms only because n ≠ 0. See the trap in the module docstring: without hn the statement is false at n = 0, not vacuous.

No HomFiniteBounded hypothesis: sphericity bounds the support by itself.

theorem CategoryTheory.Triangulated.SphericalTwist.chiHom_self_eq_one_of_zero {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {E : C} (h : IsSphericalObject k 0 E) : chiHom k C E E = 1

The degenerate value the hypothesis of chiHom_self_eq rules out.

theorem CategoryTheory.Triangulated.SphericalTwist.chiK₀_of_self_eq_two {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {E : C} [HomFiniteBounded k C] [∀ (m : ℤ), Functor.Linear k (shiftFunctor C m)] (h : IsSphericalObject k 2 E) : ((chiK₀ k C) (K₀.of C E)) (K₀.of C E) = 2

χ(E,E) = 2 for a 2-spherical object. This is the exact hypothesis the spherical twist's involutivity consumes, discharged rather than assumed.

theorem CategoryTheory.Triangulated.SphericalTwist.IsSphericalObject.twistK₀_involutive {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {E : C} [HomFiniteBounded k C] [∀ (m : ℤ), Functor.Linear k (shiftFunctor C m)] (h : IsSphericalObject k 2 E) : Function.Involutive ⇑(twistK₀ k C E)

The twist on K₀ is involutive at a 2-spherical object.

theorem CategoryTheory.Triangulated.SphericalTwist.IsSphericalObject.twistK₀_bijective {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {E : C} [HomFiniteBounded k C] [∀ (m : ℤ), Functor.Linear k (shiftFunctor C m)] (h : IsSphericalObject k 2 E) : Function.Bijective ⇑(twistK₀ k C E)

The twist on K₀ is bijective at a 2-spherical object.

theorem CategoryTheory.Triangulated.SphericalTwist.IsSphericalObject.of_serreFunctor {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : SerreFunctor.SerreFunctorData k C} {m : ℕ} {E : C} (h : SerreFunctor.IsSphericalObject D m E) : IsSphericalObject k (↑m) E

The Serre-relative predicate projects onto this one.

One direction only, and it must stay so: this predicate has no Serre functor, so nothing here reconstructs the S(E) ≅ E⟦n⟧ clause that is dropped.