The centre of the even Clifford algebra in even dimension

Let Q be a nondegenerate quadratic form on a vector space of even positive dimension n over a field of characteristic different from two, let v₁, …, vₙ be an anisotropic orthogonal basis, and let ω = v₁ ⋯ vₙ be its volume element. Then ω lies in the even Clifford algebra C₀, and

  center C₀ = K ⊕ Kω ≅ K[X] ⧸ (X² - d),   d = (-1) ^ (n.choose 2) * Q v₁ ⋯ Q vₙ,

the root of X² - d going to ω. Up to squares, d is the signed discriminant of Q, so the centre is the discriminant quadratic algebra of Q. This is the even-dimensional companion of CliffordAlgebra.center_eq_adjoin_volume, which computes the centre of the full Clifford algebra in odd dimension; in even dimension the full Clifford algebra is central (TauCeti.CliffordAlgebra.isCentral_of_even_finrank) and the two-dimensional centre appears in C₀ instead. In dimension four this centre is the discriminant quadratic algebra over which C₀ is a quaternion algebra (a product of two quaternion algebras over K when it splits).

The volume element of an orthogonal spanning list of even length anticommutes with every vector, hence commutes with every product of two vectors and so with all of C₀ (CliffordAlgebra.prod_map_ι_mem_center_even_of_even_length; this needs no field). For the converse, splitting off a line identifies C₀ with the full Clifford algebra of a regular form in odd dimension n - 1 (TauCeti.CliffordAlgebra.exists_nonempty_algEquiv_even_of_finrank_pos), whose centre is two-dimensional by CliffordAlgebra.mem_center_iff_exists_eq_add_smul_volume. Since ω is central but not a scalar (CliffordAlgebra.prod_map_ι_ne_algebraMap_of_even_length), it spans the centre together with 1.

Main results

• CliffordAlgebra.prod_map_ι_mem_center_even_of_even_length: the volume element of an orthogonal spanning list of even length is central in the even Clifford algebra.
• CliffordAlgebra.mem_center_even_iff_exists_eq_add_smul_volume: in even positive dimension, an element of the even Clifford algebra is central exactly when it is of the form a + b • ω.
• CliffordAlgebra.center_even_eq_adjoin_volume: the centre of the even Clifford algebra is generated by the volume element.
• CliffordAlgebra.adjoinRootEquivCenterEven: the centre of the even Clifford algebra is K[X] ⧸ (X² - d), the root going to the volume element.
• CliffordAlgebra.isField_center_even_iff_not_isSquare_discriminant: this centre is a field exactly when its signed discriminant is not a square.
• CliffordAlgebra.nonempty_center_even_algEquiv_prod_iff_isSquare_discriminant: this centre is isomorphic to K × K exactly when its signed discriminant is a square.
• CliffordAlgebra.finite_even_over_center: the even Clifford algebra is module-finite over its centre when the quadratic space is finite-dimensional.
• CliffordAlgebra.finrank_center_even: this centre has dimension two over the base field.
• CliffordAlgebra.finrank_even_over_center: when the centre is a field, the even Clifford algebra has dimension 2 ^ (finrank K V - 2) over its centre, with CliffordAlgebra.finrank_even_over_center_of_finrank_eq_four the dimension-four case.
• TauCeti.CliffordAlgebra.exists_mem_center_even_forall_ne_algebraMap: in even positive dimension, the centre contains a non-scalar element.

References

• M.-A. Knus, Quadratic and Hermitian Forms over Rings (1991), Chapter IV, §3.
• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter V, §2.

theorem CliffordAlgebra.prod_map_ι_mem_even_of_even_length {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hlen : Even l.length) : (List.map (⇑(ι Q)) l).prod ∈ even Q

An ordered product of evenly many generators lies in the even Clifford algebra.

theorem CliffordAlgebra.prod_map_ι_mem_center_even_of_even_length {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) : ⟨(List.map (⇑(ι Q)) l).prod, ⋯⟩ ∈ Subalgebra.center R ↥(even Q)

The volume element of even length is central in the even Clifford algebra. The ordered product of a pairwise orthogonal spanning list of even length anticommutes with every vector (CliffordAlgebra.prod_map_ι_mul_ι_of_even_length), hence commutes with every product of two vectors, and these generate the even Clifford algebra.

theorem CliffordAlgebra.prod_map_ι_ne_algebraMap_of_even_length {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [NeZero 2] {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (hne : l ≠ []) (hQl : ∀ v ∈ l, Q v ≠ 0) (c : K) : (List.map (⇑(ι Q)) l).prod ≠ (algebraMap K (CliffordAlgebra Q)) c

The volume element of even positive length is not a scalar. The ordered product ω of a nonempty pairwise orthogonal anisotropic list of even length anticommutes with each member v of the list, while a scalar commutes with ι Q v ≠ 0; away from characteristic two this forces the scalar to vanish, but ω is a unit.

theorem CliffordAlgebra.add_smul_volume_injective_of_even_length {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [NeZero 2] {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (hne : l ≠ []) (hQl : ∀ v ∈ l, Q v ≠ 0) : Function.Injective fun (p : K × K) => (algebraMap K (CliffordAlgebra Q)) p.1 + p.2 • (List.map (⇑(ι Q)) l).prod

The scalar and volume coordinates a + b • ω are unique for the volume element ω of a nonempty pairwise orthogonal anisotropic list of even length: the even-length companion of CliffordAlgebra.add_smul_volume_injective. Here both summands are even, so the grading does not separate them; instead ω is not a scalar (CliffordAlgebra.prod_map_ι_ne_algebraMap_of_even_length).

theorem CliffordAlgebra.mem_center_even_iff_exists_eq_add_smul_volume {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [NeZero 2] {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (hspan : Submodule.span K {x : V | x ∈ l} = ⊤) (hQl : ∀ v ∈ l, Q v ≠ 0) {x : ↥(even Q)} : x ∈ Subalgebra.center K ↥(even Q) ↔ ∃ (a : K) (b : K), ↑x = (algebraMap K (CliffordAlgebra Q)) a + b • (List.map (⇑(ι Q)) l).prod

The centre of the even Clifford algebra in even dimension is K + Kω. Let l be an anisotropic orthogonal spanning list of even length and let ω be the ordered product of its Clifford generators. An element of the even Clifford algebra is central in it exactly when it is a scalar plus a scalar multiple of ω.

Such a list is a basis, so the form is nondegenerate and the dimension even; the empty list is the zero space, where ω = 1, the sum K + Kω is not direct and the even Clifford algebra is the base field. Conversely, every nondegenerate form on a space of even positive finite dimension (over a field of characteristic different from two) has such a list: QuadraticMap.Nondegenerate.exists_list_pairwise_isOrtho gives an anisotropic orthogonal spanning list whose length is the dimension.

theorem CliffordAlgebra.center_even_eq_adjoin_volume {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [NeZero 2] {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (hspan : Submodule.span K {x : V | x ∈ l} = ⊤) (hQl : ∀ v ∈ l, Q v ≠ 0) : Subalgebra.center K ↥(even Q) = K[⟨(List.map (⇑(ι Q)) l).prod, ⋯⟩]

The centre of the even Clifford algebra in even dimension is generated by a volume element. For an anisotropic orthogonal spanning list l of even length, its ordered Clifford product ω, an element of the even Clifford algebra, generates the centre of that algebra as a K-subalgebra. Equivalently, the centre is the space K + Kω described by CliffordAlgebra.mem_center_even_iff_exists_eq_add_smul_volume, two-dimensional when l is nonempty.

noncomputable def CliffordAlgebra.adjoinRootEquivCenterEven {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [NeZero 2] {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (hne : l ≠ []) (hspan : Submodule.span K {x : V | x ∈ l} = ⊤) (hQl : ∀ v ∈ l, Q v ≠ 0) : AdjoinRoot (Polynomial.X ^ 2 - Polynomial.C ((-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod)) ≃ₐ[K] ↥(Subalgebra.center K ↥(even Q))

The centre of the even Clifford algebra in even dimension is the quadratic algebra K[X] ⧸ (X² - d). For a nonempty anisotropic orthogonal spanning list v₁, …, vₙ of even length, with d = (-1) ^ (n.choose 2) * Q v₁ ⋯ Q vₙ (the signed discriminant of Q, up to squares), the root of X² - d goes to the volume element ω = v₁ ⋯ vₙ (CliffordAlgebra.coe_adjoinRootEquivCenterEven_root).

@[simp]

theorem CliffordAlgebra.coe_adjoinRootEquivCenterEven_root {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [NeZero 2] {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (hne : l ≠ []) (hspan : Submodule.span K {x : V | x ∈ l} = ⊤) (hQl : ∀ v ∈ l, Q v ≠ 0) : ↑↑((adjoinRootEquivCenterEven hl hlen hne hspan hQl) (AdjoinRoot.root (Polynomial.X ^ 2 - Polynomial.C ((-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod)))) = (List.map (⇑(ι Q)) l).prod

CliffordAlgebra.adjoinRootEquivCenterEven sends the root of X² - d to the volume element.

theorem CliffordAlgebra.isField_center_even_iff_not_isSquare_discriminant {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [NeZero 2] {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (hne : l ≠ []) (hspan : Submodule.span K {x : V | x ∈ l} = ⊤) (hQl : ∀ v ∈ l, Q v ≠ 0) : IsField ↥(Subalgebra.center K ↥(even Q)) ↔ ¬IsSquare ((-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod)

The centre of an even Clifford algebra is a field exactly when the signed discriminant of an anisotropic orthogonal spanning list is not a square.

theorem CliffordAlgebra.nonempty_center_even_algEquiv_prod_iff_isSquare_discriminant {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [NeZero 2] {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (hne : l ≠ []) (hspan : Submodule.span K {x : V | x ∈ l} = ⊤) (hQl : ∀ v ∈ l, Q v ≠ 0) : Nonempty (↥(Subalgebra.center K ↥(even Q)) ≃ₐ[K] K × K) ↔ IsSquare ((-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod)

The centre of an even Clifford algebra is a split quadratic algebra exactly when the signed discriminant of an anisotropic orthogonal spanning list is a square.

theorem CliffordAlgebra.finite_even_over_center {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) : Module.Finite ↥(Subalgebra.center K ↥(even Q)) ↥(even Q)

The even Clifford algebra of a finite-dimensional quadratic space is module-finite over its center.

theorem CliffordAlgebra.finrank_center_even {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [NeZero 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (heven : Even (Module.finrank K V)) (hpos : 0 < Module.finrank K V) : Module.finrank K ↥(Subalgebra.center K ↥(even Q)) = 2

The centre of the even Clifford algebra of a regular, positive even-dimensional quadratic space has dimension two over the base field.

theorem CliffordAlgebra.finrank_even_over_center {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [NeZero 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (heven : Even (Module.finrank K V)) (hpos : 0 < Module.finrank K V) (hfield : IsField ↥(Subalgebra.center K ↥(even Q))) : Module.finrank ↥(Subalgebra.center K ↥(even Q)) ↥(even Q) = 2 ^ (Module.finrank K V - 2)

If the centre of a regular, positive even-dimensional even Clifford algebra is a field, then the algebra has dimension 2 ^ (finrank K V - 2) over its centre.

theorem CliffordAlgebra.finrank_even_over_center_of_finrank_eq_four {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [NeZero 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 4) (hfield : IsField ↥(Subalgebra.center K ↥(even Q))) : Module.finrank ↥(Subalgebra.center K ↥(even Q)) ↥(even Q) = 4

If the discriminant centre of a regular four-dimensional even Clifford algebra is a field, then the even Clifford algebra has dimension four over that centre.

theorem TauCeti.CliffordAlgebra.exists_mem_center_even_forall_ne_algebraMap {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [NeZero 2] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (heven : Even (Module.finrank K V)) (hpos : 0 < Module.finrank K V) : ∃ x ∈ Subalgebra.center K ↥(CliffordAlgebra.even Q), ∀ (a : K), x ≠ (algebraMap K ↥(CliffordAlgebra.even Q)) a

The centre of the even Clifford algebra of a regular quadratic space of even positive dimension contains a non-scalar element.