# Zulip Chat Archive

## Stream: general

### Topic: finsupp.has_scalar

#### Johan Commelin (Mar 16 2021 at 19:11):

In LTE I'm hitting goals of the form

```
smul_with_zero.to_has_scalar = finsupp.has_scalar
```

Should docs#finsupp.has_scalar be removed, now that we have `smul_with_zero`

?

#### Eric Wieser (Mar 16 2021 at 19:22):

Those don't really sound interchangable to me

#### Eric Wieser (Mar 16 2021 at 19:23):

Does refl not close that?

#### Eric Wieser (Mar 16 2021 at 19:23):

Ah, but the typeclass argument on that instance should now be relaxed from semimodule to smul_with_zero

#### Johan Commelin (Mar 16 2021 at 19:27):

`refl`

doesn't have the slightest intention of closing this goal :sad:

#### Johan Commelin (Mar 16 2021 at 19:29):

If you are interested in seeing where these come from, see `polyhedral_lattice/finsupp.lean`

in the `polyhedral-basis`

branch of LTE

#### Eric Wieser (Mar 16 2021 at 19:34):

Would you mind showing it with pp.all?

#### Eric Wieser (Mar 16 2021 at 19:34):

Sorry, just pp.implicit is enough

#### Johan Commelin (Mar 16 2021 at 19:40):

Voila:

```
@smul_with_zero.to_has_scalar ℕ (ι →₀ Λ)
(@add_monoid.to_has_zero (ι →₀ Λ)
(@add_comm_monoid.to_add_monoid (ι →₀ Λ)
(@add_comm_group.to_add_comm_monoid (ι →₀ Λ)
(@normed_group.to_add_comm_group (ι →₀ Λ) (@finsupp.normed_group ι Λ _inst_3 _inst_2)))))
(@mul_zero_class.to_has_zero ℕ
(@monoid_with_zero.to_mul_zero_class ℕ (@semiring.to_monoid_with_zero ℕ nat.semiring)))
(@mul_action_with_zero.to_smul_with_zero ℕ (ι →₀ Λ)
(@add_monoid.to_has_zero (ι →₀ Λ)
(@add_comm_monoid.to_add_monoid (ι →₀ Λ)
(@add_comm_group.to_add_comm_monoid (ι →₀ Λ)
(@normed_group.to_add_comm_group (ι →₀ Λ) (@finsupp.normed_group ι Λ _inst_3 _inst_2)))))
(@semiring.to_monoid_with_zero ℕ nat.semiring)
(@semimodule.to_mul_action_with_zero ℕ (ι →₀ Λ) nat.semiring
(@add_comm_group.to_add_comm_monoid (ι →₀ Λ)
(@normed_group.to_add_comm_group (ι →₀ Λ) (@finsupp.normed_group ι Λ _inst_3 _inst_2)))
(@add_comm_monoid.nat_semimodule (ι →₀ Λ)
(@add_comm_group.to_add_comm_monoid (ι →₀ Λ)
(@normed_group.to_add_comm_group (ι →₀ Λ) (@finsupp.normed_group ι Λ _inst_3 _inst_2)))))) =
@finsupp.has_scalar ι Λ ℕ nat.semiring
(@add_comm_group.to_add_comm_monoid Λ (@normed_group.to_add_comm_group Λ (@to_normed_group Λ _inst_2)))
(@add_comm_monoid.nat_semimodule Λ
(@add_comm_group.to_add_comm_monoid Λ (@normed_group.to_add_comm_group Λ (@to_normed_group Λ _inst_2))))
```

#### Johan Commelin (Mar 16 2021 at 19:40):

~~ouch... lean could do a better job at linebreaks )-;~~ there, that looks better

#### Eric Wieser (Mar 16 2021 at 19:46):

nat_semimodule is the culprit here

#### Eric Wieser (Mar 16 2021 at 19:49):

Every "compound" type built out of additive monoids gets two nat-module structures; one elementwise (as this is how all other semimodule structures are inherited), and one derived from addition (which itself is elementwise)

#### Eric Wieser (Mar 16 2021 at 19:49):

These are rarely defeq

#### Johan Commelin (Mar 16 2021 at 19:51):

So we should kill the one coming from addition, right?

#### Eric Wieser (Mar 16 2021 at 19:52):

I'm beginning to think so

#### Eric Wieser (Mar 16 2021 at 19:52):

Or put it in a locale at least

#### Johan Commelin (Mar 16 2021 at 19:52):

Maybe that just shouldn't be a global instance

#### Johan Commelin (Mar 16 2021 at 19:52):

exactly

#### Eric Wieser (Mar 16 2021 at 19:52):

Along with the one for int and rat

#### Eric Wieser (Mar 16 2021 at 19:52):

And the algebras for the same

#### Eric Wieser (Mar 16 2021 at 19:53):

But a lot of lemmas will then need to assume `[semimodule \N M]`

, which you could argue is mathematically redundant

#### Johan Commelin (Mar 16 2021 at 19:53):

Well... will it really be a lot?

#### Eric Wieser (Mar 16 2021 at 19:55):

I'm less concerned about the cost of changing them, and more concerned about mathematicians thinking "this is stupid, why am I telling lean my additive monoid had a nat-module structure" and being told "it's an implementation detail"

#### Eric Wieser (Mar 16 2021 at 19:57):

It's all a bit annoying, because we have a proof that all these structures are equivalent, but it's not enough unless they're also defeq

#### Johan Commelin (Mar 16 2021 at 20:06):

Well, at least for `semimodule nat M`

we know it's a subsingleton.

#### Johan Commelin (Mar 16 2021 at 20:07):

But for `has_scalar nat M`

that's obviously not true.

#### Eric Wieser (Mar 16 2021 at 20:08):

Right, but I think in this case both instances are derived from semimodules, and somehow lean can't see that?

#### Johan Commelin (Mar 16 2021 at 20:11):

`finsupp.has_scalar`

is not projecting out of a semimodule instance on `finsupp`

, right?

#### Eric Wieser (Mar 16 2021 at 20:16):

Hmm, good point; the "project out of semimodule" path is lower priority

#### Sebastien Gouezel (Mar 16 2021 at 20:22):

What happens if you lower a lot the piority of the bad nat semimodule instance (setting it to 10 or whatever)?

#### Eric Wieser (Mar 16 2021 at 20:31):

I suspect there are few if any situations where that would actually help

#### Eric Wieser (Mar 16 2021 at 20:32):

But it wouldn't do any harm

#### Sebastien Gouezel (Mar 16 2021 at 20:33):

Normally, it means that the other instances should be found before, so I am curious what this gives in Johan's specific situation.

#### Eric Wieser (Mar 16 2021 at 20:56):

In my experience the usual cause is using nat's smul in a lemma statement about a general M, which has no other instances so chooses `nat.semimodule`

, but then applying it to a compound type like `M := prod N P`

which has a different instance.

#### Sebastien Gouezel (Mar 16 2021 at 21:15):

Does this mean that, just like for `[decidable ...]`

, we should just assume `[semimodule \N E]`

in the lemmas that mention some nat multiplication. But the user is still free to use the nsmul multiplication if he likes.

#### Eric Wieser (Mar 16 2021 at 21:23):

Yes, that's what I'm thinking

#### Eric Wieser (Mar 16 2021 at 21:23):

At which point, we may as well just hide the global instance behind a locale

#### Johan Commelin (Mar 17 2021 at 06:57):

```
local attribute [-instance] add_comm_monoid.nat_semimodule add_comm_group.int_module
```

solves all the issues

#### Johan Commelin (Mar 17 2021 at 06:58):

But now I do use the following definition:

```
class polyhedral_lattice (Λ : Type*) extends normed_group Λ :=
-- unfortunately, we need the following assumptions, for technical reasons
[nat_semimodule : semimodule ℕ Λ]
[int_semimodule : semimodule ℤ Λ]
[is_scalar_tower : is_scalar_tower ℕ ℤ Λ]
-- now we get to the actual definition
(finite_free : finite_free Λ)
(polyhedral [] : ∃ (ι : Type) [fintype ι] (l : ι → Λ), generates_norm l)
```

#### Johan Commelin (Mar 17 2021 at 06:58):

Which seems slightly awkward

#### Johan Commelin (Mar 17 2021 at 07:13):

There is now just one place at the API boundary where I need

```
have ffΛ : finite_free Λ := polyhedral_lattice.finite_free,
have oops : @polyhedral_lattice.int_semimodule Λ _ = @add_comm_group.int_module Λ _,
{ exact subsingleton.elim _ _ },
rw oops at ffΛ,
```

#### Johan Commelin (Mar 17 2021 at 07:13):

So with a more principled refactor, I guess those could also be removed

#### Eric Wieser (Mar 17 2021 at 07:25):

Shouldn't those be arguments not fields?

#### Johan Commelin (Mar 17 2021 at 07:27):

Then I can't use `bundled`

to build the category

#### Eric Wieser (Mar 17 2021 at 07:27):

How do we bundle things like modules and algebras today, which also take multiple arguments?

#### Johan Commelin (Mar 17 2021 at 07:28):

#### Eric Wieser (Mar 17 2021 at 07:31):

I feel like that's probably the better approach

#### Eric Wieser (Mar 17 2021 at 07:32):

But admittedly more work

Last updated: May 08 2021 at 03:17 UTC