-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(Counterexamples/CliffordAlgebra_not_injective): Some quadratic forms cannot be constructed from bilinear forms #9670
Conversation
…orms cannot be constructed from bilinear forms
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
It shouldn't be too hard to use LinearMap.toQuadraticForm instead, right? |
@@ -260,6 +264,16 @@ is not injective, as it sends the non-zero `α * β * γ` to zero. -/ | |||
theorem algebraMap_not_injective : ¬Function.Injective (algebraMap K <| CliffordAlgebra Q) := | |||
fun h => αβγ_ne_zero <| h <| by rw [algebraMap_αβγ_eq_zero, RingHom.map_zero] | |||
|
|||
/-- Bonus counterexample: `Q` is a quadratic form that has no bilinear form. -/ | |||
theorem Q_not_in_range_toQuadraticForm : Q ∉ Set.range BilinForm.toQuadraticForm := by |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It seems there is a positive result: if a quadratic form is induced by a bilinear form, then the algebraMap to the clifford algebra is injective.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Correct; this is in fact a consequence of a (trivial) generalization of equivExterior
; for now, that definition assumes Invertible (2 : R)
instead of IsInducedByBilinear Q
, as the latter does not exist as a typeclass.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
…orms cannot be constructed from bilinear forms (#9670) Turns out that this follows trivially from the previous counterexample. Perhaps there's a slicker proof that doesn't go via Clifford algebras at all, but it seemed worth recording this one anyway.
Pull request successfully merged into master. Build succeeded: |
…orms cannot be constructed from bilinear forms (#9670) Turns out that this follows trivially from the previous counterexample. Perhaps there's a slicker proof that doesn't go via Clifford algebras at all, but it seemed worth recording this one anyway.
…orms cannot be constructed from bilinear forms (#9670) Turns out that this follows trivially from the previous counterexample. Perhaps there's a slicker proof that doesn't go via Clifford algebras at all, but it seemed worth recording this one anyway.
…orms cannot be constructed from bilinear forms (#9670) Turns out that this follows trivially from the previous counterexample. Perhaps there's a slicker proof that doesn't go via Clifford algebras at all, but it seemed worth recording this one anyway.
…orms cannot be constructed from bilinear forms (#9670) Turns out that this follows trivially from the previous counterexample. Perhaps there's a slicker proof that doesn't go via Clifford algebras at all, but it seemed worth recording this one anyway.
Turns out that this follows trivially from the previous counterexample.
Perhaps there's a slicker proof that doesn't go via Clifford algebras at all, but it seemed worth recording this one anyway.