chore: add some Unique instances (#8500)

The aim is to remove some extraneous Nonempty assumptions in Algebra/DirectLimit.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

Mathlib/Algebra/Category/ModuleCat/Limits.lean

@@ -225,7 +225,7 @@ def directLimitCocone : Cocone (directLimitDiagram G f) where
 /-- The unbundled `directLimit` of modules is a colimit
 in the sense of `CategoryTheory`. -/
 @[simps]
-def directLimitIsColimit [Nonempty ι] [IsDirected ι (· ≤ ·)] : IsColimit (directLimitCocone G f)
+def directLimitIsColimit [IsDirected ι (· ≤ ·)] : IsColimit (directLimitCocone G f)
     where
   desc s :=
     DirectLimit.lift R ι G f s.ι.app fun i j h x => by

Mathlib/Algebra/DirectLimit.lean

@@ -103,6 +103,9 @@ instance module : Module R (DirectLimit G f) :=
 instance inhabited : Inhabited (DirectLimit G f) :=
   ⟨0⟩
 
+instance unique [IsEmpty ι] : Unique (DirectLimit G f) :=
+  inferInstanceAs <| Unique (Quotient _)
+
 variable (R ι)
 
 /-- The canonical map from a component to the direct limit. -/
@@ -160,11 +163,13 @@ theorem lift_of {i} (x) : lift R ι G f g Hg (of R ι G f i x) = g i x :=
   DirectSum.toModule_lof R _ _
 #align module.direct_limit.lift_of Module.DirectLimit.lift_of
 
-theorem lift_unique [Nonempty ι] [IsDirected ι (· ≤ ·)] (F : DirectLimit G f →ₗ[R] P) (x) :
+theorem lift_unique [IsDirected ι (· ≤ ·)] (F : DirectLimit G f →ₗ[R] P) (x) :
     F x =
       lift R ι G f (fun i => F.comp <| of R ι G f i)
-        (fun i j hij x => by rw [LinearMap.comp_apply, of_f]; rfl) x :=
-  DirectLimit.induction_on x fun i x => by rw [lift_of]; rfl
+        (fun i j hij x => by rw [LinearMap.comp_apply, of_f]; rfl) x := by
+  cases isEmpty_or_nonempty ι
+  · simp_rw [Subsingleton.elim x 0, _root_.map_zero]
+  · exact DirectLimit.induction_on x fun i x => by rw [lift_of]; rfl
 #align module.direct_limit.lift_unique Module.DirectLimit.lift_unique
 
 section Totalize
@@ -294,6 +299,8 @@ instance : AddCommGroup (DirectLimit G f) :=
 instance : Inhabited (DirectLimit G f) :=
   ⟨0⟩
 
+instance [IsEmpty ι] : Unique (DirectLimit G f) := Module.DirectLimit.unique _ _
+
 /-- The canonical map from a component to the direct limit. -/
 def of (i) : G i →ₗ[ℤ] DirectLimit G f :=
   Module.DirectLimit.of ℤ ι G (fun i j hij => (f i j hij).toIntLinearMap) i
@@ -342,9 +349,11 @@ theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x :=
   Module.DirectLimit.lift_of _ _ _
 #align add_comm_group.direct_limit.lift_of AddCommGroup.DirectLimit.lift_of
 
-theorem lift_unique [Nonempty ι] [IsDirected ι (· ≤ ·)] (F : DirectLimit G f →+ P) (x) :
-    F x = lift G f P (fun i => F.comp (of G f i).toAddMonoidHom) (fun i j hij x => by simp) x :=
-  DirectLimit.induction_on x fun i x => by simp
+theorem lift_unique [IsDirected ι (· ≤ ·)] (F : DirectLimit G f →+ P) (x) :
+    F x = lift G f P (fun i => F.comp (of G f i).toAddMonoidHom) (fun i j hij x => by simp) x := by
+  cases isEmpty_or_nonempty ι
+  · simp_rw [Subsingleton.elim x 0, _root_.map_zero]
+  · exact DirectLimit.induction_on x fun i x => by simp
 #align add_comm_group.direct_limit.lift_unique AddCommGroup.DirectLimit.lift_unique
 
 end DirectLimit
@@ -671,9 +680,14 @@ theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x :=
   FreeCommRing.lift_of _ _
 #align ring.direct_limit.lift_of Ring.DirectLimit.lift_of
 
-theorem lift_unique [Nonempty ι] [IsDirected ι (· ≤ ·)] (F : DirectLimit G f →+* P) (x) :
-    F x = lift G f P (fun i => F.comp <| of G f i) (fun i j hij x => by simp [of_f]) x :=
-  DirectLimit.induction_on x fun i x => by simp [lift_of]
+theorem lift_unique [IsDirected ι (· ≤ ·)] (F : DirectLimit G f →+* P) (x) :
+    F x = lift G f P (fun i => F.comp <| of G f i) (fun i j hij x => by simp [of_f]) x := by
+  cases isEmpty_or_nonempty ι
+  · apply FunLike.congr_fun
+    apply Ideal.Quotient.ringHom_ext
+    refine FreeCommRing.hom_ext fun ⟨i, _⟩ ↦ ?_
+    exact IsEmpty.elim' inferInstance i
+  · exact DirectLimit.induction_on x fun i x => by simp [lift_of]
 #align ring.direct_limit.lift_unique Ring.DirectLimit.lift_unique
 
 end DirectLimit

Mathlib/Algebra/Group/TypeTags.lean

@@ -116,12 +116,18 @@ theorem ofMul_toMul (x : Additive α) : ofMul (toMul x) = x :=
   rfl
 #align of_mul_to_mul ofMul_toMul
 
+instance [Subsingleton α] : Subsingleton (Additive α) := toMul.injective.subsingleton
+instance [Subsingleton α] : Subsingleton (Multiplicative α) := toAdd.injective.subsingleton
+
 instance [Inhabited α] : Inhabited (Additive α) :=
   ⟨ofMul default⟩
 
 instance [Inhabited α] : Inhabited (Multiplicative α) :=
   ⟨ofAdd default⟩
 
+instance [Unique α] : Unique (Additive α) := toMul.unique
+instance [Unique α] : Unique (Multiplicative α) := toAdd.unique
+
 instance [Finite α] : Finite (Additive α) :=
   Finite.of_equiv α (by rfl)
 

Mathlib/Data/Multiset/Basic.lean

@@ -95,6 +95,10 @@ instance inhabitedMultiset : Inhabited (Multiset α) :=
   ⟨0⟩
 #align multiset.inhabited_multiset Multiset.inhabitedMultiset
 
+instance [IsEmpty α] : Unique (Multiset α) where
+  default := 0
+  uniq := by rintro ⟨_ | ⟨a, l⟩⟩; exacts [rfl, isEmptyElim a]
+
 @[simp]
 theorem coe_nil : (@nil α : Multiset α) = 0 :=
   rfl

Mathlib/Data/Quot.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.Init.Data.Quot
 import Mathlib.Logic.Relator
+import Mathlib.Logic.Unique
 import Mathlib.Mathport.Notation
 
 #align_import data.quot from "leanprover-community/mathlib"@"6ed6abbde29b8f630001a1b481603f657a3384f1"
@@ -55,6 +56,8 @@ protected instance Subsingleton [Subsingleton α] : Subsingleton (Quot ra) :=
   ⟨fun x ↦ Quot.induction_on x fun _ ↦ Quot.ind fun _ ↦ congr_arg _ (Subsingleton.elim _ _)⟩
 #align quot.subsingleton Quot.Subsingleton
 
+instance [Unique α] : Unique (Quot ra) := Unique.mk' _
+
 /-- Recursion on two `Quotient` arguments `a` and `b`, result type depends on `⟦a⟧` and `⟦b⟧`. -/
 protected def hrecOn₂ (qa : Quot ra) (qb : Quot rb) (f : ∀ a b, φ ⟦a⟧ ⟦b⟧)
     (ca : ∀ {b a₁ a₂}, ra a₁ a₂ → HEq (f a₁ b) (f a₂ b))
@@ -230,6 +233,8 @@ instance instInhabitedQuotient (s : Setoid α) [Inhabited α] : Inhabited (Quoti
 instance instSubsingletonQuotient (s : Setoid α) [Subsingleton α] : Subsingleton (Quotient s) :=
   Quot.Subsingleton
 
+instance instUniqueQuotient (s : Setoid α) [Unique α] : Unique (Quotient s) := Unique.mk' _
+
 instance {α : Type*} [Setoid α] : IsEquiv α (· ≈ ·) where
   refl := Setoid.refl
   symm _ _ := Setoid.symm

Mathlib/GroupTheory/Abelianization.lean

@@ -100,6 +100,8 @@ instance commGroup : CommGroup (Abelianization G) :=
 instance : Inhabited (Abelianization G) :=
   ⟨1⟩
 
+instance [Unique G] : Unique (Abelianization G) := Quotient.instUniqueQuotient _
+
 instance [Fintype G] [DecidablePred (· ∈ commutator G)] : Fintype (Abelianization G) :=
   QuotientGroup.fintype (commutator G)
 

Mathlib/GroupTheory/FreeAbelianGroup.lean

@@ -84,6 +84,8 @@ instance FreeAbelianGroup.addCommGroup : AddCommGroup (FreeAbelianGroup α) :=
 instance : Inhabited (FreeAbelianGroup α) :=
   ⟨0⟩
 
+instance [IsEmpty α] : Unique (FreeAbelianGroup α) := by unfold FreeAbelianGroup; infer_instance
+
 variable {α}
 
 namespace FreeAbelianGroup

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -529,6 +529,9 @@ theorem one_eq_mk : (1 : FreeGroup α) = mk [] :=
 instance : Inhabited (FreeGroup α) :=
   ⟨1⟩
 
+@[to_additive]
+instance [IsEmpty α] : Unique (FreeGroup α) := by unfold FreeGroup; infer_instance
+
 @[to_additive]
 instance : Mul (FreeGroup α) :=
   ⟨fun x y =>

Mathlib/LinearAlgebra/TensorProduct.lean

@@ -169,6 +169,16 @@ theorem tmul_add (m : M) (n₁ n₂ : N) : m ⊗ₜ (n₁ + n₂) = m ⊗ₜ n
   Eq.symm <| Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_add_right _ _ _
 #align tensor_product.tmul_add TensorProduct.tmul_add
 
+instance uniqueLeft [Subsingleton M] : Unique (M ⊗[R] N) where
+  default := 0
+  uniq z := z.induction_on rfl (fun x y ↦ by rw [Subsingleton.elim x 0, zero_tmul]; rfl) <| by
+    rintro _ _ rfl rfl; apply add_zero
+
+instance uniqueRight [Subsingleton N] : Unique (M ⊗[R] N) where
+  default := 0
+  uniq z := z.induction_on rfl (fun x y ↦ by rw [Subsingleton.elim y 0, tmul_zero]; rfl) <| by
+    rintro _ _ rfl rfl; apply add_zero
+
 section
 
 variable (R R' M N)

Mathlib/SetTheory/Cardinal/Ordinal.lean

@@ -1071,7 +1071,6 @@ theorem mk_multiset_of_nonempty (α : Type u) [Nonempty α] : #(Multiset α) = m
 theorem mk_multiset_of_infinite (α : Type u) [Infinite α] : #(Multiset α) = #α := by simp
 #align cardinal.mk_multiset_of_infinite Cardinal.mk_multiset_of_infinite
 
-@[simp]
 theorem mk_multiset_of_isEmpty (α : Type u) [IsEmpty α] : #(Multiset α) = 1 :=
   Multiset.toFinsupp.toEquiv.cardinal_eq.trans (by simp)
 #align cardinal.mk_multiset_of_is_empty Cardinal.mk_multiset_of_isEmpty