Dias II.6.1–II.6.2: transitivity on hyperbolic pairs

Not the Witt extension theorem — nothing here extends an isometry between submodules to the whole module. What is proved is the single statement Witt cancellation needs: the isometry group of plane ⊥ q acts transitively on hyperbolic pairs. Dias II.6.1 is the step of it that uses the LG axiom, and the only one in the whole chain that does.

Work in plane ⊥ q₀ on (R × R) × M₀, with standard hyperbolic pair u = ((1,0), 0), v = ((0,1), 0). A vector is i = ((α, β), m), and applying the Siegel–Eichler transvection E(u, (0, y)) to it gives

E(u, (0, y)) i = ((α - b(y, m) - β * q₀ y, β), m + β • y),

so the u-coefficient changes from α to α - b(y, m) - β·q₀(y). Dias II.6.1 says that over an LG ring one can choose y making that a unit, after which QuadraticMap.IsHyperbolicPair.exists_isometryEquiv_of_isUnit finishes the job.

The residue-field core

Over a field, with q₀ non-singular, α β + q₀ m = 0 (isotropy of i) and α ≠ 0, β ≠ 0 or q₀(m, ·) ≠ 0 (a consequence of unimodularity of i), the value α - b(y, m) - β q₀ y is nonzero for a suitable y:

• α ≠ 0 — take y = 0;
• α = 0 and m ≠ 0 — then q₀ m = 0, so m is a nonzero isotropic vector and extends to a hyperbolic pair (m, y) (exists_isHyperbolicPair_of_radical_eq_bot); the value is -1;
• α = 0 and m = 0 — then β ≠ 0 (the third disjunct is vacuous when m = 0), and any y with q₀ y ≠ 0 (QuadraticForm.exists_apply_ne_zero_of_radical_eq_bot) gives the value -β q₀ y.

The last case needs M₀ ⊗ κ(𝔪) ≠ 0 — Baeza's rank hypothesis in Baeza III (2.3), Dias's V₀ ≠ 0. Both sources assume it globally. Here it is needed only at those maximal ideals where α is not already a unit, since where it is, y = 0 works and the residue-field core is never called. That is what lets the hypothesis be dispensed with entirely.

The locus where M₀ vanishes

Where M₀ ⊗ κ(𝔪) = 0 the form plane ⊥ q₀ reduces to the plane at 𝔪, and there the hyperbolic pair (u, v) and the pair (β • v, β⁻¹ • u) are exchanged by the switch, which is not a product of transvections and dilations — it has the opposite Dickson invariant. No amount of Eichler theory reaches it.

The locus is clopen: it is cut out by Module.rankIdempotent R M₀ 0 (Module/RankDecomposition.lean), which annihilates M₀ and reduces to 1 on the locus. Rather than splitting R into a product of rings, QuadraticForm.switchIdem performs the switch on the locus and the identity off it — one isometry, defined over R. Applying it first makes the u-coefficient a unit at exactly the maximal ideals where M₀ dies, so Dias II.6.1 can be run with no hypothesis on the support of M₀ at all.

Main results

• QuadraticForm.exists_ne_zero_sub_polar_sub_smul : the residue-field core, above.
• QuadraticForm.exists_isUnit_sub_polar_sub_smul : Dias II.6.1, the LG step.
• QuadraticForm.switchIdem : the partial switch.
• QuadraticForm.exists_isometryEquiv_of_isHyperbolicPair : Dias II.6.2 — the isometry group of plane ⊥ q is transitive on hyperbolic pairs.
• QuadraticForm.isometryEquiv_of_isometryEquiv_plane_prod_of_isLGRing : cancellation of one hyperbolic plane. QuadraticForm/WittCancellation.lean passes from this to GN 6.5.

References

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

theorem QuadraticForm.exists_ne_zero_sub_polar_sub_smul {F : Type u} [Field F] {W : Type v} [AddCommGroup W] [Module F W] [Nontrivial W] {q : QuadraticForm F W} (hq : QuadraticMap.radical q = ⊥) {a b : F} {w : W} (hiso : a * b + q w = 0) (hnz : a ≠ 0 ∨ b ≠ 0 ∨ ∃ (z : W), QuadraticMap.polar (⇑q) w z ≠ 0) : ∃ (y : W), a - QuadraticMap.polar (⇑q) y w - b * q y ≠ 0

The residue-field core of Dias II.6.1. Let q be a quadratic form with vanishing radical on a nonzero vector space over a field, let a * b + q w = 0, and suppose one of a, b, q(w, ·) is nonzero. Then some y makes a - q(y, w) - b * q y nonzero.

This is the value taken by the u-coefficient of E(u, (0, y)) i for i = ((a, b), w); the three cases are those listed in the module docstring. Non-singularity of q enters twice: to extend an isotropic vector to a hyperbolic pair, and to guarantee that q is not identically zero.

The polynomial of Dias II.6.1

The function y ↦ α - b(y, m) - β * q y is an inhomogeneous quadratic polynomial function. On a free module it is computed by an explicit MvPolynomial, in the same way GPR 11.8 (QuadraticForm.toMvPolynomial) computes q itself: a constant term, a linear term from the polar form, and -β times the polynomial of q.

theorem QuadraticForm.polar_sum_smul_left {S : Type u_1} [CommRing S] {P : Type u_2} [AddCommGroup P] [Module S P] {ι : Type u_3} [Fintype ι] (Q : QuadraticForm S P) (f : ι → S) (g : ι → P) (w : P) : QuadraticMap.polar (⇑Q) (∑ i : ι, f i • g i) w = ∑ i : ι, f i * QuadraticMap.polar (⇑Q) (g i) w

The polar form evaluated on a finite linear combination.

noncomputable def QuadraticForm.eichlerMvPolynomial {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {n : ℕ} (α β : R) (q : QuadraticForm R M) (m : M) (bm : Module.Basis (Fin n) R M) : MvPolynomial (Fin n) R

The polynomial computing y ↦ α - b(y, m) - β * q y in the basis bm.

Equations

• QuadraticForm.eichlerMvPolynomial α β q m bm = MvPolynomial.C α - ∑ i : Fin n, MvPolynomial.C (QuadraticMap.polar (⇑q) (bm i) m) * MvPolynomial.X i - MvPolynomial.C β * q.toMvPolynomial bm

theorem QuadraticForm.aeval_eichlerMvPolynomial_self {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {n : ℕ} {α β : R} {q : QuadraticForm R M} {m : M} {bm : Module.Basis (Fin n) R M} (t : Fin n → R) : (MvPolynomial.aeval t) (eichlerMvPolynomial α β q m bm) = α - QuadraticMap.polar (⇑q) (∑ i : Fin n, t i • bm i) m - β * q (∑ i : Fin n, t i • bm i)

The defining property of eichlerMvPolynomial, over R itself.

theorem QuadraticForm.polar_baseChangeOfProjective_tmul {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (S : Type u_1) [CommRing S] [Algebra R S] (Q : QuadraticForm R M) (x y : M) : QuadraticMap.polar (⇑(baseChangeOfProjective S Q)) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] y) = (algebraMap R S) (QuadraticMap.polar (⇑Q) x y)

The polar form of a base-changed form on a pair of pure tensors.

theorem QuadraticForm.aeval_eichlerMvPolynomial {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {n : ℕ} {α β : R} {q : QuadraticForm R M} {m : M} {bm : Module.Basis (Fin n) R M} (S : Type u_1) [CommRing S] [Algebra R S] (s : Fin n → S) : (MvPolynomial.aeval s) (eichlerMvPolynomial α β q m bm) = (algebraMap R S) α - QuadraticMap.polar (⇑(baseChangeOfProjective S q)) (∑ i : Fin n, s i • 1 ⊗ₜ[R] bm i) (1 ⊗ₜ[R] m) - (algebraMap R S) β * (baseChangeOfProjective S q) (∑ i : Fin n, s i • 1 ⊗ₜ[R] bm i)

The defining property of eichlerMvPolynomial after base change: GPR 11.8 for the inhomogeneous polynomial.

Dias II.6.1 over an LG ring

theorem QuadraticForm.exists_isUnit_sub_polar_sub_smul {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (hLG : IsLGRing R) [Module.Finite R M] [Module.Projective R M] {q : QuadraticForm R M} (hq : q.IsGPRNonsingular) {α β : R} {m : M} (hiso : α * β + q m = 0) (hnz : ∀ (𝔪 : Ideal R), 𝔪.IsMaximal → α ∉ 𝔪 ∨ β ∉ 𝔪 ∨ ∃ (n : M), QuadraticMap.polar (⇑q) m n ∉ 𝔪) (hM : ∀ (𝔪 : Ideal R), 𝔪.IsMaximal → α ∉ 𝔪 ∨ Nontrivial (TensorProduct R (R ⧸ 𝔪) M)) : ∃ (y : M), IsUnit (α - QuadraticMap.polar (⇑q) y m - β * q y)

Dias II.6.1. Over an LG ring, for q non-singular on a finitely generated projective module, and α β m with α β + q m = 0 whose reductions never vanish simultaneously, some y makes α - q(y, m) - β * q y a unit.

Applied to i = ((α, β), m) in plane ⊥ q, this says the Siegel–Eichler transvection E(u, (0,y)) can be chosen to make the u-coefficient of i a unit — the hypothesis of QuadraticMap.IsHyperbolicPair.exists_isometryEquiv_of_isUnit.

The LG axiom is applied to QuadraticForm.eichlerMvPolynomial written in the standard basis of a presentation Rⁿ ↠ M; as in QuadraticForm/Representation.lean, pulling back along the presentation is what removes any need for M to be free.

hM is what replaces Baeza's rank hypothesis and Dias's V₀ ≠ 0: M need only be nonzero at those residue fields where α itself is not already a unit. Where it is, y = 0 works and the residue-field core is not called at all. Full support (Module.HasFullSupport) implies hM, but is strictly stronger — it fails for M = 0, which the cancellation theorem has to cover.

Dias II.6.2 and cancellation of a plane

The partial switch

The switch (x, y) ↦ (y, x) of the plane is an isometry that no product of transvections and dilations can equal — it has the opposite Dickson invariant. An idempotent ε lets it be applied on the clopen piece D(ε) of Spec R and not on the complement, still as a single global isometry: (x, y) ↦ (εy + (1-ε)x, εx + (1-ε)y). This is the one move outside the Eichler group that the argument needs, and it is exactly what handles the locus where M vanishes.

def QuadraticForm.switchIdemPlaneMap {R : Type u} [CommRing R] (ε : R) : R × R →ₗ[R] R × R

The partial switch of the plane: the switch on D(ε), the identity on D(1 - ε).

Equations

• QuadraticForm.switchIdemPlaneMap ε = (ε • LinearMap.snd R R R + (1 - ε) • LinearMap.fst R R R).prod (ε • LinearMap.fst R R R + (1 - ε) • LinearMap.snd R R R)

@[simp]

theorem QuadraticForm.switchIdemPlaneMap_apply {R : Type u} [CommRing R] (ε : R) (x : R × R) : (switchIdemPlaneMap ε) x = (ε * x.2 + (1 - ε) * x.1, ε * x.1 + (1 - ε) * x.2)

def QuadraticForm.switchIdemMap {R : Type u} [CommRing R] (ε : R) (M : Type v) [AddCommGroup M] [Module R M] : (R × R) × M →ₗ[R] (R × R) × M

The partial switch of plane ⊥ q, acting on the plane and fixing M.

Equations

• QuadraticForm.switchIdemMap ε M = (QuadraticForm.switchIdemPlaneMap ε).prodMap LinearMap.id

@[simp]

theorem QuadraticForm.switchIdemMap_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (ε : R) (x : (R × R) × M) : (switchIdemMap ε M) x = ((ε * x.1.2 + (1 - ε) * x.1.1, ε * x.1.1 + (1 - ε) * x.1.2), x.2)

theorem QuadraticForm.switchIdemMap_switchIdemMap {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ε : R} (hε : IsIdempotentElem ε) (x : (R × R) × M) : (switchIdemMap ε M) ((switchIdemMap ε M) x) = x

The partial switch is an involution, because ε is idempotent.

theorem QuadraticForm.apply_switchIdemMap {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ε : R} (hε : IsIdempotentElem ε) (q : QuadraticForm R M) (x : (R × R) × M) : (QuadraticMap.prod (plane R) q) ((switchIdemMap ε M) x) = (QuadraticMap.prod (plane R) q) x

The partial switch preserves plane ⊥ q: on the plane the product x * y is ε times the switched product plus 1 - ε times the original, and ε(1 - ε) = 0.

noncomputable def QuadraticForm.switchIdem {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ε : R} (hε : IsIdempotentElem ε) (q : QuadraticForm R M) : (QuadraticMap.prod (plane R) q).IsometryEquiv (QuadraticMap.prod (plane R) q)

The partial switch as a self-isometry of plane ⊥ q.

Equations

• QuadraticForm.switchIdem hε q = { toLinearEquiv := LinearEquiv.ofBijective (QuadraticForm.switchIdemMap ε M) ⋯, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.switchIdem_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ε : R} (hε : IsIdempotentElem ε) (q : QuadraticForm R M) (x : (R × R) × M) : (switchIdem hε q) x = ((ε * x.1.2 + (1 - ε) * x.1.1, ε * x.1.1 + (1 - ε) * x.1.2), x.2)

theorem QuadraticForm.switchIdem_switchIdem {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {ε : R} (hε : IsIdempotentElem ε) (q : QuadraticForm R M) (x : (R × R) × M) : (switchIdem hε q) ((switchIdem hε q) x) = x

theorem QuadraticForm.exists_isometryEquiv_of_isHyperbolicPair_of_notMem {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (hLG : IsLGRing R) [Module.Finite R M] [Module.Projective R M] {q : QuadraticForm R M} (hq : q.IsGPRNonsingular) (α β : R) (m : M) (j : (R × R) × M) (hij : (QuadraticMap.prod (plane R) q).IsHyperbolicPair ((α, β), m) j) (hM : ∀ (𝔪 : Ideal R), 𝔪.IsMaximal → α ∉ 𝔪 ∨ Nontrivial (TensorProduct R (R ⧸ 𝔪) M)) : ∃ (σ : (QuadraticMap.prod (plane R) q).IsometryEquiv (QuadraticMap.prod (plane R) q)), σ ((1, 0), 0) = ((α, β), m) ∧ σ ((0, 1), 0) = j

Dias II.6.2, the case where the u-coefficient is a unit where M vanishes. Over an LG ring, if q is non-singular on a finitely generated projective module and α is a unit at every residue field where M dies, then the hyperbolic pair (((α, β), m), j) is the image of the standard one under a self-isometry.

The proof is Dias II.6.1 (exists_isUnit_sub_polar_sub_smul) followed by the unit case (QuadraticMap.IsHyperbolicPair.exists_isometryEquiv_of_isUnit): the transvection E(u, (0, y)) moves the given pair to one whose u-coefficient is a unit, and the unit case moves the standard pair to that; composing with E(u, (0, y))⁻¹ finishes.

exists_isometryEquiv_of_isHyperbolicPair removes the hypothesis hM by a partial switch.

theorem QuadraticForm.exists_isometryEquiv_of_isHyperbolicPair {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (hLG : IsLGRing R) [Module.Finite R M] [Module.Projective R M] {q : QuadraticForm R M} (hq : q.IsGPRNonsingular) (i j : (R × R) × M) (hij : (QuadraticMap.prod (plane R) q).IsHyperbolicPair i j) : ∃ (σ : (QuadraticMap.prod (plane R) q).IsometryEquiv (QuadraticMap.prod (plane R) q)), σ ((1, 0), 0) = i ∧ σ ((0, 1), 0) = j

Dias II.6.2. Over an LG ring, if q is non-singular on a finitely generated projective module, then every hyperbolic pair of plane ⊥ q is the image of the standard hyperbolic pair under a self-isometry. No hypothesis on the support of M.

Where M ⊗ κ(𝔪) vanishes the plane is everything, and there the pair (u, v) reaches the pair (β • v, β⁻¹ • u) only through the switch — not a product of transvections and dilations. The partial switch switchIdem supplies exactly that, on exactly that locus: with ε₀ = Module.rankIdempotent R M 0 and i = ((α, β), m), j = ((γ, δ), n), the element

ε := ε₀ * (β * γ)

is idempotent, because ε₀ annihilates M and hence kills q m, q n and q(m, n), leaving α β = 0, γ δ = 0, α δ + β γ = 1 — the relations that make β γ idempotent on the vanishing locus. Applying switchIdem ε first turns the u-coefficient into ε β + (1 - ε) α, which is a unit at every maximal ideal where M dies: there either β γ or α δ is 1. That is the hypothesis exists_isometryEquiv_of_isHyperbolicPair_of_notMem needs.

theorem QuadraticForm.isometryEquiv_of_isometryEquiv_plane_prod_of_isLGRing {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (hLG : IsLGRing R) {M₁ : Type v₁} [AddCommGroup M₁] [Module R M₁] [Module.Finite R M] [Module.Projective R M] {q₁ : QuadraticForm R M₁} {q₂ : QuadraticForm R M} (hq₂ : q₂.IsGPRNonsingular) (h : Nonempty ((QuadraticMap.prod (plane R) q₁).IsometryEquiv (QuadraticMap.prod (plane R) q₂))) : Nonempty (QuadraticMap.IsometryEquiv q₁ q₂)

Cancellation of a hyperbolic plane over an LG ring. For q₂ non-singular on a finitely generated projective module, plane ⊥ q₁ ≅ plane ⊥ q₂ implies q₁ ≅ q₂.

This is Dias II.6.4 for one plane: Dias II.6.2 supplies the transitivity that QuadraticForm.isometryEquiv_of_isometryEquiv_plane_prod consumes. Note q₁ carries no hypotheses at all, and q₂ only non-singularity — in particular M may vanish, or vanish on part of Spec R.