mathlib

mathlib copied to clipboard

Define the centroid of a (non-unital, non-associative) semiring and shows that it forms a semiring. The centroid of a (non-unital, non-associative) ring is a ring.

When the ring is prime, the centroid is commutative.

Co-authored-by: Yaël Dillies [email protected]

---

• [x] depends on #15839

More general results are possible, but would require two sided ideals of non-unital, non-associative semirings, which has not yet been developed.

@Vierkantor, @eric-wieser, @YaelDillies : I think Christopher is still waiting on a decision about whether or not to use old_structure_cmd.

I think the ball was in @YaelDillies' court (https://github.com/leanprover-community/mathlib/pull/12746#discussion_r846250593), but perhaps we shouldn't be waiting since we have two maintainer votes for old_structure_cmd and plenty of time for Yaël to respond.

@mans0954 , do you want to make these changes then? If you don't have time I can knock them out for you soon. Just say the word.

Something seems to have changed with to_End_injective.semiring - possibly connected with #12182?

/- The `doc_blame` linter reports: -/
/- DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- algebra/hom/centroid.lean
#check @centroid_hom.to_add_monoid_hom /- def missing doc string -/
Error: centroid_hom.to_add_monoid_hom - def missing doc string
Error: Process completed with exit code 1.

Where do I need to add a doc string?

/- The `doc_blame` linter reports: -/
/- DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- algebra/hom/centroid.lean
#check @centroid_hom.to_add_monoid_hom /- def missing doc string -/
Error: centroid_hom.to_add_monoid_hom - def missing doc string
Error: Process completed with exit code 1.

Is this a bug? I found only one other case: https://github.com/leanprover-community/mathlib/blob/741d28519981f307f6f2621b44cb2156792c184a/src/algebra/order/absolute_value.lean#L32

/- The `doc_blame` linter reports: -/
/- DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- algebra/hom/centroid.lean
#check @centroid_hom.to_add_monoid_hom /- def missing doc string -/
Error: centroid_hom.to_add_monoid_hom - def missing doc string
Error: Process completed with exit code 1.

Is this a bug? I found only one other case:

https://github.com/leanprover-community/mathlib/blob/741d28519981f307f6f2621b44cb2156792c184a/src/algebra/order/absolute_value.lean#L32

Thanks - that seems to have worked around it.

@eric-wieser Are you able to approve this now?

@eric-wieser Sorry to pester you again, but I was wondering if you might have a moment to approve this PR?

Thanks.

This PR has an approval, and all of the comments appear to have been resolved. Please can I have delegated permission to merge it @eric-wieser ?

I'm afraid I'm too time-constrained to refresh myself on the full context here. I don't think I have any major concerns here, so I'm happy to delegate to another maintainer (@jcommelin?) to give it a final pass.

The only thing that immediately comes to mind is the recent discussion on Zulip that mentioned this PR, which suggested another possible name for the objects described here, which might have more backing in literature. That's squarely outside my background though, so even if I could locate the thread, I'm in no place to make a call on it.

At any rate, names are easy to change later, and the current name is certainly good enough for now.

Here is the thread.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests