Zulip Chat Archive

Stream: maths

Topic: trivial group


view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:46):

I want to say that an add_comm_group is the trivial group {0}\{0\}. Should I use subsingleton or unique?

view this post on Zulip Anne Baanen (Apr 20 2021 at 15:58):

There is an instance docs#unique.subsingleton, right? Then unique is just strictly more useful.

view this post on Zulip Gabriel Ebner (Apr 20 2021 at 16:00):

If it's an assumption to a lemma, then I'd use subsingleton.

view this post on Zulip Sebastien Gouezel (Apr 20 2021 at 16:08):

The great advantage of subsingleton is that it has no data in it, contrary to unique.

view this post on Zulip Eric Wieser (Apr 20 2021 at 16:14):

Although if you have [add_comm_group A] [unique A], chances are the data in unique is defeq to the zero in add_comm_group anyway

view this post on Zulip Eric Wieser (Apr 20 2021 at 16:14):

So the presence / absence of data is unlikely to matter

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 16:20):

It's the conclusion of a lemma. Oh, if unique isn't a prop, forget it :-)

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 16:20):

who knows what the element is

view this post on Zulip Gabriel Ebner (Apr 20 2021 at 16:22):

Eric Wieser said:

Although if you have [add_comm_group A] [unique A], chances are the data in unique is defeq to the zero in add_comm_group anyway

That's exactly the situation where they are not defeq:

example {α} [add_comm_group α] [unique α] : default α = 0 := rfl -- fails

view this post on Zulip Nick Scheel (Apr 20 2021 at 16:59):

I suspect Eric meant that for a concrete A that satisfies those constraints, the two definitions will probably agree, but obviously not when A is unknown, as you showed.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 17:00):

It hadn't occurred to me that unique wasn't a Prop; in my use case I want a Prop. Do we have propositional uniqueness? Not that it matters urgently, I've gone with subsingleton now.

view this post on Zulip Anne Baanen (Apr 20 2021 at 17:16):

unique α is a subsingleton for what it's worth, but yeah, if you need a Prop then subsingleton is the way to go


Last updated: Jun 17 2021 at 16:20 UTC