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 ((CliffordAlgebra.ι 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 := ⋯ }
Instances For
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 ((CliffordAlgebra.ι Q) m)]
:
⅟((CliffordAlgebra.ι Q) m) = (CliffordAlgebra.ι 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 ((CliffordAlgebra.ι 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 : M)
(b : M)
[Invertible ((CliffordAlgebra.ι Q) a)]
[Invertible (Q a)]
:
(CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b * ⅟((CliffordAlgebra.ι Q) a) = (CliffordAlgebra.ι Q) ((⅟(Q a) * QuadraticForm.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 : M)
(b : M)
[Invertible ((CliffordAlgebra.ι Q) a)]
[Invertible (Q a)]
:
⅟((CliffordAlgebra.ι Q) a) * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a = (CliffordAlgebra.ι Q) ((⅟(Q a) * QuadraticForm.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 ((CliffordAlgebra.ι 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.
Instances For
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 ((CliffordAlgebra.ι 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 ((CliffordAlgebra.ι Q) m) ↔ IsUnit (Q m)