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


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.

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

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

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?

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