Results about inverses in Clifford algebras

This contains some basic results about the inversion of vectors, related to the fact that $ι(m)^{-1} = \frac{ι(m)}{Q(m)}$.

def CliffordAlgebra.invertibleιOfInvertible {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) [Invertible (Q m)] : Invertible ((ι Q) m)

If the quadratic form of a vector is invertible, then so is that vector.

Equations

• CliffordAlgebra.invertibleιOfInvertible Q m = { invOf := (CliffordAlgebra.ι Q) (⅟(Q m) • m), invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem CliffordAlgebra.invOf_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) [Invertible (Q m)] [Invertible ((ι Q) m)] : ⅟((ι Q) m) = (ι Q) (⅟(Q m) • m)

For a vector with invertible quadratic form, $v^{-1} = \frac{v}{Q(v)}$

theorem CliffordAlgebra.isUnit_ι_of_isUnit {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {m : M} (h : IsUnit (Q m)) : IsUnit ((ι Q) m)

theorem CliffordAlgebra.ι_mul_ι_mul_invOf_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a b : M) [Invertible ((ι Q) a)] [Invertible (Q a)] : (ι Q) a * (ι Q) b * ⅟((ι Q) a) = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)

$aba^{-1}$ is a vector.

theorem CliffordAlgebra.invOf_ι_mul_ι_mul_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a b : M) [Invertible ((ι Q) a)] [Invertible (Q a)] : ⅟((ι Q) a) * (ι Q) b * (ι Q) a = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)

$a^{-1}ba$ is a vector.

def CliffordAlgebra.invertibleOfInvertibleι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (m : M) [Invertible ((ι Q) m)] : Invertible (Q m)

Over a ring where 2 is invertible, Q m is invertible whenever ι Q m.

Equations

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

theorem CliffordAlgebra.isUnit_of_isUnit_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {m : M} (h : IsUnit ((ι Q) m)) : IsUnit (Q m)

@[simp]

theorem CliffordAlgebra.isUnit_ι_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {m : M} : IsUnit ((ι Q) m) ↔ IsUnit (Q m)