Timeline for Clifford PBW theorem for quadratic form
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 15 at 21:27 | comment | added | Eric | (unfortunately the above link is broken, it's now at leanprover-community.github.io/mathlib4_docs/Counterexamples/…) | |
| Jan 12 at 11:08 | comment | added | Eric | "If someone could check the below I'd be very indebted.": just a final update; this is now fully formalized at leanprover-community.github.io/mathlib4_docs/Counterexamples/… | |
| Nov 22, 2021 at 17:55 | comment | added | Eric | Ah, I see the approach; multiply by $\beta\gamma$ to get $\alpha\beta\gamma a = 0$, which means $a$ must contain no scalar terms. | |
| Nov 22, 2021 at 17:19 | comment | added | Eric | Coming back to this; what approach is being used in "This map q is easily seen to be well-defined"? I get to the point where I need to show $αa - βb - γc = 0$ implies $a^2 + b^2 + c^2 = 0$, but can't see an "easy" way to proceed short of working under the quotient and trying all 8 monomials for each of a, b, and c. Am I missing something? | |
| Jan 15, 2021 at 14:37 | comment | added | darij grinberg | @Eric $\alpha \beta \gamma$ is not $0$ in $k$, only in $\operatorname{Cl}\left(L, q\right)$. The slickest way to prove that $\alpha \beta \gamma$ is not $0$ in $k$ is probably to define an $\mathbb F_2$-algebra homomorphism from $k$ to the matrix ring $\mathbb F_2^{8\times 8}$ that sends $\alpha, \beta, \gamma$ to three commuting nilpotent matrices whose product is not $0$. I'll let you find these matrices (hint: Kronecker product). | |
| Jan 15, 2021 at 13:58 | comment | added | Eric | Thanks, that clears things up - I was able to formalize this all the way up to proving that $\alpha\beta\gamma = 0$ in $k$, which I think is mostly due to a shortage of tools in my toolbox or lack of knowledge of how to use them! | |
| Jan 14, 2021 at 20:17 | comment | added | darij grinberg | @Eric My $\cdot$ is just multiplication in the Clifford algebra (which is defined as a quotient of the tensor algebra by an ideal). | |
| Jan 14, 2021 at 18:43 | comment | added | Eric | I'm attempting to formalize this, but I'm a little concerned by your use of $\cdot$ - it appears you're defining it as $x \cdot y = \frac{1}{2} (q(x + y) - q(x) - q(y))$, but doesn't the factor of 2 require that $k$ is not of characteristic 2, which as I understand it it is? | |
| Feb 9, 2012 at 3:49 | history | edited | darij grinberg | CC BY-SA 3.0 |
added 58 characters in body
|
| Feb 9, 2012 at 3:45 | vote | accept | darij grinberg | ||
| Feb 9, 2012 at 3:44 | history | answered | darij grinberg | CC BY-SA 3.0 |