# Documentation

This file defines quadratic maps on an R-module M, taking values in an R-module N. An N-valued quadratic map on a module M over a commutative ring R is a map Q : M → N such that:

• QuadraticMap.map_smul: Q (a • x) = (a * a) • Q x
• QuadraticMap.polar_add_left, QuadraticMap.polar_add_right, QuadraticMap.polar_smul_left, QuadraticMap.polar_smul_right: the map QuadraticMap.polar Q := fun x y ↦ Q (x + y) - Q x - Q y is bilinear.

This notion generalizes to commutative semirings using the approach in [IKR16] which requires that there be a (possibly non-unique) companion bilinear map B such that ∀ x y, Q (x + y) = Q x + Q y + B x y. Over a ring, this B is precisely QuadraticMap.polar Q.

To build a QuadraticMap from the polar axioms, use QuadraticMap.ofPolar.

Quadratic maps come with a scalar multiplication, (a • Q) x = a • Q x, and composition with linear maps f, Q.comp f x = Q (f x).

## Main definitions #

• QuadraticMap.ofPolar: a more familiar constructor that works on rings
• QuadraticMap.associated: associated bilinear map
• QuadraticMap.PosDef: positive definite quadratic maps
• QuadraticMap.Anisotropic: anisotropic quadratic maps
• QuadraticMap.discr: discriminant of a quadratic map
• QuadraticMap.IsOrtho: orthogonality of vectors with respect to a quadratic map.

## Main statements #

• QuadraticMap.associated_left_inverse,
• QuadraticMap.associated_rightInverse: in a commutative ring where 2 has an inverse, there is a correspondence between quadratic maps and symmetric bilinear forms
• LinearMap.BilinForm.exists_orthogonal_basis: There exists an orthogonal basis with respect to any nondegenerate, symmetric bilinear map B.

## Notation #

In this file, the variable R is used when a CommSemiring structure is available.

The variable S is used when R itself has a • action.

## Implementation notes #

While the definition and many results make sense if we drop commutativity assumptions, the correct definition of a quadratic maps in the noncommutative setting would require substantial refactors from the current version, such that $Q(rm) = rQ(m)r^*$ for some suitable conjugation $r^*$.

The Zulip thread has some further discussion.

## Tags #

def QuadraticMap.polar {M : Type u_4} {N : Type u_5} [] [] (f : MN) (x : M) (y : M) :
N

Up to a factor 2, Q.polar is the associated bilinear map for a quadratic map Q.

Equations
• = f (x + y) - f x - f y
Instances For
theorem QuadraticMap.map_add {M : Type u_4} {N : Type u_5} [] [] (f : MN) (x : M) (y : M) :
f (x + y) = f x + f y +
theorem QuadraticMap.polar_add {M : Type u_4} {N : Type u_5} [] [] (f : MN) (g : MN) (x : M) (y : M) :
QuadraticMap.polar (f + g) x y = +
theorem QuadraticMap.polar_neg {M : Type u_4} {N : Type u_5} [] [] (f : MN) (x : M) (y : M) :
theorem QuadraticMap.polar_smul {S : Type u_1} {M : Type u_4} {N : Type u_5} [] [] [] [] (f : MN) (s : S) (x : M) (y : M) :
theorem QuadraticMap.polar_comm {M : Type u_4} {N : Type u_5} [] [] (f : MN) (x : M) (y : M) :
=
theorem QuadraticMap.polar_add_left_iff {M : Type u_4} {N : Type u_5} [] [] {f : MN} {x : M} {x' : M} {y : M} :
QuadraticMap.polar f (x + x') y = + f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)

Auxiliary lemma to express bilinearity of QuadraticMap.polar without subtraction.

theorem QuadraticMap.polar_comp {S : Type u_1} {M : Type u_4} {N : Type u_5} [] [] {F : Type u_8} [] [FunLike F N S] [] (f : MN) (g : F) (x : M) (y : M) :
structure QuadraticMap (R : Type u) (M : Type v) (N : Type w) [] [] [Module R M] [] [Module R N] :
Type (max v w)

A quadratic map on a module.

For a more familiar constructor when R is a ring, see QuadraticMap.ofPolar.

• toFun : MN
• toFun_smul : ∀ (a : R) (x : M), self.toFun (a x) = (a * a) self.toFun x
• exists_companion' : ∃ (B : ), ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y + (B x) y
Instances For
theorem QuadraticMap.toFun_smul {R : Type u} {M : Type v} {N : Type w} [] [] [Module R M] [] [Module R N] (self : QuadraticMap R M N) (a : R) (x : M) :
self.toFun (a x) = (a * a) self.toFun x
theorem QuadraticMap.exists_companion' {R : Type u} {M : Type v} {N : Type w} [] [] [Module R M] [] [Module R N] (self : QuadraticMap R M N) :
∃ (B : ), ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y + (B x) y
@[reducible, inline]
abbrev QuadraticForm (R : Type u) (M : Type v) [] [] [Module R M] :
Type (max u v)

A quadratic form on a module.

Equations
Instances For
instance QuadraticMap.instFunLike {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
FunLike (QuadraticMap R M N) M N
Equations
instance QuadraticMap.instCoeFunForall {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
CoeFun (QuadraticMap R M N) fun (x : QuadraticMap R M N) => MN

Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun directly.

Equations
• QuadraticMap.instCoeFunForall = { coe := DFunLike.coe }
@[simp]
theorem QuadraticMap.toFun_eq_coe {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) :
Q.toFun = Q

The simp normal form for a quadratic map is DFunLike.coe, not toFun.

theorem QuadraticMap.ext_iff {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} {Q' : QuadraticMap R M N} :
Q = Q' ∀ (x : M), Q x = Q' x
theorem QuadraticMap.ext {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} {Q' : QuadraticMap R M N} (H : ∀ (x : M), Q x = Q' x) :
Q = Q'
theorem QuadraticMap.congr_fun {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} {Q' : QuadraticMap R M N} (h : Q = Q') (x : M) :
Q x = Q' x
def QuadraticMap.copy {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (Q' : MN) (h : Q' = Q) :

Copy of a QuadraticMap with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• Q.copy Q' h = { toFun := Q', toFun_smul := , exists_companion' := }
Instances For
@[simp]
theorem QuadraticMap.coe_copy {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (Q' : MN) (h : Q' = Q) :
(Q.copy Q' h) = Q'
theorem QuadraticMap.copy_eq {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (Q' : MN) (h : Q' = Q) :
Q.copy Q' h = Q
theorem QuadraticMap.map_smul {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (a : R) (x : M) :
Q (a x) = (a * a) Q x
theorem QuadraticMap.exists_companion {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) :
∃ (B : ), ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
theorem QuadraticMap.map_add_add_add_map {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) (z : M) :
Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)
theorem QuadraticMap.map_add_self {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (x : M) :
Q (x + x) = 4 Q x
theorem QuadraticMap.map_zero {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) :
Q 0 = 0
instance QuadraticMap.zeroHomClass {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
Equations
• =
theorem QuadraticMap.map_smul_of_tower {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) [] [Algebra S R] [Module S M] [] [Module S N] [] (a : S) (x : M) :
Q (a x) = (a * a) Q x
@[simp]
theorem QuadraticMap.map_neg {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) :
Q (-x) = Q x
theorem QuadraticMap.map_sub {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) :
Q (x - y) = Q (y - x)
@[simp]
theorem QuadraticMap.polar_zero_left {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (y : M) :
QuadraticMap.polar (⇑Q) 0 y = 0
@[simp]
theorem QuadraticMap.polar_add_left {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (x' : M) (y : M) :
@[simp]
theorem QuadraticMap.polar_smul_left {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (a : R) (x : M) (y : M) :
@[simp]
theorem QuadraticMap.polar_neg_left {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) :
@[simp]
theorem QuadraticMap.polar_sub_left {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (x' : M) (y : M) :
@[simp]
theorem QuadraticMap.polar_zero_right {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (y : M) :
QuadraticMap.polar (⇑Q) y 0 = 0
@[simp]
theorem QuadraticMap.polar_add_right {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) (y' : M) :
@[simp]
theorem QuadraticMap.polar_smul_right {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (a : R) (x : M) (y : M) :
@[simp]
theorem QuadraticMap.polar_neg_right {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) :
@[simp]
theorem QuadraticMap.polar_sub_right {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) (y' : M) :
@[simp]
theorem QuadraticMap.polar_self {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) :
QuadraticMap.polar (⇑Q) x x = 2 Q x
@[simp]
theorem QuadraticMap.polarBilin_apply_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) (m : M) (y : M) :
(Q.polarBilin m) y = QuadraticMap.polar (⇑Q) m y
def QuadraticMap.polarBilin {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) :

QuadraticMap.polar as a bilinear map

Equations
Instances For
@[simp]
theorem QuadraticMap.polar_smul_left_of_tower {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) [] [Algebra S R] [Module S M] [] [Module S N] [] (a : S) (x : M) (y : M) :
@[simp]
theorem QuadraticMap.polar_smul_right_of_tower {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) [] [Algebra S R] [Module S M] [] [Module S N] [] (a : S) (x : M) (y : M) :
@[simp]
theorem QuadraticMap.ofPolar_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (toFun : MN) (toFun_smul : ∀ (a : R) (x : M), toFun (a x) = (a * a) toFun x) (polar_add_left : ∀ (x x' y : M), QuadraticMap.polar toFun (x + x') y = QuadraticMap.polar toFun x y + QuadraticMap.polar toFun x' y) (polar_smul_left : ∀ (a : R) (x y : M), QuadraticMap.polar toFun (a x) y = a QuadraticMap.polar toFun x y) :
∀ (a : M), (QuadraticMap.ofPolar toFun toFun_smul polar_add_left polar_smul_left) a = toFun a
def QuadraticMap.ofPolar {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (toFun : MN) (toFun_smul : ∀ (a : R) (x : M), toFun (a x) = (a * a) toFun x) (polar_add_left : ∀ (x x' y : M), QuadraticMap.polar toFun (x + x') y = QuadraticMap.polar toFun x y + QuadraticMap.polar toFun x' y) (polar_smul_left : ∀ (a : R) (x y : M), QuadraticMap.polar toFun (a x) y = a QuadraticMap.polar toFun x y) :

An alternative constructor to QuadraticMap.mk, for rings where polar can be used.

Equations
• QuadraticMap.ofPolar toFun toFun_smul polar_add_left polar_smul_left = { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := }
Instances For
theorem QuadraticMap.choose_exists_companion {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) :
.choose = Q.polarBilin

In a ring the companion bilinear form is unique and equal to QuadraticMap.polar.

theorem QuadraticMap.map_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] {ι : Type u_8} [] (Q : QuadraticMap R M N) (s : ) (f : ιM) :
Q (∑ is, f i) = is, Q (f i) + ijFinset.filter (fun (x : Sym2 ι) => ¬x.IsDiag) s.sym2, Sym2.lift fun (i j : ι) => QuadraticMap.polar (⇑Q) (f i) (f j), ij
theorem QuadraticMap.map_sum' {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] {ι : Type u_8} (Q : QuadraticMap R M N) (s : ) (f : ιM) :
Q (∑ is, f i) = ijs.sym2, Sym2.lift fun (i j : ι) => QuadraticMap.polar (⇑Q) (f i) (f j), ij - is, Q (f i)
instance QuadraticMap.instSMul {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [] [] :
SMul S (QuadraticMap R M N)

QuadraticMap R M N inherits the scalar action from any algebra over R.

This provides an R-action via Algebra.id.

Equations
• QuadraticMap.instSMul = { smul := fun (a : S) (Q : QuadraticMap R M N) => { toFun := a Q, toFun_smul := , exists_companion' := } }
@[simp]
theorem QuadraticMap.coeFn_smul {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [] [] (a : S) (Q : QuadraticMap R M N) :
(a Q) = a Q
@[simp]
theorem QuadraticMap.smul_apply {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [] [] (a : S) (Q : QuadraticMap R M N) (x : M) :
(a Q) x = a Q x
instance QuadraticMap.instSMulCommClass {S : Type u_1} {T : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [] [] [] [] [] [] :
Equations
• =
instance QuadraticMap.instIsScalarTower {S : Type u_1} {T : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [] [] [] [] [] [SMul S T] [] :
Equations
• =
instance QuadraticMap.instZero {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
Equations
• QuadraticMap.instZero = { zero := { toFun := fun (x : M) => 0, toFun_smul := , exists_companion' := } }
@[simp]
theorem QuadraticMap.coeFn_zero {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
0 = 0
@[simp]
theorem QuadraticMap.zero_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (x : M) :
0 x = 0
instance QuadraticMap.instInhabited {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
Equations
• QuadraticMap.instInhabited = { default := 0 }
instance QuadraticMap.instAdd {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
Equations
• QuadraticMap.instAdd = { add := fun (Q Q' : QuadraticMap R M N) => { toFun := Q + Q', toFun_smul := , exists_companion' := } }
@[simp]
theorem QuadraticMap.coeFn_add {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (Q' : QuadraticMap R M N) :
(Q + Q') = Q + Q'
@[simp]
theorem QuadraticMap.add_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (Q' : QuadraticMap R M N) (x : M) :
(Q + Q') x = Q x + Q' x
instance QuadraticMap.instAddCommMonoid {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
Equations
@[simp]
theorem QuadraticMap.coeFnAddMonoidHom_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
def QuadraticMap.coeFnAddMonoidHom {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
QuadraticMap R M N →+ MN

@CoeFn (QuadraticMap R M) as an AddMonoidHom.

This API mirrors AddMonoidHom.coeFn.

Equations
Instances For
@[simp]
theorem QuadraticMap.evalAddMonoidHom_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (m : M) :
∀ (a : QuadraticMap R M N), = a m
def QuadraticMap.evalAddMonoidHom {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (m : M) :

Evaluation on a particular element of the module M is an additive map on quadratic maps.

Equations
Instances For
@[simp]
theorem QuadraticMap.coeFn_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {ι : Type u_8} (Q : ιQuadraticMap R M N) (s : ) :
(∑ is, Q i) = is, (Q i)
@[simp]
theorem QuadraticMap.sum_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {ι : Type u_8} (Q : ιQuadraticMap R M N) (s : ) (x : M) :
(∑ is, Q i) x = is, (Q i) x
instance QuadraticMap.instDistribMulActionOfSMulCommClass {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [] [] :
Equations
instance QuadraticMap.instModuleOfSMulCommClass {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [Module S N] [] :
Equations
instance QuadraticMap.instNeg {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
Equations
• QuadraticMap.instNeg = { neg := fun (Q : QuadraticMap R M N) => { toFun := -Q, toFun_smul := , exists_companion' := } }
@[simp]
theorem QuadraticMap.coeFn_neg {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) :
(-Q) = -Q
@[simp]
theorem QuadraticMap.neg_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (x : M) :
(-Q) x = -Q x
instance QuadraticMap.instSub {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
Equations
• QuadraticMap.instSub = { sub := fun (Q Q' : QuadraticMap R M N) => (Q + -Q').copy (Q - Q') }
@[simp]
theorem QuadraticMap.coeFn_sub {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (Q' : QuadraticMap R M N) :
(Q - Q') = Q - Q'
@[simp]
theorem QuadraticMap.sub_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (Q' : QuadraticMap R M N) (x : M) :
(Q - Q') x = Q x - Q' x
instance QuadraticMap.instAddCommGroup {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] :
Equations
@[simp]
theorem QuadraticMap.restrictScalars_apply {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [] [Module R N] [Module S M] [Module S N] [Algebra S R] [] [] (Q : QuadraticMap R M N) (x : M) :
Q.restrictScalars x = Q x
def QuadraticMap.restrictScalars {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [] [Module R N] [Module S M] [Module S N] [Algebra S R] [] [] (Q : QuadraticMap R M N) :

If B : M → N → Pₗ is R-S bilinear and R' and S' are compatible scalar multiplications, then the restriction of scalars is a R'-S' bilinear map.

Equations
• Q.restrictScalars = { toFun := fun (x : M) => Q x, toFun_smul := , exists_companion' := }
Instances For
def QuadraticMap.comp {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [] [] [Module R M] [] [Module R N] [] [Module R P] (Q : QuadraticMap R N P) (f : M →ₗ[R] N) :

Compose the quadratic map with a linear function on the right.

Equations
• Q.comp f = { toFun := fun (x : M) => Q (f x), toFun_smul := , exists_companion' := }
Instances For
@[simp]
theorem QuadraticMap.comp_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [] [] [Module R M] [] [Module R N] [] [Module R P] (Q : QuadraticMap R N P) (f : M →ₗ[R] N) (x : M) :
(Q.comp f) x = Q (f x)
@[simp]
theorem LinearMap.compQuadraticMap_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [] [] [Module R M] [] [Module R N] [] [Module R P] (f : N →ₗ[R] P) (Q : QuadraticMap R M N) (x : M) :
(f.compQuadraticMap Q) x = f (Q x)
def LinearMap.compQuadraticMap {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [] [] [Module R M] [] [Module R N] [] [Module R P] (f : N →ₗ[R] P) (Q : QuadraticMap R M N) :

Compose a quadratic map with a linear function on the left.

Equations
• f.compQuadraticMap Q = { toFun := fun (x : M) => f (Q x), toFun_smul := , exists_companion' := }
Instances For
@[simp]
theorem LinearMap.compQuadraticMap'_apply {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [] [] [Module R M] [] [Module R N] [] [] [Algebra S R] [Module S N] [Module S M] [] [] [Module S P] (f : N →ₗ[S] P) (Q : QuadraticMap R M N) (x : M) :
(f.compQuadraticMap' Q) x = f (Q x)
def LinearMap.compQuadraticMap' {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [] [] [Module R M] [] [Module R N] [] [] [Algebra S R] [Module S N] [Module S M] [] [] [Module S P] (f : N →ₗ[S] P) (Q : QuadraticMap R M N) :

Compose a quadratic map with a linear function on the left.

Equations
Instances For
def QuadraticMap.linMulLin {R : Type u_3} {M : Type u_4} {A : Type u_7} [] [] [Module R M] [Module R A] [] [] (f : M →ₗ[R] A) (g : M →ₗ[R] A) :

The product of linear forms is a quadratic form.

Equations
• = { toFun := f * g, toFun_smul := , exists_companion' := }
Instances For
@[simp]
theorem QuadraticMap.linMulLin_apply {R : Type u_3} {M : Type u_4} {A : Type u_7} [] [] [Module R M] [Module R A] [] [] (f : M →ₗ[R] A) (g : M →ₗ[R] A) (x : M) :
x = f x * g x
@[simp]
theorem QuadraticMap.add_linMulLin {R : Type u_3} {M : Type u_4} {A : Type u_7} [] [] [Module R M] [Module R A] [] [] (f : M →ₗ[R] A) (g : M →ₗ[R] A) (h : M →ₗ[R] A) :
@[simp]
theorem QuadraticMap.linMulLin_add {R : Type u_3} {M : Type u_4} {A : Type u_7} [] [] [Module R M] [Module R A] [] [] (f : M →ₗ[R] A) (g : M →ₗ[R] A) (h : M →ₗ[R] A) :
@[simp]
theorem QuadraticMap.linMulLin_comp {R : Type u_3} {M : Type u_4} {A : Type u_7} [] [] [Module R M] [Module R A] [] [] {N' : Type u_8} [] [Module R N'] (f : M →ₗ[R] A) (g : M →ₗ[R] A) (h : N' →ₗ[R] M) :
.comp h = QuadraticMap.linMulLin (f ∘ₗ h) (g ∘ₗ h)
@[simp]
theorem QuadraticMap.sq_apply {R : Type u_3} {A : Type u_7} [] [Module R A] [] [] (a : A) :
QuadraticMap.sq a = a * a
def QuadraticMap.sq {R : Type u_3} {A : Type u_7} [] [Module R A] [] [] :

sq is the quadratic form mapping the vector x : A to x * x

Equations
Instances For
def QuadraticMap.proj {R : Type u_3} {A : Type u_7} [] [Module R A] [] [] {n : Type u_9} (i : n) (j : n) :

proj i j is the quadratic form mapping the vector x : n → R to x i * x j

Equations
Instances For
@[simp]
theorem QuadraticMap.proj_apply {R : Type u_3} {A : Type u_7} [] [Module R A] [] [] {n : Type u_9} (i : n) (j : n) (x : nA) :
x = x i * x j

### Associated bilinear maps #

Over a commutative ring with an inverse of 2, the theory of quadratic maps is basically identical to that of symmetric bilinear maps. The map from quadratic maps to bilinear maps giving this identification is called the QuadraticMap.associated quadratic map.

def LinearMap.BilinMap.toQuadraticMap {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (B : ) :

A bilinear map gives a quadratic map by applying the argument twice.

Equations
• B.toQuadraticMap = { toFun := fun (x : M) => (B x) x, toFun_smul := , exists_companion' := }
Instances For
@[simp]
theorem LinearMap.BilinMap.toQuadraticMap_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (B : ) (x : M) :
B.toQuadraticMap x = (B x) x
theorem LinearMap.BilinMap.toQuadraticMap_comp_same {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {N' : Type u_8} [] [Module R N'] (B : ) (f : N' →ₗ[R] M) :
@[simp]
theorem LinearMap.BilinMap.toQuadraticMap_zero (R : Type u_3) (M : Type u_4) {N : Type u_5} [] [] [Module R M] [] [Module R N] :
@[simp]
theorem LinearMap.BilinMap.toQuadraticMap_add {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (B₁ : ) (B₂ : ) :
@[simp]
theorem LinearMap.BilinMap.toQuadraticMap_smul {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [] [] [] (a : S) (B : ) :
@[simp]
theorem LinearMap.BilinMap.toQuadraticMapAddMonoidHom_apply (R : Type u_3) (M : Type u_4) {N : Type u_5} [] [] [Module R M] [] [Module R N] (B : ) :
def LinearMap.BilinMap.toQuadraticMapAddMonoidHom (R : Type u_3) (M : Type u_4) {N : Type u_5} [] [] [Module R M] [] [Module R N] :

LinearMap.BilinForm.toQuadraticMap as an additive homomorphism

Equations
• = { toFun := LinearMap.BilinMap.toQuadraticMap, map_zero' := , map_add' := }
Instances For
@[simp]
theorem LinearMap.BilinMap.toQuadraticMapLinearMap_apply_apply (S : Type u_1) (R : Type u_3) (M : Type u_4) {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [Module S N] [] [] (B : ) (x : M) :
( B) x = (B x) x
def LinearMap.BilinMap.toQuadraticMapLinearMap (S : Type u_1) (R : Type u_3) (M : Type u_4) {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [Module S N] [] [] :

LinearMap.BilinForm.toQuadraticMap as a linear map

Equations
• = { toFun := LinearMap.BilinMap.toQuadraticMap, map_add' := , map_smul' := }
Instances For
@[simp]
theorem LinearMap.BilinMap.toQuadraticMap_list_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (B : List (LinearMap.BilinMap R M N)) :
@[simp]
theorem LinearMap.BilinMap.toQuadraticMap_multiset_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (B : Multiset (LinearMap.BilinMap R M N)) :
@[simp]
theorem LinearMap.BilinMap.toQuadraticMap_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {ι : Type u_9} (s : ) (B : ι) :
@[simp]
theorem LinearMap.BilinMap.toQuadraticMap_eq_zero {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {B : } :
@[simp]
theorem LinearMap.BilinMap.toQuadraticMap_neg {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (B : ) :
@[simp]
theorem LinearMap.BilinMap.toQuadraticMap_sub {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (B₁ : ) (B₂ : ) :
theorem LinearMap.BilinMap.polar_toQuadraticMap {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] {B : } (x : M) (y : M) :
QuadraticMap.polar (⇑B.toQuadraticMap) x y = (B x) y + (B y) x
theorem LinearMap.BilinMap.polarBilin_toQuadraticMap {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] {B : } :
@[simp]
theorem QuadraticMap.toQuadraticMap_polarBilin {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) :
theorem QuadraticMap.polarBilin_injective {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (h : ) :
theorem QuadraticMap.polarBilin_comp {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] {N' : Type u_8} [] [Module R N'] (Q : QuadraticMap R N' N) (f : M →ₗ[R] N') :
(Q.comp f).polarBilin = LinearMap.compl₁₂ Q.polarBilin f f
theorem LinearMap.compQuadraticMap_polar {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] {N' : Type u_8} [] [] [Algebra S R] [Module S N] [Module S N'] [] [Module S M] [] (f : N →ₗ[S] N') (Q : QuadraticMap R M N) (x : M) (y : M) :
theorem LinearMap.compQuadraticMap_polarBilin {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] {N' : Type u_8} [] [Module R N'] (f : N →ₗ[R] N') (Q : QuadraticMap R M N) :
(f.compQuadraticMap' Q).polarBilin = LinearMap.compr₂ Q.polarBilin f
def QuadraticMap.associatedHom (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [Algebra S R] [Module S N] [] [] :

associatedHom is the map that sends a quadratic map on a module M over R to its associated symmetric bilinear map. As provided here, this has the structure of an S-linear map where S is a commutative subring of R.

Over a commutative ring, use QuadraticMap.associated, which gives an R-linear map. Over a general ring with no nontrivial distinguished commutative subring, use QuadraticMap.associated', which gives an additive homomorphism (or more precisely a ℤ-linear map.)

Equations
• = 2, { toFun := QuadraticMap.polarBilin, map_add' := , map_smul' := }
Instances For
@[simp]
theorem QuadraticMap.associated_apply (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [Algebra S R] [Module S N] [] [] (Q : QuadraticMap R M N) (x : M) (y : M) :
(( Q) x) y = 2 (Q (x + y) - Q x - Q y)
@[simp]
theorem QuadraticMap.two_nsmul_associated (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [Algebra S R] [Module S N] [] [] (Q : QuadraticMap R M N) :
2 = Q.polarBilin
theorem QuadraticMap.associated_isSymm (S : Type u_1) {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] [Algebra S R] [] (Q : QuadraticMap R M R) :
@[simp]
theorem QuadraticMap.associated_comp (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [Algebra S R] [Module S N] [] [] (Q : QuadraticMap R M N) {N' : Type u_8} [] [Module R N'] (f : N' →ₗ[R] M) :
(Q.comp f) =
theorem QuadraticMap.associated_toQuadraticMap (S : Type u_1) {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] [Algebra S R] [] (B : ) (x : M) (y : M) :
(( B.toQuadraticMap) x) y = 2 ((B x) y + (B y) x)
theorem QuadraticMap.associated_left_inverse (S : Type u_1) {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] [Algebra S R] [] {B₁ : } (h : ) :
theorem QuadraticMap.associated_eq_self_apply (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [Algebra S R] [Module S N] [] [] (Q : QuadraticMap R M N) (x : M) :
(( Q) x) x = Q x
theorem QuadraticMap.toQuadraticMap_associated (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] [Algebra S R] [Module S N] [] [] (Q : QuadraticMap R M N) :
theorem QuadraticMap.associated_rightInverse (S : Type u_1) {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] [Algebra S R] [] :
@[reducible, inline]
abbrev QuadraticMap.associated' {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] :

associated' is the ℤ-linear map that sends a quadratic form on a module M over R to its associated symmetric bilinear form.

Equations
Instances For
instance QuadraticMap.canLift {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] :
CanLift (LinearMap.BilinMap R M R) (QuadraticForm R M) LinearMap.IsSymm

Symmetric bilinear forms can be lifted to quadratic forms

Equations
• =
theorem QuadraticMap.exists_quadraticForm_ne_zero {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] {Q : } (hB₁ : QuadraticMap.associated' Q 0) :
∃ (x : M), Q x 0

There exists a non-null vector with respect to any quadratic form Q whose associated bilinear form is non-zero, i.e. there exists x such that Q x ≠ 0.

@[reducible, inline]
abbrev QuadraticMap.associated {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] :

associated is the linear map that sends a quadratic map over a commutative ring to its associated symmetric bilinear map.

Equations
Instances For
theorem QuadraticMap.coe_associatedHom (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Algebra S R] [Module R M] [] [Module R N] [Module S N] [] [] :
@[simp]
theorem QuadraticMap.associated_linMulLin {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] (f : M →ₗ[R] R) (g : M →ₗ[R] R) :
QuadraticMap.associated = 2 ((LinearMap.mul R R).compl₁₂ f g + (LinearMap.mul R R).compl₁₂ g f)
@[simp]
theorem QuadraticMap.associated_sq {R : Type u_3} [] [] :

### Orthogonality #

def QuadraticMap.IsOrtho {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) :

The proposition that two elements of a quadratic map space are orthogonal.

Equations
• Q.IsOrtho x y = (Q (x + y) = Q x + Q y)
Instances For
theorem QuadraticMap.isOrtho_def {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} {x : M} {y : M} :
Q.IsOrtho x y Q (x + y) = Q x + Q y
theorem QuadraticMap.IsOrtho.all {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (x : M) (y : M) :
theorem QuadraticMap.IsOrtho.zero_left {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} (x : M) :
Q.IsOrtho 0 x
theorem QuadraticMap.IsOrtho.zero_right {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} (x : M) :
Q.IsOrtho x 0
theorem QuadraticMap.ne_zero_of_not_isOrtho_self {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} (x : M) (hx₁ : ¬Q.IsOrtho x x) :
x 0
theorem QuadraticMap.isOrtho_comm {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} {x : M} {y : M} :
Q.IsOrtho x y Q.IsOrtho y x
theorem QuadraticMap.IsOrtho.symm {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} {x : M} {y : M} :
Q.IsOrtho x yQ.IsOrtho y x

Alias of the forward direction of QuadraticMap.isOrtho_comm.

theorem LinearMap.BilinForm.toQuadraticMap_isOrtho {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] [] [] {B : } {x : M} {y : M} (h : ) :
@[simp]
theorem QuadraticMap.isOrtho_polarBilin {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} {x : M} {y : M} :
LinearMap.IsOrtho Q.polarBilin x y Q.IsOrtho x y
theorem QuadraticMap.IsOrtho.polar_eq_zero {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} {x : M} {y : M} (h : Q.IsOrtho x y) :
QuadraticMap.polar (⇑Q) x y = 0
@[simp]
theorem QuadraticMap.associated_isOrtho {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {Q : QuadraticMap R M N} [] {x : M} {y : M} :
LinearMap.IsOrtho (QuadraticMap.associated Q) x y Q.IsOrtho x y
def QuadraticMap.Anisotropic {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) :

An anisotropic quadratic map is zero only on zero vectors.

Equations
• Q.Anisotropic = ∀ (x : M), Q x = 0x = 0
Instances For
theorem QuadraticMap.not_anisotropic_iff_exists {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] (Q : QuadraticMap R M N) :
¬Q.Anisotropic ∃ (x : M), x 0 Q x = 0
theorem QuadraticMap.Anisotropic.eq_zero_iff {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [Module R M] [Module R N] {Q : QuadraticMap R M N} (h : Q.Anisotropic) {x : M} :
Q x = 0 x = 0
theorem QuadraticMap.separatingLeft_of_anisotropic {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] (Q : QuadraticMap R M R) (hB : Q.Anisotropic) :

The associated bilinear form of an anisotropic quadratic form is nondegenerate.

def QuadraticMap.PosDef {M : Type u_4} {N : Type u_5} {R₂ : Type u} [] [] [Module R₂ M] [] [] [Module R₂ N] (Q₂ : QuadraticMap R₂ M N) :

A positive definite quadratic form is positive on nonzero vectors.

Equations
• Q₂.PosDef = ∀ (x : M), x 00 < Q₂ x
Instances For
theorem QuadraticMap.PosDef.smul {M : Type u_4} {N : Type u_5} [] [] [] {R : Type u_8} [Module R M] [Module R N] [] {Q : QuadraticMap R M N} (h : Q.PosDef) {a : R} (a_pos : 0 < a) :
(a Q).PosDef
theorem QuadraticMap.PosDef.nonneg {M : Type u_4} {N : Type u_5} {R₂ : Type u} [] [] [Module R₂ M] [] [] [Module R₂ N] {Q : QuadraticMap R₂ M N} (hQ : Q.PosDef) (x : M) :
0 Q x
theorem QuadraticMap.PosDef.anisotropic {M : Type u_4} {N : Type u_5} {R₂ : Type u} [] [] [Module R₂ M] [] [] [Module R₂ N] {Q : QuadraticMap R₂ M N} (hQ : Q.PosDef) :
Q.Anisotropic
theorem QuadraticMap.posDef_of_nonneg {M : Type u_4} {N : Type u_5} {R₂ : Type u} [] [] [Module R₂ M] [] [] [Module R₂ N] {Q : QuadraticMap R₂ M N} (h : ∀ (x : M), 0 Q x) (h0 : Q.Anisotropic) :
Q.PosDef
theorem QuadraticMap.posDef_iff_nonneg {M : Type u_4} {N : Type u_5} {R₂ : Type u} [] [] [Module R₂ M] [] [] [Module R₂ N] {Q : QuadraticMap R₂ M N} :
Q.PosDef (∀ (x : M), 0 Q x) Q.Anisotropic
theorem QuadraticMap.PosDef.add {M : Type u_4} {N : Type u_5} {R₂ : Type u} [] [] [Module R₂ M] [] [] [Module R₂ N] [CovariantClass N N (fun (x1 x2 : N) => x1 + x2) fun (x1 x2 : N) => x1 < x2] (Q : QuadraticMap R₂ M N) (Q' : QuadraticMap R₂ M N) (hQ : Q.PosDef) (hQ' : Q'.PosDef) :
(Q + Q').PosDef
theorem QuadraticMap.linMulLinSelfPosDef {M : Type u_4} {A : Type u_7} [] {R : Type u_9} [Module R M] [] [Module R A] [] [] (f : M →ₗ[R] A) (hf : ) :
.PosDef

### Quadratic forms and matrices #

Connect quadratic forms and matrices, in order to explicitly compute with them. The convention is twos out, so there might be a factor 2⁻¹ in the entries of the matrix. The determinant of the matrix is the discriminant of the quadratic form.

def Matrix.toQuadraticMap' {R : Type u_3} {n : Type w} [] [] [] (M : Matrix n n R) :

M.toQuadraticMap' is the map fun x ↦ row x * M * col x as a quadratic form.

Equations
Instances For
def QuadraticMap.toMatrix' {R : Type u_3} {n : Type w} [] [] [] [] (Q : QuadraticMap R (nR) R) :
Matrix n n R

A matrix representation of the quadratic form.

Equations
Instances For
theorem QuadraticMap.toMatrix'_smul {R : Type u_3} {n : Type w} [] [] [] [] (a : R) (Q : QuadraticMap R (nR) R) :
(a Q).toMatrix' = a Q.toMatrix'
theorem QuadraticMap.isSymm_toMatrix' {R : Type u_3} {n : Type w} [] [] [] [] (Q : QuadraticMap R (nR) R) :
Q.toMatrix'.IsSymm
@[simp]
theorem QuadraticMap.toMatrix'_comp {R : Type u_3} {n : Type w} [] [] [] [] {m : Type w} [] [] (Q : QuadraticMap R (mR) R) (f : (nR) →ₗ[R] mR) :
(Q.comp f).toMatrix' = (LinearMap.toMatrix' f).transpose * Q.toMatrix' * LinearMap.toMatrix' f
def QuadraticMap.discr {R : Type u_3} {n : Type w} [] [] [] [] (Q : QuadraticMap R (nR) R) :
R

The discriminant of a quadratic form generalizes the discriminant of a quadratic polynomial.

Equations
• Q.discr = Q.toMatrix'.det
Instances For
theorem QuadraticMap.discr_smul {R : Type u_3} {n : Type w} [] [] [] [] {Q : QuadraticMap R (nR) R} (a : R) :
(a Q).discr = * Q.discr
theorem QuadraticMap.discr_comp {R : Type u_3} {n : Type w} [] [] [] [] {Q : QuadraticMap R (nR) R} (f : (nR) →ₗ[R] nR) :
(Q.comp f).discr = (LinearMap.toMatrix' f).det * (LinearMap.toMatrix' f).det * Q.discr
theorem LinearMap.BilinForm.separatingLeft_of_anisotropic {R : Type u_3} {M : Type u_4} [] [] [Module R M] {B : } (hB : .Anisotropic) :

A bilinear form is separating left if the quadratic form it is associated with is anisotropic.

theorem LinearMap.BilinForm.exists_bilinForm_self_ne_zero {R : Type u_3} {M : Type u_4} [] [] [Module R M] [htwo : ] {B : } (hB₁ : B 0) (hB₂ : ) :
∃ (x : M), ¬

There exists a non-null vector with respect to any symmetric, nonzero bilinear form B on a module M over a ring R with invertible 2, i.e. there exists some x : M such that B x x ≠ 0.

theorem LinearMap.BilinForm.exists_orthogonal_basis {V : Type u} {K : Type v} [] [] [Module K V] [] [hK : ] {B : } (hB₂ : ) :
∃ (v : Basis (Fin ) K V),

Given a symmetric bilinear form B on some vector space V over a field K in which 2 is invertible, there exists an orthogonal basis with respect to B.

noncomputable def QuadraticMap.basisRepr {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {ι : Type u_8} [] (Q : QuadraticMap R M N) (v : Basis ι R M) :

Given a quadratic map Q and a basis, basisRepr is the basis representation of Q.

Equations
• Q.basisRepr v = Q.comp v.equivFun.symm
Instances For
@[simp]
theorem QuadraticMap.basisRepr_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] {ι : Type u_8} [] {v : Basis ι R M} (Q : QuadraticMap R M N) (w : ιR) :
(Q.basisRepr v) w = Q (∑ i : ι, w i v i)
def QuadraticMap.weightedSumSquares {S : Type u_1} (R : Type u_3) [] {ι : Type u_8} [] [] [] [] (w : ιS) :

The weighted sum of squares with respect to some weight as a quadratic form.

The weights are applied using •; typically this definition is used either with S = R or [Algebra S R], although this is stated more generally.

Equations
• = i : ι, w i
Instances For
@[simp]
theorem QuadraticMap.weightedSumSquares_apply {S : Type u_1} {R : Type u_3} [] {ι : Type u_8} [] [] [] [] (w : ιS) (v : ιR) :
= i : ι, w i (v i * v i)
theorem QuadraticMap.basisRepr_eq_of_iIsOrtho {ι : Type u_8} [] {R : Type u_9} {M : Type u_10} [] [] [Module R M] [] (Q : QuadraticMap R M R) (v : Basis ι R M) (hv₂ : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) v) :
Q.basisRepr v = QuadraticMap.weightedSumSquares R fun (i : ι) => Q (v i)

On an orthogonal basis, the basis representation of Q is just a sum of squares.