# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: An add_monoid_hom is a linear_map ℤ

#### Eric Wieser (Dec 07 2020 at 15:00):

```
example {A B : Type*} [add_comm_group A] [add_comm_group B] (f : A →+ B) : A →ₗ[ℤ] B := sorry
```

#### Sebastien Gouezel (Dec 07 2020 at 15:14):

```
example {A B : Type*} [add_comm_group A] [add_comm_group B] (f : A →+ B) : A →ₗ[ℤ] B := by library_search
```

#### Sebastien Gouezel (Dec 07 2020 at 15:16):

it gives `f.to_int_linear_map`

. I gave the `library_search`

recipe to emphasize that it can be used to find data, not only proofs.

#### Adam Topaz (Dec 07 2020 at 15:18):

I'm surprised library search doesn't immediately find the "default" linear map, i.e. the trivial map.

#### Eric Wieser (Dec 07 2020 at 15:25):

Yeah, I didn't even try that because I made the same assumption as Adam

#### Sebastien Gouezel (Dec 07 2020 at 15:29):

It's true it's surprising that it doesn't give the zero map -- otherwise, `suggest`

could have been helpful, as it gives several suggestions. In fact,

```
example {A B : Type*} [add_comm_group A] [add_comm_group B] : A →ₗ[ℤ] B := by library_search
```

fails. It also doesn't find the zero map.

#### Sebastien Gouezel (Dec 07 2020 at 15:30):

Probably because it's given by an instance `has_zero`

, not a proper def.

#### Eric Wieser (Dec 07 2020 at 15:37):

docs#add_monoid_hom.to_int_linear_map

#### Eric Wieser (Dec 07 2020 at 15:38):

What's going wrong here?

```
import linear_algebra.tensor_product
import algebra.algebra.basic
example {R : Type*} {N : Type*} [comm_semiring R] [ring N] [algebra R N] : false :=
begin
let a' : N ⊗ N →+ N := (algebra.lmul' R).to_add_monoid_hom,
have : add_comm_group (N ⊗ N) := infer_instance,
have : add_comm_group N := infer_instance,
let a'' := a'.to_int_linear_map, -- fail
end
```

#### Adam Topaz (Dec 07 2020 at 15:40):

imports?

#### Eric Wieser (Dec 07 2020 at 15:40):

Not sure, let's guess `algebra.algebra.basic`

?

#### Eric Wieser (Dec 07 2020 at 15:41):

If I pass the type parameters explicitly, I get a super nasty error

```
example {ιa ιb : Type*} {R : Type*} {N : Type*} [comm_semiring R] [ring N] [algebra R N] : false :=
begin
let a' : N ⊗ N →+ N := (algebra.lmul' R).to_add_monoid_hom,
let a'' := @add_monoid_hom.to_int_linear_map (N ⊗ N) N _ _ a',
sorry,
end
```

#### Adam Topaz (Dec 07 2020 at 15:45):

It's the fact that `R`

is a semiring and not a ring.

#### Adam Topaz (Dec 07 2020 at 15:45):

```
import linear_algebra.tensor_product
import algebra
import algebra.algebra.basic
open_locale tensor_product
example {R : Type*} {N : Type*} [comm_ring R] [ring N] [algebra R N] : false :=
begin
let a' : N ⊗ N →+ N := (algebra.lmul' R).to_add_monoid_hom,
let := a'.to_int_linear_map, -- works
end
```

#### Eric Wieser (Dec 07 2020 at 15:45):

But `add_monoid_hom.to_int_linear_map`

doesn't even take `R`

as an argument!

#### Eric Wieser (Dec 07 2020 at 15:48):

Ah, I see the problem

#### Eric Wieser (Dec 07 2020 at 15:48):

`haveI : add_comm_group (N ⊗[R] N) := infer_instance,`

fails

#### Eric Wieser (Dec 07 2020 at 15:48):

Which it shouldn't, right?

#### Adam Topaz (Dec 07 2020 at 15:49):

Yeah, I think it's true that the tensor product of two semimodules over a semiring which just so happen to be abelian groups is again an abelian group.

#### Adam Topaz (Dec 07 2020 at 15:49):

But I guess mathlib doesn't know this?

#### Adam Topaz (Dec 07 2020 at 15:50):

One would have to track down where the `add_comm_group`

on the tensor product comes from.

#### Eric Wieser (Dec 07 2020 at 15:51):

docs#tensor_product.add_comm_group

#### Adam Topaz (Dec 07 2020 at 15:52):

Right, so notice the `comm_ring R`

assumption

#### Adam Topaz (Dec 07 2020 at 15:52):

I think this can be relaxed to `comm_semiring`

#### Reid Barton (Dec 07 2020 at 15:53):

you just need either side to be an `add_comm_group`

(as is basically clear from the next lines)

#### Adam Topaz (Dec 07 2020 at 15:54):

This is probably another instance of the "Mathematicians never think about semirings" thing...

#### Reid Barton (Dec 07 2020 at 15:54):

the definition of `neg`

will get more complicated though

#### Eric Wieser (Dec 07 2020 at 15:55):

Doesn't requiring just one side lead to multiple suitable instances for when both sides have neg?

#### Reid Barton (Dec 07 2020 at 15:55):

yes

#### Reid Barton (Dec 07 2020 at 15:55):

unless you use `choice`

I guess

#### Adam Topaz (Dec 07 2020 at 15:55):

The easiest thing to do is probably

```
def tensor_product.add_comm_group {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_monoid N] [semimodule R M] [semimodule R N] : add_comm_group (M ⊗ N) := sorry
```

#### Reid Barton (Dec 07 2020 at 15:56):

I mean, the instances will be non-defeq unless you define `neg`

using choice

#### Reid Barton (Dec 07 2020 at 15:57):

If your goal is to prove `false`

then it doesn't matter which definition you pick but in the real world you might care about the definition as well

#### Eric Wieser (Dec 07 2020 at 15:57):

My goal isn't to prove false, I just was cutting down my example

#### Adam Topaz (Dec 07 2020 at 15:58):

Can you get by with just a $\mathbb{N}$-linear map? Do you need negation for what you're actually working on?

#### Eric Wieser (Dec 07 2020 at 15:58):

Yes, negation is central to what I'm doing

#### Reid Barton (Dec 07 2020 at 15:58):

I'm sort of skeptical that your original setup is really sensible, since if $N$ is a ring that's an $R$-algebra then it's also an $R \otimes \mathbb{Z}$-algebra

#### Reid Barton (Dec 07 2020 at 15:58):

so wlog you could just assume $R$ is a ring too, and save yourself the headaches

#### Eric Wieser (Dec 07 2020 at 15:59):

Yeah, I was considering just assuming `R`

is a ring

#### Eric Wieser (Dec 07 2020 at 15:59):

I've ended up here because I was trying to extract some intermediate lemmas from my proof that currently just unfolds everything

#### Eric Wieser (Dec 07 2020 at 15:59):

But the intermediate states run into (semi)-issues that unfolding avoided

#### Eric Wieser (Dec 07 2020 at 16:00):

I think the reason I wanted `semiring R`

is because `M`

is _not_ necessarily a $\mathbb{Z}$ module

#### Reid Barton (Dec 07 2020 at 16:01):

M?

#### Eric Wieser (Dec 07 2020 at 16:01):

Ah heck, you're missing the context

#### Eric Wieser (Dec 07 2020 at 16:02):

```
def mul_general_aux {ιa ιb : Type*} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb]
{R : Type*} {M N : Type*}
[comm_semiring R] [ring N] [algebra R N] [add_comm_monoid M] [semimodule R M]
(a : alternating_map R M N ιa) (b : alternating_map R M N ιb) :
(ιa ⊕ ιb → M) → N := sorry
```

is where my typeclasses are coming from. I need the same `R`

for `M`

and `N`

to form the alternating_map

#### Reid Barton (Dec 07 2020 at 16:03):

I think the same logic applies, since you're mapping into N where you can subtract you might as well assume you can subtract in M too

#### Yury G. Kudryashov (Dec 07 2020 at 16:04):

Sometimes it is useful to deal with `comm_semiring R`

. E.g., it makes sense to deal with `fin n → \R`

as a semimodule over `nnreal`

. Then the `submodule.span`

is the cone generated by a set of vectors.

#### Yury G. Kudryashov (Dec 07 2020 at 16:05):

About the original example. Using `have : add_comm_group (N ⊗ N) := infer_instance`

doesn't help because Lean immediately forgets the definition behind this `have`

.

#### Eric Wieser (Dec 07 2020 at 16:06):

Sure, the intent of the `have`

was just to check that the instance existed

#### Eric Wieser (Dec 07 2020 at 16:06):

And in this case was a red herring because it didn't infer `[R]`

#### Reid Barton (Dec 07 2020 at 16:12):

well, here is a suggestion

#### Reid Barton (Dec 07 2020 at 16:13):

The current definition of `neg`

for the tensor product must actually involve multiplication by elements of R on one of the two factors

#### Reid Barton (Dec 07 2020 at 16:13):

so we could replace it by an instance that uses `neg`

for the same factor, and not have the other one

#### Reid Barton (Dec 07 2020 at 16:16):

logically I suppose it ought to be the left factor, because we have left modules

#### Adam Topaz (Dec 07 2020 at 16:16):

```
import linear_algebra.tensor_product
import algebra
import algebra.algebra.basic
open_locale tensor_product
variables {R : Type*} {N : Type*} [comm_ring R] [ring N] [algebra R N]
example {n1 n2 : N} : -((n1 ⊗ₜ n2) : N ⊗[R] N) = ((-1) • n1) ⊗ₜ n2 := rfl
```

#### Reid Barton (Dec 07 2020 at 16:17):

of course it won't be defeq to `neg n1 ⊗ₜ n2`

, but that seems relatively unlikely to cause a problem

#### Adam Topaz (Dec 07 2020 at 16:18):

I'm not so sure. E.g. `(-1) \bu n`

simplifies to `-n`

.

#### Adam Topaz (Dec 07 2020 at 16:19):

Actually I guess this is a good thing...

#### Reid Barton (Dec 07 2020 at 16:19):

Not so sure about which part? that it wouldn't be a problem?

#### Adam Topaz (Dec 07 2020 at 16:21):

Yeah

#### Adam Topaz (Dec 07 2020 at 16:21):

But it's not a problem. Forget what I said.

#### Eric Wieser (Dec 10 2020 at 13:30):

I've relaxed the requirements of docs#tensor_product.add_comm_group in #5305

Last updated: May 19 2021 at 00:40 UTC