Reversal on the centre of the even Clifford algebra

Over any commutative ring, reversal fixes the scalar coordinate of a + b • ω and multiplies its orthogonal volume coordinate by (-1) ^ (n.choose 2).

For a regular quadratic space of even positive dimension n over a field of characteristic different from two, the centre of the even Clifford algebra is K ⊕ Kω. Reversal fixes scalars and sends the volume element ω to (-1) ^ (n.choose 2) • ω. Thus it fixes the whole centre when n.choose 2 is even; otherwise its fixed elements in the centre are exactly the scalars.

The dimension-four and dimension-six specializations distinguish the two kinds of canonical involution: in dimension four reversal fixes the discriminant algebra pointwise, while in dimension six its central fixed elements are exactly the scalars. These statements hold whether the discriminant algebra is a quadratic field or a split quadratic algebra. They determine the base over which the canonical involution is linear in the low-dimensional unitary groups.

The centre and uniqueness of its scalar/volume coordinates are supplied by CliffordAlgebra.mem_center_even_iff_exists_eq_add_smul_volume and CliffordAlgebra.add_smul_volume_injective_of_even_length; the reversal sign is supplied by CliffordAlgebra.reverse_prod_map_ι_of_pairwise_isOrtho.

Main results

• TauCeti.CliffordAlgebra.reverse_add_smul_volume and TauCeti.CliffordAlgebra.reverseEven_add_smul_volume: reversal on scalar/volume coordinates over any commutative ring.
• TauCeti.CliffordAlgebra.reverseEven_prod_map_ι_of_pairwise_isOrtho: reversal on an even orthogonal volume element.
• TauCeti.CliffordAlgebra.reverse_add_smul_volume_eq_self_iff: the fixed-point criterion for an even anisotropic orthogonal volume element over a field with 2 ≠ 0.
• TauCeti.CliffordAlgebra.reverseEven_eq_self_iff_of_mem_center: the central fixed-point criterion for a regular quadratic space of even positive dimension over a field with 2 ≠ 0.
• TauCeti.CliffordAlgebra.forall_mem_center_reverseEven_eq_self_iff: the criterion for reversal to fix the whole centre pointwise.
• TauCeti.CliffordAlgebra.reverseEven_eq_self_of_mem_center_of_finrank_eq_four: pointwise fixedness in dimension four.
• TauCeti.CliffordAlgebra.reverseEven_eq_self_iff_of_mem_center_of_finrank_eq_six and TauCeti.CliffordAlgebra.exists_mem_center_reverseEven_ne_self_of_finrank_eq_six: scalar fixed elements and nontrivial central action in dimension six.

References

• M.-A. Knus, Quadratic and Hermitian Forms over Rings (1991), Chapter IV, §3.
• M.-A. Knus, A. Merkurjev, M. Rost, J.-P. Tignol, The Book of Involutions (1998), §15.

theorem TauCeti.CliffordAlgebra.reverse_add_smul_volume {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) (a b : R) : CliffordAlgebra.reverse ((algebraMap R (CliffordAlgebra Q)) a + b • (List.map (⇑(CliffordAlgebra.ι Q)) l).prod) = (algebraMap R (CliffordAlgebra Q)) a + ((-1) ^ l.length.choose 2 * b) • (List.map (⇑(CliffordAlgebra.ι Q)) l).prod

Reversal multiplies the volume coordinate of an orthogonal list by its reversal sign, while fixing the scalar coordinate.

@[simp]

theorem TauCeti.CliffordAlgebra.reverseEven_prod_map_ι_of_pairwise_isOrtho {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) : (CliffordAlgebra.reverseEven Q) ⟨(List.map (⇑(CliffordAlgebra.ι Q)) l).prod, ⋯⟩ = (-1) ^ l.length.choose 2 • ⟨(List.map (⇑(CliffordAlgebra.ι Q)) l).prod, ⋯⟩

Restricted reversal multiplies an even orthogonal volume element by its reversal sign.

theorem TauCeti.CliffordAlgebra.reverseEven_add_smul_volume {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) (a b : R) : (CliffordAlgebra.reverseEven Q) ((algebraMap R ↥(CliffordAlgebra.even Q)) a + b • ⟨(List.map (⇑(CliffordAlgebra.ι Q)) l).prod, ⋯⟩) = (algebraMap R ↥(CliffordAlgebra.even Q)) a + ((-1) ^ l.length.choose 2 * b) • ⟨(List.map (⇑(CliffordAlgebra.ι Q)) l).prod, ⋯⟩

Restricted reversal fixes the scalar coordinate and multiplies an even orthogonal volume coordinate by its reversal sign.

theorem TauCeti.CliffordAlgebra.reverse_add_smul_volume_eq_self_iff {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [NeZero 2] {Q : QuadraticForm K V} {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (hne : l ≠ []) (hQl : ∀ v ∈ l, Q v ≠ 0) (a b : K) : CliffordAlgebra.reverse ((algebraMap K (CliffordAlgebra Q)) a + b • (List.map (⇑(CliffordAlgebra.ι Q)) l).prod) = (algebraMap K (CliffordAlgebra Q)) a + b • (List.map (⇑(CliffordAlgebra.ι Q)) l).prod ↔ Even (l.length.choose 2) ∨ b = 0

For an even anisotropic orthogonal volume element, reversal fixes a + b • ω exactly when its reversal sign is positive or its volume coordinate b vanishes.

theorem TauCeti.CliffordAlgebra.reverseEven_eq_self_iff_of_mem_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) {x : ↥(CliffordAlgebra.even Q)} (hx : x ∈ Subalgebra.center K ↥(CliffordAlgebra.even Q)) : (CliffordAlgebra.reverseEven Q) x = x ↔ Even ((Module.finrank K V).choose 2) ∨ ∃ (a : K), x = (algebraMap K ↥(CliffordAlgebra.even Q)) a

In the centre of the even Clifford algebra of a regular quadratic space of even dimension, an element is fixed by reversal exactly when the volume sign is positive or it is a scalar.

theorem TauCeti.CliffordAlgebra.forall_mem_center_reverseEven_eq_self_iff {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) : (∀ x ∈ Subalgebra.center K ↥(CliffordAlgebra.even Q), (CliffordAlgebra.reverseEven Q) x = x) ↔ Even ((Module.finrank K V).choose 2)

Reversal fixes the centre of a regular even-dimensional even Clifford algebra pointwise exactly when the sign of reversal on a volume element is positive.

theorem TauCeti.CliffordAlgebra.reverseEven_eq_self_of_mem_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) {x : ↥(CliffordAlgebra.even Q)} (hx : x ∈ Subalgebra.center K ↥(CliffordAlgebra.even Q)) : (CliffordAlgebra.reverseEven Q) x = x

In dimension four, the canonical reversal fixes every element of the discriminant algebra, the centre of the even Clifford algebra.

@[simp]

theorem TauCeti.CliffordAlgebra.reverseEven_eq_self_iff_of_mem_center_of_finrank_eq_six {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 = 6) {x : ↥(CliffordAlgebra.even Q)} (hx : x ∈ Subalgebra.center K ↥(CliffordAlgebra.even Q)) : (CliffordAlgebra.reverseEven Q) x = x ↔ ∃ (a : K), x = (algebraMap K ↥(CliffordAlgebra.even Q)) a

In dimension six, the fixed elements of the discriminant algebra under canonical reversal are exactly the scalars.

theorem TauCeti.CliffordAlgebra.exists_mem_center_reverseEven_ne_self_of_finrank_eq_six {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 = 6) : ∃ x ∈ Subalgebra.center K ↥(CliffordAlgebra.even Q), (CliffordAlgebra.reverseEven Q) x ≠ x

In dimension six, reversal acts nontrivially on the centre of the even Clifford algebra. This includes both split and nonsplit discriminant algebras.