feat(algebra/direct_sum): the submodules of an internal direct sum satisfy supr A = ⊤ (#8274)

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.

Author: eric-wieser

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.
 

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)]

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

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