Algebraic-geometric Fourier--Mukai actions on stability conditions #
This file applies the categorical stability action to geometric Fourier--Mukai
autoequivalences. Neutral kernels, duals, swaps, and convolution live in
DerivedCategory/FourierMukai/; the generic action lives under
CategoryTheory/Triangulated/. This file is the one Fourier--Mukai module that
imports the stability tree, which is why it sits under DerivedCategory/Stability/
rather than beside the neutral kernels.
noncomputable def
AlgebraicGeometry.DerivedCategory.FourierMukai.geometricActStabOfDual
{S : Scheme}
(X Z : Families.SchemeBaseChange S)
[IsLocallyNoetherian (CategoryTheory.Over.left X)]
[IsLocallyNoetherian (CategoryTheory.Over.left Z)]
(σ : Z ⟶ Z)
(p q : Z ⟶ X)
(K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z))
[Families.SchemeBaseChange.HasCoherentPullback σ]
[Families.SchemeBaseChange.HasCoherentPullback p]
[Families.SchemeBaseChange.HasCoherentPullback q]
[HasDerivedPushforward σ]
[HasDerivedPushforward p]
[HasDerivedPushforward q]
[HasCoherentDerivedTensor Z]
[HasPullbackSwap σ p q]
[HasPushforwardSwap σ p q]
[HasProjectionFormulaRight σ]
[HasDerivedPullbackAdjunction p]
[HasKernelDual Z K]
[HasTwistedInversePullback q]
[HasDualizingTwist q]
[∀ (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)),
CategoryTheory.IsIso ((geometricDualAdjointKernelData X Z σ p q K).adj.unit.app E)]
[∀ (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)),
CategoryTheory.IsIso ((geometricDualAdjointKernelData X Z σ p q K).adj.counit.app E)]
{Λ : Type u}
[AddCommGroup Λ]
(v : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)) →+ Λ)
(lam : Λ →+ Λ)
(hlam :
∀ (x : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X))),
v (((geometricCorrespondence X X Z p q).transformK₀ (geometricDualKernelObj X Z σ q K)) x) = lam (v x))
(s :
CategoryTheory.Triangulated.StabilityCondition.WithClassMap
(SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)) v)
:
A geometric kernel autoequivalence transports a stability condition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
AlgebraicGeometry.DerivedCategory.FourierMukai.geometricToAutPair
{S : Scheme}
(X Z : Families.SchemeBaseChange S)
[IsLocallyNoetherian (CategoryTheory.Over.left X)]
[IsLocallyNoetherian (CategoryTheory.Over.left Z)]
(σ : Z ⟶ Z)
(p q : Z ⟶ X)
(K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z))
[Families.SchemeBaseChange.HasCoherentPullback σ]
[Families.SchemeBaseChange.HasCoherentPullback p]
[Families.SchemeBaseChange.HasCoherentPullback q]
[HasDerivedPushforward σ]
[HasDerivedPushforward p]
[HasDerivedPushforward q]
[HasCoherentDerivedTensor Z]
[HasPullbackSwap σ p q]
[HasPushforwardSwap σ p q]
[HasProjectionFormulaRight σ]
[HasDerivedPullbackAdjunction p]
[HasKernelDual Z K]
[HasTwistedInversePullback q]
[HasDualizingTwist q]
[∀ (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)),
CategoryTheory.IsIso ((geometricDualAdjointKernelData X Z σ p q K).adj.unit.app E)]
[∀ (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)),
CategoryTheory.IsIso ((geometricDualAdjointKernelData X Z σ p q K).adj.counit.app E)]
{Λ : Type u}
[AddCommGroup Λ]
(v : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)) →+ Λ)
(lam : Λ ≃+ Λ)
(hlam :
∀ (x : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X))),
v (((geometricCorrespondence X X Z p q).transformK₀ (geometricDualKernelObj X Z σ q K)) x) = lam (v x))
:
A geometric kernel autoequivalence defines an element of the acting group.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AlgebraicGeometry.DerivedCategory.FourierMukai.geometricMk_toAutPair_smul
{S : Scheme}
(X Z : Families.SchemeBaseChange S)
[IsLocallyNoetherian (CategoryTheory.Over.left X)]
[IsLocallyNoetherian (CategoryTheory.Over.left Z)]
(σ : Z ⟶ Z)
(p q : Z ⟶ X)
(K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z))
[Families.SchemeBaseChange.HasCoherentPullback σ]
[Families.SchemeBaseChange.HasCoherentPullback p]
[Families.SchemeBaseChange.HasCoherentPullback q]
[HasDerivedPushforward σ]
[HasDerivedPushforward p]
[HasDerivedPushforward q]
[HasCoherentDerivedTensor Z]
[HasPullbackSwap σ p q]
[HasPushforwardSwap σ p q]
[HasProjectionFormulaRight σ]
[HasDerivedPullbackAdjunction p]
[HasKernelDual Z K]
[HasTwistedInversePullback q]
[HasDualizingTwist q]
[∀ (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)),
CategoryTheory.IsIso ((geometricDualAdjointKernelData X Z σ p q K).adj.unit.app E)]
[∀ (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)),
CategoryTheory.IsIso ((geometricDualAdjointKernelData X Z σ p q K).adj.counit.app E)]
{Λ : Type u}
[AddCommGroup Λ]
(v : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)) →+ Λ)
(lam : Λ ≃+ Λ)
(hlam :
∀ (x : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X))),
v (((geometricCorrespondence X X Z p q).transformK₀ (geometricDualKernelObj X Z σ q K)) x) = lam (v x))
(s :
CategoryTheory.Triangulated.StabilityCondition.WithClassMap
(SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)) v)
:
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.mk
(geometricToAutPair X Z σ p q K v lam hlam) • s = geometricActStabOfDual X Z σ p q K v lam.toAddMonoidHom ⋯ s
The geometric group element acts by its Fourier--Mukai transport.
theorem
AlgebraicGeometry.DerivedCategory.FourierMukai.geometricActStabTrans
{S : Scheme}
(X Z₁ Z₂ Z₃ : Families.SchemeBaseChange S)
[IsLocallyNoetherian (CategoryTheory.Over.left X)]
[IsLocallyNoetherian (CategoryTheory.Over.left Z₁)]
[IsLocallyNoetherian (CategoryTheory.Over.left Z₂)]
[IsLocallyNoetherian (CategoryTheory.Over.left Z₃)]
(σ₁ : Z₁ ⟶ Z₁)
(p₁ q₁ : Z₁ ⟶ X)
(K₁ : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z₁))
(σ₂ : Z₂ ⟶ Z₂)
(p₂ q₂ : Z₂ ⟶ X)
(K₂ : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z₂))
(p₃ q₃ : Z₃ ⟶ X)
[Families.SchemeBaseChange.HasCoherentPullback σ₁]
[Families.SchemeBaseChange.HasCoherentPullback p₁]
[Families.SchemeBaseChange.HasCoherentPullback q₁]
[HasDerivedPushforward σ₁]
[HasDerivedPushforward p₁]
[HasDerivedPushforward q₁]
[HasCoherentDerivedTensor Z₁]
[HasPullbackSwap σ₁ p₁ q₁]
[HasPushforwardSwap σ₁ p₁ q₁]
[HasProjectionFormulaRight σ₁]
[HasDerivedPullbackAdjunction p₁]
[HasKernelDual Z₁ K₁]
[HasTwistedInversePullback q₁]
[HasDualizingTwist q₁]
[Families.SchemeBaseChange.HasCoherentPullback σ₂]
[Families.SchemeBaseChange.HasCoherentPullback p₂]
[Families.SchemeBaseChange.HasCoherentPullback q₂]
[HasDerivedPushforward σ₂]
[HasDerivedPushforward p₂]
[HasDerivedPushforward q₂]
[HasCoherentDerivedTensor Z₂]
[HasPullbackSwap σ₂ p₂ q₂]
[HasPushforwardSwap σ₂ p₂ q₂]
[HasProjectionFormulaRight σ₂]
[HasDerivedPullbackAdjunction p₂]
[HasKernelDual Z₂ K₂]
[HasTwistedInversePullback q₂]
[HasDualizingTwist q₂]
[∀ (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)),
CategoryTheory.IsIso ((geometricDualAdjointKernelData X Z₁ σ₁ p₁ q₁ K₁).adj.unit.app E)]
[∀ (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)),
CategoryTheory.IsIso ((geometricDualAdjointKernelData X Z₁ σ₁ p₁ q₁ K₁).adj.counit.app E)]
[∀ (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)),
CategoryTheory.IsIso ((geometricDualAdjointKernelData X Z₂ σ₂ p₂ q₂ K₂).adj.unit.app E)]
[∀ (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)),
CategoryTheory.IsIso ((geometricDualAdjointKernelData X Z₂ σ₂ p₂ q₂ K₂).adj.counit.app E)]
[Families.SchemeBaseChange.HasCoherentPullback p₃]
[HasCoherentDerivedTensor Z₃]
[HasDerivedPushforward q₃]
(G : TripleProductGeometry Z₁ Z₂ Z₃)
[IsLocallyNoetherian (CategoryTheory.Over.left G.triple)]
[Families.SchemeBaseChange.HasCoherentPullback G.πXY]
[Families.SchemeBaseChange.HasCoherentPullback G.πYW]
[Families.SchemeBaseChange.HasCoherentPullback G.πXW]
[HasCoherentDerivedTensor G.triple]
[HasDerivedPushforward G.πYW]
[HasDerivedPushforward G.πXW]
[HasFlatBaseChange q₁ G.πYW G.πXY p₂]
[HasProjectionFormula G.πYW]
[HasMonoidalDerivedPullback G.πXY]
[HasProjectionFormulaRight G.πXW]
[HasCommonPullbackRoute p₁ G.πXY p₃ G.πXW]
[HasCommonPushforwardRoute G.πYW q₂ G.πXW q₃]
{Λ : Type u}
[AddCommGroup Λ]
(v : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)) →+ Λ)
{lam₁ lam₂ : Λ →+ Λ}
(h₁ :
∀ (x : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X))),
v
((CategoryTheory.Triangulated.K₀.map (geometricKernelAutoequivalenceOfAdjoint X Z₁ σ₁ p₁ q₁ K₁).equiv.inverse)
x) = lam₁ (v x))
(h₂ :
∀ (x : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X))),
v
((CategoryTheory.Triangulated.K₀.map (geometricKernelAutoequivalenceOfAdjoint X Z₂ σ₂ p₂ q₂ K₂).equiv.inverse)
x) = lam₂ (v x))
(s :
CategoryTheory.Triangulated.StabilityCondition.WithClassMap
(SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)) v)
:
(geometricKernelAutoequivalenceOfAdjoint X Z₂ σ₂ p₂ q₂ K₂).actStab v lam₂ h₂
((geometricKernelAutoequivalenceOfAdjoint X Z₁ σ₁ p₁ q₁ K₁).actStab v lam₁ h₁ s) = (geometricTransKernelAutoequivalence X Z₁ Z₂ Z₃ σ₁ p₁ q₁ K₁ σ₂ p₂ q₂ K₂ p₃ q₃ G).actStab v (lam₁.comp lam₂) ⋯ s
Geometric stability transport respects convolution of kernels.