# Zulip Chat Archive

## Stream: maths

### Topic: products of linear combinations

#### 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`

?

#### Johan Commelin (Mar 25 2019 at 08:18):

#### Scott Morrison (Mar 25 2019 at 08:52):

What is this for?

#### Johan Commelin (Mar 25 2019 at 08:57):

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

#### Johan Commelin (Mar 25 2019 at 09:01):

It's a natural thing to do, right?

#### Johan Commelin (Mar 25 2019 at 09:01):

In particular, I needed the `mul_support`

theorem.

#### 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?

#### Johan Commelin (Mar 25 2019 at 09:55):

`lc R A`

needs that `A`

is an `R`

-module.

#### Johan Commelin (Mar 25 2019 at 09:55):

So if you have a monoid in `R`

-modules...

#### 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`

.

#### Johan Commelin (Mar 25 2019 at 10:13):

#### Johan Commelin (Mar 25 2019 at 10:14):

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

#### Scott Morrison (Mar 25 2019 at 10:15):

I guess I've never looked at `lc`

before... :-)

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

#### 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"

#### Johan Commelin (Mar 25 2019 at 10:20):

Yup...

#### Scott Morrison (Mar 25 2019 at 10:20):

.... ugh?

#### 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

#### Scott Morrison (Mar 25 2019 at 10:23):

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

#### 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