feat(Algebra/Colimit/DirectLimit): add star structures (Star, StarRing, etc.) on DirectLimit

[drocta]

add Star, InvolutiveStar, StarMul, StarAddMonoid, StarRing, and StarModule instances to DirectLimit, following the pattern of existing algebraic structures in Mathlib.Algebra.Colimit.DirectLimit.
also add the universal property API (of, lift, hom_ext, of_f, lift_of) for StarRing.

---

Use of AI:
I did make some use of ChatGPT for some advice while writing this code, as well as the auto-complete built into VS Code. However, I can personally vouch for all of the code I am submitting, and that I understand all of it.

This is the first part of my project towards supporting direct limits of $C^*$-algebras (as I described on Zulip ).

This PR adds an import of Mathlib.Algebra.Star.StarRingHom to Mathlib.Algebra.Colimit.DirectLimit, because it needs it.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary ee3a5404e5

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Colimit.DirectLimit	551	558	+7 (+1.27%)

Import changes for all files

Files	Import difference
49 files Mathlib.Algebra.Azumaya.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Central.TensorProduct Mathlib.Condensed.AB Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Module Mathlib.Condensed.EffectiveEpi Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.EffectiveEpi Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.InternallyProjective Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.Monoidal Mathlib.Condensed.Light.Sequence Mathlib.Condensed.Light.Small Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.LinearAlgebra.LinearDisjoint Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.Bialgebra.GroupLike Mathlib.RingTheory.Coalgebra.GroupLike Mathlib.RingTheory.Extension.Cotangent.BaseChange Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.Domain Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.Flat.Tensor Mathlib.RingTheory.HopfAlgebra.GroupLike Mathlib.RingTheory.Ideal.CotangentBaseChange Mathlib.RingTheory.LocalProperties.InjectiveDimension Mathlib.RingTheory.LocalProperties.ProjectiveDimension Mathlib.RingTheory.PolynomialLaw.Basic Mathlib.RingTheory.Regular.Category Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Successor	1
95 files Mathlib.Algebra.Category.AlgCat.Limits Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting Mathlib.Algebra.Category.ModuleCat.Ext.Finite Mathlib.Algebra.Category.ModuleCat.Ext.HasExt Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Localization Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Stalk Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Algebra.Category.ModuleCat.Ulift Mathlib.Algebra.Colimit.Finiteness Mathlib.Algebra.Colimit.Module Mathlib.Algebra.Colimit.Ring Mathlib.Algebra.Colimit.TensorProduct Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective Mathlib.Algebra.Homology.DerivedCategory.KInjective Mathlib.Algebra.Homology.DerivedCategory.KProjective Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Injective.Ext Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Ext Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.Morita.Matrix Mathlib.RingTheory.TensorProduct.DirectLimitFG Mathlib.Topology.Sheaves.Abelian Mathlib.Topology.Sheaves.AddCommGrpCat Mathlib.Topology.Sheaves.Flasque Mathlib.Topology.Sheaves.MayerVietoris	3
Mathlib.Algebra.Colimit.DirectLimit	7

---

Declarations diff

+ instance : InvolutiveStar (DirectLimit G f)
+ instance : Star (DirectLimit G f)
+ instance : StarAddMonoid (DirectLimit G f)
+ instance : StarMul (DirectLimit G f)
+ instance [Star R] [∀ i, Star (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)]
+ instance [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)]
+ star_def
++ hom_ext
++ lift
++ lift_of
++ of
++ of_f

You can run this locally as follows

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

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

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

---

No changes to technical debt.

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.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).

[eric-wieser]

I'd perhaps argue we want NonUnital in here somewhere, maybe @j-loreaux has opinions

[drocta]

So, as namespace NonUnitalStarRing?
I'm happy to make that change if desired.
I had used the namespace matching the class name (don't some things care about that? I guess probably not in a way that's relevant here?) but I suppose if in the future there was a structure defined for unital star ring homs, it would help distinguish there. (though I guess they could be in StarRing and UnitalStarRing ?)
Yeah, would be happy to hear opinions about this.

[eric-wieser]

Right, that's my suggestion; but I'll let Jireh make the call.

Arguably what matters here is not the typeclass name, but the type of the morphism.

[j-loreaux]

I agree with Eric. Even though there is no type class called NonUnitalStarRing, it's the morphisms that matter (otherwise you would need StarRing.of and StarRing.of', one for the non-unital morphisms and one for the unital ones). In the Star end of the library, the Star is always a mixin to the types.

The only reason that we don't have unital star ring morphisms is that no one managed to get around to it yet. Likely it had been on Christopher Hoskin's agenda.

[eric-wieser]

This looks pretty good, hopefully my comments aren't much work to address. Thanks for the contribution!

[eric-wieser]

Perhaps this should be converted to a bulleted list of the lifts provided in this module?

[drocta]

Alright. Would you also want the "The first 400 lines are" part of this module docstring updated as well? Is that meant to refer to the part in the first of the two namespace DirectLimit blocks (now ending on line 494) ?

[j-loreaux]

Other than these few comments this looks fine to me.

[j-loreaux]

Suggested change

	[∀ i, StarRing (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)]
	: StarRing (DirectLimit G f) where
	[∀ i, StarRing (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)] :
	StarRing (DirectLimit G f) where

[j-loreaux]

I agree with Eric. Even though there is no type class called NonUnitalStarRing, it's the morphisms that matter (otherwise you would need StarRing.of and StarRing.of', one for the non-unital morphisms and one for the unital ones). In the Star end of the library, the Star is always a mixin to the types.

The only reason that we don't have unital star ring morphisms is that no one managed to get around to it yet. Likely it had been on Christopher Hoskin's agenda.