[JX-Mo]

We propose a canonical type Center attached to any magma (a type M with Mul M), providing an alternative approach unifying various center subtypes API.

The main engineer work is to equip Center with the correct instance for variant [foo M] and we end up with rfl for all desired simp lemmas, no diamond.

We also provide some functoriality for Foo = Monoid/Ring/Alg

1. Center.fooHom for the embedding
2. FooEquiv.toCenter for restricring isomorphisms to their centers

Update: it turns out that we need Subgroup.center crucially and Subring.center for DivisionRing. Others can probably switch ot Center without pain if we ever want.

Zulip discussion: #mathlib4 > Center unification @ 💬

---

• awaiting-zulip: #mathlib4 > Center unification @ 💬

[JX-Mo]

!radar

[leanprover-radar]

Benchmark results for 2bfbaf4 against a88727a are in. There are significant results. @JX-Mo

• 🟥 main exited with code 1

No significant changes detected.

[github-actions]

PR summary 07dcdc10a3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ Center
+ Center.toMulOpposite
+ _root_.AlgEquiv.toCenter
+ _root_.Center.algHom
+ _root_.Center.coe_add
+ _root_.Center.coe_algebraMap
+ _root_.Center.coe_algebraMap_self
+ _root_.Center.coe_div
+ _root_.Center.coe_intCast
+ _root_.Center.coe_inv
+ _root_.Center.coe_inv'
+ _root_.Center.coe_natCast
+ _root_.Center.coe_neg
+ _root_.Center.coe_npow
+ _root_.Center.coe_nsmul
+ _root_.Center.coe_smul
+ _root_.Center.coe_smul_self
+ _root_.Center.coe_star
+ _root_.Center.coe_sub
+ _root_.Center.coe_zero
+ _root_.Center.coe_zpow
+ _root_.Center.coe_zsmul
+ _root_.Center.nonUnitalRingHom
+ _root_.Center.range_subtype_eq_top
+ _root_.Center.ringHom
+ _root_.Center.smul_def
+ _root_.Center.subtype_surjective
+ _root_.Center.toMulOppositeAlgEquiv
+ _root_.Center.toMulOppositeRingEquiv
+ _root_.MulEquiv.toCenter
+ _root_.RingEquiv.toCenter
+ coe_mul
+ coe_one
+ comm
+ eq_iff
+ ext_coe
+ instance (R) [NonUnitalNonAssocSemiring R] [StarRing R] : StarRing (Center R)
+ instance (R) [NonUnitalRing R] : NonUnitalCommRing (Center R)
+ instance : Algebra R (Center A) := inferInstanceAs <| Algebra R (center R A)
+ instance : Algebra R (Center Aᵐᵒᵖ)
+ instance : CommGroup (Center G) := inferInstanceAs <| CommGroup (center G)
+ instance : CommGroup (center G)
+ instance : CommMonoid (Center M)
+ instance : Field (Center K) := inferInstanceAs <| Field (center K)
+ instance : FunLike (Center (CentroidHom α)) α α
+ instance : NonAssocCommSemiring (Center R)
+ instance : NonUnitalNonAssocCommRing (Center R)
+ instance : NonUnitalNonAssocCommSemiring (Center R)
+ instance : Star (Center (CentroidHom α))
+ instance : StarMul (Center R)
+ instance : StarRing (Center (CentroidHom α))
+ instance [AddCommMonoid α] [Module R' α] : Module (Center R') α
+ instance [AddMonoid α] [DistribMulAction R' α] : DistribMulAction (Center R') α
+ instance [Monoid α] [MulDistribMulAction R' α] : MulDistribMulAction (Center R') α
+ instance [Mul M] : CoeOut (Center M) M := ⟨Subtype.val⟩
+ instance [Mul M] : CommMagma (Center M)
+ instance [MulAction R' α] : MulAction (Center R') α
+ instance [MulOneClass M] : MulOneClass (Center M)
+ instance [SMul R' α] : SMul (Center R') α := inferInstanceAs <| SMul (center R') α
+ instance [SMul R' α] [FaithfulSMul R' α] : FaithfulSMul (Center R') α
+ instance [SMul R' β] [SMul α β] [SMulCommClass R' α β] : SMulCommClass (Center R') α β
+ instance [SMul α β] [SMul R' α] [SMul R' β] [IsScalarTower R' α β] : IsScalarTower (Center R') α β
+ instance [SMul α β] [SMul R' β] [SMulCommClass α R' β] : SMulCommClass α (Center R') β
+ instance [Semiring α] [MulSemiringAction R' α] : MulSemiringAction (Center R') α
+ instance [Zero α] [MulActionWithZero R' α] : MulActionWithZero (Center R') α
+ instance [Zero α] [SMulWithZero R' α] : SMulWithZero (Center R') α
+ instance {M α : Type*} [Monoid M] [MulAction M α] : MulAction (Center M) α
+ instance {M} [Semigroup M] : CommSemigroup (Center M)
+ instance {R : Type*} [NonUnitalSemiring R] : NonUnitalCommSemiring (Center R)
+ instance {R : Type*} [Ring R] : CommRing (Center R)
+ instance {R : Type*} [Semiring R] : Algebra (Center R) R
+ instance {R M : Type*} [Ring R] [MulAction R M] : SMulCommClass (center R) R M
+ instance {R M : Type*} [Ring R] [MulAction R M] : SMulCommClass R (center R) M
+ instance {R M : Type*} [Semiring R] [MulAction R M] : SMulCommClass (Center R) R M
+ instance {R M : Type*} [Semiring R] [MulAction R M] : SMulCommClass R (Center R) M
+ instance {R} [Semiring R] : CommSemiring (Center R)
+ instance {α : Type*} [MulAction M α] : SMulCommClass (Center M) M α
+ instance {α : Type*} [MulAction M α] : SMulCommClass M (Center M) α
+ mk
+ monoidHom
+ mul_assoc'
+ npow_mem_center
+ range_subtype
+ subtype
+ subtype_injective
+-++++---- centerToMulOpposite
- center.smulCommClass_left
- center.smulCommClass_right
- instNonUnitalCommRing
- instNonUnitalCommSemiring
- instance : FunLike (Subsemiring.center (CentroidHom α)) α α
- instance : Star (Subsemiring.center (CentroidHom α))
- instance : StarRing (Subsemiring.center (CentroidHom α))
-++++---+- centerCongr
-- instance {R M : Type*} [Ring R] [MulAction R M] :

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 07dcdc1).

• +132 new declarations
• −7 removed declarations

+AddCenter
+AddCenter.addMonoidHom
+AddCenter.addMonoidHom_apply
+AddCenter.add_assoc'
+AddCenter.coe_add
+AddCenter.coe_neg
+AddCenter.coe_nsmul
+AddCenter.coe_zero
+AddCenter.coe_zsmul
+AddCenter.comm
+AddCenter.eq_iff
+AddCenter.ext_coe
+AddCenter.ext_coe_iff
+AddCenter.instAddCommMagma
+AddCenter.instAddZeroClass
+AddCenter.instCoeOut
+AddCenter.mk
+AddCenter.range_subtype
+AddCenter.range_subtype_eq_top
+AddCenter.subtype
+AddCenter.subtype_injective
+AddCenter.subtype_surjective
+AddCenter.toAddOpposite
+AddCenter.toAddOpposite_apply_coe
+AddCenter.toAddOpposite_symm_apply_coe
+AddEquiv.toCenter
+AddSubgroup.instAddCommGroupCenter
+AddSubgroup.instAddCommGroupSubtypeMemCenter
+AddSubmonoid.instAddCommMonoidCenter
+AddSubsemigroup.instAddCommSemigroupCenter
+AlgEquiv.toCenter
+AlgEquiv.toCenter_apply_coe
+AlgEquiv.toCenter_symm_apply_coe
+Algebra.instCenter
+Center
+Center.algHom
+Center.algHom_apply
+Center.coe_add
+Center.coe_algebraMap
+Center.coe_algebraMap_self
+Center.coe_div
+Center.coe_intCast
+Center.coe_inv
+Center.coe_inv'
+Center.coe_mul
+Center.coe_natCast
+Center.coe_neg
+Center.coe_npow
+Center.coe_nsmul
+Center.coe_one
+Center.coe_smul
+Center.coe_smul_self
+Center.coe_star
+Center.coe_sub
+Center.coe_zero
+Center.coe_zpow
+Center.coe_zsmul
+Center.comm
+Center.eq_iff
+Center.ext_coe
+Center.ext_coe_iff
+Center.instCoeOut
+Center.instCommMagma
+Center.instMulOneClass
+Center.mk
+Center.mk.congr_simp
+Center.monoidHom
+Center.monoidHom_apply
+Center.mul_assoc'
+Center.nonUnitalRingHom
+Center.nonUnitalRingHom_apply
+Center.range_subtype
+Center.range_subtype_eq_top
+Center.ringHom
+Center.ringHom_apply
+Center.smul_def
+Center.subtype
+Center.subtype_injective
+Center.subtype_surjective
+Center.toMulOpposite
+Center.toMulOppositeAlgEquiv
+Center.toMulOppositeAlgEquiv_apply_coe
+Center.toMulOppositeAlgEquiv_symm_apply_coe
+Center.toMulOppositeRingEquiv
+Center.toMulOppositeRingEquiv_apply_coe
+Center.toMulOppositeRingEquiv_symm_apply_coe
+Center.toMulOpposite_apply_coe
+Center.toMulOpposite_symm_apply_coe
+CentroidHom.instFunLikeCenter
-CentroidHom.instFunLikeSubtypeMemSubsemiringCenter
+CentroidHom.instStarCenter
+CentroidHom.instStarRingCenter
-CentroidHom.instStarRingSubtypeMemSubsemiringCenter
-CentroidHom.instStarSubtypeMemSubsemiringCenter
+MulEquiv.toCenter
+MulEquiv.toCenter_apply_coe
+MulEquiv.toCenter_symm_apply_coe
-NonUnitalStarSubalgebra.instNonUnitalCommRing
-NonUnitalStarSubalgebra.instNonUnitalCommSemiring
+NonUnitalStarSubsemiring.instStarRingCenter
+NonUnitalSubring.instNonUnitalCommRingCenter
+NonUnitalSubring.instNonUnitalNonAssocCommRingCenter
+NonUnitalSubsemiring.instNonUnitalCommSemiringCenter
+NonUnitalSubsemiring.instNonUnitalNonAssocCommSemiringCenter
+RingEquiv.toCenter
+RingEquiv.toCenter_apply_coe
+RingEquiv.toCenter_symm_apply_coe
+Set.npow_mem_center
+Set.nsmul_mem_addCenter
+Subalgebra.instAlgebraCenter
+Subalgebra.instAlgebraCenterMulOpposite
+Subgroup.instCommGroupCenter
+Subgroup.instCommGroupSubtypeMemCenter
+Submonoid.instCommMonoidCenter
+Submonoid.instMulActionCenter
+Submonoid.instSMulCommClassCenter
+Submonoid.instSMulCommClassCenter_1
-Subring.center.smulCommClass_left
-Subring.center.smulCommClass_right
+Subring.instCommRingCenter
+Subring.instFieldCenter
+Subsemigroup.instCommSemigroupCenter
+Subsemiring.instCommSemiringCenter
+Subsemiring.instDistribMulActionCenter
+Subsemiring.instFaithfulSMulCenter
+Subsemiring.instIsScalarTowerCenter
+Subsemiring.instModuleCenter
+Subsemiring.instMulActionCenter
+Subsemiring.instMulActionWithZeroCenter
+Subsemiring.instMulDistribMulActionCenter
+Subsemiring.instMulSemiringActionCenter
+Subsemiring.instNonAssocCommSemiringCenter
+Subsemiring.instSMulCenter
+Subsemiring.instSMulCommClassCenter
+Subsemiring.instSMulCommClassCenter_1
+Subsemiring.instSMulCommClassCenter_2
+Subsemiring.instSMulCommClassCenter_3
+Subsemiring.instSMulWithZeroCenter
+instStarMulCenter

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 07dcdc10a3
Reference commit 3aae103a67

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[JX-Mo]

!radar

[leanprover-radar]

Benchmark results for 26f9013 against c5945d8 are in. There are significant results. @JX-Mo

• 🟥 main exited with code 1

No significant changes detected.

[JX-Mo]

WIP

[JX-Mo]

!radar

[leanprover-radar]

Benchmark results for a98b1fd against c5945d8 are in. There are significant results. @JX-Mo

• 🟥 main exited with code 1

No significant changes detected.

[JX-Mo]

!radar

[leanprover-radar]

Benchmark results for 8ac1644 against c5945d8 are in. No significant results found. @JX-Mo

• 🟥 build//instructions: +17.2G (+0.02%)

Medium changes (2✅)

• ✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -2.4G (-5.95%) (reduced significance based on absolute threshold)
• ✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -2.9G (-5.22%) (reduced significance based on absolute threshold)

Small changes (24✅, 44🟥)

• 68 hidden