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.

As a bonus result, we also show BilinMap.not_forall_toQuadraticMap_surjective: that there are quadratic forms that cannot be expressed via even non-symmetric bilinear forms.

def Q60596.kIdeal : Ideal (MvPolynomial (Fin 3) (ZMod 2))

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

Equations

• Q60596.kIdeal = Ideal.span (Set.range fun (i : Fin 3) => MvPolynomial.X i * MvPolynomial.X i)

theorem Q60596.mem_kIdeal_iff (x : MvPolynomial (Fin 3) (ZMod 2)) : x ∈ Q60596.kIdeal ↔ ∀ m ∈ x.support, ∃ (i : Fin 3), 2 ≤ m i

theorem Q60596.X0_X1_X2_not_mem_kIdeal : MvPolynomial.X 0 * MvPolynomial.X 1 * MvPolynomial.X 2 ∉ Q60596.kIdeal

theorem Q60596.mul_self_mem_kIdeal_of_X0_X1_X2_mul_mem {x : MvPolynomial (Fin 3) (ZMod 2)} (h : MvPolynomial.X 0 * MvPolynomial.X 1 * MvPolynomial.X 2 * x ∈ Q60596.kIdeal) : x * x ∈ Q60596.kIdeal

def Q60596.K : Type

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

Equations

• Q60596.K = (MvPolynomial (Fin 3) (ZMod 2) ⧸ Q60596.kIdeal)

instance Q60596.instCommRingK : CommRing Q60596.K

Equations

• Q60596.instCommRingK = Ideal.Quotient.commRing Q60596.kIdeal

theorem Q60596.comap_C_kIdeal : Ideal.comap MvPolynomial.C Q60596.kIdeal = ⊥

instance Q60596.K.charP : CharP Q60596.K 2

k has characteristic 2.

def Q60596.K.gen (i : Fin 3) : Q60596.K

The generators of K.

Equations

• Q60596.K.gen i = (Ideal.Quotient.mk Q60596.kIdeal) (MvPolynomial.X i)

@[simp]

theorem Q60596.X_sq (i : Fin 3) : Q60596.K.gen i * Q60596.K.gen i = 0

The elements above square to zero

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

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

theorem Q60596.αβγ_ne_zero : Q60596.K.gen 0 * Q60596.K.gen 1 * Q60596.K.gen 2 ≠ 0

Though αβγ is not itself zero

def Q60596.lFunc : (Fin 3 → Q60596.K) →ₗ[Q60596.K] Q60596.K

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

• Q60596.lFunc = Q60596.K.gen 0 • LinearMap.proj 0 + Q60596.K.gen 1 • LinearMap.proj 1 + Q60596.K.gen 2 • LinearMap.proj 2

@[simp]

theorem Q60596.lFunc_apply (a : Fin 3 → Q60596.K) : Q60596.lFunc a = Q60596.K.gen 0 * a 0 + Q60596.K.gen 1 * a 1 + Q60596.K.gen 2 * a 2

@[reducible, inline]

abbrev Q60596.L : Type

The quotient of K^3 by the specified relation.

Equations

• Q60596.L = ((Fin 3 → Q60596.K) ⧸ LinearMap.ker Q60596.lFunc)

def Q60596.sq {ι : Type u_1} {R : Type u_2} [CommRing R] (i : ι) : QuadraticForm R (ι → R)

The quadratic form corresponding to squaring a single coefficient.

Equations

• Q60596.sq i = QuadraticMap.sq.comp (LinearMap.proj i)

theorem Q60596.sq_map_add_char_two {ι : Type u_1} {R : Type u_2} [CommRing R] [CharP R 2] (i : ι) (a b : ι → R) : (Q60596.sq i) (a + b) = (Q60596.sq i) a + (Q60596.sq i) b

theorem Q60596.sq_map_sub_char_two {ι : Type u_1} {R : Type u_2} [CommRing R] [CharP R 2] (i : ι) (a b : ι → R) : (Q60596.sq i) (a - b) = (Q60596.sq i) a - (Q60596.sq i) b

def Q60596.Q' : QuadraticForm Q60596.K (Fin 3 → Q60596.K)

The quadratic form (metric) is just euclidean

Equations

• Q60596.Q' = ∑ i : Fin 3, Q60596.sq i

theorem Q60596.Q'_add (x y : Fin 3 → Q60596.K) : Q60596.Q' (x + y) = Q60596.Q' x + Q60596.Q' y

theorem Q60596.Q'_sub (x y : Fin 3 → Q60596.K) : Q60596.Q' (x - y) = Q60596.Q' x - Q60596.Q' y

theorem Q60596.Q'_apply (a : Fin 3 → Q60596.K) : Q60596.Q' a = 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' (Pi.single i x) = x * x

theorem Q60596.Q'_zero_under_ideal (v : Fin 3 → Q60596.K) (hv : v ∈ LinearMap.ker Q60596.lFunc) : Q60596.Q' v = 0

def Q60596.Q : QuadraticForm Q60596.K Q60596.L

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

Equations

• Q60596.Q = QuadraticMap.ofPolar (fun (x : Q60596.L) => Quotient.liftOn' x (⇑Q60596.Q') Q60596.Q.proof_1) Q60596.Q.proof_2 Q60596.Q.proof_3 Q60596.Q.proof_4

@[simp]

theorem Q60596.Q_apply (x : Q60596.L) : Q60596.Q x = Quotient.liftOn' x (⇑Q60596.Q') Q60596.Q.proof_1

def Q60596.gen (i : Fin 3) : CliffordAlgebra Q60596.Q

Basis vectors in the Clifford algebra

Equations

• Q60596.gen i = (CliffordAlgebra.ι Q60596.Q) (Submodule.Quotient.mk (Pi.single i 1))

@[simp]

theorem Q60596.gen_mul_gen (i : Fin 3) : Q60596.gen i * Q60596.gen i = 1

The basis vectors square to one

theorem Q60596.quot_obv : Q60596.K.gen 0 • Q60596.gen 0 - Q60596.K.gen 1 • Q60596.gen 1 - Q60596.K.gen 2 • Q60596.gen 2 = 0

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

theorem Q60596.αβγ_smul_eq_zero : (Q60596.K.gen 0 * Q60596.K.gen 1 * Q60596.K.gen 2) • 1 = 0

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

theorem Q60596.algebraMap_αβγ_eq_zero : (algebraMap Q60596.K (CliffordAlgebra Q60596.Q)) (Q60596.K.gen 0 * Q60596.K.gen 1 * Q60596.K.gen 2) = 0

theorem Q60596.algebraMap_not_injective : ¬Function.Injective ⇑(algebraMap Q60596.K (CliffordAlgebra Q60596.Q))

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 Q60596.Q_not_in_range_toQuadraticForm : Q60596.Q ∉ Set.range LinearMap.BilinMap.toQuadraticMap

Bonus counterexample: Q is a quadratic form that has no bilinear form.

theorem CliffordAlgebra.not_forall_algebraMap_injective : ¬∀ (R : Type) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (Q : QuadraticForm R M), Function.Injective ⇑(algebraMap R (CliffordAlgebra Q))

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

theorem BilinMap.not_forall_toQuadraticMap_surjective : ¬∀ (R : Type) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M], Function.Surjective LinearMap.BilinMap.toQuadraticMap

The general bonus statement: not every quadratic form is the diagonal of a bilinear form.