Cancelling a hyperbolic plane

The step of Witt cancellation that turns a statement about isometries of a hyperbolic pair into a statement about cancellation: if every hyperbolic pair of H ⊥ q₂ is the image of the standard one under a self-isometry, then H ⊥ q₁ ≅ H ⊥ q₂ implies q₁ ≅ q₂.

This is the second half of Dias II.6.4 (Baeza III (4.3)), specialized to a hyperbolic plane and written with mathlib's QuadraticMap.prod in place of an internal orthogonal decomposition. The transitivity hypothesis it consumes is Dias II.6.2, whose general case is what needs the LG axiom; its unit case is QuadraticMap.IsHyperbolicPair.exists_isometryEquiv_of_isUnit.

Main results

• QuadraticForm.isHyperbolicPair_plane_prod : ((1,0), 0) and ((0,1), 0) form the standard hyperbolic pair of plane ⊥ q.
• QuadraticForm.isometryEquivOfFixesPlane : an isometry plane ⊥ q₁ ≅ plane ⊥ q₂ fixing both members of the standard hyperbolic pair restricts to an isometry q₁ ≅ q₂. The mechanism is that a vector is in the second summand exactly when it is orthogonal to the pair, which is a two-line computation for the plane and needs no regularity of q₁ or q₂.
• QuadraticForm.isometryEquiv_of_isometryEquiv_plane_prod : cancellation of a plane, given transitivity on hyperbolic pairs.

References

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

theorem QuadraticForm.isHyperbolicPair_plane_prod {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (Q : QuadraticForm R M₁) : (QuadraticMap.prod (plane R) Q).IsHyperbolicPair ((1, 0), 0) ((0, 1), 0)

The standard hyperbolic pair of plane ⊥ q.

theorem QuadraticForm.fst_eq_zero_of_polar_eq_zero {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {Q : QuadraticForm R M₁} {x : (R × R) × M₁} (h₁ : QuadraticMap.polar (⇑(QuadraticMap.prod (plane R) Q)) x ((1, 0), 0) = 0) (h₂ : QuadraticMap.polar (⇑(QuadraticMap.prod (plane R) Q)) x ((0, 1), 0) = 0) : x.1 = 0

A vector of plane ⊥ q orthogonal to both members of the standard hyperbolic pair lies in the second summand. This is the whole content of "the orthogonal complement of the plane is q", and it needs nothing of q.

theorem QuadraticForm.fst_map_inr_eq_zero {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (τ : (QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂)) (hu : τ ((1, 0), 0) = ((1, 0), 0)) (hv : τ ((0, 1), 0) = ((0, 1), 0)) (m : M₁) : (τ (0, m)).1 = 0

An isometry fixing the standard hyperbolic pair maps the second summand into the second summand.

def QuadraticForm.restrictPlane {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (τ : (QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂)) : M₁ →ₗ[R] M₂

The restriction of τ to the second summand, as a linear map.

Equations

• QuadraticForm.restrictPlane τ = LinearMap.snd R (R × R) M₂ ∘ₗ ↑τ.toLinearEquiv ∘ₗ LinearMap.inr R (R × R) M₁

@[simp]

theorem QuadraticForm.restrictPlane_apply {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (τ : (QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂)) (m : M₁) : (restrictPlane τ) m = (τ (0, m)).2

theorem QuadraticForm.map_inr {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (τ : (QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂)) (hu : τ ((1, 0), 0) = ((1, 0), 0)) (hv : τ ((0, 1), 0) = ((0, 1), 0)) (m : M₁) : τ (0, m) = (0, (restrictPlane τ) m)

theorem QuadraticForm.apply_restrictPlane {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (τ : (QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂)) (hu : τ ((1, 0), 0) = ((1, 0), 0)) (hv : τ ((0, 1), 0) = ((0, 1), 0)) (m : M₁) : Q₂ ((restrictPlane τ) m) = Q₁ m

theorem QuadraticForm.symm_fixes_left {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (τ : (QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂)) (hu : τ ((1, 0), 0) = ((1, 0), 0)) : τ.symm ((1, 0), 0) = ((1, 0), 0)

theorem QuadraticForm.symm_fixes_right {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (τ : (QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂)) (hv : τ ((0, 1), 0) = ((0, 1), 0)) : τ.symm ((0, 1), 0) = ((0, 1), 0)

theorem QuadraticForm.restrictPlane_symm_restrictPlane {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (τ : (QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂)) (hu : τ ((1, 0), 0) = ((1, 0), 0)) (hv : τ ((0, 1), 0) = ((0, 1), 0)) (m : M₁) : (restrictPlane τ.symm) ((restrictPlane τ) m) = m

theorem QuadraticForm.restrictPlane_restrictPlane_symm {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (τ : (QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂)) (hu : τ ((1, 0), 0) = ((1, 0), 0)) (hv : τ ((0, 1), 0) = ((0, 1), 0)) (n : M₂) : (restrictPlane τ) ((restrictPlane τ.symm) n) = n

noncomputable def QuadraticForm.isometryEquivOfFixesPlane {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (τ : (QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂)) (hu : τ ((1, 0), 0) = ((1, 0), 0)) (hv : τ ((0, 1), 0) = ((0, 1), 0)) : QuadraticMap.IsometryEquiv Q₁ Q₂

An isometry plane ⊥ q₁ ≅ plane ⊥ q₂ fixing the standard hyperbolic pair cancels the plane.

Equations

• QuadraticForm.isometryEquivOfFixesPlane τ hu hv = { toLinearEquiv := LinearEquiv.ofBijective (QuadraticForm.restrictPlane τ) ⋯, map_app' := ⋯ }

theorem QuadraticForm.isometryEquiv_of_isometryEquiv_plane_prod {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (htrans : ∀ (i j : (R × R) × M₂), (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) (h : Nonempty ((QuadraticMap.prod (plane R) Q₁).IsometryEquiv (QuadraticMap.prod (plane R) Q₂))) : Nonempty (QuadraticMap.IsometryEquiv Q₁ Q₂)

Cancellation of a hyperbolic plane, given transitivity on hyperbolic pairs.

The hypothesis is Dias II.6.2 for plane ⊥ q₂: every hyperbolic pair is the image of the standard one under a self-isometry. Given it, plane ⊥ q₁ ≅ plane ⊥ q₂ implies q₁ ≅ q₂, by correcting the given isometry so that it fixes the standard pair and then restricting (QuadraticForm.isometryEquivOfFixesPlane).