Finitely many spherical walls meet a compact family of exponential planes

Divisorial/Signature.lean counts the spherical walls through one plane of the period domain. That is not enough for a wall-and-chamber structure, which needs finiteness across a neighbourhood. This file supplies the region-wise count for the family of planes of exp(B + iω) with (B, ω) ranging over a compact set on which ω² is positive.

Why this is now available

QuadraticForm/OrthogonalityRegion.lean records that the coercivity constant of -Q on Wᗮ degrades to 0 at the boundary of the positive-plane locus, so a family of planes inherits no constant from its members; PlaneRegion therefore carries the constant as a field. Its criterion ofCompactPairs supplies that field for a compact family — but only from PeriodDomain.HasSignatureTwo, which nothing could provide for a divisor space until DivisorSpace.hasSignatureTwo_of_hodgeDefinite.

So the input to this file is the same single certificate as everywhere else in the divisorial layer: DivisorSpace.HodgeDefinite.

The family

expPairMap sends (B, ω) to the spanning pair (Re exp(B + iω), Im exp(B + iω)). It is continuous because the intersection form is a bilinear map on a finite-dimensional space, so a compact set of parameters gives a compact set of pairs; and each plane is positive by Mukai.isPositiveFrame_exp as soon as ω² > 0, with B unconstrained. Those are exactly the two hypotheses of ofCompactPairs.

Main results

• expPlaneRegion — the PlaneRegion of a compact parameter family.
• finite_walls_meeting_expFamily — finitely many spherical classes of a lattice have a wall meeting the family, stated with the parameters rather than with the region, which is the form a chamber argument consumes.

The lattice is the ℤ-span of an ℝ-basis and is not asserted to be a geometric lattice; D is an arbitrary finite-dimensional real divisor space.

What is still not proved

Chambers. Knowing that finitely many walls meet a compact family does not by itself produce the connected components of its complement, nor that the semistable objects are constant on one. That is the next step and is not attempted here.

The exponential family of spanning pairs

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.expPairMap {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] (S : DivisorSpace D) (p : D × D) : Mukai.RealExtension D × Mukai.RealExtension D

The spanning pair of the plane of exp(B + iω), as a function of the parameters.

Equations

• S.expPairMap p = (Mukai.expRe S.intersection p.1 p.2, Mukai.expIm S.intersection p.1 p.2)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.expPairMap_fst {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] (S : DivisorSpace D) (p : D × D) : (S.expPairMap p).1 = Mukai.expRe S.intersection p.1 p.2

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.expPairMap_snd {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] (S : DivisorSpace D) (p : D × D) : (S.expPairMap p).2 = Mukai.expIm S.intersection p.1 p.2

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.expPlane_eq_span {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] (S : DivisorSpace D) (B omega : D) : S.expPlane B omega = Submodule.span ℝ {(S.expPairMap (B, omega)).1, (S.expPairMap (B, omega)).2}

The plane of a parameter pair is the span of its exponential pair.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.continuous_pair {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] (S : DivisorSpace D) [FiniteDimensional ℝ D] : Continuous fun (p : D × D) => S.pair p.1 p.2

The intersection form is jointly continuous. Finite dimensionality is what turns the bilinear map into a continuous one.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.continuous_expPairMap {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] (S : DivisorSpace D) [FiniteDimensional ℝ D] : Continuous S.expPairMap

The exponential parameter map is continuous, so a compact set of parameters gives a compact family of spanning pairs.

The region

A uniform negative-definiteness constant on the family

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.exists_ampleLower {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] {S : DivisorSpace D} [FiniteDimensional ℝ D] {K : Set (D × D)} (hK : IsCompact K) (hpos : ∀ p ∈ K, 0 < S.pair p.2 p.2) : ∃ (a : ℝ), 0 < a ∧ ∀ p ∈ K, a ≤ S.pair p.2 p.2

A compact family of polarizations has a positive lower bound for ω².

The second constant Spherical.BoundedRegion asks for. A continuous positive function on a compact set attains a positive minimum; the empty family takes any positive number.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.exists_uniform_negDefinite {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] {S : DivisorSpace D} [FiniteDimensional ℝ D] {H : D} (h : S.HodgeDefinite H) {K : Set (D × D)} (hK : IsCompact K) (hpos : ∀ p ∈ K, 0 < S.pair p.2 p.2) : ∃ (c : ℝ), 0 < c ∧ ∀ p ∈ K, ∀ (x : D), S.pair x p.2 = 0 → S.pair x x ≤ -c * ‖x‖ ^ 2

A compact family of polarizations has a uniform negative-definiteness constant.

HodgeDefinite.of_pair_pos makes the form negative definite on ω^⊥ at every point of the family, but with a constant that could in principle degrade across it. Compactness rules that out: the pairs of the family and the unit vectors orthogonal to their ω form a compact set, on which -q is continuous and positive, so it attains a positive minimum. Homogeneity extends the bound off the sphere.

This is the input Spherical.BoundedRegion asks for and has never had.

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

The plane region of a compact family of exponential parameters.

Both inputs of PlaneRegion.ofCompactPairs are discharged: the signature by the Hodge certificate, and positivity of each plane by Mukai.isPositiveFrame_exp, which needs only ω² > 0.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.expPlaneRegion h hK hpos = PeriodDomain.PlaneRegion.ofCompactPairs ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.expPlaneRegion_carrier {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] {S : DivisorSpace D} [FiniteDimensional ℝ D] {H : D} (h : S.HodgeDefinite H) {K : Set (D × D)} (hK : IsCompact K) (hpos : ∀ p ∈ K, 0 < S.pair p.2 p.2) : (expPlaneRegion h hK hpos).carrier = (fun (q : Mukai.RealExtension D × Mukai.RealExtension D) => Submodule.span ℝ {q.1, q.2}) '' S.expPairMap '' K

The count

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.finite_orthogonalClasses_expPlaneRegion {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] {S : DivisorSpace D} [FiniteDimensional ℝ 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_1} [Finite ι] (b : Module.Basis ι ℝ (Mukai.RealExtension D)) : ((expPlaneRegion h hK hpos).orthogonalClasses ∩ ↑(Submodule.span ℤ (Set.range ⇑b))).Finite

Finitely many spherical classes of a lattice have a wall meeting the region. This is PlaneRegion.finite_orthogonalClasses_inter with the region supplied.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.finite_walls_meeting_expFamily {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] {S : DivisorSpace D} [FiniteDimensional ℝ 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_1} [Finite ι] (b : Module.Basis ι ℝ (Mukai.RealExtension D)) : {δ : Mukai.RealExtension D | PeriodDomain.IsSphericalClass (Mukai.realForm S.intersection) δ ∧ (∃ p ∈ K, S.expPlane p.1 p.2 ∈ PeriodDomain.orthogonalityLocus (Mukai.realForm S.intersection) δ) ∧ δ ∈ ↑(Submodule.span ℤ (Set.range ⇑b))}.Finite

Bridgeland's local finiteness, region-wise, on a divisor space.

For a compact set K of parameters on which ω² is positive, only finitely many spherical classes of the lattice have a wall through the plane of exp(B + iω) for some (B, ω) ∈ K.

This is the form a chamber argument consumes: the parameters appear, not the region. The hypotheses are the Hodge certificate, compactness, and positivity of ω² on the family.