Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

refactor(LinearAlgebra/SesquilinearForm/Properties): Refactor BilinForm dual and nondegenerate properties #11032

Closed
wants to merge 19 commits into from
Closed

refactor(LinearAlgebra/SesquilinearForm/Properties): Refactor BilinForm dual and nondegenerate properties #11032

wants to merge 19 commits into from

Conversation

mans0954
Copy link
Collaborator

@mans0954 mans0954 commented Feb 28, 2024 •
edited
Loading

Redefines dualSubmodule, dualSubmoduleToDual, toDual, dualBasis, symmCompOfNondegenerate and leftAdjointOfNondegenerate in terms of LinearMap.BilinForm instead of BilinForm. Associated results are migrated to LinearMap.BilinForm and the BilinForm versions recovered.

This is required inorder to define the TraceForm in LinearMap.BilinForm (#11057).

Contributes to #10553

Required for: #11057

Open in Gitpod

@mans0954 mans0954 added the WIP Work in progress label Feb 28, 2024
This was referenced Feb 28, 2024
Closed
Closed
@mans0954 mans0954 marked this pull request as ready for review February 28, 2024 22:28
@mans0954 mans0954 added awaiting-review and removed WIP Work in progress labels Feb 28, 2024
@eric-wieser
Copy link
Member

eric-wieser commented Feb 29, 2024 •
edited
Loading

Does anything use the old BilinForm files in this PR after this change? I'd be tempted to update them in place to be about LinearMap.BilinForm, so as to keep the history of the file, like we did with the TensorProduct file.

(perhaps worth a second opinion on Zulip before doing that)

@mans0954
Copy link
Collaborator Author

Does anything use the old BilinForm files in this PR after this change? I'd be tempted to update them in place to be about LinearMap.BilinForm, so as to keep the history of the file, like we did with the TensorProduct file.

@eric-wieser That could work for LinearAlgebra/BilinearForm/DualLattice. I'm less sure what to do about LinearAlgebra/BilinearForm/Properties because several of the concepts in that file not touched by this PR (e.g. IsRefl, IsAlt, IsSymm) already have equivalents in LinearAlgebra/SesquilinearForm. (Not quite the same as commutativity of the semi-ring is required there.)

@mans0954 mans0954 mentioned this pull request Mar 10, 2024
Closed
1 task
@mans0954
Copy link
Collaborator Author

Does anything use the old BilinForm files in this PR after this change? I'd be tempted to update them in place to be about LinearMap.BilinForm, so as to keep the history of the file, like we did with the TensorProduct file.

@eric-wieser is #11278 better?

I asked on Zulip but got no response.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 19, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 29, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 9, 2024
@mans0954 @eric-wieser @Vierkantor
refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …
aee79f6 
…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]>
@mans0954
Copy link
Collaborator Author

mans0954 commented Apr 9, 2024

I think this PR makes no sense in its current form now that #11278 has been merged, so closing.

@mans0954 mans0954 closed this Apr 9, 2024
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@mans0954 @eric-wieser
@Vierkantor @Louddy
refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …
e5ec108 
…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
@mans0954 @eric-wieser
@Vierkantor @atarnoam
refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …
6db7513 
…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
@mans0954 @eric-wieser
@Vierkantor @uniwuni
refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …
1ce336b 
…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
@mans0954 @eric-wieser
@Vierkantor @callesonne
refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …
9cfef67 
…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]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@mans0954 @eric-wieser @leanprover-community-mathlib4-bot