feat(algebra/direct_sum/module) : coe and internal (#10004)

This extracts the following `def`s from within the various `is_internal` properties:
* `direct_sum.add_submonoid_coe`
* `direct_sum.add_subgroup_coe`
* `direct_sum.submodule_coe`

Packing these into a def makes things more concise, and avoids some annoying elaboration issues.

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>



Co-authored-by: jjaassoonn <jujian.zhang1998@out.com>

src/algebra/direct_sum/basic.lean

@@ -191,13 +191,24 @@ protected def id (M : Type v) (ι : Type* := punit) [add_comm_monoid M] [unique
   right_inv := λ x, to_add_monoid_of _ _ _,
   ..direct_sum.to_add_monoid (λ _, add_monoid_hom.id M) }
 
+/-- 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 :=
+to_add_monoid_of _ _ _
+
 /-- 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.
 
 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 (direct_sum.to_add_monoid (λ i, (A i).subtype) : (⨁ i, A i) →+ M)
+function.bijective (add_submonoid_coe A)
 
 lemma add_submonoid_is_internal.supr_eq_top {M : Type*} [decidable_eq ι] [add_comm_monoid M]
   (A : ι → add_submonoid M)
@@ -207,13 +218,24 @@ begin
   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 _ _ _
+
 /-- 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 (direct_sum.to_add_monoid (λ i, (A i).subtype) : (⨁ i, A i) →+ M)
+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) :

src/algebra/direct_sum/module.lean

@@ -194,6 +194,18 @@ lemma component.of (i j : ι) (b : M j) :
   if h : j = i then eq.rec_on h b else 0 :=
 dfinsupp.single_apply
 
+/-- The canonical embedding from `⨁ i, A i` to `M`  where `A` is a collection of `submodule R M`
+indexed by `ι`-/
+def submodule_coe {R M : Type*} [semiring R] [add_comm_monoid M] [module R M]
+  (A : ι → submodule R M) : (⨁ i, A i) →ₗ[R] M :=
+to_module R ι M (λ i, (A i).subtype)
+
+@[simp] lemma submodule_coe_of {R M : Type*} [semiring R] [add_comm_monoid M] [module R M]
+  (A : ι → submodule R M) (i : ι) (x : A i) :
+  submodule_coe A (of (λ i, A i) i x) = x :=
+to_add_monoid_of _ _ _
+
+
 /-- The `direct_sum` formed by a collection of `submodule`s of `M` is said to be internal if the
 canonical map `(⨁ i, A i) →ₗ[R] M` is bijective.
 
@@ -202,7 +214,7 @@ For the alternate statement in terms of independence and spanning, see
 def submodule_is_internal {R M : Type*}
   [semiring R] [add_comm_monoid M] [module R M]
   (A : ι → submodule R M) : Prop :=
-function.bijective (to_module R ι M (λ i, (A i).subtype))
+function.bijective (submodule_coe A)
 
 lemma submodule_is_internal.to_add_submonoid {R M : Type*}
   [semiring R] [add_comm_monoid M] [module R M] (A : ι → submodule R M) :