Submonoids containing the base/central ring

Stream: maths

[Eric Wieser]

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]

Oh, this probably belongs in #maths

[Reid Barton]

I think you can edit the stream

[Reid Barton]

oh maybe not on this server

[Notification Bot]

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

[Reid Barton]

What is this notion for?

[Reid Barton]

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

[Eric Wieser]

Submonoids of an algebra which include algebra_map R A r

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

I need a fresh type in order to attach those instances

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

Yes

[Eric Wieser]

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]

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

[Reid Barton]

I'm still confused, what is the group_with_zero?

[Eric Wieser]

Sorry

[Eric Wieser]

monoid_with_zero

[Reid Barton]

What is the monoid_with_zero?

[Eric Wieser]

It's the monoid_with_zero that is inherited from the algebra

[Adam Topaz]

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

[Eric Wieser]

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

[Reid Barton]

You mean each such submonoid is a monoid_with_zero?

[Eric Wieser]

Yes

[Reid Barton]

Then why do you need a structure?

[Reid Barton]

submonoid_with_zero I understand

[Adam Topaz]

You want it to also be closed under scalar multiplication

[Reid Barton]

Why do I want that?

[Adam Topaz]

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

[Reid Barton]

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

[Adam Topaz]

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

[Reid Barton]

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

[Eric Wieser]

Yeah, but I had two examples and it was tiring

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

I agree this is a drawback of the bundled setup

[Eric Wieser]

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

[Adam Topaz]

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

[Reid Barton]

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

[Adam Topaz]

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]

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

[Eric Wieser]

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

[Kevin Buzzard]

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

[Eric Wieser]

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]

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