Zulip Chat Archive

Stream: general

Topic: adding an element to a set


Kevin Buzzard (Jul 26 2018 at 08:52):

The notation + is attached to has_add.add : X -> X -> X. Mathematicians use + in more general ways though. I find myself wanting to write r + J for r an element of, and J a subset of, an additive abelian group (J is a subgroup in fact). This is standard notation in mathematics and I suspect I can't have it given the set-up we have. Does anyone have any thoughts as to how I might try and represent such an idea in Lean? I can make the object I want no problem, the issue is simply that I want the notation to be as close to what a mathematician would write as possible.

Kenny Lau (Jul 26 2018 at 08:56):

It's called a coset.

Kenny Lau (Jul 26 2018 at 08:56):

specifically, a left coset

Kevin Buzzard (Jul 26 2018 at 08:57):

I've seen cosets in group theory but unfortunately this is an additive group ;-)

Kenny Lau (Jul 26 2018 at 08:57):

additive

Kevin Buzzard (Jul 26 2018 at 09:21):

How scalable is this additive idea I wonder? I recently wanted a free abelian group with group law multiplication but ultimately settled on group law addition because thay was what the finsupp construction gave me and I couldn't face cluttering everything up with additive and multiplicative everywhere.

Kenny Lau (Jul 26 2018 at 09:22):

as scalable as I made it in my constructive tensor product

Kenny Lau (Jul 26 2018 at 09:22):

def free_abelian_group : Type u :=
additive $ abelianization $ free_group α

Kenny Lau (Jul 26 2018 at 09:22):

and the proof that it works is that I built the whole tensor product out of the free abelian group

Chris Hughes (Jul 26 2018 at 09:23):

(+ r) '' J

Kenny Lau (Jul 26 2018 at 09:23):

I would prefer ((-) r) ⁻¹' J

Johan Commelin (Jul 26 2018 at 09:24):

I would prefer readable notation.

Kevin Buzzard (Jul 26 2018 at 09:49):

I would prefer the notation mathematicians use, i.e. what we can't have.


Last updated: Dec 20 2023 at 11:08 UTC