Fourier--Mukai autoequivalences acting on stability conditions

The generic KernelAutoequivalence, dual-kernel, unit, and convolution theory lives in CategoryTheory.Triangulated.FourierMukai.Autoequivalence. This specialized consumer adds only transport of Bridgeland stability conditions and the comparison with the categorical group action.

The declarations extend the canonical FourierMukai.KernelAutoequivalence namespace even though their implementation is physically owned by the stability-condition subtree.

@[reducible]

def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.toTriEquiv {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] : WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv C

The underlying triangulated autoequivalence, with its instances bundled.

Equations

• A.toTriEquiv = { e := A.equiv, fAdd := ⋯, iAdd := ⋯, fCS := inferInstance, iCS := inferInstance, fTri := ⋯, iTri := ⋯ }

noncomputable def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.actStab {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] (lam : Λ →+ Λ) (hlam : ∀ (x : K₀ C), v ((K₀.map A.equiv.inverse) x) = lam (v x)) (σ : StabilityCondition.WithClassMap C v) : StabilityCondition.WithClassMap C v

A kernel autoequivalence transports a stability condition.

Equations

• A.actStab v lam hlam σ = CategoryTheory.Triangulated.actStabAut A.equiv v lam hlam σ

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.actStab_slicing {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] (lam : Λ →+ Λ) (hlam : ∀ (x : K₀ C), v ((K₀.map A.equiv.inverse) x) = lam (v x)) (σ : StabilityCondition.WithClassMap C v) : (A.actStab v lam hlam σ).slicing = σ.slicing.mapEquiv A.equiv

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.actStab_Z {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] (lam : Λ →+ Λ) (hlam : ∀ (x : K₀ C), v ((K₀.map A.equiv.inverse) x) = lam (v x)) (σ : StabilityCondition.WithClassMap C v) (x : Λ) : (A.actStab v lam hlam σ).Z x = σ.Z (lam x)

noncomputable def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.actStabOfDual {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] (lam : Λ →+ Λ) (hlam : ∀ (x : K₀ C), v ((A.corr.transformK₀ D.dual) x) = lam (v x)) (σ : StabilityCondition.WithClassMap C v) : StabilityCondition.WithClassMap C v

Transport with the class-map compatibility stated through the dual kernel.

Equations

• A.actStabOfDual v D lam hlam σ = A.actStab v lam ⋯ σ

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.actStabOfDual_slicing {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] (lam : Λ →+ Λ) (hlam : ∀ (x : K₀ C), v ((A.corr.transformK₀ D.dual) x) = lam (v x)) (σ : StabilityCondition.WithClassMap C v) : (A.actStabOfDual v D lam hlam σ).slicing = σ.slicing.mapEquiv A.equiv

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.actStabOfDual_Z {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] (lam : Λ →+ Λ) (hlam : ∀ (x : K₀ C), v ((A.corr.transformK₀ D.dual) x) = lam (v x)) (σ : StabilityCondition.WithClassMap C v) (x : Λ) : (A.actStabOfDual v D lam hlam σ).Z x = σ.Z (lam x)

def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.toAutPair {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] (lam : Λ ≃+ Λ) (hlam : ∀ (x : K₀ C), v ((A.corr.transformK₀ D.dual) x) = lam (v x)) : WeakStabilityCondition.StabilityCondition.GroupAction.AutPair v

A kernel autoequivalence with dual kernel defines an acting group element.

Equations

• A.toAutPair v D lam hlam = { Φ := A.toTriEquiv, lam := lam, compat := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.toAutPair_lam {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] (lam : Λ ≃+ Λ) (hlam : ∀ (x : K₀ C), v ((A.corr.transformK₀ D.dual) x) = lam (v x)) : (A.toAutPair v D lam hlam).lam = lam

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.toAutPair_act {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] (lam : Λ ≃+ Λ) (hlam : ∀ (x : K₀ C), v ((A.corr.transformK₀ D.dual) x) = lam (v x)) (σ : StabilityCondition.WithClassMap C v) : (A.toAutPair v D lam hlam).act σ = A.actStabOfDual v D lam.toAddMonoidHom ⋯ σ

The group element acts by the stability transport from which it was built.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.mk_toAutPair_smul {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) [A.equiv.functor.Additive] [A.equiv.inverse.Additive] [A.equiv.functor.CommShift ℤ] [A.equiv.inverse.CommShift ℤ] [A.equiv.functor.IsTriangulated] [A.equiv.inverse.IsTriangulated] (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] (lam : Λ ≃+ Λ) (hlam : ∀ (x : K₀ C), v ((A.corr.transformK₀ D.dual) x) = lam (v x)) (σ : StabilityCondition.WithClassMap C v) : WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.mk (A.toAutPair v D lam hlam) • σ = A.actStabOfDual v D lam.toAddMonoidHom ⋯ σ

The corresponding quotient action agrees with kernel transport.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.actStab_trans {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {𝒲₁ : Type t₁} {𝒲₂ : Type t₂} {𝒲₃ : Type t₃} [Category.{x₁, t₁} 𝒲₁] [Limits.HasZeroObject 𝒲₁] [HasShift 𝒲₁ ℤ] [Preadditive 𝒲₁] [∀ (n : ℤ), (shiftFunctor 𝒲₁ n).Additive] [Pretriangulated 𝒲₁] [Category.{x₂, t₂} 𝒲₂] [Limits.HasZeroObject 𝒲₂] [HasShift 𝒲₂ ℤ] [Preadditive 𝒲₂] [∀ (n : ℤ), (shiftFunctor 𝒲₂ n).Additive] [Pretriangulated 𝒲₂] [Category.{x₃, t₃} 𝒲₃] [Limits.HasZeroObject 𝒲₃] [HasShift 𝒲₃ ℤ] [Preadditive 𝒲₃] [∀ (n : ℤ), (shiftFunctor 𝒲₃ n).Additive] [Pretriangulated 𝒲₃] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) (A₁ : KernelAutoequivalence C 𝒲₁) (A₂ : KernelAutoequivalence C 𝒲₂) (corr₃ : Correspondence C C 𝒲₃) (D : ConvolutionData A₁.corr A₂.corr corr₃) [A₁.equiv.functor.Additive] [A₁.equiv.inverse.Additive] [A₂.equiv.functor.Additive] [A₂.equiv.inverse.Additive] [A₁.equiv.functor.CommShift ℤ] [A₁.equiv.inverse.CommShift ℤ] [A₂.equiv.functor.CommShift ℤ] [A₂.equiv.inverse.CommShift ℤ] [A₁.equiv.functor.IsTriangulated] [A₁.equiv.inverse.IsTriangulated] [A₂.equiv.functor.IsTriangulated] [A₂.equiv.inverse.IsTriangulated] {lam₁ lam₂ : Λ →+ Λ} (h₁ : ∀ (x : K₀ C), v ((K₀.map A₁.equiv.inverse) x) = lam₁ (v x)) (h₂ : ∀ (x : K₀ C), v ((K₀.map A₂.equiv.inverse) x) = lam₂ (v x)) (σ : StabilityCondition.WithClassMap C v) : A₂.actStab v lam₂ h₂ (A₁.actStab v lam₁ h₁ σ) = (A₁.trans A₂ corr₃ D).actStab v (lam₁.comp lam₂) ⋯ σ

Stability transport respects convolution of kernel autoequivalences.