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):

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?

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

Not 0

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:42):

So the name(s) are currently a mouthful

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