Zulip Chat Archive

Stream: Is there code for X?

Topic: An add_monoid_hom is a linear_map ℤ


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:25):

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

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Dec 07 2020 at 15:30):

Probably because it's given by an instance has_zero, not a proper def.

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:37):

docs#add_monoid_hom.to_int_linear_map

view this post on Zulip 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

view this post on Zulip Adam Topaz (Dec 07 2020 at 15:40):

imports?

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:40):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Dec 07 2020 at 15:45):

It's the fact that R is a semiring and not a ring.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:45):

But add_monoid_hom.to_int_linear_map doesn't even take R as an argument!

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:48):

Ah, I see the problem

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:48):

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

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:48):

Which it shouldn't, right?

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Dec 07 2020 at 15:49):

But I guess mathlib doesn't know this?

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:51):

docs#tensor_product.add_comm_group

view this post on Zulip Adam Topaz (Dec 07 2020 at 15:52):

Right, so notice the comm_ring R assumption

view this post on Zulip Adam Topaz (Dec 07 2020 at 15:52):

I think this can be relaxed to comm_semiring

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Dec 07 2020 at 15:54):

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

view this post on Zulip Reid Barton (Dec 07 2020 at 15:54):

the definition of neg will get more complicated though

view this post on Zulip 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?

view this post on Zulip Reid Barton (Dec 07 2020 at 15:55):

yes

view this post on Zulip Reid Barton (Dec 07 2020 at 15:55):

unless you use choice I guess

view this post on Zulip 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

view this post on Zulip Reid Barton (Dec 07 2020 at 15:56):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:57):

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

view this post on Zulip Adam Topaz (Dec 07 2020 at 15:58):

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

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:58):

Yes, negation is central to what I'm doing

view this post on Zulip Reid Barton (Dec 07 2020 at 15:58):

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

view this post on Zulip Reid Barton (Dec 07 2020 at 15:58):

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

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:59):

Yeah, I was considering just assuming R is a ring

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 07 2020 at 15:59):

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

view this post on Zulip Eric Wieser (Dec 07 2020 at 16:00):

I think the reason I wanted semiring R is because M is _not_ necessarily a Z\mathbb{Z} module

view this post on Zulip Reid Barton (Dec 07 2020 at 16:01):

M?

view this post on Zulip Eric Wieser (Dec 07 2020 at 16:01):

Ah heck, you're missing the context

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Dec 07 2020 at 16:06):

Sure, the intent of the have was just to check that the instance existed

view this post on Zulip Eric Wieser (Dec 07 2020 at 16:06):

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

view this post on Zulip Reid Barton (Dec 07 2020 at 16:12):

well, here is a suggestion

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Dec 07 2020 at 16:16):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Dec 07 2020 at 16:18):

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

view this post on Zulip Adam Topaz (Dec 07 2020 at 16:19):

Actually I guess this is a good thing...

view this post on Zulip Reid Barton (Dec 07 2020 at 16:19):

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

view this post on Zulip Adam Topaz (Dec 07 2020 at 16:21):

Yeah

view this post on Zulip Adam Topaz (Dec 07 2020 at 16:21):

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

view this post on Zulip 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