[Merged by Bors] - 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.

---

• depends on: [Merged by Bors] - refactor(LinearAlgebra/QuadraticForm/Basic): remove non-commutativity support #7581

[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.

[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]

✌️ 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]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style