feat(algebra/free_algebra): Define a grading #4321

eric-wieser · 2020-09-29T14:37:59Z

The grading takes the form free_algebra R X →ₐ[R] add_monoid_algebra (free_algebra R X) ℕ

It's likely that there are more generic lemmas about grading that can be shared with tensor_algebra and friends, but that's left to follow-up work

depends on [Merged by Bors] - feat(data/monoid_algebra): add missing has_coe_to_fun #4315 (first commit)
depends on [Merged by Bors] - feat(data/monoid_algebra): Allow R ≠ k in semimodule R (monoid_algebra k G) #4365
depends on [Merged by Bors] - feat(algebra/algebra/basic): Add map_finsupp_(sum|prod) to alg_(hom|equiv) #4603
depends on [Merged by Bors] feat(algebra/monoid_algebra): Bundle lift_nc_mul and lift_nc_one into a ring_hom and alg_hom #4789

src/algebra/free_algebra.lean

eric-wieser · 2020-09-29T16:54:03Z

src/algebra/free_algebra.lean

+noncomputable
+instance : has_coe (add_monoid_algebra (free_algebra R X) ℕ) (free_algebra R X) := ⟨
+  (add_monoid_algebra.sum_id R : add_monoid_algebra (free_algebra R X) ℕ →ₐ[R] (free_algebra R X))
+⟩
+
+@[simp, norm_cast]
+lemma coe_def (x : add_monoid_algebra (free_algebra R X) ℕ) : (x : free_algebra R X) = add_monoid_algebra.sum_id R x := rfl


This seemed harmless, and it makes the mouthful that is add_monoid_algebra.sum_id not really matter

You mean the instance? Why not make it a local instance?

src/algebra/free_algebra.lean

rwbarton · 2020-09-30T14:15:20Z

src/data/monoid_algebra.lean

@@ -679,6 +684,42 @@ lemma alg_hom_ext_iff {R : Type u₃} [comm_semiring k] [add_monoid G]
  (∀ x, φ₁ (finsupp.single x 1) = φ₂ (finsupp.single x 1)) ↔ φ₁ = φ₂ :=
 ⟨λ h, alg_hom_ext h, by rintro rfl _; refl⟩

+/--
+The `alg_hom` which maps from a grading of an algebra `A` back to that algebra.


I wouldn't use the word "grading" in this context. Rather, I would call this map the augmentation map of the monoid algebra: https://ncatlab.org/nlab/show/augmentation+ideal#for_group_algebras

For the Lean identifier, either augmentation or something like your sum_id or perhaps sum_coeffs seems fine.

Would you mind suggesting a complete docstring? My mathematical background is severely lacking.

src/data/monoid_algebra.lean

rwbarton · 2020-09-30T14:35:13Z

src/data/monoid_algebra.lean

@@ -225,10 +225,10 @@ instance [ring k] [monoid G] : ring (monoid_algebra k G) :=
 instance [comm_ring k] [comm_monoid G] : comm_ring (monoid_algebra k G) :=
 { mul_comm := mul_comm, .. monoid_algebra.ring}

-instance [semiring k] : has_scalar k (monoid_algebra k G) :=
+instance {R : Type*} [semiring R] [semiring k] [semimodule R k] : has_scalar R (monoid_algebra k G) :=


Can you switch the names R and k in this instance and the next one? This way around is too confusing.

I've updated #4365 to use a clearer naming

src/data/monoid_algebra.lean

…gebra-induction

…gebra-grading

src/algebra/monoid_algebra.lean

kbuzzard

I think that if this is to be the way a grading is defined, it might be good to spell out what the heck is going on in the module docstring -- it took me a while to figure out the relationship between grades and what most people think of as a grading (a decomposition of A into a direct sum of A_i).

kbuzzard · 2020-10-22T12:00:43Z

src/algebra/free_algebra.lean

+-/
+noncomputable
+def grades : (free_algebra R X) →ₐ[R] add_monoid_algebra (free_algebra R X) ℕ :=
+lift R $ finsupp.single 1 ∘ ι R


We have some algebra A (the free algebra), and the question is how to usefully state that A is actually an infinite internal direct sum of submodules A_i. This grades map here seems to be a map which does the following: if a is in A, let a_i be its i'th "piece". Then a_i is in A_i and all but finitely many a_i are zero. We can regard the a_i as elements of A. Now the a_i is a finite sequence of elements of A. So we can make them into a polynomial a_i X^i. grades sends a to this polynomial. I am surprised that this is a useful concept! But one cool thing about it is that it does seem to be a ring homomorphism, rather than just an R-module homomorphism. The next lemma says that if you evaluate the polynomial at 1 then you get back the element you started with. I've been out of the loop for over a month -- sorry if all this conversation has been had already. Is this the way to do grading of an algebra? It still seems a bit weird to me.

I think my choice not to use polynomial was deliberate, since I wasn't really trying to invoke the mental model of one (although admittedly I had not spotted that polynomial A is defeq to add_monoid_algebra A ℕ).

I am surprised that this is a useful concept!

It seemed to me like the only (and obvious) way to induce a grading from the universal property alone. I have no idea if this is "how it's done", it's just the way I stumbled upon. I suppose though there's no need for it to be the public interface to the grading, it was just simplest to leave it that way, and the fact it was a ring homomorphism seemed cute, even though there's zero reason to need grades x * grades y as an alternate spelling of grades (x * y).

Is this the way to do grading of an algebra?

I assume you mean for a general algebra?

the question is how to usefully state that A is actually an infinite internal direct sum of submodules A_i

I attempted to do this in #4812. The proofs were really quite painful, and I don't think we want to use an API like that until dfinsupp is easier to use.

kbuzzard · 2020-10-22T12:01:32Z

src/algebra/free_algebra.lean

+noncomputable
+instance : has_coe (add_monoid_algebra (free_algebra R X) ℕ) (free_algebra R X) := ⟨
+  (add_monoid_algebra.sum_id R : add_monoid_algebra (free_algebra R X) ℕ →ₐ[R] (free_algebra R X))
+⟩


Should this really be an instance? Do we know for sure that this is the coercion that everyone will want? "evaluate the polynomial at 1"?

I'm reading this as "evaluate my direct sum over A_i back into A" - I hadn't thought of the "evaluate the polynomial" interpretation, and I think it hurts rather than hinders

kbuzzard · 2020-10-22T12:02:32Z

src/algebra/free_algebra.lean

+noncomputable
+instance : has_coe (add_monoid_algebra (free_algebra R X) ℕ) (free_algebra R X) := ⟨
+  (add_monoid_algebra.sum_id R : add_monoid_algebra (free_algebra R X) ℕ →ₐ[R] (free_algebra R X))
+⟩
+
+@[simp, norm_cast]
+lemma coe_def (x : add_monoid_algebra (free_algebra R X) ℕ) : (x : free_algebra R X) = add_monoid_algebra.sum_id R x := rfl


You mean the instance? Why not make it a local instance?

src/data/finsupp/basic.lean

…gebra-grading

… eric-wieser/free_algebra-grading

eric-wieser · 2020-10-28T22:27:27Z

Now without any real changes to add_monoid_algebra, since those were split to other PRs.

eric-wieser · 2020-12-04T13:20:42Z

src/data/finsupp/basic.lean

@@ -200,6 +200,16 @@ begin
  { rw [single_eq_of_ne h, zero_apply] }
 end

+lemma single_of_single_apply (a a' : α) (b : M) :


Split to #5219

eric-wieser added WIP Work in progress 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 Sep 29, 2020

eric-wieser changed the title ~~feat(algebra/free_algebra): Attempt to define a grading~~ feat(algebra/free_algebra): Attempt to define a grading (deps: #4315) Sep 29, 2020

eric-wieser commented Sep 29, 2020

View reviewed changes

src/algebra/free_algebra.lean Outdated Show resolved Hide resolved

eric-wieser commented Sep 29, 2020

View reviewed changes

eric-wieser mentioned this pull request Sep 30, 2020

[Merged by Bors] - feat(data/monoid_algebra): add missing has_coe_to_fun #4315

Closed

eric-wieser added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Sep 30, 2020

eric-wieser marked this pull request as ready for review September 30, 2020 08:35

eric-wieser mentioned this pull request Sep 30, 2020

[Merged by Bors] - feat(algebra/free_algebra): Add an inductive principle #4335

Closed

rwbarton reviewed Sep 30, 2020

View reviewed changes

rwbarton added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 30, 2020

eric-wieser changed the base branch from master to eric-wieser/monoid_algebra-tweaks September 30, 2020 15:02

eric-wieser mentioned this pull request Sep 30, 2020

[Merged by Bors] - chore(*): Tidy some proofs and variables #4338

Closed

eric-wieser force-pushed the eric-wieser/monoid_algebra-tweaks branch from 53afbc0 to 9824b22 Compare October 2, 2020 11:58

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 2, 2020

eric-wieser force-pushed the eric-wieser/monoid_algebra-tweaks branch from 9824b22 to c31795f Compare October 2, 2020 15:37

eric-wieser changed the title ~~feat(algebra/free_algebra): Attempt to define a grading (deps: #4315)~~ feat(algebra/free_algebra): Attempt to define a grading (deps: #4315, #4365) Oct 2, 2020

eric-wieser mentioned this pull request Oct 2, 2020

[Merged by Bors] - feat(data/monoid_algebra): Allow R ≠ k in semimodule R (monoid_algebra k G) #4365

Closed

eric-wieser added 4 commits October 3, 2020 11:09

feat(algebra/free_algebra): Add an inductive principle

957b483

chore(algebra/free_algebra): Use a subtype instead of a struct

e789702

chore(algebra/free_algebra): Disable false positive linter

87d31ff

chore(algebra/free_algebra): Tidy up coercions

778e9db

eric-wieser force-pushed the eric-wieser/free_algebra-grading branch from ad8308a to a66671e Compare October 3, 2020 14:33

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 3, 2020

eric-wieser added 4 commits October 6, 2020 16:17

refactor(algebra/free_algebra): Replace most of the code with subalgebra

67e8211

fix(*): remove squeeze_simp

28b1893

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

ed419ec

…gebra-induction

chore(*): Tidy the proof

d816bfa

semorrison changed the title ~~feat(algebra/free_algebra): Define a grading (deps: #4315)~~ feat(algebra/free_algebra): Define a grading Oct 20, 2020

semorrison removed 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 Oct 20, 2020

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

bee9b3c

…gebra-grading

eric-wieser commented Oct 20, 2020

View reviewed changes

src/algebra/monoid_algebra.lean Outdated Show resolved Hide resolved

Update src/algebra/monoid_algebra.lean

caaa54d

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 22, 2020

kbuzzard reviewed Oct 22, 2020

View reviewed changes

eric-wieser mentioned this pull request Oct 26, 2020

[Merged by Bors] - feat(algebra/monoid_algebra): define a non-commutative version of lift #4725

Closed

7 tasks

eric-wieser added 2 commits October 26, 2020 13:02

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

33f38c7

…gebra-grading

wip

db82059

eric-wieser mentioned this pull request Oct 26, 2020

[Merged by Bors] feat(algebra/monoid_algebra): Bundle lift_nc_mul and lift_nc_one into a ring_hom and alg_hom #4789

Closed

eric-wieser 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 Oct 26, 2020

eric-wieser mentioned this pull request Oct 28, 2020

feat(algebra/graded_algebra): Define a dependent version of add_monoid_algebra #4812

Closed

Merge branch 'master' of github.com:leanprover-community/mathlib into…

986ed3c

… eric-wieser/free_algebra-grading

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 28, 2020

fix(*): adjust for changed lemmas

1d0b9c9

eric-wieser removed 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 Oct 28, 2020

eric-wieser force-pushed the eric-wieser/free_algebra-grading branch from 7274502 to 1d0b9c9 Compare October 28, 2020 22:24

jcommelin requested a review from rwbarton October 29, 2020 18:38

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 19, 2020

Merge branch 'master' into eric-wieser/free_algebra-grading

7c58060

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 4, 2020

eric-wieser mentioned this pull request Dec 4, 2020

[Merged by Bors] - chore(data/finsupp/basic): Add single_of_single_apply #5219

Closed

eric-wieser commented Dec 4, 2020

View reviewed changes

bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jan 16, 2021

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 30, 2021

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

semorrison added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(algebra/free_algebra): Define a grading #4321

feat(algebra/free_algebra): Define a grading #4321

eric-wieser commented Sep 29, 2020 •

edited by github-actions bot

eric-wieser Sep 29, 2020

kbuzzard Oct 22, 2020

rwbarton Sep 30, 2020

eric-wieser Sep 30, 2020

rwbarton Sep 30, 2020

eric-wieser Oct 2, 2020 •

edited

kbuzzard left a comment

kbuzzard Oct 22, 2020

eric-wieser Oct 22, 2020 •

edited

eric-wieser Oct 28, 2020

kbuzzard Oct 22, 2020

eric-wieser Oct 22, 2020

kbuzzard Oct 22, 2020

eric-wieser commented Oct 28, 2020

eric-wieser Dec 4, 2020

feat(algebra/free_algebra): Define a grading #4321

Are you sure you want to change the base?

feat(algebra/free_algebra): Define a grading #4321

Conversation

eric-wieser commented Sep 29, 2020 • edited by github-actions bot

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Oct 2, 2020 • edited

Choose a reason for hiding this comment

kbuzzard left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Oct 22, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser commented Oct 28, 2020

Choose a reason for hiding this comment

eric-wieser commented Sep 29, 2020 •

edited by github-actions bot

eric-wieser Oct 2, 2020 •

edited

eric-wieser Oct 22, 2020 •

edited