refactor(LinearAlgebra/BilinearForm/Properties): Restrict the definition of BilinForm.IsSymm to commutative semiring#10422
Closed
refactor(LinearAlgebra/BilinearForm/Properties): Restrict the definition of BilinForm.IsSymm to commutative semiring#10422
Conversation
1 task
Contributor
|
This sounds like a strict downgrade: the definition of |
Contributor
Linear maps don't, but bilinear maps do, since the instance |
Contributor
|
I think replacing |
Contributor
|
I made a start in commit 4244c22, and it builds. We still need to deduplicate/rename the variables in those files. Feel free to adopt. |
Vierkantor
added
awaiting-author
This was referenced Mar 10, 2024
ghost
added
the
merge-conflict
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 18, 2024
…dules over commutative semirings (#11280) Require the module in the definition of the `BilinForm` structure to be over a commutative semiring. This PR is a per-requisite for #11278. It supersedes #10422. It's been pointed out elsewhere that the current definition over a non-commutative semiring doesn't make mathematical sense: #10553 (comment) Eventually the non-commutative situation may be considered in a mathematically meaningful way in the context of sesquilinear maps (e.g. something like #9334 (review)). Co-authored-by: @Vierkantor Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
Member
|
I attempted to resolve the conflicts, it seems that #11280 completely subsumed this. |
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
…dules over commutative semirings (#11280) Require the module in the definition of the `BilinForm` structure to be over a commutative semiring. This PR is a per-requisite for #11278. It supersedes #10422. It's been pointed out elsewhere that the current definition over a non-commutative semiring doesn't make mathematical sense: #10553 (comment) Eventually the non-commutative situation may be considered in a mathematically meaningful way in the context of sesquilinear maps (e.g. something like #9334 (review)). Co-authored-by: @Vierkantor Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
utensil
pushed a commit
that referenced
this pull request
Mar 26, 2024
…dules over commutative semirings (#11280) Require the module in the definition of the `BilinForm` structure to be over a commutative semiring. This PR is a per-requisite for #11278. It supersedes #10422. It's been pointed out elsewhere that the current definition over a non-commutative semiring doesn't make mathematical sense: #10553 (comment) Eventually the non-commutative situation may be considered in a mathematically meaningful way in the context of sesquilinear maps (e.g. something like #9334 (review)). Co-authored-by: @Vierkantor Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 9, 2024
…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278) Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` Closes: #10553 This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs. Supersedes: - #11057 - #11032 - #10432 - #10422 Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Vierkantor <[email protected]>
xgenereux
pushed a commit
that referenced
this pull request
Apr 15, 2024
…dules over commutative semirings (#11280) Require the module in the definition of the `BilinForm` structure to be over a commutative semiring. This PR is a per-requisite for #11278. It supersedes #10422. It's been pointed out elsewhere that the current definition over a non-commutative semiring doesn't make mathematical sense: #10553 (comment) Eventually the non-commutative situation may be considered in a mathematically meaningful way in the context of sesquilinear maps (e.g. something like #9334 (review)). Co-authored-by: @Vierkantor Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
xgenereux
pushed a commit
that referenced
this pull request
Apr 15, 2024
…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278) Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` Closes: #10553 This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs. Supersedes: - #11057 - #11032 - #10432 - #10422 Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Vierkantor <[email protected]>
atarnoam
pushed a commit
that referenced
this pull request
Apr 16, 2024
…dules over commutative semirings (#11280) Require the module in the definition of the `BilinForm` structure to be over a commutative semiring. This PR is a per-requisite for #11278. It supersedes #10422. It's been pointed out elsewhere that the current definition over a non-commutative semiring doesn't make mathematical sense: #10553 (comment) Eventually the non-commutative situation may be considered in a mathematically meaningful way in the context of sesquilinear maps (e.g. something like #9334 (review)). Co-authored-by: @Vierkantor Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
atarnoam
pushed a commit
that referenced
this pull request
Apr 16, 2024
…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278) Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` Closes: #10553 This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs. Supersedes: - #11057 - #11032 - #10432 - #10422 Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Vierkantor <[email protected]>
uniwuni
pushed a commit
that referenced
this pull request
Apr 19, 2024
…dules over commutative semirings (#11280) Require the module in the definition of the `BilinForm` structure to be over a commutative semiring. This PR is a per-requisite for #11278. It supersedes #10422. It's been pointed out elsewhere that the current definition over a non-commutative semiring doesn't make mathematical sense: #10553 (comment) Eventually the non-commutative situation may be considered in a mathematically meaningful way in the context of sesquilinear maps (e.g. something like #9334 (review)). Co-authored-by: @Vierkantor Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
uniwuni
pushed a commit
that referenced
this pull request
Apr 19, 2024
…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278) Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` Closes: #10553 This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs. Supersedes: - #11057 - #11032 - #10432 - #10422 Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Vierkantor <[email protected]>
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
…dules over commutative semirings (#11280) Require the module in the definition of the `BilinForm` structure to be over a commutative semiring. This PR is a per-requisite for #11278. It supersedes #10422. It's been pointed out elsewhere that the current definition over a non-commutative semiring doesn't make mathematical sense: #10553 (comment) Eventually the non-commutative situation may be considered in a mathematically meaningful way in the context of sesquilinear maps (e.g. something like #9334 (review)). Co-authored-by: @Vierkantor Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278) Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` Closes: #10553 This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs. Supersedes: - #11057 - #11032 - #10432 - #10422 Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Vierkantor <[email protected]>
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
4 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.
Restrict the definition of
BilinForm.IsSymmandBilinForm.IsReflto modules over a commutative semiring.Currently
BilinForm.IsSymmandBilinForm.IsReflare defined for modules over a semiring, whereasLinearMap.IsSymmis defined for modules over a commutative semiring. We wish to redefineBilinForm.IsSymmin terms ofLinearMap.IsSymmas part of #10432. This PR is a preliminary step in that direction.