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/remove BilinForm #10553

Closed
mans0954 opened this issue Feb 14, 2024 · 1 comment
Closed

Refactor/remove BilinForm #10553

mans0954 opened this issue Feb 14, 2024 · 1 comment

Comments

@mans0954
Copy link
Collaborator

mans0954 commented Feb 14, 2024 •
edited
Loading

There seems to be broad agreement that in the long term structure BilinForm should not exist - instead we should use M →ₗ[R] M →ₗ[R] R.

Many BilinForm results already have equivalents e.g. following #9485, many of the results in LinearAlgebra/Matrix/BilinearForm are just wrappers around results in LinearAlgebra/Matrix/SesquilinearForm.

One possible objection to removing BilinForm altogether at this stage is that it supports non-commutative semirings, which M →ₗ[R] M →ₗ[R] R does not support without further assumptions.

Zulip discussion:

Related issues/PRs:
@eric-wieser
Copy link
Member

eric-wieser commented Feb 14, 2024 •
edited
Loading

One possible objection to removing BilinForm altogether at this stage is that it supports non-commutative semirings,

I don't think this is meaningfully true; the axiomatization is basically nonsense for non-commutative semirings, so while we may support BilinForm R when Semiring R, it's not a "bilinear form" any more.

@eric-wieser eric-wieser mentioned this issue Feb 16, 2024
Closed
mathlib-bors bot pushed a commit that referenced this issue Feb 17, 2024
@eric-wieser @mans0954
chore(LinearAlgebra): Introduce a LinearMap.BilinForm alias (#10632)
2ef6133 
This is one of the steps in #10553.

Once we eliminate `_root_.BilinForm`, we can drop the `LinearMap.` prefix.

Requested on Zulip [by me](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bounded.20bilinear.20forms/near/261981962) (2021), [by @kmill](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60bilinear_form.60/near/310675731) (2022), and perhaps one or two other places.



Co-authored-by: Christopher Hoskin <[email protected]>
riccardobrasca pushed a commit that referenced this issue Feb 18, 2024
@eric-wieser @mans0954 @riccardobrasca
chore(LinearAlgebra): Introduce a LinearMap.BilinForm alias (#10632)
8dedddf 
This is one of the steps in #10553.

Once we eliminate `_root_.BilinForm`, we can drop the `LinearMap.` prefix.

Requested on Zulip [by me](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bounded.20bilinear.20forms/near/261981962) (2021), [by @kmill](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60bilinear_form.60/near/310675731) (2022), and perhaps one or two other places.



Co-authored-by: Christopher Hoskin <[email protected]>
thorimur pushed a commit that referenced this issue Feb 24, 2024
@eric-wieser @mans0954 @thorimur
chore(LinearAlgebra): Introduce a LinearMap.BilinForm alias (#10632)
8111fb5 
This is one of the steps in #10553.

Once we eliminate `_root_.BilinForm`, we can drop the `LinearMap.` prefix.

Requested on Zulip [by me](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bounded.20bilinear.20forms/near/261981962) (2021), [by @kmill](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60bilinear_form.60/near/310675731) (2022), and perhaps one or two other places.



Co-authored-by: Christopher Hoskin <[email protected]>
thorimur pushed a commit that referenced this issue Feb 26, 2024
@eric-wieser @mans0954 @thorimur
chore(LinearAlgebra): Introduce a LinearMap.BilinForm alias (#10632)
0ac1782 
This is one of the steps in #10553.

Once we eliminate `_root_.BilinForm`, we can drop the `LinearMap.` prefix.

Requested on Zulip [by me](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bounded.20bilinear.20forms/near/261981962) (2021), [by @kmill](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60bilinear_form.60/near/310675731) (2022), and perhaps one or two other places.



Co-authored-by: Christopher Hoskin <[email protected]>
This was referenced Feb 28, 2024
Closed
Closed
Closed
Closed
mathlib-bors bot pushed a commit that referenced this issue Mar 2, 2024
@mans0954
Refactor(Analysis): from BilinForm to LinearMap.BilinForm (#11097)
6cf6e97 
Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553



Co-authored-by: Christopher Hoskin <[email protected]>
mathlib-bors bot pushed a commit that referenced this issue Mar 2, 2024
@mans0954 @eric-wieser
Refactor(Analysis): from BilinForm to LinearMap.BilinForm (#11097)
4e3cf2f 
Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
mathlib-bors bot pushed a commit that referenced this issue Mar 8, 2024
@mans0954
refactor(Algebra/Lie/SkewAdjoint): from BilinForm to LinearMap.BilinF…
9830814 
…orm (#11078)

Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553
This was referenced Mar 10, 2024
Closed
Closed
kbuzzard pushed a commit that referenced this issue Mar 12, 2024
@mans0954 @eric-wieser @kbuzzard
Refactor(Analysis): from BilinForm to LinearMap.BilinForm (#11097)
2a2022b 
Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
kbuzzard pushed a commit that referenced this issue Mar 12, 2024
@mans0954 @kbuzzard
refactor(Algebra/Lie/SkewAdjoint): from BilinForm to LinearMap.BilinF…
f5ed71f 
…orm (#11078)

Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553
mathlib-bors bot pushed a commit that referenced this issue Mar 18, 2024
@Vierkantor @mans0954 @eric-wieser
refactor(LinearAlgebra/BilinearForm/Basic): descope BilinForm to mo…
346550b 
…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]>
dagurtomas pushed a commit that referenced this issue Mar 22, 2024
@eric-wieser @mans0954 @dagurtomas
chore(LinearAlgebra): Introduce a LinearMap.BilinForm alias (#10632)
c9b4b99 
This is one of the steps in #10553.

Once we eliminate `_root_.BilinForm`, we can drop the `LinearMap.` prefix.

Requested on Zulip [by me](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bounded.20bilinear.20forms/near/261981962) (2021), [by @kmill](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60bilinear_form.60/near/310675731) (2022), and perhaps one or two other places.



Co-authored-by: Christopher Hoskin <[email protected]>
dagurtomas pushed a commit that referenced this issue Mar 22, 2024
@mans0954 @eric-wieser @dagurtomas
Refactor(Analysis): from BilinForm to LinearMap.BilinForm (#11097)
e537ad0 
Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
dagurtomas pushed a commit that referenced this issue Mar 22, 2024
@mans0954 @dagurtomas
refactor(Algebra/Lie/SkewAdjoint): from BilinForm to LinearMap.BilinF…
179c229 
…orm (#11078)

Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553
dagurtomas pushed a commit that referenced this issue Mar 22, 2024
@Vierkantor @mans0954
@eric-wieser @dagurtomas
refactor(LinearAlgebra/BilinearForm/Basic): descope BilinForm to mo…
5300ea8 
…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 issue Mar 26, 2024
@mans0954 @eric-wieser @utensil
Refactor(Analysis): from BilinForm to LinearMap.BilinForm (#11097)
e9b96a0 
Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
utensil pushed a commit that referenced this issue Mar 26, 2024
@mans0954 @utensil
refactor(Algebra/Lie/SkewAdjoint): from BilinForm to LinearMap.BilinF…
a67f7ce 
…orm (#11078)

Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553
utensil pushed a commit that referenced this issue Mar 26, 2024
@Vierkantor @mans0954
@eric-wieser @utensil
refactor(LinearAlgebra/BilinearForm/Basic): descope BilinForm to mo…
f6d1a10 
…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 mathlib-bors bot closed this as completed in aee79f6 Apr 9, 2024
Louddy pushed a commit that referenced this issue Apr 15, 2024
@mans0954 @eric-wieser @Louddy
Refactor(Analysis): from BilinForm to LinearMap.BilinForm (#11097)
3093c3b 
Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Louddy pushed a commit that referenced this issue Apr 15, 2024
@mans0954 @Louddy
refactor(Algebra/Lie/SkewAdjoint): from BilinForm to LinearMap.BilinF…
45c9282 
…orm (#11078)

Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553
Louddy pushed a commit that referenced this issue Apr 15, 2024
@Vierkantor @mans0954
@eric-wieser @Louddy
refactor(LinearAlgebra/BilinearForm/Basic): descope BilinForm to mo…
63e4c65 
…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]>
Louddy pushed a commit that referenced this issue 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 issue Apr 16, 2024
@Vierkantor @mans0954
@eric-wieser @atarnoam
refactor(LinearAlgebra/BilinearForm/Basic): descope BilinForm to mo…
3591469 
…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 issue 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 issue Apr 19, 2024
@mans0954 @uniwuni
refactor(Algebra/Lie/SkewAdjoint): from BilinForm to LinearMap.BilinF…
59652bc 
…orm (#11078)

Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553
uniwuni pushed a commit that referenced this issue Apr 19, 2024
@Vierkantor @mans0954
@eric-wieser @uniwuni
refactor(LinearAlgebra/BilinearForm/Basic): descope BilinForm to mo…
eb357ff 
…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 issue 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 issue Apr 22, 2024
@mans0954 @callesonne
refactor(Algebra/Lie/SkewAdjoint): from BilinForm to LinearMap.BilinF…
b4546d4 
…orm (#11078)

Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553
callesonne pushed a commit that referenced this issue Apr 22, 2024
@Vierkantor @mans0954
@eric-wieser @callesonne
refactor(LinearAlgebra/BilinearForm/Basic): descope BilinForm to mo…
51ffdfe 
…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 issue 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
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
2 participants
@eric-wieser @mans0954