Zulip Chat Archive

Stream: maths

Topic: products of linear combinations


view this post on Zulip Johan Commelin (Mar 23 2019 at 19:29):

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?

view this post on Zulip Johan Commelin (Mar 25 2019 at 08:18):

#847

view this post on Zulip Scott Morrison (Mar 25 2019 at 08:52):

What is this for?

view this post on Zulip Johan Commelin (Mar 25 2019 at 08:57):

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

view this post on Zulip Johan Commelin (Mar 25 2019 at 09:01):

It's a natural thing to do, right?

view this post on Zulip Johan Commelin (Mar 25 2019 at 09:01):

In particular, I needed the mul_support theorem.

view this post on Zulip Scott Morrison (Mar 25 2019 at 09:50):

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?

view this post on Zulip Johan Commelin (Mar 25 2019 at 09:55):

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

view this post on Zulip Johan Commelin (Mar 25 2019 at 09:55):

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

view this post on Zulip Scott Morrison (Mar 25 2019 at 10:10):

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.

view this post on Zulip Johan Commelin (Mar 25 2019 at 10:13):

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

view this post on Zulip Johan Commelin (Mar 25 2019 at 10:14):

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

view this post on Zulip Scott Morrison (Mar 25 2019 at 10:15):

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

view this post on Zulip Scott Morrison (Mar 25 2019 at 10:18):

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

view this post on Zulip Scott Morrison (Mar 25 2019 at 10:20):

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"

view this post on Zulip Johan Commelin (Mar 25 2019 at 10:20):

Yup...

view this post on Zulip Scott Morrison (Mar 25 2019 at 10:20):

.... ugh?

view this post on Zulip Johan Commelin (Mar 25 2019 at 10:20):

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

view this post on Zulip Scott Morrison (Mar 25 2019 at 10:23):

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

view this post on Zulip Johan Commelin (Mar 25 2019 at 10:23):

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.


Last updated: May 11 2021 at 15:12 UTC