[Merged by Bors] - feat(Algebra/Colimit/DirectLimit): add star structures (Star, StarRing, etc.) on DirectLimit

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)]
 
@@ -97,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)]
 
@@ -108,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
@@ -140,6 +182,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)]
 
@@ -291,6 +342,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
@@ -480,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 ι]
@@ -503,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)
 
@@ -523,4 +599,49 @@ 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 (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) →⋆ₙ+* 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 →⋆ₙ+* 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 StarRing
+
 end DirectLimit