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: Dec 20 2023 at 11:08 UTC