An exceptional object in the derived category of a field

The abstract layer gets its real inhabitant: the residue field, as a complex concentrated in degree zero, is an exceptional object of DerivedCategory (ModuleCat k), and it assembles into a length-one exceptional collection with its semiorthogonal sequence. This discharges the design note's requirement — .claude/notes/2026-08-28-semiorthogonal-reconnaissance.md §4: "issue #852 requires those notions to be added only when a theorem consumes each property" — for this milestone, with a non-geometric consumer that leaves the projective-families lane's territory untouched.

Why this category

Mathlib/Algebra/Homology/DerivedCategory/Linear.lean provides noncomputable instance : Linear R (DerivedCategory C) and instance (n : ℤ) : (shiftFunctor (DerivedCategory C) n).Linear R — the latter is exactly the shift-linearity hypothesis IsExceptional.shift had to assume in general, and the derived category is one of the few places in Mathlib where it is a global instance. HasDerivedCategory.{w} (ModuleCat k) is a hypothesis throughout; HasDerivedCategory.standard supplies it at max u v for C : Type u with Category.{v} C — here u + 1, since ModuleCat.{u} k : Type (u + 1) — when a caller needs a concrete choice.

Fullness is not claimed — and is expected to be false

ObjectProperty.triangEnvelope reaches only objects assembled from the generator by shifts, binary products, retracts, and FINITELY many extension steps (triangEnvelope = ⨆ n, triangEnvelopeIter n). An object of the unbounded DerivedCategory (ModuleCat k) with infinitely many nonzero cohomology objects is not reachable that way, so IsFull for the length-one collection is expected to be FALSE here, not merely unproved. Fullness belongs to a bounded-derived-category consumer, which this milestone does not file.

Main definitions

• residueObject — the field in degree zero.
• residueObjectExceptionalCollection — the length-one collection over PUnit, through ExceptionalCollection.ofExceptional.

Main results

• isExceptional_residueObject — exceptionality, in three parts: endomorphisms through the fully faithful k-linear singleFunctor and End(k) = k; positive shifts through projectivity of k and the vanishing of higher Ext; negative shifts through the canonical t-structure.
• ModuleCat.algebraMap_end_self_bijective — the base case: evaluation at 1 inverts algebraMap into the linear endomorphisms of the ring itself.
• residueObjectExceptionalCollection_component — the single component is the envelope of the shift closure of the residue object.

References

• Bondal, Representations of associative algebras and coherent sheaves, Izv. Akad. Nauk SSSR (1989).
• Huybrechts, Fourier–Mukai Transforms in Algebraic Geometry, §1.4.

Tags

exceptional object, derived category, residue field

theorem CategoryTheory.ModuleCat.algebraMap_end_self_bijective (R : Type u) [CommRing R] : Function.Bijective ⇑(algebraMap R (End (ModuleCat.of R R)))

algebraMap into the linear endomorphisms of the ring itself is bijective: evaluation at 1 inverts it. The base case the derived-category transport stands on; only commutativity enters, so a CommRing suffices.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.residueObject (k : Type u) [Field k] [HasDerivedCategory (ModuleCat k)] : DerivedCategory (ModuleCat k)

The residue field, as a complex concentrated in degree zero. Deliberately an abbrev: instance search must see the singleFunctor application to find the t-structure IsLE/IsGE instances the negative-shift argument consumes.

Equations

• CategoryTheory.Triangulated.residueObject k = (DerivedCategory.singleFunctor (ModuleCat k) 0).obj (ModuleCat.of k k)

theorem CategoryTheory.Triangulated.isExceptional_residueObject (k : Type u) [Field k] [HasDerivedCategory (ModuleCat k)] : IsExceptional k (residueObject k)

The residue field in degree zero is exceptional. Endomorphisms: singleFunctor is fully faithful and k-linear, so algebraMap bijectivity transports from End(k) = k. Positive shifts: k is projective, so higher Ext vanishes, read through Ext.homEquiv. Negative shifts: the source is IsLE 0 and the shifted target IsGE (-n) for the canonical t-structure, so the map vanishes by TStructure.zero.

noncomputable def CategoryTheory.Triangulated.residueObjectExceptionalCollection (k : Type u) [Field k] [HasDerivedCategory (ModuleCat k)] : ExceptionalCollection k (DerivedCategory (ModuleCat k)) PUnit.{u_1 + 1}

The length-one exceptional collection on the residue object — the honest inhabitant of ExceptionalCollection in the tree, through ofExceptional. Its semiorthogonal sequence exists by the collection layer; fullness is not claimed, and is expected to fail — see the module docstring.

Equations

• CategoryTheory.Triangulated.residueObjectExceptionalCollection k = CategoryTheory.Triangulated.ExceptionalCollection.ofExceptional ⋯

@[simp]

theorem CategoryTheory.Triangulated.residueObjectExceptionalCollection_component (k : Type u) [Field k] [HasDerivedCategory (ModuleCat k)] : (residueObjectExceptionalCollection k).component PUnit.unit = (ObjectProperty.shiftClosure (fun (X : DerivedCategory (ModuleCat k)) => X = residueObject k) ℤ).triangEnvelope

The single component of the length-one collection is the triangulated envelope of the shift closure of the residue object.