Zulip Chat Archive

Stream: maths

Topic: Submonoids containing the base/central ring


view this post on Zulip Eric Wieser (Dec 03 2020 at 16:37):

Is this a good name for this structure?

/-- A `center_submonoid` is a submonoid that includes the central ring of the algebra -/
structure center_submonoid (R : Type*) (A : Type*) [comm_semiring R] [semiring A] [algebra R A]
  extends submonoid A, sub_mul_action R A.

which has the property

@[simp] lemma algebra_map_mem (r : R) : algebra_map R A r  S :=
by { rw algebra_map_eq_smul_one r, exact S.smul_mem r S.one_mem, }

and

@[simp] lemma zero_mem : 0  S := (algebra_map R A).map_zero  S.algebra_map_mem 0

and thus inherits the mul_action and the group_with_zero structures of A

view this post on Zulip Eric Wieser (Dec 03 2020 at 16:39):

Oh, this probably belongs in #maths

view this post on Zulip Reid Barton (Dec 03 2020 at 16:47):

I think you can edit the stream

view this post on Zulip Reid Barton (Dec 03 2020 at 16:47):

oh maybe not on this server

view this post on Zulip Notification Bot (Dec 03 2020 at 16:48):

This topic was moved here from #general > Submonoids containing the base/central ring by Rob Lewis

view this post on Zulip Reid Barton (Dec 03 2020 at 16:50):

What is this notion for?

view this post on Zulip Reid Barton (Dec 03 2020 at 16:51):

"center" means something different, and center_submonoid sounds too much like "central submonoid"

view this post on Zulip Eric Wieser (Dec 03 2020 at 16:54):

Submonoids of an algebra which include algebra_map R A r

view this post on Zulip Eric Wieser (Dec 03 2020 at 16:54):

Because those submonoids form a group_with_zero and inherit the same mul_action as their parent algebra

view this post on Zulip Adam Topaz (Dec 03 2020 at 16:55):

I'm confused about what the structure is supposed to be...

view this post on Zulip Eric Wieser (Dec 03 2020 at 16:55):

I need a fresh type in order to attach those instances

view this post on Zulip Eric Wieser (Dec 03 2020 at 16:56):

As a concrete example, it contains the non-unit spinor submonoid of the clifford algebra

view this post on Zulip Adam Topaz (Dec 03 2020 at 17:00):

I guess the elements of the form aXna \cdot X^n in a polynomial ring is also an example?

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:00):

Yes

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:00):

I've asked this in a thread before, but I can now ask it with less code because more is already in mathlib

view this post on Zulip Adam Topaz (Dec 03 2020 at 17:01):

I guess I'm wondering whether there are enough "natural" examples to give this a name :)

view this post on Zulip Reid Barton (Dec 03 2020 at 17:02):

I'm still confused, what is the group_with_zero?

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:03):

Sorry

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:03):

monoid_with_zero

view this post on Zulip Reid Barton (Dec 03 2020 at 17:03):

What is the monoid_with_zero?

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:03):

It's the monoid_with_zero that is inherited from the algebra

view this post on Zulip Adam Topaz (Dec 03 2020 at 17:03):

It's a submonoid of the ring, and 0 \bu 1 is the zero...

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:04):

I suppose this raises that a submonoid_with_zero would probably be a nice to have

view this post on Zulip Reid Barton (Dec 03 2020 at 17:04):

You mean each such submonoid is a monoid_with_zero?

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:05):

Yes

view this post on Zulip Reid Barton (Dec 03 2020 at 17:05):

Then why do you need a structure?

view this post on Zulip Reid Barton (Dec 03 2020 at 17:06):

submonoid_with_zero I understand

view this post on Zulip Adam Topaz (Dec 03 2020 at 17:06):

You want it to also be closed under scalar multiplication

view this post on Zulip Reid Barton (Dec 03 2020 at 17:06):

Why do I want that?

view this post on Zulip Adam Topaz (Dec 03 2020 at 17:06):

That's what @Eric Wieser wants... I dont know about you :)

view this post on Zulip Reid Barton (Dec 03 2020 at 17:07):

There must be something we're going to do at some point

view this post on Zulip Adam Topaz (Dec 03 2020 at 17:07):

Yeah, that's kind of my point too... It's unclear whether there are enough natural examples to make this a thing.

view this post on Zulip Reid Barton (Dec 03 2020 at 17:07):

Also, if you just have individual examples, then you can put the instances on the examples

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:08):

Yeah, but I had two examples and it was tiring

view this post on Zulip Reid Barton (Dec 03 2020 at 17:08):

I don't understand what's special about this combination of hypotheses

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:08):

It's not so much about whether it's special

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:08):

It's that we don't have any sensible way to work with them uncombined

view this post on Zulip Reid Barton (Dec 03 2020 at 17:09):

I agree this is a drawback of the bundled setup

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:10):

(s : submonoid A) (s' : sub_mul_action R A) (h : (s : set A) = s') seems like it would be ugly

view this post on Zulip Adam Topaz (Dec 03 2020 at 17:10):

Why not define a class on submonoid_with_zero saying it's closed under scalar multiplication?

view this post on Zulip Reid Barton (Dec 03 2020 at 17:10):

this is why stuff like is_submonoid shouldn't just go away

view this post on Zulip Adam Topaz (Dec 03 2020 at 17:11):

This is one point where I think the agda standard library has things right.... everything is consistently done with is_subfoo, and the bundled things are made using these.

view this post on Zulip Kevin Buzzard (Dec 03 2020 at 17:12):

So deprecated.subgroup should be refactored so that is_subgroup is a structure not a class, and then undeprecated?

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:13):

How would subtypes and attaching a group instance to them work in the is_subgroup style world?

view this post on Zulip Kevin Buzzard (Dec 03 2020 at 17:14):

subgroup G could be defined as (s : set G) (hs : is_subgroup s)

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:16):

My question was about what the implementation of has_coe_to_sort would look like under that design, for when I want to talk about (S : subgroup A) (s : S)

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:17):

Because I don't see a way out of defining the structure center_submonoid object I have above, all it would change was how the fields are laid out


Last updated: May 14 2021 at 20:13 UTC