Naming for `monoid_algebra k G`

Stream: maths

[Eric Wieser]

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]

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]

What object do you want terminology for precisely?

[Eric Wieser]

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]

map_index and map_basis?

[Adam Topaz]

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

[Adam Topaz]

So I think they should already have names, no?

[Eric Wieser]

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]

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

[Eric Wieser]

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]

I'm a bit confused. Is it proven somewhere that monoid_algebra G k is functorial in G?

[Adam Topaz]

Or is that what you're working on proving?

[Eric Wieser]

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

[Kevin Buzzard]

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]

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]

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]

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

[Adam Topaz]

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]

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]

You can see the generalization in the lift_aux lemma

[Kevin Buzzard]

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]

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]

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

[Eric Wieser]

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]

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]

That's the algebra map

[Eric Wieser]

Not when k is not a commutative ring

[Kevin Buzzard]

what other k did you have in mind?

[Eric Wieser]

The free algebra

[Adam Topaz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Oh you make the group commutative instead?

[Eric Wieser]

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]

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]

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]

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

[Adam Topaz]

You need the map sending elements of X to degree 1

[Adam Topaz]

Not 0

[Eric Wieser]

Yes, I have that already

[Eric Wieser]

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

[Adam Topaz]

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]

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

[Eric Wieser]

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]

You're right. I would call it const or scalar for "constants" or "scalars".

[Adam Topaz]

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

[Eric Wieser]

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

[Eric Wieser]

So the name(s) are currently a mouthful

[Adam Topaz]

@Eric Wieser https://github.com/leanprover-community/mathlib/blob/0bfc68fcabfca3ea05d144479145d3ac8ba4fa91/src/algebra/monoid_algebra.lean#L252

[Adam Topaz]

docs#monoid_algebra.algebra_map'

[Eric Wieser]

I know, I removed those lines in my PR

[Eric Wieser]

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.