A twist-shaped autoequivalence acts on stability conditions by the reflection

This connects the lattice half of the spherical-twist lane to the stability machinery: an autoequivalence whose action on K₀ is the twist τ_E becomes a group element acting on WithClassMap C v, and that action is transport along the Mukai reflection ρ_{v(E)}.

It is the precise form of "the spherical twist acts on Stab(X) through the reflection" that is available before the twist is constructed.

Nothing here constructs a twist

TwistShaped is supplied data and is named to say so. It carries an autoequivalence together with the hypothesis that its K₀ action is twistK₀. That is the property T_E will have once it exists; building T_E is a separate lane, and no inhabitant of TwistShaped is produced here.

Two things not to conclude

The quotient is not Aut(D). AutPairQuot quotients by a bare natural isomorphism of underlying functors, leaving the CommShift datum unconstrained, so it is a priori coarser than exact autoequivalences up to isomorphism of exact functors. Slicing/Quotient.lean says this explicitly. No statement here is about Aut(Dᵇ(X)).

The order-two statement is about the lattice, not the functor. reflect_reflect makes lam an involution, so the class of a twist-shaped pair squares to one whose lattice part is the identity. It does not follow that T_E has order two in any automorphism group — it does not; T_E has infinite order. τ_E being an involution on K₀ says nothing about the functor.

Why [IsTriangulated C] is in the variable block

GroupAction.AutPair is declared under a section carrying it, so it does not arrive from the sphericity hypotheses: chiK₀ and twistK₀ need only the pretriangulated structure, and EulerForm.lean's variable list omits it. Leaving it out makes AutPair fail to elaborate here for a reason that looks unrelated to the mathematics.

structure CategoryTheory.Triangulated.SphericalTwist.TwistShaped {k : Type w} [DivisionRing 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 : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} (R : MukaiRealization k C b) (E : C) : Type (max u v)

An autoequivalence shaped like the twist at E.

Supplied, not constructed: the K₀ action is asserted to be twistK₀. Φ is a TriEquiv rather than a bare C ≌ C precisely so that its additivity, shift-compatibility and triangulatedness travel as instances, which is what makes K₀.map Φ.e.functor well-formed.

• Φ : WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv C

  The autoequivalence, with its instances alongside.

• map_eq : K₀.map self.Φ.e.functor = twistK₀ k C E

  Its action on K₀ is the twist. This is the whole content of "twist-shaped".

• chi_self : ((chiK₀ k C) (K₀.of C E)) (K₀.of C E) = 2

  Sphericity, in the only form this file needs.

theorem CategoryTheory.Triangulated.SphericalTwist.TwistShaped.map_inverse_eq {k : Type w} [DivisionRing 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 : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) : K₀.map T.Φ.e.inverse = twistK₀ k C E

The inverse acts by the twist too.

Not free, and not waved at. K₀.map_congr on the unit isomorphism upgrades "Φ⁻¹ ∘ Φ is naturally isomorphic to the identity" into an equality of maps on K₀; composing that with map_eq and involutivity of twistK₀ identifies the inverse's action.

theorem CategoryTheory.Triangulated.SphericalTwist.TwistShaped.isSpherical_v {k : Type w} [DivisionRing 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 : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) : Mukai.IsSpherical b (R.v (K₀.of C E))

The Mukai vector of E is spherical, from chi_self through the realization.

noncomputable def CategoryTheory.Triangulated.SphericalTwist.TwistShaped.lam {k : Type w} [DivisionRing 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 : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) : Mukai.MukaiLattice N ≃+ Mukai.MukaiLattice N

The lattice automorphism attached to a twist-shaped pair: the Mukai reflection in v(E).

Equations

• T.lam = (Mukai.reflectEquiv b (R.v (CategoryTheory.Triangulated.K₀.of C E)) ⋯).toAddEquiv

theorem CategoryTheory.Triangulated.SphericalTwist.TwistShaped.compat {k : Type w} [DivisionRing 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 : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) (x : K₀ C) : R.v ((K₀.map T.Φ.e.inverse) x) = T.lam (R.v x)

The compatibility AutPair asks for. v ∘ K₀(Φ⁻¹) = ρ ∘ v, which is map_inverse_eq followed by map_twistK₀.

noncomputable def CategoryTheory.Triangulated.SphericalTwist.TwistShaped.toAutPair {k : Type w} [DivisionRing 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 : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) : WeakStabilityCondition.StabilityCondition.GroupAction.AutPair R.v

The group element.

Equations

• T.toAutPair = { Φ := T.Φ, lam := T.lam, compat := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.SphericalTwist.TwistShaped.toAutPair_lam {k : Type w} [DivisionRing 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 : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) : T.toAutPair.lam = T.lam

@[simp]

theorem CategoryTheory.Triangulated.SphericalTwist.TwistShaped.toAutPair_Φ {k : Type w} [DivisionRing 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 : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) : T.toAutPair.Φ = T.Φ

theorem CategoryTheory.Triangulated.SphericalTwist.TwistShaped.act_eq {k : Type w} [DivisionRing 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] [IsTriangulated C] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) (σ : StabilityCondition.WithClassMap C R.v) : WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.mk T.toAutPair • σ = actStabAut T.Φ.e R.v T.lam.toAddMonoidHom ⋯ σ

The action is transport along the reflection. The existing actStabAut is reused, not restated; this records that the group element built here is the one that transport describes.

theorem CategoryTheory.Triangulated.SphericalTwist.TwistShaped.act_slicing {k : Type w} [DivisionRing 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] [IsTriangulated C] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) (σ : StabilityCondition.WithClassMap C R.v) : (WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.mk T.toAutPair • σ).slicing = σ.slicing.mapEquiv T.Φ.e

The slicing moves by the autoequivalence. Reuses the existing simp lemma.

theorem CategoryTheory.Triangulated.SphericalTwist.TwistShaped.act_Z {k : Type w} [DivisionRing 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] [IsTriangulated C] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) (σ : StabilityCondition.WithClassMap C R.v) (x : Mukai.MukaiLattice N) : (WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.mk T.toAutPair • σ).Z x = σ.Z (T.lam x)

The charge is precomposed with the reflection.

theorem CategoryTheory.Triangulated.SphericalTwist.TwistShaped.lam_lam {k : Type w} [DivisionRing 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 : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFiniteBounded k C] {N : Type u_1} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} {R : MukaiRealization k C b} {E : C} (T : TwistShaped R E) (x : Mukai.MukaiLattice N) : T.lam (T.lam x) = x

The order-two statement, at the level the quotient supports.

The lattice part of the square is the identity, by reflect_reflect. Read the module docstring before generalising this: it is a statement about lam, not about Φ, and T_E does not have order two in any automorphism group.