Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.Walls.Divisorial.Signature

Spherical-wall finiteness for exponential planes #

The Hodge-index certificate, its signature calculation, and nondegeneracy now live in the neutral linear-algebra module LinearAlgebra/BilinearForm/HodgeIndex.lean. This downstream wall module uses that input to form the exponential positive plane and count lattice classes whose spherical orthogonality walls pass through it.

No geometric surface or ample cone is constructed here. D is an arbitrary finite-dimensional real space and the lattice is the integer span of a supplied real basis.

source
noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.expPlane {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] (S : DivisorSpace D) (B omega : D) :
Submodule ℝ (Mukai.RealExtension D)

The positive plane of exp(B + iω), spanned by its real and imaginary parts.

Equations
Instances For
    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.isPositivePlane_expPlane {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] (S : DivisorSpace D) (B omega : D) (homega : 0 < S.pair omega omega) :
    PeriodDomain.IsPositivePlane (Mukai.realForm S.intersection) (S.expPlane B omega)

    The exponential plane is positive as soon as ω² > 0; the B-field is unconstrained.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.finite_walls_through_expPlane {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] {S : DivisorSpace D} {H : D} [FiniteDimensional ℝ D] (h : S.HodgeDefinite H) (B omega : D) (homega : 0 < S.pair omega omega) {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℝ (Mukai.RealExtension D)) :
    {δ : Mukai.RealExtension D | PeriodDomain.IsSphericalClass (Mukai.realForm S.intersection) δ ∧ S.expPlane B omega ∈ PeriodDomain.orthogonalityLocus (Mukai.realForm S.intersection) δ ∧ δ ∈ ↑(Submodule.span ℤ (Set.range ⇑b))}.Finite

    For a lattice in the real Mukai extension, only finitely many spherical classes have a wall through the exponential plane.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.finite_sphericalOrthogonal_expPlane {D : Type w} [NormedAddCommGroup D] [NormedSpace ℝ D] {S : DivisorSpace D} {H : D} [FiniteDimensional ℝ D] (h : S.HodgeDefinite H) (B omega : D) (homega : 0 < S.pair omega omega) {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℝ (Mukai.RealExtension D)) :
    (PeriodDomain.sphericalOrthogonal (Mukai.realForm S.intersection) (S.expPlane B omega) ∩ ↑(Submodule.span ℤ (Set.range ⇑b))).Finite

    The same finiteness, stated as a bounded set of spherical classes orthogonal to the plane.