Zulip Chat Archive

Stream: general

Topic: Stabilizers

Yaël Dillies (Dec 15 2022 at 11:32):

We have both docs#mul_action.stabilizer and docs#mul_action.stabilizer.submonoid. Would it make sense to rename them to subgroup.stabilizer and submonoid.stabilizer?

Eric Wieser (Dec 15 2022 at 13:30):

The only downside I can think of is it weakens the canonicity of one of the spellings. Arguably we already need to repeat results for both though, such as the instance in this comment.

Eric Wieser (Dec 15 2022 at 13:31):

I would imagine that we could also have a subring.stabilizer?

Yaël Dillies (Dec 15 2022 at 13:33):

Yes, probably!

Eric Rodriguez (Dec 15 2022 at 13:34):

I think it's there in the little wedderburn PR, which I should probably push to get merged before the relevant files go to lean4

Yaël Dillies (Dec 15 2022 at 13:34):

What I like about this is that there's exactly one bit of the name that changes between the additive and multiplicative version, and it's much nicer to refer to subgroup_stabilizer than to mul_action_stabilizer if ever we need to disambiguate them in a lemma name.

Eric Rodriguez (Dec 15 2022 at 13:35):

(subring.stabilizer, that is. Or it may be the centraliser instead, now that I think about it...)

Last updated: Dec 20 2023 at 11:08 UTC