refactor(algebra/direct_sum/basic): use the new polymorphic subobject API (#14341)

This doesn't let us deduplicate the lattice lemmas, but does eliminate the duplicate instances and definitions!

This merges:

* `direct_sum.add_submonoid_is_internal`, `direct_sum.add_subgroup_is_internal`, `direct_sum.submodule_is_internal` into `direct_sum.is_internal`
* `direct_sum.add_submonoid_coe`, `direct_sum.add_subgroup_coe` into `direct_sum.coe_add_monoid_hom`
* `direct_sum.add_submonoid_coe_ring_hom`, `direct_sum.add_subgroup_coe_ring_hom` into `direct_sum.coe_ring_hom`
* `add_submonoid.gsemiring`, `add_subgroup.gsemiring`, `submodule.gsemiring` into `set_like.gsemiring`
* `add_submonoid.gcomm_semiring`, `add_subgroup.gcomm_semiring`, `submodule.gcomm_semiring` into `set_like.gcomm_semiring`

Renames

* `direct_sum.submodule_coe` into `direct_sum.coe_linear_map`
* `direct_sum.submodule_coe_alg_hom` into `direct_sum.coe_alg_hom

And adds:

* `set_like.gnon_unital_non_assoc_semiring`, now that it doesn't need to be repeated three times!

A large number of related lemmas are also renamed to match the new definition names.

This was what originally motivated the `set_like` typeclass; thanks to @Vierkantor for doing the subobject follow up I never got around to!

Author: eric-wieser

counterexamples/direct_sum_is_internal.lean

@@ -14,7 +14,7 @@ This shows that while `ℤ≤0` and `ℤ≥0` are complementary `ℕ`-submodules
 implies as a collection they are `complete_lattice.independent` and that they span all of `ℤ`, they
 do not form a decomposition into a direct sum.
 
-This file demonstrates why `direct_sum.submodule_is_internal_of_independent_of_supr_eq_top` must
+This file demonstrates why `direct_sum.is_internal_submodule_of_independent_of_supr_eq_top` must
 take `ring R` and not `semiring R`.
 -/
 
@@ -89,5 +89,5 @@ begin
 end
 
 /-- And so they do not represent an internal direct sum. -/
-lemma with_sign.not_internal : ¬direct_sum.submodule_is_internal with_sign :=
+lemma with_sign.not_internal : ¬direct_sum.is_internal with_sign :=
 with_sign.not_injective ∘ and.elim_left

counterexamples/homogeneous_prime_not_prime.lean

@@ -91,7 +91,7 @@ def grading.decompose : (R × R) →+ direct_sum two (λ i, grading R i) :=
   end }
 
 lemma grading.left_inv :
-  function.left_inverse grading.decompose (submodule_coe (grading R)) := λ zz,
+  function.left_inverse grading.decompose (coe_linear_map (grading R)) := λ zz,
 begin
   induction zz using direct_sum.induction_on with i zz d1 d2 ih1 ih2,
   { simp only [map_zero],},
@@ -101,11 +101,11 @@ begin
 end
 
 lemma grading.right_inv :
-  function.right_inverse grading.decompose (submodule_coe (grading R)) := λ zz,
+  function.right_inverse grading.decompose (coe_linear_map (grading R)) := λ zz,
 begin
   cases zz with a b,
   unfold grading.decompose,
-  simp only [add_monoid_hom.coe_mk, map_add, submodule_coe_of, subtype.coe_mk, prod.mk_add_mk,
+  simp only [add_monoid_hom.coe_mk, map_add, coe_linear_map_of, subtype.coe_mk, prod.mk_add_mk,
     add_zero, add_sub_cancel'_right],
 end
 

docs/undergrad.yaml

@@ -9,7 +9,7 @@ Linear algebra:
     vector subspace: 'subspace'
     quotient space: 'submodule.has_quotient'
     sum of subspaces: 'submodule.complete_lattice'
-    direct sum: 'direct_sum.submodule_is_internal'
+    direct sum: 'direct_sum.is_internal'
     complementary subspaces: 'submodule.exists_is_compl'
     linear independence: 'linear_independent'
     generating sets: 'submodule.span'

src/algebra/direct_sum/basic.lean

@@ -245,73 +245,43 @@ noncomputable def sigma_curry_equiv : (⨁ (i : Σ i, _), δ i.1 i.2) ≃+ ⨁ i
 end sigma
 
 /-- The canonical embedding from `⨁ i, A i` to `M` where `A` is a collection of `add_submonoid M`
-indexed by `ι`-/
-def add_submonoid_coe {M : Type*} [decidable_eq ι] [add_comm_monoid M]
-  (A : ι → add_submonoid M) : (⨁ i, A i) →+ M :=
-to_add_monoid (λ i, (A i).subtype)
-
-@[simp] lemma add_submonoid_coe_of {M : Type*} [decidable_eq ι] [add_comm_monoid M]
-  (A : ι → add_submonoid M) (i : ι) (x : A i) :
-  add_submonoid_coe A (of (λ i, A i) i x) = x :=
+indexed by `ι`.
+
+When `S = submodule _ M`, this is available as a `linear_map`, `direct_sum.coe_linear_map`. -/
+protected def coe_add_monoid_hom {M S : Type*} [decidable_eq ι] [add_comm_monoid M]
+  [set_like S M] [add_submonoid_class S M] (A : ι → S) : (⨁ i, A i) →+ M :=
+to_add_monoid (λ i, add_submonoid_class.subtype (A i))
+
+@[simp] lemma coe_add_monoid_hom_of {M S : Type*} [decidable_eq ι] [add_comm_monoid M]
+  [set_like S M] [add_submonoid_class S M] (A : ι → S) (i : ι) (x : A i) :
+  direct_sum.coe_add_monoid_hom A (of (λ i, A i) i x) = x :=
 to_add_monoid_of _ _ _
 
-lemma coe_of_add_submonoid_apply {M : Type*} [decidable_eq ι] [add_comm_monoid M]
-  {A : ι → add_submonoid M} (i j : ι) (x : A i) :
+lemma coe_of_apply {M S : Type*} [decidable_eq ι] [add_comm_monoid M]
+  [set_like S M] [add_submonoid_class S M] {A : ι → S} (i j : ι) (x : A i) :
   (of _ i x j : M) = if i = j then x else 0 :=
 begin
   obtain rfl | h := decidable.eq_or_ne i j,
   { rw [direct_sum.of_eq_same, if_pos rfl], },
-  { rw [direct_sum.of_eq_of_ne _ _ _ _ h, if_neg h, add_submonoid.coe_zero], },
+  { rw [direct_sum.of_eq_of_ne _ _ _ _ h, if_neg h, add_submonoid_class.coe_zero], },
 end
 
-/-- The `direct_sum` formed by a collection of `add_submonoid`s of `M` is said to be internal if the
-canonical map `(⨁ i, A i) →+ M` is bijective.
+/-- The `direct_sum` formed by a collection of additive submonoids (or subgroups, or submodules) of
+`M` is said to be internal if the canonical map `(⨁ i, A i) →+ M` is bijective.
 
-See `direct_sum.add_subgroup_is_internal` for the same statement about `add_subgroup`s. -/
-def add_submonoid_is_internal {M : Type*} [decidable_eq ι] [add_comm_monoid M]
-  (A : ι → add_submonoid M) : Prop :=
-function.bijective (add_submonoid_coe A)
+For the alternate statement in terms of independence and spanning, see
+`direct_sum.subgroup_is_internal_iff_independent_and_supr_eq_top` and
+`direct_sum.is_internal_submodule_iff_independent_and_supr_eq_top`. -/
+def is_internal {M S : Type*} [decidable_eq ι] [add_comm_monoid M]
+  [set_like S M] [add_submonoid_class S M] (A : ι → S) : Prop :=
+function.bijective (direct_sum.coe_add_monoid_hom A)
 
-lemma add_submonoid_is_internal.supr_eq_top {M : Type*} [decidable_eq ι] [add_comm_monoid M]
+lemma is_internal.add_submonoid_supr_eq_top {M : Type*} [decidable_eq ι] [add_comm_monoid M]
   (A : ι → add_submonoid M)
-  (h : add_submonoid_is_internal A) : supr A = ⊤ :=
+  (h : is_internal A) : supr A = ⊤ :=
 begin
   rw [add_submonoid.supr_eq_mrange_dfinsupp_sum_add_hom, add_monoid_hom.mrange_top_iff_surjective],
   exact function.bijective.surjective h,
 end
 
-/-- The canonical embedding from `⨁ i, A i` to `M`  where `A` is a collection of `add_subgroup M`
-indexed by `ι`-/
-def add_subgroup_coe {M : Type*} [decidable_eq ι] [add_comm_group M]
-  (A : ι → add_subgroup M) : (⨁ i, A i) →+ M :=
-to_add_monoid (λ i, (A i).subtype)
-
-@[simp] lemma add_subgroup_coe_of {M : Type*} [decidable_eq ι] [add_comm_group M]
-  (A : ι → add_subgroup M) (i : ι) (x : A i) :
-  add_subgroup_coe A (of (λ i, A i) i x) = x :=
-to_add_monoid_of _ _ _
-
-lemma coe_of_add_subgroup_apply {M : Type*} [decidable_eq ι] [add_comm_group M]
-  {A : ι → add_subgroup M} (i j : ι) (x : A i) :
-  (of _ i x j : M) = if i = j then x else 0 :=
-begin
-  obtain rfl | h := decidable.eq_or_ne i j,
-  { rw [direct_sum.of_eq_same, if_pos rfl], },
-  { rw [direct_sum.of_eq_of_ne _ _ _ _ h, if_neg h, add_subgroup.coe_zero], },
-end
-
-/-- The `direct_sum` formed by a collection of `add_subgroup`s of `M` is said to be internal if the
-canonical map `(⨁ i, A i) →+ M` is bijective.
-
-See `direct_sum.submodule_is_internal` for the same statement about `submodules`s. -/
-def add_subgroup_is_internal {M : Type*} [decidable_eq ι] [add_comm_group M]
-  (A : ι → add_subgroup M) : Prop :=
-function.bijective (add_subgroup_coe A)
-
-lemma add_subgroup_is_internal.to_add_submonoid
-  {M : Type*} [decidable_eq ι] [add_comm_group M] (A : ι → add_subgroup M) :
-  add_subgroup_is_internal A ↔
-    add_submonoid_is_internal (λ i, (A i).to_add_submonoid) :=
-iff.rfl
-
 end direct_sum

src/algebra/direct_sum/internal.lean

@@ -14,24 +14,23 @@ import algebra.direct_sum.algebra
 This module provides `gsemiring` and `gcomm_semiring` instances for a collection of subobjects `A`
 when a `set_like.graded_monoid` instance is available:
 
-* on `add_submonoid R`s: `add_submonoid.gsemiring`, `add_submonoid.gcomm_semiring`.
-* on `add_subgroup R`s: `add_subgroup.gsemiring`, `add_subgroup.gcomm_semiring`.
-* on `submodule S R`s: `submodule.gsemiring`, `submodule.gcomm_semiring`.
+* `set_like.gnon_unital_non_assoc_semiring`
+* `set_like.gsemiring`
+* `set_like.gcomm_semiring`
 
 With these instances in place, it provides the bundled canonical maps out of a direct sum of
 subobjects into their carrier type:
 
-* `direct_sum.add_submonoid_coe_ring_hom` (a `ring_hom` version of `direct_sum.add_submonoid_coe`)
-* `direct_sum.add_subgroup_coe_ring_hom` (a `ring_hom` version of `direct_sum.add_subgroup_coe`)
-* `direct_sum.submodule_coe_alg_hom` (an `alg_hom` version of `direct_sum.submodule_coe`)
+* `direct_sum.coe_ring_hom` (a `ring_hom` version of `direct_sum.coe_add_monoid_hom`)
+* `direct_sum.coe_alg_hom` (an `alg_hom` version of `direct_sum.submodule_coe`)
 
 Strictly the definitions in this file are not sufficient to fully define an "internal" direct sum;
-to represent this case, `(h : direct_sum.submodule_is_internal A) [set_like.graded_monoid A]` is
+to represent this case, `(h : direct_sum.is_internal A) [set_like.graded_monoid A]` is
 needed. In the future there will likely be a data-carrying, constructive, typeclass version of
-`direct_sum.submodule_is_internal` for providing an explicit decomposition function.
+`direct_sum.is_internal` for providing an explicit decomposition function.
 
 When `complete_lattice.independent (set.range A)` (a weaker condition than
-`direct_sum.submodule_is_internal A`), these provide a grading of `⨆ i, A i`, and the
+`direct_sum.is_internal A`), these provide a grading of `⨆ i, A i`, and the
 mapping `⨁ i, A i →+ ⨆ i, A i` can be obtained as
 `direct_sum.to_monoid (λ i, add_submonoid.inclusion $ le_supr A i)`.
 
@@ -42,7 +41,7 @@ internally graded ring
 
 open_locale direct_sum big_operators
 
-variables {ι : Type*} {S R : Type*}
+variables {ι : Type*} {σ S R : Type*}
 
 lemma set_like.has_graded_one.algebra_map_mem [has_zero ι]
   [comm_semiring S] [semiring R] [algebra S R]
@@ -55,118 +54,71 @@ end
 section direct_sum
 variables [decidable_eq ι]
 
-/-! #### From `add_submonoid`s -/
+/-! #### From `add_submonoid`s and `add_subgroup`s -/
 
-namespace add_submonoid
+namespace set_like
 
-/-- Build a `gsemiring` instance for a collection of `add_submonoid`s. -/
-instance gsemiring [add_monoid ι] [semiring R]
-  (A : ι → add_submonoid R) [set_like.graded_monoid A] :
+/-- Build a `gnon_unital_non_assoc_semiring` instance for a collection of additive submonoids. -/
+instance gnon_unital_non_assoc_semiring [has_add ι] [non_unital_non_assoc_semiring R]
+  [set_like σ R] [add_submonoid_class σ R]
+  (A : ι → σ) [set_like.has_graded_mul A] :
+  direct_sum.gnon_unital_non_assoc_semiring (λ i, A i) :=
+{ mul_zero := λ i j _, subtype.ext (mul_zero _),
+  zero_mul := λ i j _, subtype.ext (zero_mul _),
+  mul_add := λ i j _ _ _, subtype.ext (mul_add _ _ _),
+  add_mul := λ i j _ _ _, subtype.ext (add_mul _ _ _),
+  ..set_like.ghas_mul A }
+
+/-- Build a `gsemiring` instance for a collection of additive submonoids. -/
+instance gsemiring [add_monoid ι] [semiring R] [set_like σ R] [add_submonoid_class σ R]
+  (A : ι → σ) [set_like.graded_monoid A] :
   direct_sum.gsemiring (λ i, A i) :=
 { mul_zero := λ i j _, subtype.ext (mul_zero _),
   zero_mul := λ i j _, subtype.ext (zero_mul _),
   mul_add := λ i j _ _ _, subtype.ext (mul_add _ _ _),
   add_mul := λ i j _ _ _, subtype.ext (add_mul _ _ _),
   ..set_like.gmonoid A }
 
-/-- Build a `gcomm_semiring` instance for a collection of `add_submonoid`s. -/
-instance gcomm_semiring [add_comm_monoid ι] [comm_semiring R]
-  (A : ι → add_submonoid R) [set_like.graded_monoid A] :
+/-- Build a `gcomm_semiring` instance for a collection of additive submonoids. -/
+instance gcomm_semiring [add_comm_monoid ι] [comm_semiring R] [set_like σ R]
+  [add_submonoid_class σ R] (A : ι → σ) [set_like.graded_monoid A] :
   direct_sum.gcomm_semiring (λ i, A i) :=
 { ..set_like.gcomm_monoid A,
-  ..add_submonoid.gsemiring A, }
+  ..set_like.gsemiring A, }
 
-end add_submonoid
+end set_like
 
 /-- The canonical ring isomorphism between `⨁ i, A i` and `R`-/
-def direct_sum.submonoid_coe_ring_hom [add_monoid ι] [semiring R]
-  (A : ι → add_submonoid R) [h : set_like.graded_monoid A] : (⨁ i, A i) →+* R :=
-direct_sum.to_semiring (λ i, (A i).subtype) rfl (λ _ _ _ _, rfl)
+def direct_sum.coe_ring_hom [add_monoid ι] [semiring R] [set_like σ R]
+  [add_submonoid_class σ R] (A : ι → σ) [set_like.graded_monoid A] : (⨁ i, A i) →+* R :=
+direct_sum.to_semiring (λ i, add_submonoid_class.subtype (A i)) rfl (λ _ _ _ _, rfl)
 
 /-- The canonical ring isomorphism between `⨁ i, A i` and `R`-/
-@[simp] lemma direct_sum.submonoid_coe_ring_hom_of [add_monoid ι] [semiring R]
-  (A : ι → add_submonoid R) [h : set_like.graded_monoid A] (i : ι) (x : A i) :
-  direct_sum.submonoid_coe_ring_hom A (direct_sum.of (λ i, A i) i x) = x :=
+@[simp] lemma direct_sum.coe_ring_hom_of [add_monoid ι] [semiring R]
+  (A : ι → add_submonoid R) [set_like.graded_monoid A] (i : ι) (x : A i) :
+  direct_sum.coe_ring_hom A (direct_sum.of (λ i, A i) i x) = x :=
 direct_sum.to_semiring_of _ _ _ _ _
 
-lemma direct_sum.coe_mul_apply_add_submonoid [add_monoid ι] [semiring R]
-  (A : ι → add_submonoid R) [set_like.graded_monoid A]
+lemma direct_sum.coe_mul_apply [add_monoid ι] [semiring R] [set_like σ R]
+  [add_submonoid_class σ R] (A : ι → σ) [set_like.graded_monoid A]
   [Π (i : ι) (x : A i), decidable (x ≠ 0)] (r r' : ⨁ i, A i) (i : ι) :
   ((r * r') i : R) =
     ∑ ij in finset.filter (λ ij : ι × ι, ij.1 + ij.2 = i) (r.support.product r'.support),
       r ij.1 * r' ij.2 :=
 begin
   rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply,
     add_submonoid_class.coe_finset_sum],
-  simp_rw [direct_sum.coe_of_add_submonoid_apply, ←finset.sum_filter, set_like.coe_ghas_mul],
+  simp_rw [direct_sum.coe_of_apply, ←finset.sum_filter, set_like.coe_ghas_mul],
 end
 
-/-! #### From `add_subgroup`s -/
-
-namespace add_subgroup
-
-/-- Build a `gsemiring` instance for a collection of `add_subgroup`s. -/
-instance gsemiring [add_monoid ι] [ring R]
-  (A : ι → add_subgroup R) [h : set_like.graded_monoid A] :
-  direct_sum.gsemiring (λ i, A i) :=
-have i' : set_like.graded_monoid (λ i, (A i).to_add_submonoid) := {..h},
-by exactI add_submonoid.gsemiring (λ i, (A i).to_add_submonoid)
-
-/-- Build a `gcomm_semiring` instance for a collection of `add_subgroup`s. -/
-instance gcomm_semiring [add_comm_group ι] [comm_ring R]
-  (A : ι → add_subgroup R) [h : set_like.graded_monoid A] :
-  direct_sum.gsemiring (λ i, A i) :=
-have i' : set_like.graded_monoid (λ i, (A i).to_add_submonoid) := {..h},
-by exactI add_submonoid.gsemiring (λ i, (A i).to_add_submonoid)
-
-end add_subgroup
-
-/-- The canonical ring isomorphism between `⨁ i, A i` and `R`. -/
-def direct_sum.subgroup_coe_ring_hom [add_monoid ι] [ring R]
-  (A : ι → add_subgroup R) [set_like.graded_monoid A] : (⨁ i, A i) →+* R :=
-direct_sum.to_semiring (λ i, (A i).subtype) rfl (λ _ _ _ _, rfl)
-
-@[simp] lemma direct_sum.subgroup_coe_ring_hom_of [add_monoid ι] [ring R]
-  (A : ι → add_subgroup R) [set_like.graded_monoid A] (i : ι) (x : A i) :
-  direct_sum.subgroup_coe_ring_hom A (direct_sum.of (λ i, A i) i x) = x :=
-direct_sum.to_semiring_of _ _ _ _ _
-
-lemma direct_sum.coe_mul_apply_add_subgroup [add_monoid ι] [ring R]
-  (A : ι → add_subgroup R) [set_like.graded_monoid A] [Π (i : ι) (x : A i), decidable (x ≠ 0)]
-  (r r' : ⨁ i, A i) (i : ι) :
-  ((r * r') i : R) =
-    ∑ ij in finset.filter (λ ij : ι × ι, ij.1 + ij.2 = i) (r.support.product r'.support),
-      r ij.1 * r' ij.2 :=
-begin
-  rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply,
-    add_submonoid_class.coe_finset_sum],
-  simp_rw [direct_sum.coe_of_add_subgroup_apply, ←finset.sum_filter, set_like.coe_ghas_mul],
-end
-
-/-! #### From `submodules`s -/
+/-! #### From `submodule`s -/
 
 namespace submodule
 
-/-- Build a `gsemiring` instance for a collection of `submodule`s. -/
-instance gsemiring [add_monoid ι]
-  [comm_semiring S] [semiring R] [algebra S R]
-  (A : ι → submodule S R) [h : set_like.graded_monoid A] :
-  direct_sum.gsemiring (λ i, A i) :=
-have i' : set_like.graded_monoid (λ i, (A i).to_add_submonoid) := {..h},
-by exactI add_submonoid.gsemiring (λ i, (A i).to_add_submonoid)
-
-/-- Build a `gsemiring` instance for a collection of `submodule`s. -/
-instance gcomm_semiring [add_comm_monoid ι]
-  [comm_semiring S] [comm_semiring R] [algebra S R]
-  (A : ι → submodule S R) [h : set_like.graded_monoid A] :
-  direct_sum.gcomm_semiring (λ i, A i) :=
-have i' : set_like.graded_monoid (λ i, (A i).to_add_submonoid) := {..h},
-by exactI add_submonoid.gcomm_semiring (λ i, (A i).to_add_submonoid)
-
 /-- Build a `galgebra` instance for a collection of `submodule`s. -/
 instance galgebra [add_monoid ι]
   [comm_semiring S] [semiring R] [algebra S R]
-  (A : ι → submodule S R) [h : set_like.graded_monoid A] :
+  (A : ι → submodule S R) [set_like.graded_monoid A] :
   direct_sum.galgebra S (λ i, A i) :=
 { to_fun := ((algebra.linear_map S R).cod_restrict (A 0) $
     set_like.has_graded_one.algebra_map_mem A).to_add_monoid_hom,
@@ -178,7 +130,7 @@ instance galgebra [add_monoid ι]
 
 @[simp] lemma set_like.coe_galgebra_to_fun [add_monoid ι]
   [comm_semiring S] [semiring R] [algebra S R]
-  (A : ι → submodule S R) [h : set_like.graded_monoid A] (s : S) :
+  (A : ι → submodule S R) [set_like.graded_monoid A] (s : S) :
     ↑(@direct_sum.galgebra.to_fun _ S (λ i, A i) _ _ _ _ _ _ _ s) = (algebra_map S R s : R) := rfl
 
 /-- A direct sum of powers of a submodule of an algebra has a multiplicative structure. -/
@@ -191,36 +143,24 @@ instance nat_power_graded_monoid
 end submodule
 
 /-- The canonical algebra isomorphism between `⨁ i, A i` and `R`. -/
-def direct_sum.submodule_coe_alg_hom [add_monoid ι]
+def direct_sum.coe_alg_hom [add_monoid ι]
   [comm_semiring S] [semiring R] [algebra S R]
-  (A : ι → submodule S R) [h : set_like.graded_monoid A] : (⨁ i, A i) →ₐ[S] R :=
+  (A : ι → submodule S R) [set_like.graded_monoid A] : (⨁ i, A i) →ₐ[S] R :=
 direct_sum.to_algebra S _ (λ i, (A i).subtype) rfl (λ _ _ _ _, rfl) (λ _, rfl)
 
 /-- The supremum of submodules that form a graded monoid is a subalgebra, and equal to the range of
-`direct_sum.submodule_coe_alg_hom`. -/
+`direct_sum.coe_alg_hom`. -/
 lemma submodule.supr_eq_to_submodule_range [add_monoid ι]
   [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [set_like.graded_monoid A] :
-  (⨆ i, A i) = (direct_sum.submodule_coe_alg_hom A).range.to_submodule :=
+  (⨆ i, A i) = (direct_sum.coe_alg_hom A).range.to_submodule :=
 (submodule.supr_eq_range_dfinsupp_lsum A).trans $ set_like.coe_injective rfl
 
-@[simp] lemma direct_sum.submodule_coe_alg_hom_of [add_monoid ι]
+@[simp] lemma direct_sum.coe_alg_hom_of [add_monoid ι]
   [comm_semiring S] [semiring R] [algebra S R]
-  (A : ι → submodule S R) [h : set_like.graded_monoid A] (i : ι) (x : A i) :
-  direct_sum.submodule_coe_alg_hom A (direct_sum.of (λ i, A i) i x) = x :=
+  (A : ι → submodule S R) [set_like.graded_monoid A] (i : ι) (x : A i) :
+  direct_sum.coe_alg_hom A (direct_sum.of (λ i, A i) i x) = x :=
 direct_sum.to_semiring_of _ rfl (λ _ _ _ _, rfl) _ _
 
-lemma direct_sum.coe_mul_apply_submodule [add_monoid ι]
-  [comm_semiring S] [semiring R] [algebra S R]
-  (A : ι → submodule S R) [Π (i : ι) (x : A i), decidable (x ≠ 0)]
-  [set_like.graded_monoid A] (r r' : ⨁ i, A i) (i : ι) :
-  ((r * r') i : R) =
-    ∑ ij in finset.filter (λ ij : ι × ι, ij.1 + ij.2 = i) (r.support.product r'.support),
-      r ij.1 * r' ij.2 :=
-begin
-  rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply, submodule.coe_sum],
-  simp_rw [direct_sum.coe_of_submodule_apply, ←finset.sum_filter, set_like.coe_ghas_mul],
-end
-
 end direct_sum
 
 section homogeneous_element