noncommutative polynomials

Stream: general

[Scott Morrison]

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

[Scott Morrison]

The two obstacles to me starting are:

1. I know @Yury G. Kudryashov has had plans to refactor this file, and I don't want to have two concurrent refactors going
2. 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]

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]

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

[Scott Morrison]

no problem!

[Scott Morrison]

Do you have a suggestion for how to handle C?

[Scott Morrison]

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]

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

[Yury G. Kudryashov]

This makes sense without algebra structure.

[Scott Morrison]

I want to see if I have this right.

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

1. R is a comm_ring,
2. A is a ring, and
3. we've chosen an f : R →+* A
4. 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:

1. R is a comm_ring,
2. A is a ring, and
3. we've chosen an f : R →+* A
4. with the additional property that f r * a = a * f r
5. separately, has_scalar R A
6. 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:

1. R is a ring,
2. A is a ring, and
3. we've chosen an f : R →+* A
4. separately, has_scalar R A
5. 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]

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.)

[Scott Morrison]

What should they be called?

[Scott Morrison]

OTOH, it seems that no one actually used the fact that we had set up polynomial.C as an alg_hom.

[Scott Morrison]

Downgrading it to a ring_hom causes a few easily fixable breakages.

[Scott Morrison]

So I think I'm going to proceed just on this basis.

[Scott Morrison]

and see if we run into any trouble warranting not-a-algebras later. :-)

[Yury G. Kudryashov]

I did not suggest introducing not-a-algebras, only using mul_semiring_action_hom instead of alg_homs everywhere.

[Yury G. Kudryashov]

(and probably distrib_mul_action_homs instead of linear_maps)

[Yury G. Kudryashov]

But go ahead with C : R →+* polynomial R, we can easily change this later.

[Scott Morrison]

It looks like it's going well just with a ring_hom.

[Scott Morrison]

#3193

[Scott Morrison]

It was not as bad as I feared!

[Johan Commelin]

Scott Morrison said:

OTOH, it seems that no one actually used the fact that we had set up polynomial.C as an alg_hom.

I think that's because it's a very recent change.