adding an element to a set

Stream: general

[Kevin Buzzard]

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]

It's called a coset.

[Kenny Lau]

specifically, a left coset

[Kevin Buzzard]

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

[Kenny Lau]

additive

[Kevin Buzzard]

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]

as scalable as I made it in my constructive tensor product

[Kenny Lau]

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

[Kenny Lau]

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

[Chris Hughes]

(+ r) '' J

[Kenny Lau]

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

[Johan Commelin]

I would prefer readable notation.

[Kevin Buzzard]

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