[Merged by Bors] - feat(linear_algebra/exterior_algebra): Add an exterior algebra #4297
Conversation
eric-wieser
added
the
awaiting-review
| It is endowed with the structure of an `R`-algebra. Some results only hold at the level of | ||
| generality of an `S`-module `M` and the space `exterior_algebra S N`. |
There was a problem hiding this comment.
I don't understand the meaning of the last sentence.
There was a problem hiding this comment.
Removed, it was part of the other branch that I decided to leave out for now
| The canonical quotient map `tensor_algebra R M → exterior_algebra R M`. | ||
| -/ | ||
| protected def quot : tensor_algebra R M →ₐ[R] exterior_algebra R M := | ||
| ring_quot.mk_alg_hom R _ |
There was a problem hiding this comment.
Here and below, don't indent the first line after :=. (Indenting happens before the := when the theorem statement runs over more than one line, but then the definition/proof starts again in the first column.)
There was a problem hiding this comment.
Removed this definition entirely, it wasn't used and I'm not yet convinced it was useful.
|
Otherwise, looks great! |
semorrison
added
awaiting-author
eric-wieser
added
awaiting-review
Co-authored-by: Adam Topaz <github@adamtopaz.com> Co-authored-by: Zhangir Azerbayev <zazerbayev@gmail.com>
eric-wieser
force-pushed
the
eric-wieser/exterior_algebra-def
branch
from
8b67c5d
to
5fa8938
Compare
|
Rebased on the merge of #4299 to eliminate some |
Vierkantor
added
awaiting-author
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
eric-wieser
added
awaiting-review
There was a problem hiding this comment.
Thank you for the fixes! It looks ready to merge to me, if we add a variables statement like in daf239d.
bors d+
| `cond : ∀ m : M, f m * f m = 0`, this is the canonical lift of `f` to a morphism of `R`-algebras | ||
| from `exterior_algebra R M` to `A`. | ||
| -/ | ||
| def lift {A : Type*} [semiring A] [algebra R A] (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = 0) : |
There was a problem hiding this comment.
Thank you so much for the cleanup PR! I pushed a commit to a new branch, adding the variables statement. If you agree with it, could you add it to this branch?
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Vierkantor
added
delegated
…rameters Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
|
bors r+ |
This adds the basic exterior algebra definitions using a very similar approach to `universal_enveloping_algebra`. It's based off the `exterior_algebra` branch, dropping the `wedge` stuff for now as development in multilinear maps is happening elsewhere. Co-authored-by: Adam Topaz <github@adamtopaz.com> Co-authored-by: Zhangir Azerbayev <zazerbayev@gmail.com>
|
This PR was included in a batch that was canceled, it will be automatically retried |
This adds the basic exterior algebra definitions using a very similar approach to `universal_enveloping_algebra`. It's based off the `exterior_algebra` branch, dropping the `wedge` stuff for now as development in multilinear maps is happening elsewhere. Co-authored-by: Adam Topaz <github@adamtopaz.com> Co-authored-by: Zhangir Azerbayev <zazerbayev@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This adds the basic exterior algebra definitions using a very similar approach to `universal_enveloping_algebra`. It's based off the `exterior_algebra` branch, dropping the `wedge` stuff for now as development in multilinear maps is happening elsewhere. Co-authored-by: Adam Topaz <github@adamtopaz.com> Co-authored-by: Zhangir Azerbayev <zazerbayev@gmail.com>
This adds the basic exterior algebra definitions using a very similar approach to
universal_enveloping_algebra.It's based off the
exterior_algebrabranch, dropping thewedgestuff for now as development in multilinear maps is happening elsewhere.Co-authored-by: Adam Topaz github@adamtopaz.com
Co-authored-by: Zhangir Azerbayev zazerbayev@gmail.com
This will conflict with #4299, I don't really care which goes in first.