Exceptional collections and the semiorthogonal sequence they generate

An exceptional collection is a family of exceptional objects, indexed by a preorder, whose cross-member maps vanish in the CLASSICAL direction: maps from a LATER member into any shift of an EARLIER one are zero. The theorem this lane exists for is proved here: the triangulated envelopes of the shift-closures of the members form a semiorthogonal sequence.

The classical direction, deliberately

The field hom_shift_eq_zero is the definition of the literature (this structure is an upstream candidate), and it is the OPPOSITE of the repository root's convention — the root vanishes Hom(earlier, later). The two are NOT definitionally aligned; the bridge to the root is Orientation.lean's order-reversing adapter, applied in toSemiorthogonalSequence. No file should restate the flip.

One meaning of generation

component i is the triangulated envelope of the shift closure of the singleton at obj i, and that is the ONLY component convention: Mathlib's shiftClosure already closes under isomorphism, and defining a second generator-level component would create two meanings of generation. The repository's Triangulated.ExtensionClosure is not used, for the reason the projective-families reconnaissance rejected it: it proves neither shift stability nor retract closure.

What is deliberately out of scope

Admissibility of component i needs finite-dimensional Hom-spaces (AlgebraicGeometry/Modules/Coherent/Linear.lean, issue #332) and is not claimed. Mutation is not filed in this milestone. Beilinson's collection O, O(1), …, O(n) on P^n, its fullness, and the decomposition of D^b(P^n) land in AlgebraicGeometry/ProjectiveSpectrum/** (issues #570, #586, #571, #332, #806, #833, #824–#828) and are deliberately NOT touched here; the concrete inhabitant of this structure is the D^b(field) example of the next issue in this lane.

Main definitions

• ExceptionalCollection — the structure, classical direction.
• ExceptionalCollection.IsStrong — an independent predicate, not a field.
• ExceptionalCollection.component — the envelope of the shift closure.
• ExceptionalCollection.toSemiorthogonalSequence — the image in the root, through Orientation.lean's adapter; toSemiorthogonalSequenceFin lands the finite case back on Fin n.
• ExceptionalCollection.ofExceptional and ExceptionalCollection.reindex — the two honest producers of the structure.

Main results

• ExceptionalCollection.semiorthogonal_component — the envelopes are semiorthogonal in the classical direction; the proof peels both envelopes with triangEnvelope_le_iff against the orthogonals' triangulated and retract-stability instances.
• ObjectProperty.rightOrthogonal_isStableUnderRetracts and its left dual — two short lemmas absent from the pinned Mathlib (the only files mentioning rightOrthogonal there prove no retract stability); flagged as upstream candidates.

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 collection, semiorthogonal decomposition, triangulated envelope

structure CategoryTheory.Triangulated.ExceptionalCollection (k : Type u_1) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (ι : Type w) [Preorder ι] : Type (max u w)

An exceptional collection: exceptional objects indexed by a preorder, with cross-member vanishing in the CLASSICAL direction — maps from a later member into any shift of an earlier one are zero. This is the reverse of the repository root's convention; toSemiorthogonalSequence bridges through Orientation.lean's adapter, and the two conventions are not definitionally aligned.

• obj : ι → C

  The members of the collection.

• exceptional (i : ι) : IsExceptional k (self.obj i)

  Each member is exceptional.

• hom_shift_eq_zero ⦃i j : ι⦄ : i < j → ∀ (n : ℤ) (f : self.obj j ⟶ (shiftFunctor C n).obj (self.obj i)), f = 0

  Maps from a later member into any shift of an earlier one vanish.

def CategoryTheory.Triangulated.ExceptionalCollection.IsStrong {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) : Prop

A collection is strong when maps between any two members into nonzero shifts vanish, in both index directions. An independent predicate, not a field, matching the root's discipline for IsFull. Its content beyond the structure's fields is the i < j case alone: j < i already follows from hom_shift_eq_zero and i = j from exceptional.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Triangulated.ExceptionalCollection.component {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) (i : ι) : ObjectProperty C

The component generated by a member: the triangulated envelope of the shift closure of the singleton. shiftClosure already closes under isomorphism, so no isoClosure wrapper appears; shift stability of the component is Mathlib's global envelope instance. Deliberately an abbrev: instance search must see through to triangEnvelope to find IsStableUnderShift ℤ, hence IsTriangulated of the orthogonals, which triangEnvelope_le_iff demands in semiorthogonal_component.

Equations

• E.component i = (CategoryTheory.ObjectProperty.shiftClosure (fun (X : C) => X = E.obj i) ℤ).triangEnvelope

theorem CategoryTheory.Triangulated.ExceptionalCollection.obj_mem_component {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) (i : ι) : E.component i (E.obj i)

The generating member lies in its own component: it is in the shift closure at shift 0, hence in the envelope.

theorem CategoryTheory.Triangulated.ExceptionalCollection.component_nonempty {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) (i : ι) : (E.component i).Nonempty

The envelope-level nonemptiness of a component. Note that Mathlib's instance [P.Nonempty] [IsTriangulated C] : P.triangEnvelope.IsTriangulated consumes nonemptiness of the generator, not of the envelope — which is why hasTriangulatedComponents supplies its own generator-level witness — so this is the exported form for downstream consumers, not that instance's input.

theorem CategoryTheory.Triangulated.ExceptionalCollection.hom_shift_shift_eq_zero {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) ⦃i j : ι⦄ (hij : i < j) (a b : ℤ) (f : (shiftFunctor C a).obj (E.obj j) ⟶ (shiftFunctor C b).obj (E.obj i)) : f = 0

Cross-member vanishing between arbitrary shifts, transported from the collection's field by conjugating with the shift by -b — the two-object form of IsExceptional.hom_shift_shift_eq_zero's argument.

theorem CategoryTheory.Triangulated.ExceptionalCollection.semiorthogonal_component {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) ⦃i j : ι⦄ (hij : i < j) : E.component i ≤ (E.component j).rightOrthogonal

The envelopes are semiorthogonal in the classical direction. The proof peels the two triangulated envelopes in turn with triangEnvelope_le_iff — first against (component j).rightOrthogonal, then against the left orthogonal of the earlier member's shift closure — using the orthogonals' triangulated instances and the retract-stability instances above; what remains is the transported cross-member vanishing.

def CategoryTheory.Triangulated.ExceptionalCollection.toSemiorthogonalSequence {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) : SemiorthogonalSequence C ιᵒᵈ

The collection's image in the repository root, through Orientation.lean's order-reversing adapter.

Equations

• E.toSemiorthogonalSequence = CategoryTheory.Triangulated.SemiorthogonalSequence.ofReverse E.component ⋯

@[simp]

theorem CategoryTheory.Triangulated.ExceptionalCollection.toSemiorthogonalSequence_component {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) (i : ιᵒᵈ) : E.toSemiorthogonalSequence.component i = E.component (OrderDual.ofDual i)

def CategoryTheory.Triangulated.ExceptionalCollection.IsFull {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) : Prop

The root's classical fullness, on the collection's image. A definition by reuse: no second fullness notion appears.

Equations

• E.IsFull = E.toSemiorthogonalSequence.IsFull

def CategoryTheory.Triangulated.ExceptionalCollection.IsStronglyFull {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) : Prop

The root's strong fullness, on the collection's image.

Equations

• E.IsStronglyFull = E.toSemiorthogonalSequence.IsStronglyFull

theorem CategoryTheory.Triangulated.ExceptionalCollection.IsStronglyFull.isFull {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] {E : ExceptionalCollection k C ι} (h : E.IsStronglyFull) : E.IsFull

theorem CategoryTheory.Triangulated.ExceptionalCollection.hasTriangulatedComponents {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) [IsTriangulated C] : E.toSemiorthogonalSequence.HasTriangulatedComponents

Every component is triangulated, from Mathlib's envelope instance — which demands nonemptiness, supplied by component_nonempty, and [IsTriangulated C].

def CategoryTheory.Triangulated.ExceptionalCollection.ofExceptional {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {E : C} (h : IsExceptional k E) : ExceptionalCollection k C PUnit.{u_2 + 1}

A single exceptional object is a collection over PUnit: the cross-member condition is vacuous because PUnit has no strict inequality. One of the two honest producers of this structure.

Equations

• CategoryTheory.Triangulated.ExceptionalCollection.ofExceptional h = { obj := fun (x : PUnit.{?u.1 + 1}) => E, exceptional := ⋯, hom_shift_eq_zero := ⋯ }

def CategoryTheory.Triangulated.ExceptionalCollection.reindex {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) {κ : Type u_2} [Preorder κ] (f : κ → ι) (hf : ∀ ⦃a b : κ⦄, a < b → f a < f b) : ExceptionalCollection k C κ

Restrict a collection along a strictly monotone map of index types — the second producer. The unfolded strict-monotonicity binder matches the shape the root's reindex established rather than StrictMono.

Equations

• E.reindex f hf = { obj := E.obj ∘ f, exceptional := ⋯, hom_shift_eq_zero := ⋯ }

theorem CategoryTheory.Triangulated.ExceptionalCollection.reindex_toSemiorthogonalSequence {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] (E : ExceptionalCollection k C ι) {κ : Type u_2} [Preorder κ] (f : κ → ι) (hf : ∀ ⦃a b : κ⦄, a < b → f a < f b) : (E.reindex f hf).toSemiorthogonalSequence = E.toSemiorthogonalSequence.reindex (fun (i : κᵒᵈ) => OrderDual.toDual (f (OrderDual.ofDual i))) ⋯

Reindexing commutes with passage to the root, as an equality of semiorthogonal sequences — through the root's own reindex, not a second one.

def CategoryTheory.Triangulated.ExceptionalCollection.toSemiorthogonalSequenceFin {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {n : ℕ} (F : ExceptionalCollection k C (Fin n)) : SemiorthogonalSequence C (Fin n)

The finite case, landed back on Fin n through Orientation.lean's ofReverseFin: component i of the result is the collection's component i.rev.

Equations

• F.toSemiorthogonalSequenceFin = CategoryTheory.Triangulated.SemiorthogonalSequence.ofReverseFin n F.component ⋯

@[simp]

theorem CategoryTheory.Triangulated.ExceptionalCollection.toSemiorthogonalSequenceFin_component {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {n : ℕ} (F : ExceptionalCollection k C (Fin n)) (i : Fin n) : F.toSemiorthogonalSequenceFin.component i = F.component i.rev

theorem CategoryTheory.Triangulated.ExceptionalCollection.hasTriangulatedComponentsFin {k : Type u_1} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {n : ℕ} (F : ExceptionalCollection k C (Fin n)) [IsTriangulated C] : F.toSemiorthogonalSequenceFin.HasTriangulatedComponents

Every component of the finite sequence is triangulated. This is the Fin n counterpart of hasTriangulatedComponents; it is stated separately because toSemiorthogonalSequenceFin lands back in the original finite order rather than in OrderDual (Fin n).