## Stream: new members

### Topic: multiplicative set

#### Holly Liu (Aug 05 2021 at 22:27):

so far i understand that multiplicative ℤ is the additive group on ℤ with 1 as the identity, * the group operation, ^-1 the inverse. Then does that mean it has two binary operations, + and *?

#### Mario Carneiro (Aug 05 2021 at 22:28):

No, it only has *

#### Mario Carneiro (Aug 05 2021 at 22:28):

in particular, although 1 : multiplicative ℤ works, 2 : multiplicative ℤ doesn't

#### Mario Carneiro (Aug 05 2021 at 22:30):

also, your description is wrong. multiplicative ℤ is the multiplicative group on ℤ with an identity written 1 (which is actually 0 : ℤ), a multiplication * (which is actually addition of integers), and ^-1 the inverse (which is actually negation).

got it

#### Kevin Buzzard (Aug 05 2021 at 22:32):

multiplicative ℤ should be thought of as a type which is completely different to ℤ. It's just an infinite cyclic group. There are maps between Z and multiplicative Z, and they're isomorphisms, but these are different types.

#### Holly Liu (Aug 05 2021 at 22:35):

Mario Carneiro said:

in particular, although 1 : multiplicative ℤ works, 2 : multiplicative ℤ doesn't

why is that

#### Mario Carneiro (Aug 05 2021 at 22:40):

because 2 is 1 + 1 and + doesn't exist

#### Mario Carneiro (Aug 05 2021 at 22:40):

oh yeah I said 1 : multiplicative ℤ works but it means 0 : ℤ

oh i understand

#### Eric Wieser (Aug 05 2021 at 22:54):

In case you haven't already found it, multiplicative.of_add (1 : ℤ) gives you the generator of the infinite cyclic group

#### Kevin Buzzard (Aug 06 2021 at 07:12):

The problem with understanding this mathematically is that the definition of multiplicative X is "it's X". This is a very confusing definition for mathematicians because if X already has a 1 (eg if X is the integers) then multiplicative X will now...have two 1s? The way to think about this is that the definition is merely an implementation detail which should be ignored, and multiplicative X should just be regarded as a totally different object to X.

#### Eric Wieser (Aug 06 2021 at 07:45):

Another interpretation is that multiplicative X forgets all the structure on X except the additive structure (ie forgets about 1 and *), but then changes that additive structure to use 1, (*), ⁻¹, (/), ^ as notation instead of 0, (+), -, (-), •.

#### Kevin Buzzard (Aug 06 2021 at 08:09):

Mathematicians are forever telling computer scientists that two things are the same and causing all sorts of problems because if you look at the definitions you find that it's an equiv, not an equality. Here the reverse is true -- you're telling us "multiplicative X is the same as X except that there is some totally different structure attached to it" and I think a more helpful perspective is that these things are equiv, and the fact that they are defeq might be convenient for the API writer but is positively confusing for the beginner user.

#### Kevin Buzzard (Aug 06 2021 at 08:11):

If two things are the same then they have the same 1, and this is not happening here. If two things biject with each other then sure they can different 1s

#### Kevin Buzzard (Aug 06 2021 at 08:12):

One issue is that we do not have the correct equiv in mathlib AFAIK: a bijection which sends + to *.

#### Kevin Buzzard (Aug 06 2021 at 08:14):

This is because of the (extraordinary, in my opinion) observation that most natural mathematical constructions between monoids in mathematics are between monoids which share notation for their group law. We even write valuations multiplicatively.

#### Eric Wieser (Aug 06 2021 at 08:15):

I think of it a having exactly the same structure with just a notation change, but I'll admit that outlook can be confusing if X already had a multiplicative structure. The "just a notation change" outlook is easier to apply to something like multiplicative (fin 3 → ℝ).

#### Eric Wieser (Aug 06 2021 at 08:16):

I'm not sure how much I believe that - I've come across lots of constructions that need multiplicative or additive on one side

#### Eric Wieser (Aug 06 2021 at 08:17):

It might be fun to write a metaprogram to count them

#### Kevin Buzzard (Aug 06 2021 at 08:23):

Eric Wieser said:

I think of it a having exactly the same structure with just a notation change.

Exactly. But such a thing tends not to happen in paper mathematics or in the lecture theatre (we "get our notation right the first time"), so this is why I am encouraging the "it's a completely different type but canonically isomorphic to X --the map is called of_add" approach because it will be more familiar to people like Holly who seems to have a mathematical background but is a newcomer to Lean.

#### Eric Wieser (Aug 06 2021 at 08:29):

And in fact, you should never just cast from X to multiplicative X in a definition, the right thing to do is always use the canonical map; otherwise you get things that unfold to nonsense like @has_one.one (multiplicative X) X.has_one which puts the original 1 of X into multiplicative X.

#### Kevin Buzzard (Aug 06 2021 at 08:29):

Here's another way of thinking it: if you asked a mathematician about the relationship between $(\mathbb{Z},+)$ and $(C_\infty,\times)$ (the infinite cyclic group) they would claim that these things were isomorphic (some may even claim something involving the word canonical) but absolutely none of them would suggest that the underlying sets/types were equal, this would be an absurd suggestion from our viewpoint.

#### Kevin Buzzard (Aug 06 2021 at 08:30):

In particular, the "it's the same set with a notation change" idea is not something which would ever cross our mind.

#### Holly Liu (Aug 06 2021 at 22:31):

thanks for the input. that was very interesting to read.

#### Holly Liu (Aug 11 2021 at 00:04):

i have some more questions about multiplicative ℤ: what are some of the elements of this set? since 2 isn't in here, what represents 2? i'm guessing it's something like 1 * 1 since it's an infinite cyclic group?

#### Holly Liu (Aug 11 2021 at 00:08):

also when i am trying to check that 1  is an element of multiplicative ℤ like #check 1 : multiplicative ℤ i get a red underline under : and the error command expected

#### Holly Liu (Aug 11 2021 at 00:09):

however, #check multiplicative.of_add (1 : ℤ) works, but isn't this just putting it into the multiplicative ℤ set?

#### Adam Topaz (Aug 11 2021 at 00:09):

multiplicative.of_add 2. The function docs#multiplicative.of_add takes a : A and produces the corresponding element of multiplicative A. You can prove that multiplicative.of_add 2 = g * g where g := multiplicative.of_add 1

#### Eric Wieser (Aug 11 2021 at 00:10):

You can prove ...

The proof is rfl isn't it?

#### Eric Wieser (Aug 11 2021 at 00:12):

x : Y is not valid syntax by itself, (x : Y) is; your #check needs parentheses

Should be

#### Holly Liu (Aug 11 2021 at 00:15):

ok that makes sense, thanks

Last updated: Dec 20 2023 at 11:08 UTC