products of linear combinations

Stream: maths

[Johan Commelin]

If you have a comm_ring R and an algebra R A, then you can look at R-linear combinations of elements in A. Those are terms of lc R A. Of course you can naturally multiply those things, so that you get algebra R (lc R A). Also, lc.total becomes an algebra hom.
(N.b.: The multiplication on lc R A is not the multiplication on finsupp.)
I've proven these things in https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/lc_algebra.lean
What is the right place in mathlib for these facts? Should I start a new file? (If so, where?) Or should this go in linear_algebra.linear_combination?

[Johan Commelin]

#847

[Scott Morrison]

What is this for?

[Johan Commelin]

I needed this for some stuff on topological rings (part of the perfectoid project).

[Johan Commelin]

It's a natural thing to do, right?

[Johan Commelin]

In particular, I needed the mul_support theorem.

[Scott Morrison]

It feels like a strange construction. It seems you're using much less than that A is an R-algebra here. Is it just that A needs to be a monoid, and then lc R A is an algebra?

[Johan Commelin]

lc R A needs that A is an R-module.

[Johan Commelin]

So if you have a monoid in R-modules...

[Scott Morrison]

I'm confused, sorry, why does lc R A need that A is an R-module? I thought it was just formal R-linear combinations of terms in A.

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/b39d6d8a502edfb5adb3026c256c82bea526328b/src/linear_algebra/linear_combination.lean#L18

[Johan Commelin]

@Scott Morrison I guess there is a lot of linear algebra that can be generalised.

[Scott Morrison]

I guess I've never looked at lc before... :-)

[Scott Morrison]

That's so weird that they put [add_comm_group β] [module α β] in the requirements for lc, right from the beginning.

[Scott Morrison]

It's like lc doesn't mean "formal linear combinations", which is what I'd always assumed, but "not-yet -added-up linear expressions in a module"

[Johan Commelin]

Yup...

[Scott Morrison]

.... ugh?

[Johan Commelin]

I guess this might be the first time you need the assumption: https://github.com/leanprover-community/mathlib/blob/b39d6d8a502edfb5adb3026c256c82bea526328b/src/linear_algebra/linear_combination.lean#L142

[Scott Morrison]

but then much of the rest of the file doesn't need such strong assumptions again

[Johan Commelin]

I'm willing to invest time in refactoring the algebraic hierarchy... but it will need to be streamlined. Currently PR's are opened faster than they are merged.