Witt cancellation over LG rings (GN 6.5, GPR 11.27)

The capstone of Layer 0. QuadraticForm/PlaneTransitivity.lean cancels one hyperbolic plane; this file passes from there to QuadraticForm.dualProd R N for an arbitrary finitely generated projective N, and then to GN 6.5 by way of the reduction in QuadraticForm/Cancellation.lean.

The route

1. dualProd R (Fin 0 → R) is the form on a trivial module, so it can simply be dropped (QuadraticMap.IsometryEquiv.prodOfSubsingletonLeft).
2. dualProd R R ≅ plane R (QuadraticForm.isometryEquivPlane) and dualProd R (M × N) ≅ dualProd R M ⊥ dualProd R N (mathlib's QuadraticForm.dualProdProdIsometry). Together with Fin (n+1) → R ≃ₗ R × (Fin n → R) these turn dualProd R (Fin n → R) into n planes, so n applications of QuadraticForm.isometryEquiv_of_isometryEquiv_plane_prod_of_isLGRing cancel it — QuadraticForm.cancel_dualProd_fin.
3. A finitely generated projective N is a direct summand of some Rⁿ (QuadraticForm.exists_linearEquiv_prod_submodule). Adding dualProd R N' for a complement N' to both sides of dualProd R N ⊥ q₁ ≅ dualProd R N ⊥ q₂ turns it into the free case — QuadraticForm.cancel_dualProd. Note N' needs no hypotheses whatever: it is only ever fed to dualProd, which is defined for every module.
4. QuadraticForm.cancel is GN 6.5, obtained from cancel_dualProd and QuadraticForm.isometryEquiv_prod_dualProd_of_isometryEquiv_prod.

Note where the hypotheses are consumed. Non-singularity is asked of q₂ only, since the plane cancellation of step 2 needs the second summand non-singular at each stage; GN 6.5 also lists q₁, which is redundant (it follows from the others — see QuadraticForm/Cancellation.lean). Regularity — as opposed to non-singularity — is used exactly once, on q₃, in the reduction of step 4, and GN's counterexample (see QuadraticForm/Cancellation.lean) shows it cannot be dropped there.

References

• [GN] Gille, Neher, Group schemes over LG-rings and applications to cancellation theorems and Azumaya algebras, European Journal of Mathematics 11 (2025), article 42, 6.5.
• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.27.
• I. Dias, Formas Quadráticas Sobre LG-Anéis, Ph.D. thesis, Universidade Estadual de Campinas, 1988, II.6.4.

noncomputable def QuadraticMap.IsometryEquiv.prodOfSubsingletonLeft {R : Type u} [CommRing R] {M₁ : Type v₁} [AddCommGroup M₁] [Module R M₁] {M₂ : Type v₂} [AddCommGroup M₂] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) [Subsingleton M₁] : (QuadraticMap.prod Q₁ Q₂).IsometryEquiv Q₂

A summand on a trivial module can be dropped from an orthogonal sum.

Equations

• QuadraticMap.IsometryEquiv.prodOfSubsingletonLeft Q₁ Q₂ = { toLinearEquiv := LinearEquiv.ofBijective (LinearMap.snd R M₁ M₂) ⋯, map_app' := ⋯ }

The hyperbolic form of Rⁿ

noncomputable def QuadraticForm.isometryEquivPlane {R : Type u} [CommRing R] : QuadraticMap.IsometryEquiv (dualProd R R) (plane R)

dualProd R R is the hyperbolic plane. Evaluation at 1 identifies R* with R.

Equations

• QuadraticForm.isometryEquivPlane = { toLinearEquiv := (LinearMap.ringLmapEquivSelf R R R).prodCongr (LinearEquiv.refl R R), map_app' := ⋯ }

noncomputable def QuadraticForm.isometryEquivDualProdFinSucc (R : Type u) [CommRing R] (k : ℕ) : QuadraticMap.IsometryEquiv (dualProd R (Fin (k + 1) → R)) (QuadraticMap.prod (plane R) (dualProd R (Fin k → R)))

Splitting off the first coordinate: dualProd R (Rⁿ⁺¹) ≅ plane ⊥ dualProd R (Rⁿ).

Equations

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

Cancelling a hyperbolic form

theorem QuadraticForm.cancel_dualProd_fin {R : Type u} [CommRing R] {M₁ : Type v₁} [AddCommGroup M₁] [Module R M₁] {M₂ : Type v₂} [AddCommGroup M₂] [Module R M₂] (hLG : IsLGRing R) [Module.Finite R M₂] [Module.Projective R M₂] {q₁ : QuadraticForm R M₁} {q₂ : QuadraticForm R M₂} (h₂ : q₂.IsGPRNonsingular) (n : ℕ) (h : Nonempty ((QuadraticMap.prod (dualProd R (Fin n → R)) q₁).IsometryEquiv (QuadraticMap.prod (dualProd R (Fin n → R)) q₂))) : Nonempty (QuadraticMap.IsometryEquiv q₁ q₂)

Cancellation of dualProd R (Rⁿ) over an LG ring, by induction on n: strip off one plane at a time with isometryEquiv_of_isometryEquiv_plane_prod_of_isLGRing.

At the k-th stage the form being cancelled against is dualProd R (Rᵏ) ⊥ q₂, non-singular by GN (C.8.3) since the hyperbolic summand is regular; that is why the hyperbolic form is kept on the left. Nothing is assumed about q₁.

theorem QuadraticForm.exists_linearEquiv_prod_submodule {R : Type u} [CommRing R] (N : Type v₁) [AddCommGroup N] [Module R N] [Module.Finite R N] [Module.Projective R N] : ∃ (n : ℕ) (N' : Submodule R (Fin n → R)), Nonempty ((N × ↥N') ≃ₗ[R] Fin n → R)

A finitely generated projective module is a direct summand of Rⁿ. The complement is produced as a submodule of Rⁿ, so that no auxiliary type has to be introduced.

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

Cancellation of a hyperbolic form over an LG ring. For N finitely generated projective and q₂ non-singular, dualProd R N ⊥ q₁ ≅ dualProd R N ⊥ q₂ implies q₁ ≅ q₂.

Choose a complement N' with N × N' ≅ Rⁿ and add dualProd R N' to both sides: since dualProd R (N × N') ≅ dualProd R N ⊥ dualProd R N', this turns the hypothesis into one about dualProd R (Rⁿ), which cancel_dualProd_fin handles. N' carries no hypotheses — it is only ever fed to dualProd, which every module has.

theorem QuadraticForm.cancel {R : Type u} [CommRing R] {M₁ : Type v₁} [AddCommGroup M₁] [Module R M₁] {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₃] [Module.Finite R M₂] [Module.Projective R M₂] {q₁ : QuadraticForm R M₁} {q₂ : QuadraticForm R M₂} {q₃ : QuadraticForm R M₃} (h₂ : q₂.IsGPRNonsingular) (h₃ : q₃.IsGPRRegular) (h : Nonempty ((QuadraticMap.prod q₁ q₃).IsometryEquiv (QuadraticMap.prod q₂ q₃))) : Nonempty (QuadraticMap.IsometryEquiv q₁ q₂)

Witt cancellation over an LG ring (GN 6.5; cf. GPR 11.27). If q₃ is regular and q₂ is non-singular, then q₁ ⊥ q₃ ≅ q₂ ⊥ q₃ implies q₁ ≅ q₂.

Adding -q₃ turns q₃ into a hyperbolic form (QuadraticForm.isometryEquiv_prod_dualProd_of_isometryEquiv_prod), which cancel_dualProd cancels. Regularity of q₃ is consumed in that first step and nowhere else; it cannot be weakened to non-singularity (EKM, p. 49 — see QuadraticForm/Cancellation.lean).

GN also lists q₁ non-singular. It is not carried here because it is implied: q₂ ⊥ q₃ is non-singular, hence so is q₁ ⊥ q₃, hence so is q₁ (QuadraticForm.IsGPRNonsingular.of_prod_left).