Local finiteness of the spherical walls

Only finitely many spherical walls meet a bounded region of the chart. This is the second half of Bridgeland's Proposition 11.2; Walls/Spherical/Basic.lean supplies the arithmetic it runs on and stops deliberately short of this statement.

Two hypotheses the printed proof leaves implicit

The argument is: a nonpositiveRayLocus through (β, ω) forces Δ − rβ ∈ ω^⊥, negative definiteness there bounds q(Δ − rβ, Δ − rβ) ≤ 0, sphericity turns the nonpositiveRayLocus inequality into r²·q(ω,ω) ≤ 2 + q(Δ − rβ, Δ − rβ) ≤ 2, and then "only finitely many r, hence only finitely many Δ". Writing that down forces two quantifiers the source does not state.

q(ω,ω) must be bounded below by a positive constant. Boundedness of the region does not give this: a bounded subset of the chart can approach the boundary of the ample cone, where q(ω,ω) → 0 and r² ≤ 2/q(ω,ω) bounds nothing. The source's region is implicitly one whose closure stays inside the chart.

The coercivity constant on ω^⊥ must be uniform in ω. The subspace varies with ω across the region, so a per-point constant gives a per-point bound and no single finite set. Compactness of the closure supplies a uniform one, but that is a separate argument about the region, not about the walls.

BoundedRegion carries both as fields, so a caller has to produce them and the theorem cannot quietly assume either. Neither is proved here: exhibiting a region with these constants is a statement about the ample cone, and the ample cone does not appear in this file any more than it does in Basic.

A caller that does produce them is Walls/Spherical/DivisorialRegion.lean: on a divisor space with a DivisorSpace.HodgeDefinite certificate, a compact family of parameters supplies both constants, so everything below is inhabited rather than vacuous.

What is still not assumed

No K3 surface, no Néron--Severi group, no ample cone, no Hodge index theorem. neg_definite is the hypothesis that the geometric theory would discharge by Hodge index; here it is supplied. latticeBasis is a ℤ-span of an ℝ-basis, not NS(X).

Main results

• BoundedRegion — a region together with the two constants above.
• rk_sq_le — r² ≤ 2 / ampleLower for a spherical class whose nonpositiveRayLocus meets the region. This is where positivity of the lower bound on q(ω,ω) is spent.
• normSq_sub_smul_le — ‖Δ − rβ‖² ≤ 2 / coercivity, from the same inequality read the other way.
• finite_walls_meeting — the theorem.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.BoundedRegion {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : Type u_1

A bounded region of the (β, ω) chart, together with the two uniform constants the finiteness argument needs.

ample_le and neg_definite are the two hypotheses Bridgeland's Proposition 11.2 uses without stating; see the module docstring. Both are fields rather than side conditions so that producing a region is visibly an obligation.

• carrier : Set (V × V)

  The region itself.

• bounded : Bornology.IsBounded self.carrier

  It is bounded.

• ampleLower : ℝ

  A positive lower bound for q(ω,ω) on the region.

• ampleLower_pos : 0 < self.ampleLower

  It is positive. This is what stops r running away.

• ample_le (p : V × V) : p ∈ self.carrier → self.ampleLower ≤ (q p.2) p.2

  The bound holds.

• coercivity : ℝ

  A uniform coercivity constant for −q on ω^⊥.

• coercivity_pos : 0 < self.coercivity

  It is positive.

• neg_definite (p : V × V) : p ∈ self.carrier → ∀ (x : V), (q x) p.2 = 0 → (q x) x ≤ -self.coercivity * ‖x‖ ^ 2

  q is uniformly negative definite on ω^⊥, with that constant, at every point of the region.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.BoundedRegion.key {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} (R : BoundedRegion q) (hq : ∀ (x y : V), (q x) y = (q y) x) {δ : Mukai.RealExtension V} (hs : IsSpherical q δ) (hr : 0 < δ.1) {p : V × V} (hp : p ∈ R.carrier) (hw : p ∈ nonpositiveRayLocus q δ) : (q (δ.2.1 - δ.1 • p.1)) (δ.2.1 - δ.1 • p.1) ≤ -R.coercivity * ‖δ.2.1 - δ.1 • p.1‖ ^ 2 ∧ δ.1 ^ 2 * (q p.2) p.2 ≤ 2 + (q (δ.2.1 - δ.1 • p.1)) (δ.2.1 - δ.1 • p.1)

The two facts a nonpositiveRayLocus through the region gives about the class, before any finiteness reasoning: the offset Δ − rβ is q-negative, and the nonpositiveRayLocus inequality holds.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.BoundedRegion.rk_sq_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} (R : BoundedRegion q) (hq : ∀ (x y : V), (q x) y = (q y) x) {δ : Mukai.RealExtension V} (hs : IsSpherical q δ) (hr : 0 < δ.1) {p : V × V} (hp : p ∈ R.carrier) (hw : p ∈ nonpositiveRayLocus q δ) : δ.1 ^ 2 ≤ 2 / R.ampleLower

The rank is bounded. r² ≤ 2 / ampleLower.

This is the step that needs ampleLower > 0, and the step the printed argument performs by saying "ω is constrained to lie in a bounded region".

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.BoundedRegion.normSq_sub_smul_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} (R : BoundedRegion q) (hq : ∀ (x y : V), (q x) y = (q y) x) {δ : Mukai.RealExtension V} (hs : IsSpherical q δ) (hr : 0 < δ.1) {p : V × V} (hp : p ∈ R.carrier) (hw : p ∈ nonpositiveRayLocus q δ) : ‖δ.2.1 - δ.1 • p.1‖ ^ 2 ≤ 2 / R.coercivity

The offset is bounded. ‖Δ − rβ‖² ≤ 2 / coercivity.

The same inequality as rk_sq_le, read for the other term: r²·q(ω,ω) ≥ 0 absorbs the rank contribution and what is left bounds the offset.

From the two bounds to a finite set

rk_sq_le and normSq_sub_smul_le bound r and the offset Δ − rβ. Turning that into finiteness needs one more input the source states without comment: the rank is an integer. Over ℝ alone the bounds are useless for this — r ranges in (0, √(2/ampleLower)], which is bounded and infinite, and worse, the third coordinate s = (q(Δ,Δ) + 2)/(2r) supplied by corank_eq_of_isSpherical blows up as r → 0. Integrality of the rank is what makes r ≥ 1, which bounds s and lets a class be reconstructed from (r, Δ) alone.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.reconstruct {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (nΔ : ℤ × V) : Mukai.RealExtension V

Rebuild a class from its rank and middle coordinate, with the third coordinate forced by sphericity.

This is corank_eq_of_isSpherical read as a definition: on spherical classes of nonzero rank the third coordinate is not free, so (n, Δ) already determines the class and a finiteness statement never has to bound s.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.reconstruct q nΔ = (↑nΔ.1, nΔ.2, ((q nΔ.2) nΔ.2 + 2) / (2 * ↑nΔ.1))

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.rayCandidates {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (R : BoundedRegion q) (Λ : Set V) : Set (Mukai.RealExtension V)

The spherical classes of positive integral rank, with middle coordinate in Λ, whose nonpositiveRayLocus meets the region.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.BoundedRegion.exists_norm_fst_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} (R : BoundedRegion q) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ p ∈ R.carrier, ‖p.1‖ ≤ M

A bound on ‖β‖ over the region, extracted from boundedness.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.BoundedRegion.rayCandidates_subset {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} (R : BoundedRegion q) (hq : ∀ (x y : V), (q x) y = (q y) x) (Λ : Set V) {M : ℝ} (hM : ∀ p ∈ R.carrier, ‖p.1‖ ≤ M) : rayCandidates q R Λ ⊆ reconstruct q '' Set.Icc 1 ⌈2 / R.ampleLower⌉ ×ˢ (Metric.closedBall 0 (√(2 / R.coercivity) + √(2 / R.ampleLower) * M) ∩ Λ)

Every candidate is reconstructed from a bounded integer and a bounded lattice point. This is the whole content of the finiteness argument; the finiteness itself is then two standard facts.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.BoundedRegion.finite_rayCandidates {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} (R : BoundedRegion q) (hq : ∀ (x y : V), (q x) y = (q y) x) [FiniteDimensional ℝ V] {ι : Type u_2} [Finite ι] (basis : Module.Basis ι ℝ V) : (rayCandidates q R ↑(Submodule.span ℤ (Set.range ⇑basis))).Finite

Only finitely many spherical walls meet a bounded region.

Bridgeland's Proposition 11.2, with the two uniform constants of BoundedRegion made explicit and the rank required to be an integer. Λ is the ℤ-span of an ℝ-basis; it is not asserted to be NS(X).

The signedRayRegularLocus is cut out by finitely many walls on the region

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.latticeSpherical {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Λ : Set V) : Set (Mukai.RealExtension V)

The classes the signedRayRegularLocus of a lattice is cut out by: spherical, of positive integral rank, with middle coordinate in Λ.

rayCandidates is this set intersected with "has a nonpositiveRayLocus meeting the region", so the two differ only by a condition that is vacuous off the region.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.rayCandidates_subset_latticeSpherical {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (R : BoundedRegion q) (Λ : Set V) : rayCandidates q R Λ ⊆ latticeSpherical q Λ

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.signedRayRegularLocus_inter_carrier {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (R : BoundedRegion q) (Λ : Set V) : signedRayRegularLocus q (latticeSpherical q Λ) ∩ R.carrier = signedRayRegularLocus q (rayCandidates q R Λ) ∩ R.carrier

On the region, the signedRayRegularLocus of the whole lattice is the signedRayRegularLocus of the finitely many candidates.

A class whose nonpositiveRayLocus misses the region cannot separate two of its points, so the signedRayRegularLocus restricted to the region only sees rayCandidates — which finite_rayCandidates shows is finite. This is what turns local finiteness into a signedRayRegularLocus decomposition.