Documentation

Counterexamples.CliffordAlgebraNotInjective

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:

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.

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)) :
    x Q60596.kIdeal mx.support, ∃ (i : Fin 3), 2 m i

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

    Equations
    Instances For

      k has characteristic 2.

      Equations

      The generators of K.

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

        The elements above square to zero

        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) :
        Q60596.lFunc a = Q60596.K.gen 0 * a 0 + Q60596.K.gen 1 * a 1 + Q60596.K.gen 2 * 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
          @[reducible, inline]
          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} [CommRing R] (i : ι) :
            QuadraticForm R (ιR)

            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} [CommRing R] [CharP R 2] (i : ι) (a : ιR) (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 : ιR) (b : ιR) :
              (Q60596.sq i) (a - b) = (Q60596.sq i) a - (Q60596.sq i) b

              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) = Q60596.Q' x + Q60596.Q' y
                theorem Q60596.Q'_sub (x : Fin 3Q60596.K) (y : Fin 3Q60596.K) :
                Q60596.Q' (x - y) = Q60596.Q' x - Q60596.Q' y
                theorem Q60596.Q'_apply (a : Fin 3Q60596.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 3Q60596.K) (hv : v LinearMap.ker Q60596.lFunc) :
                Q60596.Q' v = 0

                Basis vectors in the Clifford algebra

                Equations
                Instances For
                  @[simp]

                  The basis vectors square to one

                  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 Q60596.Q_not_in_range_toQuadraticForm :
                  Q60596.QSet.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.