Witt cancellation

Over a field in which 2 is invertible, a regular summand may be cancelled from an orthogonal sum: if q ⊥ q₁ and q ⊥ q₂ are isometric and q is regular and finite dimensional, then q₁ and q₂ are isometric. This is Witt's cancellation theorem, and it is what makes the isometry classes of regular forms cancellative under orthogonal sum, hence a monoid that embeds into its Grothendieck group.

The file also provides cancellation interfaces for a summand fixed pointwise and for a form on a space spanned by one vector of nonzero value. The proof of the general theorem follows Lam I.4.5–I.4.7.

Main definitions

• TauCeti.prodCancelIsometryEquiv: the isometry obtained by cancelling a regular summand that an isometry of orthogonal sums fixes pointwise.

Main results

• TauCeti.equivalent_of_equivalent_prod_of_span_singleton_eq_top: cancellation of a summand carried by a line spanned by a vector of nonzero value.
• TauCeti.equivalent_of_equivalent_prod: Witt cancellation for a regular finite-dimensional summand, and TauCeti.equivalent_of_equivalent_prod_right on the other side.
• TauCeti.RegularFormClass is cancellative under orthogonal sum.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter I, §4.

Cancelling a summand that is fixed pointwise

theorem TauCeti.isometryEquiv_prod_fst_eq_zero {R : Type u} [CommRing R] [Invertible 2] {P : Type v} [AddCommGroup P] [Module R P] {V₀ : Type v₀} [AddCommGroup V₀] [Module R V₀] {V₁ : Type v₁} [AddCommGroup V₁] [Module R V₁] {V₂ : Type v₂} [AddCommGroup V₂] [Module R V₂] {Q₀ : QuadraticMap R V₀ P} {Q₁ : QuadraticMap R V₁ P} {Q₂ : QuadraticMap R V₂ P} (hQ₀ : QuadraticMap.Nondegenerate) (e : (Q₀.prod Q₁).IsometryEquiv (Q₀.prod Q₂)) (he : ∀ (u : V₀), e (u, 0) = (u, 0)) (v : V₁) : (e (0, v)).1 = 0

If an isometry of orthogonal sums fixes a regular first summand pointwise, the first component of the image of every vector in the second summand is zero.

def TauCeti.prodCancelIsometryEquiv {R : Type u} [CommRing R] [Invertible 2] {P : Type v} [AddCommGroup P] [Module R P] {V₀ : Type v₀} [AddCommGroup V₀] [Module R V₀] {V₁ : Type v₁} [AddCommGroup V₁] [Module R V₁] {V₂ : Type v₂} [AddCommGroup V₂] [Module R V₂] {Q₀ : QuadraticMap R V₀ P} {Q₁ : QuadraticMap R V₁ P} {Q₂ : QuadraticMap R V₂ P} (hQ₀ : QuadraticMap.Nondegenerate) (e : (Q₀.prod Q₁).IsometryEquiv (Q₀.prod Q₂)) (he : ∀ (u : V₀), e (u, 0) = (u, 0)) : Q₁.IsometryEquiv Q₂

Cancel the first summand of an orthogonal sum along an isometry that fixes it pointwise: the second component of e (0, ·) is an isometry of the second summands.

@[simp]

theorem TauCeti.prodCancelIsometryEquiv_apply {R : Type u} [CommRing R] [Invertible 2] {P : Type v} [AddCommGroup P] [Module R P] {V₀ : Type v₀} [AddCommGroup V₀] [Module R V₀] {V₁ : Type v₁} [AddCommGroup V₁] [Module R V₁] {V₂ : Type v₂} [AddCommGroup V₂] [Module R V₂] {Q₀ : QuadraticMap R V₀ P} {Q₁ : QuadraticMap R V₁ P} {Q₂ : QuadraticMap R V₂ P} (hQ₀ : QuadraticMap.Nondegenerate) (e : (Q₀.prod Q₁).IsometryEquiv (Q₀.prod Q₂)) (he : ∀ (u : V₀), e (u, 0) = (u, 0)) (v : V₁) : (prodCancelIsometryEquiv hQ₀ e he) v = (e (0, v)).2

@[simp]

theorem TauCeti.prodCancelIsometryEquiv_symm_apply {R : Type u} [CommRing R] [Invertible 2] {P : Type v} [AddCommGroup P] [Module R P] {V₀ : Type v₀} [AddCommGroup V₀] [Module R V₀] {V₁ : Type v₁} [AddCommGroup V₁] [Module R V₁] {V₂ : Type v₂} [AddCommGroup V₂] [Module R V₂] {Q₀ : QuadraticMap R V₀ P} {Q₁ : QuadraticMap R V₁ P} {Q₂ : QuadraticMap R V₂ P} (hQ₀ : QuadraticMap.Nondegenerate) (e : (Q₀.prod Q₁).IsometryEquiv (Q₀.prod Q₂)) (he : ∀ (u : V₀), e (u, 0) = (u, 0)) (w : V₂) : (prodCancelIsometryEquiv hQ₀ e he).symm w = (e.symm (0, w)).2

The inverse cancellation isometry is the second component of e.symm on the second summand.

Cancelling a line

theorem TauCeti.equivalent_of_equivalent_prod_of_span_singleton_eq_top {K : Type u} [Field K] [Invertible 2] {V₀ : Type v₀} [AddCommGroup V₀] [Module K V₀] {V₁ : Type v₁} [AddCommGroup V₁] [Module K V₁] {V₂ : Type v₂} [AddCommGroup V₂] [Module K V₂] {Q₀ : QuadraticForm K V₀} {v₀ : V₀} (hspan : K ∙ v₀ = ⊤) (hv₀ : Q₀ v₀ ≠ 0) {Q₁ : QuadraticForm K V₁} {Q₂ : QuadraticForm K V₂} (h : (QuadraticMap.prod Q₀ Q₁).Equivalent (QuadraticMap.prod Q₀ Q₂)) : QuadraticMap.Equivalent Q₁ Q₂

Witt cancellation for a summand carried by a line: a form on a space spanned by a single vector of nonzero value cancels from an orthogonal sum.

Witt cancellation

theorem TauCeti.equivalent_of_equivalent_prod {K : Type u} [Field K] [Invertible 2] {V₀ : Type v₀} [AddCommGroup V₀] [Module K V₀] {V₁ : Type v₁} [AddCommGroup V₁] [Module K V₁] {V₂ : Type v₂} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V₀] {Q₀ : QuadraticForm K V₀} (hQ₀ : QuadraticMap.Nondegenerate) {Q₁ : QuadraticForm K V₁} {Q₂ : QuadraticForm K V₂} (h : (QuadraticMap.prod Q₀ Q₁).Equivalent (QuadraticMap.prod Q₀ Q₂)) : QuadraticMap.Equivalent Q₁ Q₂

Witt cancellation (Lam I.4.2): a regular finite-dimensional summand cancels from an orthogonal sum.

theorem TauCeti.equivalent_of_equivalent_prod_right {K : Type u} [Field K] [Invertible 2] {V₀ : Type v₀} [AddCommGroup V₀] [Module K V₀] {V₁ : Type v₁} [AddCommGroup V₁] [Module K V₁] {V₂ : Type v₂} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V₀] {Q₀ : QuadraticForm K V₀} (hQ₀ : QuadraticMap.Nondegenerate) {Q₁ : QuadraticForm K V₁} {Q₂ : QuadraticForm K V₂} (h : (QuadraticMap.prod Q₁ Q₀).Equivalent (QuadraticMap.prod Q₂ Q₀)) : QuadraticMap.Equivalent Q₁ Q₂

Witt cancellation, cancelling the summand on the right.

instance TauCeti.instIsCancelAddRegularFormClass {K : Type u} [Field K] [Invertible 2] : IsCancelAdd (RegularFormClass K)

Orthogonal sum is cancellative on the isometry classes of regular forms: this is Witt cancellation read on TauCeti.RegularFormClass, and it is what makes the canonical map from the monoid of isometry classes into the Witt-Grothendieck ring injective.