Mutation triangles and projection chains

A right-admissible triangulated subcategory has two related forms of data. The proposition-valued form says that a right adjoint to its inclusion exists; the chosen form records that right adjoint and its adjunction. This file connects the two and constructs the objectwise counit triangle

i i⁽!⁾ X ⟶ X ⟶ L_P(X).

The third vertex is in P.rightOrthogonal. This is the objectwise mutation triangle available in every triangulated category. It deliberately does not claim a mutation functor: making the cone functorial is enhancement-level data and is one of the jobs of the dg lane (#855, #853, #854).

The second half is the formal engine behind Paper II, Remark 2.3(ii). If successive members of a block are joined by distinguished triangles whose third vertices are killed by the residual projection, then the projected successive map is an isomorphism. Iterating gives the same residual projection for every member of the block, not only its first member.

structure CategoryTheory.ObjectProperty.RightProjectionData.CounitTriangle {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} (Q : P.RightProjectionData) (X : C) : Type (max u v)

The objectwise counit triangle of a chosen right projection.

The first map is fixed to be the adjunction counit. The third vertex and the remaining maps are chosen from the triangulated-category axiom; the last field is the genuine mutation conclusion that this vertex lies in the right orthogonal of the projected component.

• mutation : C

  The mutation object, i.e. a cone of the projection counit.

• toMutation : X ⟶ self.mutation

  The second map of the counit triangle.

• connecting : self.mutation ⟶ (shiftFunctor C 1).obj (Q.projectObj X)

  The connecting map of the counit triangle.

• distinguished : Pretriangulated.Triangle.mk (Q.counitApp X) self.toMutation self.connecting ∈ Pretriangulated.distinguishedTriangles

  The counit triangle is distinguished.

• mutation_mem : P.rightOrthogonal self.mutation

  The mutation object is right orthogonal to the projected component.

noncomputable def CategoryTheory.ObjectProperty.RightProjectionData.counitTriangle {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} (Q : P.RightProjectionData) (hP : P.IsTriangulated) (X : C) : Q.CounitTriangle X

Construct the objectwise mutation triangle of a chosen right projection.

The proof that the cone lies in P.rightOrthogonal applies the right adjoint to the counit triangle. Full faithfulness of the inclusion makes the mapped counit invertible, so the mapped cone is zero; adjunction then kills every map from a P-object to the original cone.

Equations

• Q.counitTriangle hP X = { mutation := ⋯.choose, toMutation := ⋯.choose, connecting := ⋯.choose, distinguished := ⋯, mutation_mem := ⋯ }

theorem CategoryTheory.ObjectProperty.RightProjectionData.projectMap_isIso_of_distinguished {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} (Q : P.RightProjectionData) (hP : P.IsTriangulated) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) (hZ : P.rightOrthogonal Z) : IsIso (Q.projection.map f)

A morphism whose cone is right orthogonal to P becomes an isomorphism after applying the right projection onto P.

noncomputable def CategoryTheory.ObjectProperty.RightProjectionData.projectMapIsoOfDistinguished {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} (Q : P.RightProjectionData) (hP : P.IsTriangulated) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) (hZ : P.rightOrthogonal Z) : Q.project X ≅ Q.project Y

The isomorphism of projections induced by a distinguished triangle whose third vertex is killed by the projection.

Equations

• Q.projectMapIsoOfDistinguished hP f g h hT hZ = CategoryTheory.asIso (Q.projection.map f)

structure CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.ProjectionChainData {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] {I : Type t} (B : OrthogonalExceptionalBlocks k C I) (P : ObjectProperty C) : Type (max (max t u) v)

Distinguished triangles comparing consecutive members of every exceptional block, with cones killed by the residual projection.

For the Enriques application the third vertex is the sheaf on the intervening (-2)-curve. The generic root only records the exact categorical condition which the same-projection proof consumes.

• stepMap (i : I) (j : ℕ) (hj : j + 1 < B.length i) : (B.collection i).obj ⟨j, ⋯⟩ ⟶ (B.collection i).obj ⟨j + 1, hj⟩

  The map from position j to position j+1.

• cone (i : I) (j : ℕ) (_hj : j + 1 < B.length i) : C

  A cone of each successive map.

• toCone (i : I) (j : ℕ) (hj : j + 1 < B.length i) : (B.collection i).obj ⟨j + 1, hj⟩ ⟶ self.cone i j hj

  The second map in each successive triangle.

• connecting (i : I) (j : ℕ) (hj : j + 1 < B.length i) : self.cone i j hj ⟶ (shiftFunctor C 1).obj ((B.collection i).obj ⟨j, ⋯⟩)

  The connecting map in each successive triangle.

• distinguished (i : I) (j : ℕ) (hj : j + 1 < B.length i) : Pretriangulated.Triangle.mk (self.stepMap i j hj) (self.toCone i j hj) (self.connecting i j hj) ∈ Pretriangulated.distinguishedTriangles

  Each successive triangle is distinguished.

• cone_mem (i : I) (j : ℕ) (hj : j + 1 < B.length i) : P.rightOrthogonal (self.cone i j hj)

  Every successive cone is killed by the residual projection.

noncomputable def CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.ProjectionChainData.stepProjectionIso {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] {I : Type t} (B : OrthogonalExceptionalBlocks k C I) (P : ObjectProperty C) (Q : P.RightProjectionData) (A : B.ProjectionChainData P) (hP : P.IsTriangulated) (i : I) (j : ℕ) (hj : j + 1 < B.length i) : Q.project ((B.collection i).obj ⟨j, ⋯⟩) ≅ Q.project ((B.collection i).obj ⟨j + 1, hj⟩)

Consecutive members of a block have isomorphic residual projections.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.ProjectionChainData.projectionIsoFromFirst {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] {I : Type t} (B : OrthogonalExceptionalBlocks k C I) (P : ObjectProperty C) (Q : P.RightProjectionData) (A : B.ProjectionChainData P) (hP : P.IsTriangulated) (i : I) (j : ℕ) (hj : j < B.length i) : Q.project (B.firstObject i) ≅ Q.project ((B.collection i).obj ⟨j, hj⟩)

Iterate the successive projection isomorphisms from the first member to the member at natural-number position j.

Equations

• One or more equations did not get rendered due to their size.
• CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.ProjectionChainData.projectionIsoFromFirst B P Q A hP i 0 x_2 = CategoryTheory.Iso.refl (Q.project (B.firstObject i))

noncomputable def CategoryTheory.Triangulated.OrthogonalExceptionalBlocks.ProjectionChainData.projectionIso {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] {I : Type t} (B : OrthogonalExceptionalBlocks k C I) (P : ObjectProperty C) (Q : P.RightProjectionData) (A : B.ProjectionChainData P) (hP : P.IsTriangulated) (i : I) (j : Fin (B.length i)) : Q.project (B.firstObject i) ≅ Q.project ((B.collection i).obj j)

Same-projection theorem for every member of every block.

This is Paper II, Remark 2.3(ii), in the exact generality used by the extension argument: the residual projection of every Lᵢⱼ is isomorphic to the projection of Lᵢ₁.

Equations

• One or more equations did not get rendered due to their size.