Zulip Chat Archive

Stream: general

Topic: noncommutative polynomials

Scott Morrison (Jun 26 2020 at 13:17):

I would really like to generalize as much as possible of data/polynomial.lean to noncommutative rings.

Scott Morrison (Jun 26 2020 at 13:18):

The two obstacles to me starting are:

I know @Yury G. Kudryashov has had plans to refactor this file, and I don't want to have two concurrent refactors going
A lot of that file is written in terms of C : R →ₐ[R] polynomial R, expressed as an algebra hom, which won't make sense when R is noncommutative.

Scott Morrison (Jun 26 2020 at 13:19):

The minimal solution to 2. is presumably just to downgrade C to a ring_hom, maybe patching on C_alg_hom if it's needed in places.

Yury G. Kudryashov (Jun 26 2020 at 13:20):

Sorry, I got distracted by other refactors (mostly measure_theory/).

Scott Morrison (Jun 26 2020 at 13:20):

no problem!

Scott Morrison (Jun 26 2020 at 13:21):

Do you have a suggestion for how to handle C?

Scott Morrison (Jun 26 2020 at 13:22):

I'm going to head off to sleep shortly, but unless you say that you're planning on doing this soon, I might have a go at a refactor tomorrow.

Yury G. Kudryashov (Jun 26 2020 at 13:32):

Actually we might want to have alg_hom (under another name?) extending ring_hom and linear_map.

Yury G. Kudryashov (Jun 26 2020 at 13:33):

This makes sense without algebra structure.

Scott Morrison (Jun 26 2020 at 23:44):

I want to see if I have this right.

"In maths", an R-algebra A just means that

R is a comm_ring,
A is a ring, and
we've chosen an f : R →+* A
with the additional property that f r * a = a * f r (i.e. it lands in the centre) (this is the axiom commutes' in Lean).

"In Lean", we model it slightly differently! In order to allow for good definitional reduction, we say that an R-algebra A means:

R is a comm_ring,
A is a ring, and
we've chosen an f : R →+* A
with the additional property that f r * a = a * f r
separately, has_scalar R A
however there is an equation r • x = f r * x

Now, what if we want to talk about the case where R is noncommutative? "In maths", this is nothing but a ring homomorphism R →+* A between (not necessarily commutative) rings, so it doesn't get a name or a mention at all. The prototypical interesting example I want to think about is R →+* polynomial R, for non-commutative polynomials. I think what @Yury G. Kudryashov is suggesting is that we might want to have a Lean notion here, of a "not-a-algebra", defined as:

R is a ring,
A is a ring, and
we've chosen an f : R →+* A
separately, has_scalar R A
however there is an equation r • x = f r * x

I suspect (perhaps regretfully) that we do actually need this in the noncommutative polynomial case. The point is that polynomial R already has a has_scalar R (polynomial R) (just thinking of polynomial R as finsupp nat R), and then separately we give is a multiplication, and it is a theorem, rather than a definition, that r • x = f r * x.

Scott Morrison (Jun 26 2020 at 23:46):

So, if I have that right, should I begin the "make noncommutative polynomials" refactor be first introducing "not-a-algebras"? (Presumably everything about alg_hom will move to being about these gadgets; no need to make a second version.)