From b091c3fb2865d3df62e28790fb80fcaf823063a8 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 13 Jul 2021 17:32:47 +0000
Subject: [PATCH] =?UTF-8?q?feat(algebra/direct=5Fsum):=20the=20submodules?=
 =?UTF-8?q?=20of=20an=20internal=20direct=20sum=20satisfy=20`supr=20A=20?=
 =?UTF-8?q?=3D=20=E2=8A=A4`=20(#8274)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The main results here are:

* `direct_sum.add_submonoid_is_internal.supr_eq_top`
* `direct_sum.submodule_is_internal.supr_eq_top`

Which we prove using the new lemmas

* `add_submonoid.supr_eq_mrange_dfinsupp_sum_add_hom`
* `submodule.supr_eq_range_dfinsupp_lsum`

There's no obvious way to reuse the proofs between the two, but thankfully all four proofs are quite short anyway.

These should aid in shortening #8246.
---
 src/algebra/direct_sum.lean               |  8 +++++
 src/data/dfinsupp.lean                    | 29 ++++++++++++++++++
 src/linear_algebra/dfinsupp.lean          | 36 +++++++++++++++++++++--
 src/linear_algebra/direct_sum_module.lean |  8 +++++
 4 files changed, 79 insertions(+), 2 deletions(-)

diff --git a/src/algebra/direct_sum.lean b/src/algebra/direct_sum.lean
index ad09fcdcd1d16..40561e1af3d38 100644
--- a/src/algebra/direct_sum.lean
+++ b/src/algebra/direct_sum.lean
@@ -178,6 +178,14 @@ 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)
 
+lemma add_submonoid_is_internal.supr_eq_top {M : Type*} [decidable_eq ι] [add_comm_monoid M]
+  (A : ι → add_submonoid M)
+  (h : add_submonoid_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 `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.
 
diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean
index 825b4905d8290..c6620a35eb14c 100644
--- a/src/data/dfinsupp.lean
+++ b/src/data/dfinsupp.lean
@@ -958,6 +958,35 @@ begin
   exact h
 end
 
+/-- The supremum of a family of commutative additive submonoids is equal to the range of
+`finsupp.sum_add_hom`; that is, every element in the `supr` can be produced from taking a finite
+number of non-zero elements of `p i`, coercing them to `γ`, and summing them. -/
+lemma _root_.add_submonoid.supr_eq_mrange_dfinsupp_sum_add_hom [add_comm_monoid γ]
+  (p : ι → add_submonoid γ) : supr p = (dfinsupp.sum_add_hom (λ i, (p i).subtype)).mrange :=
+begin
+  apply le_antisymm,
+  { apply supr_le _,
+    intros i y hy,
+    exact ⟨dfinsupp.single i ⟨y, hy⟩, dfinsupp.sum_add_hom_single _ _ _⟩, },
+  { rintros x ⟨v, rfl⟩,
+    exact add_submonoid.dfinsupp_sum_add_hom_mem _ v _ (λ i _, (le_supr p i : p i ≤ _) (v i).prop) }
+end
+
+lemma _root_.add_submonoid.mem_supr_iff_exists_dfinsupp [add_comm_monoid γ]
+  (p : ι → add_submonoid γ) (x : γ) :
+  x ∈ supr p ↔ ∃ f : Π₀ i, p i, dfinsupp.sum_add_hom (λ i, (p i).subtype) f = x :=
+set_like.ext_iff.mp (add_submonoid.supr_eq_mrange_dfinsupp_sum_add_hom p) x
+
+/-- A variant of `add_submonoid.mem_supr_iff_exists_dfinsupp` with the RHS fully unfolded. -/
+lemma _root_.add_submonoid.mem_supr_iff_exists_dfinsupp' [add_comm_monoid γ]
+  (p : ι → add_submonoid γ) [Π i (x : p i), decidable (x ≠ 0)] (x : γ) :
+  x ∈ supr p ↔ ∃ f : Π₀ i, p i, f.sum (λ i xi, ↑xi) = x :=
+begin
+  rw add_submonoid.mem_supr_iff_exists_dfinsupp,
+  simp_rw sum_add_hom_apply,
+  congr',
+end
+
 omit dec
 lemma sum_add_hom_comm {ι₁ ι₂ : Sort*} {β₁ : ι₁ → Type*} {β₂ : ι₂ → Type*} {γ : Type*}
   [decidable_eq ι₁] [decidable_eq ι₂] [Π i, add_zero_class (β₁ i)] [Π i, add_zero_class (β₂ i)]
diff --git a/src/linear_algebra/dfinsupp.lean b/src/linear_algebra/dfinsupp.lean
index 035ae26793206..48ce2a24b7d2d 100644
--- a/src/linear_algebra/dfinsupp.lean
+++ b/src/linear_algebra/dfinsupp.lean
@@ -205,12 +205,44 @@ end dfinsupp
 
 include dec_ι
 
-lemma submodule.dfinsupp_sum_mem {β : ι → Type*} [Π i, has_zero (β i)]
+namespace submodule
+
+lemma dfinsupp_sum_mem {β : ι → Type*} [Π i, has_zero (β i)]
   [Π i (x : β i), decidable (x ≠ 0)] (S : submodule R N)
   (f : Π₀ i, β i) (g : Π i, β i → N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S :=
 S.to_add_submonoid.dfinsupp_sum_mem f g h
 
-lemma submodule.dfinsupp_sum_add_hom_mem {β : ι → Type*} [Π i, add_zero_class (β i)]
+lemma dfinsupp_sum_add_hom_mem {β : ι → Type*} [Π i, add_zero_class (β i)]
   (S : submodule R N) (f : Π₀ i, β i) (g : Π i, β i →+ N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) :
   dfinsupp.sum_add_hom g f ∈ S :=
 S.to_add_submonoid.dfinsupp_sum_add_hom_mem f g h
+
+/-- The supremum of a family of submodules is equal to the range of `dfinsupp.lsum`; that is
+every element in the `supr` can be produced from taking a finite number of non-zero elements
+of `p i`, coercing them to `N`, and summing them. -/
+lemma supr_eq_range_dfinsupp_lsum (p : ι → submodule R N) :
+  supr p = (dfinsupp.lsum ℕ (λ i, (p i).subtype)).range :=
+begin
+  apply le_antisymm,
+  { apply supr_le _,
+    intros i y hy,
+    exact ⟨dfinsupp.single i ⟨y, hy⟩, dfinsupp.sum_add_hom_single _ _ _⟩, },
+  { rintros x ⟨v, rfl⟩,
+    exact dfinsupp_sum_add_hom_mem _ v _ (λ i _, (le_supr p i : p i ≤ _) (v i).prop) }
+end
+
+lemma mem_supr_iff_exists_dfinsupp (p : ι → submodule R N) (x : N) :
+  x ∈ supr p ↔ ∃ f : Π₀ i, p i, dfinsupp.lsum ℕ (λ i, (p i).subtype) f = x :=
+set_like.ext_iff.mp (supr_eq_range_dfinsupp_lsum p) x
+
+/-- A variant of `submodule.mem_supr_iff_exists_dfinsupp` with the RHS fully unfolded. -/
+lemma mem_supr_iff_exists_dfinsupp' (p : ι → submodule R N) [Π i (x : p i), decidable (x ≠ 0)]
+  (x : N) :
+  x ∈ supr p ↔ ∃ f : Π₀ i, p i, f.sum (λ i xi, ↑xi) = x :=
+begin
+  rw mem_supr_iff_exists_dfinsupp,
+  simp_rw [dfinsupp.lsum_apply_apply, dfinsupp.sum_add_hom_apply],
+  congr',
+end
+
+end submodule
diff --git a/src/linear_algebra/direct_sum_module.lean b/src/linear_algebra/direct_sum_module.lean
index aeb978a039a40..dc0e040156d1a 100644
--- a/src/linear_algebra/direct_sum_module.lean
+++ b/src/linear_algebra/direct_sum_module.lean
@@ -167,4 +167,12 @@ lemma submodule_is_internal.to_add_subgroup {R M : Type*}
   submodule_is_internal A ↔ add_subgroup_is_internal (λ i, (A i).to_add_subgroup) :=
 iff.rfl
 
+lemma submodule_is_internal.supr_eq_top {R M : Type*}
+  [semiring R] [add_comm_monoid M] [module R M] (A : ι → submodule R M)
+  (h : submodule_is_internal A) : supr A = ⊤ :=
+begin
+  rw [submodule.supr_eq_range_dfinsupp_lsum, linear_map.range_eq_top],
+  exact function.bijective.surjective h,
+end
+
 end direct_sum