Chains of elementary equivalences between diagonal quadratic forms

This file defines the elementary steps in the chain theorem for diagonal quadratic forms. A permutation step reorders the coefficients, while a binary step replaces two coefficients by an equivalent binary form and leaves all other coefficients fixed. A diagonal chain is the reflexive transitive closure of these two kinds of steps.

Permutation steps introduce no additional generators: every permutation is a chain of binary steps, since a transposition of coefficients is itself a binary equivalence. The main result here is the forward implication of the chain theorem: a diagonal chain induces an isometry between its endpoint diagonal forms. The converse is the substantive Witt chain theorem.

The bodies of the four relations below are not exposed, so their constructors are unavailable outside this file. Downstream modules build steps through TauCeti.BinaryStep.of_pair and TauCeti.DiagonalStep.binary/permutation, and chains through TauCeti.DiagonalChain.refl/binary/permutation/tail/trans instead. They take steps apart through TauCeti.PermutationStep.exists_perm and TauCeti.BinaryStep.exists_pair.

The declarations in this file assume only a commutative semiring and establish the elementary forward implication. The classical converse cited below is a theorem over fields with 2 invertible.

Main definitions

• TauCeti.PermutationStep: one permutation of a coefficient family.
• TauCeti.BinaryStep: one equivalent replacement of two coefficients.
• TauCeti.DiagonalStep: either kind of elementary step.
• TauCeti.DiagonalChain: a finite chain of elementary steps.

Main results

• TauCeti.PermutationStep.to_reflTransGen_binaryStep: every permutation step is generated by binary steps.
• TauCeti.DiagonalChain.equivalent: the endpoint diagonal forms of a chain are isometric.
• TauCeti.DiagonalChain.cons: chains are stable under adjoining a fixed first coefficient.
• TauCeti.diagonalChain_iff_equivalent_fin_zero: the chain theorem in rank zero.
• TauCeti.diagonalChain_fin_one_iff_eq: in rank one, a chain is exactly equality of coefficient families. Isometry can be strictly weaker there, so the unrestricted converse of TauCeti.DiagonalChain.equivalent fails in general.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Graduate Studies in Mathematics 67, American Mathematical Society (2005), Chapter I, Theorem 5.2.

def TauCeti.PermutationStep {R : Type u} [CommSemiring R] {n : ℕ} (w w' : Fin n → Rˣ) : Prop

A permutation step reorders the unit coefficients of a diagonal quadratic form.

def TauCeti.BinaryStep {R : Type u} [CommSemiring R] {n : ℕ} (w w' : Fin n → Rˣ) : Prop

A binary step replaces two distinct unit coefficients by an equivalent binary form and fixes all other coefficients.

def TauCeti.DiagonalStep {R : Type u} [CommSemiring R] {n : ℕ} (w w' : Fin n → Rˣ) : Prop

An elementary step between diagonal coefficient families is either a permutation step or a binary step.

def TauCeti.DiagonalChain {R : Type u} [CommSemiring R] {n : ℕ} (w w' : Fin n → Rˣ) : Prop

A diagonal chain is a finite sequence of permutation or binary steps.

theorem TauCeti.BinaryStep.of_pair {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (i j : Fin n) (hij : i ≠ j) (hrest : ∀ (k : Fin n), k ≠ i → k ≠ j → w k = w' k) (hpair : (QuadraticMap.weightedSumSquares R ![↑(w i), ↑(w j)]).Equivalent (QuadraticMap.weightedSumSquares R ![↑(w' i), ↑(w' j)])) : BinaryStep w w'

Construct a binary step from the changed pair, equality away from that pair, and an equivalence of the corresponding binary forms.

theorem TauCeti.BinaryStep.exists_pair {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : BinaryStep w w') : ∃ (i : Fin n) (j : Fin n), i ≠ j ∧ (∀ (k : Fin n), k ≠ i → k ≠ j → w k = w' k) ∧ (QuadraticMap.weightedSumSquares R ![↑(w i), ↑(w j)]).Equivalent (QuadraticMap.weightedSumSquares R ![↑(w' i), ↑(w' j)])

Eliminate a binary step into the changed pair, equality away from that pair, and an equivalence of the corresponding binary forms. This is the converse of BinaryStep.of_pair.

theorem TauCeti.BinaryStep.swap {R : Type u} [CommSemiring R] {n : ℕ} (w : Fin n → Rˣ) {i j : Fin n} (hij : i ≠ j) : BinaryStep w (w ∘ ⇑(Equiv.swap i j))

Swapping two distinct coefficients is a binary step.

theorem TauCeti.PermutationStep.exists_perm {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : PermutationStep w w') : ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin n), w' i = w (σ i)

Eliminate a permutation step into the permutation that reorders the coefficients.

theorem TauCeti.PermutationStep.symm {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : PermutationStep w w') : PermutationStep w' w

Permutation steps may be reversed.

theorem TauCeti.PermutationStep.to_reflTransGen_binaryStep {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : PermutationStep w w') : Relation.ReflTransGen BinaryStep w w'

Every permutation step is a reflexive-transitive chain of binary steps. Thus coefficient permutations introduce no generators beyond binary equivalence.

theorem TauCeti.PermutationStep.equivalent {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : PermutationStep w w') : (QuadraticMap.weightedSumSquares R fun (i : Fin n) => ↑(w i)).Equivalent (QuadraticMap.weightedSumSquares R fun (i : Fin n) => ↑(w' i))

The diagonal forms at the endpoints of a permutation step are equivalent.

theorem TauCeti.BinaryStep.symm {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : BinaryStep w w') : BinaryStep w' w

Binary steps may be reversed.

theorem TauCeti.BinaryStep.equivalent {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : BinaryStep w w') : (QuadraticMap.weightedSumSquares R fun (i : Fin n) => ↑(w i)).Equivalent (QuadraticMap.weightedSumSquares R fun (i : Fin n) => ↑(w' i))

The diagonal forms at the endpoints of a binary step are equivalent.

theorem TauCeti.BinaryStep.cons {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (a : Rˣ) (h : BinaryStep w w') : BinaryStep (Fin.cons a w) (Fin.cons a w')

A binary step remains a binary step after adjoining a fixed first coefficient.

theorem TauCeti.DiagonalStep.binary {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : BinaryStep w w') : DiagonalStep w w'

A binary step is an elementary diagonal step.

theorem TauCeti.DiagonalStep.permutation {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : PermutationStep w w') : DiagonalStep w w'

A permutation step is an elementary diagonal step.

theorem TauCeti.DiagonalStep.elim {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : DiagonalStep w w') {P : Prop} (hperm : PermutationStep w w' → P) (hbin : BinaryStep w w' → P) : P

Eliminate an elementary diagonal step by handling its permutation and binary cases.

theorem TauCeti.DiagonalStep.symm {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : DiagonalStep w w') : DiagonalStep w' w

Elementary diagonal steps may be reversed.

theorem TauCeti.DiagonalStep.equivalent {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : DiagonalStep w w') : (QuadraticMap.weightedSumSquares R fun (i : Fin n) => ↑(w i)).Equivalent (QuadraticMap.weightedSumSquares R fun (i : Fin n) => ↑(w' i))

The diagonal forms at the endpoints of an elementary diagonal step are equivalent.

theorem TauCeti.DiagonalChain.refl {R : Type u} [CommSemiring R] {n : ℕ} (w : Fin n → Rˣ) : DiagonalChain w w

Every coefficient family is connected to itself by a diagonal chain.

theorem TauCeti.DiagonalChain.binary {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : BinaryStep w w') : DiagonalChain w w'

A single binary step is a diagonal chain.

theorem TauCeti.DiagonalChain.permutation {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : PermutationStep w w') : DiagonalChain w w'

A permutation step is a diagonal chain, since it is generated by binary steps.

theorem TauCeti.DiagonalChain.tail {R : Type u} [CommSemiring R] {n : ℕ} {w w' w'' : Fin n → Rˣ} (h : DiagonalChain w w') (h' : DiagonalStep w' w'') : DiagonalChain w w''

Append an elementary step to a diagonal chain.

theorem TauCeti.DiagonalChain.trans {R : Type u} [CommSemiring R] {n : ℕ} {w w' w'' : Fin n → Rˣ} (h : DiagonalChain w w') (h' : DiagonalChain w' w'') : DiagonalChain w w''

Concatenate two diagonal chains.

theorem TauCeti.DiagonalChain.induction_on {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : DiagonalChain w w') {P : (Fin n → Rˣ) → Prop} (hw : P w) (hstep : ∀ {v v' : Fin n → Rˣ}, DiagonalStep v v' → P v → P v') : P w'

Induct over a diagonal chain from a property of its initial coefficient family, provided the property is preserved by each permutation or binary replacement.

theorem TauCeti.DiagonalChain.symm {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : DiagonalChain w w') : DiagonalChain w' w

Diagonal chains may be reversed.

theorem TauCeti.DiagonalChain.equivalent {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (h : DiagonalChain w w') : (QuadraticMap.weightedSumSquares R fun (i : Fin n) => ↑(w i)).Equivalent (QuadraticMap.weightedSumSquares R fun (i : Fin n) => ↑(w' i))

The diagonal forms at the endpoints of a diagonal chain are equivalent over a commutative semiring. This is the forward implication of Witt's chain theorem; its classical converse requires a field with 2 invertible.

theorem TauCeti.DiagonalChain.cons {R : Type u} [CommSemiring R] {n : ℕ} {w w' : Fin n → Rˣ} (a : Rˣ) (h : DiagonalChain w w') : DiagonalChain (Fin.cons a w) (Fin.cons a w')

A diagonal chain remains a diagonal chain after adjoining a fixed first coefficient.

@[simp]

theorem TauCeti.diagonalChain_iff_equivalent_fin_zero {R : Type u} [CommSemiring R] {w w' : Fin 0 → Rˣ} : DiagonalChain w w' ↔ (QuadraticMap.weightedSumSquares R fun (i : Fin 0) => ↑(w i)).Equivalent (QuadraticMap.weightedSumSquares R fun (i : Fin 0) => ↑(w' i))

In rank zero, the unique coefficient families are connected by a diagonal chain and their weighted sums of squares are isometric.

@[simp]

theorem TauCeti.diagonalChain_fin_one_iff_eq {R : Type u} [CommSemiring R] {w w' : Fin 1 → Rˣ} : DiagonalChain w w' ↔ w = w'

In rank one a diagonal chain is equality of coefficient families. Isometry can be strictly weaker than equality, since isometric one-dimensional forms need only have coefficients in the same square class; thus the unrestricted converse of TauCeti.DiagonalChain.equivalent fails in general.