refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise `QuadraticForm` to `QuadraticMap`

[mans0954]

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.

---

• [x] depends on: #7581
• [ ] depends on: #12617

[eric-wieser]

Having thought some more, I think the non-commutative case should be $Q(ax) = aQ(x)a^*$ (making $x \mapsto xx^*$ a quadratic form), but I don't think we should worry about that until someone asks for it

[mans0954]

Having thought some more, I think the non-commutative case should be Q(ax)=aQ(x)a∗ (making x↦xx∗ a quadratic form), but I don't think we should worry about that until someone asks for it

I had that thought too - the polar would be a σ-sesquilinear form.

[github-actions[bot]]

Import summary

No significant changes to the import graph

[github-actions[bot]]

PR summary 2532a7b58d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Matrix.toQuadraticMap' + QuadraticMap + QuadraticMap.isSymm_toMatrix' + QuadraticMap.toMatrix' + QuadraticMap.toMatrix'_smul + _root_.LinearMap.BilinForm.toQuadraticMap_isOrtho + _root_.LinearMap.compQuadraticMap + _root_.LinearMap.compQuadraticMap' + _root_.LinearMap.compQuadraticMap_polar + _root_.LinearMap.compQuadraticMap_polarBilin + _root_.QuadraticMap.polarBilin_comp + _root_.QuadraticMap.polarBilin_injective + _root_.QuadraticMap.toQuadraticMap_polarBilin + associated_toQuadraticMap + instance : Add (QuadraticMap R M N) + instance : AddCommGroup (QuadraticMap R M N) + instance : AddCommMonoid (QuadraticMap R M N) + instance : CoeFun (QuadraticMap R M N) fun _ => M → N + instance : Inhabited (QuadraticMap R M N) + instance : Neg (QuadraticMap R M N) + instance : SMul S (QuadraticMap R M N) + instance : Sub (QuadraticMap R M N) + instance : Zero (QuadraticMap R M N) + instance [Monoid S] [DistribMulAction S N] [SMulCommClass S R N] : + instance [SMul S T] [IsScalarTower S T N] : IsScalarTower S T (QuadraticMap R M N) + instance [SMulCommClass S T N] : SMulCommClass S T (QuadraticMap R M N) + instance [Semiring S] [Module S N] [SMulCommClass S R N] : + polarBilin_toQuadraticMap + polar_toQuadraticMap + restrictScalars + toQuadraticMap + toQuadraticMapAddMonoidHom + toQuadraticMapLinearMap + toQuadraticMap_add + toQuadraticMap_apply + toQuadraticMap_associated + toQuadraticMap_comp_same + toQuadraticMap_eq_zero + toQuadraticMap_list_sum + toQuadraticMap_multiset_sum + toQuadraticMap_neg + toQuadraticMap_smul + toQuadraticMap_sub + toQuadraticMap_sum + toQuadraticMap_zero - Matrix.toQuadraticForm' - QuadraticForm - QuadraticForm.isSymm_toMatrix' - QuadraticForm.toMatrix' - QuadraticForm.toMatrix'_smul - _root_.LinearMap.BilinForm.toQuadraticForm_isOrtho - _root_.LinearMap.compQuadraticForm - _root_.QuadraticForm.polarBilin_comp - _root_.QuadraticForm.polarBilin_injective - _root_.QuadraticForm.toQuadraticForm_polarBilin - associated_toQuadraticForm - compQuadraticForm_polar - compQuadraticForm_polarBilin - instance : Add (QuadraticForm R M) - instance : AddCommGroup (QuadraticForm R M) - instance : AddCommMonoid (QuadraticForm R M) - instance : CoeFun (QuadraticForm R M) fun _ => M → R - instance : Inhabited (QuadraticForm R M) - instance : Neg (QuadraticForm R M) - instance : SMul S (QuadraticForm R M) - instance : Sub (QuadraticForm R M) - instance : Zero (QuadraticForm R M) - instance [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] : - instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T (QuadraticForm R M) - instance [SMulCommClass S T R] : SMulCommClass S T (QuadraticForm R M) - instance [Semiring S] [Module S R] [SMulCommClass S R R] : - polarBilin_toQuadraticForm - polar_toQuadraticForm - toQuadraticForm - toQuadraticFormAddMonoidHom - toQuadraticFormLinearMap - toQuadraticForm_add - toQuadraticForm_apply - toQuadraticForm_associated - toQuadraticForm_comp_same - toQuadraticForm_eq_zero - toQuadraticForm_list_sum - toQuadraticForm_multiset_sum - toQuadraticForm_neg - toQuadraticForm_smul - toQuadraticForm_sub - toQuadraticForm_sum - toQuadraticForm_zero -+-+ separatingLeft_of_anisotropic

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#7581~~ By Dependent Issues (🤖). Happy coding!

[eric-wieser]

!bench

[leanprover-bot]

Here are the benchmark results for commit 102aa6bc58970c2dc024c883438e0aef72bb80ec. There were significant changes against commit 41eb6f94b1259c02e310381d93cf257d5049773c:

  Benchmark                                        Metric         Change
  ======================================================================
+ build                                            linting         -5.3%
- ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading   instructions    20.1%
- ~Mathlib.LinearAlgebra.QuadraticForm.Basic       instructions    30.0%

[eric-wieser]

!bench

[leanprover-bot]

Here are the benchmark results for commit 24107938e020a3fe34c99243c1e5386e34701d49. There were significant changes against commit 8e7020a51c06ed9898967c4da5dcd473d1048171:

  Benchmark                                        Metric         Change
  ======================================================================
- ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading   instructions    19.6%
- ~Mathlib.LinearAlgebra.QuadraticForm.Basic       instructions    30.1%

[MichaelStollBayreuth]

General information:

lint:                                                  +23.963 * 10⁹ (+0.299%)
build:                                                 +114.28 * 10⁹ (+0.0933%)

15 files got slower by at least 10⁹ instructions

Mathlib.LinearAlgebra.QuadraticForm.Basic:             +42.057 * 10⁹ (+30.1%)
Mathlib.LinearAlgebra.ExteriorAlgebra.Grading:         +10.988 * 10⁹ (+19.6%)
Mathlib.LinearAlgebra.QuadraticForm.TensorProduct:     +9.0410 * 10⁹ (+8.80%)
Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating:   +7.3102 * 10⁹ (+18.8%)
Mathlib.LinearAlgebra.CliffordAlgebra.Equivs:          +6.7790 * 10⁹ (+10.2%)
Mathlib.LinearAlgebra.CliffordAlgebra.Contraction:     +6.4159 * 10⁹ (+5.59%)
Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries:
                                                       +4.8889 * 10⁹ (+5.80%)
Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv:       +4.6507 * 10⁹ (+3.63%)
Mathlib.LinearAlgebra.QuadraticForm.Prod:              +4.3047 * 10⁹ (+10.5%)
Mathlib.CategoryTheory.Category.Cat.Limit:             +2.0291 * 10⁹ (+2.13%)
Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv:     +1.8858 * 10⁹ (+11.8%)
Mathlib.LinearAlgebra.Matrix.PosDef:                   +1.5872 * 10⁹ (+3.38%)
Mathlib.LinearAlgebra.CliffordAlgebra.Inversion:       +1.4714 * 10⁹ (+6.60%)
Mathlib.LinearAlgebra.ExteriorAlgebra.Basic:           +1.2953 * 10⁹ (+2.01%)
Mathlib.LinearAlgebra.CliffordAlgebra.Prod:            +1.0083 * 10⁹ (+1.90%)

6 files got slower by at least 10%:

Mathlib.LinearAlgebra.QuadraticForm.Basic:                            +30.1%
Mathlib.LinearAlgebra.ExteriorAlgebra.Grading:                        +19.6%
Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating:                  +18.8%
Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv:                    +11.8%
Mathlib.LinearAlgebra.QuadraticForm.Prod:                             +10.5%
Mathlib.LinearAlgebra.CliffordAlgebra.Equivs:                         +10.2%

No file got faster by at least 10⁹ instructions.

No file got faster by at least 10%.

[eric-wieser]

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.

[mathlib-bors[bot]]

:v: mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mans0954]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style