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
Instances For
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₁ : QuadraticMap R M N)
(Q₂ : QuadraticMap R M N)
:
@[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)
:
@[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
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' := ⋯ }