# Zulip Chat Archive

## Stream: general

### Topic: Monoid ring in Lean

#### Daniel Donnelly (Dec 13 2019 at 17:12):

How do you create and work with a Monoid Ring?

#### Johan Commelin (Dec 13 2019 at 17:34):

You need to use `finsupp`

#### Johan Commelin (Dec 13 2019 at 17:35):

@Daniel Donnelly The best thing is probably to look for `instance : semiring`

in `data/finsupp.lean`

#### Johan Commelin (Dec 13 2019 at 18:49):

https://github.com/leanprover-community/mathlib/blob/master/src/data/finsupp.lean#L1196

#### Johan Commelin (Dec 13 2019 at 18:49):

It wants an additive monoid though

#### Johan Commelin (Dec 13 2019 at 18:50):

If in your context the monoid is multiplicative, you can switch to additive notation by using `(additive M)`

#### Daniel Donnelly (Dec 13 2019 at 20:26):

@Johan Commelin can you give me an example useage?

#### Kevin Buzzard (Dec 13 2019 at 20:33):

import data.real.basic data.finsupp def monoid_ring (M : Type*) [monoid M] := (additive M) →₀ ℤ noncomputable example (M : Type*) [monoid M] : ring (monoid_ring M) := by unfold monoid_ring; apply_instance

#### Kevin Buzzard (Dec 13 2019 at 20:40):

import data.finsupp def monoid_ring (M : Type*) [monoid M] := (additive M) →₀ ℤ noncomputable theory instance {M : Type*} [monoid M] : ring (monoid_ring M) := by unfold monoid_ring; apply_instance variables {M : Type*} [monoid M] def of_monoid (a : M) : monoid_ring M := finsupp.single a 1 example (a b : M) : of_monoid a * of_monoid b = of_monoid (a * b) := begin apply finsupp.single_mul_single, end

#### Kevin Buzzard (Dec 13 2019 at 20:50):

Maybe bundled is better:

import data.finsupp def monoid_ring (M : Type*) [monoid M] := (additive M) →₀ ℤ noncomputable theory instance {M : Type*} [monoid M] : ring (monoid_ring M) := by unfold monoid_ring; apply_instance variables {M : Type*} [monoid M] def monoid_ring.of_monoid (M : Type*) [monoid M] : monoid_hom M (monoid_ring M) := { to_fun := λ m, finsupp.single m 1, map_one' := rfl, map_mul' := λ x y, (@finsupp.single_mul_single (additive M) _ _ _ x y 1 1).symm }

#### Johan Commelin (Dec 14 2019 at 05:25):

@Daniel Donnelly See Kevin's examples. If you want more, you should provide more context of the things you want to do...

#### Daniel Donnelly (Dec 16 2019 at 20:16):

@Kevin Buzzard what is that "o" next to the "\to" arrow?

#### Patrick Massot (Dec 16 2019 at 20:17):

Finitely supported map

#### Patrick Massot (Dec 16 2019 at 20:18):

You can copy-paste Kevin's code and use "Go to definition" (F12 in VScode)

Last updated: May 14 2021 at 03:27 UTC