Orthogonal blocks of exceptional objects

This file records the categorical part of the block-shaped semiorthogonal decompositions used in arXiv:2104.13610v2, Proposition 1.4 and Setup 2.5. Each block is an ordered exceptional collection; distinct blocks are completely orthogonal after taking their triangulated spans. The geometry which produces the objects or relates consecutive objects by chains of (-2)-curves does not belong in this generic root.

The span of a block is the triangulated envelope of the union of its one-object components. This is important: the union itself need not be closed under extensions. The residual property is the right orthogonal of the union of these spans, matching the convention already used by SemiorthogonalSequence.residual.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.ExceptionalCollection.span {k : Type w} [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 t} [Preorder ι] (E : ExceptionalCollection k C ι) : ObjectProperty C

The full triangulated span of an exceptional collection.

Equations

• E.span = E.toSemiorthogonalSequence.total.triangEnvelope

theorem CategoryTheory.Triangulated.ExceptionalCollection.obj_mem_span {k : Type w} [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 t} [Preorder ι] (E : ExceptionalCollection k C ι) (i : ι) : E.span (E.obj i)

Every member of an exceptional collection belongs to its full span.

theorem CategoryTheory.Triangulated.ExceptionalCollection.span_isTriangulated {k : Type w} [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 t} [Preorder ι] [Nonempty ι] [IsTriangulated C] (E : ExceptionalCollection k C ι) : E.span.IsTriangulated

The span of a nonempty exceptional collection is triangulated.

structure CategoryTheory.Triangulated.OrthogonalExceptionalBlocks (k : Type w) [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 t) : Type (max t u)

A family of mutually orthogonal exceptional blocks.

The field orthogonal is written in the right-orthogonal convention: blockSpan i ≤ (blockSpan j).rightOrthogonal says that maps from block j to block i vanish. Since the field is available for every ordered pair of distinct indices, it records orthogonality in both directions.

• length : ι → ℕ

  The positive length of each block.

• length_pos (i : ι) : 0 < self.length i

  Blocks are nonempty.

• collection (i : ι) : ExceptionalCollection k C (Fin (self.length i))

  The exceptional collection inside each block.

• orthogonal {i j : ι} : i ≠ j → (self.collection i).span ≤ (self.collection j).span.rightOrthogonal

  Distinct block spans are completely orthogonal.

def CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.firstIndex {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) (i : ι) : Fin (B.length i)

The first position in a block, available because block lengths are positive.

Equations

• B.firstIndex i = ⟨0, ⋯⟩

@[reducible, inline]

abbrev CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.firstObject {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) (i : ι) : C

The first exceptional object in a block.

Equations

• B.firstObject i = (B.collection i).obj (B.firstIndex i)

@[reducible, inline]

abbrev CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.blockSpan {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) (i : ι) : ObjectProperty C

The triangulated span of one exceptional block.

Equations

• B.blockSpan i = (B.collection i).span

def CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.total {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) : ObjectProperty C

The union of all block spans. Its right orthogonal defines the residual property below.

Equations

• B.total = ⨆ (i : ι), B.blockSpan i

def CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.residual {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) : ObjectProperty C

The residual object property of the block decomposition.

Equations

• B.residual = B.total.rightOrthogonal

@[reducible, inline]

abbrev CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.ResidualCategory {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) : Type u

The full subcategory on the residual property.

Equations

• B.ResidualCategory = B.residual.FullSubcategory

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.obj_mem_blockSpan {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) (i : ι) (j : Fin (B.length i)) : B.blockSpan i ((B.collection i).obj j)

Every member of a block belongs to that block's span.

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.obj_mem_total {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) (i : ι) (j : Fin (B.length i)) : B.total ((B.collection i).obj j)

Every member of every block belongs to the total exceptional part.

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.total_le_of_forall_obj {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) {P : ObjectProperty C} [P.IsTriangulated] [P.IsStableUnderRetracts] (hP : ∀ (i : ι) (j : Fin (B.length i)), P ((B.collection i).obj j)) : B.total ≤ P

To prove that the total exceptional part lies in a triangulated, retract-closed property, it suffices to check every member of every block.

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.length_eq_one_or_two_le {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) (i : ι) : B.length i = 1 ∨ 2 ≤ B.length i

A positive block length is either one or at least two.

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.hom_eq_zero_of_ne {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) {i j : ι} (hij : i ≠ j) {X Y : C} (hX : B.blockSpan i X) (hY : B.blockSpan j Y) (f : X ⟶ Y) : f = 0

Maps between distinct block spans vanish in either direction.

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.obj_hom_shift_eq_zero_of_ne {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) {i j : ι} (hij : i ≠ j) (a : Fin (B.length i)) (b : Fin (B.length j)) (n : ℤ) (f : (B.collection i).obj a ⟶ (shiftFunctor C n).obj ((B.collection j).obj b)) : f = 0

Maps between members of distinct exceptional blocks vanish.

def CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.toSemiorthogonalSequence {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [Preorder ι] : SemiorthogonalSequence C ι

The blocks as a root-oriented semiorthogonal sequence. Because distinct blocks are orthogonal, any preorder on their indices is permitted.

Equations

• B.toSemiorthogonalSequence = { component := B.blockSpan, semiorthogonal := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.toSemiorthogonalSequence_component {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [Preorder ι] (i : ι) : B.toSemiorthogonalSequence.component i = B.blockSpan i

@[simp]

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.toSemiorthogonalSequence_total {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [Preorder ι] : B.toSemiorthogonalSequence.total = B.total

@[simp]

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.toSemiorthogonalSequence_residual {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [Preorder ι] : B.toSemiorthogonalSequence.residual = B.residual

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.blockSpan_isTriangulated {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [IsTriangulated C] (i : ι) : (B.blockSpan i).IsTriangulated

Every block span is triangulated.

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.hasTriangulatedComponents {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [Preorder ι] [IsTriangulated C] : B.toSemiorthogonalSequence.HasTriangulatedComponents

The block sequence has triangulated components.

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.total_isStableUnderShift {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) : B.total.IsStableUnderShift ℤ

The union of the block spans is stable under every integral shift.

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.residual_isTriangulated {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) : B.residual.IsTriangulated

The residual property of orthogonal exceptional blocks is triangulated.

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.obj_hom_residual_eq_zero {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) (i : ι) (j : Fin (B.length i)) {R : C} (hR : B.residual R) (f : (B.collection i).obj j ⟶ R) : f = 0

Maps from any block object to a residual object vanish.

def CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.totalLength {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [Fintype ι] : ℕ

The total number of exceptional objects across all blocks.

Equations

• B.totalLength = ∑ i : ι, B.length i

noncomputable def CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.decompositionType {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [Fintype ι] : Multiset ℕ

The unordered block-length sequence, i.e. the type of the block-shaped decomposition in the terminology of arXiv:2104.13610v2, Definition 1.5.

Equations

• B.decompositionType = Multiset.map B.length Finset.univ.val

@[simp]

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.decompositionType_card {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [Fintype ι] : B.decompositionType.card = Fintype.card ι

@[simp]

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.decompositionType_sum {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [Fintype ι] : B.decompositionType.sum = B.totalLength

theorem CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.card_le_totalLength {k : Type w} [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 t} (B : OrthogonalExceptionalBlocks k C ι) [Fintype ι] : Fintype.card ι ≤ B.totalLength

The number of blocks is bounded by the total number of exceptional objects.