canonical group_with_zero {-1,0,1}

Stream: maths

[Johan Commelin]

• Do we have a canonical multiplicative group with zero of cardinality three? (Candidates: zmod 3)
• Related: Do we have a canonical multiplicative group of cardinality two? (Candidates: units ℤ, units (zmod 3))

I'm not so happy with zmod 3. Intuitively it's too ringy. A group_with_zero_hom zmod 3 →* ℤ (or any ring for that matter) just feels morally wrong.

[Johan Commelin]

Should I ignore this feeling, and use zmod 3 nonetheless? Or is there a better candidate? Or do we want/need a new type?

[Kevin Buzzard]

Do we have a canonical cyclic group of any order? Maria has been using multiplicative int for the infinite cyclic group.

[Kevin Buzzard]

So with_zero (multiplicative (zmod 2)) is my suggestion for your first question.

[Kevin Buzzard]

OTOH since addition was defined on fin 2 to match zmod 2 (despite my protestations ;-) ) you could also use that...

[Johan Commelin]

I think it would be nice to have the notations -1, 0, 1 for the three elements. Your with_zero (multiplicate _) will not have that out of the box, right?
Also, it's a pretty long name for a simple thing...

[Eric Wieser]

That notation should work for with_zero (units Z), right?

[Kevin Buzzard]

I mean, there are a ton of ways to do it

[Eric Wieser]

Does it make sense to have a units_or_zero type?

[Kevin Buzzard]

I see -- somehow the issue is not that Johan wants "cyclic groups with zero" at this point (although Maria did for valuation theory) -- he just wants {-1,0,1}. I hadn't read the title of the thread because it was cut off in the app :-)

[Eric Wieser]

Eric Wieser said:

That notation should work for with_zero (units Z), right?

#check (1 : with_zero (units ℤ))  -- ok
#check (0 : with_zero (units ℤ))  -- ok
#check (-1 : with_zero (units ℤ))  -- fail :(

[Yakov Pechersky]

Your coercions are too eager

[Johan Commelin]

Kevin Buzzard said:

I mean, there are a ton of ways to do it

Exactly. Hence my question.

[Kevin Buzzard]

Now I understand that you want the notation, I think zmod 3 is a clever choice ;-)

[Yakov Pechersky]

You'll need ((-1 : units int) : with_zero blah), and hope that neg works properly for units int.

[Eric Wieser]

We're missing:

section
attribute [semireducible] with_zero
instance {α} [has_neg α] : has_neg (with_zero α) := ⟨λ a, option.map has_neg.neg a⟩
end

[Eric Wieser]

If we add that the example above works

[Kevin Buzzard]

I think that's better than the zmod 3 hack

[Adam Topaz]

Should we define galois_field 1 n? :wink: (sorry)

[Yakov Pechersky]

IIRC doing the semireducible trick could make things annoying later on. We hit that with with_top before.

[Yakov Pechersky]

Rather, a with_zero.rec definition would be kinder to api users

[Eric Wieser]

#10194

[Eric Wieser]

Yakov Pechersky said:

IIRC doing the semireducible trick could make things annoying later on. We hit that with with_top before.

I'm just copying what is already done for the has_mul instance

[Yury G. Kudryashov]

-1 works for zmod 3 too

[Kevin Buzzard]

yeah but it's a hack

[Floris van Doorn]

One thing worth considering:
Do you ever want to define a map using pattern matching like this?

def f : with_zero (units Z) -> X
| (-1) := ...
| 0    := ...
| 1    := ...

Depending on the choice this may not work.
But maybe this is not important, because you might only care about monoid_with_zero_hom out of this type?

[Eric Wieser]

Does that actually work right now, @Floris van Doorn?

[Kevin Buzzard]

oh surely not (edit: no)

[Johan Commelin]

Right. With zmod 3 you can do something very close to that, I guess.

[Johan Commelin]

Anyway, with any type, we can get reasonably close to that by writing a custom recursor.

[Floris van Doorn]

I just meant that there are ways to make it work, but if you do that you cannot reuse stuff from the library, so it's probably not worth it.