[Merged by Bors] - refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise QuadraticForm to QuadraticMap#7569
Closed
[Merged by Bors] - refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise QuadraticForm to QuadraticMap#7569
QuadraticForm to QuadraticMap#7569Conversation
eric-wieser
reviewed
Oct 8, 2023
Member
|
Having thought some more, I think the non-commutative case should be |
Collaborator
Author
I had that thought too - the polar would be a σ-sesquilinear form. |
ghost
added
blocked-by-other-PR
ghost
removed
the
merge-conflict
eric-wieser
reviewed
Oct 9, 2023
Contributor
|
General information: 15 files got slower by at least 10⁹ instructions6 files got slower by at least 10%: No file got faster by at least 10⁹ instructions. No file got faster by at least 10%. |
Member
|
bors d+ Thanks again for your patience here! Please look over @MichaelStollBayreuth's suggestions above, and reword the docstrings where appropriate. The performance doesn't look great (especially impacting files that I spend time on!), but I think this is likely just an unavoidable cost of generality, and so we don't need to worry about it for now. |
Contributor
|
✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
the
delegated
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Collaborator
Author
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jul 13, 2024
…rm` to `QuadraticMap` (#7569) Most of the theory in `LinearAlgebra/QuadraticForm/Basic` also holds for Quadratic Maps with minimal modification. A quadratic form is just a special case of a quadratic map. To keep this PR to a reasonable size I have not attempted to generalise other files in `LinearAlgebra/QuadraticForm` - this can be done in subsequent PRs. To facilitate dot notation we also introduce `LinearMap.BilinMap` as an abbreviation for `M →ₗ[R] M →ₗ[R] N`. No attempt has been made to generalise all `BilinForm` results to `BilinMap` at this stage. Some results in `LinearAlgebra/QuadraticForm/Basic` are still stated for quadratic forms either because there was no obvious generalisation to quadratic maps, or the generalisation requires improvements elsewhere in Mathlib which can be considered in subsequent PRs. My motivation for introducing Quadratic Maps to Mathlib is that it would allow the definition of interesting non-associative structures such as quadratic Jordan Algebras and Jordan Pairs. Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
QuadraticForm to QuadraticMapQuadraticForm to QuadraticMap
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jul 17, 2024
Also `.prod` and `.pi`, since these are heavily entangled with `Isometry` and `IsometryEquiv`. Follows on from #7569.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
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.
Most of the theory in
LinearAlgebra/QuadraticForm/Basicalso holds for Quadratic Maps with minimal modification. A quadratic form is just a special case of a quadratic map.To keep this PR to a reasonable size I have not attempted to generalise other files in
LinearAlgebra/QuadraticForm- this can be done in subsequent PRs.To facilitate dot notation we also introduce
LinearMap.BilinMapas an abbreviation forM →ₗ[R] M →ₗ[R] N. No attempt has been made to generalise allBilinFormresults toBilinMapat this stage.Some results in
LinearAlgebra/QuadraticForm/Basicare still stated for quadratic forms either because there was no obvious generalisation to quadratic maps, or the generalisation requires improvements elsewhere in Mathlib which can be considered in subsequent PRs.My motivation for introducing Quadratic Maps to Mathlib is that it would allow the definition of interesting non-associative structures such as quadratic Jordan Algebras and Jordan Pairs.