feat(algebra/direct_sum): Fix two todos about generalizing over uniqu…

…e types (#4764)

Also promotes `id` to a `≃+`, and prefers coercion over direct use of `subtype.val`.

src/algebra/direct_sum.lean

@@ -30,20 +30,14 @@ variables (ι : Type v) [dec_ι : decidable_eq ι] (β : ι → Type w) [Π i, a
 /-- `direct_sum β` is the direct sum of a family of additive commutative groups `β i`.
 
 Note: `open_locale direct_sum` will enable the notation `⨁ i, β i` for `direct_sum β`. -/
+@[derive [has_coe_to_fun, add_comm_group, inhabited]]
 def direct_sum : Type* := Π₀ i, β i
 
 localized "notation `⨁` binders `, ` r:(scoped f, direct_sum _ f) := r" in direct_sum
 
 namespace direct_sum
 
-variables {ι β}
-
-instance : add_comm_group (⨁ i, β i) :=
-dfinsupp.add_comm_group
-
-instance : inhabited (⨁ i, β i) := ⟨0⟩
-
-variables β
+variables {ι}
 
 include dec_ι
 
@@ -66,7 +60,7 @@ theorem mk_injective (s : finset ι) : function.injective (mk β s) :=
 dfinsupp.mk_injective s
 
 theorem of_injective (i : ι) : function.injective (of β i) :=
-λ x y H, congr_fun (mk_injective _ H) ⟨i, by simp⟩
+dfinsupp.single_injective
 
 @[elab_as_eliminator]
 protected theorem induction_on {C : (⨁ i, β i) → Prop}
@@ -139,23 +133,21 @@ where `h : S ⊆ T`. -/
 -- TODO: generalize this to remove the assumption `S ⊆ T`.
 def set_to_set (S T : set ι) (H : S ⊆ T) :
   (⨁ (i : S), β i) →+ (⨁ (i : T), β i) :=
-to_group $ λ i, of (β ∘ @subtype.val _ T) ⟨i.1, H i.2⟩
+to_group $ λ i, of (λ (i : subtype T), β i) ⟨↑i, H i.prop⟩
 variables {β}
 
 omit dec_ι
 
-/-- The natural equivalence between `⨁ _ : punit, M` and `M`. -/
--- TODO: generalize this to a sum over any type `ι` that is `unique ι`.
-protected def id (M : Type v) [add_comm_group M] : (⨁ (_ : punit), M) ≃ M :=
+/-- The natural equivalence between `⨁ _ : ι, M` and `M` when `unique ι`. -/
+protected def id (M : Type v) (ι : Type* := punit) [add_comm_group M] [unique ι] :
+  (⨁ (_ : ι), M) ≃+ M :=
 { to_fun := direct_sum.to_group (λ _, add_monoid_hom.id M),
-  inv_fun := of (λ _, M) punit.star,
+  inv_fun := of (λ _, M) (default ι),
   left_inv := λ x, direct_sum.induction_on x
     (by rw [add_monoid_hom.map_zero, add_monoid_hom.map_zero])
-    (λ ⟨⟩ x, by rw [to_group_of]; refl)
+    (λ p x, by rw [unique.default_eq p, to_group_of]; refl)
     (λ x y ihx ihy, by rw [add_monoid_hom.map_add, add_monoid_hom.map_add, ihx, ihy]),
-  right_inv := λ x, to_group_of _ _ _ }
-
-instance : has_coe_to_fun (⨁ i, β i) :=
-dfinsupp.has_coe_to_fun
+  right_inv := λ x, to_group_of _ _ _,
+  ..direct_sum.to_group (λ _, add_monoid_hom.id M) }
 
 end direct_sum

src/data/dfinsupp.lean

@@ -308,6 +308,9 @@ by simp only [single_apply, dif_pos rfl]
 lemma single_eq_of_ne {i i' b} (h : i ≠ i') : (single i b : Π₀ i, β i) i' = 0 :=
 by simp only [single_apply, dif_neg h]
 
+lemma single_injective {i} : function.injective (single i : β i → Π₀ i, β i) :=
+λ x y H, congr_fun (mk_injective _ H) ⟨i, by simp⟩
+
 /-- Redefine `f i` to be `0`. -/
 def erase (i : ι) (f : Π₀ i, β i) : Π₀ i, β i :=
 quotient.lift_on f (λ x, ⟦(⟨λ j, if j = i then 0 else x.1 j, x.2,

src/linear_algebra/direct_sum_module.lean

@@ -75,7 +75,8 @@ def to_module : (⨁ i, M i) →ₗ[R] N :=
       by rw [← of_smul, to_group_of, to_group_of, linear_map.to_add_monoid_hom_coe,
         linear_map.map_smul])
     (λ x y ihx ihy,
-      by rw [smul_add, add_monoid_hom.map_add, ihx, ihy, add_monoid_hom.map_add, smul_add]) }
+      by rw [smul_add, add_monoid_hom.map_add, ihx, ihy, add_monoid_hom.map_add, smul_add]),
+  ..(to_group (λ i, (φ i).to_add_monoid_hom))}
 
 variables {ι N φ}
 
@@ -103,16 +104,16 @@ into a larger subset of the direct summands, as a linear map.
 -/
 def lset_to_set (S T : set ι) (H : S ⊆ T) :
   (⨁ (i : S), M i) →ₗ (⨁ (i : T), M i) :=
-to_module R _ _ $ λ i, lof R T (M ∘ @subtype.val _ T) ⟨i.1, H i.2⟩
+to_module R _ _ $ λ i, lof R T (λ (i : subtype T), M i) ⟨i, H i.prop⟩
 
 omit dec_ι
 
-/-- The natural linear equivalence between `⨁ _ : punit, M` and `M`. -/
+/-- The natural linear equivalence between `⨁ _ : ι, M` and `M` when `unique ι`. -/
 -- TODO: generalize this to arbitrary index type `ι` with `unique ι`
-protected def lid (M : Type v) [add_comm_group M] [semimodule R M] :
-  (⨁ (_ : punit), M) ≃ₗ M :=
-{ .. direct_sum.id M,
-  .. to_module R punit M (λ i, linear_map.id) }
+protected def lid (M : Type v) (ι : Type* := punit) [add_comm_group M] [semimodule R M] [unique ι] :
+  (⨁ (_ : ι), M) ≃ₗ M :=
+{ .. direct_sum.id M ι,
+  .. to_module R ι M (λ i, linear_map.id) }
 
 variables (ι M)
 /-- The projection map onto one component, as a linear map. -/