Constructing a bilinear map from a quadratic map, given a basis

This file provides an alternative to QuadraticMap.associated; unlike that definition, this one does not require Invertible (2 : R). Unlike that definition, this only works in the presence of a basis.

noncomputable def QuadraticMap.toBilin {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [LinearOrder ι] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (bm : Basis ι R M) : LinearMap.BilinMap R M N

Given an ordered basis, produce a bilinear form associated with the quadratic form.

Unlike QuadraticMap.associated, this is not symmetric; however, as a result it can be used even in characteristic two. When considered as a matrix, the form is triangular.

Equations

• Q.toBilin bm = (bm.constr R) fun (i : ι) => (bm.constr R) fun (j : ι) => if i = j then Q (bm i) else if i < j then QuadraticMap.polar (⇑Q) (bm i) (bm j) else 0

theorem QuadraticMap.toBilin_apply {ι : Type u_4} {R : Type u_1} {M : Type u_2} {N : Type u_3} [LinearOrder ι] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (bm : Basis ι R M) (i : ι) (j : ι) : ((Q.toBilin bm) (bm i)) (bm j) = if i = j then Q (bm i) else if i < j then QuadraticMap.polar (⇑Q) (bm i) (bm j) else 0

theorem QuadraticMap.toQuadraticMap_toBilin {ι : Type u_4} {R : Type u_1} {M : Type u_2} {N : Type u_3} [LinearOrder ι] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (bm : Basis ι R M) : (Q.toBilin bm).toQuadraticMap = Q

theorem LinearMap.BilinMap.toQuadraticMap_surjective {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Free R M] : Function.Surjective LinearMap.BilinMap.toQuadraticMap

From a free module, every quadratic map can be built from a bilinear form.

See BilinMap.not_forall_toQuadraticMap_surjective for a counterexample when the module is not free.