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

type mismatch at application
  a'.to_int_linear_map
term
  a'
has type
  @add_monoid_hom
    (@tensor_product R _inst_20 N N (@add_comm_group.to_add_comm_monoid N (@ring.to_add_comm_group N _inst_21))
       (@add_comm_group.to_add_comm_monoid N (@ring.to_add_comm_group N _inst_21))
       (@algebra.to_semimodule R N _inst_20 (@ring.to_semiring N _inst_21) _inst_22)
       (@algebra.to_semimodule R N _inst_20 (@ring.to_semiring N _inst_21) _inst_22))
    N
    (@add_comm_monoid.to_add_monoid
       (@tensor_product R _inst_20 N N (@semiring.to_add_comm_monoid N (@ring.to_semiring N _inst_21))
          (@semiring.to_add_comm_monoid N (@ring.to_semiring N _inst_21))
          (@algebra.to_semimodule R N _inst_20 (@ring.to_semiring N _inst_21) _inst_22)
          (@algebra.to_semimodule R N _inst_20 (@ring.to_semiring N _inst_21) _inst_22))
       (@tensor_product.add_comm_monoid R _inst_20 N N (@semiring.to_add_comm_monoid N (@ring.to_semiring N _inst_21))
          (@semiring.to_add_comm_monoid N (@ring.to_semiring N _inst_21))
          (@algebra.to_semimodule R N _inst_20 (@ring.to_semiring N _inst_21) _inst_22)
          (@algebra.to_semimodule R N _inst_20 (@ring.to_semiring N _inst_21) _inst_22)))
    (@add_group.to_add_monoid N (@add_comm_group.to_add_group N (@ring.to_add_comm_group N _inst_21)))
but is expected to have type
  @add_monoid_hom
    (@tensor_product ?m_1 ?m_2 N N (@add_comm_group.to_add_comm_monoid N (@ring.to_add_comm_group N _inst_21))
       (@add_comm_group.to_add_comm_monoid N (@ring.to_add_comm_group N _inst_21))
       ?m_3
       ?m_4)
    N
    (@add_group.to_add_monoid
       (@tensor_product ?m_1 ?m_2 N N (@add_comm_group.to_add_comm_monoid N (@ring.to_add_comm_group N _inst_21))
          (@add_comm_group.to_add_comm_monoid N (@ring.to_add_comm_group N _inst_21))
          ?m_3
          ?m_4)
       (@add_comm_group.to_add_group
          (@tensor_product ?m_1 ?m_2 N N (@add_comm_group.to_add_comm_monoid N (@ring.to_add_comm_group N _inst_21))
             (@add_comm_group.to_add_comm_monoid N (@ring.to_add_comm_group N _inst_21))
             ?m_3
             ?m_4)
          ?m_5))
    (@add_group.to_add_monoid N (@add_comm_group.to_add_group N (@ring.to_add_comm_group N _inst_21)))

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

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: Dec 20 2023 at 11:08 UTC