From 9a4ae4a9c08ba44f8b3a9deff5161b2cb47f7631 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 20 Nov 2023 19:06:29 +0000 Subject: [PATCH] chore: add some Unique instances (#8500) The aim is to remove some extraneous Nonempty assumptions in Algebra/DirectLimit. Co-authored-by: Junyan Xu Co-authored-by: Jujian Zhang --- .../Algebra/Category/ModuleCat/Limits.lean | 2 +- Mathlib/Algebra/DirectLimit.lean | 32 +++++++++++++------ Mathlib/Algebra/Group/TypeTags.lean | 6 ++++ Mathlib/Data/Multiset/Basic.lean | 4 +++ Mathlib/Data/Quot.lean | 5 +++ Mathlib/GroupTheory/Abelianization.lean | 2 ++ Mathlib/GroupTheory/FreeAbelianGroup.lean | 2 ++ Mathlib/GroupTheory/FreeGroup/Basic.lean | 3 ++ Mathlib/LinearAlgebra/TensorProduct.lean | 10 ++++++ Mathlib/SetTheory/Cardinal/Ordinal.lean | 1 - 10 files changed, 56 insertions(+), 11 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Limits.lean b/Mathlib/Algebra/Category/ModuleCat/Limits.lean index dcdd78dcfaa88..fd2e8aff1d249 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Limits.lean +++ b/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 diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean index 9e3d45e2c64a8..4016d06a42961 100644 --- a/Mathlib/Algebra/DirectLimit.lean +++ b/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 diff --git a/Mathlib/Algebra/Group/TypeTags.lean b/Mathlib/Algebra/Group/TypeTags.lean index 289cbad9fa875..9cf73af1c836a 100644 --- a/Mathlib/Algebra/Group/TypeTags.lean +++ b/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) diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index 3c5805cc6345f..a6960ea6cdef6 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/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 diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean index baee0240d5f37..5e41921a269cb 100644 --- a/Mathlib/Data/Quot.lean +++ b/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 diff --git a/Mathlib/GroupTheory/Abelianization.lean b/Mathlib/GroupTheory/Abelianization.lean index f6ae1c63f35d5..8bd2aee2d5b81 100644 --- a/Mathlib/GroupTheory/Abelianization.lean +++ b/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) diff --git a/Mathlib/GroupTheory/FreeAbelianGroup.lean b/Mathlib/GroupTheory/FreeAbelianGroup.lean index 47fb1d5b944dd..458563bdfd540 100644 --- a/Mathlib/GroupTheory/FreeAbelianGroup.lean +++ b/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 diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean index 4f7a0e4332bd8..15bb93d17693e 100644 --- a/Mathlib/GroupTheory/FreeGroup/Basic.lean +++ b/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 => diff --git a/Mathlib/LinearAlgebra/TensorProduct.lean b/Mathlib/LinearAlgebra/TensorProduct.lean index 2615fc9968e5a..f16d5d672c804 100644 --- a/Mathlib/LinearAlgebra/TensorProduct.lean +++ b/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) diff --git a/Mathlib/SetTheory/Cardinal/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Ordinal.lean index c29c28fc154e8..916c1027e2bf9 100644 --- a/Mathlib/SetTheory/Cardinal/Ordinal.lean +++ b/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