## Stream: maths

### Topic: Submonoids containing the base/central ring

#### 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

#### Eric Wieser (Dec 03 2020 at 16:39):

Oh, this probably belongs in #maths

#### Reid Barton (Dec 03 2020 at 16:47):

I think you can edit the stream

#### Reid Barton (Dec 03 2020 at 16:47):

oh maybe not on this server

#### Notification Bot (Dec 03 2020 at 16:48):

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

#### Reid Barton (Dec 03 2020 at 16:50):

What is this notion for?

#### Reid Barton (Dec 03 2020 at 16:51):

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

#### Eric Wieser (Dec 03 2020 at 16:54):

Submonoids of an algebra which include algebra_map R A r

#### 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

#### Adam Topaz (Dec 03 2020 at 16:55):

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

#### Eric Wieser (Dec 03 2020 at 16:55):

I need a fresh type in order to attach those instances

#### Eric Wieser (Dec 03 2020 at 16:56):

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

#### Adam Topaz (Dec 03 2020 at 17:00):

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

Yes

#### 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

#### Adam Topaz (Dec 03 2020 at 17:01):

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

#### Reid Barton (Dec 03 2020 at 17:02):

I'm still confused, what is the group_with_zero?

Sorry

#### Eric Wieser (Dec 03 2020 at 17:03):

monoid_with_zero

#### Reid Barton (Dec 03 2020 at 17:03):

What is the monoid_with_zero?

#### Eric Wieser (Dec 03 2020 at 17:03):

It's the monoid_with_zero that is inherited from the algebra

#### Adam Topaz (Dec 03 2020 at 17:03):

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

#### Eric Wieser (Dec 03 2020 at 17:04):

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

#### Reid Barton (Dec 03 2020 at 17:04):

You mean each such submonoid is a monoid_with_zero?

Yes

#### Reid Barton (Dec 03 2020 at 17:05):

Then why do you need a structure?

#### Reid Barton (Dec 03 2020 at 17:06):

submonoid_with_zero I understand

#### Adam Topaz (Dec 03 2020 at 17:06):

You want it to also be closed under scalar multiplication

#### Reid Barton (Dec 03 2020 at 17:06):

Why do I want that?

#### Adam Topaz (Dec 03 2020 at 17:06):

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

#### Reid Barton (Dec 03 2020 at 17:07):

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

#### 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.

#### Reid Barton (Dec 03 2020 at 17:07):

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

#### Eric Wieser (Dec 03 2020 at 17:08):

Yeah, but I had two examples and it was tiring

#### Reid Barton (Dec 03 2020 at 17:08):

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

#### Eric Wieser (Dec 03 2020 at 17:08):

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

#### Eric Wieser (Dec 03 2020 at 17:08):

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

#### Reid Barton (Dec 03 2020 at 17:09):

I agree this is a drawback of the bundled setup

#### 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

#### Adam Topaz (Dec 03 2020 at 17:10):

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

#### Reid Barton (Dec 03 2020 at 17:10):

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

#### 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.

#### 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?

#### 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?

#### Kevin Buzzard (Dec 03 2020 at 17:14):

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

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

#### 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