Add a description of a graded algebra. #5
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
eric-wieser
commented
Jul 2, 2020
| /-- Chisholm 6a, ish. | ||
| This says A = ⟨A}_r for r-vectors. | ||
| Chisholm aditionally wants proof that A != ⟨A}_r for non-rvectors -/ | ||
| lemma r_grade_of_coe {r : ℤ} (v : A r) : ⟨(to_fun v : G)⟩_r = v := begin |
There was a problem hiding this comment.
I want to be able to write this
Suggested change
| lemma r_grade_of_coe {r : ℤ} (v : A r) : ⟨(to_fun v : G)⟩_r = v := begin | |
| lemma r_grade_of_coe {r : ℤ} (v : A r) : ⟨(v : G)⟩_r = v := begin |
or even
Suggested change
| lemma r_grade_of_coe {r : ℤ} (v : A r) : ⟨(to_fun v : G)⟩_r = v := begin | |
| lemma r_grade_of_coe {r : ℤ} (v : A r) : ⟨v : G⟩_r = v := begin |
but I don't know how to prove the former, and the latter isn't legal syntax.
eric-wieser
commented
Jul 2, 2020
| end | ||
|
|
||
| /-- Chisholm 6b -/ | ||
| lemma grade_of_sum (r : ℤ) (a b : G) : (⟨a + b⟩_r : A r) = ⟨a⟩_r + ⟨b⟩_r := by simp |
There was a problem hiding this comment.
I would much rather write this
Suggested change
| lemma grade_of_sum (r : ℤ) (a b : G) : (⟨a + b⟩_r : A r) = ⟨a⟩_r + ⟨b⟩_r := by simp | |
| lemma grade_of_sum (r : ℤ) (a b : G) : ⟨a + b⟩_r = ⟨a⟩_r + ⟨b⟩_r := by simp |
but lean needs the type annotation for some reason.
There was a problem hiding this comment.
Can you do this in the definition of notation?
eric-wieser
commented
Jul 2, 2020
|
|
||
| /-- chisholm 6d. This is super awkward to express due to all the casting -/ | ||
| lemma grade_grade (r s : ℤ) (a : G) : | ||
| (to_fun (⟨ (to_fun (⟨a⟩_r : A r) : G) ⟩_s : A s) : G) = if r = s then to_fun (⟨a⟩_r : A r) else 0 |
There was a problem hiding this comment.
Ideally this would be:
Suggested change
| (to_fun (⟨ (to_fun (⟨a⟩_r : A r) : G) ⟩_s : A s) : G) = if r = s then to_fun (⟨a⟩_r : A r) else 0 | |
| ⟨⟨a⟩_r⟩_s = if r = s then ⟨a⟩_r else 0 |
but lean isn't happy at all with that.
eric-wieser
commented
Jul 2, 2020
| variables [graded_module A G] | ||
|
|
||
| /-- convert from r-vectors to multi-vectors -/ | ||
| instance has_coe (r : ℤ) : has_coe (A r) G := { coe := to_fun } |
There was a problem hiding this comment.
This coe ends up being rather hard to work with in proofs
There was a problem hiding this comment.
Been there. Have you tried norm_cast?
There was a problem hiding this comment.
Introducing a trivial rfl lemma seemed to help.
utensil
approved these changes
Jul 2, 2020
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.