Signature consequences for a paired complex functional #
This downstream module combines the wall-independent functional/kernel algebra with positive-plane and signature theory. Kernel negativity is one half of a quadratic support criterion; it is not by itself the full support property.
theorem
PeriodDomain.neg_of_centralCharge_eq_zero
{M : Type u_1}
[AddCommGroup M]
[Module ℝ M]
{Q : QuadraticForm ℝ M}
[FiniteDimensional ℝ M]
(hsig : HasSignatureTwo Q)
{x y : M}
(hxy : IsPositiveFrame Q x y)
{v : M}
(hv : centralCharge Q x y v = 0)
(hv0 : v ≠ 0)
:
On the kernel of the paired complex functional the form is negative definite. A full support claim additionally requires nonnegativity on the relevant semistable classes.
theorem
PeriodDomain.centralCharge_ne_zero_of_nonneg
{M : Type u_1}
[AddCommGroup M]
[Module ℝ M]
{Q : QuadraticForm ℝ M}
[FiniteDimensional ℝ M]
(hsig : HasSignatureTwo Q)
{x y : M}
(hxy : IsPositiveFrame Q x y)
{v : M}
(hv : 0 ≤ Q v)
(hv0 : v ≠ 0)
:
No nonzero class of nonnegative square lies in the kernel.
theorem
PeriodDomain.isCompl_ker_centralCharge
{M : Type u_1}
[AddCommGroup M]
[Module ℝ M]
{Q : QuadraticForm ℝ M}
[FiniteDimensional ℝ M]
{x y : M}
(hxy : IsPositiveFrame Q x y)
:
IsCompl (pairSpan x y) (orthogonal Q (pairSpan x y))
The positive-frame span and the functional kernel split the space.