## 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