center and centralizer

Stream: mathlib4

[Ruben Van de Velde]

It seems like we've historically ended up with parallel Center and Centralizer modules:

./Mathlib/Algebra/Group/Center.lean
./Mathlib/Algebra/Group/Centralizer.lean
./Mathlib/Algebra/Ring/Center.lean
./Mathlib/Algebra/Ring/Centralizer.lean
./Mathlib/GroupTheory/Subgroup/Center.lean
./Mathlib/GroupTheory/Subgroup/Centralizer.lean
./Mathlib/GroupTheory/Submonoid/Center.lean
./Mathlib/GroupTheory/Submonoid/Centralizer.lean
./Mathlib/GroupTheory/Subsemigroup/Center.lean
./Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

In #13034, Yaël is proposing merging the ones for Group (and splitting out results related to GroupWithZero). Does anyone have thoughts on this?

[Yaël Dillies]

"historically" is a strong word. It's mostly @Kim Morrison's doing

[Josha Dekker]

You've probably done this differently for a good reason, but just for my interest: in the PR, why don't you define center as a special case of centralizer?

[Yaël Dillies]

I am just moving stuff around

[Ruben Van de Velde]

So, @Kim Morrison , thoughts? :)

[Eric Wieser]

Without further context, I'd be inclined to either merge all the pairs or merge none of them, and the former seems like something for a standalone PR.

[Kim Morrison]

What is the reason for merging them? My default is to prefer more smaller files, as usual, but if there's good reason it's not a strong preference.

[Yaël Dillies]

I am splitting off the GroupWithZero results. If I don't merge them, I find myself with four tiny files. If I merge them, I find myself with one short file and one tiny file.

[Yaël Dillies]

There are also no import considerations against merging

[Josha Dekker]

(also, motivated by my previous question: we could refactor center as a special case of centralizer in the future... I guess this gives you some center API for free)

[Yaël Dillies]

Yeah, I don't think there's enough difference mathematicall between center and centralizer to warrant separate files

[Kim Morrison]

Will the later center/centralizer files be similarly tiny? I have no objections to doing the refactor in stages, but would be sad if avoiding tiny files here resulted in large files later. Otherwise, sounds good.

[Yaël Dillies]

• GroupTheory.Subsemigroup: Nothing about GroupWithZero, so no tiny file
• GroupTheory.Submonoid: Nothing about GroupWithZero, so no tiny file
• GroupTheory.Subgroup: A few declarations about GroupWithZero, so two tiny files