feat: algebraic hierarchy on DirectLimit (#19893)

**Order/DirectedInverseSystem.lean**: define the DirectLimit of a DirectedSystem of types as a quotient (by a setoid (equivalence relation)) of the Sigma type (disjoint union). Provide the `induction` lemmas and `map`/`lift` constructions used to define algebraic operations on DirectLimit.

New file **Algebra/Colimit/DirectLimit.lean**: the first 400 lines are boilerplate code that defines algebraic instances on DirectLImit from magma (Mul) to Field. To make everything "hom-polymorphic", the DirectedSystem consists of FunLikes rather than plain/unbundled functions, and we use algebraic hom typeclasses (e.g. LinearMapClass, RingHomClass) everywhere. The remaining 70 lines essentially shows that DirectLimit is the colimit in the categories of Module and Ring.

**Algebra/DirectLimit.lean**: renamed to **Algebra/Colimit/ModuleRing.lean**. This file was originally added @kckennylau 5 years ago in [mathlib3#754](leanprover-community/mathlib3#754) and defines `Module.DirectLimit` and `Ring.DirectLimit` as quotients of the universal objects (DirectSum and FreeCommRing). This definition is more general and suitable for arbitrary colimits, but makes it very cumbersome to prove [`of.zero_exact`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/DirectLimit.html#Ring.DirectLimit.of.zero_exact) lemmas (130+ lines!); for DirectLimit constructed as quotients of the disjoint union, these are just by definition. We golf these proofs by constructing isomorphisms between `Module/Ring.DirectLimit` and `_root_.DirectLimit`. I have more work done that generalizes most lemmas there to work for arbitrary colimits, that's why I put it under a new Colimit directory.

**Data/Int/Cast/Lemmas.lean**: add `map_intCast'`
**Data/Nat/Cast/Basic.lean**: golf a lemma
**Order/Directed.lean**: add a lemma
**ModelTheory/DirectLimit.lean**: change two lemmas to aliases of the general FunLike lemmas

Author: alreadydone

Mathlib.lean

@@ -181,6 +181,8 @@ import Mathlib.Algebra.CharZero.Defs
 import Mathlib.Algebra.CharZero.Infinite
 import Mathlib.Algebra.CharZero.Lemmas
 import Mathlib.Algebra.CharZero.Quotient
+import Mathlib.Algebra.Colimit.DirectLimit
+import Mathlib.Algebra.Colimit.ModuleRing
 import Mathlib.Algebra.ContinuedFractions.Basic
 import Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
 import Mathlib.Algebra.ContinuedFractions.Computation.Approximations
@@ -194,7 +196,6 @@ import Mathlib.Algebra.ContinuedFractions.Determinant
 import Mathlib.Algebra.ContinuedFractions.TerminatedStable
 import Mathlib.Algebra.ContinuedFractions.Translations
 import Mathlib.Algebra.CubicDiscriminant
-import Mathlib.Algebra.DirectLimit
 import Mathlib.Algebra.DirectSum.AddChar
 import Mathlib.Algebra.DirectSum.Algebra
 import Mathlib.Algebra.DirectSum.Basic

Mathlib/Algebra/Category/ModuleCat/Limits.lean

@@ -5,7 +5,7 @@ Authors: Kim Morrison
 -/
 import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.Algebra.Category.Grp.Limits
-import Mathlib.Algebra.DirectLimit
+import Mathlib.Algebra.Colimit.ModuleRing
 
 /-!
 # The category of R-modules has all limits
@@ -221,7 +221,7 @@ def directLimitDiagram : ι ⥤ ModuleCat R where
   map_comp hij hjk := by
     ext
     symm
-    apply Module.DirectedSystem.map_map
+    apply Module.DirectedSystem.map_map f
 
 variable [DecidableEq ι]
 
@@ -243,7 +243,7 @@ in the sense of `CategoryTheory`. -/
 @[simps]
 def directLimitIsColimit [IsDirected ι (· ≤ ·)] : IsColimit (directLimitCocone G f) where
   desc s := ofHom <|
-    DirectLimit.lift R ι G f (fun i => (s.ι.app i).hom) fun i j h x => by
+    Module.DirectLimit.lift R ι G f (fun i => (s.ι.app i).hom) fun i j h x => by
       simp only [Functor.const_obj_obj]
       rw [← s.w (homOfLE h)]
       rfl