The exterior-square model of quadratic Clifford elements

The half-normalized Clifford bivector map identifies the second exterior power with the canonical Lie subalgebra of quadratic elements in the Clifford algebra. Transporting its Lie structure equips the exterior square with the corresponding commutator bracket.

This is a generic interface for identifying bivectors with the orthogonal Lie algebra. It does not construct that orthogonal Lie equivalence.

Main results

• CliffordAlgebra.bivectorExteriorEquivQuadraticLieSubalgebra: the exterior square is linearly equivalent to the quadratic Lie subalgebra.
• CliffordAlgebra.bivectorLieRing and CliffordAlgebra.bivectorLieAlgebra: the Lie structures transported to the exterior square.
• CliffordAlgebra.bivectorLieEquiv: the transported Lie equivalence with the quadratic Lie subalgebra.

noncomputable def CliffordAlgebra.bivectorExteriorEquivQuadraticLieSubalgebra {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : ↥(⋀[R]^2 M) ≃ₗ[R] ↥(quadraticLieSubalgebra Q)

The second exterior power is linearly equivalent to the quadratic elements of the Clifford algebra through the half-normalized Clifford bivector map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CliffordAlgebra.coe_bivectorExteriorEquivQuadraticLieSubalgebra_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(⋀[R]^2 M)) : ↑((bivectorExteriorEquivQuadraticLieSubalgebra Q) x) = (bivectorExterior Q) x

The quadratic element underlying the exterior-square equivalence is the Clifford bivector map.

@[simp]

theorem CliffordAlgebra.coe_bivectorExteriorEquivQuadraticLieSubalgebra_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(quadraticLieSubalgebra Q)) : ↑((bivectorExteriorEquivQuadraticLieSubalgebra Q).symm x) = (equivExterior Q) ↑x

The exterior-algebra element underlying the inverse equivalence is the exterior model of the quadratic Clifford element.

@[reducible, inline]

noncomputable abbrev CliffordAlgebra.bivectorLieRing {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : LieRing ↥(⋀[R]^2 M)

The Lie ring structure on the second exterior power transported from the quadratic elements through bivectorExteriorEquivQuadraticLieSubalgebra. It is explicit in Q because the exterior square alone does not determine the quadratic form. This is an abbreviation so the canonical exterior-power additive structure remains visible to downstream linear maps.

Equations

• CliffordAlgebra.bivectorLieRing Q = (CliffordAlgebra.bivectorExteriorEquivQuadraticLieSubalgebra Q).toAddEquiv.lieRing

@[reducible, inline]

noncomputable abbrev CliffordAlgebra.bivectorLieAlgebra {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : LieAlgebra R ↥(⋀[R]^2 M)

The Lie algebra structure on the second exterior power transported from the quadratic elements. It is explicit in Q for the same reason as bivectorLieRing.

Equations

• CliffordAlgebra.bivectorLieAlgebra Q = (CliffordAlgebra.bivectorExteriorEquivQuadraticLieSubalgebra Q).lieAlgebra

noncomputable def CliffordAlgebra.bivectorLieEquiv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : ↥(⋀[R]^2 M) ≃ₗ⁅R⁆ ↥(quadraticLieSubalgebra Q)

The transported Lie equivalence between the second exterior power and the quadratic elements.

Equations

• CliffordAlgebra.bivectorLieEquiv Q = LinearEquiv.lieEquiv R (CliffordAlgebra.bivectorExteriorEquivQuadraticLieSubalgebra Q)

@[simp]

theorem CliffordAlgebra.bivectorLieEquiv_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(⋀[R]^2 M)) : (bivectorLieEquiv Q) x = (bivectorExteriorEquivQuadraticLieSubalgebra Q) x

The transported Lie equivalence has the same forward map as the exterior-square linear equivalence.

@[simp]

theorem CliffordAlgebra.bivectorLieEquiv_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(quadraticLieSubalgebra Q)) : (bivectorLieEquiv Q).symm x = (bivectorExteriorEquivQuadraticLieSubalgebra Q).symm x

The inverse transported Lie equivalence has the same map as the inverse exterior-square linear equivalence.