feat(linear_algebra/decomposition): Define module decompositions and prove basic facts by winston-h-zhang · Pull Request #8246 · leanprover-community/mathlib3

winston-h-zhang · 2021-07-10T02:54:42Z

We define a new structure decomposition ι R M as the type of ι-indexed decompositions of M. We provide a correspondence between internal direct sums and decompositions. Some helpful auxiliary lemmas have been added as well.

Suggestions or criticisms about how I could do this better is certainly welcome!

depends on: [Merged by Bors] - feat(algebra/direct_sum): the submodules of an internal direct sum satisfy supr A = ⊤ #8274
depends on: [Merged by Bors] - feat(order/compactly_generated): For any b, there exists a set of independent atoms s such that Sup s is the complement of b. #8475

src/algebra/module/submodule.lean

src/data/dfinsupp.lean

src/data/finsupp/basic.lean

src/data/fintype/basic.lean

eric-wieser · 2021-07-10T07:16:45Z

src/linear_algebra/decomposition.lean

+
+open_locale direct_sum classical big_operators
+open classical linear_map dfinsupp direct_sum
+noncomputable theory


I'd be interested to know exactly which bits of this are noncomputable.

My hunch right now is that this is not a good choice of definition of decomposition; I think the decomposition should just hold the actual equiv, and you should have a noncomputablr def decomposition.of_independent that constructs one from the fields you currently have.

Are there code/formalization specific benefits to holding to actual equiv? I'm not attached to my definition; they all look equivalent to me.

def decomposition (ι : Type u) (R : Type v) (M : Type w) [semiring R] [add_comm_monoid M] [module R M] := subtype (λ (p : ι → submodule R M), submodule_is_internal p) structure decomposition' (ι : Type u) (R : Type v) (M : Type w) [semiring R] [add_comm_monoid M] [module R M] := (factors : ι → submodule R M) (to_equiv : (⨁ i, factors i) ≃ₗ[R] M)

These were the two other definitions I was thinking about, but they honestly look exactly the same :P

To be clear by "hold the actual equiv" I assume you mean something like the second one?

Yes, although I guess you don't want to hold the equiv, rather just the inverse and the proof it is an inverse of the function we care about.

The advantage of doing that is you can compute with decompositions.

I can reply with a mwe on Monday, but can't really do so from mobile.

src/order/complete_lattice.lean

eric-wieser

Thanks for taking this on! 🎉

eric-wieser · 2021-07-11T16:52:32Z

src/linear_algebra/basic.lean

+-- pretty atrocious but hey it works
+lemma mem_supr'
+  {ι : Type w} (p : ι → submodule R M) {x : M} :
+  x ∈ supr p ↔ ∃ v : ι →₀ M, (∀ i, v i ∈ p i) ∧ ∑ i in v.support, v i = x :=
+begin
+  classical,
+  rw submodule.supr_eq_span,
+  refine ⟨λ h, _, λ h, _⟩,
+  refine submodule.span_induction h _ _ _ _,
+  { intros y hy,
+    rw set.mem_Union at hy,
+    cases hy with i hy,
+    use finsupp.single i y,
+    split,
+    { intro j, by_cases h : j = i,
+      simp only [h, finsupp.single_eq_same], exact hy,
+      rw ← ne.def at h,
+      simp only [finsupp.single_eq_of_ne h.symm, submodule.zero_mem], },
+    by_cases hy : y = 0, rw hy,
+    simp only [finsupp.coe_zero, pi.zero_apply, finsupp.single_zero, finset.sum_const_zero],
+    rw [finsupp.support_single_ne_zero hy, finset.sum_singleton],
+    exact finsupp.single_eq_same, },
+  { use 0,
+    simp only [finsupp.coe_zero, pi.zero_apply, implies_true_iff, eq_self_iff_true, and_self,
+      finset.sum_const_zero, submodule.zero_mem], },
+  { intros x y hx hy,
+    rcases hx with ⟨v, hv, hvs⟩,
+    rcases hy with ⟨w, hw, hws⟩,
+    use v + w,
+    refine ⟨λ i, submodule.add_mem _ (hv i) (hw i), _⟩,
+    rw [← hvs, ← hws],
+    simp only [finsupp.add_apply],
+    convert finsupp.sum_add_add v w, },
+  { intros r x hx,
+    rcases hx with ⟨v, hv, hvs⟩,
+    use r • v,
+    refine ⟨λ i, submodule.smul_mem _ _ (hv i), _⟩,
+    rw [← hvs, finset.smul_sum],
+    simp only [finsupp.smul_apply],
+    refine finset.sum_subset finsupp.support_smul
+      (λ a ha han, finsupp.not_mem_support_iff.mp han) },
+  rcases h with ⟨v, hv, hvs⟩,
+  have := submodule.sum_mem (supr p) (λ i _, (le_supr p i : p i ≤ supr p) (hv i)),
+  rw ← submodule.supr_eq_span,
+  rwa hvs at this,
+end
+
+-- this is **definitely** going to be atrocious
+lemma mem_bsupr {p : ι → Prop} (f : ι → submodule R M) (x : M) :
+  x ∈ (⨆ i (H : p i), f i) ↔
+  ∃ v : ι →₀ M, (∀ i, v i ∈ f i) ∧ ∑ i in v.support, v i = x ∧ (∀ i, ¬ p i → v i = 0) :=
+begin
+  classical,
+  change set ι at p,
+  refine ⟨λ h, _, λ h, _⟩,
+  { rw bsupr_eq_supr at h,
+    rcases (mem_supr' _).mp h with ⟨v', hv', hsum⟩,
+    change p →₀ M at v',
+    -- define `v = v'` where `p i` is true and zero otherwise
+    let v : ι →₀ M :=
+      ⟨v'.support.map (function.embedding.subtype p),
+       λ (i : ι), dite (p i) (λ hi, v' ⟨i, hi⟩) (λ _, 0), _⟩,
+    refine ⟨v, _, _, _⟩,
+    { intros i,
+      simp only [finsupp.coe_mk],
+      split_ifs with hi,
+      { exact hv' ⟨i, hi⟩ },
+      exact zero_mem _ },
+    { simp only [finsupp.coe_mk, dite_eq_ite, function.embedding.coe_subtype, finset.sum_map,
+        subtype.coe_eta],
+      convert hsum,
+      ext i, split_ifs with hi, refl,
+      exfalso, apply hi, exact i.2 },
+    { intros i hi,
+      simp only [finsupp.coe_mk, dif_neg hi], },
+    intros i,
+    simp only [exists_prop, function.embedding.coe_subtype, set_coe.exists, finset.mem_map,
+      exists_and_distrib_right, exists_eq_right, finsupp.mem_support_iff, ne.def, subtype.coe_mk],
+    split_ifs with hi,
+    { refine ⟨λ hh, _, λ hh, ⟨hi, hh⟩⟩,
+      cases hh with _ key, exact key },
+    refine ⟨λ hh _, _, λ hh, _⟩,
+    { cases hh with key _,
+      exact hi key },
+    exfalso, exact hh rfl },
+  rcases h with ⟨v, hv, hsum, hzero⟩,
+  have hle: (⨆ i ∈ v.support, f i) ≤ ⨆ (i : ι) (H : p i), f i,
+  { refine bsupr_le_bsupr' (λ i hi, _),
+    revert hi, contrapose!,
+    refine λ h, finsupp.not_mem_support_iff.mpr (hzero i h), },
+  have key: x ∈ ⨆ i ∈ v.support, f i,
+  { rw ← hsum, exact sum_mem_bsupr (λ i hi, hv i), },
+  exact hle key,
+end
+


I think it might be worth splitting these two proofs (and anything you added in order to prove them) into their own smaller PR, and asking zulip for help golfing them. This PR is great, but it's also large, and if you split it up you can get more focussed feedback on each part.

…ubmodule}.[d]finsupp_sum_mem` These lemmas are trivial consequences of the finset lemmas, but having them avoids having to unfold `[d]finsupp.sum`. `dfinsupp_sum_add_hom_mem` is particularly useful because this one has some messy decidability arguments to eliminate.

eric-wieser · 2021-09-16T13:56:20Z

src/linear_algebra/basic.lean

+-- this is **definitely** going to be atrocious
+lemma mem_bsupr {p : ι → Prop} (f : ι → submodule R M) (x : M) :
+  x ∈ (⨆ i (H : p i), f i) ↔
+  ∃ v : ι →₀ M, (∀ i, v i ∈ f i) ∧ ∑ i in v.support, v i = x ∧ (∀ i, ¬ p i → v i = 0) :=


I've PR'd an alternate version of this as #9202

Also a version for `add_submonoid`. Unfortunately the proofs are almost identical, but that's consistent with the surrounding bits of the file anyway. The key result is a dfinsupp version of the lemma in #8246, ```lean x ∈ (⨆ i (H : p i), f i) ↔ ∃ v : ι →₀ M, (∀ i, v i ∈ f i) ∧ ∑ i in v.support, v i = x ∧ (∀ i, ¬ p i → v i = 0) := ``` as ```lean x ∈ (⨆ i (h : p i), S i) ↔ ∃ f : Π₀ i, S i, dfinsupp.lsum ℕ (λ i, (S i).subtype) (f.filter p) = x ```

…nt_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>

eric-wieser · 2021-10-01T17:38:50Z

@acxxa, I think #9202 contains most of the interesting proofs from this PR; all that's left is the decomposition API.

Did you have a motivation for bundling factors rather than leaving it unbundled? Was there something you planned to build on top of this?

This removes some proofs which now already exist more generally

eric-wieser · 2021-11-03T23:30:36Z

src/linear_algebra/decomposition.lean

+which phased out of the `set` design because of problems with it.
+-/
+@[nolint has_inhabited_instance]
+structure decomposition (ι : Type u) (R : Type v) (M : Type w)


This bears a resemblance to #10115. Both approaches have their merits, but I hope we can get the best of both.

eric-wieser · 2022-01-20T16:03:00Z

Note that graded_algebra is now merged. I think probably to make it play well with this PR, we want to change it's definition from

class graded_algebra extends set_like.graded_monoid 𝒜 :=
(decompose' : A → ⨁ i, 𝒜 i)
(left_inv : function.left_inverse decompose' (direct_sum.submodule_coe 𝒜))
(right_inv : function.right_inverse decompose' (direct_sum.submodule_coe 𝒜))

to

-- this is essentially your `decomposition`
class graded_module :=
(decompose' : A → ⨁ i, 𝒜 i)
(left_inv : function.left_inverse decompose' (direct_sum.submodule_coe 𝒜))
(right_inv : function.right_inverse decompose' (direct_sum.submodule_coe 𝒜))

class graded_algebra extends set_like.graded_monoid 𝒜, graded_module 𝒜

ghost · 2023-04-21T01:15:19Z

This PR/issue depends on:

~~[Merged by Bors] - feat(algebra/direct_sum): the submodules of an internal direct sum satisfy supr A = ⊤ #8274~~
~~[Merged by Bors] - feat(order/compactly_generated): For any b, there exists a set of independent atoms s such that Sup s is the complement of b. #8475~~
By Dependent Issues (🤖). Happy coding!

YaelDillies · 2023-04-22T09:01:38Z

@eric-wieser, what's your opinion on this PR nowadays?

winston-h-zhang added 17 commits July 6, 2021 20:55

initial commit

b0c9be1

fix

f9a78c1

lint

abd95f5

fix

b570ff3

nolint inhabited_instance

d8505f7

add coe_sum

a987aa8

define decompositions

187a719

lint

133054b

lint again

98d48db

equiv between is_internal and decomposition

cd9ec71

port new stuff

d64ff68

lint

f91f973

finish moving stuff

f5b1508

missed a file

844f926

final pass

8605d17

doc-string

1fa6680

move file to linear_algebra

cb018b3