From 85fe90e9cd37cfc9a9233753b55efd41313e02f7 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 1 Nov 2021 07:01:57 +0000 Subject: [PATCH] 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 Co-authored-by: jjaassoonn --- src/algebra/direct_sum/basic.lean | 26 ++++++++++++++++++++++++-- src/algebra/direct_sum/module.lean | 14 +++++++++++++- 2 files changed, 37 insertions(+), 3 deletions(-) diff --git a/src/algebra/direct_sum/basic.lean b/src/algebra/direct_sum/basic.lean index a1e312c3ff0e3..da4963a7dee91 100644 --- a/src/algebra/direct_sum/basic.lean +++ b/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) : diff --git a/src/algebra/direct_sum/module.lean b/src/algebra/direct_sum/module.lean index dc76dae379fcb..4786ed9ea4f59 100644 --- a/src/algebra/direct_sum/module.lean +++ b/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) :