[Merged by Bors] - feat(Algebra/Colimit/DirectLimit): add Algebra structure for DirectLimit

[drocta]

add Algebra instance to DirectLimit. also add a few lemmas for it for the algebra map, and also define the of, lift, and the of_f, lift_of and hom_ext lemmas for it.

---

Use of AI:
I again made some use of ChatGPT for some advice while writing this code, as well as the auto-complete in VS Code.
However, I can personally vouch for all of these contributions, and that I understand all of it.

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

This PR adds an import of Mathlib.Algebra.Algebra.Hom (because it needs AlgHom and AlgHomClass ) in addition to the import of Mathlib.Algebra.Star.StarRingHom added in PR #38308 . In the next PR I intend to make, these two should be replaced with an import of Mathlib.Algebra.Star.StarAlgHom .

[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 ea11ccc0c5

Import changes exceeding 2%

%	File
+39.46%	Mathlib.Algebra.Colimit.DirectLimit

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Colimit.DirectLimit	560	781	+221 (+39.46%)

Import changes for all files

Files	Import difference
6 files Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.Ulift Mathlib.Algebra.Homology.LocalCohomology Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.RingTheory.Morita.Matrix Mathlib.RingTheory.Regular.Category	1
Mathlib.Algebra.Category.ModuleCat.Localization	2
81 files 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.Ext.DimensionShifting Mathlib.Algebra.Category.ModuleCat.Ext.HasExt Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Limits 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.Colimit.Finiteness Mathlib.Algebra.Colimit.Module 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.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.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.Topology.Sheaves.Abelian Mathlib.Topology.Sheaves.AddCommGrpCat Mathlib.Topology.Sheaves.Flasque Mathlib.Topology.Sheaves.MayerVietoris	3
Mathlib.Algebra.Colimit.DirectLimit	221

---

Declarations diff

+ algebraMap_def
+ instance : Algebra R (DirectLimit G f)
+ map₀MonoidHom
+ map₀RingHom
+ map₀_algebraMap
+ map₀_mul
+ map₀_one
++ hom_ext
++ lift
++ lift_comp_of
++ lift_of
++ of
++ of_f

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[drocta]

I forgot to update some things to take into account changes in #38440 which made some of the steps here unnecessary. Fixing now.
Edit: fixed now.

[Whysoserioushah]

LGTM!

[eric-wieser]

I realize I led you astray with map₀RingHom earlier, I pushed a simplification

[eric-wieser]

Suggested change

	@[to_additive]
	@[to_additive (attr := simp)]

[drocta]

Will do.
Btw, in map₀ f (1 : ∀ i, G i) = 1, it does still work as just map₀ f 1 = 1, but I thought it was easier to understand what the lemma is saying with the type ascription. Is that alright, or would it be better to omit the type ascription?

[eric-wieser]

I'm a little surprised the linter doesn't reject this attribute; it's not on any of the other lift_ofs, right?

[drocta]

Ah, indeed, it isn't on any of the existing ones. Not sure how I got it into my head to add it here (and in the unital algebra case). I'll take them off.

[eric-wieser]

bors d+

Thanks!

[mathlib-bors]

✌️ drocta can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[drocta]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job