feat(linear_algebra/direct_sum): submodule_is_internal_iff_independent_and_supr_eq_top (#9214)

This shows that a grade decomposition into submodules is bijective iff and only iff the submodules are independent and span the whole module.

The key proofs are:
* `complete_lattice.independent_of_dfinsupp_lsum_injective`
* `complete_lattice.independent.dfinsupp_lsum_injective`

Everything else is just glue.

This replaces parts of #8246, and uses what is probably a similar proof strategy, but without unfolding down to finsets.

Unlike the proof there, this requires only `add_comm_monoid` for the `complete_lattice.independent_of_dfinsupp_lsum_injective` direction of the proof. I was not able to find a proof of `complete_lattice.independent.dfinsupp_lsum_injective` with the same weak assumptions, as it is not true! A counter-example is included,

Co-authored-by: Hanting Zhang <hantingzhang03@gmail.com>

Author: eric-wieser

counterexamples/direct_sum_is_internal.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser, Kevin Buzzard
+-/
+
+import algebra.direct_sum.module
+import tactic.fin_cases
+
+/-!
+# Not all complementary decompositions of a module over a semiring make up a direct sum
+
+This shows that while `ℤ≤0` and `ℤ≥0` are complementary `ℕ`-submodules of `ℤ`, which in turn
+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
+take `ring R` and not `semiring R`.
+-/
+
+lemma units_int.one_ne_neg_one : (1 : units ℤ) ≠ -1 := dec_trivial
+
+/-- Submodules of positive and negative integers, keyed by sign. -/
+def with_sign (i : units ℤ) : submodule ℕ ℤ :=
+add_submonoid.to_nat_submodule $ show add_submonoid ℤ, from
+  { carrier := {z | 0 ≤ i • z},
+    zero_mem' := show 0 ≤ i • (0 : ℤ), from (smul_zero _).ge,
+    add_mem' := λ x y (hx : 0 ≤ i • x) (hy : 0 ≤ i • y), show _ ≤ _, begin
+      rw smul_add,
+      exact add_nonneg hx hy
+    end }
+
+local notation `ℤ≥0` := with_sign 1
+local notation `ℤ≤0` := with_sign (-1)
+
+lemma mem_with_sign_one {x : ℤ} : x ∈ ℤ≥0 ↔ 0 ≤ x :=
+show _ ≤ _ ↔ _, by rw one_smul
+
+lemma mem_with_sign_neg_one {x : ℤ} : x ∈ ℤ≤0 ↔ x ≤ 0 :=
+show _ ≤ _ ↔ _, by rw [units.neg_smul, le_neg, one_smul, neg_zero]
+
+/-- The two submodules are complements. -/
+lemma with_sign.is_compl : is_compl (ℤ≥0) (ℤ≤0) :=
+begin
+  split,
+  { apply submodule.disjoint_def.2,
+    intros x hx hx',
+    exact le_antisymm (mem_with_sign_neg_one.mp hx') (mem_with_sign_one.mp hx), },
+  { intros x hx,
+    obtain hp | hn := (le_refl (0 : ℤ)).le_or_le x,
+    exact submodule.mem_sup_left (mem_with_sign_one.mpr hp),
+    exact submodule.mem_sup_right (mem_with_sign_neg_one.mpr hn), }
+end
+
+def with_sign.independent : complete_lattice.independent with_sign :=
+begin
+  intros i,
+  rw [←finset.sup_univ_eq_supr, units_int.univ, finset.sup_insert, finset.sup_singleton],
+  fin_cases i,
+  { convert with_sign.is_compl.disjoint,
+    convert bot_sup_eq,
+    { exact supr_neg (not_not_intro rfl), },
+    { rw supr_pos units_int.one_ne_neg_one.symm } },
+  { convert with_sign.is_compl.disjoint.symm,
+    convert sup_bot_eq,
+    { exact supr_neg (not_not_intro rfl), },
+    { rw supr_pos units_int.one_ne_neg_one } },
+end
+
+lemma with_sign.supr : supr with_sign = ⊤ :=
+begin
+  rw [←finset.sup_univ_eq_supr, units_int.univ, finset.sup_insert, finset.sup_singleton],
+  exact with_sign.is_compl.sup_eq_top,
+end
+
+/-- But there is no embedding into `ℤ` from the direct sum. -/
+lemma with_sign.not_injective :
+  ¬function.injective (direct_sum.to_module ℕ (units ℤ) ℤ (λ i, (with_sign i).subtype)) :=
+begin
+  intro hinj,
+  let p1 : ℤ≥0 := ⟨1, mem_with_sign_one.2 zero_le_one⟩,
+  let n1 : ℤ≤0 := ⟨-1, mem_with_sign_neg_one.2 $ neg_nonpos.2 zero_le_one⟩,
+  let z := direct_sum.lof ℕ _ (λ i, with_sign i) 1 p1 +
+           direct_sum.lof ℕ _ (λ i, with_sign i) (-1) n1,
+  have : z ≠ 0,
+  { intro h,
+    dsimp [z, direct_sum.lof_eq_of, direct_sum.of] at h,
+    replace h := dfinsupp.ext_iff.mp h 1,
+    rw [dfinsupp.zero_apply, dfinsupp.add_apply, dfinsupp.single_eq_same,
+      dfinsupp.single_eq_of_ne (units_int.one_ne_neg_one.symm), add_zero, subtype.ext_iff,
+      submodule.coe_zero] at h,
+    apply zero_ne_one h.symm, },
+  apply hinj.ne this,
+  rw [linear_map.map_zero, linear_map.map_add, direct_sum.to_module_lof, direct_sum.to_module_lof],
+  simp,
+end
+
+/-- And so they do not represent an internal direct sum. -/
+lemma with_sign.not_internal : ¬direct_sum.submodule_is_internal with_sign :=
+with_sign.not_injective ∘ and.elim_left

src/algebra/direct_sum/module.lean

@@ -162,7 +162,10 @@ lemma component.of (i j : ι) (b : M j) :
 dfinsupp.single_apply
 
 /-- 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. -/
+canonical map `(⨁ i, A i) →ₗ[R] M` is bijective.
+
+For the alternate statement in terms of independence and spanning, see
+`direct_sum.submodule_is_internal_iff_independent_and_supr_eq_top`. -/
 def submodule_is_internal {R M : Type*}
   [semiring R] [add_comm_monoid M] [module R M]
   (A : ι → submodule R M) : Prop :=
@@ -178,12 +181,36 @@ 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
 
+/-- If a direct sum of submodules is internal then the submodules span the module. -/
 lemma submodule_is_internal.supr_eq_top {R M : Type*}
-  [semiring R] [add_comm_monoid M] [module R M] (A : ι → submodule R M)
+  [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
 
+/-- If a direct sum of submodules is internal then the submodules are independent. -/
+lemma submodule_is_internal.independent {R M : Type*}
+  [semiring R] [add_comm_monoid M] [module R M] {A : ι → submodule R M}
+  (h : submodule_is_internal A) : complete_lattice.independent A :=
+complete_lattice.independent_of_dfinsupp_lsum_injective _ h.injective
+
+/-- Note that this is not generally true for `[semiring R]`; see
+`complete_lattice.independent.dfinsupp_lsum_injective` for details. -/
+lemma submodule_is_internal_of_independent_of_supr_eq_top {R M : Type*}
+  [ring R] [add_comm_group M] [module R M] {A : ι → submodule R M}
+  (hi : complete_lattice.independent A) (hs : supr A = ⊤) : submodule_is_internal A :=
+⟨hi.dfinsupp_lsum_injective, linear_map.range_eq_top.1 $
+  (submodule.supr_eq_range_dfinsupp_lsum _).symm.trans hs⟩
+
+/-- `iff` version of `direct_sum.submodule_is_internal_of_independent_of_supr_eq_top`,
+`direct_sum.submodule_is_internal.independent`, and `direct_sum.submodule_is_internal.supr_eq_top`.
+-/
+lemma submodule_is_internal_iff_independent_and_supr_eq_top {R M : Type*}
+  [ring R] [add_comm_group M] [module R M] (A : ι → submodule R M) :
+    submodule_is_internal A ↔ complete_lattice.independent A ∧ supr A = ⊤ :=
+⟨λ i, ⟨i.independent, i.supr_eq_top⟩,
+ and.rec submodule_is_internal_of_independent_of_supr_eq_top⟩
+
 end direct_sum

src/linear_algebra/dfinsupp.lean

@@ -128,6 +128,13 @@ def lsum [semiring S] [module S N] [smul_comm_class R S N] :
   map_add' := λ F G, by { ext x y, simp },
   map_smul' := λ c F, by { ext, simp } }
 
+/-- While `simp` can prove this, it is often convenient to avoid unfolding `lsum` into `sum_add_hom`
+with `dfinsupp.lsum_apply_apply`. -/
+lemma lsum_single [semiring S] [module S N] [smul_comm_class R S N]
+  (F : Π i, M i →ₗ[R] N) (i) (x : M i) :
+  lsum S F (single i x) = F i x :=
+sum_add_hom_single _ _ _
+
 end lsum
 
 /-! ### Bundled versions of `dfinsupp.map_range`
@@ -277,3 +284,79 @@ lemma mem_bsupr_iff_exists_dfinsupp (p : ι → Prop) [decidable_pred p] (S : ι
 set_like.ext_iff.mp (bsupr_eq_range_dfinsupp_lsum p S) x
 
 end submodule
+
+namespace complete_lattice
+
+open dfinsupp
+
+/-- Independence of a family of submodules can be expressed as a quantifier over `dfinsupp`s.
+
+This is an intermediate result used to prove
+`complete_lattice.independent_of_dfinsupp_lsum_injective` and
+`complete_lattice.independent.dfinsupp_lsum_injective`. -/
+lemma independent_iff_forall_dfinsupp {R M : Type*}
+  [semiring R] [add_comm_monoid M] [module R M] (p : ι → submodule R M) :
+  independent p ↔
+    ∀ i (x : p i) (v : Π₀ (i : ι), ↥(p i)), lsum ℕ (λ i, (p i).subtype) (erase i v) = x → x = 0 :=
+begin
+  simp_rw [complete_lattice.independent_def, submodule.disjoint_def,
+    submodule.mem_bsupr_iff_exists_dfinsupp, exists_imp_distrib, filter_ne_eq_erase],
+  apply forall_congr (λ i, _),
+  refine subtype.forall'.trans _,
+  simp_rw submodule.coe_eq_zero,
+  refl,
+end
+
+/- If `dfinsupp.lsum` applied with `submodule.subtype` is injective then the submodules are
+independent. -/
+lemma independent_of_dfinsupp_lsum_injective {R M : Type*}
+  [semiring R] [add_comm_monoid M] [module R M] (p : ι → submodule R M)
+  (h : function.injective (lsum ℕ (λ i, (p i).subtype))) :
+  independent p :=
+begin
+  rw independent_iff_forall_dfinsupp,
+  intros i x v hv,
+  replace hv : lsum ℕ (λ i, (p i).subtype) (erase i v) = lsum ℕ (λ i, (p i).subtype) (single i x),
+  { simpa only [lsum_single] using hv, },
+  have := dfinsupp.ext_iff.mp (h hv) i,
+  simpa [eq_comm] using this,
+end
+
+/-- The canonical map out of a direct sum of a family of submodules is injective when the submodules
+are `complete_lattice.independent`.
+
+Note that this is not generally true for `[semiring R]`, for instance when `A` is the
+`ℕ`-submodules of the positive and negative integers.
+
+See `counterexamples/direct_sum_is_internal.lean` for a proof of this fact. -/
+lemma independent.dfinsupp_lsum_injective {R M : Type*}
+  [ring R] [add_comm_group M] [module R M] {p : ι → submodule R M}
+  (h : independent p) : function.injective (lsum ℕ (λ i, (p i).subtype)) :=
+begin
+  -- simplify everything down to binders over equalities in `M`
+  rw independent_iff_forall_dfinsupp at h,
+  suffices : (lsum ℕ (λ i, (p i).subtype)).ker = ⊥,
+  { -- Lean can't find this without our help
+    letI : add_comm_group (Π₀ i, p i) := @dfinsupp.add_comm_group _ (λ i, p i) _,
+    rw linear_map.ker_eq_bot at this, exact this },
+  rw linear_map.ker_eq_bot',
+  intros m hm,
+  ext i : 1,
+  -- split `m` into the piece at `i` and the pieces elsewhere, to match `h`
+  rw [dfinsupp.zero_apply, ←neg_eq_zero],
+  refine h i (-m i) m _,
+  rwa [←erase_add_single i m, linear_map.map_add, lsum_single, submodule.subtype_apply,
+    add_eq_zero_iff_eq_neg, ←submodule.coe_neg] at hm,
+end
+
+/-- A family of submodules over an additive group are independent if and only iff `dfinsupp.lsum`
+applied with `submodule.subtype` is injective.
+
+Note that this is not generally true for `[semiring R]`; see
+`complete_lattice.independent.dfinsupp_lsum_injective` for details. -/
+lemma independent_iff_dfinsupp_lsum_injective {R M : Type*}
+  [ring R] [add_comm_group M] [module R M] (p : ι → submodule R M) :
+  independent p ↔ function.injective (lsum ℕ (λ i, (p i).subtype)) :=
+⟨independent.dfinsupp_lsum_injective, independent_of_dfinsupp_lsum_injective p⟩
+
+end complete_lattice