Zulip Chat Archive

Stream: general

Topic: Positive parts


Yaël Dillies (Mar 10 2022 at 21:03):

@Christopher Hoskin, your docs#lattice_ordered_comm_group.has_one_lattice_has_pos_part is creating a diamond when α is a ring. Then the positive part is both a ⊔ 1 and a ⊔ 0.

Yaël Dillies (Mar 10 2022 at 21:03):

Not sure this happens in practice, but we should be aware of it.

Eric Wieser (Mar 10 2022 at 22:15):

Can you elaborate, maybe with an mwe?

Eric Wieser (Mar 10 2022 at 22:15):

rings aren't commutative groups

Eric Wieser (Mar 10 2022 at 22:15):

So did you mean docs#lattice_ordered_comm_group.has_zero_lattice_has_pos_part?

Yaël Dillies (Mar 10 2022 at 22:16):

Ah true. But the instance really only needs the bare syntax typeclasses.

Yaël Dillies (Mar 10 2022 at 22:17):

So at some point it will get generalized and suddenly a⁺ means two different things.

Eric Wieser (Mar 10 2022 at 22:18):

It feels like maybe it should have been called has_mul_pos_part

Eric Wieser (Mar 10 2022 at 22:19):

The pos name seems a pretty weird spelling for "at least 1". Is this from the literature, or just additivized pre-emptively?

Yaël Dillies (Mar 10 2022 at 22:19):

That we should read from Birkhoff.

Christopher Hoskin (Mar 13 2022 at 21:50):

In hindsight I should have stuck to my original plan of only developing the theory for additive groups. I'm happy to do a PR to remove the multiplicative case if that would help?

Christopher Hoskin (Mar 13 2022 at 22:29):

I think this may have been discussed previously, but I don't recall the conclusion.

Yaël Dillies (Mar 14 2022 at 08:01):

I currently don't see the point of developing the theory of multiplicative groups except that "it can be done". I don't think you need to strip down your work either. We should just have a big warning sign.


Last updated: Dec 20 2023 at 11:08 UTC