# Zulip Chat Archive

## Stream: general

### Topic: p + q = p * q solves by refl!

#### Eric Wieser (Oct 04 2020 at 11:27):

Something seems wrong either with the pretty-printer or with type-class resolution here:

```
example {G : Type u} [add_monoid G] (p q : multiplicative G) :
(p * q) = (@has_add.add (multiplicative G) (@add_semigroup.to_has_add G (add_monoid.to_add_semigroup G))
p q) :=
begin
/-
p q : multiplicative G
⊢ p * q = p + q
-/
refl,
end
```

Obviously the RHS of my lemma is contrived, but it's what `extract_goal`

produced mid-proof

#### Eric Wieser (Oct 04 2020 at 12:08):

This lets me make a rather strange `(multiplicative G) ≃+ G`

object

```
import algebra.algebra.basic
def bad_add (G : Type) [add_monoid G] : has_add (multiplicative G) :=
(@add_semigroup.to_has_add (multiplicative G) (@add_monoid.to_add_semigroup (multiplicative G) _inst_1))
lemma bad_map_add {G : Type} [add_monoid G] (x y : multiplicative G) :
by haveI := bad_add G; exact
multiplicative.to_add x + multiplicative.to_add y = multiplicative.to_add (x + y) :=
rfl
def bad_to_add {G : Type} [add_monoid G] :
by haveI := bad_add; exact
(multiplicative G) ≃+ G :=
{add_equiv.
map_add' := λ x y, by {simp only [equiv.to_fun_as_coe, bad_map_add x y]},
..@multiplicative.to_add G
}
#check bad_to_add
```

#### Mario Carneiro (Oct 04 2020 at 12:09):

This is expected behavior

#### Eric Wieser (Oct 04 2020 at 12:10):

Would `bad_to_add`

make sense in mathlib then?

#### Eric Wieser (Oct 04 2020 at 12:10):

With a better name, obviously

#### Mario Carneiro (Oct 04 2020 at 12:10):

absolutely not

#### Eric Wieser (Oct 04 2020 at 12:10):

Perhaps some more context - I'm trying to implement `add_monoid_algebra k G ≃+* monoid_algebra k (multiplicative G)`

#### Mario Carneiro (Oct 04 2020 at 12:10):

it is pretty obviously not a desirable instance

#### Mario Carneiro (Oct 04 2020 at 12:11):

You can locally override instances, as you are doing in these examples

#### Mario Carneiro (Oct 04 2020 at 12:11):

but they cause problems down the line so you should keep it to a minimum

#### Eric Wieser (Oct 04 2020 at 12:11):

Sorry, I'm not suggesting `bad_add`

should be a global instance

#### Mario Carneiro (Oct 04 2020 at 12:11):

I don't see how that equiv makes sense

#### Mario Carneiro (Oct 04 2020 at 12:12):

are those both rings?

#### Eric Wieser (Oct 04 2020 at 12:12):

Perhaps I need to show a longer example

#### Mario Carneiro (Oct 04 2020 at 12:12):

I'm pretty sure `≃+*`

works on rings and ringish things

#### Eric Wieser (Oct 04 2020 at 12:13):

Both `add_monoid_algebra k G`

and `monoid_algebra k (multiplicative G)`

are semirings, yes

#### Eric Wieser (Oct 04 2020 at 12:15):

I was able to prove this lemma:

```
lemma add_monoid_algebra.map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [add_monoid α] [add_monoid α₂] {x y : add_monoid_algebra β α}
{f : α → α₂} (f_map_mul : ∀ x y, f x + f y = f (x + y)):
(map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) =
(map_domain f x * map_domain f y : add_monoid_algebra β α₂) := sorry
```

and I can then use it to construct the ring isomorphism as

```
def add_monoid_algebra.to_multiplicative :
add_monoid_algebra k G ≃+* monoid_algebra k (multiplicative G) :=
{ map_mul' := λ x y, by {
unfold finsupp.dom_congr,
simp,
rw map_domain_mul _,
extract_goal, -- this is where the weird goal appears
intros p q,
simp [← to_add_mul],
refl, },
map_add' := λ x y, by {
simp [finsupp.dom_congr, map_domain_add],
},
..finsupp.dom_congr multiplicative.to_add }
```

What I'd like to do is bundle `f`

and `f_map_mul`

into a `α →+ α₂`

. The `→+`

object I need is exactly `bad_to_add`

.

#### Mario Carneiro (Oct 04 2020 at 12:18):

I'm asking a more basic question, I think. What kind of object is `monoid_algebra k (multiplicative G)`

? What operations does it support?

#### Mario Carneiro (Oct 04 2020 at 12:18):

Does it have an addition and multiplication, and do they make sense

#### Eric Wieser (Oct 04 2020 at 12:19):

Perhaps it helps to note that the implementation notes for `add_monoid_algebra`

say

Similarly, I attempted to just define

`add_monoid_algebra k G := monoid_algebra k (multiplicative G)`

,

but the definitional equality`multiplicative G = G`

leaks through everywhere, and

seems impossible to use.

#### Mario Carneiro (Oct 04 2020 at 12:20):

well there you have it

#### Eric Wieser (Oct 04 2020 at 12:21):

Right - and IMO the thing that makes it impossible to use is the absence of `add_monoid_algebra.to_multiplicative`

above

#### Eric Wieser (Oct 04 2020 at 12:21):

With that in place I can (hopefully) replace all the `add_monoid_algebra`

theorems with

- Apply the iso
- use the proof for
`monoid_algebra`

#### Mario Carneiro (Oct 04 2020 at 12:21):

the problem is the defeqs are wrong

#### Eric Wieser (Oct 04 2020 at 12:22):

The problem with what and which defeqs?

#### Mario Carneiro (Oct 04 2020 at 12:22):

The iso is trivial, I guess, because they are equal objects

#### Mario Carneiro (Oct 04 2020 at 12:23):

To fix the defeqs, the definition should be changed to something like

```
def add_monoid_algebra k G :=
{ add := something reasonable,
mul := something reasonable,
..monoid_algebra k (multiplicative G) } -- use the unreasonable equalities to do the proof obligations
```

#### Eric Wieser (Oct 04 2020 at 12:24):

I don't quite get that example - today it's defined as `def add_monoid_algebra := G →₀ k`

#### Mario Carneiro (Oct 04 2020 at 12:25):

oh I see, it is not the definition

#### Mario Carneiro (Oct 04 2020 at 12:25):

and you want to recover that representation

#### Chris Hughes (Oct 04 2020 at 12:26):

The idiomatic way to use `multiplicatuve`

is to use the `to_add`

function, and others like it.

#### Eric Wieser (Oct 04 2020 at 12:26):

@Chris, which message is that in response to?

#### Mario Carneiro (Oct 04 2020 at 12:27):

somewhere in your definition is an "illegal" unfolding of `multiplicative`

#### Mario Carneiro (Oct 04 2020 at 12:28):

you could try making `multiplicative`

irreducible to see if that pinpoints the issue, but I don't have your code to test

#### Eric Wieser (Oct 04 2020 at 12:28):

@Mario Carneiro, I think what you're recommending is already what I'm planning to do:

- Keep the definition of
`add_monoid_algebra`

- Keep the definition of
`add_monoid_algebra.has_add`

- Keep the definition of
`add_monoid_algebra.has_mul`

- Transfer the ring structure of
`add_monoid_algebra`

over the isomorphism

#### Mario Carneiro (Oct 04 2020 at 12:28):

the question is whether the isomorphism itself is well typed

#### Eric Wieser (Oct 04 2020 at 12:28):

There are two isomorphism here - `bad_add_to_add`

and `monoid_algebra.to_additive`

#### Eric Wieser (Oct 04 2020 at 12:29):

The former is obviously badly typed, IMO the latter is totally safe

#### Eric Wieser (Oct 04 2020 at 12:29):

But the former is a valuable tool for building the latter

#### Mario Carneiro (Oct 04 2020 at 12:29):

A `~=+*`

isomorphism comes with the assumption that both sides have reasonable addition/multiplication structures

#### Eric Wieser (Oct 04 2020 at 12:30):

Any `to_additive`

def will inevitably perform an `illegal`

unfolding of `multiplicative`

#### Mario Carneiro (Oct 04 2020 at 12:30):

yes, but you aren't doing such a def

#### Mario Carneiro (Oct 04 2020 at 12:30):

actually I take that back, `to_additive`

does no unfolding

#### Mario Carneiro (Oct 04 2020 at 12:31):

`to_additive`

does a copy paste job

#### Mario Carneiro (Oct 04 2020 at 12:31):

so there is no leakage

#### Eric Wieser (Oct 04 2020 at 12:31):

My claim is `bad_add_to_add`

is a utility function to perform that unfolding / copy paste

#### Mario Carneiro (Oct 04 2020 at 12:31):

`bad_add`

is aptly named, because `multiplicative G`

isn't supposed to have an add

#### Mario Carneiro (Oct 04 2020 at 12:32):

and anything that contains `bad_add`

in its statement is also bad

#### Kevin Buzzard (Oct 04 2020 at 12:33):

I had problems with leakage when using with_zero and I fixed it by making with_zero irreducible and approaching everything in a principled way, never using definitional equality apart from when I was setting up the API

#### Eric Wieser (Oct 04 2020 at 12:33):

The statement of `bad_add_to_add`

is exactly an intermediate goal state in `add_monoid_algebra.to_multiplicative`

(edited)

#### Mario Carneiro (Oct 04 2020 at 12:33):

which includes `bad_add_to_add`

#### Mario Carneiro (Oct 04 2020 at 12:33):

what `to_additive`

are you talking about?

#### Eric Wieser (Oct 04 2020 at 12:33):

Ah, sorry - `add_monoid_algebra.to_multiplicative`

#### Eric Wieser (Oct 04 2020 at 12:34):

I meant that throughout

#### Mario Carneiro (Oct 04 2020 at 12:34):

I don't know what the statement of `add_monoid_algebra.to_multiplicative`

is but it seems highly likely that some bad_add stuff is in there

#### Eric Wieser (Oct 04 2020 at 12:34):

I pasted it above

#### Eric Wieser (Oct 04 2020 at 12:35):

It's my proposed isomorphism

#### Mario Carneiro (Oct 04 2020 at 12:35):

I mean the full statement

#### Eric Wieser (Oct 04 2020 at 12:35):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/p.20.2B.20q.20.3D.20p.20*.20q.20solves.20by.20refl!/near/212220659 is the full statement?

#### Mario Carneiro (Oct 04 2020 at 12:36):

I just don't understand how you can have a `add_monoid_algebra`

on one side and a `monoid_algebra `

on the other and they are the same type of object

#### Kevin Buzzard (Oct 04 2020 at 12:36):

There are maps from G to multiplicative G which could be used at all times. Does this solve the problems you have Eric? In my mind the fix for the leakage mentioned in the docs is to make `multiplicative`

irreducible after the API has been set up

#### Mario Carneiro (Oct 04 2020 at 12:36):

There are implicit arguments

#### Mario Carneiro (Oct 04 2020 at 12:36):

and all the interesting stuff in this discussion is only visible if you look at the implicit arguments

#### Kevin Buzzard (Oct 04 2020 at 12:36):

An add_monoid_algebra and a monoid_algebra are just both semirings, they can be isomorphic

#### Mario Carneiro (Oct 04 2020 at 12:37):

aha

#### Mario Carneiro (Oct 04 2020 at 12:37):

so is it the `finsupp`

lemmas then that are exposing the defeqs?

#### Eric Wieser (Oct 04 2020 at 12:38):

Perhaps the easiest way to see is:

`add_monoid_algebra`

:`single a1 b1 * single a2 b2 = single (a1 + a2) (b2 * b2)`

`monoid_algebra`

:`single a1 b1 * single a2 b2 = single (a1 * a2) (b2 * b2)`

#### Eric Wieser (Oct 04 2020 at 12:38):

So this is an obvious candidate for the type of map that Kevin is talking about - all I want to do is extend the existing maps to preserve additional structure

#### Mario Carneiro (Oct 04 2020 at 12:42):

Aha:

```
lemma add_monoid_algebra.map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [add_monoid α] [add_monoid α₂] {x y : add_monoid_algebra β α}
{f : α → α₂} (f_map_mul : ∀ x y, f x + f y = f (x + y)):
(map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) =
(map_domain f x * map_domain f y : add_monoid_algebra β α₂) := sorry
```

In your definition, the function `f`

is `multiplicative.to_add`

, so it should not be type correct for `f_map_mul`

#### Kevin Buzzard (Oct 04 2020 at 12:43):

I think that if you want to relate the two structures you could go further and define a group homomorphism between an add_group and a group, give it a nice notation, prove that this induces a morphism of semirings from add_monoid_alg and monoid_alg, do things the other way, prove that isomorphisms get sent to isomorphisms etc

#### Kevin Buzzard (Oct 04 2020 at 12:46):

We have spent two years running from the fact that we have two kinds of groups; usually it works fine because mathematicians use multiplication and addition in quite different ways, but with valuations I ran into problems because we didn't have eg any API for an infinite cyclic group. Valuations are both additive and multiplicative in the literature and lean's eccentric approach to keeping them separate has had advantages (eg the crystallisation of the monoid with 0 idea) but it also has disadvantages, and one we're seeing now is that it's difficult to pass from one world to the other.

#### Kevin Buzzard (Oct 04 2020 at 12:47):

But I think that one reason it's difficult is that nobody cared enough to write the API yet

#### Kevin Buzzard (Oct 04 2020 at 12:48):

I need an additive valuation on a multiplicative object to continue with discrete valuation rings and it's not there. Maybe it's time to put these things there? We've as yet seen no issues with people wanting to use ten different notations for groups and this idea not scaling.

#### Kevin Buzzard (Oct 04 2020 at 12:50):

I think that defining the structure which is a group hom from an additive to a multiplicative object and making a proper API would be the correct way to get the morphisms you want. Or are there other problems I've not foreseen?

#### Eric Wieser (Oct 04 2020 at 12:59):

We already have the group homs between additive and multiplicative objects - the case in question is dependent types `D X`

and `D (multiplicative Y)`

, where the `monoid`

on X is used internally by `D X`

#### Eric Wieser (Oct 04 2020 at 13:10):

Anyway, I've put the first lemma I need (`finsupp.dom_add_congr`

) up as #4398.

~~I think that alone is enough to demonstrate the issue, without complicating things with monoid_algebra.~~

~~The simplified question is, given ~~`monoid α`

how do I construct the canonical isomorphism `finsupp α β ≃+ finsupp (additive α) β`

? I can construct `finsupp α β ≃ finsupp (additive α) β`

easily with `finsupp.dom_congr`

, but I can't use `finsupp.dom_add_congr`

without the "illegal" `α ≃+ additive α`

object discussed above.

#### Eric Wieser (Oct 04 2020 at 13:28):

Mario Carneiro said:

Aha: <snip>

In your definition, the function`f`

is`multiplicative.to_add`

, so it should not be type correct for`f_map_mul`

Right, so I just called `rw`

on that definition, and lean created the nonsense goal for me automatically

#### Reid Barton (Oct 04 2020 at 14:15):

The moral is with these different instances on plain `def B := A`

definitions, you really should avoid doing anything that would be ill-typed if `B`

wasn't defeq to `A`

. At some point, it becomes easier to just not have them be defeq in the first place.

#### Eric Wieser (Oct 04 2020 at 15:06):

I ended up not using `bad_add_to_add`

, as I forgot that I did not need that `f 0 = 0`

. #4402 still has the nonsense intermediate goal state that started this thread.

#### Adam Topaz (Oct 04 2020 at 16:23):

Does mathlib have something like a monoid morphism from a multiplicative monoid to an additive monoid (or vice versa)? If not, should we add it? We can call one a `logarithm`

and the other an `exponential`

.

#### Adam Topaz (Oct 04 2020 at 16:26):

(Oh, I now see Kevin's comments about this.)

#### Reid Barton (Oct 04 2020 at 16:46):

The combinatorial explosion of lemmas in all the variants sounds a bit scary, but maybe this is the logical conclusion of having `add_monoid`

and `monoid`

in the first place?

#### Reid Barton (Oct 04 2020 at 16:47):

Also, we can call `to_add`

the "universal logarithm" on `multiplicative α`

, which sounds very sophisticated.

#### Reid Barton (Oct 04 2020 at 16:49):

For notation: `+→*`

for exponentials and `*→+`

for logarithms?

#### Adam Topaz (Oct 04 2020 at 17:28):

What about this approach:

```
import algebra
class has_binop (α : Type*) :=
(op : α → α → α)
class has_const (α : Type*) :=
(const : α)
structure widget (α β : Type*) [has_binop α] [has_binop β] [has_const α] [has_const β] :=
(to_fun : α → β)
(map_const : to_fun has_const.const = has_const.const)
(map_binop {x y : α} : to_fun (has_binop.op x y) = has_binop.op (to_fun x) (to_fun y))
instance add_to_op {α} [has_add α] : has_binop α := ⟨(+)⟩
instance zero_to_const {α} [has_zero α] : has_const α := ⟨0⟩
instance mul_to_op {α} [has_mul α] : has_binop α := ⟨(*)⟩
instance one_to_const {α} [has_one α] : has_const α := ⟨1⟩
variables {M N : Type*} [monoid M] [add_monoid N]
#check widget M N
#check widget N M
```

#### Adam Topaz (Oct 04 2020 at 17:28):

I guess this is a problem if `M`

is a ring.

#### Eric Wieser (Oct 04 2020 at 17:42):

I was also wondering about the similar:

```
class base_monoid {T : Type} (identity : T) (op: T -> T -> T)
:=
(op_identity : ...) -- etc
abbreviation add_monoid = base_monoid 0 (+)
abbreviation monoid = base_monoid 1 (*)
```

#### Adam Topaz (Oct 04 2020 at 17:47):

@Eric Wieser check out how these things work in Agda. It's similar to what you suggest.

#### Mario Carneiro (Oct 04 2020 at 23:32):

In the interest of avoiding combinatorial explosions, to what extent can we get away with using `G ->* multiplicative H`

for "logarithmic homs"?

#### Adam Topaz (Oct 05 2020 at 00:33):

I guess most things should work out if we define the the `has_coe_to_fun`

correctly, no?

#### Yury G. Kudryashov (Oct 05 2020 at 01:06):

I think that we can't redefine `has_coe_to_fun`

for this subcase.

#### Adam Topaz (Oct 05 2020 at 01:09):

You use a type alias

#### Yury G. Kudryashov (Oct 05 2020 at 01:19):

And loose lots of lemmas.

#### Yury G. Kudryashov (Oct 05 2020 at 01:19):

This is not better than adding a new type.

#### Adam Topaz (Oct 05 2020 at 01:20):

Yeah, you're right.

#### Adam Topaz (Oct 05 2020 at 01:20):

Is there some @[derive] magic that can be used?

#### Mario Carneiro (Oct 05 2020 at 01:22):

My suggestion is *not* to create a new type at all, just live with the fact that the codomain of the hom is `multiplicative H`

and use `multiplicative`

lemmas to convert the statements to things about addition in `H`

#### Kevin Buzzard (Oct 05 2020 at 06:09):

How about a new type for`multiplicative int`

?

#### Chris Hughes (Oct 05 2020 at 06:41):

I've been using `multiplicative int`

a lot lately. I just made notation for it. `C∞`

for the infinite cyclic group.

#### Eric Wieser (Oct 05 2020 at 15:16):

Eric Wieser said:

I was also wondering about the similar: <snip>

Turns out this is already discussed here: https://github.com/leanprover/lean/wiki/Refactoring-structures#encoding-the-algebraic-hierarchy-1

Last updated: May 11 2021 at 00:31 UTC