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.

@[simp]

theorem QuadraticMap.add_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] (bm : Basis ι R M) (Q₁ Q₂ : QuadraticMap R M N) : (Q₁ + Q₂).toBilin bm = Q₁.toBilin bm + Q₂.toBilin bm

@[simp]

theorem QuadraticMap.smul_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] (S : Type u_5) [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] (bm : Basis ι R M) (s : S) (Q : QuadraticMap R M N) : (s • Q).toBilin bm = s • Q.toBilin bm

noncomputable def QuadraticMap.toBilinHom {ι : 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] (S : Type u_5) [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] (bm : Basis ι R M) : QuadraticMap R M N →ₗ[S] LinearMap.BilinMap R M N

QuadraticMap.toBilin as an S-linear map

Equations

• QuadraticMap.toBilinHom S bm = { toFun := fun (Q : QuadraticMap R M N) => Q.toBilin bm, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem QuadraticMap.toBilinHom_apply {ι : 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] (S : Type u_5) [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] (bm : Basis ι R M) (Q : QuadraticMap R M N) : (QuadraticMap.toBilinHom S bm) Q = Q.toBilin bm