Zulip Chat Archive

Stream: general

Topic: Monoid ring in Lean


view this post on Zulip Daniel Donnelly (Dec 13 2019 at 17:12):

How do you create and work with a Monoid Ring?

view this post on Zulip Johan Commelin (Dec 13 2019 at 17:34):

You need to use finsupp

view this post on Zulip Johan Commelin (Dec 13 2019 at 17:35):

@Daniel Donnelly The best thing is probably to look for instance : semiring in data/finsupp.lean

view this post on Zulip Johan Commelin (Dec 13 2019 at 18:49):

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

view this post on Zulip Johan Commelin (Dec 13 2019 at 18:49):

It wants an additive monoid though

view this post on Zulip 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)

view this post on Zulip Daniel Donnelly (Dec 13 2019 at 20:26):

@Johan Commelin can you give me an example useage?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip 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...

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 20:16):

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

view this post on Zulip Patrick Massot (Dec 16 2019 at 20:17):

Finitely supported map

view this post on Zulip 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