Hyperbolic pairs and Siegel–Eichler transvections

The two elementary ingredients of the Witt extension theorem, and hence of Witt cancellation (Dias II.6.1–6.4, Baeza III.2–III.4):

• a hyperbolic pair in a quadratic module is a pair u, v with q u = q v = 0 and polar q u v = 1;
• the Siegel–Eichler transvection E(x, y) attached to x isotropic and y orthogonal to x is the isometry z ↦ z + b(z,x) • y - (b(z,y) + q y * b(z,x)) • x.

Transvections are the characteristic-2-safe substitute for hyperplane reflections: they are defined for every commutative ring and need no invertible scalar, whereas the reflection σ_x requires q x to be a unit. This is why the Dias/Baeza/Knebusch route to cancellation survives characteristic 2, and it is the reason overview §8 prescribes it over GN's cohomological proof.

Main definitions

• QuadraticForm.plane R : the hyperbolic plane (a, b) ↦ a * b on R × R. This is the elementary model, defined without dual modules, of QuadraticForm.dualProd R R.
• QuadraticMap.IsHyperbolicPair Q u v : Q u = 0, Q v = 0, polar Q u v = 1.
• QuadraticMap.eichler hx hxy : the transvection, TauCeti's QuadraticMap.transvection, as a self-isometry of Q.
• QuadraticMap.IsHyperbolicPair.dilation : the dilation along a hyperbolic pair, TauCeti's TauCeti.QuadraticMap.hyperbolicPairTorus, as a self-isometry of Q.

Main results

• QuadraticMap.eichler_apply : the formula for E(x, y).
• QuadraticMap.IsHyperbolicPair.decomposition : any w is b(w,v) • u + b(w,u) • v plus a vector orthogonal to both u and v. This replaces, in explicit form, the splitting V = ⟨u, v⟩ ⊥ ⟨u, v⟩^⊥ that Dias II.6.2 uses.
• QuadraticMap.IsHyperbolicPair.exists_isometryEquiv_of_isUnit : the unit case of Dias II.6.2. If i = α • u + β • v + z with α a unit and z orthogonal to u and v, then some self-isometry of Q carries the hyperbolic pair (u, v) to the hyperbolic pair (i, j). Reducing the general case to this one is what needs the LG axiom, and is done in QuadraticForm/PlaneTransitivity.lean.

References

• I. Dias, Formas Quadráticas Sobre LG-Anéis, Ph.D. thesis, Universidade Estadual de Campinas, 1988, II.6.
• R. Baeza, Quadratic Forms over Semilocal Rings, Lecture Notes in Math. 655, Springer 1978, III, (1.5), (1.6), (2.2), (4.2).

def QuadraticForm.plane (R : Type u) [CommRing R] : QuadraticForm R (R × R)

The hyperbolic plane (a, b) ↦ a * b on R × R.

This is the elementary model of QuadraticForm.dualProd R R, written without dual modules so that computations with an explicit hyperbolic pair stay computational.

Equations

• QuadraticForm.plane R = QuadraticMap.linMulLin (LinearMap.fst R R R) (LinearMap.snd R R R)

@[simp]

theorem QuadraticForm.plane_apply {R : Type u} [CommRing R] (x : R × R) : (plane R) x = x.1 * x.2

theorem QuadraticForm.polar_plane {R : Type u} [CommRing R] (x y : R × R) : QuadraticMap.polar (⇑(plane R)) x y = x.1 * y.2 + x.2 * y.1

@[simp]

theorem QuadraticForm.polar_plane_one {R : Type u} [CommRing R] (x : R × R) : QuadraticMap.polar (⇑(plane R)) 1 x = x.1 + x.2

The polar form of the hyperbolic plane at the unit of R × R is the sum of the coordinates. This is the trace of the split quadratic étale algebra.

Hyperbolic pairs

structure QuadraticMap.IsHyperbolicPair {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) (u v : V) : Prop

A hyperbolic pair of a quadratic module: two isotropic vectors pairing to 1 under the un-halved polar form. The submodule they span is a hyperbolic plane.

• apply_left : Q u = 0

  The first vector is isotropic.

• apply_right : Q v = 0

  The second vector is isotropic.

• polar_eq_one : polar (⇑Q) u v = 1

  The two vectors pair to 1.

theorem QuadraticMap.IsHyperbolicPair.symm {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {u v : V} (h : IsHyperbolicPair Q u v) : IsHyperbolicPair Q v u

theorem QuadraticMap.IsHyperbolicPair.polar_self_left {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {u v : V} (h : IsHyperbolicPair Q u v) : polar (⇑Q) u u = 0

theorem QuadraticMap.IsHyperbolicPair.polar_self_right {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {u v : V} (h : IsHyperbolicPair Q u v) : polar (⇑Q) v v = 0

theorem QuadraticMap.IsHyperbolicPair.plane (R : Type u) [CommRing R] : IsHyperbolicPair (QuadraticForm.plane R) (1, 0) (0, 1)

The standard hyperbolic pair of the hyperbolic plane.

theorem QuadraticMap.IsHyperbolicPair.decomposition {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {u v : V} (h : IsHyperbolicPair Q u v) (w : V) : polar (⇑Q) (w - polar (⇑Q) w v • u - polar (⇑Q) w u • v) u = 0 ∧ polar (⇑Q) (w - polar (⇑Q) w v • u - polar (⇑Q) w u • v) v = 0

The explicit splitting along a hyperbolic pair. Every w is the sum of its components along u and v and a vector orthogonal to both.

This is the computational form of V = ⟨u, v⟩ ⊥ ⟨u, v⟩^⊥, and it is all that Dias II.6.2 uses of that decomposition.

Siegel–Eichler transvections

The transvection, its isometry property and its bijectivity are TauCeti's QuadraticMap.transvection; here it is packaged as a self-isometry of Q, with its formula in the variables used below.

noncomputable def QuadraticMap.eichler {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {x y : V} (hx : Q x = 0) (hxy : polar (⇑Q) x y = 0) : IsometryEquiv Q Q

The Siegel–Eichler transvection E(x, y) attached to an isotropic x and a vector y orthogonal to it, as a self-isometry of Q: E(x, y) z = z + b(z, x) • y - (b(z, y) + q y * b(z, x)) • x. It is TauCeti's QuadraticMap.transvection. Unlike a hyperplane reflection it needs no unit, so it is available in characteristic 2 and over any commutative ring.

Equations

• QuadraticMap.eichler hx hxy = (TauCeti.QuadraticMap.orthogonalGroupEquivIsometryEquiv Q) ⟨QuadraticMap.transvection Q hx hxy, ⋯⟩

@[simp]

theorem QuadraticMap.eichler_apply {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {x y : V} (hx : Q x = 0) (hxy : polar (⇑Q) x y = 0) (z : V) : (eichler hx hxy) z = z + polar (⇑Q) x z • y - (polar (⇑Q) y z + Q y * polar (⇑Q) x z) • x

theorem QuadraticMap.isHyperbolicPair_neg_smul_add {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {u w : V} (hu : Q u = 0) (huw : polar (⇑Q) u w = 1) : IsHyperbolicPair Q u (-Q w • u + w)

Building a hyperbolic pair from a dual vector. If u is isotropic and some w pairs with it to 1, then (u, -q(w) • u + w) is a hyperbolic pair. This is the construction in the proof of GPR 11.17, isolated from the hypotheses used to produce w.

Only additivity is used, so this is valid in characteristic 2: the correction term -q(w) • u replaces the "complete the square" step that would divide by 2.

The expansion of Q along a hyperbolic pair

theorem QuadraticMap.IsHyperbolicPair.apply_add_smul_add_smul {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {u v : V} (h : IsHyperbolicPair Q u v) (w : V) (s t : R) : Q (w + s • u + t • v) = Q w + s * polar (⇑Q) w u + t * polar (⇑Q) w v + s * t

Expanding Q on a vector shifted by the two members of a hyperbolic pair. All the identities below are corollaries of this one computation.

theorem QuadraticMap.IsHyperbolicPair.map {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {u v : V} {V' : Type w} [AddCommGroup V'] [Module R V'] {Q' : QuadraticForm R V'} (h : IsHyperbolicPair Q u v) (f : IsometryEquiv Q Q') : IsHyperbolicPair Q' (f u) (f v)

A hyperbolic pair is carried to a hyperbolic pair by an isometry.

Dilations along a hyperbolic pair

noncomputable def QuadraticMap.IsHyperbolicPair.dilation {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {u v : V} (h : IsHyperbolicPair Q u v) (l : Rˣ) : IsometryEquiv Q Q

The dilation φ(l) attached to a hyperbolic pair (u, v) and a unit l: it scales u by l, scales v by l⁻¹, and fixes every vector orthogonal to both (Baeza III §2's P(λ), Dias II.6's φ(λ)). It is TauCeti's TauCeti.QuadraticMap.hyperbolicPairTorus, packaged as a self-isometry of Q. Unlike a Siegel–Eichler transvection it needs a unit, but only a unit of R, never an invertible value of the form.

Equations

• h.dilation l = (TauCeti.QuadraticMap.orthogonalGroupEquivIsometryEquiv Q) ((TauCeti.QuadraticMap.hyperbolicPairTorus Q ⋯ ⋯ ⋯) l)

theorem QuadraticMap.IsHyperbolicPair.dilation_left {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {u v : V} (h : IsHyperbolicPair Q u v) (l : Rˣ) : (h.dilation l) u = ↑l • u

The dilation φ(l) scales u by l.

Moving one hyperbolic pair to another: the unit case

theorem QuadraticMap.IsHyperbolicPair.exists_isometryEquiv_of_isUnit {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {u v : V} (huv : IsHyperbolicPair Q u v) {i j : V} (hij : IsHyperbolicPair Q i j) {a : Rˣ} {b : R} {z : V} (hzu : polar (⇑Q) u z = 0) (hzv : polar (⇑Q) v z = 0) (hi : i = z + ↑a • u + b • v) : ∃ (σ : IsometryEquiv Q Q), σ u = i ∧ σ v = j

The unit case of Dias II.6.2. Let (u, v) be a hyperbolic pair and let (i, j) be another one whose first vector i = z + α • u + β • v has α a unit, with z orthogonal to u and v. Then a self-isometry of Q carries (u, v) to (i, j).

The isometry is an explicit product E(i, z') ∘ E(v, α⁻¹ • z) ∘ φ(α) of two Siegel–Eichler transvections and a dilation, exactly as in Dias II.6.2 (Baeza III (4.2)). Nothing here needs the base ring to be an LG ring: that hypothesis enters only in reducing the general case to this one, by producing the unit α (Dias II.6.1).