A hyperbolic pair splits off a hyperbolic plane

If (u, v) is a hyperbolic pair of (M, q) — q u = q v = 0 and q(u, v) = 1 — then the submodule R u ⊕ R v they span is free of rank two, the restriction of q to it is the hyperbolic plane (a, b) ↦ ab, and that restriction is regular. So the plane splits off orthogonally:

q ≅ ⟨plane⟩ ⊥ q|_{(Ru ⊕ Rv)ᗮ}.

Nothing here needs M finitely generated or projective, q regular, or 2 invertible. The regularity that the orthogonal splitting of QuadraticForm/OrthogonalComplement.lean consumes is regularity of the restricted form, and that is supplied by the pair itself: the plane is hyperbolic, and hyperbolic forms on finitely generated projective — here free of rank two — modules are regular.

This is the missing half of GPR 11.17: QuadraticForm/Isotropic.lean turns an isotropic vector into a hyperbolic pair (isGPRIsotropic_iff_exists_isHyperbolicPair), and this file turns the pair into a splitting.

Main definitions

• QuadraticMap.IsHyperbolicPair.planeEmbedding : the map (a, b) ↦ a u + b v.
• QuadraticMap.IsHyperbolicPair.planeSubmodule : its range, R u ⊕ R v.

Main results

• QuadraticMap.IsHyperbolicPair.isGPRRegular_comp_planeSubmodule_subtype : the restriction of q to R u ⊕ R v is regular.
• QuadraticMap.IsHyperbolicPair.isometryEquivPlaneProd : q ≅ plane ⊥ q|_{(Ru ⊕ Rv)ᗮ}.
• QuadraticForm.isGPRRegular_plane : the hyperbolic plane is regular over any commutative ring.

Implementation notes

The embedding is injective because the pair recovers coordinates: q(a u + b v, v) = a and q(a u + b v, u) = b, using q(u, u) = 2 q u = 0 and q(v, v) = 0. This is why no hypothesis on M is needed — the splitting is entirely local to the plane.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.11, 11.17.
• R. Baeza, Quadratic Forms over Semilocal Rings, Lecture Notes in Math. 655, Springer 1978, I, (3.3).

theorem QuadraticForm.isGPRRegular_plane (R : Type u) [CommRing R] : (plane R).IsGPRRegular

The hyperbolic plane is regular over any commutative ring: (a, b) ↦ ab is the pairing of R against R, so QuadraticForm.isGPRRegular_of_basis_pairing applies to the one-element basis of R. No hypothesis on 2.

theorem QuadraticForm.isGPRNonsingular_plane (R : Type u) [CommRing R] : (plane R).IsGPRNonsingular

The hyperbolic plane is non-singular.

def QuadraticMap.IsHyperbolicPair.planeEmbedding {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (u v : M) : R × R →ₗ[R] M

The map R × R → M, (a, b) ↦ a u + b v, whose image is the plane spanned by a hyperbolic pair. Defined for any two vectors; it is the hypothesis IsHyperbolicPair that makes it injective and an isometry from QuadraticForm.plane.

Equations

• QuadraticMap.IsHyperbolicPair.planeEmbedding u v = LinearMap.toSpanSingleton R M u ∘ₗ LinearMap.fst R R R + LinearMap.toSpanSingleton R M v ∘ₗ LinearMap.snd R R R

@[simp]

theorem QuadraticMap.IsHyperbolicPair.planeEmbedding_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {u v : M} (x : R × R) : (planeEmbedding u v) x = x.1 • u + x.2 • v

theorem QuadraticMap.IsHyperbolicPair.apply_planeEmbedding {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : IsHyperbolicPair Q u v) (x : R × R) : Q ((planeEmbedding u v) x) = (QuadraticForm.plane R) x

The embedding carries the hyperbolic plane to Q.

theorem QuadraticMap.IsHyperbolicPair.polar_planeEmbedding_right {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : IsHyperbolicPair Q u v) (x : R × R) : polar (⇑Q) ((planeEmbedding u v) x) v = x.1

Pairing a u + b v with v recovers a.

theorem QuadraticMap.IsHyperbolicPair.polar_planeEmbedding_left {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : IsHyperbolicPair Q u v) (x : R × R) : polar (⇑Q) ((planeEmbedding u v) x) u = x.2

Pairing a u + b v with u recovers b.

theorem QuadraticMap.IsHyperbolicPair.injective_planeEmbedding {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : IsHyperbolicPair Q u v) : Function.Injective ⇑(planeEmbedding u v)

def QuadraticMap.IsHyperbolicPair.planeSubmodule {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (u v : M) : Submodule R M

The submodule R u ⊕ R v spanned by a hyperbolic pair, presented as the range of QuadraticMap.IsHyperbolicPair.planeEmbedding.

Equations

• QuadraticMap.IsHyperbolicPair.planeSubmodule u v = (QuadraticMap.IsHyperbolicPair.planeEmbedding u v).range

noncomputable def QuadraticMap.IsHyperbolicPair.planeEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : IsHyperbolicPair Q u v) : (R × R) ≃ₗ[R] ↥(planeSubmodule u v)

The plane of a hyperbolic pair, as a module, is R × R.

Equations

• h.planeEquiv = LinearEquiv.ofInjective (QuadraticMap.IsHyperbolicPair.planeEmbedding u v) ⋯

@[simp]

theorem QuadraticMap.IsHyperbolicPair.planeEquiv_coe {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : IsHyperbolicPair Q u v) (x : R × R) : ↑(h.planeEquiv x) = x.1 • u + x.2 • v

theorem QuadraticMap.IsHyperbolicPair.comp_planeEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : IsHyperbolicPair Q u v) : (comp Q (planeSubmodule u v).subtype).comp ↑h.planeEquiv = QuadraticForm.plane R

The restriction of Q to the plane of a hyperbolic pair is the hyperbolic plane, read through QuadraticMap.IsHyperbolicPair.planeEquiv.

noncomputable def QuadraticMap.IsHyperbolicPair.planeIsometryEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : IsHyperbolicPair Q u v) : IsometryEquiv (QuadraticForm.plane R) (comp Q (planeSubmodule u v).subtype)

The hyperbolic plane, as a quadratic module, is the plane of the pair inside (M, Q).

Equations

• h.planeIsometryEquiv = { toLinearEquiv := h.planeEquiv, map_app' := ⋯ }

theorem QuadraticMap.IsHyperbolicPair.isGPRRegular_comp_planeSubmodule_subtype {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : IsHyperbolicPair Q u v) : QuadraticForm.IsGPRRegular (comp Q (planeSubmodule u v).subtype)

The restriction of Q to the plane of a hyperbolic pair is regular. This is what lets the plane split off orthogonally, and it holds over any commutative ring with no hypothesis on 2.

noncomputable def QuadraticMap.IsHyperbolicPair.isometryEquivPlaneProd {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : IsHyperbolicPair Q u v) : (prod (QuadraticForm.plane R) (comp Q (Q.polarOrthogonal (planeSubmodule u v)).subtype)).IsometryEquiv Q

A hyperbolic pair splits off a hyperbolic plane: Q ≅ plane ⊥ Q|_{(Ru ⊕ Rv)ᗮ}.

The orthogonal complement is taken for the polar form of Q (QuadraticForm.polarOrthogonal).

Equations

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