multiplicative set

Stream: new members

[Holly Liu]

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]

No, it only has *

[Mario Carneiro]

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

[Mario Carneiro]

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

[Holly Liu]

got it

[Kevin Buzzard]

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]

Mario Carneiro said:

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

why is that

[Mario Carneiro]

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

[Mario Carneiro]

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

[Holly Liu]

oh i understand

[Eric Wieser]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

It might be fun to write a metaprogram to count them

[Kevin Buzzard]

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]

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]

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]

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

[Holly Liu]

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

[Holly Liu]

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]

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]

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

[Adam Topaz]

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]

You can prove ...

The proof is rfl isn't it?

[Eric Wieser]

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

[Adam Topaz]

Should be

[Holly Liu]

ok that makes sense, thanks