A bounded region from a Hodge divisor space

Spherical/Finiteness.lean proves that finitely many spherical walls meet a BoundedRegion of the (β, ω) chart, and defines the signedRayRegularLocus they cut out. Its own module docstring records that nothing inhabits that structure:

exhibiting a region with these constants is a statement about the ample cone, and the ample cone does not appear in this file

and

neg_definite is the hypothesis that the geometric theory would discharge by Hodge index; here it is supplied.

Until now nothing in the tree discharged either, so every consequence of BoundedRegion was vacuous. This file supplies the witness.

The two constants

BoundedRegion asks for a positive lower bound on q(ω,ω) and a uniform negative-definiteness constant for q on ω^⊥. Both come from Divisorial/Region.lean:

• DivisorSpace.exists_ampleLower — a continuous positive function on a compact set attains a positive minimum.
• DivisorSpace.exists_uniform_negDefinite — the definiteness is pointwise by HodgeDefinite.of_pair_pos, and compactness makes the constant uniform.

The Hodge input enters once, as DivisorSpace.HodgeDefinite at a single reference class. HodgeDefinite.of_pair_pos is what lets one certificate cover every ω of the family, which is why the region does not have to carry a certificate per point.

What this does and does not settle

It makes finite_walls_meeting and signedRayRegularLocus non-vacuous on any Hodge divisor space. It does not prove a Hodge index theorem for a geometric surface, and it says nothing about semistable objects: signedRayRegularLocus is a subset of the parameter chart, and constancy of anything on it is not asserted.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.BoundedRegion.ofDivisorSpace {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] [FiniteDimensional ℝ D] {S : Divisorial.DivisorSpace D} {H : D} (h : S.HodgeDefinite H) {K : Set (D × D)} (hK : IsCompact K) (hpos : ∀ p ∈ K, 0 < S.pair p.2 p.2) : BoundedRegion S.intersection

The bounded region of a compact family of parameters on a Hodge divisor space.

The carrier is the family itself; the two constants are the ones Divisorial/Region.lean produces. This is the first witness for BoundedRegion, and it is what makes everything downstream of it non-vacuous.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.BoundedRegion.ofDivisorSpace_carrier {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] [FiniteDimensional ℝ D] {S : Divisorial.DivisorSpace D} {H : D} (h : S.HodgeDefinite H) {K : Set (D × D)} (hK : IsCompact K) (hpos : ∀ p ∈ K, 0 < S.pair p.2 p.2) : (ofDivisorSpace h hK hpos).carrier = K

The two charts are one

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.expPlane_eq_chartPlane {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (S : Divisorial.DivisorSpace D) (B omega : D) : S.expPlane B omega = chartPlane S.intersection B omega

The divisorial exponential plane is the spherical chart plane.

Divisorial/Region.lean builds the plane of exp(B + iω) for a divisor space, and Spherical/WallComparison.lean builds it in the (β, ω) chart. Since Spherical/Basic.lean now spells its chart with Mukai.expRe and Mukai.expIm, the two are the same submodule and this is rfl.

With it, mem_periodDomainWall_iff_mem_wall reads as a statement about a divisor space: the walls counted by Divisorial/Region.lean are the vanishing locus inside the half-walls counted here.

The consequences, now non-vacuous

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.finite_rayCandidates_ofDivisorSpace {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] [FiniteDimensional ℝ D] {S : Divisorial.DivisorSpace D} {H : D} (h : S.HodgeDefinite H) {K : Set (D × D)} (hK : IsCompact K) (hpos : ∀ p ∈ K, 0 < S.pair p.2 p.2) {ι : Type u_2} [Finite ι] (basis : Module.Basis ι ℝ D) : (rayCandidates S.intersection (BoundedRegion.ofDivisorSpace h hK hpos) ↑(Submodule.span ℤ (Set.range ⇑basis))).Finite

Finitely many spherical classes of a lattice have a nonpositiveRayLocus meeting a compact family of parameters on a Hodge divisor space.

This is BoundedRegion.finite_rayCandidates with the region supplied. Every hypothesis is discharged except the Hodge certificate itself.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.signedRayRegularLocus_inter_ofDivisorSpace {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] [FiniteDimensional ℝ D] {S : Divisorial.DivisorSpace D} {H : D} (h : S.HodgeDefinite H) {K : Set (D × D)} (hK : IsCompact K) (hpos : ∀ p ∈ K, 0 < S.pair p.2 p.2) {ι : Type u_2} (basis : Module.Basis ι ℝ D) : signedRayRegularLocus S.intersection (latticeSpherical S.intersection ↑(Submodule.span ℤ (Set.range ⇑basis))) ∩ K = signedRayRegularLocus S.intersection (rayCandidates S.intersection (BoundedRegion.ofDivisorSpace h hK hpos) ↑(Submodule.span ℤ (Set.range ⇑basis))) ∩ K

On a compact family over a Hodge divisor space, the signedRayRegularLocus is cut out by finitely many walls.

signedRayRegularLocus_inter_carrier says the signedRayRegularLocus of the whole lattice agrees, on the region, with the signedRayRegularLocus of the nonpositiveRayLocus candidates, and finite_rayCandidates_ofDivisorSpace says those are finite. Together they are the signedRayRegularLocus decomposition the missing witness has been blocking.