The volume element and even part of the split real Clifford plane

In the matrix model of Cliff(1, 1), the product z = e₁ e₂ of the coordinate generators is the swap matrix. It satisfies z² = 1, reverse z = -z, and star z = -z. The even Clifford algebra consists of the elements a + b z, uniquely, represented by the matrices !![a, b; b, a].

These are Clifford algebra computations independent of the Spin group and its hyperbolic parametrization. Both Bott periodicity and the Spin classification use this general layer.

Main definitions and results

• TauCeti.realCliffordOneOneEquivMatrix_e₀_mul_e₁: the coordinate-generator product is the swap matrix.
• TauCeti.realCliffordOneOneVolume: the volume element, with defining equation TauCeti.realCliffordOneOneVolume_def.
• TauCeti.mem_even_realCliffordOneOne_iff: the even part consists of the elements a + b z.
• TauCeti.algebraMap_add_smul_realCliffordOneOneVolume_inj: these coordinates are unique.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.

theorem TauCeti.realCliffordOneOneEquivMatrix_e₀_mul_e₁ : realCliffordOneOneEquivMatrix ((CliffordAlgebra.ι (realCliffordForm 1 1)) (Pi.single 0 1) * (CliffordAlgebra.ι (realCliffordForm 1 1)) (Pi.single 1 1)) = !![0, 1; 1, 0]

The two coordinate generators of Cliff(1, 1) multiply to the swap matrix.

noncomputable def TauCeti.realCliffordOneOneVolume : CliffordAlgebra (realCliffordForm 1 1)

The product z = e₁ e₂ of the two coordinate generators of Cliff(1, 1), the generator e₁ squaring to 1 and e₂ to -1.

theorem TauCeti.realCliffordOneOneVolume_def : realCliffordOneOneVolume = (CliffordAlgebra.ι (realCliffordForm 1 1)) (Pi.single 0 1) * (CliffordAlgebra.ι (realCliffordForm 1 1)) (Pi.single 1 1)

The volume element is the product of the positive and negative coordinate generators.

theorem TauCeti.realCliffordOneOneEquivMatrix_algebraMap_add_smul_realCliffordOneOneVolume (a b : ℝ) : realCliffordOneOneEquivMatrix ((algebraMap ℝ (CliffordAlgebra (realCliffordForm 1 1))) a + b • realCliffordOneOneVolume) = !![a, b; b, a]

In the matrix model of Cliff(1, 1), a + b z is the matrix !![a, b; b, a].

@[simp]

theorem TauCeti.realCliffordOneOneVolume_mul_self : realCliffordOneOneVolume * realCliffordOneOneVolume = 1

z² = 1.

theorem TauCeti.algebraMap_add_smul_realCliffordOneOneVolume_mul (a b c d : ℝ) : ((algebraMap ℝ (CliffordAlgebra (realCliffordForm 1 1))) a + b • realCliffordOneOneVolume) * ((algebraMap ℝ (CliffordAlgebra (realCliffordForm 1 1))) c + d • realCliffordOneOneVolume) = (algebraMap ℝ (CliffordAlgebra (realCliffordForm 1 1))) (a * c + b * d) + (a * d + b * c) • realCliffordOneOneVolume

Multiplication in the even plane ℝ + ℝ z, where z² = 1.

@[simp]

theorem TauCeti.involute_realCliffordOneOneVolume : CliffordAlgebra.involute realCliffordOneOneVolume = realCliffordOneOneVolume

z is even: the grade involution fixes it.

@[simp]

theorem TauCeti.star_realCliffordOneOneVolume : star realCliffordOneOneVolume = -realCliffordOneOneVolume

star z = -z.

@[simp]

theorem TauCeti.reverse_realCliffordOneOneVolume : CliffordAlgebra.reverse realCliffordOneOneVolume = -realCliffordOneOneVolume

reverse z = -z.

theorem TauCeti.realCliffordOneOneVolume_mem_even : realCliffordOneOneVolume ∈ CliffordAlgebra.even (realCliffordForm 1 1)

z lies in the even part of Cliff(1, 1).

theorem TauCeti.algebraMap_add_smul_realCliffordOneOneVolume_inj {a b a' b' : ℝ} : (algebraMap ℝ (CliffordAlgebra (realCliffordForm 1 1))) a + b • realCliffordOneOneVolume = (algebraMap ℝ (CliffordAlgebra (realCliffordForm 1 1))) a' + b' • realCliffordOneOneVolume ↔ a = a' ∧ b = b'

The coefficients a and b of a + b z are unique.

theorem TauCeti.exists_eq_algebraMap_add_smul_realCliffordOneOneVolume {x : CliffordAlgebra (realCliffordForm 1 1)} (hx : x ∈ CliffordAlgebra.even (realCliffordForm 1 1)) : ∃ (a : ℝ) (b : ℝ), x = (algebraMap ℝ (CliffordAlgebra (realCliffordForm 1 1))) a + b • realCliffordOneOneVolume

The even part of Cliff(1, 1). Every even element is a + b z for some real a, b.

theorem TauCeti.mem_even_realCliffordOneOne_iff {x : CliffordAlgebra (realCliffordForm 1 1)} : x ∈ CliffordAlgebra.even (realCliffordForm 1 1) ↔ ∃ (a : ℝ) (b : ℝ), x = (algebraMap ℝ (CliffordAlgebra (realCliffordForm 1 1))) a + b • realCliffordOneOneVolume

The even part of Cliff(1, 1) consists of the elements a + b z.

theorem TauCeti.star_algebraMap_add_smul_realCliffordOneOneVolume (a b : ℝ) : star ((algebraMap ℝ (CliffordAlgebra (realCliffordForm 1 1))) a + b • realCliffordOneOneVolume) = (algebraMap ℝ (CliffordAlgebra (realCliffordForm 1 1))) a + -b • realCliffordOneOneVolume

The Clifford conjugate of a + b z is a - b z.