Positive planes avoiding countably many orthogonality loci exist

#700 fixed positivePlanesAway to take its cutting classes from a set, after the reading that cut by every real class of square -2 turned out to be empty. That leaves the obvious question, and this file answers it: for a countable set of nonzero classes — the spherical classes of a lattice, countable because the lattice is finitely generated and free — the cut domain is nonempty.

The argument

Genericity, over pairs rather than planes, since M × M carries the topology.

• The positive frames are open (isOpen_setOf_isPositiveFrame) and nonempty (exists_isPositiveFrame).
• For δ ≠ 0 the pairs orthogonal to δ form a proper closed subspace of M × M: it is the kernel of p ↦ (⟪δ, p.1⟫, ⟪δ, p.2⟫), nonzero because the form is nondegenerate. A proper subspace of a normed space has empty interior, so its complement is open and dense.
• Baire: a countable intersection of dense open sets is dense, and a dense set meets every nonempty open set.

Density of the cut locus in the positive frames is what the argument actually gives; nonemptiness is the corollary that was asked for.

The cheap route does not work

Along a ray ω_t = t • ω₀ in the exponential chart, the orthogonalityLocus condition for a rank-zero spherical class is b ω₀ c = 0 together with b c c = -2, and neither depends on t: such a class blocks the whole ray. Nonemptiness needs genericity, not a scaling trick — which is also why Bridgeland works with an ample class rather than a merely positive one.

theorem PeriodDomain.exists_isPositiveFrame {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) : ∃ (x : M) (y : M), IsPositiveFrame Q x y

A positive plane is spanned by a positive frame. Taking any nonzero x of the plane and any y outside its line, the discriminant is positive because Q ((-⟪x,y⟫) • x + (2 * Q x) • y) = Q x * (4 * Q x * Q y - ⟪x,y⟫ ^ 2) and the left side is positive.

def PeriodDomain.orthogonalityPairs {N : Type u_2} [NormedAddCommGroup N] [NormedSpace ℝ N] (Q : QuadraticForm ℝ N) (δ : N) : Submodule ℝ (N × N)

The pairs both of whose entries are orthogonal to δ.

Equations

• PeriodDomain.orthogonalityPairs Q δ = (((QuadraticMap.polarBilin Q) δ).prodMap ((QuadraticMap.polarBilin Q) δ)).ker

@[simp]

theorem PeriodDomain.mem_orthogonalityPairs_iff {N : Type u_2} [NormedAddCommGroup N] [NormedSpace ℝ N] {Q : QuadraticForm ℝ N} {δ : N} {p : N × N} : p ∈ orthogonalityPairs Q δ ↔ QuadraticMap.polar (⇑Q) δ p.1 = 0 ∧ QuadraticMap.polar (⇑Q) δ p.2 = 0

Membership unfolded: a pair is on the orthogonalityLocus of δ when δ is orthogonal to both entries, which is the form the Baire argument and mem_orthogonalityLocus_iff_mem_orthogonal both consume.

theorem PeriodDomain.orthogonalityPairs_ne_top {N : Type u_2} [NormedAddCommGroup N] [NormedSpace ℝ N] {Q : QuadraticForm ℝ N} (hnd : QuadraticMap.Nondegenerate) {δ : N} (hδ : δ ≠ 0) : orthogonalityPairs Q δ ≠ ⊤

For a nonzero class the orthogonalityLocus is a proper subspace of M × M.

Nondegeneracy is what supplies a vector the class does not annihilate, and properness is the whole content: it is what gives the orthogonalityLocus empty interior, and hence a dense complement for Baire to intersect. Without nondegeneracy a class could pair to zero with everything and its orthogonalityLocus would be all of M × M.

theorem PeriodDomain.dense_compl_orthogonalityPairs {N : Type u_2} [NormedAddCommGroup N] [NormedSpace ℝ N] {Q : QuadraticForm ℝ N} (hnd : QuadraticMap.Nondegenerate) {δ : N} (hδ : δ ≠ 0) : Dense (↑(orthogonalityPairs Q δ))ᶜ

Hence its complement is dense.

A proper subspace of a normed space has empty interior — otherwise a ball inside it would generate the whole space — and a set with empty interior has dense complement. This is the input Baire consumes, one class at a time.

theorem PeriodDomain.nonempty_positivePlanesAway {N : Type u_2} [NormedAddCommGroup N] [NormedSpace ℝ N] [FiniteDimensional ℝ N] {Q : QuadraticForm ℝ N} (hsig : HasSignatureTwo Q) {Δ : Set N} (hcount : Δ.Countable) (hzero : ∀ δ ∈ Δ, δ ≠ 0) : (positivePlanesAway Q Δ).Nonempty

The positive-plane locus avoiding the selected classes is nonempty.

The positive frames are open and nonempty, each orthogonality locus of a nonzero class is closed with dense complement, and Baire lets a countable family of them be avoided all at once.