Rank-two Gram determinants of a bilinear form

For a module M over a commutative ring R with a bilinear form B, the Gram determinant of a pair is B v v * B w w - (B v w)^2, and the pair is hyperbolic when that determinant is negative -- signature (1, 1) for a rank-two lattice.

This is stated over an arbitrary ambient form, not over one extension

Lattice/Mukai/RankTwo.lean used to own these identities on the single carrier ℤ × N × ℤ, but every one of them is arithmetic of two vectors under a bilinear form. They are restated here on (R, M, B) and the Mukai file specialises them at B := Mukai.pairingBilin b.

The file splits at the point where order is needed, which is also where the hypotheses stop being purely algebraic:

• gram, the change-of-basis identity and orthWitness need only a commutative ring, and apply_orthWitness needs no symmetry either;
• IsHyperbolicPair and everything reading a sign need a linear order and a strict ordered ring structure.

What is deliberately not here

HasSphericalClass and HasIsotropicClass stay with the Mukai lane. They are phrased in terms of IsSpherical and IsIsotropic, which are application vocabulary for -2 and 0, and the ledger keeps that vocabulary with the application.

No geometry is asserted. The correspondence between rank-two data and actual walls in a space of stability conditions is Bayer--Macrì Theorem 5.7; it needs moduli of stable objects and is not formalised anywhere below.

def BilinearForm.gram {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (v w : M) : R

The Gram determinant of the pair (v, w): B v v * B w w - (B v w)^2.

Equations

• BilinearForm.gram B v w = (B v) v * (B w) w - (B v) w ^ 2

theorem BilinearForm.gram_comm {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) (v w : M) : gram B v w = gram B w v

@[simp]

theorem BilinearForm.gram_zero_left {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (w : M) : gram B 0 w = 0

@[simp]

theorem BilinearForm.gram_zero_right {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (v : M) : gram B v 0 = 0

theorem BilinearForm.apply_lincomb {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) (a₁ a₂ a₃ a₄ : R) (v w : M) : (B (a₁ • v + a₂ • w)) (a₃ • v + a₄ • w) = a₁ * a₃ * (B v) v + (a₁ * a₄ + a₂ * a₃) * (B v) w + a₂ * a₄ * (B w) w

theorem BilinearForm.self_lincomb {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) (a₁ a₂ : R) (v w : M) : (B (a₁ • v + a₂ • w)) (a₁ • v + a₂ • w) = a₁ ^ 2 * (B v) v + 2 * (a₁ * a₂) * (B v) w + a₂ ^ 2 * (B w) w

theorem BilinearForm.gram_lincomb {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) (a₁ a₂ a₃ a₄ : R) (v w : M) : gram B (a₁ • v + a₂ • w) (a₃ • v + a₄ • w) = (a₁ * a₄ - a₂ * a₃) ^ 2 * gram B v w

def BilinearForm.orthWitness {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (v w : M) : M

B v w • v - B v v • w, the projection of w off v cleared of denominators. Orthogonal to v with no symmetry hypothesis.

Equations

• BilinearForm.orthWitness B v w = (B v) w • v - (B v) v • w

theorem BilinearForm.apply_orthWitness {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (v w : M) : (B v) (orthWitness B v w) = 0

theorem BilinearForm.self_orthWitness {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) (v w : M) : (B (orthWitness B v w)) (orthWitness B v w) = (B v) v * gram B v w

def BilinearForm.pairSpan {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (v w : M) : Set M

The set of R-combinations of v and w.

Equations

• BilinearForm.pairSpan v w = {x : M | ∃ (a₁ : R) (a₂ : R), x = a₁ • v + a₂ • w}

theorem BilinearForm.mem_pairSpan_left {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (v w : M) : v ∈ pairSpan v w

theorem BilinearForm.mem_pairSpan_right {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (v w : M) : w ∈ pairSpan v w

theorem BilinearForm.orthWitness_mem_pairSpan {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (v w : M) : orthWitness B v w ∈ pairSpan v w

def BilinearForm.IsHyperbolicPair {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (v w : M) : Prop

Negative Gram determinant: the rank-two form spanned by v and w is indefinite. For a rank-two lattice this is signature (1, 1).

A numerical condition on two vectors, and not a claim that a wall exists in any space of stability conditions.

Equations

• BilinearForm.IsHyperbolicPair B v w = (BilinearForm.gram B v w < 0)

theorem BilinearForm.isHyperbolicPair_iff {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (v w : M) : IsHyperbolicPair B v w ↔ (B v) v * (B w) w < (B v) w ^ 2

theorem BilinearForm.discr_pos_of_isHyperbolicPair {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {v w : M} (h : IsHyperbolicPair B v w) : 0 < 4 * ((B v) w ^ 2 - (B v) v * (B w) w)

theorem BilinearForm.gram_ne_zero_of_isHyperbolicPair {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {v w : M} (h : IsHyperbolicPair B v w) : gram B v w ≠ 0

theorem BilinearForm.ne_zero_left_of_isHyperbolicPair {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {v w : M} (h : IsHyperbolicPair B v w) : v ≠ 0

theorem BilinearForm.ne_zero_right_of_isHyperbolicPair {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {v w : M} (h : IsHyperbolicPair B v w) : w ≠ 0

theorem BilinearForm.isHyperbolicPair_comm {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) (v w : M) : IsHyperbolicPair B v w ↔ IsHyperbolicPair B w v

theorem BilinearForm.isHyperbolicPair_lincomb {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) {a₁ a₂ a₃ a₄ : R} (hd : (a₁ * a₄ - a₂ * a₃) ^ 2 = 1) {v w : M} (h : IsHyperbolicPair B v w) : IsHyperbolicPair B (a₁ • v + a₂ • w) (a₃ • v + a₄ • w)

theorem BilinearForm.self_orthWitness_neg {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) {v w : M} (hv : 0 < (B v) v) (h : IsHyperbolicPair B v w) : (B (orthWitness B v w)) (orthWitness B v w) < 0

theorem BilinearForm.orthWitness_ne_zero {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) {v w : M} (hv : 0 < (B v) v) (h : IsHyperbolicPair B v w) : orthWitness B v w ≠ 0

theorem BilinearForm.exists_neg_self_of_isHyperbolicPair {R : Type u_1} {M : Type u_2} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) {v w : M} (hv : 0 < (B v) v) (h : IsHyperbolicPair B v w) : ∃ x ∈ pairSpan v w, x ≠ 0 ∧ (B x) x < 0