Adjacent Ext profiles and shift rigidity

Inside a longer exceptional block in the non-generic Enriques argument, adjacent line bundles have derived Hom k ⊕ k[-1]: their shifted Hom spaces are one-dimensional in degrees zero and one and vanish elsewhere. Comparing this profile through a fully faithful linear functor forces two adjacent objects to carry the same shift.

This is the formal core of the t = 0 calculation in the proof of arXiv:2104.13610v2, Theorem 3.3. The geometric computation establishing the profile remains in the Enriques layer; the rigidity argument is pure linear triangulated category theory.

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

The shifted-Hom profile k ⊕ k[-1] of two adjacent members of an exceptional block.

• zero_one : Module.finrank k (E ⟶ (shiftFunctor C 0).obj F) = 1

  The degree-zero Hom space is one-dimensional.

• one_one : Module.finrank k (E ⟶ (shiftFunctor C 1).obj F) = 1

  The degree-one Hom space is one-dimensional.

• other_zero (i : ℤ) : i ≠ 0 → i ≠ 1 → Module.finrank k (E ⟶ (shiftFunctor C i).obj F) = 0

  All other shifted Hom spaces vanish.

theorem CategoryTheory.Triangulated.AdjacentExtProfile.shifts_eq_of_finrank_eq {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {E F : C} {E' F' : D} (A : AdjacentExtProfile E F) (B : AdjacentExtProfile E' F') (s t : ℤ) (hfinrank : ∀ (i : ℤ), Module.finrank k (E ⟶ (shiftFunctor C i).obj F) = Module.finrank k (E' ⟶ (shiftFunctor D (t + i - s)).obj F')) : s = t

The arithmetic heart of adjacent-shift rigidity. If the dimensions of the source shifted Homs agree with those of the target after translating by t - s, then the two shifts are equal.

theorem CategoryTheory.Triangulated.AdjacentExtProfile.shifts_eq {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {E F : C} {E' F' : D} (A : AdjacentExtProfile E F) (B : AdjacentExtProfile E' F') [∀ (n : ℤ), (shiftFunctor D n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor D n)] (G : Functor C D) [G.Additive] [Functor.Linear k G] [G.CommShift ℤ] (hG : G.FullyFaithful) (s t : ℤ) (eE : G.obj E ≅ (shiftFunctor D s).obj E') (eF : G.obj F ≅ (shiftFunctor D t).obj F') : s = t

Adjacent objects have one common shift.

If a fully faithful linear shift-compatible functor maps an adjacent source pair to an adjacent target pair with shifts s and t, then s = t.

structure CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.AdjacentExtData {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {ι : Type t} [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (B : OrthogonalExceptionalBlocks k C ι) : Prop

Adjacent Ext profiles for every consecutive pair in every exceptional block.

• profile (i : ι) (j : ℕ) (hj : j + 1 < B.length i) : AdjacentExtProfile ((B.collection i).obj ⟨j, ⋯⟩) ((B.collection i).obj ⟨j + 1, hj⟩)

  Every consecutive pair has profile k ⊕ k[-1].

Length comparison from prefix-by-prefix extension

structure CategoryTheory.Triangulated.PrefixBlockEmbeddingData {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {I : Type t} {J : Type t'} [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (B_C : OrthogonalExceptionalBlocks k C I) (B_D : OrthogonalExceptionalBlocks k D J) (e : I ≃ J) : Type t

A one-sided prefix-by-prefix matching of block members. The index equality records the output of iterating the one-step extension in order: the j-th source member is matched to the j-th target member.

• targetIndex (i : I) : Fin (B_C.length i) → Fin (B_D.length (e i))

  The target position reached by each source extension step.

• targetIndex_val (i : I) (j : Fin (B_C.length i)) : ↑(self.targetIndex i j) = ↑j

  Extension proceeds in the same order inside the two blocks.

def CategoryTheory.Triangulated.PrefixBlockEmbeddingData.embedding {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {I : Type t} {J : Type t'} [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {B_C : OrthogonalExceptionalBlocks k C I} {B_D : OrthogonalExceptionalBlocks k D J} {e : I ≃ J} (A : PrefixBlockEmbeddingData B_C B_D e) (i : I) : Fin (B_C.length i) ↪ Fin (B_D.length (e i))

The ordered member map is an embedding.

Equations

• A.embedding i = { toFun := A.targetIndex i, inj' := ⋯ }

theorem CategoryTheory.Triangulated.PrefixBlockEmbeddingData.length_le {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {I : Type t} {J : Type t'} [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {B_C : OrthogonalExceptionalBlocks k C I} {B_D : OrthogonalExceptionalBlocks k D J} {e : I ≃ J} (A : PrefixBlockEmbeddingData B_C B_D e) (i : I) : B_C.length i ≤ B_D.length (e i)

A one-sided prefix extension proves the corresponding block-length inequality.

structure CategoryTheory.Triangulated.BidirectionalPrefixBlockEmbeddingData {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {I : Type t} {J : Type t'} [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (B_C : OrthogonalExceptionalBlocks k C I) (B_D : OrthogonalExceptionalBlocks k D J) (e : I ≃ J) : Type (max t t')

Prefix extension in both directions forces exact equality of corresponding block lengths.

• forward : PrefixBlockEmbeddingData B_C B_D e

  Forward prefix extension.

• backward : PrefixBlockEmbeddingData B_D B_C e.symm

  Prefix extension after reversing the equivalence.

theorem CategoryTheory.Triangulated.BidirectionalPrefixBlockEmbeddingData.length_eq {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {I : Type t} {J : Type t'} [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {B_C : OrthogonalExceptionalBlocks k C I} {B_D : OrthogonalExceptionalBlocks k D J} {e : I ≃ J} (A : BidirectionalPrefixBlockEmbeddingData B_C B_D e) (i : I) : B_C.length i = B_D.length (e i)

Corresponding blocks have equal length. This is a theorem from the two finite prefix extensions, rather than a field supplied by the caller.

theorem CategoryTheory.Triangulated.BidirectionalPrefixBlockEmbeddingData.targetIndex_eq_cast {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {I : Type t} {J : Type t'} [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {B_C : OrthogonalExceptionalBlocks k C I} {B_D : OrthogonalExceptionalBlocks k D J} {e : I ≃ J} (A : BidirectionalPrefixBlockEmbeddingData B_C B_D e) (i : I) (j : Fin (B_C.length i)) : A.forward.targetIndex i j = Fin.cast ⋯ j

The forward prefix position is the canonical cast along length_eq.

Common shifts along a matched block

structure CategoryTheory.Triangulated.MemberwiseBlockShiftData {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {I : Type t} {J : Type t'} [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (B_C : OrthogonalExceptionalBlocks k C I) (B_D : OrthogonalExceptionalBlocks k D J) (e : I ≃ J) (length_eq : ∀ (i : I), B_C.length i = B_D.length (e i)) (G : Functor C D) : Type (max t v')

Memberwise image data after a finite extension has matched blocks of equal length. The shift is initially allowed to depend on the member; the adjacent-Ext theorem below proves that it is constant on each block.

• shift (i : I) : Fin (B_C.length i) → ℤ

  The shift initially attached to each individual member.

• objectIso (i : I) (j : Fin (B_C.length i)) : G.obj ((B_C.collection i).obj j) ≅ (shiftFunctor D (self.shift i j)).obj ((B_D.collection (e i)).obj (Fin.cast ⋯ j))

  The image of each member is the same-position target member with its initially assigned shift.

theorem CategoryTheory.Triangulated.MemberwiseBlockShiftData.shift_eq_first {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] {I : Type t} {J : Type t'} [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor D n)] [Pretriangulated D] {B_C : OrthogonalExceptionalBlocks k C I} {B_D : OrthogonalExceptionalBlocks k D J} {e : I ≃ J} {length_eq : ∀ (i : I), B_C.length i = B_D.length (e i)} {G : Functor C D} [G.Additive] [Functor.Linear k G] [G.CommShift ℤ] (M : MemberwiseBlockShiftData B_C B_D e length_eq G) (A_C : B_C.AdjacentExtData) (A_D : B_D.AdjacentExtData) (hG : G.FullyFaithful) (i : I) (j : Fin (B_C.length i)) : M.shift i j = M.shift i (B_C.firstIndex i)

Every member of a matched block has the shift of its first member.