Zulip Chat Archive

Stream: maths

Topic: Naming for `monoid_algebra k G`


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

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

view this post on Zulip Adam Topaz (Oct 11 2020 at 17:31):

What object do you want terminology for precisely?

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

view this post on Zulip Eric Wieser (Oct 11 2020 at 17:38):

map_index and map_basis?

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

view this post on Zulip Adam Topaz (Oct 11 2020 at 17:40):

So I think they should already have names, no?

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

view this post on Zulip Adam Topaz (Oct 11 2020 at 17:46):

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

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

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

view this post on Zulip Adam Topaz (Oct 11 2020 at 18:08):

Or is that what you're working on proving?

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

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

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

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

view this post on Zulip Eric Wieser (Oct 11 2020 at 20:38):

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

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

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

view this post on Zulip Eric Wieser (Oct 11 2020 at 22:08):

You can see the generalization in the lift_aux lemma

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

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

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

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

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

view this post on Zulip Adam Topaz (Oct 12 2020 at 12:22):

That's the algebra map

view this post on Zulip Eric Wieser (Oct 12 2020 at 12:24):

Not when k is not a commutative ring

view this post on Zulip Kevin Buzzard (Oct 12 2020 at 12:25):

what other k did you have in mind?

view this post on Zulip Eric Wieser (Oct 12 2020 at 12:26):

The free algebra

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

view this post on Zulip Kevin Buzzard (Oct 12 2020 at 12:28):

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

view this post on Zulip Kevin Buzzard (Oct 12 2020 at 12:28):

Oh you make the group commutative instead?

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

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

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

view this post on Zulip Adam Topaz (Oct 12 2020 at 12:35):

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

view this post on Zulip Adam Topaz (Oct 12 2020 at 12:35):

You need the map sending elements of X to degree 1

view this post on Zulip Adam Topaz (Oct 12 2020 at 12:35):

Not 0

view this post on Zulip Eric Wieser (Oct 12 2020 at 12:37):

Yes, I have that already

view this post on Zulip Eric Wieser (Oct 12 2020 at 12:38):

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

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

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

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

view this post on Zulip Adam Topaz (Oct 12 2020 at 13:04):

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

view this post on Zulip Adam Topaz (Oct 12 2020 at 13:39):

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

view this post on Zulip Eric Wieser (Oct 12 2020 at 13:41):

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

view this post on Zulip Eric Wieser (Oct 12 2020 at 13:42):

So the name(s) are currently a mouthful

view this post on Zulip Adam Topaz (Oct 12 2020 at 13:51):

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

view this post on Zulip Adam Topaz (Oct 12 2020 at 13:53):

docs#monoid_algebra.algebra_map'

view this post on Zulip Eric Wieser (Oct 12 2020 at 13:53):

I know, I removed those lines in my PR

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