Exceptional objects in a k-linear pretriangulated category

An object E is exceptional when it has no self-maps into a nonzero shift and its endomorphism ring is exactly the base field. This file defines the predicate and proves the theorems that consume each clause, so that neither clause ships as decoration: every endomorphism is a scalar multiple of the identity, an exceptional object is nonzero, its endomorphism ring has no idempotents besides 0 and 1, it is not isomorphic to any nonzero shift of itself, and every map between two distinct shifts of it vanishes.

Why algebraMap bijectivity rather than a bundled isomorphism

The endomorphism clause is Function.Bijective (algebraMap k (End E)), against Mathlib's Algebra k (End E) instance from Mathlib/CategoryTheory/Linear/Basic.lean. Bijectivity is proposition-valued, so two proofs of exceptionality of the same object are equal and no second carrier appears; a bundled k ≃ₐ[k] End E would be data. Per docs/architecture/abstraction-tree.md, no KLinearCategory or other new linearity class is introduced — Mathlib's Preadditive and Linear carry everything.

The trap the vanishing clause avoids

The clause is ∀ f : E ⟶ E⟦n⟧, f = 0, never IsZero (E ⟶ E⟦n⟧) on a bare Type: the latter would compile, pass every gate, and make the structure uninhabitable, because IsZero there speaks about a zero object of Type, not about the zero morphism.

Transport hypotheses are assumptions at this pin

IsExceptional.shift carries [∀ n : ℤ, (shiftFunctor C n).Linear k] explicitly: k-linearity of the shift is not derivable from [Linear k C] [Pretriangulated C] at this pin — Mathlib/CategoryTheory/Shift/Linear.lean:30 carries the same instance argument, and the only global instances of that shape in the library are for DerivedCategory and for localizations. Without it the ring isomorphism End (E⟦m⟧) ≅ End E is not a k-algebra map and bijectivity of algebraMap does not transport. of_equivalence likewise assumes [e.functor.Linear k].

Main definitions

• IsExceptional — the predicate. Its fields consume only [Preadditive C] [Linear k C] [HasShift C ℤ], so the predicate is statable before a category's triangulation is assembled; the pretriangulated setting of the title is where the notion lives mathematically, not a requirement of the definition.

Main results

• IsExceptional.end_eq_smul_id, IsExceptional.not_isZero, IsExceptional.end_eq_zero_or_eq_one_of_mul_self — the endomorphism clause at work: scalars, nonvanishing, and indecomposability in element form.
• IsExceptional.not_nonempty_iso_shift, IsExceptional.hom_shift_shift_eq_zero — both clauses at work: no shift periodicity, and vanishing between distinct shifts.
• IsExceptional.shift, IsExceptional.of_equivalence — transport.
• CategoryTheory.algebraMap_end_apply — the smul unfolding of algebraMap into an endomorphism ring, a pure linear-category fact.

References

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

Tags

exceptional object, semiorthogonal decomposition, linear category

theorem CategoryTheory.algebraMap_end_apply {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type u_1} [CommSemiring R] [Linear R C] (c : R) (E : C) : (algebraMap R (End E)) c = c • CategoryStruct.id E

The algebraMap into an endomorphism ring, unfolded to the smul form every later proof works with. A pure linear-category fact — no shift or triangulation enters — discharged from Algebra.algebraMap_eq_smul_one and End.one_def.

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

An exceptional object: no self-maps into a nonzero shift, and endomorphism ring exactly the base field. See the module docstring for why the second clause is algebraMap bijectivity rather than a bundled algebra isomorphism, and why the first is ∀ f, f = 0 rather than an IsZero.

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

  Every self-map into a nonzero shift vanishes.

• algebraMap_bijective : Function.Bijective ⇑(algebraMap k (End E))

  The base field exhausts the endomorphism ring.

theorem CategoryTheory.Triangulated.IsExceptional.end_eq_smul_id {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) (f : End E) : ∃ (c : k), f = c • CategoryStruct.id E

Every endomorphism of an exceptional object is a scalar multiple of the identity — surjectivity of algebraMap, read through algebraMap_end_apply.

theorem CategoryTheory.Triangulated.IsExceptional.not_isZero {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) : ¬Limits.IsZero E

An exceptional object is nonzero: a zero object has End = 0, so algebraMap would identify 1 and 0 in k, against injectivity.

theorem CategoryTheory.Triangulated.IsExceptional.end_eq_zero_or_eq_one_of_mul_self {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) (e : End E) (he : e * e = e) : e = 0 ∨ e = 1

The endomorphism ring of an exceptional object has no idempotents besides 0 and 1: transport the idempotent along the algebra bijection and use that a field has only trivial idempotents. This is indecomposability in the element form a mutation or decomposition argument consumes; no abstract Indecomposable class is introduced, because nothing here would inhabit it.

theorem CategoryTheory.Triangulated.IsExceptional.not_nonempty_iso_shift {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) (n : ℤ) (hn : n ≠ 0) : ¬Nonempty (E ≅ (shiftFunctor C n).obj E)

An exceptional object is not isomorphic to any nonzero shift of itself: the forward half of such an isomorphism vanishes by the shift clause, so 𝟙 E = e.hom ≫ e.inv = 0 and E is zero, against not_isZero.

theorem CategoryTheory.Triangulated.IsExceptional.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 ℤ] {E : C} (h : IsExceptional k E) (a b : ℤ) (hab : a ≠ b) (f : (shiftFunctor C a).obj E ⟶ (shiftFunctor C b).obj E) : f = 0

Every map between two distinct shifts of an exceptional object vanishes. Obtained by transporting to E ⟶ E⟦b - a⟧ along the shift by -a; this needs only that shiftFunctor C (-a) is an equivalence, not linearity or additivity, and it is the exact form the collection layer consumes.

theorem CategoryTheory.Triangulated.IsExceptional.shift {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) [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (m : ℤ) : IsExceptional k ((shiftFunctor C m).obj E)

Exceptionality transports along shifts. k-linearity of the shift is an explicit hypothesis at this pin — see the module docstring — because without it algebraMap bijectivity does not move: the transport identifies algebraMap into End (E⟦m⟧) with the shift functor's action on End E, which is a k-algebra map only when the functor is k-linear.

theorem CategoryTheory.Triangulated.IsExceptional.of_equivalence {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) {D : Type u_2} [Category.{v, u_2} D] [Preadditive D] [Linear k D] [HasShift D ℤ] (e : C ≌ D) [e.functor.CommShift ℤ] [e.functor.Additive] [Functor.Linear k e.functor] : IsExceptional k (e.functor.obj E)

Exceptionality transports along a shift-commuting k-linear equivalence. The functor's linearity is an assumption for the same reason as in shift. Nothing else is assumed of the target: neither clause consumes a triangulation, additivity of the target's shifts, or a zero object, so the adapter is usable before any of those are assembled — which is also why the issue's [e.functor.IsTriangulated] hypothesis is deliberately absent.