[Merged by Bors] - feat(linear_algebra): submodules of f.g. free modules are free #6178

Vierkantor · 2021-02-11T14:19:51Z

This PR proves the first half of the structure theorem for modules over a PID: if R is a principal ideal domain and M an R-module which is free and finitely generated (expressed by is_basis R (b : ι → M), for a [fintype ι]), then all submodules of M are also free and finitely generated.

This result requires some lemmas about the rank of (free) modules (which in that case is basically the same as fintype.card ι). If M were a vector space, this could just be expressed as findim R M, but it isn't necessarily, so it can't be.

depends on: [Merged by Bors] - feat(algebra/module,linear_algebra): generalize smul_eq_zero #6199

src/data/finsupp/basic.lean

eric-wieser · 2021-02-11T14:36:29Z

src/linear_algebra/free_module.lean

+A free `R`-module `M` is a module with a basis over `R`,
+equivalently it is an `R`-module linearly equivalent to `ι →₀ R` for some `ι`.


Is it worth adding abbreviation free_module := ι →₀ R to this file, just so that people using doc search find it?

I don't think this file actually proves anything for ι →₀ R itself, only indirectly via is_basis. (Spoiler alert: I'm even experimenting with redefining a basis to be the linear equivalence with ι →₀ R.)

Moves the theorem on division rings `smul_eq_zero` to a typeclass `no_zero_smul_divisors` with instances for the previously existing cases. The motivation for this change is that #6178 added another `smul_eq_zero`, which could be captured neatly as an instance of the typeclass. I didn't spend a lot of time yet on figuring out all the necessary instances, first let's see whether this compiles.

Moves the theorem on division rings `smul_eq_zero` to a typeclass `no_zero_smul_divisors` with instances for the previously existing cases. The motivation for this change is that #6178 added another `smul_eq_zero`, which could be captured neatly as an instance of the typeclass. I didn't spend a lot of time yet on figuring out all the necessary instances, first let's see whether this compiles. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Moves the theorem on division rings `smul_eq_zero` to a typeclass `no_zero_smul_divisors` with instances for the previously existing cases. The motivation for this change is that #6178 added another `smul_eq_zero`, which could be captured neatly as an instance of the typeclass. I didn't spend a lot of time yet on figuring out all the necessary instances, first let's see whether this compiles. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

github-actions · 2021-02-22T22:33:16Z

🎉 Great news! Looks like all the dependencies have been resolved:

~~[Merged by Bors] - feat(algebra/module,linear_algebra): generalize smul_eq_zero #6199~~

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

src/linear_algebra/linear_independent.lean

jcommelin · 2021-03-08T16:05:52Z

src/linear_algebra/free_module.lean

+open submodule.is_principal
+
+lemma eq_bot_of_rank_eq_zero [no_zero_divisors R] (hb : is_basis R b) (N : submodule R M)
+  (rank_eq : ∀ {m : ℕ} (v : fin m → N),


Does it make sense to have a similar lemma for fintypes instead of only fin m?

It's a bit awkward because the condition would look like

(rank_eq : ∀ {ι : Type*} {ft : fintype ι} (v : ι → N), linear_independent R (coe ∘ v : ι → M) → @fintype.card ι ft = 0) :

and the counterexample becomes fintype.card (ulift (fin 1)) ≠ 0 instead of just 1 ≠ 0. I'll add a version for finset Ns, let me know if you still want a fintype version.

(Also, using fin works well with the condition of submodule.induction_on_rank_aux. I recall trying to state that with finsets instead and it became a mess of coes, erases and inserts.)

Bah, I can't figure out how to turn sum_eq : ∑ (i : ↥↑{⟨x, hx⟩}), g i • ↑i = 0, into g ⟨⟨x, hx⟩, _⟩ = 0 and it's almost dinner time. Let me know if you still want a different variant, I'll take a fresh look at it tomorrow.

Ooh well, we can always add it later. It's probably useful to have both variants.

src/linear_algebra/free_module.lean

jcommelin

Thanks 🎉

bors merge

This PR proves the first half of the structure theorem for modules over a PID: if `R` is a principal ideal domain and `M` an `R`-module which is free and finitely generated (expressed by `is_basis R (b : ι → M)`, for a `[fintype ι]`), then all submodules of `M` are also free and finitely generated. This result requires some lemmas about the rank of (free) modules (which in that case is basically the same as `fintype.card ι`). If `M` were a vector space, this could just be expressed as `findim R M`, but it isn't necessarily, so it can't be.

bors · 2021-03-08T22:36:45Z

Pull request successfully merged into master.

Build succeeded:

This PR proves the first half of the structure theorem for modules over a PID: if `R` is a principal ideal domain and `M` an `R`-module which is free and finitely generated (expressed by `is_basis R (b : ι → M)`, for a `[fintype ι]`), then all submodules of `M` are also free and finitely generated. This result requires some lemmas about the rank of (free) modules (which in that case is basically the same as `fintype.card ι`). If `M` were a vector space, this could just be expressed as `findim R M`, but it isn't necessarily, so it can't be.

Moves the theorem on division rings `smul_eq_zero` to a typeclass `no_zero_smul_divisors` with instances for the previously existing cases. The motivation for this change is that #6178 added another `smul_eq_zero`, which could be captured neatly as an instance of the typeclass. I didn't spend a lot of time yet on figuring out all the necessary instances, first let's see whether this compiles. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

This PR proves the first half of the structure theorem for modules over a PID: if `R` is a principal ideal domain and `M` an `R`-module which is free and finitely generated (expressed by `is_basis R (b : ι → M)`, for a `[fintype ι]`), then all submodules of `M` are also free and finitely generated. This result requires some lemmas about the rank of (free) modules (which in that case is basically the same as `fintype.card ι`). If `M` were a vector space, this could just be expressed as `findim R M`, but it isn't necessarily, so it can't be.

Vierkantor added the awaiting-review The author would like community review of the PR label Feb 11, 2021

eric-wieser reviewed Feb 11, 2021

View reviewed changes

src/data/finsupp/basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Feb 11, 2021

View reviewed changes

Vierkantor mentioned this pull request Feb 12, 2021

[Merged by Bors] - feat(algebra/module,linear_algebra): generalize smul_eq_zero #6199

Closed

Vierkantor force-pushed the free-module branch from fd41f78 to 93ea342 Compare February 12, 2021 12:47

github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 12, 2021

github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Feb 22, 2021

Vierkantor added 6 commits March 1, 2021 10:59

WIP

e6ff5ff

More WIP: code cleanup

e6f0fad

Finish rewrite, time for cleanup

d6206bc

Improve docstrings

11d1616

Move stuff to the correct files

12a5e89

Fix overlong comment (which was incorrect anyway)

bef8a75

Vierkantor force-pushed the free-module branch from 93ea342 to 2e1312e Compare March 1, 2021 11:31

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 1, 2021

Update to latest mathlib

2e1312e

Vierkantor requested review from urkud and jcommelin March 8, 2021 12:21

jcommelin reviewed Mar 8, 2021

View reviewed changes

Vierkantor added 2 commits March 8, 2021 16:41

Refer back to fin_cons' from fin_cons

1312cdf

sum_fin_succ_above already exists as fin.sum_univ_succ_above

349be9a

jcommelin approved these changes Mar 8, 2021

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Mar 8, 2021

bors bot changed the title ~~feat(linear_algebra): submodules of f.g. free modules are free~~ [Merged by Bors] - feat(linear_algebra): submodules of f.g. free modules are free Mar 8, 2021

bors bot closed this Mar 8, 2021

bors bot deleted the free-module branch March 8, 2021 22:36

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(linear_algebra): submodules of f.g. free modules are free #6178

[Merged by Bors] - feat(linear_algebra): submodules of f.g. free modules are free #6178

Vierkantor commented Feb 11, 2021 •

edited by github-actions bot

Loading

eric-wieser Feb 11, 2021

Vierkantor Feb 11, 2021

github-actions bot commented Feb 22, 2021

jcommelin Mar 8, 2021

Vierkantor Mar 8, 2021

Vierkantor Mar 8, 2021

Vierkantor Mar 8, 2021

jcommelin Mar 8, 2021

jcommelin left a comment

bors bot commented Mar 8, 2021

		A free `R`-module `M` is a module with a basis over `R`,
		equivalently it is an `R`-module linearly equivalent to `ι →₀ R` for some `ι`.

[Merged by Bors] - feat(linear_algebra): submodules of f.g. free modules are free #6178

[Merged by Bors] - feat(linear_algebra): submodules of f.g. free modules are free #6178

Conversation

Vierkantor commented Feb 11, 2021 • edited by github-actions bot Loading

eric-wieser Feb 11, 2021

Choose a reason for hiding this comment

Vierkantor Feb 11, 2021

Choose a reason for hiding this comment

github-actions bot commented Feb 22, 2021

jcommelin Mar 8, 2021

Choose a reason for hiding this comment

Vierkantor Mar 8, 2021

Choose a reason for hiding this comment

Vierkantor Mar 8, 2021

Choose a reason for hiding this comment

Vierkantor Mar 8, 2021

Choose a reason for hiding this comment

jcommelin Mar 8, 2021

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Mar 8, 2021

Vierkantor commented Feb 11, 2021 •

edited by github-actions bot

Loading