The signature of the real Mukai extension, from the signature of V

PeriodDomain.HasSignatureTwo has been a hypothesis everywhere in route (A). For the Mukai extension it should be a consequence: ℝ × V × ℝ is a hyperbolic plane orthogonal to V, the plane contributes (1, 1), and the rest is V's own signature. With V = NS(X) ⊗ ℝ that reduces the hypothesis to the Hodge index theorem, which is where it should rest.

This is step 2 of the additivity work; step 1 is QuadraticForm/SignatureAdditive.lean.

Shape of the argument

The two summands are the ranges of the obvious inclusions rather than Submodule.prods. That is not cosmetic: a range comes with LinearEquiv.ofInjective, which is exactly the isometry needed to transport a signature computation from ℝ × ℝ and from V into the summand, and it gives the dimension count for free.

The plane's own signature is pinned by two explicit lines — (1, -1) is positive, (1, 1) is negative — plus the counting identity, which forces sigPos = sigNeg = 1 and leaves no radical.

Convention, restated because it is load-bearing

realForm b is half the self-pairing (Mukai/RealForm.lean), so on the plane it is (r, s) ↦ -r * s, and on the middle summand it is c ↦ b c c / 2. Halving does not move definite subspaces, which is sigPos_smul_of_pos below, so V's signature transports unchanged.

noncomputable def QuadraticMap.rangeIsometry {M : Type u_1} [AddCommGroup M] [Module ℝ M] {N : Type u_2} [AddCommGroup N] [Module ℝ N] (Q : QuadraticForm ℝ M) (f : N →ₗ[ℝ] M) (hf : Function.Injective ⇑f) : (comp Q f).IsometryEquiv (restrict Q f.range)

The restriction of a form to the range of an injective map is the form pulled back along that map. This is what makes a range-shaped summand cheap to compute with.

Equations

• QuadraticMap.rangeIsometry Q f hf = { toLinearEquiv := LinearEquiv.ofInjective f hf, map_app' := ⋯ }

theorem QuadraticMap.sigPos_smul_of_pos {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] {c : ℝ} (hc : 0 < c) (Q : QuadraticForm ℝ M) : sigPos (c • Q) = sigPos Q

A positive scalar does not move the positive definite subspaces.

theorem QuadraticMap.sigNeg_smul_of_pos {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] {c : ℝ} (hc : 0 < c) (Q : QuadraticForm ℝ M) : sigNeg (c • Q) = sigNeg Q

The same for sigNeg, which is sigPos of the negative.

def Mukai.hyperbolicIncl (V : Type u_1) [AddCommGroup V] [Module ℝ V] : ℝ × ℝ →ₗ[ℝ] RealExtension V

The inclusion of the hyperbolic plane summand {(r, 0, s)}.

Equations

• Mukai.hyperbolicIncl V = { toFun := fun (p : ℝ × ℝ) => (p.1, 0, p.2), map_add' := ⋯, map_smul' := ⋯ }

def Mukai.middleIncl (V : Type u_1) [AddCommGroup V] [Module ℝ V] : V →ₗ[ℝ] RealExtension V

The inclusion of the middle summand {(0, c, 0)}.

Equations

• Mukai.middleIncl V = { toFun := fun (c : V) => (0, c, 0), map_add' := ⋯, map_smul' := ⋯ }

theorem Mukai.hyperbolicIncl_injective (V : Type u_1) [AddCommGroup V] [Module ℝ V] : Function.Injective ⇑(hyperbolicIncl V)

theorem Mukai.middleIncl_injective (V : Type u_1) [AddCommGroup V] [Module ℝ V] : Function.Injective ⇑(middleIncl V)

def Mukai.hyperbolic (V : Type u_1) [AddCommGroup V] [Module ℝ V] : Submodule ℝ (RealExtension V)

The hyperbolic plane summand.

Equations

• Mukai.hyperbolic V = (Mukai.hyperbolicIncl V).range

def Mukai.middle (V : Type u_1) [AddCommGroup V] [Module ℝ V] : Submodule ℝ (RealExtension V)

The middle summand.

Equations

• Mukai.middle V = (Mukai.middleIncl V).range

theorem Mukai.mem_hyperbolic_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {v : RealExtension V} : v ∈ hyperbolic V ↔ v.2.1 = 0

theorem Mukai.mem_middle_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {v : RealExtension V} : v ∈ middle V ↔ v.1 = 0 ∧ v.2.2 = 0

theorem Mukai.isCompl_hyperbolic_middle {V : Type u_1} [AddCommGroup V] [Module ℝ V] : IsCompl (hyperbolic V) (middle V)

theorem Mukai.orthogonal_hyperbolic_middle {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (hb : ∀ (x y : V), (b x) y = (b y) x) (w : RealExtension V) : w ∈ hyperbolic V → ∀ w' ∈ middle V, QuadraticMap.polar (⇑(realForm b)) w w' = 0

theorem Mukai.comp_hyperbolicIncl_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (p : ℝ × ℝ) : (QuadraticMap.comp (realForm b) (hyperbolicIncl V)) p = -(p.1 * p.2)

The form the plane carries: (r, s) ↦ -r * s.

theorem Mukai.comp_middleIncl_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (c : V) : (QuadraticMap.comp (realForm b) (middleIncl V)) c = (b c) c / 2

The form the middle summand carries: c ↦ b c c / 2.

theorem Mukai.hasSignatureTwo_realForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) [FiniteDimensional ℝ V] (hb : ∀ (x y : V), (b x) y = (b y) x) (hpos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1) (hneg : sigNeg (LinearMap.BilinMap.toQuadraticMap b) + 1 = Module.finrank ℝ V) : PeriodDomain.HasSignatureTwo (realForm b)

The signature of the real Mukai extension, from the signature of V.

With V = NS(X) ⊗ ℝ the hypotheses are the Hodge index theorem, so the signature condition every period-domain result carries stops being an assumption about the Mukai lattice.