Documentation

TauCeti.LinearAlgebra.QuadraticForm.RegularFormClass.Clifford

The Clifford invariant of a regular quadratic form #

Over a field K in which two is invertible, a regular quadratic form q of rank n on a finite-dimensional space determines a central simple K-algebra: its Clifford algebra C(q) when n is even, and its even Clifford algebra C₀(q) when n is odd. The Clifford invariant (or Witt invariant) c(q) is the Brauer class of that algebra (Lam V.3.12).

The invariant is defined on TauCeti.RegularFormClass, through the Clifford algebra of a diagonal presentation. It does not depend on the presentation, because an isometry of quadratic forms induces an isomorphism of Clifford algebras and of their even subalgebras. Its value on the class of an arbitrary regular form is the Brauer class of any central simple algebra isomorphic to the Clifford algebra, or the even Clifford algebra, of that form (TauCeti.RegularFormClass.cliffordInvariant_formClass_eq_mk and TauCeti.RegularFormClass.cliffordInvariant_formClass_of_odd).

Every Clifford invariant is 2-torsion, because the reversion of a Clifford algebra identifies it with its opposite algebra, and in odd rank the even Clifford algebra is itself a Clifford algebra in one lower rank. In ranks at most two the Clifford and Hasse invariants agree: the Clifford algebra of ⟨a, b⟩ is the quaternion algebra ℍ[K, a, b], while in ranks 0 and 1 the algebra is K. In rank three the even Clifford algebra is the quaternion algebra (-a/c,-b/c). Expanding that symbol gives the first nontrivial case of Lam's comparison with the Hasse invariant, including both correction terms.

Two recurrences reduce the invariant of any diagonal form to quaternion symbols. Splitting off a binary plane, the Clifford algebra of ⟨a, b⟩ ⊥ q is ℍ[K, a, b] ⊗ C(-a⁻¹b⁻¹ · q), so c(⟨a, b⟩ ⊥ x) = [(a, b)] · c(⟨-ab⟩ ⊗ x) when x has even rank. Splitting off a line, the even Clifford algebra of q ⊥ ⟨a⟩ is C(-a⁻¹ · q), so c(x ⊥ ⟨a⟩) = c(⟨-a⟩ ⊗ x) when x has even rank. In rank four the first gives c⟨a, b, c, d⟩ = [(a, b)] · [(-abc, -abd)].

Together with the orthogonal-sum and scaling formulas for the Hasse invariant, these recurrences give Lam's comparison (Lam V.3.20) in every rank: for a class of rank n and discriminant d, c(q) = s(q) · [(-1, d)]^C(n-1,2) · [(-1,-1)]^C(n+1,4). Since every quaternion symbol is 2-torsion, only the parities of the binomial exponents matter. On a class of rank 2m with trivial signed discriminant, which is a class whose Witt class lies in the square of the fundamental ideal, the formula becomes c(q) = s(q) · [(-1,-1)]^C(m,2). Lam (p. 120) cautions that the version of this formula published by C. T. C. Wall is incorrect.

On such a class x the Clifford invariant is additive: c(x ⊥ y) = c(x) · c(y) for every class y. This follows by induction on the rank of y from the two recurrences, since rescaling x does not change c(x). In particular adding a hyperbolic plane does not change the Clifford invariant, so it depends only on the Witt class.

Main definitions #

Main results #

References #

The central simple algebra of a presentation #

The Clifford invariant #

source
noncomputable def TauCeti.RegularFormClass.cliffordInvariant {K : Type u} [Field K] [Invertible 2] :
RegularFormClass K → BrauerGroup K

The Clifford invariant of an isometry class of regular quadratic forms: for a diagonal presentation q of rank n, the Brauer class of the Clifford algebra C(q) when n is even and of the even Clifford algebra C₀(q) when n is odd (Lam V.3.12). It does not depend on the presentation.

Instances For
    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_mk_of_even {K : Type u} [Field K] [Invertible 2] (p : RegularFormPresentation K) (h : Even p.fst) (A : CSA K) (e : CliffordAlgebra (presentedForm p) ≃ₐ[K] ↑A.toAlgCat) :
    cliffordInvariant ⟦p⟧ = BrauerGroup.mk A

    On a presentation of even rank, the Clifford invariant is the Brauer class of any central simple algebra isomorphic to the Clifford algebra of the presented form.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_mk_of_odd {K : Type u} [Field K] [Invertible 2] (p : RegularFormPresentation K) (h : Odd p.fst) (A : CSA K) (e : ↥(CliffordAlgebra.even (presentedForm p)) ≃ₐ[K] ↑A.toAlgCat) :
    cliffordInvariant ⟦p⟧ = BrauerGroup.mk A

    On a presentation of odd rank, the Clifford invariant is the Brauer class of any central simple algebra isomorphic to the even Clifford algebra of the presented form.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_formClass_eq_mk {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (A : CSA K) (e : CliffordAlgebra Q ≃ₐ[K] ↑A.toAlgCat) :
    (formClass Q hQ).cliffordInvariant = BrauerGroup.mk A

    The Clifford invariant of a regular form is the Brauer class of any central simple algebra isomorphic to its Clifford algebra. Such an algebra exists only in even dimension, because the Clifford algebra is not central in odd dimension.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_formClass_of_odd {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (h : Odd (Module.finrank K V)) (A : CSA K) (e : ↥(CliffordAlgebra.even Q) ≃ₐ[K] ↑A.toAlgCat) :
    (formClass Q hQ).cliffordInvariant = BrauerGroup.mk A

    The Clifford invariant of a regular form of odd dimension is the Brauer class of any central simple algebra isomorphic to its even Clifford algebra.

    Two-torsion #

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_sq {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) :
    x.cliffordInvariant ^ 2 = 1

    The Clifford invariant is 2-torsion.

    Low rank #

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_eq_one_of_rank_le_one {K : Type u} [Field K] [Invertible 2] {x : RegularFormClass K} (hx : x.rank ≤ 1) :
    x.cliffordInvariant = 1

    The Clifford invariant is trivial in ranks 0 and 1, where the selected algebra is K.

    source
    @[simp]
    theorem TauCeti.RegularFormClass.cliffordInvariant_zero {K : Type u} [Field K] [Invertible 2] :
    cliffordInvariant 0 = 1

    The zero class has trivial Clifford invariant.

    source
    @[simp]
    theorem TauCeti.RegularFormClass.cliffordInvariant_one {K : Type u} [Field K] [Invertible 2] :
    cliffordInvariant 1 = 1

    The unit class ⟨1⟩ has trivial Clifford invariant.

    source
    @[simp]
    theorem TauCeti.RegularFormClass.cliffordInvariant_mk_binary {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) :
    cliffordInvariant ⟦⟨2, ![a, b]⟩⟧ = BrauerGroup.quaternionClass a b

    The Clifford invariant of a binary form ⟨a, b⟩ is the quaternion symbol [(a, b)]: the Clifford algebra of ⟨a, b⟩ is the quaternion algebra ℍ[K, a, b].

    source
    @[simp]
    theorem TauCeti.RegularFormClass.cliffordInvariant_mk_ternary {K : Type u} [Field K] [Invertible 2] (a b c : Kˣ) :
    cliffordInvariant ⟦⟨3, ![a, b, c]⟩⟧ = BrauerGroup.quaternionClass (-c⁻¹ * a) (-c⁻¹ * b)

    The Clifford invariant of a ternary form is the quaternion symbol [(-a/c, -b/c)].

    Splitting off a binary plane and a line #

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_mk_binary_add {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) {x : RegularFormClass K} (hx : Even x.rank) :
    cliffordInvariant (⟦⟨2, ![a, b]⟩⟧ + x) = BrauerGroup.quaternionClass a b * cliffordInvariant (⟦⟨1, fun (x : Fin 1) => -(a * b)⟩⟧ * x)

    Splitting a binary plane off the Clifford invariant (Lam, Chapter V, §2): for a class x of even rank, c(⟨a, b⟩ ⊥ x) = [(a, b)] · c(⟨-ab⟩ ⊗ x). Indeed the Clifford algebra of ⟨a, b⟩ ⊥ q is ℍ[K, a, b] ⊗ C(-a⁻¹b⁻¹ · q), and -a⁻¹b⁻¹ and -ab differ by a square.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_add_mk_rankOne {K : Type u} [Field K] [Invertible 2] (a : Kˣ) {x : RegularFormClass K} (hx : Even x.rank) :
    (x + ⟦⟨1, fun (x : Fin 1) => a⟩⟧).cliffordInvariant = cliffordInvariant (⟦⟨1, fun (x : Fin 1) => -a⟩⟧ * x)

    Splitting a line off the Clifford invariant: for a class x of even rank, c(x ⊥ ⟨a⟩) = c(⟨-a⟩ ⊗ x). The even Clifford algebra of q ⊥ ⟨a⟩ is the Clifford algebra of -a⁻¹ · q, and -a⁻¹ and -a differ by a square.

    source
    @[simp]
    theorem TauCeti.RegularFormClass.cliffordInvariant_mk_quaternary {K : Type u} [Field K] [Invertible 2] (a b c d : Kˣ) :
    cliffordInvariant ⟦⟨4, ![a, b, c, d]⟩⟧ = BrauerGroup.quaternionClass a b * BrauerGroup.quaternionClass (-(a * b) * c) (-(a * b) * d)

    The Clifford invariant of a quaternary form is the product of quaternion symbols [(a, b)] · [(-abc, -abd)], by splitting off the plane ⟨a, b⟩.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_eq_hasseInvariant_of_rank_le_two {K : Type u} [Field K] [Invertible 2] {x : RegularFormClass K} (hx : x.rank ≤ 2) :
    x.cliffordInvariant = x.hasseInvariant

    In ranks at most two the Clifford invariant is the Hasse invariant. This is the low-rank case of Lam V.3.20, whose correction terms vanish for n ≤ 2.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_mk_ternary_eq_hasseInvariant_mul {K : Type u} [Field K] [Invertible 2] (a b c : Kˣ) :
    cliffordInvariant ⟦⟨3, ![a, b, c]⟩⟧ = hasseInvariant ⟦⟨3, ![a, b, c]⟩⟧ * BrauerGroup.quaternionClass (-1) (a * b * c) * BrauerGroup.quaternionClass (-1) (-1)

    Lam's Clifford--Hasse comparison in rank three. For q = ⟨a,b,c⟩, c(q) = s(q) · [(-1,abc)] · [(-1,-1)]. These are exactly the two correction terms in Lam V.3.20, since both relevant binomial exponents are one in rank three.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_eq_hasseInvariant_mul_of_rank_eq_three {K : Type u} [Field K] [Invertible 2] {x : RegularFormClass K} (hx : x.rank = 3) :
    x.cliffordInvariant = x.hasseInvariant * BrauerGroup.quaternionClassOnSquareClasses (squareClass (-1)) x.discr * BrauerGroup.quaternionClass (-1) (-1)

    Lam's Clifford--Hasse comparison for every rank-three regular-form class. The second correction pairs -1 with the discriminant, while the last is the constant symbol [(-1,-1)].

    Lam's comparison in every rank #

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_eq_hasseInvariant_mul {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) :
    x.cliffordInvariant = x.hasseInvariant * BrauerGroup.quaternionClassOnSquareClasses (squareClass (-1)) x.discr ^ (x.rank - 1).choose 2 * BrauerGroup.quaternionClass (-1) (-1) ^ (x.rank + 1).choose 4

    Lam's comparison of the Clifford and Hasse invariants (Lam V.3.20). For a class of rank n with discriminant d, c(q) = s(q) · [(-1, d)]^C(n-1,2) · [(-1,-1)]^C(n+1,4), where C(n-1,2) = (n-1)(n-2)/2 and C(n+1,4) = (n+1)n(n-1)(n-2)/24.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_eq_hasseInvariant_mul_of_signedDiscr_eq_zero {K : Type u} [Field K] [Invertible 2] {x : RegularFormClass K} {m : ℕ} (hx : x.rank = 2 * m) (hd : x.signedDiscr = 0) :
    x.cliffordInvariant = x.hasseInvariant * BrauerGroup.quaternionClass (-1) (-1) ^ m.choose 2

    Lam's comparison on the square of the fundamental ideal. For a class of rank 2m with trivial signed discriminant, c(q) = s(q) · [(-1,-1)]^C(m,2): the discriminant correction in TauCeti.RegularFormClass.cliffordInvariant_eq_hasseInvariant_mul cancels. These are the classes whose Witt class lies in the square of the fundamental ideal (TauCeti.wittClass_mem_fundamentalIdeal_sq_iff).

    source
    @[simp]
    theorem TauCeti.RegularFormClass.cliffordInvariant_hyperbolicClass {K : Type u} [Field K] [Invertible 2] :
    (hyperbolicClass K).cliffordInvariant = 1

    The hyperbolic plane has trivial Clifford invariant: its Clifford algebra ℍ[K, 1, -1] is split.

    Additivity on the square of the fundamental ideal #

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_mk_rankOne_mul_of_odd {K : Type u} [Field K] [Invertible 2] (t : Kˣ) {x : RegularFormClass K} (hx : Odd x.rank) :
    cliffordInvariant (⟦⟨1, fun (x : Fin 1) => t⟩⟧ * x) = x.cliffordInvariant

    In odd rank the Clifford invariant is a similarity invariant: scaling a form by a unit preserves its even Clifford algebra.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_mk_rankOne_mul_of_signedDiscr_eq_zero {K : Type u} [Field K] [Invertible 2] (t : Kˣ) {x : RegularFormClass K} (hd : x.signedDiscr = 0) :
    cliffordInvariant (⟦⟨1, fun (x : Fin 1) => t⟩⟧ * x) = x.cliffordInvariant

    Scaling preserves the Clifford invariant of a class with trivial signed discriminant: for a class x with trivial signed discriminant, c(⟨t⟩ ⊗ x) = c(x). In even rank this says that the Witt class lies in the square of the fundamental ideal; in odd rank it is cliffordInvariant_mk_rankOne_mul_of_odd.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_add_of_signedDiscr_eq_zero {K : Type u} [Field K] [Invertible 2] {x : RegularFormClass K} (hx : Even x.rank) (hd : x.signedDiscr = 0) (y : RegularFormClass K) :
    (x + y).cliffordInvariant = x.cliffordInvariant * y.cliffordInvariant

    Additivity of the Clifford invariant on the square of the fundamental ideal: if x has even rank and trivial signed discriminant, that is if its Witt class lies in I(K)² (TauCeti.wittClass_mem_fundamentalIdeal_sq_iff), then c(x ⊥ y) = c(x) · c(y) for every class y. The identity fails for a general pair: for x = y = ⟨-1⟩ the left side is c⟨-1, -1⟩ = [(-1, -1)], which is nontrivial over ℝ, while c⟨-1⟩ = 1 in rank one.

    source
    theorem TauCeti.RegularFormClass.cliffordInvariant_nsmul_hyperbolicClass_add {K : Type u} [Field K] [Invertible 2] (m : ℕ) (x : RegularFormClass K) :
    (m • hyperbolicClass K + x).cliffordInvariant = x.cliffordInvariant

    Adding hyperbolic planes does not change the Clifford invariant, so the Clifford invariant depends only on the Witt class.

    Scalar extension #

    source
    @[simp]
    theorem TauCeti.RegularFormClass.cliffordInvariant_baseChange {K : Type u} [Field K] [Invertible 2] {L : Type u} [Field L] [Algebra K L] [Invertible 2] (x : RegularFormClass K) :
    (baseChange L x).cliffordInvariant = (BrauerGroup.baseChange K L) x.cliffordInvariant

    The Clifford invariant commutes with scalar extension: the Clifford invariant of the extension of a class to L is the image of its Clifford invariant in the Brauer group of L.