Regions of positive planes, and the orthogonality loci that meet them

OrthogonalityFiniteness.lean counts the spherical orthogonality loci through one positive plane. This file does it for a family, which is what a local-finiteness statement about the period domain needs.

The constant is a hypothesis, and this file says why

The pointwise count runs on the coercivity constant of -Q on Wᗮ. That constant depends on W and degrades to 0 as the plane approaches the boundary of the positive-plane locus, so a family of planes inherits no constant from its members. This is one of the two gaps in Bridgeland's own §11 argument.

PlaneRegion therefore carries coercivity as an explicit field, exactly as Walls/Spherical/Finiteness.lean does for BoundedRegion in the other chart. It is never derived from boundedness of the region.

And a criterion that inhabits it

A structure whose hypothesis nobody can satisfy proves nothing. exists_uniform_coercivity supplies the field for a compact family of spanning pairs: orthogonality is a closed condition, so the unit vectors orthogonal to the planes of the family form a compact set, -Q is continuous and positive there, and its minimum is the constant. ofCompactPairs packages that as a PlaneRegion.

The family is parametrized by spanning pairs rather than by the Grassmannian, which keeps everything inside the linear algebra already in the tree.

Main results

• exists_uniform_coercivity — a compact family of positive planes has a uniform coercivity constant. Its closedness input, mem_orthogonal_span_pair_iff, is pure algebra and lives in PositivePlane.lean.
• PlaneRegion.finite_orthogonalClasses_inter — finitely many spherical classes of a lattice have an orthogonality locus meeting the region.
• PlaneRegion.ofCompactPairs — the criterion, packaged; and PlaneRegion.empty for contrast, a witness that proves only non-vacuity of the structure.

As in PositivePlane.lean, everything is about an arbitrary real quadratic space and its lattices, and no geometry is asserted.

theorem PeriodDomain.exists_uniform_coercivity {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} (hsig : HasSignatureTwo Q) {S : Set (M × M)} (hS : IsCompact S) (hpos : ∀ p ∈ S, IsPositivePlane Q (Submodule.span ℝ {p.1, p.2})) : ∃ (c : ℝ), 0 < c ∧ ∀ p ∈ S, ∀ u ∈ orthogonal Q (Submodule.span ℝ {p.1, p.2}), c * ‖u‖ ^ 2 ≤ -Q u

A compact family of positive planes has a uniform coercivity constant.

The pairs of the family and the unit vectors orthogonal to the plane they span form a compact set — orthogonality is closed by continuous_polar, and the sphere is compact. -Q is continuous and, by neg_of_mem_orthogonal, positive there, so it attains a positive minimum. Homogeneity extends the bound off the sphere.

structure PeriodDomain.PlaneRegion {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] (Q : QuadraticForm ℝ M) : Type u_1

A region of positive planes carrying a uniform coercivity constant.

coercivity is a field on purpose: it does not follow from boundedness of the region, and deriving it is the mistake §11 makes. Use ofCompactPairs to build one.

• carrier : Set (Submodule ℝ M)

  The planes of the region.

• isPositivePlane (W : Submodule ℝ M) : W ∈ self.carrier → IsPositivePlane Q W

  Each of them is a positive plane.

• coercivity : ℝ

  The uniform constant.

• coercivity_pos : 0 < self.coercivity

  It is positive.

• uniform (W : Submodule ℝ M) : W ∈ self.carrier → ∀ u ∈ orthogonal Q W, self.coercivity * ‖u‖ ^ 2 ≤ -Q u

  And it works for every plane of the region at once.

def PeriodDomain.PlaneRegion.orthogonalClasses {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] {Q : QuadraticForm ℝ M} (R : PlaneRegion Q) : Set M

The spherical classes with a orthogonalityLocus meeting the region.

Equations

• R.orthogonalClasses = {δ : M | PeriodDomain.IsSphericalClass Q δ ∧ ∃ W ∈ R.carrier, W ∈ PeriodDomain.orthogonalityLocus Q δ}

theorem PeriodDomain.PlaneRegion.isBounded_orthogonalClasses {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] {Q : QuadraticForm ℝ M} (R : PlaneRegion Q) : Bornology.IsBounded R.orthogonalClasses

The orthogonalityLocus classes of a region are bounded, by the one constant the region carries.

theorem PeriodDomain.PlaneRegion.finite_orthogonalClasses_inter {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} (R : PlaneRegion Q) {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℝ M) : (R.orthogonalClasses ∩ ↑(Submodule.span ℤ (Set.range ⇑b))).Finite

Only finitely many spherical classes of a lattice have a orthogonalityLocus meeting the region. Bridgeland's local finiteness in the period-domain chart, with the uniform constant explicit.

noncomputable def PeriodDomain.PlaneRegion.ofCompactPairs {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} (hsig : HasSignatureTwo Q) {S : Set (M × M)} (hS : IsCompact S) (hpos : ∀ p ∈ S, IsPositivePlane Q (Submodule.span ℝ {p.1, p.2})) : PlaneRegion Q

The criterion, packaged. A compact family of spanning pairs is a region, with the constant supplied by exists_uniform_coercivity rather than assumed.

Equations

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

def PeriodDomain.PlaneRegion.empty {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] (Q : QuadraticForm ℝ M) : PlaneRegion Q

The empty region. It inhabits the structure and proves nothing else — every statement about it is vacuous. ofCompactPairs is the witness that carries content; this one is here so the difference is on the record.

Equations

• PeriodDomain.PlaneRegion.empty Q = { carrier := ∅, isPositivePlane := ⋯, coercivity := 1, coercivity_pos := PeriodDomain.PlaneRegion.empty._proof_2, uniform := ⋯ }