# Zulip Chat Archive

## Stream: maths

### Topic: multiplicative finsupp

#### Johan Commelin (Jan 22 2019 at 10:29):

I'm trying to stress test my adjunctions code. A natural example is `mv_polynomial`

being left adjoint to `forget`

. This adjunction is actually a composite of two adjunctions: the free monoid construction, and monoid rings. While trying to write these things down, I got stuck in the whole additive-multiplicative business again. So, let's forget about this motivation for now.

Has anyone ever attempted to turn `data/finsupp`

into a file that supports both multiplicative and additive coefficients? Are there any expected problems? Or is this just something that has to be done by someone?

#### Mario Carneiro (Jan 22 2019 at 10:32):

use `multiplicative A`

for the coefficients

#### Johan Commelin (Jan 22 2019 at 10:43):

I know I can do that. But it becomes pretty messy. And it feels to me like it defeats the purpose of the `add`

/`mul`

distinction.

#### Johan Commelin (Jan 22 2019 at 10:44):

All of a sudden I'm having proofs like

{ map_one := map_domain_zero, map_mul := λ _ _, map_domain_add }

which creates cognitive dissonance.

#### Johan Commelin (Jan 22 2019 at 10:45):

I think that if we want to use `multiplicative`

(or `additive`

, I don't care) we should just use it everywhere.

#### Mario Carneiro (Jan 22 2019 at 10:45):

well we did, and now you want the other one

#### Johan Commelin (Jan 22 2019 at 10:47):

No, I mean everywhere in mathlib.

#### Mario Carneiro (Jan 22 2019 at 10:47):

I have argued since day 1 that it would be much nicer to use add for group theory and forget about mul except in specialized circumstances, but mathematicians get hissy about non-commutative addition

#### Kevin Buzzard (Jan 22 2019 at 11:04):

Mathematicians definitely want both.

#### Kevin Buzzard (Jan 22 2019 at 11:04):

Non-commutative addition is the least of our worries here.

#### Mario Carneiro (Jan 22 2019 at 11:19):

If I said "all groups must use addition", what exactly would be the downside? AFAICT there are very few places where you actually need multiplicative groups besides "it looks better"

#### Mario Carneiro (Jan 22 2019 at 11:20):

by contrast it is quite common to use the group structure of additive groups embedded in rings and other things

#### Mario Carneiro (Jan 22 2019 at 11:21):

Note that a ring does not have a multiplicative group; multiplication is not a group operation. Instead there is an associated structure, the "units group", that is a group

#### Kevin Buzzard (Jan 22 2019 at 11:30):

If you said "all groups must use addition" then mathematicians would consistently be utterly confused about why the unit group of a ring had group law addition. I guess there's nothing stopping this convention -- equally, there is nothing stopping the convention that you use a little heart symbol. It's just that mathematicians would then find this stuff even harder to understand. Notation conveys meaning and notation which mathematicians have fixed on is *very* hard to change. I personally loathe the standard symbol for quadratic residues / non-residues, because it's a fraction in a bracket -- but there's very little I can do about this.

#### Johan Commelin (Jan 22 2019 at 11:38):

We have proof irrelevance. Why can't we have notation irrelevance. (I know that the current implementation via type classes makes it hard. But that just means we need a better solution.)

#### Johan Commelin (Jan 22 2019 at 12:12):

@Mario Carneiro I can see why you would want all groups to be additive (although adding invertible matrices feels very wrong). But with monoids you wouldn't have a clean solution, right? Every ring gives you two monoids, one for addition, the other for multiplication. I'm interested in knowing what you would do there.

#### Kevin Buzzard (Jan 22 2019 at 16:00):

I thought about this more. A mathematician has a fixed notation for a ring, so you can't change it -- it uses `+`

and `*`

. And a ring is a group under `+`

and the units of a ring are a group under `*`

, and these come up again and again, so you can't change these either :-/ And the point is that in mathematics we are capable of rewriting these group axioms from `+`

to `*`

seamlessly because *it is true that it works fine*, yet Lean struggles to do it seamlessly. There clearly is some sort of a problem here, but I don't think mathematicians will accept removal of `*`

because it goes the wrong way. For us, the units of $R$ are a subset of $R$. This is not how it works in DTT and somehow we need a better solution :-/

#### Johan Commelin (Jan 22 2019 at 16:01):

How about `End(V)`

? We'll use `\circ`

instead of `*`

, without blinking an eye.

#### Reid Barton (Jan 22 2019 at 16:02):

A unit is just an automorphism of a ring as a module over itself, what's the problem?

#### Reid Barton (Jan 22 2019 at 16:03):

Last updated: May 19 2021 at 00:40 UTC