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.

theorem QuadraticMap.map_finsuppSum' {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (f : ι →₀ R) (g : ι → R → M) : Q (f.sum g) = ∑ p ∈ f.support.sym2, polarSym2 (⇑Q) (Sym2.map (fun (i : ι) => g i (f i)) p) - f.sum fun (i : ι) (a : R) => Q (g i a)

theorem QuadraticMap.apply_linearCombination' {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) {g : ι → M} (l : ι →₀ R) : Q ((Finsupp.linearCombination R g) l) = (Finsupp.linearCombination R (polarSym2 ⇑Q ∘ Sym2.map g)) l.sym2Mul - (Finsupp.linearCombination R (⇑Q ∘ g)) (l * l)

theorem QuadraticMap.sum_polar_sub_repr_sq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (bm : Basis ι R M) (x : M) : (Finsupp.linearCombination R (polarSym2 ⇑Q ∘ Sym2.map ⇑bm)) (bm.repr x).sym2Mul - (Finsupp.linearCombination R (⇑Q ∘ ⇑bm)) (bm.repr x * bm.repr x) = Q x

theorem QuadraticMap.map_finsuppSum {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] (Q : QuadraticMap R M N) (f : ι →₀ R) (g : ι → R → M) : Q (f.sum g) = (f.sum fun (i : ι) (r : R) => Q (g i r)) + ∑ p ∈ {p ∈ f.support.sym2 | ¬p.IsDiag}, polarSym2 (⇑Q) (Sym2.map (fun (i : ι) => g i (f i)) p)

The quadratic version of _root_.map_finsupp_sum.

theorem QuadraticMap.apply_linearCombination {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] (Q : QuadraticMap R M N) {g : ι → M} (l : ι →₀ R) : Q ((Finsupp.linearCombination R g) l) = (Finsupp.linearCombination R (⇑Q ∘ g)) (l * l) + ∑ p ∈ {p ∈ l.support.sym2 | ¬p.IsDiag}, (Sym2.map (⇑l) p).mul • polarSym2 (⇑Q) (Sym2.map g p)

The quadratic version of Finsupp.apply_linearCombination.

theorem QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] (Q : QuadraticMap R M N) (bm : Basis ι R M) (x : M) : (Finsupp.linearCombination R (⇑Q ∘ ⇑bm)) (bm.repr x * bm.repr x) + ∑ p ∈ {p ∈ (bm.repr x).support.sym2 | ¬p.IsDiag}, (Sym2.map (⇑(bm.repr x)) p).mul • polarSym2 (⇑Q) (Sym2.map (⇑bm) p) = Q x

The quadratic version of LinearMap.sum_repr_mul_repr_mul.

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_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) (i j : ι) : ((Q.toBilin bm) (bm i)) (bm j) = if i = j then Q (bm i) else if i < j then polar (⇑Q) (bm i) (bm j) else 0

theorem QuadraticMap.toQuadraticMap_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) : (Q.toBilin bm).toQuadraticMap = Q

theorem LinearMap.BilinMap.toQuadraticMap_surjective {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Free R M] : Function.Surjective 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) : (toBilinHom S bm) Q = Q.toBilin bm