Isotropic sequences in an integral bilinear lattice

A sequence v : Fin n → Λ in a ℤ-bilinear lattice is isotropic when ⟨v i, v j⟩ = 1 - δᵢⱼ: every member is isotropic and every distinct ordered pair pairs to 1. For n = 10 this is the combinatorial skeleton of the half-fiber configurations on an Enriques surface (Li–Nuer–Stellari–Zhao, arXiv:1912.04332, §2.3), but nothing here mentions a surface: every statement is lattice arithmetic, true whether or not any geometry exists — the same discipline Lattice/Mukai/Basic.lean records for the Mukai extension.

Neither existing isotropy notion is reusable here, which is why a new predicate appears at all: Mukai.IsIsotropic is bound to the Mukai extension's own pairing, and IntegralLattice.NumLattice names the rank-two numerical lattice Fin 2 → ℤ, not an ambient carrier.

Main definitions

• IsIsotropicSequence — the predicate.
• hyperbolicPairing — the Gram matrix !![0, 1; 1, 0] of the hyperbolic plane U, as a bilinear map on Fin 2 → ℤ.

Main results

• IsIsotropicSequence.linearIndependent — for n ≥ 2 an isotropic sequence is linearly independent over ℤ, through the separation statement eq_zero_of_pairing_smul_sum_eq_zero (the Gram argument in elementary form).
• IsIsotropicSequence.pairing_sum_left, pairing_sum_right, pairing_sum_sum — the sum-vector identities ⟨s, v j⟩ = ⟨v j, s⟩ = n - 1 and ⟨s, s⟩ = n(n - 1).
• two geometry-free inhabitants: the hyperbolic plane carries an isotropic 2-sequence, and any lattice carries the degenerate singleton.

Implementation notes

Symmetry is not assumed. The two defining clauses quantify over all ordered pairs, so ⟨v i, v j⟩ and ⟨v j, v i⟩ are each 1 by hypothesis and no symmetry of b enters any proof below. A symmetric lattice loses nothing; an asymmetric pairing (an Euler form before symmetrization) can still carry an isotropic sequence. The left and right sum identities are both provided for exactly this reason.

What is deferred. For s = ∑ i, v i and n = 10 the identities read ⟨s, v j⟩ = 9 and ⟨s, s⟩ = 90, which are the shadows of the Fano class Δ = s/3 with Δ·F_j = 3 and Δ² = 10 — but division by 3 is a statement about divisibility in the lattice, not about the pairing, and is deferred until the rank-ten Enriques lattice exists to state it in.

References

• Li, Nuer, Stellari, Zhao, A refined Derived Torelli Theorem for Enriques surfaces, arXiv:1912.04332, §2.3.

Tags

isotropic sequence, integral lattice, Enriques surface, hyperbolic plane

structure IntegralLattice.IsIsotropicSequence {Λ : Type u_1} [AddCommGroup Λ] (b : Λ →ₗ[ℤ] Λ →ₗ[ℤ] ℤ) {n : ℕ} (v : Fin n → Λ) : Prop

An isotropic sequence: ⟨v i, v j⟩ = 1 - δᵢⱼ, stated as two clauses so neither needs an if. Both clauses range over ordered pairs, which is why no symmetry hypothesis on b appears here or in any consequence.

• self_isotropic (i : Fin n) : (b (v i)) (v i) = 0

  Every member of the sequence is isotropic.

• pairwise_one (i j : Fin n) : i ≠ j → (b (v i)) (v j) = 1

  Every ordered pair of distinct members pairs to 1.

theorem IntegralLattice.IsIsotropicSequence.pairing_ite {Λ : Type u_1} [AddCommGroup Λ] {b : Λ →ₗ[ℤ] Λ →ₗ[ℤ] ℤ} {n : ℕ} {v : Fin n → Λ} (h : IsIsotropicSequence b v) (i j : Fin n) : (b (v i)) (v j) = if i = j then 0 else 1

The two clauses in if normal form, for summing over an index. No symmetry is needed to state either orientation: the if is on the index pair, and pairwise_one covers both orders by hypothesis.

theorem IntegralLattice.IsIsotropicSequence.pairing_smul_sum_left {Λ : Type u_1} [AddCommGroup Λ] {b : Λ →ₗ[ℤ] Λ →ₗ[ℤ] ℤ} {n : ℕ} {v : Fin n → Λ} (h : IsIsotropicSequence b v) (g : Fin n → ℤ) (j : Fin n) : (b (∑ i : Fin n, g i • v i)) (v j) = ∑ i : Fin n, g i - g j

The weighted sum identity: pairing ∑ gᵢ vᵢ against v j reads off the coefficient sum minus the j-th coefficient. This is the single computation behind every result below — the unweighted identity is g = 1 and linear independence is the statement that it separates coefficients.

theorem IntegralLattice.IsIsotropicSequence.pairing_sum_left {Λ : Type u_1} [AddCommGroup Λ] {b : Λ →ₗ[ℤ] Λ →ₗ[ℤ] ℤ} {n : ℕ} {v : Fin n → Λ} (h : IsIsotropicSequence b v) (j : Fin n) : (b (∑ i : Fin n, v i)) (v j) = ↑n - 1

The sum vector pairs to n - 1 against every member. For the Enriques configuration n = 10 this is the ⟨s, F_j⟩ = 9 identity behind Δ·F_j = 3; see the module docstring for why the division by 3 is not taken here.

theorem IntegralLattice.IsIsotropicSequence.pairing_sum_right {Λ : Type u_1} [AddCommGroup Λ] {b : Λ →ₗ[ℤ] Λ →ₗ[ℤ] ℤ} {n : ℕ} {v : Fin n → Λ} (h : IsIsotropicSequence b v) (j : Fin n) : (b (v j)) (∑ i : Fin n, v i) = ↑n - 1

The right-slot companion of pairing_sum_left, provided because no symmetry of b is assumed anywhere in this file.

theorem IntegralLattice.IsIsotropicSequence.pairing_sum_sum {Λ : Type u_1} [AddCommGroup Λ] {b : Λ →ₗ[ℤ] Λ →ₗ[ℤ] ℤ} {n : ℕ} {v : Fin n → Λ} (h : IsIsotropicSequence b v) : (b (∑ i : Fin n, v i)) (∑ i : Fin n, v i) = ↑n * (↑n - 1)

The self-pairing of the sum vector is n(n - 1). For n = 10 this is the ⟨s, s⟩ = 90 identity behind Δ² = 10.

theorem IntegralLattice.IsIsotropicSequence.eq_zero_of_pairing_smul_sum_eq_zero {Λ : Type u_1} [AddCommGroup Λ] {b : Λ →ₗ[ℤ] Λ →ₗ[ℤ] ℤ} {n : ℕ} {v : Fin n → Λ} (h : IsIsotropicSequence b v) (hn : 2 ≤ n) (g : Fin n → ℤ) (hg : ∀ (j : Fin n), (b (∑ i : Fin n, g i • v i)) (v j) = 0) (i : Fin n) : g i = 0

An isotropic sequence of length at least two separates coefficients: if ∑ gᵢ vᵢ pairs to zero against every member, every coefficient vanishes. This is non-degeneracy of the pairing on the span of the sequence, stated without mentioning the span; linearIndependent is its immediate consumer, and the Torelli-lane numerical steps consume it directly when the vanishing comes from geometry rather than from a linear relation.

By pairing_smul_sum_left, the hypothesis says every coefficient equals the common sum S; summing again gives S = nS, and n ≥ 2 forces S = 0 in ℤ.

theorem IntegralLattice.IsIsotropicSequence.linearIndependent {Λ : Type u_1} [AddCommGroup Λ] {b : Λ →ₗ[ℤ] Λ →ₗ[ℤ] ℤ} {n : ℕ} {v : Fin n → Λ} (h : IsIsotropicSequence b v) (hn : 2 ≤ n) : LinearIndependent ℤ v

An isotropic sequence of length at least two is linearly independent over ℤ. The hypothesis 2 ≤ n is necessary at n = 1: the single vector may be 0, as the degenerate inhabitant below shows (at n = 0 the statement is vacuous).

Two geometry-free inhabitants

The hyperbolic witness is the honest one: U's standard basis is a genuine isotropic 2-sequence, and it is the seed from which the Enriques lattice U ⊕ E₈(−1) will grow its length-ten sequences. The singleton 0 is the degenerate boundary case, and it is why linearIndependent needs 2 ≤ n.

def IntegralLattice.hyperbolicPairing : (Fin 2 → ℤ) →ₗ[ℤ] (Fin 2 → ℤ) →ₗ[ℤ] ℤ

The hyperbolic pairing on ℤ²: ⟨x, y⟩ = x₀y₁ + x₁y₀, the Gram matrix !![0, 1; 1, 0] of the hyperbolic plane U.

Equations

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

@[simp]

theorem IntegralLattice.hyperbolicPairing_apply (x y : Fin 2 → ℤ) : (hyperbolicPairing x) y = x 0 * y 1 + x 1 * y 0

theorem IntegralLattice.isIsotropicSequence_hyperbolic : IsIsotropicSequence hyperbolicPairing ![![1, 0], ![0, 1]]

The standard basis of the hyperbolic plane is an isotropic 2-sequence: ⟨e, e⟩ = ⟨f, f⟩ = 0 and ⟨e, f⟩ = ⟨f, e⟩ = 1.

theorem IntegralLattice.isIsotropicSequence_zero_singleton {Λ : Type u_1} [AddCommGroup Λ] (b : Λ →ₗ[ℤ] Λ →ₗ[ℤ] ℤ) : IsIsotropicSequence b ![0]

Any lattice carries the degenerate singleton sequence ![0]: the self-pairing clause is b 0 0 = 0 and the pairwise clause is vacuous. This is the boundary case excluded by linearIndependent's 2 ≤ n.