Scheme-derived K3 specialization of the Mukai tilt stability function

This file specializes K3MukaiTilt.lean to the numerical surface assembled from geometric Todd and reconstruction data. It is separate so the reusable numerical adapter does not acquire the full geometric Riemann--Roch import.

noncomputable def AlgebraicGeometry.DerivedCategory.Stability.K3MukaiTilt.schemeTiltStabilityFunction {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {A : Type v} [CommRing A] [Algebra ℚ A] {W : Type w} [AddCommGroup W] [Module ℝ W] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {Q : IntersectionTheory.ChernCharacter.PairingContext D C 2 A} {K : SmoothProperVariety.CanonicalSheafData k X 2} [hK3Surface : SmoothProperVariety.IsK3Surface k X K] [FiniteDimensional ℝ W] (T : RiemannRoch.Surface.ToddData.Data Q K) (Rg : RiemannRoch.ReconstructionSystem) (RR : Numerical.Surface.NumericalRealization (RiemannRoch.Surface.Assembly.toNumericalVariety T Rg).ring) {β ω : W} (G : Stability.Gieseker.PolarizedVarietyData k X) (N : SlopeNormalization G RR ω) (hμ : Stability.Gieseker.MuPositivityData G) (hbounded : SlopeBoundedness G) (hchi : Q.intersection.eulerPic 1 = 2) (m : CategoryTheory.Triangulated.K₀ (DerivedCategory.Bounded (Coh X)) →+ Mukai.RealExtension W) (hm : IsAmbientMukaiClass RR m) (hHodge : RR.divisorSpace.HodgeDefinite ω) (hω : 2 < RR.divisorSpace.pair ω ω) (hzero : HasDimensionZeroMukaiClasses RR ω) (hboundary : CategoryTheory.Triangulated.MukaiTilt.HasBoundaryMukaiDecomposition m RR.divisorSpace.intersection β ω (N.boundedMukaiSlopeData hμ)) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityFunction ((N.boundedMukaiSlopeData hμ).toWeakStabilityFunction.hnTilt ↑((RR.divisorSpace.intersection β) ω) ⋯)

The K3 Mukai tilt stability function for the numerical surface assembled from geometric Todd and reconstruction data.

χ(O_X)=2 remains explicit: the current K3 package supplies trivial canonical class and H¹(O_X)=0, but the needed Serre-duality bridge to the Euler characteristic has not yet been formalized.

Equations

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

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Stability.K3MukaiTilt.schemeTiltStabilityFunction_Z {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {A : Type v} [CommRing A] [Algebra ℚ A] {W : Type w} [AddCommGroup W] [Module ℝ W] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {Q : IntersectionTheory.ChernCharacter.PairingContext D C 2 A} {K : SmoothProperVariety.CanonicalSheafData k X 2} [hK3Surface : SmoothProperVariety.IsK3Surface k X K] [FiniteDimensional ℝ W] (T : RiemannRoch.Surface.ToddData.Data Q K) (Rg : RiemannRoch.ReconstructionSystem) (RR : Numerical.Surface.NumericalRealization (RiemannRoch.Surface.Assembly.toNumericalVariety T Rg).ring) {β ω : W} (G : Stability.Gieseker.PolarizedVarietyData k X) (N : SlopeNormalization G RR ω) (hμ : Stability.Gieseker.MuPositivityData G) (hbounded : SlopeBoundedness G) (hchi : Q.intersection.eulerPic 1 = 2) (m : CategoryTheory.Triangulated.K₀ (DerivedCategory.Bounded (Coh X)) →+ Mukai.RealExtension W) (hm : IsAmbientMukaiClass RR m) (hHodge : RR.divisorSpace.HodgeDefinite ω) (hω : 2 < RR.divisorSpace.pair ω ω) (hzero : HasDimensionZeroMukaiClasses RR ω) (hboundary : CategoryTheory.Triangulated.MukaiTilt.HasBoundaryMukaiDecomposition m RR.divisorSpace.intersection β ω (N.boundedMukaiSlopeData hμ)) : (schemeTiltStabilityFunction T Rg RR G N hμ hbounded hchi m hm hHodge hω hzero hboundary).Z = CategoryTheory.Triangulated.MukaiChargeData.ambientChargeHom m RR.divisorSpace.intersection β ω

noncomputable def AlgebraicGeometry.DerivedCategory.Stability.K3MukaiTilt.canonicalSchemeTiltStabilityFunction {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {A : Type v} [CommRing A] [Algebra ℚ A] {W : Type w} [AddCommGroup W] [Module ℝ W] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {Q : IntersectionTheory.ChernCharacter.PairingContext D C 2 A} {K : SmoothProperVariety.CanonicalSheafData k X 2} [hK3Surface : SmoothProperVariety.IsK3Surface k X K] [FiniteDimensional ℝ W] (T : RiemannRoch.Surface.ToddData.Data Q K) (Rg : RiemannRoch.ReconstructionSystem) (RR : Numerical.Surface.NumericalRealization (RiemannRoch.Surface.Assembly.toNumericalVariety T Rg).ring) {β ω : W} (G : Stability.Gieseker.PolarizedVarietyData k X) (N : SlopeNormalization G RR ω) (hμ : Stability.Gieseker.MuPositivityData G) (hbounded : SlopeBoundedness G) (hchi : Q.intersection.eulerPic 1 = 2) (hHodge : RR.divisorSpace.HodgeDefinite ω) (hω : 2 < RR.divisorSpace.pair ω ω) (hzero : HasDimensionZeroMukaiClasses RR ω) (hboundary : CategoryTheory.Triangulated.MukaiTilt.HasBoundaryMukaiDecomposition (derivedMukaiClass RR) RR.divisorSpace.intersection β ω (N.boundedMukaiSlopeData hμ)) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityFunction ((N.boundedMukaiSlopeData hμ).toWeakStabilityFunction.hnTilt ↑((RR.divisorSpace.intersection β) ω) ⋯)

The scheme-derived K3 tilt stability function using the canonical cohomological extension of the coherent Mukai class. This removes the separate ambient class map and restriction proof from the geometric input.

Equations

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

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Stability.K3MukaiTilt.canonicalSchemeTiltStabilityFunction_Z {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {A : Type v} [CommRing A] [Algebra ℚ A] {W : Type w} [AddCommGroup W] [Module ℝ W] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {Q : IntersectionTheory.ChernCharacter.PairingContext D C 2 A} {K : SmoothProperVariety.CanonicalSheafData k X 2} [hK3Surface : SmoothProperVariety.IsK3Surface k X K] [FiniteDimensional ℝ W] (T : RiemannRoch.Surface.ToddData.Data Q K) (Rg : RiemannRoch.ReconstructionSystem) (RR : Numerical.Surface.NumericalRealization (RiemannRoch.Surface.Assembly.toNumericalVariety T Rg).ring) {β ω : W} (G : Stability.Gieseker.PolarizedVarietyData k X) (N : SlopeNormalization G RR ω) (hμ : Stability.Gieseker.MuPositivityData G) (hbounded : SlopeBoundedness G) (hchi : Q.intersection.eulerPic 1 = 2) (hHodge : RR.divisorSpace.HodgeDefinite ω) (hω : 2 < RR.divisorSpace.pair ω ω) (hzero : HasDimensionZeroMukaiClasses RR ω) (hboundary : CategoryTheory.Triangulated.MukaiTilt.HasBoundaryMukaiDecomposition (derivedMukaiClass RR) RR.divisorSpace.intersection β ω (N.boundedMukaiSlopeData hμ)) : (canonicalSchemeTiltStabilityFunction T Rg RR G N hμ hbounded hchi hHodge hω hzero hboundary).Z = CategoryTheory.Triangulated.MukaiChargeData.ambientChargeHom (derivedMukaiClass RR) RR.divisorSpace.intersection β ω