[Merged by Bors] - feat(algebra/direct_sum): state what it means for a direct sum to be internal #7190

eric-wieser · 2021-04-14T14:39:51Z

The goal here is primarily to tick off the item in undergrad.yml.

We'll want some theorems relating this statement to independence / spanning of the submodules, but I'll leave those for someone else to follow-up with.

We end up needing three variants of this - one for each of add_submonoids, add_subgroups, and submodules.

…internal

kbuzzard

I need this concept for grading a ring by a module. Modulo the yaml comment this looks good to me.

docs/undergrad.yaml

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

eric-wieser · 2021-04-14T17:01:09Z

src/linear_algebra/direct_sum_module.lean

+/-- 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. -/
+def submodule_is_internal {R M : Type*}
+  [semiring R] [add_comm_monoid M] [semimodule R M]
+  (A : ι → submodule R M) : Prop :=
+function.bijective (to_module R ι M (λ i, (A i).subtype))
+
+lemma submodule_is_internal.to_add_submonoid {R M : Type*}
+  [semiring R] [add_comm_monoid M] [semimodule R M] (A : ι → submodule R M) :
+  submodule_is_internal A ↔ add_submonoid_is_internal (λ i, (A i).to_add_submonoid) :=
+iff.rfl
+
+lemma submodule_is_internal.to_add_subgroup {R M : Type*}
+  [ring R] [add_comm_group M] [semimodule R M] (A : ι → submodule R M) :
+  submodule_is_internal A ↔ add_subgroup_is_internal (λ i, (A i).to_add_subgroup) :=
+iff.rfl


I figure I don't need to mention add_submonoid_is_internal in the docstring of submodule_is_internal, since doc-gen will immediately show the lemmas below it.

adamtopaz

This all looks good to me. I do think it would be worthwhile to add a def for the isomorphism between the (external) direct sum (⨁ i, A i) and the Sup of the family A i (as a subobject of the ambient object), given the is_internal assumption.

(This could be left to a subsequent PR, if you would like.)

eric-wieser · 2021-04-20T10:18:29Z

If we're going to provide isomorphisms, then I'd be inclined to provide a second structure in Type:

structure add_submonoid_grading {M : Type*} [decidable_eq ι] [add_comm_monoid M]
  (A : ι → add_submonoid M) :=
(to_fun : M →+ (⨁ i, A i))
(left_inv : function.left_inverse (direct_sum.to_add_monoid (λ i, (A i).subtype) : (⨁ i, A i) →+ M) to_fun)
(right_inv : function.right_inverse (direct_sum.to_add_monoid (λ i, (A i).subtype) : (⨁ i, A i) →+ M) to_fun)

variables {M : Type*} [decidable_eq ι] [add_comm_monoid M] (A : ι → add_submonoid M) (g : add_submonoid_grading A)

def add_submonoid_grading.to_equiv : M ≃+ (⨁ i, A i) :=
{ to_fun := g.to_fun,
  inv_fun := _,
  left_inv := g.left_inv,
  right_inv := g.right_inv }

lemma add_submonoid_grading.is_internal : add_submonoid_is_internal A := to_equiv.symm.bijective

/-- Noncomputably obtain a grading from a proof that a direct sum is internal, via equiv.of_bijective -/
noncomputable def add_submonoid_is_internal.to_grading (h : add_submonoid_is_internal A) : add_submonoid_grading A :=
{ to_fun := sorry, left_inv := sorry, right_inv := sorry}  -- bijective has the API for this somewhere

But I think we should leave that until we've worked out what the grading structure should look like for rings too.

adamtopaz · 2021-04-22T03:15:24Z

@eric-wieser So do I understand correctly that you prefer to leave the definitions of the isoms to a later PR which will also include the grading code above? If so then that sounds good to me!

bors d+

bors · 2021-04-22T03:15:26Z

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bryangingechen · 2021-04-26T16:03:49Z

@eric-wieser ping?

eric-wieser · 2021-04-26T20:56:47Z

bors r+

…internal (#7190) The goal here is primarily to tick off the item in undergrad.yml. We'll want some theorems relating this statement to independence / spanning of the submodules, but I'll leave those for someone else to follow-up with. We end up needing three variants of this - one for each of add_submonoids, add_subgroups, and submodules.

bors · 2021-04-26T22:02:52Z

Build failed (retrying...):

Build mathlib

…internal (#7190) The goal here is primarily to tick off the item in undergrad.yml. We'll want some theorems relating this statement to independence / spanning of the submodules, but I'll leave those for someone else to follow-up with. We end up needing three variants of this - one for each of add_submonoids, add_subgroups, and submodules.

bors · 2021-04-26T22:18:42Z

Build failed:

Build mathlib

…sum_is_internal

eric-wieser · 2021-04-27T06:09:24Z

bors r+

…internal (#7190) The goal here is primarily to tick off the item in undergrad.yml. We'll want some theorems relating this statement to independence / spanning of the submodules, but I'll leave those for someone else to follow-up with. We end up needing three variants of this - one for each of add_submonoids, add_subgroups, and submodules.

bors · 2021-04-27T11:31:24Z

Pull request successfully merged into master.

Build succeeded:

feat(algebra/direct_sum): state what it means for a direct sum to be …

67fc19e

…internal

eric-wieser added the awaiting-review The author would like community review of the PR label Apr 14, 2021

eric-wieser requested review from urkud and adamtopaz April 14, 2021 14:40

fix

47236ac

kbuzzard reviewed Apr 14, 2021

View reviewed changes

docs/undergrad.yaml Outdated Show resolved Hide resolved

Update docs/undergrad.yaml

de5c85e

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

eric-wieser commented Apr 14, 2021

View reviewed changes

adamtopaz reviewed Apr 20, 2021

View reviewed changes

bryangingechen added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Apr 22, 2021

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Apr 26, 2021

eric-wieser added 2 commits April 26, 2021 23:34

Merge remote-tracking branch 'origin/master' into eric-wieser/direct_…

0a26765

…sum_is_internal

fix

6909344

bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Apr 26, 2021

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-author A reviewer has asked the author a question or requested changes labels Apr 27, 2021

bors bot changed the title ~~feat(algebra/direct_sum): state what it means for a direct sum to be internal~~ [Merged by Bors] - feat(algebra/direct_sum): state what it means for a direct sum to be internal Apr 27, 2021

bors bot closed this Apr 27, 2021

bors bot deleted the eric-wieser/direct_sum_is_internal branch April 27, 2021 11:31

eric-wieser added this to Done in Graded modules, rings, and algebras Aug 31, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(algebra/direct_sum): state what it means for a direct sum to be internal #7190

[Merged by Bors] - feat(algebra/direct_sum): state what it means for a direct sum to be internal #7190

eric-wieser commented Apr 14, 2021

kbuzzard left a comment

eric-wieser Apr 14, 2021 •

edited

Loading

adamtopaz left a comment

eric-wieser commented Apr 20, 2021 •

edited

Loading

adamtopaz commented Apr 22, 2021

bors bot commented Apr 22, 2021

bryangingechen commented Apr 26, 2021

eric-wieser commented Apr 26, 2021

bors bot commented Apr 26, 2021

bors bot commented Apr 26, 2021

eric-wieser commented Apr 27, 2021

bors bot commented Apr 27, 2021

[Merged by Bors] - feat(algebra/direct_sum): state what it means for a direct sum to be internal #7190

[Merged by Bors] - feat(algebra/direct_sum): state what it means for a direct sum to be internal #7190

Conversation

eric-wieser commented Apr 14, 2021

kbuzzard left a comment

Choose a reason for hiding this comment

eric-wieser Apr 14, 2021 • edited Loading

Choose a reason for hiding this comment

adamtopaz left a comment

Choose a reason for hiding this comment

eric-wieser commented Apr 20, 2021 • edited Loading

adamtopaz commented Apr 22, 2021

bors bot commented Apr 22, 2021

bryangingechen commented Apr 26, 2021

eric-wieser commented Apr 26, 2021

bors bot commented Apr 26, 2021

bors bot commented Apr 26, 2021

eric-wieser commented Apr 27, 2021

bors bot commented Apr 27, 2021

eric-wieser Apr 14, 2021 •

edited

Loading

eric-wieser commented Apr 20, 2021 •

edited

Loading