Orthogonality loci among positive planes

This file owns the deleted-locus arrangement attached to a real quadratic space. For a class δ, orthogonalityLocus Q δ consists of positive planes orthogonal to δ. After choosing a positive frame, membership is the pair of real equations saying that the associated complex functional kills δ.

This is not a determinant-alignment locus: alignment is one real equation and also contains zero charges and opposite rays. It is not an actual destabilization wall either; there is no category or semistable object here.

def PeriodDomain.IsSphericalClass {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (δ : M) : Prop

A class of pairing square -2.

Equations

• PeriodDomain.IsSphericalClass Q δ = (QuadraticMap.polar (⇑Q) δ δ = -2)

def PeriodDomain.orthogonalityLocus {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (δ : M) : Set (Submodule ℝ M)

The positive planes orthogonal to δ.

Equations

• PeriodDomain.orthogonalityLocus Q δ = {W : Submodule ℝ M | PeriodDomain.IsPositivePlane Q W ∧ ∀ w ∈ W, QuadraticMap.polar (⇑Q) δ w = 0}

def PeriodDomain.sphericalClasses {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (Λ : Set M) : Set M

The spherical classes lying in a chosen set of classes.

Equations

• PeriodDomain.sphericalClasses Q Λ = {δ : M | δ ∈ Λ ∧ PeriodDomain.IsSphericalClass Q δ}

def PeriodDomain.positivePlanesAway {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (Δ : Set M) : Set (Submodule ℝ M)

Positive planes away from all orthogonality loci indexed by Δ.

Equations

• PeriodDomain.positivePlanesAway Q Δ = {W : Submodule ℝ M | W ∈ PeriodDomain.positivePlanes Q ∧ ∀ δ ∈ Δ, W ∉ PeriodDomain.orthogonalityLocus Q δ}

theorem PeriodDomain.isSphericalClass_iff_apply {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {δ : M} : IsSphericalClass Q δ ↔ Q δ = -1

A spherical class has quadratic value -1; the factor two comes from the polar form.

theorem PeriodDomain.mem_orthogonalityLocus_iff_mem_orthogonal {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {W : Submodule ℝ M} {δ : M} (hW : IsPositivePlane Q W) : W ∈ orthogonalityLocus Q δ ↔ δ ∈ orthogonal Q W

A positive plane is in the orthogonality locus of δ exactly when δ lies in its orthogonal complement.

theorem PeriodDomain.notMem_of_isSphericalClass {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {W : Submodule ℝ M} {δ : M} (hW : IsPositivePlane Q W) (hδ : IsSphericalClass Q δ) : δ ∉ W

A spherical class lies in no positive plane.

theorem PeriodDomain.positivePlanesAway_sphericalClasses_univ_eq_empty {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) (hdim : 3 ≤ Module.finrank ℝ M) : positivePlanesAway Q (sphericalClasses Q Set.univ) = ∅

Cutting by every real spherical class empties the positive-plane locus in dimension at least three. This is why a geometric application cuts by a discrete lattice of classes instead.