From fdbb91fa89968694f0435ca0c5d062f76caddc98 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Thu, 23 Apr 2026 13:43:03 -0700
Subject: [PATCH 01/28] add instance of Algebra for DirectLimit

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 34 ++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 439ddb1bcc85a6..8138ffecf017ff 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Module.LinearMap.Defs
 public import Mathlib.Algebra.Star.StarRingHom
+public import Mathlib.Algebra.Algebra.Hom
 public import Mathlib.Data.Rat.Cast.Defs
 public import Mathlib.Order.DirectedInverseSystem
 public import Mathlib.Tactic.SuppressCompilation
@@ -572,6 +573,39 @@ instance [∀ i, Field (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
   __ : DivisionRing _ := inferInstance
   mul_comm := mul_comm
 
+--TODO: add support for non-unital algebras
+section Algebra
+
+variable [CommSemiring R]
+variable [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)]
+variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
+
+noncomputable def algebraMapAux : R →+* DirectLimit G f where
+  toFun := fun r => ⟦⟨Classical.arbitrary ι, algebraMap R (G (Classical.arbitrary ι)) r⟩⟧
+  map_one' := by rw [algebraMap, RingHom.map_one, one_def]
+  map_mul' := fun r s => by rw [algebraMap, mul_def, map_mul]
+  map_add' := fun r s => by simp only [algebraMap, add_def, map_add]
+  map_zero' := by rw [algebraMap, map_zero, zero_def]
+
+lemma algebraMapAux_at (i : ι) (r : R) :
+    algebraMapAux (R:=R) r
+      = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) := by
+  let j := Classical.arbitrary ι
+  change ⟦⟨j, (algebraMap R (G j)) r⟩⟧ = (⟦⟨i, (algebraMap R (G i)) r⟩⟧ : DirectLimit G f)
+  obtain ⟨k, hik, hjk⟩ := directed_of (α := ι) (· ≤ ·) i j
+  rw [eq_of_le (f := f) ⟨j, (algebraMap R (G j) r)⟩ k hjk]
+  rw [eq_of_le (f := f) ⟨i, (algebraMap R (G i) r)⟩ k hik]
+  simp_rw [AlgHomClass.commutes]
+
+noncomputable instance : Algebra R (DirectLimit G f) where
+  algebraMap := algebraMapAux
+  commutes' r := DirectLimit.induction f fun i _ ↦ by
+    rw [algebraMapAux_at i, mul_def, mul_def, Algebra.commutes]
+  smul_def' r := DirectLimit.induction _ fun i _ => by
+    rw [smul_def, algebraMapAux_at i, mul_def, Algebra.smul_def']; rfl
+
+end Algebra
+
 end DirectLimit
 
 namespace DirectLimit

From 85519eb1ac1dff6e0a5b3689a2fb86f9be3a61d6 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Thu, 23 Apr 2026 13:44:40 -0700
Subject: [PATCH 02/28] add algebraMap_at in Algebra/Colimit/DirectLimit.lean

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 8138ffecf017ff..f982886a19e685 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -604,6 +604,10 @@ noncomputable instance : Algebra R (DirectLimit G f) where
   smul_def' r := DirectLimit.induction _ fun i _ => by
     rw [smul_def, algebraMapAux_at i, mul_def, Algebra.smul_def']; rfl
 
+lemma algebraMap_at (i : ι) (r : R) :
+    algebraMap R (DirectLimit G f) r = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) := by
+  rw [← algebraMapAux_at i]; rfl
+
 end Algebra
 
 end DirectLimit

From e56da434f4be6c02e901384cebbfac01aaa1bf9b Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Thu, 23 Apr 2026 14:02:25 -0700
Subject: [PATCH 03/28] add lift, of, etc. for DirectLimit.Algebra

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 45 ++++++++++++++++++++++++
 1 file changed, 45 insertions(+)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index f982886a19e685..0106a559ad2e21 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -797,4 +797,49 @@ theorem hom_ext {g₁ g₂ : DirectLimit G f →⋆ₙ+* P}
 
 end NonUnitalStarRing
 
+namespace Algebra
+
+variable [CommSemiring R]
+variable [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)]
+variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
+variable [Nonempty ι]
+
+variable (G f) in
+/-- The canonical map from a component to the direct limit. -/
+noncomputable def of (i) : G i →ₐ[R] DirectLimit G f where
+  toFun x := ⟦⟨i, x⟩⟧
+  __ := (DirectLimit.Ring.of G f i)
+  commutes' r := by rw [algebraMap_at i]
+
+@[simp] lemma of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x := .symm <| eq_of_le ..
+
+variable (P : Type*) [Semiring P] [Algebra R P]
+
+variable (G f) in
+/-- The universal property of the direct limit: maps from the components to another R-algebra
+that respect the directed system structure (i.e. make some diagram commute) give rise
+to a unique map out of the direct limit.
+-/
+noncomputable def lift (g : ∀ i, G i →ₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) :
+    DirectLimit G f →ₐ[R] P where
+  toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm
+  __ := DirectLimit.Ring.lift G f P (g:= fun i => (g i).toRingHom) (Hg:=Hg)
+  commutes' r := by
+    let i := Classical.arbitrary ι
+    rw [algebraMap_at i r, lift_def, AlgHom.commutes]
+
+variable (g : ∀ i, G i →ₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
+
+@[simp] theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x := rfl
+
+@[ext]
+theorem hom_ext {g₁ g₂ : DirectLimit G f →ₐ[R] P}
+    (h : ∀ i, g₁.comp (of G f i) = g₂.comp (of G f i)) :
+    g₁ = g₂ := by
+  ext x
+  induction x using DirectLimit.induction with | _ i x
+  exact congr($(h i) x)
+
+end Algebra
+
 end DirectLimit

From 0f0437ab724d66b7666c8aa9ab2b7e17e4a50dde Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Tue, 28 Apr 2026 17:16:31 -0700
Subject: [PATCH 04/28] remove an unnecessary rfl that was causing an error, an
 unused argument to simp, and some unnecessarily explicit noncomputable
 markers

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 0106a559ad2e21..d3f9a9ad145281 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -580,11 +580,11 @@ variable [CommSemiring R]
 variable [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)]
 variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 
-noncomputable def algebraMapAux : R →+* DirectLimit G f where
+def algebraMapAux : R →+* DirectLimit G f where
   toFun := fun r => ⟦⟨Classical.arbitrary ι, algebraMap R (G (Classical.arbitrary ι)) r⟩⟧
   map_one' := by rw [algebraMap, RingHom.map_one, one_def]
   map_mul' := fun r s => by rw [algebraMap, mul_def, map_mul]
-  map_add' := fun r s => by simp only [algebraMap, add_def, map_add]
+  map_add' := fun r s => by simp only [add_def, map_add]
   map_zero' := by rw [algebraMap, map_zero, zero_def]
 
 lemma algebraMapAux_at (i : ι) (r : R) :
@@ -597,12 +597,12 @@ lemma algebraMapAux_at (i : ι) (r : R) :
   rw [eq_of_le (f := f) ⟨i, (algebraMap R (G i) r)⟩ k hik]
   simp_rw [AlgHomClass.commutes]
 
-noncomputable instance : Algebra R (DirectLimit G f) where
+instance : Algebra R (DirectLimit G f) where
   algebraMap := algebraMapAux
   commutes' r := DirectLimit.induction f fun i _ ↦ by
     rw [algebraMapAux_at i, mul_def, mul_def, Algebra.commutes]
   smul_def' r := DirectLimit.induction _ fun i _ => by
-    rw [smul_def, algebraMapAux_at i, mul_def, Algebra.smul_def']; rfl
+    rw [smul_def, algebraMapAux_at i, mul_def, Algebra.smul_def']
 
 lemma algebraMap_at (i : ι) (r : R) :
     algebraMap R (DirectLimit G f) r = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) := by
@@ -806,7 +806,7 @@ variable [Nonempty ι]
 
 variable (G f) in
 /-- The canonical map from a component to the direct limit. -/
-noncomputable def of (i) : G i →ₐ[R] DirectLimit G f where
+def of (i) : G i →ₐ[R] DirectLimit G f where
   toFun x := ⟦⟨i, x⟩⟧
   __ := (DirectLimit.Ring.of G f i)
   commutes' r := by rw [algebraMap_at i]
@@ -820,7 +820,7 @@ variable (G f) in
 that respect the directed system structure (i.e. make some diagram commute) give rise
 to a unique map out of the direct limit.
 -/
-noncomputable def lift (g : ∀ i, G i →ₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) :
+def lift (g : ∀ i, G i →ₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) :
     DirectLimit G f →ₐ[R] P where
   toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm
   __ := DirectLimit.Ring.lift G f P (g:= fun i => (g i).toRingHom) (Hg:=Hg)

From db1e95318591955777beca39cff8f1d891d74a6a Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Tue, 28 Apr 2026 17:54:48 -0700
Subject: [PATCH 05/28] add docstring for algebraMapAux

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index d3f9a9ad145281..ae8e1df2ca0c25 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -580,6 +580,7 @@ variable [CommSemiring R]
 variable [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)]
 variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 
+/-- The algebra map for the DirectLimit of a directed system of algebras -/
 def algebraMapAux : R →+* DirectLimit G f where
   toFun := fun r => ⟦⟨Classical.arbitrary ι, algebraMap R (G (Classical.arbitrary ι)) r⟩⟧
   map_one' := by rw [algebraMap, RingHom.map_one, one_def]

From 5a2bdccc782502e6a644f7e5d57e69797cf30b5e Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Tue, 5 May 2026 13:21:24 -0700
Subject: [PATCH 06/28] apply suggestions from code review (simplifying proofs)

Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>
---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index ae8e1df2ca0c25..626a1efe4ed751 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -582,11 +582,11 @@ variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 
 /-- The algebra map for the DirectLimit of a directed system of algebras -/
 def algebraMapAux : R →+* DirectLimit G f where
-  toFun := fun r => ⟦⟨Classical.arbitrary ι, algebraMap R (G (Classical.arbitrary ι)) r⟩⟧
-  map_one' := by rw [algebraMap, RingHom.map_one, one_def]
-  map_mul' := fun r s => by rw [algebraMap, mul_def, map_mul]
-  map_add' := fun r s => by simp only [add_def, map_add]
-  map_zero' := by rw [algebraMap, map_zero, zero_def]
+  toFun r := ⟦⟨Classical.arbitrary ι, algebraMap R (G (Classical.arbitrary ι)) r⟩⟧
+  map_one' := by rw [map_one, one_def]
+  map_mul' r s := by rw [mul_def, map_mul]
+  map_add' r s := by rw [add_def, map_add]
+  map_zero' := by rw [map_zero, zero_def]
 
 lemma algebraMapAux_at (i : ι) (r : R) :
     algebraMapAux (R:=R) r
@@ -606,8 +606,8 @@ instance : Algebra R (DirectLimit G f) where
     rw [smul_def, algebraMapAux_at i, mul_def, Algebra.smul_def']
 
 lemma algebraMap_at (i : ι) (r : R) :
-    algebraMap R (DirectLimit G f) r = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) := by
-  rw [← algebraMapAux_at i]; rfl
+    algebraMap R (DirectLimit G f) r = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) :=
+  algebraMapAux_at i r
 
 end Algebra
 

From b7948a2907e51ac2c5e73631a262d781215c63c3 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Tue, 5 May 2026 15:06:27 -0700
Subject: [PATCH 07/28] following PR feedback, use map_0 in algebraMapAux and
 map_0_def in algebraMapAux_at

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 23 ++++++++++-------------
 1 file changed, 10 insertions(+), 13 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 626a1efe4ed751..8a9c61907b71ad 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -582,21 +582,18 @@ variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 
 /-- The algebra map for the DirectLimit of a directed system of algebras -/
 def algebraMapAux : R →+* DirectLimit G f where
-  toFun r := ⟦⟨Classical.arbitrary ι, algebraMap R (G (Classical.arbitrary ι)) r⟩⟧
-  map_one' := by rw [map_one, one_def]
-  map_mul' r s := by rw [mul_def, map_mul]
-  map_add' r s := by rw [add_def, map_add]
-  map_zero' := by rw [map_zero, zero_def]
+  toFun r := map₀ _ fun _ ↦ algebraMap R _ r
+  map_one' := by rw [map₀, map_one, one_def]
+  map_mul' r s := by simp_rw [map₀, mul_def, map_mul]
+  map_add' r s :=  by simp_rw [map₀, add_def, map_add]
+  map_zero' := by rw [map₀, map_zero, zero_def]
 
 lemma algebraMapAux_at (i : ι) (r : R) :
-    algebraMapAux (R:=R) r
-      = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) := by
-  let j := Classical.arbitrary ι
-  change ⟦⟨j, (algebraMap R (G j)) r⟩⟧ = (⟦⟨i, (algebraMap R (G i)) r⟩⟧ : DirectLimit G f)
-  obtain ⟨k, hik, hjk⟩ := directed_of (α := ι) (· ≤ ·) i j
-  rw [eq_of_le (f := f) ⟨j, (algebraMap R (G j) r)⟩ k hjk]
-  rw [eq_of_le (f := f) ⟨i, (algebraMap R (G i) r)⟩ k hik]
-  simp_rw [AlgHomClass.commutes]
+    algebraMapAux (R:=R) r = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) := by
+  simp only [algebraMapAux, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
+  apply map₀_def
+  intro i j hij
+  rw [AlgHomClass.commutes]
 
 instance : Algebra R (DirectLimit G f) where
   algebraMap := algebraMapAux

From 34f10fc29ceb1b1b8879a783c4208869c491b1d3 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Tue, 5 May 2026 15:23:03 -0700
Subject: [PATCH 08/28] add DirectLimit.Algebra.lift_comp_of

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 8a9c61907b71ad..1a697b7e37f704 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -828,6 +828,9 @@ def lift (g : ∀ i, G i →ₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g
 
 variable (g : ∀ i, G i →ₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
 
+@[simp]
+theorem lift_comp_of {i} : (lift G f P g Hg).comp (of G f i) = g i := rfl
+
 @[simp] theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x := rfl
 
 @[ext]

From b0895246f333769daeae81f2cff5389c43ce4770 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Tue, 5 May 2026 16:20:39 -0700
Subject: [PATCH 09/28] rename algebraMap_at to algebraMap_def, and remove
 unnecessary type ascription

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 1a697b7e37f704..23f9226080f442 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -588,7 +588,7 @@ def algebraMapAux : R →+* DirectLimit G f where
   map_add' r s :=  by simp_rw [map₀, add_def, map_add]
   map_zero' := by rw [map₀, map_zero, zero_def]
 
-lemma algebraMapAux_at (i : ι) (r : R) :
+lemma algebraMapAux_def (i : ι) (r : R) :
     algebraMapAux (R:=R) r = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) := by
   simp only [algebraMapAux, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
   apply map₀_def
@@ -598,13 +598,13 @@ lemma algebraMapAux_at (i : ι) (r : R) :
 instance : Algebra R (DirectLimit G f) where
   algebraMap := algebraMapAux
   commutes' r := DirectLimit.induction f fun i _ ↦ by
-    rw [algebraMapAux_at i, mul_def, mul_def, Algebra.commutes]
+    rw [algebraMapAux_def i, mul_def, mul_def, Algebra.commutes]
   smul_def' r := DirectLimit.induction _ fun i _ => by
-    rw [smul_def, algebraMapAux_at i, mul_def, Algebra.smul_def']
+    rw [smul_def, algebraMapAux_def i, mul_def, Algebra.smul_def']
 
-lemma algebraMap_at (i : ι) (r : R) :
-    algebraMap R (DirectLimit G f) r = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) :=
-  algebraMapAux_at i r
+lemma algebraMap_def (i : ι) (r : R) :
+    algebraMap R (DirectLimit G f) r = ⟦⟨i, algebraMap R (G i) r⟩⟧:=
+  algebraMapAux_def i r
 
 end Algebra
 
@@ -807,7 +807,7 @@ variable (G f) in
 def of (i) : G i →ₐ[R] DirectLimit G f where
   toFun x := ⟦⟨i, x⟩⟧
   __ := (DirectLimit.Ring.of G f i)
-  commutes' r := by rw [algebraMap_at i]
+  commutes' r := by rw [algebraMap_def i]
 
 @[simp] lemma of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x := .symm <| eq_of_le ..
 
@@ -824,7 +824,7 @@ def lift (g : ∀ i, G i →ₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g
   __ := DirectLimit.Ring.lift G f P (g:= fun i => (g i).toRingHom) (Hg:=Hg)
   commutes' r := by
     let i := Classical.arbitrary ι
-    rw [algebraMap_at i r, lift_def, AlgHom.commutes]
+    rw [algebraMap_def i r, lift_def, AlgHom.commutes]
 
 variable (g : ∀ i, G i →ₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
 

From 63d2d4530f67c3894f7389d7116f3373ad21a215 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Tue, 5 May 2026 16:23:47 -0700
Subject: [PATCH 10/28] add @[simps] to DirectLimit.Algebra.of and
 DirectLimit.Algebra.lift

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 23f9226080f442..e90cc2d6364faa 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -804,6 +804,7 @@ variable [Nonempty ι]
 
 variable (G f) in
 /-- The canonical map from a component to the direct limit. -/
+@[simps]
 def of (i) : G i →ₐ[R] DirectLimit G f where
   toFun x := ⟦⟨i, x⟩⟧
   __ := (DirectLimit.Ring.of G f i)
@@ -818,6 +819,7 @@ variable (G f) in
 that respect the directed system structure (i.e. make some diagram commute) give rise
 to a unique map out of the direct limit.
 -/
+@[simps]
 def lift (g : ∀ i, G i →ₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) :
     DirectLimit G f →ₐ[R] P where
   toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm

From 15190ebc16ec8c78f949328ebeef074226f4b993 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Tue, 5 May 2026 17:01:55 -0700
Subject: [PATCH 11/28] remove the @[simp] on DirectLimit.Algebra.of_f for
 consistency with the other of_f and to satisfy linter

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index e90cc2d6364faa..84edaec03325c9 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -810,7 +810,7 @@ def of (i) : G i →ₐ[R] DirectLimit G f where
   __ := (DirectLimit.Ring.of G f i)
   commutes' r := by rw [algebraMap_def i]
 
-@[simp] lemma of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x := .symm <| eq_of_le ..
+lemma of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x := .symm <| eq_of_le ..
 
 variable (P : Type*) [Semiring P] [Algebra R P]
 

From 1609007e17bd046b14cc753f5b9928091ef663e1 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 12:54:44 -0700
Subject: [PATCH 12/28] add map0MonoidHom, map0RingHom, map0RingHom_def, &
 replace algebraMapAux with use of map0RingHom

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 54 ++++++++++++++++++------
 1 file changed, 40 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 84edaec03325c9..3b2db3d26ec6c0 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -213,6 +213,17 @@ theorem lift_npow (g : ∀ i, H i) (h) (x : DirectLimit G f) (n : ℕ) :
     DirectLimit.lift f (g ·) h (x ^ n) = DirectLimit.lift f (g ·) h x ^ n :=
   x.induction _ fun i x ↦ by simp_rw [npow_def, lift_def, map_pow (g i)]
 
+/-- A monoid hom into the direct limit obtained by picking an arbitrary stage from a
+family of monoid homs to the stages of the directed system. No compatibility condition is assumed.
+If the family of maps into the directed system is compatible with the maps of the directed system,
+then more can be done.
+-/
+@[simps, to_additive]
+def map₀MonoidHom (x : ∀ i, MonoidHom C (G i)) : MonoidHom C (DirectLimit G f) where
+  toFun r := map₀ _ fun _ ↦ x _ r
+  map_one' := by rw [map₀, map_one, one_def]
+  map_mul' r s := by simp_rw [map₀, mul_def, map_mul]
+
 end Monoid
 
 @[to_additive] instance [∀ i, CommMonoid (G i)] [∀ i j h, MonoidHomClass (T h) (G i) (G j)] :
@@ -433,6 +444,31 @@ instance [∀ i, NonAssocSemiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G
 instance [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
     Semiring (DirectLimit G f) where
 
+/-TODO: this could more generally be done for non-associative semirings, but would need to either
+repeat the definitions for map_one' and map_mul' from map₀MonoidHom,
+or maybe define map₀MulHom and map₀OneHom.
+-/
+/-- A ring hom into the direct limit obtained by picking an arbitrary stage from a
+family of ring homs to the stages of the directed system. No compatibility condition is assumed.
+If the family of maps into the directed system is compatible with the maps of the directed system,
+then more can be done.
+-/
+@[simps]
+def map₀RingHom [Semiring R] [∀ i, Semiring (G i)]
+    [∀ i j h, RingHomClass (T h) (G i) (G j)]
+    (x : ∀ i, R →+* G i) : R →+* DirectLimit G f where
+  toFun r := map₀ _ fun _ ↦ x _ r
+  __ := map₀AddMonoidHom (f := f) (fun i => (x i).toAddMonoidHom)
+  __ := map₀MonoidHom (f := f) (fun i => (x i).toMonoidHom)
+
+lemma map₀RingHom_def [Semiring R] [∀ i, Semiring (G i)]
+    [∀ i j h, RingHomClass (T h) (G i) (G j)]
+    (x : ∀ i, R →+* G i) (compat : ∀ r i j h, (f i j h) ((x i) r) = (x j) r) (i : ι) (r : R) :
+    map₀RingHom x r
+    = (⟦⟨i, x i r⟩⟧ : DirectLimit G f) := by
+  rw [map₀RingHom_apply]
+  apply map₀_def (compat := compat r)
+
 instance [∀ i, NonUnitalNonAssocCommSemiring (G i)]
     [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] :
     NonUnitalNonAssocCommSemiring (DirectLimit G f) where
@@ -580,23 +616,13 @@ variable [CommSemiring R]
 variable [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)]
 variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 
-/-- The algebra map for the DirectLimit of a directed system of algebras -/
-def algebraMapAux : R →+* DirectLimit G f where
-  toFun r := map₀ _ fun _ ↦ algebraMap R _ r
-  map_one' := by rw [map₀, map_one, one_def]
-  map_mul' r s := by simp_rw [map₀, mul_def, map_mul]
-  map_add' r s :=  by simp_rw [map₀, add_def, map_add]
-  map_zero' := by rw [map₀, map_zero, zero_def]
-
 lemma algebraMapAux_def (i : ι) (r : R) :
-    algebraMapAux (R:=R) r = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) := by
-  simp only [algebraMapAux, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
-  apply map₀_def
-  intro i j hij
-  rw [AlgHomClass.commutes]
+    map₀RingHom (fun i ↦ algebraMap R (G i)) r
+    = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) :=
+  map₀RingHom_def _ (fun r i j hij => by rw[AlgHomClass.commutes]) i r
 
 instance : Algebra R (DirectLimit G f) where
-  algebraMap := algebraMapAux
+  algebraMap := map₀RingHom (fun i ↦ algebraMap R (G i))
   commutes' r := DirectLimit.induction f fun i _ ↦ by
     rw [algebraMapAux_def i, mul_def, mul_def, Algebra.commutes]
   smul_def' r := DirectLimit.induction _ fun i _ => by

From 1026f0606df7bd787f1aca3857ab1c457cf7a48a Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 13:32:46 -0700
Subject: [PATCH 13/28] add docstring to map0AddMonoidHom, and use the proper
 notation for the monoid hom in map0MonoidHom instead of the name MonoidHom

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 3b2db3d26ec6c0..1f408d9ee74005 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -218,8 +218,12 @@ family of monoid homs to the stages of the directed system. No compatibility con
 If the family of maps into the directed system is compatible with the maps of the directed system,
 then more can be done.
 -/
-@[simps, to_additive]
-def map₀MonoidHom (x : ∀ i, MonoidHom C (G i)) : MonoidHom C (DirectLimit G f) where
+@[simps, to_additive /-- An additive monoid hom into the direct limit obtained by picking an
+arbitrary stage from a family of additive monoid homs to the stages of the directed system.
+No compatibility condition is assumed.
+If the family of maps into the directed system is compatible with the maps of the directed system,
+then more can be done. -/]
+def map₀MonoidHom (x : ∀ i, C →* (G i)) : C →*(DirectLimit G f) where
   toFun r := map₀ _ fun _ ↦ x _ r
   map_one' := by rw [map₀, map_one, one_def]
   map_mul' r s := by simp_rw [map₀, mul_def, map_mul]

From 61022bfe17ae5f4c661d3126239fc4151470e922 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 14:17:44 -0700
Subject: [PATCH 14/28] fix whitespace and remove excess parentheses in
 Mathlib/Algebra/Colimit/DirectLimit.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 1f408d9ee74005..d5f25e7736037e 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -223,7 +223,7 @@ arbitrary stage from a family of additive monoid homs to the stages of the direc
 No compatibility condition is assumed.
 If the family of maps into the directed system is compatible with the maps of the directed system,
 then more can be done. -/]
-def map₀MonoidHom (x : ∀ i, C →* (G i)) : C →*(DirectLimit G f) where
+def map₀MonoidHom (x : ∀ i, C →* G i) : C →* DirectLimit G f where
   toFun r := map₀ _ fun _ ↦ x _ r
   map_one' := by rw [map₀, map_one, one_def]
   map_mul' r s := by simp_rw [map₀, mul_def, map_mul]

From dbdab9dd5401b49964728a9a67863a45fd92524e Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 14:20:50 -0700
Subject: [PATCH 15/28] make lemma algebraMapAux_def private, and rename it to
 map0RingHom_algebraMap_def

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index d5f25e7736037e..8de61571ae8595 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -620,7 +620,7 @@ variable [CommSemiring R]
 variable [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)]
 variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 
-lemma algebraMapAux_def (i : ι) (r : R) :
+private lemma map₀RingHom_algebraMap_def (i : ι) (r : R) :
     map₀RingHom (fun i ↦ algebraMap R (G i)) r
     = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) :=
   map₀RingHom_def _ (fun r i j hij => by rw[AlgHomClass.commutes]) i r
@@ -628,13 +628,13 @@ lemma algebraMapAux_def (i : ι) (r : R) :
 instance : Algebra R (DirectLimit G f) where
   algebraMap := map₀RingHom (fun i ↦ algebraMap R (G i))
   commutes' r := DirectLimit.induction f fun i _ ↦ by
-    rw [algebraMapAux_def i, mul_def, mul_def, Algebra.commutes]
+    rw [map₀RingHom_algebraMap_def i, mul_def, mul_def, Algebra.commutes]
   smul_def' r := DirectLimit.induction _ fun i _ => by
-    rw [smul_def, algebraMapAux_def i, mul_def, Algebra.smul_def']
+    rw [smul_def, map₀RingHom_algebraMap_def i, mul_def, Algebra.smul_def']
 
 lemma algebraMap_def (i : ι) (r : R) :
     algebraMap R (DirectLimit G f) r = ⟦⟨i, algebraMap R (G i) r⟩⟧:=
-  algebraMapAux_def i r
+  map₀RingHom_algebraMap_def i r
 
 end Algebra
 

From 28013cc6162280b5a25df3f3b3228bdd444aba94 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 14:21:58 -0700
Subject: [PATCH 16/28] add R-algebras to the list of categories for which the
 lift map is defined

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 8de61571ae8595..05d9967cedf586 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -45,6 +45,7 @@ So far we only show that `DirectLimit` is the colimit in the following categorie
 * non-unital semirings
 * rings
 * (non-unital) star rings
+* R-algebras
 
 but for the other algebraic structures the constructions and proofs will be easy following
 the same pattern. Since any two colimits are isomorphic, this allows us to golf proofs of

From b21c1e9147bbf44de514b0159660bfa2e3b6d00c Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 6 May 2026 14:30:53 -0700
Subject: [PATCH 17/28] =?UTF-8?q?Simplify=20map=E2=82=80RingHom?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 65 +++++++++---------------
 1 file changed, 23 insertions(+), 42 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 05d9967cedf586..d5b9f33cc12348 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Module.LinearMap.Defs
 public import Mathlib.Algebra.Star.StarRingHom
 public import Mathlib.Algebra.Algebra.Hom
+public import Mathlib.Algebra.Algebra.Pi
 public import Mathlib.Data.Rat.Cast.Defs
 public import Mathlib.Order.DirectedInverseSystem
 public import Mathlib.Tactic.SuppressCompilation
@@ -214,20 +215,12 @@ theorem lift_npow (g : ∀ i, H i) (h) (x : DirectLimit G f) (n : ℕ) :
     DirectLimit.lift f (g ·) h (x ^ n) = DirectLimit.lift f (g ·) h x ^ n :=
   x.induction _ fun i x ↦ by simp_rw [npow_def, lift_def, map_pow (g i)]
 
-/-- A monoid hom into the direct limit obtained by picking an arbitrary stage from a
-family of monoid homs to the stages of the directed system. No compatibility condition is assumed.
-If the family of maps into the directed system is compatible with the maps of the directed system,
-then more can be done.
--/
-@[simps, to_additive /-- An additive monoid hom into the direct limit obtained by picking an
-arbitrary stage from a family of additive monoid homs to the stages of the directed system.
-No compatibility condition is assumed.
-If the family of maps into the directed system is compatible with the maps of the directed system,
-then more can be done. -/]
-def map₀MonoidHom (x : ∀ i, C →* G i) : C →* DirectLimit G f where
-  toFun r := map₀ _ fun _ ↦ x _ r
-  map_one' := by rw [map₀, map_one, one_def]
-  map_mul' r s := by simp_rw [map₀, mul_def, map_mul]
+/-- `map₀` as a `MonoidHom`. -/
+@[to_additive (attr := simps) /-- `map₀` as an `AddMonoidHom`. -/]
+def map₀MonoidHom : (∀ i, G i) →* DirectLimit G f where
+  toFun x := map₀ _ x
+  map_one' := by rw [map₀, Pi.one_apply, one_def]
+  map_mul' r s := by simp_rw [map₀, Pi.mul_apply, mul_def]
 
 end Monoid
 
@@ -453,26 +446,13 @@ instance [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
 repeat the definitions for map_one' and map_mul' from map₀MonoidHom,
 or maybe define map₀MulHom and map₀OneHom.
 -/
-/-- A ring hom into the direct limit obtained by picking an arbitrary stage from a
-family of ring homs to the stages of the directed system. No compatibility condition is assumed.
-If the family of maps into the directed system is compatible with the maps of the directed system,
-then more can be done.
--/
+/-- `map₀` as a `RingHom`. -/
 @[simps]
-def map₀RingHom [Semiring R] [∀ i, Semiring (G i)]
-    [∀ i j h, RingHomClass (T h) (G i) (G j)]
-    (x : ∀ i, R →+* G i) : R →+* DirectLimit G f where
-  toFun r := map₀ _ fun _ ↦ x _ r
-  __ := map₀AddMonoidHom (f := f) (fun i => (x i).toAddMonoidHom)
-  __ := map₀MonoidHom (f := f) (fun i => (x i).toMonoidHom)
-
-lemma map₀RingHom_def [Semiring R] [∀ i, Semiring (G i)]
-    [∀ i j h, RingHomClass (T h) (G i) (G j)]
-    (x : ∀ i, R →+* G i) (compat : ∀ r i j h, (f i j h) ((x i) r) = (x j) r) (i : ι) (r : R) :
-    map₀RingHom x r
-    = (⟦⟨i, x i r⟩⟧ : DirectLimit G f) := by
-  rw [map₀RingHom_apply]
-  apply map₀_def (compat := compat r)
+def map₀RingHom [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
+    (∀ i, G i) →+* DirectLimit G f where
+  toFun r := map₀ _ r
+  __ := map₀AddMonoidHom (f := f)
+  __ := map₀MonoidHom (f := f)
 
 instance [∀ i, NonUnitalNonAssocCommSemiring (G i)]
     [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] :
@@ -618,24 +598,25 @@ instance [∀ i, Field (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
 section Algebra
 
 variable [CommSemiring R]
-variable [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)]
+variable [∀ i, Semiring (G i)] -- [∀ i j h, RingHomClass (T h) (G i) (G j)]
 variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 
-private lemma map₀RingHom_algebraMap_def (i : ι) (r : R) :
-    map₀RingHom (fun i ↦ algebraMap R (G i)) r
-    = (⟦⟨i, algebraMap R (G i) r⟩⟧ : DirectLimit G f) :=
-  map₀RingHom_def _ (fun r i j hij => by rw[AlgHomClass.commutes]) i r
+lemma map₀_algebraMap (i : ι) (r : R) :
+    map₀ f (fun i ↦ algebraMap R (G i) r) = ⟦⟨i, algebraMap R (G i) r⟩⟧ :=
+  map₀_def _ _ (fun _ _ _ => AlgHomClass.commutes _ _) i
 
 instance : Algebra R (DirectLimit G f) where
-  algebraMap := map₀RingHom (fun i ↦ algebraMap R (G i))
+  algebraMap := map₀RingHom (f := f).comp (algebraMap R (∀ i, G i))
   commutes' r := DirectLimit.induction f fun i _ ↦ by
-    rw [map₀RingHom_algebraMap_def i, mul_def, mul_def, Algebra.commutes]
+    dsimp [Pi.algebraMap_def]
+    rw [map₀_algebraMap i, mul_def, mul_def, Algebra.commutes]
   smul_def' r := DirectLimit.induction _ fun i _ => by
-    rw [smul_def, map₀RingHom_algebraMap_def i, mul_def, Algebra.smul_def']
+    dsimp [Pi.algebraMap_def]
+    rw [smul_def, map₀_algebraMap i, mul_def, Algebra.smul_def']
 
 lemma algebraMap_def (i : ι) (r : R) :
     algebraMap R (DirectLimit G f) r = ⟦⟨i, algebraMap R (G i) r⟩⟧:=
-  map₀RingHom_algebraMap_def i r
+  map₀_algebraMap i r
 
 end Algebra
 

From 3b72e57e5c3b4bbc8e4db17112324f9bd13b6206 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 15:42:07 -0700
Subject: [PATCH 18/28] make variable (f) explicit in map0MonoidHom,
 map0AddMonoidHom, and map0RingHom

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index d5b9f33cc12348..7a09c1de89ddad 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -215,6 +215,7 @@ theorem lift_npow (g : ∀ i, H i) (h) (x : DirectLimit G f) (n : ℕ) :
     DirectLimit.lift f (g ·) h (x ^ n) = DirectLimit.lift f (g ·) h x ^ n :=
   x.induction _ fun i x ↦ by simp_rw [npow_def, lift_def, map_pow (g i)]
 
+variable (f) in
 /-- `map₀` as a `MonoidHom`. -/
 @[to_additive (attr := simps) /-- `map₀` as an `AddMonoidHom`. -/]
 def map₀MonoidHom : (∀ i, G i) →* DirectLimit G f where
@@ -446,13 +447,14 @@ instance [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
 repeat the definitions for map_one' and map_mul' from map₀MonoidHom,
 or maybe define map₀MulHom and map₀OneHom.
 -/
+variable (f) in
 /-- `map₀` as a `RingHom`. -/
 @[simps]
 def map₀RingHom [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
     (∀ i, G i) →+* DirectLimit G f where
   toFun r := map₀ _ r
-  __ := map₀AddMonoidHom (f := f)
-  __ := map₀MonoidHom (f := f)
+  __ := map₀AddMonoidHom f
+  __ := map₀MonoidHom f
 
 instance [∀ i, NonUnitalNonAssocCommSemiring (G i)]
     [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] :

From b850d12d41bd51257eef610e4411c03488bf4920 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 15:42:35 -0700
Subject: [PATCH 19/28] remove commented out typeclass variable

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 7a09c1de89ddad..2910d36609205c 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -600,7 +600,7 @@ instance [∀ i, Field (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
 section Algebra
 
 variable [CommSemiring R]
-variable [∀ i, Semiring (G i)] -- [∀ i j h, RingHomClass (T h) (G i) (G j)]
+variable [∀ i, Semiring (G i)]
 variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 
 lemma map₀_algebraMap (i : ι) (r : R) :

From 9ed65bcd97754d0c67850a021632420870475239 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 15:57:13 -0700
Subject: [PATCH 20/28] pull out proofs of map_one' and map_mul' from
 definition of map0MonoidHom to produce lemmas map0_one and map0_mul

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 2910d36609205c..1b1719b8b01973 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -88,6 +88,9 @@ theorem lift_one (g : ∀ i, H i) (h) :
   let ⟨i⟩ := ‹Nonempty ι›
   rw [one_def, lift_def, map_one (g i)]
 
+@[to_additive]
+lemma map₀_one : map₀ f (1 : ∀ i, G i) = 1 := by rw [map₀, Pi.one_apply, one_def]
+
 end ZeroOne
 
 section Star
@@ -136,6 +139,10 @@ theorem lift_mul (g : ∀ i, H i) (h) (x y : DirectLimit G f) :
       DirectLimit.lift f (g ·) h x * DirectLimit.lift f (g ·) h y :=
   DirectLimit.induction₂ _ (fun i x y ↦ by simp_rw [mul_def, lift_def, map_mul (g i)]) x y
 
+@[to_additive]
+lemma map₀_mul [Nonempty ι] (r s : ∀ i, G i) : map₀ f (r * s) = map₀ f r * map₀ f s := by
+  simp_rw [map₀, Pi.mul_apply, mul_def]
+
 end AddMul
 
 @[to_additive] instance [∀ i, CommMagma (G i)] [∀ i j h, MulHomClass (T h) (G i) (G j)] :
@@ -220,8 +227,8 @@ variable (f) in
 @[to_additive (attr := simps) /-- `map₀` as an `AddMonoidHom`. -/]
 def map₀MonoidHom : (∀ i, G i) →* DirectLimit G f where
   toFun x := map₀ _ x
-  map_one' := by rw [map₀, Pi.one_apply, one_def]
-  map_mul' r s := by simp_rw [map₀, Pi.mul_apply, mul_def]
+  map_one' := map₀_one
+  map_mul' r s := map₀_mul r s
 
 end Monoid
 

From 8280c168b14aa61b123daf717303bd75de30753e Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 16:16:49 -0700
Subject: [PATCH 21/28] make map0RingHom work for NonAssocSemiring by using
 map0_one and map0_mul instead of map0MonoidHom

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 1b1719b8b01973..6546ba9a72e232 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -450,18 +450,15 @@ instance [∀ i, NonAssocSemiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G
 instance [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
     Semiring (DirectLimit G f) where
 
-/-TODO: this could more generally be done for non-associative semirings, but would need to either
-repeat the definitions for map_one' and map_mul' from map₀MonoidHom,
-or maybe define map₀MulHom and map₀OneHom.
--/
 variable (f) in
 /-- `map₀` as a `RingHom`. -/
 @[simps]
-def map₀RingHom [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
+def map₀RingHom [∀ i, NonAssocSemiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
     (∀ i, G i) →+* DirectLimit G f where
   toFun r := map₀ _ r
   __ := map₀AddMonoidHom f
-  __ := map₀MonoidHom f
+  map_one' := map₀_one
+  map_mul' := map₀_mul
 
 instance [∀ i, NonUnitalNonAssocCommSemiring (G i)]
     [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] :

From 7172b17a56681bbbe849bbc93c789e0a086776c2 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 16:37:13 -0700
Subject: [PATCH 22/28] tiny simplification to map0MonoidHom

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 6546ba9a72e232..e48f576f19839b 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -228,7 +228,7 @@ variable (f) in
 def map₀MonoidHom : (∀ i, G i) →* DirectLimit G f where
   toFun x := map₀ _ x
   map_one' := map₀_one
-  map_mul' r s := map₀_mul r s
+  map_mul' := map₀_mul
 
 end Monoid
 

From e6f64a002570e26c7ef2c3c3ed16d12426995e4c Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 17:05:53 -0700
Subject: [PATCH 23/28] make map0MonoidHom assume only MapOneClass (G i) rather
 than Monoid (G i), so that map0RingHom can use map0MonoidHom instead of
 map0_one and map0_mul and still support NonAssocSemiring

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index e48f576f19839b..8b8f084df8cf64 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -203,6 +203,15 @@ variable [Nonempty ι]
   one_mul := DirectLimit.induction _ fun i _ ↦ by simp_rw [one_def i, mul_def, one_mul]
   mul_one := DirectLimit.induction _ fun i _ ↦ by simp_rw [one_def i, mul_def, mul_one]
 
+variable (f) in
+/-- `map₀` as a `MonoidHom`. -/
+@[to_additive (attr := simps) /-- `map₀` as an `AddMonoidHom`. -/]
+def map₀MonoidHom [∀ i, MulOneClass (G i)] [∀ i j h, MonoidHomClass (T h) (G i) (G j)] :
+    (∀ i, G i) →* DirectLimit G f where
+  toFun x := map₀ _ x
+  map_one' := map₀_one
+  map_mul' := map₀_mul
+
 section Monoid
 variable [∀ i, Monoid (G i)] [Monoid C]
 variable [∀ i j h, MonoidHomClass (T h) (G i) (G j)] [∀ i, MonoidHomClass (H i) (G i) C]
@@ -222,14 +231,6 @@ theorem lift_npow (g : ∀ i, H i) (h) (x : DirectLimit G f) (n : ℕ) :
     DirectLimit.lift f (g ·) h (x ^ n) = DirectLimit.lift f (g ·) h x ^ n :=
   x.induction _ fun i x ↦ by simp_rw [npow_def, lift_def, map_pow (g i)]
 
-variable (f) in
-/-- `map₀` as a `MonoidHom`. -/
-@[to_additive (attr := simps) /-- `map₀` as an `AddMonoidHom`. -/]
-def map₀MonoidHom : (∀ i, G i) →* DirectLimit G f where
-  toFun x := map₀ _ x
-  map_one' := map₀_one
-  map_mul' := map₀_mul
-
 end Monoid
 
 @[to_additive] instance [∀ i, CommMonoid (G i)] [∀ i j h, MonoidHomClass (T h) (G i) (G j)] :
@@ -457,8 +458,7 @@ def map₀RingHom [∀ i, NonAssocSemiring (G i)] [∀ i j h, RingHomClass (T h)
     (∀ i, G i) →+* DirectLimit G f where
   toFun r := map₀ _ r
   __ := map₀AddMonoidHom f
-  map_one' := map₀_one
-  map_mul' := map₀_mul
+  __ := map₀MonoidHom f
 
 instance [∀ i, NonUnitalNonAssocCommSemiring (G i)]
     [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] :

From 26ec4f4946f7c4973358945f28117c9cc50138aa Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 17:14:35 -0700
Subject: [PATCH 24/28] add simp attr to the map0_one lemma

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 8b8f084df8cf64..bc1fd14476eb8a 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -88,7 +88,7 @@ theorem lift_one (g : ∀ i, H i) (h) :
   let ⟨i⟩ := ‹Nonempty ι›
   rw [one_def, lift_def, map_one (g i)]
 
-@[to_additive]
+@[to_additive (attr := simp)]
 lemma map₀_one : map₀ f (1 : ∀ i, G i) = 1 := by rw [map₀, Pi.one_apply, one_def]
 
 end ZeroOne

From 720e839943d2635b7af760d3cf9e33fbd090ab3f Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 18:15:14 -0700
Subject: [PATCH 25/28] remove todo comment in light of PR #39017

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index bc1fd14476eb8a..02a562cf1ee601 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -600,7 +600,6 @@ instance [∀ i, Field (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] :
   __ : DivisionRing _ := inferInstance
   mul_comm := mul_comm
 
---TODO: add support for non-unital algebras
 section Algebra
 
 variable [CommSemiring R]

From 1585f69613fb687164e9979fe8f91b8d3469a4ba Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 18:35:52 -0700
Subject: [PATCH 26/28] add DirectLimit.NonUnitalAlgebra.lift etc.

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 50 +++++++++++++++++++++++-
 1 file changed, 49 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index bc1fd14476eb8a..d4f35b9eac8fe5 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.Module.LinearMap.Defs
 public import Mathlib.Algebra.Star.StarRingHom
-public import Mathlib.Algebra.Algebra.Hom
+public import Mathlib.Algebra.Algebra.NonUnitalHom
 public import Mathlib.Algebra.Algebra.Pi
 public import Mathlib.Data.Rat.Cast.Defs
 public import Mathlib.Order.DirectedInverseSystem
@@ -863,4 +863,52 @@ theorem hom_ext {g₁ g₂ : DirectLimit G f →ₐ[R] P}
 
 end Algebra
 
+namespace NonUnitalAlgebra
+
+variable [CommSemiring R]
+variable [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i, DistribMulAction R (G i)]
+variable [∀ i j h, NonUnitalAlgHomClass (T h) R (G i) (G j)]
+variable [Nonempty ι]
+
+variable (G f) in
+/-- The canonical map from a component to the direct limit. -/
+@[simps]
+def of (i) : G i →ₙₐ[R] DirectLimit G f where
+  toFun x := ⟦⟨i, x⟩⟧
+  __ := (DirectLimit.NonUnitalRing.of G f i)
+  map_smul' m x := by rw [smul_def, MonoidHom.id_apply]
+
+lemma of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x := .symm <| eq_of_le ..
+
+variable (P : Type*) [NonUnitalNonAssocSemiring P] [DistribMulAction R P]
+
+variable (G f) in
+/-- The universal property of the direct limit: maps from the components to another R-algebra
+that respect the directed system structure (i.e. make some diagram commute) give rise
+to a unique map out of the direct limit.
+-/
+@[simps]
+def lift (g : ∀ i, G i →ₙₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) :
+    DirectLimit G f →ₙₐ[R] P where
+  toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm
+  __ := DirectLimit.NonUnitalRing.lift G f P (g:= fun i => (g i)) (Hg:=Hg)
+  map_smul' m := by apply lift_smul
+
+variable (g : ∀ i, G i →ₙₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
+
+@[simp]
+theorem lift_comp_of {i} : (lift G f P g Hg).comp (of G f i) = g i := rfl
+
+@[simp] theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x := rfl
+
+@[ext]
+theorem hom_ext {g₁ g₂ : DirectLimit G f →ₙₐ[R] P}
+    (h : ∀ i, g₁.comp (of G f i) = g₂.comp (of G f i)) :
+    g₁ = g₂ := by
+  ext x
+  induction x using DirectLimit.induction with | _ i x
+  exact congr($(h i) x)
+
+end NonUnitalAlgebra
+
 end DirectLimit

From c24b02d21be5b8bb8c03e7915c2fa4a9752f12d2 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 19:00:43 -0700
Subject: [PATCH 27/28] remove @[simp] tag on the lift_of lemmas for Algebra
 and NonUnitalAlgebra

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 86f94734e9118d..d08c5983819cf6 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -850,7 +850,7 @@ variable (g : ∀ i, G i →ₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g
 @[simp]
 theorem lift_comp_of {i} : (lift G f P g Hg).comp (of G f i) = g i := rfl
 
-@[simp] theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x := rfl
+theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x := rfl
 
 @[ext]
 theorem hom_ext {g₁ g₂ : DirectLimit G f →ₐ[R] P}
@@ -898,7 +898,7 @@ variable (g : ∀ i, G i →ₙₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x)
 @[simp]
 theorem lift_comp_of {i} : (lift G f P g Hg).comp (of G f i) = g i := rfl
 
-@[simp] theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x := rfl
+theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x := rfl
 
 @[ext]
 theorem hom_ext {g₁ g₂ : DirectLimit G f →ₙₐ[R] P}

From f4a7e82f672d2b7293d4dc94a81f99e29c33d152 Mon Sep 17 00:00:00 2001
From: drocta <madaco.madaco@gmail.com>
Date: Wed, 6 May 2026 19:55:53 -0700
Subject: [PATCH 28/28] add simp tag for map0_mul to match the tag on map0_one

---
 Mathlib/Algebra/Colimit/DirectLimit.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index d08c5983819cf6..3c8edf21854754 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -139,7 +139,7 @@ theorem lift_mul (g : ∀ i, H i) (h) (x y : DirectLimit G f) :
       DirectLimit.lift f (g ·) h x * DirectLimit.lift f (g ·) h y :=
   DirectLimit.induction₂ _ (fun i x y ↦ by simp_rw [mul_def, lift_def, map_mul (g i)]) x y
 
-@[to_additive]
+@[to_additive (attr := simp)]
 lemma map₀_mul [Nonempty ι] (r s : ∀ i, G i) : map₀ f (r * s) = map₀ f r * map₀ f s := by
   simp_rw [map₀, Pi.mul_apply, mul_def]