The reverse-dual Clifford action

For an R-algebra K, a K-linear Clifford action ρ on S induces an action on its K-linear dual by (a · φ)(s) = φ (ρ (CliffordAlgebra.reverse a) s). Reversal and transposition each reverse multiplication, so their composite is again an algebra action. In particular, a vector acts by the transpose of its original action. This is an algebraic dual, linear over the coefficient ring; over the complex numbers it is distinct from conjugate-linear Hermitian adjunction.

The construction needs neither finite dimension nor a nondegenerate quadratic form. It is contravariantly natural in intertwiners, and the canonical map to the double dual intertwines the original action with its double reverse dual. For reflexive modules this is an equivalence. On an orthogonal volume product of length n, the dual action is the transpose multiplied by (-1) ^ n.choose 2; this fixes the sign needed when comparing dual chiralities.

The construction uses Mathlib's LinearMap.dualMap and CliffordAlgebra.reverse.

References

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

def AlgHom.cliffordReverseDual {R : Type u_1} {K : Type u_2} {V : Type u_3} {S : Type u_4} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} [AddCommGroup S] [Module K S] [Module R S] [IsScalarTower R K S] (ρ : CliffordAlgebra Q →ₐ[R] Module.End K S) : CliffordAlgebra Q →ₐ[R] Module.End K (Module.Dual K S)

The action on the scalar dual obtained by transposing the action after Clifford reversal. No Hermitian conjugation of the coefficients is involved.

theorem AlgHom.cliffordReverseDual_apply {R : Type u_1} {K : Type u_2} {V : Type u_3} {S : Type u_4} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} [AddCommGroup S] [Module K S] [Module R S] [IsScalarTower R K S] (ρ : CliffordAlgebra Q →ₐ[R] Module.End K S) (a : CliffordAlgebra Q) : ρ.cliffordReverseDual a = LinearMap.dualMap (ρ (CliffordAlgebra.reverse a))

The reverse-dual action is the transpose of the original action after reversal.

@[simp]

theorem AlgHom.cliffordReverseDual_apply_apply {R : Type u_1} {K : Type u_2} {V : Type u_3} {S : Type u_4} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} [AddCommGroup S] [Module K S] [Module R S] [IsScalarTower R K S] (ρ : CliffordAlgebra Q →ₐ[R] Module.End K S) (a : CliffordAlgebra Q) (φ : Module.Dual K S) (s : S) : ((ρ.cliffordReverseDual a) φ) s = φ ((ρ (CliffordAlgebra.reverse a)) s)

Evaluation characterizes the reverse-dual action.

@[simp]

theorem AlgHom.cliffordReverseDual_ι {R : Type u_1} {K : Type u_2} {V : Type u_3} {S : Type u_4} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} [AddCommGroup S] [Module K S] [Module R S] [IsScalarTower R K S] (ρ : CliffordAlgebra Q →ₐ[R] Module.End K S) (v : V) : ρ.cliffordReverseDual ((CliffordAlgebra.ι Q) v) = LinearMap.dualMap (ρ ((CliffordAlgebra.ι Q) v))

Each vector acts on the reverse dual by the transpose of its action on the original module.

theorem AlgHom.dualMap_mul_cliffordReverseDual_ι {R : Type u_1} {K : Type u_2} {V : Type u_3} {S : Type u_4} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} [AddCommGroup S] [Module K S] [Module R S] [IsScalarTower R K S] (ρ : CliffordAlgebra Q →ₐ[R] Module.End K S) (γ : Module.End K S) (hγρ : ∀ (v : V), γ * ρ ((CliffordAlgebra.ι Q) v) = -(ρ ((CliffordAlgebra.ι Q) v) * γ)) (v : V) : LinearMap.dualMap γ * ρ.cliffordReverseDual ((CliffordAlgebra.ι Q) v) = -(ρ.cliffordReverseDual ((CliffordAlgebra.ι Q) v) * LinearMap.dualMap γ)

The transpose of a Clifford grading anticommutes with the reverse-dual vector action.

theorem AlgHom.cliffordReverseDual_unique {R : Type u_1} {K : Type u_2} {V : Type u_3} {S : Type u_4} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} [AddCommGroup S] [Module K S] [Module R S] [IsScalarTower R K S] (ρ : CliffordAlgebra Q →ₐ[R] Module.End K S) (σ : CliffordAlgebra Q →ₐ[R] Module.End K (Module.Dual K S)) (hσ : ∀ (v : V), σ ((CliffordAlgebra.ι Q) v) = LinearMap.dualMap (ρ ((CliffordAlgebra.ι Q) v))) : σ = ρ.cliffordReverseDual

The reverse-dual action is the unique Clifford algebra action with the prescribed transposed vector action.

theorem AlgHom.cliffordReverseDual_comp_dualMap {R : Type u_1} {K : Type u_2} {V : Type u_3} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} [AddCommGroup S] [Module K S] [Module R S] [IsScalarTower R K S] [AddCommGroup T] [Module K T] [Module R T] [IsScalarTower R K T] (ρ : CliffordAlgebra Q →ₐ[R] Module.End K S) (σ : CliffordAlgebra Q →ₐ[R] Module.End K T) (f : S →ₗ[K] T) (hf : ∀ (a : CliffordAlgebra Q), f ∘ₗ ρ a = σ a ∘ₗ f) (a : CliffordAlgebra Q) : ρ.cliffordReverseDual a ∘ₗ f.dualMap = f.dualMap ∘ₗ σ.cliffordReverseDual a

Transposition sends a Clifford intertwiner to an intertwiner in the opposite direction.

theorem AlgHom.cliffordReverseDual_cliffordReverseDual_comp_eval {R : Type u_1} {K : Type u_2} {V : Type u_3} {S : Type u_4} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} [AddCommGroup S] [Module K S] [Module R S] [IsScalarTower R K S] (ρ : CliffordAlgebra Q →ₐ[R] Module.End K S) (a : CliffordAlgebra Q) : ρ.cliffordReverseDual.cliffordReverseDual a ∘ₗ Module.Dual.eval K S = Module.Dual.eval K S ∘ₗ ρ a

The canonical evaluation into the double dual is equivariant for double reverse duality.

theorem AlgHom.cliffordReverseDual_cliffordReverseDual_eq_conj {R : Type u_1} {K : Type u_2} {V : Type u_3} {S : Type u_4} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} [AddCommGroup S] [Module K S] [Module R S] [IsScalarTower R K S] [Module.IsReflexive K S] (ρ : CliffordAlgebra Q →ₐ[R] Module.End K S) (a : CliffordAlgebra Q) : ρ.cliffordReverseDual.cliffordReverseDual a = (Module.evalEquiv K S).conj (ρ a)

On a reflexive module, evaluation identifies the double reverse-dual action with the original action. This includes finite-dimensional vector spaces and the zero module.

theorem AlgHom.cliffordReverseDual_smul_prod_map_ι {R : Type u_1} {K : Type u_2} {V : Type u_3} {S : Type u_4} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} [AddCommGroup S] [Module K S] [Module R S] [IsScalarTower R K S] (ρ : CliffordAlgebra Q →ₐ[R] Module.End K S) {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (r : R) : ρ.cliffordReverseDual (r • (List.map (⇑(CliffordAlgebra.ι Q)) l).prod) = (r * (-1) ^ l.length.choose 2) • LinearMap.dualMap (ρ (List.map (⇑(CliffordAlgebra.ι Q)) l).prod)

For an orthogonal volume product, reversal contributes the permutation sign. Scalar normalizations, including complex ones, are transposed linearly.