# Documentation

Counterexamples.CliffordAlgebra_not_injective

# algebraMap R (CliffordAlgebra Q) is not always injective. #

A formalization of Darij Grinberg's answer to a "Clifford PBW theorem for quadratic form" post on MathOverflow, that provides a counterexample to Function.Injective (algebraMap R (CliffordAlgebra Q)).

The outline is that we define:

• $k$ (Q60596.K) as the commutative ring $𝔽₂[α, β, γ] / (α², β², γ²)$
• $L$ (Q60596.L) as the $k$-module $⟨x,y,z⟩ / ⟨αx + βy + γz⟩$
• $Q$ (Q60596.Q) as the quadratic form sending $Q(\overline{ax + by = cz}) = a² + b² + c²$

and discover that $αβγ ≠ 0$ as an element of $K$, but $αβγ = 0$ as an element of $𝒞l(Q)$.

Some Zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.F0.9D.94.BD.E2.82.82.5B.CE.B1.2C.20.CE.B2.2C.20.CE.B3.5D.20.2F.20.28.CE.B1.C2.B2.2C.20.CE.B2.C2.B2.2C.20.CE.B3.C2.B2.29/near/222716333.

The monomial ideal generated by terms of the form $x_ix_i$.

Equations
Instances For
theorem Q60596.mem_kIdeal_iff (x : MvPolynomial (Fin 3) (ZMod 2)) :
m, ∃ (i : Fin 3), 2 m i

𝔽₂[α, β, γ] / (α², β², γ²)

Equations
Instances For
instance Q60596.K.charP :

k has characteristic 2.

Equations

The generators of K.

Equations
Instances For
@[simp]
theorem Q60596.X_sq (i : Fin 3) :
= 0

The elements above square to zero

theorem Q60596.sq_zero_of_αβγ_mul {x : Q60596.K} :
* x = 0x * x = 0

If an element multiplied by αβγ is zero then it squares to zero.

Though αβγ is not itself zero

@[simp]
theorem Q60596.lFunc_apply (a : Fin 3Q60596.K) :
= * a 0 + * a 1 + * a 2

The 1-form on $K^3$, the kernel of which we will take a quotient by.

Our source uses $αx - βy - γz$, though since this is characteristic two we just use $αx + βy + γz$.

Equations
Instances For
@[inline, reducible]
abbrev Q60596.L :

The quotient of K^3 by the specified relation.

Equations
Instances For
def Q60596.sq {ι : Type u_1} {R : Type u_2} [] (i : ι) :

The quadratic form corresponding to squaring a single coefficient.

Equations
Instances For
theorem Q60596.sq_map_add_char_two {ι : Type u_1} {R : Type u_2} [] [CharP R 2] (i : ι) (a : ιR) (b : ιR) :
() (a + b) = () a + () b
theorem Q60596.sq_map_sub_char_two {ι : Type u_1} {R : Type u_2} [] [CharP R 2] (i : ι) (a : ιR) (b : ιR) :
() (a - b) = () a - () b
def Q60596.Q' :

The quadratic form (metric) is just euclidean

Equations
Instances For
theorem Q60596.Q'_add (x : Fin 3Q60596.K) (y : Fin 3Q60596.K) :
Q60596.Q' (x + y) =
theorem Q60596.Q'_sub (x : Fin 3Q60596.K) (y : Fin 3Q60596.K) :
Q60596.Q' (x - y) =
theorem Q60596.Q'_apply (a : Fin 3Q60596.K) :
= a 0 * a 0 + a 1 * a 1 + a 2 * a 2
theorem Q60596.Q'_apply_single (i : Fin 3) (x : Q60596.K) :
Q60596.Q' () = x * x
theorem Q60596.Q'_zero_under_ideal (v : Fin 3Q60596.K) (hv : ) :
= 0
@[simp]
theorem Q60596.Q_apply (x : Q60596.L) :

Q', lifted to operate on the quotient space L.

Equations
Instances For
def Q60596.gen (i : Fin 3) :

Basis vectors in the Clifford algebra

Equations
Instances For
@[simp]
theorem Q60596.gen_mul_gen (i : Fin 3) :
= 1

The basis vectors square to one

theorem Q60596.quot_obv :
- - = 0

By virtue of the quotient, terms of this form are zero

The core of the proof - scaling 1 by α * β * γ gives zero

Our final result: for the quadratic form Q60596.Q, the algebra map to the Clifford algebra is not injective, as it sends the non-zero α * β * γ to zero.

theorem CliffordAlgebra.not_forall_algebraMap_injective :
¬∀ (R : Type) (M : Type v) [inst : ] [inst_1 : ] [inst_2 : Module R M] (Q : ),

The general statement: not every Clifford algebra over a module has an injective algebra map.