feat(algebra/algebra/non_unital): define non-unital, non-associative algebras

[ocfnash]

With sufficient refactoring effort, the non_unital_non_assoc_algebra proposed here could replace our extant algebra definition entirely. This would have the advantage that whether we wish to specialize to unital / associative algebras would then be controlled entirely by whether we pass a non_assoc_semiring / non_unital_semiring / ... as the unbundled typeclass.

The extant algebra definition uses both the existence of units and associativity. However the path to remove its dependence on associativity looks fairly easy since this arises through the redundant requirement of associativity in ring_hom (via monoid_hom) in the usual way: an overly proscriptive typeclass. I actually explored relaxing this (i.e., changing [monoid M] to [has_mul M] [has_one M] in the definition of monoid_hom) but I quickly ran into difficulties associated with to_additive magic.

I also experimented with using the mul_one_class and add_zero_class in the definitions of monoid and add_monoid and ran into trouble. However I think this could be resolved fairly easily. It's just a slow debug loop because of the long build time. Since the gain from such a change is negligible I gave up.

Co-authored-by: Eric Wieser wieser.eric@gmail.com

---

For what it's worth, I'm defining these with the following plan in mind:

1. Define non-unital, non-assoc algebras
2. Construct the magma algebra (I claim this needs non-unital, non-assoc algebras to define universal property conveniently)
3. Construct the free non-associative algebra as the magma algebra of the free magma
4. Construct the free Lie algebra as a quotient of the free non-associative algebra
5. Construct the semisimple Lie algebras as quotients of the free Lie algebra using the Serre-Chevalley construction (with relations defined by their Cartan matrices)
6. Define the exceptional Lie algebras via the Cartan matrices

There is now a branch replace_algebra_def that builds off this PR and attempts to replace the definition of algebra as described. It is still incomplete.

• depends on: [Merged by Bors] - feat(algebra/ring/basic): define non-unital, non-associative rings #6786

[ocfnash]

Looking very likely I'll close this PR eventually. In particular see #6723 (comment)

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(algebra/ring/basic): define non-unital, non-associative rings #6786

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[eric-wieser]

Do you think it's worth merging the latest master into this anyway to see what's left, or not?

[eric-wieser]

I think this made it into a zulip message, but is worth recording in this PR too: these two conditions are respectively [is_scalar_tower R A A] and (modulo symmetry) [smul_comm_class R A A].

[eric-wieser]

At least, it would be if we added has_mul.to_has_scalar, since monoid.to_mul_action can't apply here

[ocfnash]

Yep, hadn't forgotten but good to get this reminder.

[ocfnash]

I just might take advantage of this approach so I'll record the following snippet for emphasis:

import linear_algebra.basic

variables (R A : Type*) [semiring R] [non_unital_non_assoc_semiring A] [module R A]
variables (t : R) (a b : A)

example [smul_comm_class R A A] : a * (t • b) = t • (a * b) := (smul_comm t a b).symm

example [is_scalar_tower R A A] : (t • a) * b = t • (a * b) := smul_assoc t a b

Incidentally, the scalar action of A on itself is obtained from the combination of:

• non_unital_non_assoc_semiring.to_mul_zero_class
• mul_zero_class.to_smul_with_zero
• smul_with_zero.to_has_scalar

[eric-wieser]

I forgot that smul_with_zero.to_has_scalar applied here!

[kbuzzard]

Wait -- so doesn't this just mean that either one doesn't need the class at all, or that one can just make the class by extending other classes?

We had this sort of thing with number fields too --

import linear_algebra.finite_dimensional

variables (K : Type*) [field K] [char_zero K] [finite_dimensional ℚ K]

is mathematically "let K be a number field" so now you start wondering whether you even need a number field typeclass (and indeed I don't think we have one)

[ocfnash]

Exactly right! Hence my remark at the top of #7847 about it being a plausible replacement for this class.

[ocfnash]

(although we do face the problem of "exponential term size" if we go too far this way)

[ocfnash]

Do you think it's worth merging the latest master into this anyway to see what's left, or not?

Sure, I'll merge master in now since there's still a small chance I'll want this. My goal is to construct the free Lie algebras and I see my current options as one of the following:

1. Directly construct free Lie algebras using inductive and not as a quotient of the free non-assoc, non-unital algebra (i.e., the magma algebra of the free magma).
2. Introduce the non_unital_non_assoc_algebra class here and use it to construct the quotient I need (i.e., what I proposed in feat(algebra/lie/free): construction of free Lie algebras #6723),
3. Refactor our existing algebra class and so obviate the need for non_unital_non_assoc_algebra,
4. Avoid the non_unital_non_assoc_algebra vs algebra issue entirely but constructing just the free Lie ring, and then extending scalars at the very end to get the free Lie algebra.

Obviously 3 is the best solution but I'm reluctant to take it on for now. I'm going to see if I can get 4 to work neatly before I make a call on which option I'll take.

cc @kbuzzard in case you're interested!

[kbuzzard]

This looks fine to me, but I am not an expert in the subtleties of these things. I've left a couple of other comments.

[kbuzzard]

Wait -- so doesn't this just mean that either one doesn't need the class at all, or that one can just make the class by extending other classes?

We had this sort of thing with number fields too --

import linear_algebra.finite_dimensional

variables (K : Type*) [field K] [char_zero K] [finite_dimensional ℚ K]

is mathematically "let K be a number field" so now you start wondering whether you even need a number field typeclass (and indeed I don't think we have one)

[kbuzzard]

Often the point of having a primed field in a structure and an unprimed one directly afterwards is that the unprimed one can take advantage of things like coercions (e.g. it can refer to ⇑f rather than f.to_fun) but here it seems to me that the primed and unprimed versions are exactly the same even up to the binders. Is it clear that we need the primed ones?

[ocfnash]

Agreed. Fortunately this PR is (hopefully) going to be closed in favour of #7847 so this detail can be forgotten. It's old and I'd guess I wrote it before I understood this convention.

[ocfnash]

Closing this in favour of alternative approach where we declare a non_unital_non_assoc_algebra as follows:

import algebra.module.basic

variables {R A : Type*}
variables [semiring R] [non_unital_non_assoc_semiring A] [module R A]
variables [is_scalar_tower R A A] [smul_comm_class R A A]

and where we use non_unital_alg_hom (introduced in #7863) for morphisms.

This has the disadvantage that we have larger term sizes (we need [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] instead of just a single type class) but the great advantage that we do not need to define a new algebra class, especially since it would awkwardly compete with algebra.