# Zulip Chat Archive

## Stream: maths

### Topic: Naming for `monoid_algebra k G`

#### Eric Wieser (Oct 11 2020 at 16:09):

`monoid_algebra k G`

is defined by mathlib as `finsupp G k`

. When working with `finsupp a b`

, we can call `a`

the domain and `b`

the codomain (and do so in lemma names, eg docs#finsupp.map_domain).

Since `monoid_algebra`

doesn't define `has_coe_to_fun`

(and @Scott Morrison argues it should not), the terminology of domain and codomain doesn't really make sense when stating lemmas about it.

What terminology should I use instead?

#### Adam Topaz (Oct 11 2020 at 17:31):

It just so happens that this algebra has a basis indexed by `G`

. That's why (from a mathematical perspective) one should not name anything the domain and/or codomain.

#### Adam Topaz (Oct 11 2020 at 17:31):

What object do you want terminology for precisely?

#### Eric Wieser (Oct 11 2020 at 17:37):

I want a name for the mappings from `monoid_algebra G1 k1`

to `monoid_algebra G2 k1`

and `monoid_algebra G1 k2`

. `map_G fG`

and `map_k fk`

are lousy names, and I know to avoid names with domain or codomain in them

#### Eric Wieser (Oct 11 2020 at 17:38):

`map_index`

and `map_basis`

?

#### Adam Topaz (Oct 11 2020 at 17:39):

Well the second map is a base change, and the first one is a special case of the universal property.

#### Adam Topaz (Oct 11 2020 at 17:40):

So I think they should already have names, no?

#### Eric Wieser (Oct 11 2020 at 17:44):

If you're asking if the lemmas already exist, they do not. If you're asking if we have names for similar concepts elsewhere we can reuse, then I haven't looked at enough of elsewhere to know.

#### Adam Topaz (Oct 11 2020 at 17:46):

Can you give an example of a lemma you would like to name?

#### Eric Wieser (Oct 11 2020 at 17:58):

Sure, the `map_domain_mul`

from #4402. Ideally that lemma wouldn't even be stated in terms of `finsupp.map_domain`

, and that file would provide the same operation under a better name `monoid_algebra.map_...`

(which would eliminate the messy type ascriptions from that lemma statement)

#### Adam Topaz (Oct 11 2020 at 18:08):

I'm a bit confused. Is it proven somewhere that `monoid_algebra G k`

is functorial in `G`

?

#### Adam Topaz (Oct 11 2020 at 18:08):

Or is that what you're working on proving?

#### Eric Wieser (Oct 11 2020 at 19:02):

I'm afraid I don't know the meaning of "functorial in G" there, so can't really answer your question

#### Kevin Buzzard (Oct 11 2020 at 20:26):

If you have a monoid hom from G to H, does Lean already know that this induces a semiring hom from k[G] to k[H]?

#### Kevin Buzzard (Oct 11 2020 at 20:27):

i.e. is the construction G maps to k[G] the construction on objects underlying a functor from the category of monoids to the category of semirings?

#### Eric Wieser (Oct 11 2020 at 20:37):

Thanks Kevin for expanding - that first statement is indeed exactly what lean does not know and I want to teach it in with the `map_domain_mul`

lemma in the linked PR

#### Eric Wieser (Oct 11 2020 at 20:38):

While that second statement nicely captures all the ideas I am not yet familiar with.

#### Adam Topaz (Oct 11 2020 at 21:09):

Sorry, I've been away for a little while.

One thing to note is that mathlib has this: docs#monoid_algebra.lift

This together with the canonical map `G \to monoid_algebra G k`

(which should be a morphism of monoids) can be combined to obtain functoriality.

#### Eric Wieser (Oct 11 2020 at 22:06):

That's where this all started - to my eye that lift is insufficiently general, and I needed to generalize further to implement #4321

#### Eric Wieser (Oct 11 2020 at 22:08):

You can see the generalization in the `lift_aux`

lemma

#### Kevin Buzzard (Oct 11 2020 at 22:12):

So you need that the map from H to k[H] is a monoid hom as well, and then you get a monoid hom from G to k[H] which lifts to a k-algebra hom from k[G] to k[H].

#### Adam Topaz (Oct 11 2020 at 22:20):

Kevin Buzzard said:

So you need that the map from H to k[H] is a monoid hom as well, and then you get a monoid hom from G to k[H] which lifts to a k-algebra hom from k[G] to k[H].

Mathlib doesn't have the fact that the map from `G`

to `k[G]`

is a monoid hom?! :surprise:

#### Kevin Buzzard (Oct 12 2020 at 06:27):

I didn't look, I was just sketching how to use lift to get what we wanted

#### Eric Wieser (Oct 12 2020 at 08:31):

Adam Topaz said:

Mathlib doesn't have the fact that the map from

`G`

to`k[G]`

is a monoid hom?! :surprise:

No, that exists: docs#monoid_algebra.of

#### Eric Wieser (Oct 12 2020 at 10:44):

What should the name be for the canonical map `k → monoid_algebra k G`

? It's defeq to `finsupp.single 1`

, but `single`

doesn't seem like a good name to keep using in `monoid_algebra`

-land

#### Adam Topaz (Oct 12 2020 at 12:22):

That's the algebra map

#### Eric Wieser (Oct 12 2020 at 12:24):

Not when k is not a commutative ring

#### Kevin Buzzard (Oct 12 2020 at 12:25):

what other k did you have in mind?

#### Eric Wieser (Oct 12 2020 at 12:26):

The free algebra

#### Adam Topaz (Oct 12 2020 at 12:27):

Oh and G is N? I.e. you're working on the grading of the free algebra?

#### Kevin Buzzard (Oct 12 2020 at 12:28):

so non-commutative rings? Do group rings work over non-commutative rings?

#### Kevin Buzzard (Oct 12 2020 at 12:28):

Oh you make the group commutative instead?

#### Eric Wieser (Oct 12 2020 at 12:29):

To elaborate on @Adam's point: I'm defining the grading of the free algebra as `(free_algebra R X) →ₐ[R] add_monoid_algebra (free_algebra R X) ℕ`

#### Eric Wieser (Oct 12 2020 at 12:30):

Where `add_monoid_algebra (free_algebra R X) ℕ`

is isomorphic to `monoid_algebra (free_algebra R X) (multiplicative ℕ)`

if that helps (although mathlib doesn't know that yet)

#### Adam Topaz (Oct 12 2020 at 12:33):

I don't know whether monoid rings work over non commutative rings, but in this case it's the polynomial ring, so it's fine.

#### Adam Topaz (Oct 12 2020 at 12:35):

Note that the algebra map would not give the grading in this case

#### Adam Topaz (Oct 12 2020 at 12:35):

You need the map sending elements of X to degree 1

#### Adam Topaz (Oct 12 2020 at 12:35):

Not 0

#### Eric Wieser (Oct 12 2020 at 12:37):

Yes, I have that already

#### Eric Wieser (Oct 12 2020 at 12:38):

Although now you mention it it sounds like I may have messed up a refactor

#### Adam Topaz (Oct 12 2020 at 12:49):

My point is that this map does not agree with "the" map from k to `monoid_algebra G k`

where k is the free algebra and G is N. By "the" map I mean the map you get from the theory of monoid rings.

#### Eric Wieser (Oct 12 2020 at 12:58):

Indeed - it turns out the question I'm asking is not useful for grading the free algebra

#### Eric Wieser (Oct 12 2020 at 13:00):

But,for the question I asked, it's still not `algebra.algebra_map`

either, since that maps `R`

into `algebra R (monoid_algebra G k)`

and I want to map `k`

#### Adam Topaz (Oct 12 2020 at 13:04):

You're right. I would call it `const`

or `scalar`

for "constants" or "scalars".

#### Adam Topaz (Oct 12 2020 at 13:39):

I'm surprised mathlib doesn't have this ring hom already...

#### Eric Wieser (Oct 12 2020 at 13:41):

I've added it in #4582, but before we had this conversation

#### Eric Wieser (Oct 12 2020 at 13:42):

So the name(s) are currently a mouthful

#### Adam Topaz (Oct 12 2020 at 13:51):

#### Adam Topaz (Oct 12 2020 at 13:53):

docs#monoid_algebra.algebra_map'

#### Eric Wieser (Oct 12 2020 at 13:53):

I know, I removed those lines in my PR

#### Eric Wieser (Oct 12 2020 at 13:55):

`algebra_map' ring_hom.id`

is the thing we're talking about, but with the proposed name `const`

(`= single_one_ring_hom `

in that PR), `algebra_map' = const.comp`

, suggesting that `const`

is the more primitive (and therfore useful) definition. The fact that the proof is shorter is also a good indication that `const`

is a better thing to have.

Last updated: May 10 2021 at 06:13 UTC