This repository was archived by the owner on Jul 24, 2024. It is now read-only.
[Merged by Bors] - feat(linear_algebra/matrix): Add matrix properties for sesquilinear forms#15906
Closed
[Merged by Bors] - feat(linear_algebra/matrix): Add matrix properties for sesquilinear forms#15906
Conversation
This was referenced Aug 7, 2022
[Merged by Bors] - chore(analysis/inner_product_space/basic): remove
bilin_form_of_real_inner
#15780
Closed
mcdoll
added
awaiting-review
…over-community/mathlib into mcdoll/bilin_form_matrix_refactor
Vierkantor
reviewed
Sep 24, 2022
Collaborator
Vierkantor
left a comment
Vierkantor
left a comment
There was a problem hiding this comment.
A couple of suggestions, looks pretty good overall. I didn't have time yet to go through the entirety of matrix/sesquilinear_form.lean.
Vierkantor
added
awaiting-author
Co-authored-by: Anne Baanen <[email protected]>
Co-authored-by: Anne Baanen <[email protected]>
mcdoll
added
awaiting-review
mcdoll
commented
Sep 26, 2022
mcdoll
commented
Sep 27, 2022
|
✌️ mcdoll can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
Co-authored-by: Anne Baanen <[email protected]>
Member
Author
|
@Vierkantor your suggestion gives funny errors and I have no idea how to fix them without reverting to the original version. |
Vierkantor
reviewed
Oct 3, 2022
Co-authored-by: Anne Baanen <[email protected]>
Member
Author
|
bors merge |
bors bot
pushed a commit
that referenced
this pull request
Oct 3, 2022
…orms (#15906) The main goal of this PR is to move `linear_algebra/matrix/bilinear_form` to the curried bilinear map form. Since this file as quite few dependencies we copy it to a new file `linear_algebra/matrix/sesquilinear_form` and then move all the dependencies. The structure is taken literally from `linear_algebra/matrix/bilinear_form` with generalizations and easier proofs where possible. The new lemmas are named exactly as the old ones with the following changes: - the namespace changed from `bilin_form` to `linear_map` - `bilin` is changed to `linear_map₂`. In case there is the necessity for separate bilinear and semi-bilinear lemmas we use `linear_map₂` and `linear_mapₛₗ₂` - If `bilin` is not in the name of a lemma, `matrix` is changed to `matrix₂` to avoid nameclashes with lemmas for linear maps `M →ₛₗ[ρ₁₂] N` Moreover, the following changes were necessary: `linear_algebra/bilinear_map`: - Weakened some typeclass assumptions - Added bilinear version of `sum_repr_mul_repr_mul` and moved sesquilinear version to `sum_repr_mul_repr_mulₛₗ` `linear_algebra/matrix/bilinear_form`: - Moved `basis.equiv_fun_symm_std_basis` to `linear_algebra/std_basis` - `adjoint_pair` section: Removed a few definitions (they are now in `linear_algebra/matrix/sesquilinear_form`) and added a prime to the names of lemmas that have the same name as the version in `linear_algebra/matrix/sesquilinear_form` `linear_algebra/sesquilinear_form`: - Added a few missing lemmas about left-separating bilinear forms (note that `separating_left` was previously known as `nondegenerate`) `linear_algebra/std_basis`: - Lemma `std_basis_apply'` for calculating the application of `i' : ι` to `(std_basis R (λ (_x : ι), R) i)` `algebra/hom/ring/`: - Lemmas for calculating a ring homomorphism applied to `ite 0 1` and `ite 1 0` The last two additions are needed to get a reasonable proof for `matrix.to_linear_map₂'_aux_std_basis`. Co-authored-by: Moritz Doll <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
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 subscribe to this conversation on GitHub.
Already have an account?
Sign in.
3 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.
The main goal of this PR is to move
linear_algebra/matrix/bilinear_formto the curried bilinear map form. Since this file as quite few dependencies we copy it to a new filelinear_algebra/matrix/sesquilinear_formand then move all the dependencies.The structure is taken literally from
linear_algebra/matrix/bilinear_formwith generalizations and easier proofs where possible. The new lemmas are named exactly as the old ones with the following changes:bilin_formtolinear_mapbilinis changed tolinear_map₂. In case there is the necessity for separate bilinear and semi-bilinear lemmas we uselinear_map₂andlinear_mapₛₗ₂bilinis not in the name of a lemma,matrixis changed tomatrix₂to avoid nameclashes with lemmas for linear mapsM →ₛₗ[ρ₁₂] NMoreover, the following changes were necessary:
linear_algebra/bilinear_map:sum_repr_mul_repr_muland moved sesquilinear version tosum_repr_mul_repr_mulₛₗlinear_algebra/matrix/bilinear_form:basis.equiv_fun_symm_std_basistolinear_algebra/std_basisadjoint_pairsection: Removed a few definitions (they are now inlinear_algebra/matrix/sesquilinear_form) and added a prime to the names of lemmas that have the same name as the version inlinear_algebra/matrix/sesquilinear_formlinear_algebra/sesquilinear_form:separating_leftwas previously known asnondegenerate)linear_algebra/std_basis:std_basis_apply'for calculating the application ofi' : ιto(std_basis R (λ (_x : ι), R) i)algebra/hom/ring/:ite 0 1andite 1 0The last two additions are needed to get a reasonable proof for
matrix.to_linear_map₂'_aux_std_basis.There are some bikeshedding questions about docstrings: Should the map
M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] Rbe called "semi-bilinear" or "sesquilinear" or something completely different?I have very slight naming inconsistency in that I add a subscript
₂aftermatrixin some lemmas if there is no reference to bilinear maps in some sense, i.e., there islinear_map.mul_to_matrix₂_mul(l. 412), butlinear_map.to_matrix'_to_linear_map₂'(l.223).I thought about using the subscript everywhere but I find these subscripts annoying to type.
Please let me know if you want any further explanation of the naming schemes, I find them completely obvious but I spend too much time on this PR..