From f3166f5f11271d228c71150ee601a7e2dcb78e5b Mon Sep 17 00:00:00 2001 From: drocta Date: Fri, 17 Apr 2026 16:55:45 -0700 Subject: [PATCH 01/18] add Star and InvolutiveStar instances for DirectLimit --- Mathlib/Algebra/Colimit/DirectLimit.lean | 26 ++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index 22817938353332..a23ba46f292500 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -6,6 +6,7 @@ Authors: Junyan Xu module public import Mathlib.Algebra.Module.LinearMap.Defs +public import Mathlib.Algebra.Star.StarRingHom public import Mathlib.Data.Rat.Cast.Defs public import Mathlib.Order.DirectedInverseSystem public import Mathlib.Tactic.SuppressCompilation @@ -73,6 +74,31 @@ variable [∀ i j h, OneHomClass (T h) (G i) (G j)] end ZeroOne +section Star +variable [∀ i, Star (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)] + +instance : Star (DirectLimit G f) where + star := DirectLimit.map f f (fun _ x => star x) (compat := by + intro i j h + exact StarHomClass.map_star (f i j h)) + +lemma star_def (i : ι) (x : G i) : + star ⟦⟨i, x⟩⟧ = (⟦⟨i, star x ⟩⟧ : DirectLimit G f) := by + rfl + +end Star + +section InvolutiveStar +variable [∀ i, InvolutiveStar (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)] + +instance : InvolutiveStar (DirectLimit G f) where + star_involutive := by + apply DirectLimit.induction + intro i x + rw [star_def, star_def, star_star] + +end InvolutiveStar + section AddMul variable [∀ i, Mul (G i)] [∀ i j h, MulHomClass (T h) (G i) (G j)] From 5ae686861ae634a7a17db5626e2af835be310bf2 Mon Sep 17 00:00:00 2001 From: drocta Date: Fri, 17 Apr 2026 17:14:52 -0700 Subject: [PATCH 02/18] add StarMul instance for DirectLimit --- Mathlib/Algebra/Colimit/DirectLimit.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index a23ba46f292500..c11a97165f8410 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -123,6 +123,15 @@ end AddMul CommSemigroup (DirectLimit G f) where mul_comm := mul_comm +section StarMul +variable [∀ i, Mul (G i)] [∀ i j h, MulHomClass (T h) (G i) (G j)] +variable [∀ i, StarMul (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)] + +instance : StarMul (DirectLimit G f) where + star_mul := DirectLimit.induction₂ _ fun i _ _ ↦ by simp_rw [mul_def, star_def, star_mul, mul_def] + +end StarMul + section SMul variable [∀ i, SMul R (G i)] [∀ i j h, MulActionHomClass (T h) R (G i) (G j)] From 06ed7214783bd0438eb7428062a38b3cec96b666 Mon Sep 17 00:00:00 2001 From: drocta Date: Fri, 17 Apr 2026 17:22:03 -0700 Subject: [PATCH 03/18] add StarAddMonoid instance for DirectLimit --- Mathlib/Algebra/Colimit/DirectLimit.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index c11a97165f8410..0b6284c0e5f257 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -175,6 +175,15 @@ end Monoid CommMonoid (DirectLimit G f) where mul_comm := mul_comm +section StarAddMonoid +variable [∀ i, AddMonoid (G i)] [∀ i j h, AddMonoidHomClass (T h) (G i) (G j)] +variable [∀ i, StarAddMonoid (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)] + +instance : StarAddMonoid (DirectLimit G f) where + star_add := DirectLimit.induction₂ _ fun i _ _ ↦ by simp_rw [add_def, star_def, star_add, add_def] + +end StarAddMonoid + section Group variable [∀ i, Group (G i)] [∀ i j h, MonoidHomClass (T h) (G i) (G j)] From b80e78f7ae8bfc6a960dc14dde9bc2debc575b3e Mon Sep 17 00:00:00 2001 From: drocta Date: Fri, 17 Apr 2026 18:23:48 -0700 Subject: [PATCH 04/18] add StarRing instance for DirectLimit --- Mathlib/Algebra/Colimit/DirectLimit.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index 0b6284c0e5f257..d83d9e0492f4b7 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -335,6 +335,12 @@ instance [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomCl zero_mul := zero_mul mul_zero := mul_zero +instance [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] + [∀ i, StarRing (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)] + : StarRing (DirectLimit G f) where + star_mul := DirectLimit.induction₂ _ fun i _ _ ↦ by simp_rw [mul_def, star_def, star_mul, mul_def] + star_add := DirectLimit.induction₂ _ fun i _ _ ↦ by simp_rw [add_def, star_def, star_add, add_def] + instance [∀ i, NonUnitalSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalSemiring (DirectLimit G f) where mul_assoc := mul_assoc From a1ec83d22aa680e394c3d4f4906476b04dd04c02 Mon Sep 17 00:00:00 2001 From: drocta Date: Fri, 17 Apr 2026 19:01:05 -0700 Subject: [PATCH 05/18] add StarModule instance for DirectLimit --- Mathlib/Algebra/Colimit/DirectLimit.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index d83d9e0492f4b7..2d3aa9636947ad 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -143,6 +143,13 @@ variable [∀ i, SMul R (G i)] [∀ i j h, MulActionHomClass (T h) R (G i) (G j) end SMul +instance [Star R] [∀ i, Star (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)] + [∀ i, SMul R (G i)] [∀ i j h, MulActionHomClass (T h) R (G i) (G j)] + [∀ i, StarModule R (G i)] : + StarModule R (DirectLimit G f) where + star_smul r := DirectLimit.induction _ fun i x ↦ by + simp_rw [star_def, smul_def, ← star_smul, star_def] + @[to_additive] instance [Monoid R] [∀ i, MulAction R (G i)] [∀ i j h, MulActionHomClass (T h) R (G i) (G j)] : MulAction R (DirectLimit G f) where From 0168559d975f91bba7823697ad7b3556d36fbb02 Mon Sep 17 00:00:00 2001 From: drocta Date: Fri, 17 Apr 2026 19:15:36 -0700 Subject: [PATCH 06/18] add DirectLimit.StarRing.(of, of_f, lift, lift_of, hom_ext) --- Mathlib/Algebra/Colimit/DirectLimit.lean | 47 ++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index 2d3aa9636947ad..1a10b6106c6920 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -580,4 +580,51 @@ theorem hom_ext {g₁ g₂ : DirectLimit G f →+* P} (h : ∀ i, g₁.comp (of end Ring +namespace StarRing + +variable [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] +variable [∀ i, StarRing (G i)] [∀ i j h, StarHomClass (T h) (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 →⋆ₙ+* DirectLimit G f where + toFun x := ⟦⟨i, x⟩⟧ + map_mul' _ _ := (mul_def ..).symm + map_add' _ _ := (add_def ..).symm + map_zero' := (zero_def ..).symm + map_star' _ := (star_def ..).symm + +@[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 (A : Type*) [NonUnitalNonAssocSemiring A] [StarRing A] +variable (G f) in +/-- The universal property of the direct limit: maps from the components to another StarRing +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) →⋆ₙ+* A) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) : + DirectLimit G f →⋆ₙ+* A where + toFun := _root_.DirectLimit.lift _ (g · ·) (fun i j hij x ↦ (Hg i j hij x).symm) + map_mul' := DirectLimit.induction₂ _ fun i x y ↦ by simp_rw [mul_def, lift_def, map_mul (g i)] + map_zero' := by simp_rw [zero_def (Classical.arbitrary ι), lift_def, map_zero] + map_add' := DirectLimit.induction₂ _ fun i x y ↦ by simp_rw [add_def, lift_def, map_add (g i)] + map_star' := DirectLimit.induction _ fun i x ↦ by simp_rw [star_def, lift_def, map_star (g i)] + +variable (g : ∀ i, G i →⋆ₙ+* A) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) + +@[simp] theorem lift_of (i x) : lift G f A g Hg (of G f i x) = g i x := rfl + +@[ext] +theorem hom_ext {g₁ g₂ : DirectLimit G f →⋆ₙ+* A} + (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 StarRing + end DirectLimit From 75a0708ecdd7b4645d176eced8a38e0f91937418 Mon Sep 17 00:00:00 2001 From: drocta Date: Mon, 20 Apr 2026 17:58:57 -0700 Subject: [PATCH 07/18] add DirectLimit.NonUnitalRing.lift and use it to shorten Ring.lift and StarRing.lift --- Mathlib/Algebra/Colimit/DirectLimit.lean | 51 ++++++++++++++++-------- 1 file changed, 34 insertions(+), 17 deletions(-) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index 1a10b6106c6920..58aa7055b8efce 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -537,6 +537,26 @@ theorem hom_ext {g₁ g₂ : DirectLimit G f →ₗ[R] P} end Module +namespace NonUnitalRing +variable [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] +variable [Nonempty ι] + +variable (P : Type*) [NonUnitalNonAssocSemiring P] +variable (G f) in +/-- The universal property of the direct limit: maps from the components to another +NonUnitalNonAsssocSemiRing 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) →ₙ+* P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) : + DirectLimit G f →ₙ+* P where + toFun := _root_.DirectLimit.lift _ (g · ·) (fun i j hij x ↦ (Hg i j hij x).symm) + map_mul' := DirectLimit.induction₂ _ fun i x y ↦ by simp_rw [mul_def, lift_def, map_mul (g i)] + map_zero' := by simp_rw [zero_def (Classical.arbitrary ι), lift_def, map_zero] + map_add' := DirectLimit.induction₂ _ fun i x y ↦ by simp_rw [add_def, lift_def, map_add (g i)] + +end NonUnitalRing + namespace Ring variable [∀ i, NonAssocSemiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)] [Nonempty ι] @@ -560,12 +580,11 @@ that respect the directed system structure (i.e. make some diagram commute) give to a unique map out of the direct limit. -/ def lift (g : ∀ i, G i →+* P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) : - DirectLimit G f →+* P where - toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm - map_one' := by rw [one_def (Classical.arbitrary ι), lift_def, map_one] - map_mul' := DirectLimit.induction₂ _ fun i x y ↦ by simp_rw [mul_def, lift_def, map_mul] - map_zero' := by simp_rw [zero_def (Classical.arbitrary ι), lift_def, map_zero] - map_add' := DirectLimit.induction₂ _ fun i x y ↦ by simp_rw [add_def, lift_def, map_add] + DirectLimit G f →+* P := { + (NonUnitalRing.lift G f P (fun _ => (g _).toNonUnitalRingHom) Hg) with + toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm + map_one' := by rw [one_def (Classical.arbitrary ι), lift_def, map_one]} + variable (g : ∀ i, G i →+* P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) @@ -597,27 +616,25 @@ noncomputable def of (i) : G i →⋆ₙ+* DirectLimit G f where @[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 (A : Type*) [NonUnitalNonAssocSemiring A] [StarRing A] +variable (P : Type*) [NonUnitalNonAssocSemiring P] [StarRing P] variable (G f) in /-- The universal property of the direct limit: maps from the components to another StarRing 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) →⋆ₙ+* A) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) : - DirectLimit G f →⋆ₙ+* A where - toFun := _root_.DirectLimit.lift _ (g · ·) (fun i j hij x ↦ (Hg i j hij x).symm) - map_mul' := DirectLimit.induction₂ _ fun i x y ↦ by simp_rw [mul_def, lift_def, map_mul (g i)] - map_zero' := by simp_rw [zero_def (Classical.arbitrary ι), lift_def, map_zero] - map_add' := DirectLimit.induction₂ _ fun i x y ↦ by simp_rw [add_def, lift_def, map_add (g i)] - map_star' := DirectLimit.induction _ fun i x ↦ by simp_rw [star_def, lift_def, map_star (g i)] + (g : ∀ i, (G i) →⋆ₙ+* P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) : + DirectLimit G f →⋆ₙ+* P := { + (NonUnitalRing.lift G f P (fun _ => (g _).toNonUnitalRingHom) Hg) with + toFun := _root_.DirectLimit.lift _ (g · ·) (fun i j hij x ↦ (Hg i j hij x).symm) + map_star' := DirectLimit.induction _ fun i x ↦ by simp_rw [star_def, lift_def, map_star (g i)]} -variable (g : ∀ i, G i →⋆ₙ+* A) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) +variable (g : ∀ i, G i →⋆ₙ+* 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 A g Hg (of G f i x) = g i x := 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 →⋆ₙ+* A} +theorem hom_ext {g₁ g₂ : DirectLimit G f →⋆ₙ+* P} (h : ∀ i, g₁.comp (of G f i) = g₂.comp (of G f i)) : g₁ = g₂ := by ext x From da8a600a3b3772b9171d8a11353166a19fbc49d2 Mon Sep 17 00:00:00 2001 From: drocta Date: Tue, 21 Apr 2026 14:45:47 -0700 Subject: [PATCH 08/18] make instance of Star for DirectLimit more concise --- Mathlib/Algebra/Colimit/DirectLimit.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index 58aa7055b8efce..181ee074d7cd79 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -78,9 +78,7 @@ section Star variable [∀ i, Star (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)] instance : Star (DirectLimit G f) where - star := DirectLimit.map f f (fun _ x => star x) (compat := by - intro i j h - exact StarHomClass.map_star (f i j h)) + star := .map f f (fun _ x ↦ star x) (fun i j h x ↦ map_star (f i j h) x) lemma star_def (i : ι) (x : G i) : star ⟦⟨i, x⟩⟧ = (⟦⟨i, star x ⟩⟧ : DirectLimit G f) := by From 9b37cfbe3d7b7f41010f8cec1dbf3394a177f12b Mon Sep 17 00:00:00 2001 From: drocta Date: Tue, 21 Apr 2026 14:51:32 -0700 Subject: [PATCH 09/18] use the existing proofs for star_add and star_mul in the instance of StarRing for DirectLimit instead of repeating them --- Mathlib/Algebra/Colimit/DirectLimit.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index 181ee074d7cd79..b6dc9a6b5210f8 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -343,8 +343,7 @@ instance [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomCl instance [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] [∀ i, StarRing (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)] : StarRing (DirectLimit G f) where - star_mul := DirectLimit.induction₂ _ fun i _ _ ↦ by simp_rw [mul_def, star_def, star_mul, mul_def] - star_add := DirectLimit.induction₂ _ fun i _ _ ↦ by simp_rw [add_def, star_def, star_add, add_def] + star_add := star_add instance [∀ i, NonUnitalSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalSemiring (DirectLimit G f) where From 370d3f426af060c9b937d4ee331a88ff2cf49552 Mon Sep 17 00:00:00 2001 From: drocta Date: Tue, 21 Apr 2026 15:08:01 -0700 Subject: [PATCH 10/18] add NonUnitalRing.of and use it to shorten Ring.of and StarRing.of --- Mathlib/Algebra/Colimit/DirectLimit.lean | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index b6dc9a6b5210f8..e66188b9bbe95f 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -538,6 +538,15 @@ namespace NonUnitalRing variable [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] variable [Nonempty ι] +variable (G f) in +/-- The canonical map from a component to the direct limit. -/ +nonrec def of (i) : G i →ₙ+* DirectLimit G f where + toFun x := ⟦⟨i, x⟩⟧ + map_mul' _ _ := (mul_def ..).symm + map_zero' := (zero_def i).symm + map_add' _ _ := (add_def ..).symm + + variable (P : Type*) [NonUnitalNonAssocSemiring P] variable (G f) in /-- The universal property of the direct limit: maps from the components to another @@ -561,11 +570,9 @@ variable [∀ i, NonAssocSemiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G variable (G f) in /-- The canonical map from a component to the direct limit. -/ nonrec def of (i) : G i →+* DirectLimit G f where + __ := NonUnitalRing.of G f i toFun x := ⟦⟨i, x⟩⟧ map_one' := (one_def i).symm - map_mul' _ _ := (mul_def ..).symm - map_zero' := (zero_def i).symm - map_add' _ _ := (add_def ..).symm @[simp] theorem of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x := .symm <| eq_of_le .. @@ -605,10 +612,8 @@ variable [Nonempty ι] variable (G f) in /-- The canonical map from a component to the direct limit. -/ noncomputable def of (i) : G i →⋆ₙ+* DirectLimit G f where + __ := NonUnitalRing.of G f i toFun x := ⟦⟨i, x⟩⟧ - map_mul' _ _ := (mul_def ..).symm - map_add' _ _ := (add_def ..).symm - map_zero' := (zero_def ..).symm map_star' _ := (star_def ..).symm @[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 .. From 3890cd2f2043a1e9b192610aed0b17533c919cc0 Mon Sep 17 00:00:00 2001 From: drocta Date: Tue, 21 Apr 2026 15:09:04 -0700 Subject: [PATCH 11/18] tidy syntax for Ring.lift and StarRing.lift --- 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 e66188b9bbe95f..d6290dc11c872a 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -584,10 +584,10 @@ that respect the directed system structure (i.e. make some diagram commute) give to a unique map out of the direct limit. -/ def lift (g : ∀ i, G i →+* P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) : - DirectLimit G f →+* P := { - (NonUnitalRing.lift G f P (fun _ => (g _).toNonUnitalRingHom) Hg) with - toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm - map_one' := by rw [one_def (Classical.arbitrary ι), lift_def, map_one]} + DirectLimit G f →+* P where + __ := (NonUnitalRing.lift G f P (fun _ => (g _).toNonUnitalRingHom) Hg) + toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm + map_one' := by rw [one_def (Classical.arbitrary ι), lift_def, map_one] variable (g : ∀ i, G i →+* P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) @@ -626,10 +626,10 @@ to a unique map out of the direct limit. -/ noncomputable def lift (g : ∀ i, (G i) →⋆ₙ+* P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) : - DirectLimit G f →⋆ₙ+* P := { - (NonUnitalRing.lift G f P (fun _ => (g _).toNonUnitalRingHom) Hg) with - toFun := _root_.DirectLimit.lift _ (g · ·) (fun i j hij x ↦ (Hg i j hij x).symm) - map_star' := DirectLimit.induction _ fun i x ↦ by simp_rw [star_def, lift_def, map_star (g i)]} + DirectLimit G f →⋆ₙ+* P where + __ := (NonUnitalRing.lift G f P (fun _ => (g _).toNonUnitalRingHom) Hg) + toFun := _root_.DirectLimit.lift _ (g · ·) (fun i j hij x ↦ (Hg i j hij x).symm) + map_star' := DirectLimit.induction _ fun i x ↦ by simp_rw [star_def, lift_def, map_star (g i)] variable (g : ∀ i, G i →⋆ₙ+* P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) From 249547b78e3c3fd0a54630822086a5c46c36c225 Mon Sep 17 00:00:00 2001 From: drocta Date: Tue, 21 Apr 2026 16:31:17 -0700 Subject: [PATCH 12/18] improve whitespace --- Mathlib/Algebra/Colimit/DirectLimit.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index d6290dc11c872a..b7e544051f49b1 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -638,12 +638,11 @@ variable (g : ∀ i, G i →⋆ₙ+* P) (Hg : ∀ i j hij x, g j (f i j hij x) = @[ext] theorem hom_ext {g₁ g₂ : DirectLimit G f →⋆ₙ+* P} (h : ∀ i, g₁.comp (of G f i) = g₂.comp (of G f i)) : - g₁ = g₂ := by + g₁ = g₂ := by ext x induction x using DirectLimit.induction with | _ i x exact congr($(h i) x) - end StarRing end DirectLimit From 3ce7a77d8575e777907da1dcb8726de8500d455b Mon Sep 17 00:00:00 2001 From: drocta Date: Tue, 21 Apr 2026 16:37:46 -0700 Subject: [PATCH 13/18] add of_f, lift_of, hom_ext for DirectLimit.NonUnitalRing --- Mathlib/Algebra/Colimit/DirectLimit.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index b7e544051f49b1..ca275ae85a6505 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -546,6 +546,7 @@ nonrec def of (i) : G i →ₙ+* DirectLimit G f where map_zero' := (zero_def i).symm map_add' _ _ := (add_def ..).symm +@[simp] theorem 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] variable (G f) in @@ -561,6 +562,17 @@ noncomputable def lift map_zero' := by simp_rw [zero_def (Classical.arbitrary ι), lift_def, map_zero] map_add' := DirectLimit.induction₂ _ fun i x y ↦ by simp_rw [add_def, lift_def, map_add (g i)] +variable (g : ∀ i, G i →ₙ+* 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 →ₙ+* 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 NonUnitalRing namespace Ring From 04f2eb1da4e5c7c347c340832edd1b820126cec6 Mon Sep 17 00:00:00 2001 From: drocta Date: Wed, 22 Apr 2026 11:39:28 -0700 Subject: [PATCH 14/18] update list of categories which have lift showing that the DirectLimit is the colimit (making it a bulleted list) --- Mathlib/Algebra/Colimit/DirectLimit.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean index ca275ae85a6505..137599133054cf 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -38,7 +38,13 @@ universal object for each type of algebraic structure; the same type `DirectLimi works for all of them. This file is therefore more general than the `Module` and `Ring` files in terms of the variety of algebraic structures supported. -So far we only show that `DirectLimit` is the colimit in the categories of modules and rings, +So far we only show that `DirectLimit` is the colimit in the following categories: + +* modules +* non-unital semirings +* rings +* (non-unital) star rings + 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 equality criteria for `Module/AddCommGroup/Ring.DirectLimit`. From 8e2328dcc83dc7428b8ab321ed36c4563e5a320e Mon Sep 17 00:00:00 2001 From: drocta Date: Wed, 22 Apr 2026 11:59:40 -0700 Subject: [PATCH 15/18] remove excess newline --- 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 137599133054cf..985f7ab6daf68d 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -607,7 +607,6 @@ def lift (g : ∀ i, G i →+* P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm map_one' := by rw [one_def (Classical.arbitrary ι), lift_def, map_one] - variable (g : ∀ i, G i →+* 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 From a40734fd10e5a358c0123831222156a1d82a5982 Mon Sep 17 00:00:00 2001 From: drocta Date: Wed, 22 Apr 2026 12:04:09 -0700 Subject: [PATCH 16/18] in Algebra/Colimit/DirectLimit.lean, improve whitespace Co-authored-by: Eric Wieser --- 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 985f7ab6daf68d..62411df4d67952 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -87,7 +87,7 @@ instance : Star (DirectLimit G f) where star := .map f f (fun _ x ↦ star x) (fun i j h x ↦ map_star (f i j h) x) lemma star_def (i : ι) (x : G i) : - star ⟦⟨i, x⟩⟧ = (⟦⟨i, star x ⟩⟧ : DirectLimit G f) := by + star ⟦⟨i, x⟩⟧ = (⟦⟨i, star x⟩⟧ : DirectLimit G f) := by rfl end Star From 4399ee3a110b2ca0b2fe8e38e51b1deae19f6f08 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 23 Apr 2026 14:52:19 -0700 Subject: [PATCH 17/18] Apply suggestions from code review Co-authored-by: Eric Wieser --- 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 62411df4d67952..ebb8131e49341d 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -620,7 +620,7 @@ theorem hom_ext {g₁ g₂ : DirectLimit G f →+* P} (h : ∀ i, g₁.comp (of end Ring -namespace StarRing +namespace NonUnitalStarRing variable [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] variable [∀ i, StarRing (G i)] [∀ i j h, StarHomClass (T h) (G i) (G j)] @@ -660,6 +660,6 @@ theorem hom_ext {g₁ g₂ : DirectLimit G f →⋆ₙ+* P} induction x using DirectLimit.induction with | _ i x exact congr($(h i) x) -end StarRing +end NonUnitalStarRing end DirectLimit From 9b2d95248a19a95c7ade75879af77511a2ba2d44 Mon Sep 17 00:00:00 2001 From: drocta Date: Thu, 23 Apr 2026 15:10:15 -0700 Subject: [PATCH 18/18] update formatting in Algebra/Colimit/DirectLimit.lean move a colon to the end of the line before the type (`StarRing (DirectLimit G f)`) rather than at the start of the line with the type Co-authored-by: Jireh Loreaux --- 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 ebb8131e49341d..8a14961a3cdf05 100644 --- a/Mathlib/Algebra/Colimit/DirectLimit.lean +++ b/Mathlib/Algebra/Colimit/DirectLimit.lean @@ -347,8 +347,8 @@ instance [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomCl mul_zero := mul_zero instance [∀ i, NonUnitalNonAssocSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] - [∀ 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 star_add := star_add instance [∀ i, NonUnitalSemiring (G i)] [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)] :