feat(algebra/direct_sum*): relax a lot of constraints to add_comm_monoid (#3537)

Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: eric-wieser

src/algebra/direct_limit.lean

@@ -156,7 +156,7 @@ span_induction ((quotient.mk_eq_zero _).1 H)
       subst hxy,
       split,
       { intros i0 hi0,
-        rw [dfinsupp.mem_support_iff, dfinsupp.sub_apply, ← direct_sum.single_eq_lof,
+        rw [dfinsupp.mem_support_iff, direct_sum.sub_apply, ← direct_sum.single_eq_lof,
             ← direct_sum.single_eq_lof, dfinsupp.single_apply, dfinsupp.single_apply] at hi0,
         split_ifs at hi0 with hi hj hj, { rwa hi at hik }, { rwa hi at hik }, { rwa hj at hjk },
         exfalso, apply hi0, rw sub_zero },

src/algebra/direct_sum.lean

@@ -25,20 +25,34 @@ open_locale big_operators
 
 universes u v w u₁
 
-variables (ι : Type v) [dec_ι : decidable_eq ι] (β : ι → Type w) [Π i, add_comm_group (β i)]
+variables (ι : Type v) [dec_ι : decidable_eq ι] (β : ι → Type w)
 
-/-- `direct_sum β` is the direct sum of a family of additive commutative groups `β i`.
+/-- `direct_sum β` is the direct sum of a family of additive commutative monoids `β 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
+@[derive [has_coe_to_fun, add_comm_monoid, inhabited]]
+def direct_sum [Π i, add_comm_monoid (β i)] : Type* := Π₀ i, β i
 
 localized "notation `⨁` binders `, ` r:(scoped f, direct_sum _ f) := r" in direct_sum
 
 namespace direct_sum
 
 variables {ι}
 
+section add_comm_group
+
+variables [Π i, add_comm_group (β i)]
+
+instance : add_comm_group (direct_sum ι β) := dfinsupp.add_comm_group
+
+variables {β}
+@[simp] lemma sub_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ - g₂) i = g₁ i - g₂ i :=
+dfinsupp.sub_apply _ _ _
+
+end add_comm_group
+
+variables [Π i, add_comm_monoid (β i)]
+
 @[simp] lemma zero_apply (i : ι) : (0 : ⨁ i, β i) i = 0 := rfl
 
 variables {β}
@@ -80,13 +94,13 @@ begin
   solve_by_elim
 end
 
-variables {γ : Type u₁} [add_comm_group γ]
+variables {γ : Type u₁} [add_comm_monoid γ]
 variables (φ : Π i, β i →+ γ)
 
 variables (φ)
-/-- `to_group φ` is the natural homomorphism from `⨁ i, β i` to `γ`
+/-- `to_add_monoid φ` is the natural homomorphism from `⨁ i, β i` to `γ`
 induced by a family `φ` of homomorphisms `β i → γ`. -/
-def to_group : (⨁ i, β i) →+ γ :=
+def to_add_monoid : (⨁ i, β i) →+ γ :=
 { to_fun := (λ f,
     quotient.lift_on f (λ x, ∑ i in x.2.to_finset, φ i (x.1 i)) $ λ x y H,
     begin
@@ -121,17 +135,17 @@ def to_group : (⨁ i, β i) →+ γ :=
   map_zero' := rfl
 }
 
-@[simp] lemma to_group_of (i) (x : β i) : to_group φ (of β i x) = φ i x :=
+@[simp] lemma to_add_monoid_of (i) (x : β i) : to_add_monoid φ (of β i x) = φ i x :=
 (add_zero _).trans $ congr_arg (φ i) $ show (if H : i ∈ ({i} : finset _) then x else 0) = x,
 from dif_pos $ finset.mem_singleton_self i
 
 variables (ψ : (⨁ i, β i) →+ γ)
 
-theorem to_group.unique (f : ⨁ i, β i) :
-  ψ f = to_group (λ i, ψ.comp (of β i)) f :=
+theorem to_add_monoid.unique (f : ⨁ i, β i) :
+  ψ f = to_add_monoid (λ i, ψ.comp (of β i)) f :=
 direct_sum.induction_on f
   (by rw [add_monoid_hom.map_zero, add_monoid_hom.map_zero])
-  (λ i x, by rw [to_group_of, add_monoid_hom.comp_apply])
+  (λ i x, by rw [to_add_monoid_of, add_monoid_hom.comp_apply])
   (λ x y ihx ihy, by rw [add_monoid_hom.map_add, add_monoid_hom.map_add, ihx, ihy])
 
 variables (β)
@@ -140,21 +154,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 (λ (i : subtype T), β i) ⟨↑i, H i.prop⟩
+to_add_monoid $ λ i, of (λ (i : subtype T), β i) ⟨↑i, H i.prop⟩
 variables {β}
 
 omit dec_ι
 
 /-- The natural equivalence between `⨁ _ : ι, M` and `M` when `unique ι`. -/
-protected def id (M : Type v) (ι : Type* := punit) [add_comm_group M] [unique ι] :
+protected def id (M : Type v) (ι : Type* := punit) [add_comm_monoid M] [unique ι] :
   (⨁ (_ : ι), M) ≃+ M :=
-{ to_fun := direct_sum.to_group (λ _, add_monoid_hom.id M),
+{ to_fun := direct_sum.to_add_monoid (λ _, add_monoid_hom.id M),
   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])
-    (λ p x, by rw [unique.default_eq p, to_group_of]; refl)
+    (λ p x, by rw [unique.default_eq p, to_add_monoid_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 _ _ _,
-  ..direct_sum.to_group (λ _, add_monoid_hom.id M) }
+  right_inv := λ x, to_add_monoid_of _ _ _,
+  ..direct_sum.to_add_monoid (λ _, add_monoid_hom.id M) }
 
 end direct_sum

src/linear_algebra/direct_sum_module.lean

@@ -28,17 +28,17 @@ universes u v w u₁
 
 variables (R : Type u) [semiring R]
 variables (ι : Type v) [dec_ι : decidable_eq ι] (M : ι → Type w)
-variables [Π i, add_comm_group (M i)] [Π i, semimodule R (M i)]
+variables [Π i, add_comm_monoid (M i)] [Π i, semimodule R (M i)]
 include R
 
 namespace direct_sum
 open_locale direct_sum
 
 variables {R ι M}
 
-instance : semimodule R (⨁ i, M i) := @dfinsupp.to_semimodule ι M _ _ _ _
+instance : semimodule R (⨁ i, M i) := dfinsupp.to_semimodule
 
-@[simp] lemma smul_apply (b : R) (v : ⨁ i, M i) (i : ι) :
+lemma smul_apply (b : R) (v : ⨁ i, M i) (i : ι) :
   (b • v) i = b • (v i) := dfinsupp.smul_apply _ _ _
 
 include dec_ι
@@ -68,36 +68,36 @@ variables {R}
 lemma support_smul [Π (i : ι) (x : M i), decidable (x ≠ 0)]
   (c : R) (v : ⨁ i, M i) : (c • v).support ⊆ v.support := dfinsupp.support_smul _ _
 
-variables {N : Type u₁} [add_comm_group N] [semimodule R N]
+variables {N : Type u₁} [add_comm_monoid N] [semimodule R N]
 variables (φ : Π i, M i →ₗ[R] N)
 
 variables (R ι N φ)
 /-- The linear map constructed using the universal property of the coproduct. -/
 def to_module : (⨁ i, M i) →ₗ[R] N :=
-{ to_fun := to_group (λ i, (φ i).to_add_monoid_hom),
-  map_add' := (to_group (λ i, (φ i).to_add_monoid_hom)).map_add,
+{ to_fun := to_add_monoid (λ i, (φ i).to_add_monoid_hom),
+  map_add' := (to_add_monoid (λ i, (φ i).to_add_monoid_hom)).map_add,
   map_smul' := λ c x, direct_sum.induction_on x
     (by rw [smul_zero, add_monoid_hom.map_zero, smul_zero])
     (λ i x,
-      by rw [← of_smul, to_group_of, to_group_of, linear_map.to_add_monoid_hom_coe,
+      by rw [← of_smul, to_add_monoid_of, to_add_monoid_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]),
-  ..(to_group (λ i, (φ i).to_add_monoid_hom))}
+  ..(to_add_monoid (λ i, (φ i).to_add_monoid_hom))}
 
 variables {ι N φ}
 
 /-- The map constructed using the universal property gives back the original maps when
 restricted to each component. -/
 @[simp] lemma to_module_lof (i) (x : M i) : to_module R ι N φ (lof R ι M i x) = φ i x :=
-to_group_of (λ i, (φ i).to_add_monoid_hom) i x
+to_add_monoid_of (λ i, (φ i).to_add_monoid_hom) i x
 
 variables (ψ : (⨁ i, M i) →ₗ[R] N)
 
 /-- Every linear map from a direct sum agrees with the one obtained by applying
 the universal property to each of its components. -/
 theorem to_module.unique (f : ⨁ i, M i) : ψ f = to_module R ι N (λ i, ψ.comp $ lof R ι M i) f :=
-to_group.unique ψ.to_add_monoid_hom f
+to_add_monoid.unique ψ.to_add_monoid_hom f
 
 variables {ψ} {ψ' : (⨁ i, M i) →ₗ[R] N}
 
@@ -117,7 +117,8 @@ omit dec_ι
 
 /-- 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) (ι : Type* := punit) [add_comm_group M] [semimodule R M] [unique ι] :
+protected def lid (M : Type v) (ι : Type* := punit) [add_comm_monoid M] [semimodule R M]
+  [unique ι] :
   (⨁ (_ : ι), M) ≃ₗ M :=
 { .. direct_sum.id M ι,
   .. to_module R ι M (λ i, linear_map.id) }