Descending diagonal invariants to isometry classes

This file constructs functions on isometry classes of diagonal presentations from functions on their coefficient tuples. Invariance under permutation and binary replacement handles ranks at least two through Witt's chain theorem. In rank one, the coefficients of isometric forms can differ by a square, so descent also requires invariance under that relation.

The chain theorem follows Lam, Introduction to Quadratic Forms over Fields, Chapter I, Theorem 5.2.

def TauCeti.RegularFormClass.liftDiagonal {K : Type u} [Field K] [Invertible 2] {α : Type v} (f : RegularFormPresentation K → α) (hperm : ∀ {n : ℕ} {w w' : Fin n → Kˣ}, PermutationStep w w' → f ⟨n, w⟩ = f ⟨n, w'⟩) (hbin : ∀ {n : ℕ} {w w' : Fin n → Kˣ}, BinaryStep w w' → f ⟨n, w⟩ = f ⟨n, w'⟩) (hone : ∀ (a b : Kˣ), IsSquare (a * b) → f ⟨1, fun (x : Fin 1) => a⟩ = f ⟨1, fun (x : Fin 1) => b⟩) : RegularFormClass K → α

Lift a function on diagonal coefficient presentations to isometry classes when it is invariant under coefficient permutations and binary replacements. The rank-one condition records the necessary invariance under changing a coefficient by a square, since no binary replacement is available in that rank.

@[simp]

theorem TauCeti.RegularFormClass.liftDiagonal_mk {K : Type u} [Field K] [Invertible 2] {α : Type v} (f : RegularFormPresentation K → α) (hperm : ∀ {n : ℕ} {w w' : Fin n → Kˣ}, PermutationStep w w' → f ⟨n, w⟩ = f ⟨n, w'⟩) (hbin : ∀ {n : ℕ} {w w' : Fin n → Kˣ}, BinaryStep w w' → f ⟨n, w⟩ = f ⟨n, w'⟩) (hone : ∀ (a b : Kˣ), IsSquare (a * b) → f ⟨1, fun (x : Fin 1) => a⟩ = f ⟨1, fun (x : Fin 1) => b⟩) (p : RegularFormPresentation K) : liftDiagonal f ⋯ ⋯ hone ⟦p⟧ = f p

The lifted invariant agrees with its defining function on every diagonal presentation.

theorem TauCeti.RegularFormClass.liftDiagonal_unique {K : Type u} [Field K] [Invertible 2] {α : Type v} (f : RegularFormPresentation K → α) (hperm : ∀ {n : ℕ} {w w' : Fin n → Kˣ}, PermutationStep w w' → f ⟨n, w⟩ = f ⟨n, w'⟩) (hbin : ∀ {n : ℕ} {w w' : Fin n → Kˣ}, BinaryStep w w' → f ⟨n, w⟩ = f ⟨n, w'⟩) (hone : ∀ (a b : Kˣ), IsSquare (a * b) → f ⟨1, fun (x : Fin 1) => a⟩ = f ⟨1, fun (x : Fin 1) => b⟩) (g : RegularFormClass K → α) (hg : ∀ (p : RegularFormPresentation K), g ⟦p⟧ = f p) : g = liftDiagonal f ⋯ ⋯ hone

The lifted invariant is the unique function on isometry classes with the stated values on diagonal presentations.