feat: categorical description of center of a ring #20652

jjaassoonn · 2025-01-11T01:13:54Z

We show the isomorphism between Z(R) and End(1 Mod-R)

depends on:[Merged by Bors] - feat(Algebra): Mul/RingEquivs between center and Module.End #20721

github-actions · 2025-01-11T01:14:45Z

PR summary 75c519e0e5

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Preadditive.Basic	605	609	+4 (+0.66%)
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor	689	693	+4 (+0.58%)

Import changes for all files

Files	Import difference
172 files `Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Algebra.Homology.BifunctorAssociator` `Mathlib.Algebra.Homology.BifunctorFlip` `Mathlib.Algebra.Homology.BifunctorHomotopy` `Mathlib.Algebra.Homology.BifunctorShift` `Mathlib.Algebra.Homology.Bifunctor` `Mathlib.Algebra.Homology.DerivedCategory.Basic` `Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass` `Mathlib.Algebra.Homology.DerivedCategory.HomologySequence` `Mathlib.Algebra.Homology.DerivedCategory.ShortExact` `Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle` `Mathlib.Algebra.Homology.Embedding.CochainComplex` `Mathlib.Algebra.Homology.Embedding.ExtendHomology` `Mathlib.Algebra.Homology.Embedding.Extend` `Mathlib.Algebra.Homology.Embedding.HomEquiv` `Mathlib.Algebra.Homology.Embedding.IsSupported` `Mathlib.Algebra.Homology.Embedding.RestrictionHomology` `Mathlib.Algebra.Homology.Embedding.StupidTrunc` `Mathlib.Algebra.Homology.Embedding.TruncGEHomology` `Mathlib.Algebra.Homology.Embedding.TruncGE` `Mathlib.Algebra.Homology.Embedding.TruncLEHomology` `Mathlib.Algebra.Homology.Embedding.TruncLE` `Mathlib.Algebra.Homology.Factorizations.Basic` `Mathlib.Algebra.Homology.HomologicalComplexAbelian` `Mathlib.Algebra.Homology.HomologySequenceLemmas` `Mathlib.Algebra.Homology.HomologySequence` `Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplex` `Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor` `Mathlib.Algebra.Homology.HomotopyCategory.MappingCone` `Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated` `Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence` `Mathlib.Algebra.Homology.HomotopyCategory.Shift` `Mathlib.Algebra.Homology.HomotopyCategory.ShortExact` `Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors` `Mathlib.Algebra.Homology.HomotopyCategory.Triangulated` `Mathlib.Algebra.Homology.HomotopyCategory` `Mathlib.Algebra.Homology.HomotopyCofiber` `Mathlib.Algebra.Homology.Homotopy` `Mathlib.Algebra.Homology.Linear` `Mathlib.Algebra.Homology.Localization` `Mathlib.Algebra.Homology.Monoidal` `Mathlib.Algebra.Homology.Opposite` `Mathlib.Algebra.Homology.QuasiIso` `Mathlib.Algebra.Homology.Refinements` `Mathlib.Algebra.Homology.ShortComplex.ExactFunctor` `Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex` `Mathlib.Algebra.Homology.SingleHomology` `Mathlib.Algebra.Homology.TotalComplexShift` `Mathlib.Algebra.Homology.TotalComplexSymmetry` `Mathlib.Algebra.Homology.TotalComplex` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.AlgebraicGeometry.IdealSheaf` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.AlgebraicGeometry.Over` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.AlgebraicTopology.AlternatingFaceMapComplex` `Mathlib.AlgebraicTopology.DoldKan.Decomposition` `Mathlib.AlgebraicTopology.DoldKan.Degeneracies` `Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive` `Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian` `Mathlib.AlgebraicTopology.DoldKan.Equivalence` `Mathlib.AlgebraicTopology.DoldKan.Faces` `Mathlib.AlgebraicTopology.DoldKan.FunctorGamma` `Mathlib.AlgebraicTopology.DoldKan.FunctorN` `Mathlib.AlgebraicTopology.DoldKan.GammaCompN` `Mathlib.AlgebraicTopology.DoldKan.Homotopies` `Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence` `Mathlib.AlgebraicTopology.DoldKan.NCompGamma` `Mathlib.AlgebraicTopology.DoldKan.NReflectsIso` `Mathlib.AlgebraicTopology.DoldKan.Normalized` `Mathlib.AlgebraicTopology.DoldKan.Notations` `Mathlib.AlgebraicTopology.DoldKan.PInfty` `Mathlib.AlgebraicTopology.DoldKan.Projections` `Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.CategoryTheory.Abelian.Exact` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory` `Mathlib.CategoryTheory.Abelian.InjectiveResolution` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.CategoryTheory.Abelian.ProjectiveResolution` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.CategoryTheory.Galois.IsFundamentalgroup` `Mathlib.CategoryTheory.Galois.Prorepresentability` `Mathlib.CategoryTheory.Galois.Topology` `Mathlib.CategoryTheory.Monoidal.Subcategory` `Mathlib.CategoryTheory.Monoidal.Tor` `Mathlib.CategoryTheory.Preadditive.InjectiveResolution` `Mathlib.CategoryTheory.Preadditive.ProjectiveResolution` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.CategoryTheory.Shift.Opposite` `Mathlib.CategoryTheory.Shift.ShiftedHomOpposite` `Mathlib.CategoryTheory.Sites.Abelian` `Mathlib.CategoryTheory.Triangulated.Opposite.Basic` `Mathlib.CategoryTheory.Triangulated.Opposite.Functor` `Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated` `Mathlib.CategoryTheory.Triangulated.Opposite.Triangle` `Mathlib.Condensed.Basic` `Mathlib.Condensed.CartesianClosed` `Mathlib.Condensed.Discrete.Basic` `Mathlib.Condensed.Discrete.Colimit` `Mathlib.Condensed.Discrete.LocallyConstant` `Mathlib.Condensed.Equivalence` `Mathlib.Condensed.Functors` `Mathlib.Condensed.Light.Basic` `Mathlib.Condensed.Light.CartesianClosed` `Mathlib.Condensed.Light.Functors` `Mathlib.Condensed.Light.TopCatAdjunction` `Mathlib.Condensed.Light.TopComparison` `Mathlib.Condensed.TopCatAdjunction` `Mathlib.Condensed.TopComparison` `Mathlib.Geometry.Manifold.Sheaf.Basic` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.RingedSpace.Basic` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace` `Mathlib.Geometry.RingedSpace.OpenImmersion` `Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing` `Mathlib.Topology.Category.CompHaus.EffectiveEpi` `Mathlib.Topology.Category.LightProfinite.EffectiveEpi` `Mathlib.Topology.Category.Profinite.EffectiveEpi` `Mathlib.Topology.Category.Stonean.EffectiveEpi` `Mathlib.Topology.Sheaves.CommRingCat`	1
118 files `Mathlib.Algebra.Category.Grp.Adjunctions` `Mathlib.Algebra.Category.Grp.Biproducts` `Mathlib.Algebra.Category.Grp.Colimits` `Mathlib.Algebra.Category.Grp.Kernels` `Mathlib.Algebra.Category.Grp.Limits` `Mathlib.Algebra.Category.Grp.Preadditive` `Mathlib.Algebra.Category.Ring.Constructions` `Mathlib.Algebra.Category.Ring.Limits` `Mathlib.Algebra.Homology.ExactSequence` `Mathlib.Algebra.Homology.ShortComplex.Exact` `Mathlib.Algebra.Homology.ShortComplex.Linear` `Mathlib.Algebra.Homology.ShortComplex.Preadditive` `Mathlib.Algebra.Homology.ShortComplex.ShortExact` `Mathlib.Algebra.Homology.ShortComplex.SnakeLemma` `Mathlib.AlgebraicTopology.MooreComplex` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four` `Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel` `Mathlib.CategoryTheory.Abelian.Opposite` `Mathlib.CategoryTheory.Abelian.Refinements` `Mathlib.CategoryTheory.Abelian.Transfer` `Mathlib.CategoryTheory.Idempotents.SimplicialObject` `Mathlib.CategoryTheory.Linear.LinearFunctor` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive` `Mathlib.CategoryTheory.Localization.Triangulated` `Mathlib.CategoryTheory.Monoidal.Linear` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.CategoryTheory.Preadditive.Mat` `Mathlib.CategoryTheory.Preadditive.Opposite` `Mathlib.CategoryTheory.Preadditive.SingleObj` `Mathlib.CategoryTheory.Preadditive.Transfer` `Mathlib.CategoryTheory.Quotient.Linear` `Mathlib.CategoryTheory.Sites.Coherent.Equivalence` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits` `Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective` `Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit` `Mathlib.CategoryTheory.Sites.Coherent.SheafComparison` `Mathlib.CategoryTheory.Sites.ConstantSheaf` `Mathlib.CategoryTheory.Sites.DenseSubsite.Basic` `Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology` `Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv` `Mathlib.CategoryTheory.Sites.EpiMono` `Mathlib.CategoryTheory.Sites.Equivalence` `Mathlib.CategoryTheory.Sites.LeftExact` `Mathlib.CategoryTheory.Sites.LocallyBijective` `Mathlib.CategoryTheory.Sites.LocallyFullyFaithful` `Mathlib.CategoryTheory.Sites.LocallyInjective` `Mathlib.CategoryTheory.Sites.LocallySurjective` `Mathlib.CategoryTheory.Sites.PreservesLocallyBijective` `Mathlib.CategoryTheory.Sites.Pullback` `Mathlib.CategoryTheory.Triangulated.Functor` `Mathlib.CategoryTheory.Triangulated.HomologicalFunctor` `Mathlib.CategoryTheory.Triangulated.Pretriangulated` `Mathlib.CategoryTheory.Triangulated.Subcategory` `Mathlib.CategoryTheory.Triangulated.TStructure.Basic` `Mathlib.CategoryTheory.Triangulated.TriangleShift` `Mathlib.CategoryTheory.Triangulated.Triangulated` `Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits` `Mathlib.Geometry.RingedSpace.SheafedSpace` `Mathlib.Geometry.RingedSpace.Stalks` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.Invariant` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.RingTheory.Localization.Free` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.RingTheory.RingHomProperties` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.Topology.Sheaves.Alexandrov` `Mathlib.Topology.Sheaves.Forget` `Mathlib.Topology.Sheaves.Functors` `Mathlib.Topology.Sheaves.Limits` `Mathlib.Topology.Sheaves.LocalPredicate` `Mathlib.Topology.Sheaves.LocallySurjective` `Mathlib.Topology.Sheaves.PUnit` `Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts` `Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover` `Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections` `Mathlib.Topology.Sheaves.SheafCondition.Sites` `Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing` `Mathlib.Topology.Sheaves.SheafOfFunctions` `Mathlib.Topology.Sheaves.Sheaf` `Mathlib.Topology.Sheaves.Sheafify` `Mathlib.Topology.Sheaves.Skyscraper` `Mathlib.Topology.Sheaves.Stalks`	2
53 files `Mathlib.Algebra.Homology.Additive` `Mathlib.Algebra.Homology.Augment` `Mathlib.Algebra.Homology.DifferentialObject` `Mathlib.Algebra.Homology.Embedding.Boundary` `Mathlib.Algebra.Homology.Embedding.Restriction` `Mathlib.Algebra.Homology.Functor` `Mathlib.Algebra.Homology.HomologicalBicomplex` `Mathlib.Algebra.Homology.HomologicalComplexBiprod` `Mathlib.Algebra.Homology.HomologicalComplexLimits` `Mathlib.Algebra.Homology.HomologicalComplex` `Mathlib.Algebra.Homology.ImageToKernel` `Mathlib.Algebra.Homology.Single` `Mathlib.Algebra.Homology.Square` `Mathlib.CategoryTheory.Abelian.Subobject` `Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems` `Mathlib.CategoryTheory.Dialectica.Monoidal` `Mathlib.CategoryTheory.Generator.Basic` `Mathlib.CategoryTheory.Generator.Indization` `Mathlib.CategoryTheory.Generator.Presheaf` `Mathlib.CategoryTheory.Generator.Sheaf` `Mathlib.CategoryTheory.Idempotents.HomologicalComplex` `Mathlib.CategoryTheory.Linear.Basic` `Mathlib.CategoryTheory.Linear.FunctorCategory` `Mathlib.CategoryTheory.Localization.SmallShiftedHom` `Mathlib.CategoryTheory.Noetherian` `Mathlib.CategoryTheory.Shift.Pullback` `Mathlib.CategoryTheory.Simple` `Mathlib.CategoryTheory.Sites.Adjunction` `Mathlib.CategoryTheory.Sites.CartesianClosed` `Mathlib.CategoryTheory.Sites.ChosenFiniteProducts` `Mathlib.CategoryTheory.Sites.Coherent.Basic` `Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves` `Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology` `Mathlib.CategoryTheory.Sites.Coherent.Comparison` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology` `Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent` `Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular` `Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves` `Mathlib.CategoryTheory.Sites.Coherent.RegularTopology` `Mathlib.CategoryTheory.Sites.CoverLifting` `Mathlib.CategoryTheory.Sites.CoverPreserving` `Mathlib.CategoryTheory.Sites.Limits` `Mathlib.CategoryTheory.Sites.Localization` `Mathlib.CategoryTheory.Sites.Over` `Mathlib.CategoryTheory.Sites.PreservesSheafification` `Mathlib.CategoryTheory.Sites.SheafHom` `Mathlib.CategoryTheory.Sites.Sheafification` `Mathlib.CategoryTheory.Sites.Subsheaf` `Mathlib.CategoryTheory.Subobject.FactorThru` `Mathlib.CategoryTheory.Subobject.Lattice` `Mathlib.CategoryTheory.Subobject.Limits` `Mathlib.Topology.Category.CompHausLike.EffectiveEpi`	3
38 files `Mathlib.Algebra.Homology.CommSq` `Mathlib.Algebra.Homology.ShortComplex.Abelian` `Mathlib.CategoryTheory.Abelian.Basic` `Mathlib.CategoryTheory.Abelian.FunctorCategory` `Mathlib.CategoryTheory.Abelian.NonPreadditive` `Mathlib.CategoryTheory.Idempotents.Basic` `Mathlib.CategoryTheory.Idempotents.Biproducts` `Mathlib.CategoryTheory.Idempotents.FunctorCategories` `Mathlib.CategoryTheory.Idempotents.FunctorExtension` `Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi` `Mathlib.CategoryTheory.Idempotents.Karoubi` `Mathlib.CategoryTheory.Monoidal.Preadditive` `Mathlib.CategoryTheory.Preadditive.AdditiveFunctor` `Mathlib.CategoryTheory.Preadditive.Basic` `Mathlib.CategoryTheory.Preadditive.Biproducts` `Mathlib.CategoryTheory.Preadditive.EilenbergMoore` `Mathlib.CategoryTheory.Preadditive.EndoFunctor` `Mathlib.CategoryTheory.Preadditive.FunctorCategory` `Mathlib.CategoryTheory.Preadditive.LeftExact` `Mathlib.CategoryTheory.Quotient.Preadditive` `Mathlib.CategoryTheory.Shift.InducedShiftSequence` `Mathlib.CategoryTheory.Shift.ShiftSequence` `Mathlib.CategoryTheory.Shift.ShiftedHom` `Mathlib.CategoryTheory.Sites.Canonical` `Mathlib.CategoryTheory.Sites.CompatiblePlus` `Mathlib.CategoryTheory.Sites.CompatibleSheafification` `Mathlib.CategoryTheory.Sites.ConcreteSheafification` `Mathlib.CategoryTheory.Sites.Continuous` `Mathlib.CategoryTheory.Sites.Coverage` `Mathlib.CategoryTheory.Sites.CoversTop` `Mathlib.CategoryTheory.Sites.IsSheafOneHypercover` `Mathlib.CategoryTheory.Sites.OneHypercover` `Mathlib.CategoryTheory.Sites.Plus` `Mathlib.CategoryTheory.Sites.Sheaf` `Mathlib.CategoryTheory.Sites.Subcanonical` `Mathlib.CategoryTheory.Sites.Types` `Mathlib.CategoryTheory.Sites.Whiskering` `Mathlib.CategoryTheory.Triangulated.Rotate`	4
`Mathlib.Algebra.Category.Ring.Center` (new file)	1202

Declarations diff

+ Functor.FullyFaithful.ringEquivEnd
+ Iso.conjRingEquiv
+ RingEquiv.ofModuleCatEquiv
+ Subring.centerEquivEndIdFunctor
+ Subring.centerEquivEndIdFunctorAux
+ Subring.centerEquivOfModuleCatEquiv
+ endMonoidEquiv
+ endRingEquiv
+ instance (e : C ≌ D) : (e.congrLeft (E := E)).functor.Additive
+ instance (e : D ≌ E) [e.functor.Additive] : (e.congrRight (E := C)).functor.Additive
+ instance (f : C ⥤ D) : ((whiskeringLeft C D E).obj f).Additive
+ instance (f : D ⥤ E) [f.Additive] : ((whiskeringRight C D E).obj f).Additive
+ instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
+ instance {R S} [Ring R] [Ring S] (e : R ≃+* S) :
+ of
- conj_apply

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
1406	1	erw

Current commit 75c519e0e5
Reference commit 3c77579087

You can run this locally as

./scripts/technical-debt-metrics.sh 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).

Mathlib/Algebra/Category/Ring/Center.lean

jjaassoonn · 2025-01-11T01:47:30Z

Maybe the location of this file is wrong, after all it did not use any RingCat

Mathlib/Algebra/Category/Ring/Center.lean

…ity/mathlib4 into zjj/center_cat

Mathlib/CategoryTheory/Endomorphism.lean

…er_cat

alreadydone · 2025-02-03T21:37:00Z

Thanks 🎉
maintainer merge

github-actions · 2025-02-03T21:37:16Z

🚀 Pull request has been placed on the maintainer queue by alreadydone.

Mathlib/CategoryTheory/Conj.lean

Mathlib/Algebra/Category/Ring/Center.lean

jcommelin · 2025-02-04T08:20:47Z

Mathlib/Algebra/Category/Ring/Center.lean

+
+open CategoryTheory
+
+/--


Could you please add the equivalence of linear categories between ModuleCat.{v} R and ModuleCat.{v} (Shrink.{v} R)?
Then you can use that together with your Equivalence.endRingEquiv that you add in the other file to golf the ring isomorphism below.

I think I have done what you want, can you check if this is what you mean please?

Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib/Algebra/Category/Ring/Center.lean

jcommelin · 2025-02-04T14:52:02Z

Mathlib/Algebra/Category/Ring/Center.lean

+    simpa using mul_smul x.1 y.1 m
+  map_add' x y := by
+    apply NatTrans.ext
+    ext M (m : M)
+    simpa using add_smul x.1 y.1 m


These proofs are hiding some heavy rfls, as witnessed by the erws below

Suggested change

simpa using mul_smul x.1 y.1 m

map_add' x y := by

apply NatTrans.ext

ext M (m : M)

simpa using add_smul x.1 y.1 m

simp

erw [End.mul_def] -- why is this simp lemma not firing?

simp

exact mul_smul x y m

map_add' x y := by

apply NatTrans.ext

ext M (m : M)

simp

erw [NatTrans.app_add] -- why is this simp lemma not firing?

simp

exact add_smul x y m

erw [NatTrans.app_add] -- why is this simp lemma not firing?

Strangely, this does not require erw, rw actually works, but simp does not fire nonetheless

Probably this issue.

Mathlib/Algebra/Category/Ring/Center.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

…ity/mathlib4 into zjj/center_cat

Co-authored-by: Johan Commelin <johan@commelin.net>

…ity/mathlib4 into zjj/center_cat

jjaassoonn · 2025-02-04T15:52:12Z

Given #20640, I wonder if I should upgrade everything to algebra

initial

0509776

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 11, 2025

relax univ a bit

f490cd6

jjaassoonn added the t-category-theory Category theory label Jan 11, 2025

much more universe freedom

bb18894

jjaassoonn commented Jan 11, 2025

View reviewed changes

Mathlib/Algebra/Category/Ring/Center.lean Outdated Show resolved Hide resolved

shake

188a38d

qawbecrdtey requested changes Jan 11, 2025

View reviewed changes

Mathlib/Algebra/Category/Ring/Center.lean Outdated Show resolved Hide resolved

minimizr imoort

5dfca56

jjaassoonn requested review from alreadydone, kbuzzard, erdOne, Whysoserioushah and qawbecrdtey January 11, 2025 13:15

alreadydone reviewed Jan 11, 2025

View reviewed changes

Mathlib/Algebra/Category/Ring/Center.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Category/Ring/Center.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Category/Ring/Center.lean Outdated Show resolved Hide resolved

zjj and others added 6 commits January 13, 2025 06:35

change to small

18a4746

Merge branch 'zjj/center_cat' of https://github.com/leanprover-commun…

c1ce126

…ity/mathlib4 into zjj/center_cat

noncomputable

5ffaaaf

long line

11e34ed

factor

a55712c

Update AdditiveFunctor.lean

1c4ed3f

alreadydone reviewed Jan 13, 2025

View reviewed changes

Mathlib/CategoryTheory/Endomorphism.lean Outdated Show resolved Hide resolved

zjj and others added 3 commits January 13, 2025 17:57

shorten

3e05bce

feat(Algebra): RingEquivs between center and Module.End

bd08deb

golfs

5971b5d

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 26, 2025

Merge remote-tracking branch 'origin/master' into zjj/center_cat

165390e

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 31, 2025

zjj and others added 3 commits February 3, 2025 20:17

Merge commit 'c3cf924568a06a14be484ac12f3639b3efbd46a5' into zjj/cent…

1455ec7

…er_cat

shake

8186ad6

Discard changes to Mathlib/CategoryTheory/SingleObj.lean

9a76697

github-actions bot added the maintainer-merge label Feb 3, 2025

kbuzzard reviewed Feb 3, 2025

View reviewed changes

Mathlib/CategoryTheory/Conj.lean Outdated Show resolved Hide resolved

jcommelin reviewed Feb 4, 2025

View reviewed changes

Mathlib/Algebra/Category/Ring/Center.lean Outdated Show resolved Hide resolved

jcommelin reviewed Feb 4, 2025

View reviewed changes

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed maintainer-merge labels Feb 4, 2025

zjj and others added 3 commits February 4, 2025 11:44

up to natural isomorphism

1545354

Update Mathlib/Algebra/Category/Ring/Center.lean

385e779

Co-authored-by: Johan Commelin <johan@commelin.net>

apply suggestion from @jcommelin

ecb3552

jjaassoonn removed the awaiting-author A reviewer has asked the author a question or requested changes label Feb 4, 2025

jcommelin reviewed Feb 4, 2025

View reviewed changes

zjj and others added 2 commits February 4, 2025 14:54

generalize

5f15487

Update Mathlib/Algebra/Category/Ring/Center.lean

a75956a

Co-authored-by: Johan Commelin <johan@commelin.net>

jjaassoonn added the awaiting-author A reviewer has asked the author a question or requested changes label Feb 4, 2025

jjaassoonn and others added 9 commits February 4, 2025 14:58

Update Mathlib/Algebra/Category/Ring/Center.lean

3ecc821

Co-authored-by: Johan Commelin <johan@commelin.net>

asd

69cc9e5

Merge branch 'zjj/center_cat' of https://github.com/leanprover-commun…

4d07d2f

…ity/mathlib4 into zjj/center_cat

Update Mathlib/Algebra/Category/Ring/Center.lean

6a745d9

Co-authored-by: Johan Commelin <johan@commelin.net>

fix

1490ed6

Merge branch 'zjj/center_cat' of https://github.com/leanprover-commun…

394953e

…ity/mathlib4 into zjj/center_cat

test

b980e8f

shake

c4c14ea

simp to simp only

75c519e

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 13, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: categorical description of center of a ring #20652

feat: categorical description of center of a ring #20652

jjaassoonn commented Jan 11, 2025 •

edited by Whysoserioushah

Loading

github-actions bot commented Jan 11, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

jjaassoonn commented Jan 11, 2025

alreadydone commented Feb 3, 2025

github-actions bot commented Feb 3, 2025

jcommelin Feb 4, 2025

jjaassoonn Feb 4, 2025

jcommelin Feb 4, 2025

jjaassoonn Feb 4, 2025

alreadydone Feb 4, 2025

jjaassoonn commented Feb 4, 2025


		open CategoryTheory

		/--

feat: categorical description of center of a ring #20652

Are you sure you want to change the base?

feat: categorical description of center of a ring #20652

Conversation

jjaassoonn commented Jan 11, 2025 • edited by Whysoserioushah Loading

github-actions bot commented Jan 11, 2025 • edited Loading

PR summary 75c519e0e5

Import changes for modified files

Declarations diff

jjaassoonn commented Jan 11, 2025

alreadydone commented Feb 3, 2025

github-actions bot commented Feb 3, 2025

jcommelin Feb 4, 2025

Choose a reason for hiding this comment

jjaassoonn Feb 4, 2025

Choose a reason for hiding this comment

jcommelin Feb 4, 2025

Choose a reason for hiding this comment

jjaassoonn Feb 4, 2025

Choose a reason for hiding this comment

alreadydone Feb 4, 2025

Choose a reason for hiding this comment

jjaassoonn commented Feb 4, 2025

jjaassoonn commented Jan 11, 2025 •

edited by Whysoserioushah

Loading

github-actions bot commented Jan 11, 2025 •

edited

Loading