Assemble the Mukai stability function on the HN-tilted heart #
This file is the terminal categorical assembly for Bridgeland's four
tilted-heart positivity cases. It consumes the two named geometric contracts
from Mukai.GeometricInput and proves positivity for torsion generators,
shifted torsion-free generators, and their extensions. The ambient exponential
Mukai charge is consequently a StabilityFunction on the HN-tilted heart.
The parent constructor tiltStabilityFunctionOfPred takes the boundary
contract for an arbitrary predicate P on the factors together with a proof
that P forces positive real charge on a positive-rank factor at the cutoff.
No Hodge-index hypothesis reaches it. tiltStabilityFunctionOfMargin chooses
the exact Hodge margin as P; tiltStabilityFunctionOfLowerBound chooses a
uniform lower bound realForm ≥ -δ and needs only 2δ < ω²; and
tiltStabilityFunction is the legacy K3-normalized child δ = 1. Thus the
categorical layer does not decide whether the geometric bound comes from the
K3 stable-simple Ext calculation, a stronger abelian surface result, or another
surface realization. None of these constructors chooses between ch and
ch * sqrt(td); that choice has already been made by the additive Mukai class
map m.
No Harder--Narasimhan property for the resulting stability function is claimed. The HN hypothesis below belongs only to the weak slope function used to define the torsion pair and its tilt.
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.mem_semiClosedUpperHalfPlane_of_hnTors
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
{T₀ : t.heart.FullSubcategory}
(hT₀ : ¬Limits.IsZero T₀)
(hT : T₀ ∈ S.toWeakStabilityFunction.hnTors ↑((b β) ω))
:
The complete torsion-generator case, with only the residual rank-and-degree-zero classification supplied geometrically.
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.mem_semiClosedUpperHalfPlane_of_shift_hnFree_of_pred
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
{P : t.heart.FullSubcategory → Prop}
(hP :
∀ (G : t.heart.FullSubcategory),
0 < S.rank G → S.slope G = (b β) ω → P G → 0 < (MukaiChargeData.charge b β ω (MukaiChargeData.ofAmbient t m) G).re)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWith m b β ω S P)
{F₀ : t.heart.FullSubcategory}
(hF₀ : ¬Limits.IsZero F₀)
(hF : F₀ ∈ S.toWeakStabilityFunction.hnFree ↑((b β) ω))
:
The complete shifted torsion-free generator case for a boundary
decomposition into factors satisfying a predicate P, given that P forces
positive real charge on a positive-rank factor at the cutoff. Strictly below
the cutoff is formal slope arithmetic; equality is discharged by the
decomposition contract. No Hodge-index hypothesis appears: whatever justifies
hP stays with the consumer that chose P.
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.mem_semiClosedUpperHalfPlane_of_mem_hnTilt_heart_of_pred
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
{P : t.heart.FullSubcategory → Prop}
(hP :
∀ (G : t.heart.FullSubcategory),
0 < S.rank G → S.slope G = (b β) ω → P G → 0 < (MukaiChargeData.charge b β ω (MukaiChargeData.ofAmbient t m) G).re)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWith m b β ω S P)
{X : C}
(hX : (S.toWeakStabilityFunction.hnTilt (↑((b β) ω)) hHN).heart X)
(hX0 : ¬Limits.IsZero X)
:
The exponential Mukai charge is positive on every nonzero object of the HN-tilted heart, for any boundary predicate whose real positivity has been proved. The generic HRS assembly reduces this to the two Mukai generator theorems.
noncomputable def
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.tiltStabilityFunctionOfPred
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
{P : t.heart.FullSubcategory → Prop}
(hP :
∀ (G : t.heart.FullSubcategory),
0 < S.rank G → S.slope G = (b β) ω → P G → 0 < (MukaiChargeData.charge b β ω (MukaiChargeData.ofAmbient t m) G).re)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWith m b β ω S P)
:
WeakStabilityCondition.StabilityFunction (S.toWeakStabilityFunction.hnTilt (↑((b β) ω)) hHN)
The exponential Mukai charge as a stability function on the tilted
heart, for any boundary predicate whose real positivity has been proved. This
is the parent constructor: every other constructor in this file chooses P and
supplies hP. It does not assert an HN property for the new stability
function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.tiltStabilityFunctionOfPred_Z
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
{P : t.heart.FullSubcategory → Prop}
(hP :
∀ (G : t.heart.FullSubcategory),
0 < S.rank G → S.slope G = (b β) ω → P G → 0 < (MukaiChargeData.charge b β ω (MukaiChargeData.ofAmbient t m) G).re)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWith m b β ω S P)
:
(tiltStabilityFunctionOfPred hb Cpt hHN hzero hP hboundary).Z = MukaiChargeData.ambientChargeHom m b β ω
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.mem_semiClosedUpperHalfPlane_of_shift_hnFree_of_margin
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 0 < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWithMargin m b β ω S)
{F₀ : t.heart.FullSubcategory}
(hF₀ : ¬Limits.IsZero F₀)
(hF : F₀ ∈ S.toWeakStabilityFunction.hnFree ↑((b β) ω))
:
The complete shifted torsion-free generator case under the exact
factorwise Hodge margin: tiltStabilityFunctionOfPred's predicate is the
margin and re_charge_pos_of_margin is the positivity proof.
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.mem_semiClosedUpperHalfPlane_of_shift_hnFree_of_lower_bound
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
(δ : ℝ)
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 0 < (b ω) ω)
(hωδ : 2 * δ < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWithLowerBound m b β ω S δ)
{F₀ : t.heart.FullSubcategory}
(hF₀ : ¬Limits.IsZero F₀)
(hF : F₀ ∈ S.toWeakStabilityFunction.hnFree ↑((b β) ω))
:
The complete shifted torsion-free generator case for an arbitrary
factorwise quadratic lower bound: the predicate is realForm ≥ -δ and
re_charge_pos_of_lower_bound supplies positivity from 2δ < ω².
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.mem_semiClosedUpperHalfPlane_of_shift_hnFree
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 2 < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hboundary : MukaiTilt.HasBoundaryMukaiDecomposition m b β ω S)
{F₀ : t.heart.FullSubcategory}
(hF₀ : ¬Limits.IsZero F₀)
(hF : F₀ ∈ S.toWeakStabilityFunction.hnFree ↑((b β) ω))
:
The K3-normalized shifted-free theorem, obtained from the general lower
bound with δ = 1.
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.mem_semiClosedUpperHalfPlane_of_mem_hnTilt_heart_of_margin
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 0 < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWithMargin m b β ω S)
{X : C}
(hX : (S.toWeakStabilityFunction.hnTilt (↑((b β) ω)) hHN).heart X)
(hX0 : ¬Limits.IsZero X)
:
The exponential Mukai charge is positive on every nonzero object of the HN-tilted heart under the exact factorwise Hodge margin.
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.mem_semiClosedUpperHalfPlane_of_mem_hnTilt_heart_of_lower_bound
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
(δ : ℝ)
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 0 < (b ω) ω)
(hωδ : 2 * δ < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWithLowerBound m b β ω S δ)
{X : C}
(hX : (S.toWeakStabilityFunction.hnTilt (↑((b β) ω)) hHN).heart X)
(hX0 : ¬Limits.IsZero X)
:
The exponential Mukai charge is positive on every nonzero object of the HN-tilted heart under an arbitrary factorwise lower bound.
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.mem_semiClosedUpperHalfPlane_of_mem_hnTilt_heart
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 2 < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
(hboundary : MukaiTilt.HasBoundaryMukaiDecomposition m b β ω S)
{X : C}
(hX : (S.toWeakStabilityFunction.hnTilt (↑((b β) ω)) hHN).heart X)
(hX0 : ¬Limits.IsZero X)
:
The K3-normalized whole-heart positivity theorem, recovered at δ = 1.
noncomputable def
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.tiltStabilityFunctionOfMargin
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 0 < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWithMargin m b β ω S)
:
WeakStabilityCondition.StabilityFunction (S.toWeakStabilityFunction.hnTilt (↑((b β) ω)) hHN)
The exponential Mukai charge as a stability function on the tilted
heart under the exact factorwise Hodge margin. The predicate is the margin
of each factor; re_charge_pos_of_margin is the only Hodge-index input.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.tiltStabilityFunctionOfLowerBound
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
(δ : ℝ)
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 0 < (b ω) ω)
(hωδ : 2 * δ < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWithLowerBound m b β ω S δ)
:
WeakStabilityCondition.StabilityFunction (S.toWeakStabilityFunction.hnTilt (↑((b β) ω)) hHN)
The exponential Mukai charge as a stability function on the tilted heart, parameterized by a factorwise quadratic lower bound. This is the categorical conclusion of the four-case positivity argument; it does not assert an HN property for this new stability function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.tiltStabilityFunction
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 2 < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
(hboundary : MukaiTilt.HasBoundaryMukaiDecomposition m b β ω S)
:
WeakStabilityCondition.StabilityFunction (S.toWeakStabilityFunction.hnTilt (↑((b β) ω)) hHN)
The historical K3-normalized stability-function constructor.
This is the δ = 1 specialization of
tiltStabilityFunctionOfLowerBound. The wrapper keeps existing consumers
source-compatible while making the geometric constant explicit for new
surface children.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.tiltStabilityFunctionOfMargin_Z
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 0 < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWithMargin m b β ω S)
:
(tiltStabilityFunctionOfMargin hb hsigPos hω Cpt hHN hzero hboundary).Z = MukaiChargeData.ambientChargeHom m b β ω
@[simp]
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.tiltStabilityFunctionOfLowerBound_Z
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
(δ : ℝ)
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 0 < (b ω) ω)
(hωδ : 2 * δ < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
(hboundary : MukaiTilt.HasBoundaryMukaiDecompositionWithLowerBound m b β ω S δ)
:
(tiltStabilityFunctionOfLowerBound δ hb hsigPos hω hωδ Cpt hHN hzero hboundary).Z = MukaiChargeData.ambientChargeHom m b β ω
@[simp]
theorem
CategoryTheory.Triangulated.MukaiWeakSlopeCompat.tiltStabilityFunction_Z
{C : Type u_1}
[Category.{u_3, u_1} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{V : Type u_2}
[AddCommGroup V]
[Module ℝ V]
{t : TStructure C}
[FiniteDimensional ℝ V]
{m : K₀ C →+ Mukai.RealExtension V}
{b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ}
{β ω : V}
(hb : ∀ (x y : V), (b x) y = (b y) x)
(hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1)
(hω : 2 < (b ω) ω)
{S : WeakSlopeData t.heart.FullSubcategory}
(Cpt : MukaiWeakSlopeCompat (MukaiChargeData.ofAmbient t m) S b ω)
(hHN : S.toWeakStabilityFunction.HasHNProperty)
(hzero : MukaiTilt.HasDimensionZeroTorsionClasses m b β ω S)
(hboundary : MukaiTilt.HasBoundaryMukaiDecomposition m b β ω S)
:
(tiltStabilityFunction hb hsigPos hω Cpt hHN hzero hboundary).Z = MukaiChargeData.ambientChargeHom m b β ω