Exterior algebras over semiring

Stream: maths

[Eric Wieser]

I'd like to redefine docs#exterior_algebra to be clifford_algebra 0, as that avoids having to transfer across lots of results tediously.

Unfortunately, strictly speaking docs#exterior_algebra is more general as it operates over a semiring and add_comm_monoid, unlike docs#clifford_algebra which requires negation due to the way docs#quadratic_form.polar is defined.

As I see it, I have three options:

1. Declare that exterior_algebra over a semiring is nonsense, and throw away the extra generality we currently have
2. Change the Q : quadratic_form R M in clifford_algebra to Q : M → R, and let clifford_algebra refer to semirings too. Surprisingly this works, but it creates awful elaboration problems because the elaborator is eager to perform higher-order unification on Q now that its a function.
3. Leave thing as separate definitions, and transfer things across docs#clifford_algebra.as_exterior

Is option 1 reasonable?

[Patrick Massot]

The differential geometer in me thinks that option one is super reasonable, but I'm cautious. Formalized math taught me that semirings and semimodules are actually useful...

[Adam Topaz]

does the polar form actually appear in the definition of the Clifford algebra?

[Eric Wieser]

It appears in the definition of quadratic_form

[Kevin Buzzard]

The commutative ring theorist in me feels the same as Patrick -- I have books with entire chapters talking about exterior algebras and Koszul complexes etc and they never once mention semirings. Patrick you pointed out the semiring of ideals of a commutative ring when I suggested that semirings were a complete waste of time; nat is also an example which comes up. Maybe nat is the most promising option here -- do we ever wedge over nat? I don't know any examples.

[Eric Wieser]

Perhaps also worth noting that docs#ideal.quotient doesn't work over semirings, but docs#ring_quot does (which is how both exterior and clifford algebras are defined). Are we sure the latter does something sensible in the semiring case?

[Adam Topaz]

Oh, so the definition of a quadratic form should be changed!

[Eric Wieser]

Adam Topaz said:

Oh, so the definition of a quadratic form should be changed!

What to?

[Eric Wieser]

I couldn't find a reference for an alternative definition that didn't seem to ignore characteristic two

[Kevin Buzzard]

Many people do ignore char 2 when doing quadratic forms, but I remember an algebraist once going through the theory explaining how it can be made to work.

[Adam Topaz]

In the equations in the def of a quadratic form involving the polar form, we can just move everything involving a subtraction from one side of the equality to the other.

[Eric Wieser]

Kevin Buzzard said:

Many people do ignore char 2 when doing quadratic forms, but I remember an algebraist once going through the theory explaining how it can be made to work.

If we're going to ignore char 2 then I may as well just change clifford_algebra to take a bilinear form

[Eric Wieser]

Which frankly seems to work out better for all the things I care about (namely the module isomorphism with the exterior algebra following the writeup by @Darij Grinberg, which I have sorry-free), but aligns with a minority of the literature

[Kevin Buzzard]

I remember who the algebraist was -- I'll drop them an email and see if they have any comments.

[Adam Topaz]

There's a book by Elman, Merkurjev and Karpenko
https://bookstore.ams.org/coll-56

I'm fairly sure this deals with the characteristic 2 case as well...
Unfortunately, my university's library proxy won't let me access a PDF (even though one of the authors is in my department!)

[Eric Wieser]

Eric Wieser said:

but it creates awful elaboration problems because the elaborator is eager to perform higher-order unification on Q now that its a function.

Actually it seems that def has this cursed behavior of not deciding what type its going to use until it sees your implementation; so maybe option 2 is perfectly viable

[Reid Barton]

Eric Wieser said:

Perhaps also worth noting that docs#ideal.quotient doesn't work over semirings, but docs#ring_quot does (which is how both exterior and clifford algebras are defined). Are we sure the latter does something sensible in the semiring case?

Any algebraic theory has a well-behaved theory of quotients by congruences but only for things like [additive] groups do those congruences have a description in terms of [normal] subgroups/ideals

[Damiano Testa]

I would personally be a little sad if quadratic forms were not defined in characteristic 2.

[Eric Wieser]

Adam Topaz said:

In the equations in the def of a quadratic form involving the polar form, we can just move everything involving a subtraction from one side of the equality to the other.

I started having a go at this but decided it would be easier to do some cleanup first: #14246

[Kevin Buzzard]

From Liebeck, Martin W
Yes, that’s right, Clifford algebras are just fine and dandy in characteristic 2.
I learned all this stuff ages ago from Chevalley’s little book “The algebraic theory of spinors”,
but I can’t seem to get hold of it electronically.

[Reid Barton]

Speaking purely hypothetically of course, one could probably find it online in the usual places.

[Violeta Hernández]

A certain Library that rhymes with "Nemesis" has the book

[Eric Wieser]

To be clear, my comment wasn't really about whether the quadratic Clifford algebra is well-defined over characteristic two, but rather observing that some sources claim a different definition in terms of bilinear forms is more "useful". The two definitions are equivalent in other characteristics. Either way, thanks for the reference, I'll check it out soon

[Eric Wieser]

Eric Wieser said:

Adam Topaz said:

In the equations in the def of a quadratic form involving the polar form, we can just move everything involving a subtraction from one side of the equality to the other.

I started having a go at this but decided it would be easier to do some cleanup first: #14246

#14303 is the result; although the diff will be hard to read until the dependencies are resolved.

[Eric Wieser]

The dependencies are all resolved, and I found a nicer generalization of quadratic_form following https://www.sciencedirect.com/science/article/pii/S0022404915001589, as:

structure quadratic_form (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] :=
(to_fun : M → R)
(to_fun_smul : ∀ (a : R) (x : M), to_fun (a • x) = a * a * to_fun x)
(exists_companion' : ∃ B : bilin_form R M, ∀ x y, to_fun (x + y) = to_fun x + to_fun y + B x y)

[Eric Wieser]

@Adam Topaz, do you think you have time to look at #14303?

[Adam Topaz]

Sorry! I've been meaning to look it over but got bogged down with some LTE stuff... I'll try to take a look tomorrow.

[Eric Wieser]

Thanks!

[Eric Wieser]

Somehow that review slipped through my inbox!

[Eric Wieser]

So a status update from the original post; docs#quadratic_form now is defined on semirings, and I even found a reference that used this version of quadratic forms on the tropical semiring (linked in the docs). In #14350, I change the definition of docs#clifford_algebra to use semiring instead of ring, which largely just adds some annoying variable juggling and some unification issues that require annotations or @ to solve. It's not clear to me whether this is a good idea to merge.

To recap, the motivation for this is _not_ that I care about semirings; nor do I even know if there's anyone at all who does. it's that I want to makeexterior_algebra R M defeq to clifford_algebra 0. This requires either adding unusual and performance-impacting generalizations to clifford_algebra, or making exterior_algebra less general. What are people's opinions?

[Eric Wieser]

/poll should exterior_algebra and clifford_algebra support semirings?

• Yes. Even if we don't have a reference of it being useful, we should make the generalization because mathlib allows us to.
• No. A future generalization that no one currently needs is not worth fighting elaboration problems before they need it
• No. The generalization is mathematically unfounded.

[Eric Wieser]

(For those voting for the unfounded option; the reason mathlib allows it is because docs#ring_quot uses a congruence relation instead of a quotient by an ideal, and the two notions happen to coincide when negation is available. All the literature seems to phrase things in terms of ideals though)

[Adam Topaz]

Yeah I'm curios why people are saying that it's mathematically unfounded. What's the issue?

[Adam Topaz]

It's the free algebra on a semimodule M satisfying x * x = 0 for all x : M.

[Eric Wieser]

What's a bit weird is that0 = (x+y)^2 = x^2 + y ^2 + x * y + y * x = 0 + 0 + x * y + y * x = x * y + y * x, yet we can't write x * y = -y * x

[Adam Topaz]

But we can write $x * y + y * x = 0$

[Kalle Kytölä]

I was just going to note that my vote for the very strongly worded option "the generalization is mathematically unfounded" was because it matches my mental picture of what the exterior algebra and the Clifford algebra are meant to do mathematically (which is more specific than Adam's description of these above). By contrast, the second option seemed rather cautiously worded for this. I therefore shared my vote between the two. I was also going to say I am willing to be persuaded to back off of the "mathematically unfounded" position. I'll think a bit more about Adam's argument above.

[Adam Topaz]

I guess one issue is this: If $R$ is a semiring, what is, say, $\wedge^2(R^2)$?

[Adam Topaz]

If $e_1,e_2$ denote the standard basis, then all we know $e_1 \wedge e_2 + e_2 \wedge e_1 = 0$, but of course we can't write $e_1 \wedge e_2 = - e_2 \wedge e_1$.

[Adam Topaz]

I'm sure someone somewhere out there gave some thoughts to determinants over semirings....

[Kalle Kytölä]

Ok, I think I will withdraw my vote for the strong phrasing. It has certainly happened to me before that properties that I consider essential can be replaced by something else that makes sense in more generality and turn out to be fruitful. I guess the more cautiously worded option is better, although I currently believe the semiring-generality of exterior algebras and Clifford algebras is unnecessary (of not necessarily "unfounded").

[Kevin Buzzard]

I think the way it works is that sometimes you have to let go. I've done lots of tinkering around with group cohomology and on one of those tinkers I let G be a monoid and let A be an additive monoid and saw how far I could get, with group cohomology, and you very quickly realise that you're not really getting anywhere unless A is abelian and has a neg because you can't do any of the alternating sums involved in the differentials. We all agree that mathematicians give up with monoids too early and Patrick always reminds me that ideals of a Dedekind domain are a commutative semiring, but I'm pretty sure they're not a Clifford algebra.

[Patrick Massot]

You don't need a Dedeking domain. Any commutative ring will do.

[Kevin Buzzard]

Sure but ideals of a Dedekind domain are definitely interesting.

[Eric Wieser]

You also don't need ideals, submodules of any module algebra will do :)

[Eric Wieser]

Which makes me wonder whether there's any sensible interpretation to exterior_algebra R (submodule R M), which as far as I can tell is technically permitted by the current definition

[Eric Wieser]

Eric Wieser said:

/poll should exterior_algebra and clifford_algebra support semirings?

The vote feels fairly unanimous to me; I've gone ahead and removed support for semirings from exterior_algebra in #14819