@[reducible]
def
clifford_algebra.clifford_hom
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(A : Type u_3)
[semiring A]
[algebra R A] :
Type (max u_2 u_3)
theorem
clifford_algebra.preserves_iff_bilin
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
{A : Type u_3}
[ring A]
[algebra R A]
(h2 : is_unit 2)
(f : M →ₗ[R] A) :
(∀ (x : M), ⇑f x * ⇑f x = ⇑(algebra_map R A) (⇑Q x)) ↔ ((linear_map.mul R A).compl₂ f).comp f + ((linear_map.mul R A).flip.compl₂ f).comp f = (⇑bilin_form.to_lin Q.polar_bilin).compr₂ (algebra.linear_map R A)
def
clifford_algebra.ι_wedge
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(n : ℕ)
[invertible ↑(n.factorial)] :
alternating_map R M (clifford_algebra Q) (fin n)
A wedge product of n vectors. Note this does not define the wedge product of arbitrary multivectors.
Equations
- clifford_algebra.ι_wedge n = ⅟ ↑(n.factorial) • ⇑multilinear_map.alternatization ((multilinear_map.mk_pi_algebra_fin R n (clifford_algebra Q)).comp_linear_map (λ (i : fin n), clifford_algebra.ι Q))