Quadratic maps

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 discusion.

References

• https://en.wikipedia.org/wiki/Quadratic_form
• https://en.wikipedia.org/wiki/Discriminant#Quadratic_forms

Tags

quadratic map, homogeneous polynomial, quadratic polynomial

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

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

Source of this name: https://en.wikipedia.org/wiki/Quadratic_form#Generalization

Equations

• QuadraticMap.polar f x y = f (x + y) - f x - f y

theorem QuadraticMap.map_add {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : M → N) (x : M) (y : M) : f (x + y) = f x + f y + QuadraticMap.polar f x y

theorem QuadraticMap.polar_add {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : M → N) (g : M → N) (x : M) (y : M) : QuadraticMap.polar (f + g) x y = QuadraticMap.polar f x y + QuadraticMap.polar g x y

theorem QuadraticMap.polar_neg {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : M → N) (x : M) (y : M) : QuadraticMap.polar (-f) x y = -QuadraticMap.polar f x y

theorem QuadraticMap.polar_smul {S : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [Monoid S] [DistribMulAction S N] (f : M → N) (s : S) (x : M) (y : M) : QuadraticMap.polar (s • f) x y = s • QuadraticMap.polar f x y

theorem QuadraticMap.polar_comm {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : M → N) (x : M) (y : M) : QuadraticMap.polar f x y = QuadraticMap.polar f y x

theorem QuadraticMap.polar_add_left_iff {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] {f : M → N} {x : M} {x' : M} {y : M} : QuadraticMap.polar f (x + x') y = QuadraticMap.polar f x y + QuadraticMap.polar f 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} [AddCommGroup M] [AddCommGroup N] {F : Type u_8} [CommRing S] [FunLike F N S] [AddMonoidHomClass F N S] (f : M → N) (g : F) (x : M) (y : M) : QuadraticMap.polar (⇑g ∘ f) x y = g (QuadraticMap.polar f x y)

structure QuadraticMap (R : Type u) (M : Type v) (N : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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 : M → N
• toFun_smul : ∀ (a : R) (x : M), self.toFun (a • x) = (a * a) • self.toFun x
• exists_companion' : ∃ (B : LinearMap.BilinMap R M N), ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y + (B x) y

theorem QuadraticMap.toFun_smul {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (self : QuadraticMap R M N) : ∃ (B : LinearMap.BilinMap R M N), ∀ (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) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max u v)

A quadratic form on a module.

Equations

• QuadraticForm R M = QuadraticMap R M R

instance QuadraticMap.instFunLike {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : FunLike (QuadraticMap R M N) M N

Equations

• QuadraticMap.instFunLike = { coe := QuadraticMap.toFun, coe_injective' := ⋯ }

instance QuadraticMap.instCoeFunForall {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : CoeFun (QuadraticMap R M N) fun (x : QuadraticMap R M N) => M → N

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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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 {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {Q' : QuadraticMap R M N} (h : Q = Q') (x : M) : Q x = Q' x

theorem QuadraticMap.ext_iff {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {Q' : QuadraticMap R M N} : Q = Q' ↔ ∀ (x : M), Q x = Q' x

def QuadraticMap.copy {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (Q' : M → N) (h : Q' = ⇑Q) : QuadraticMap R M N

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' := ⋯ }

@[simp]

theorem QuadraticMap.coe_copy {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (Q' : M → N) (h : Q' = ⇑Q) : ⇑(Q.copy Q' h) = Q'

theorem QuadraticMap.copy_eq {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (Q' : M → N) (h : Q' = ⇑Q) : Q.copy Q' h = Q

theorem QuadraticMap.map_smul {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : ∃ (B : LinearMap.BilinMap R M N), ∀ (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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : ZeroHomClass (QuadraticMap R M N) M N

Equations

• ⋯ = ⋯

theorem QuadraticMap.map_smul_of_tower {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] [Module S N] [IsScalarTower S R 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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (x' : M) (y : M) : QuadraticMap.polar (⇑Q) (x + x') y = QuadraticMap.polar (⇑Q) x y + QuadraticMap.polar (⇑Q) x' y

@[simp]

theorem QuadraticMap.polar_smul_left {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (a : R) (x : M) (y : M) : QuadraticMap.polar (⇑Q) (a • x) y = a • QuadraticMap.polar (⇑Q) x y

@[simp]

theorem QuadraticMap.polar_neg_left {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) : QuadraticMap.polar (⇑Q) (-x) y = -QuadraticMap.polar (⇑Q) x y

@[simp]

theorem QuadraticMap.polar_sub_left {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (x' : M) (y : M) : QuadraticMap.polar (⇑Q) (x - x') y = QuadraticMap.polar (⇑Q) x y - QuadraticMap.polar (⇑Q) x' y

@[simp]

theorem QuadraticMap.polar_zero_right {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) (y' : M) : QuadraticMap.polar (⇑Q) x (y + y') = QuadraticMap.polar (⇑Q) x y + QuadraticMap.polar (⇑Q) x y'

@[simp]

theorem QuadraticMap.polar_smul_right {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (a : R) (x : M) (y : M) : QuadraticMap.polar (⇑Q) x (a • y) = a • QuadraticMap.polar (⇑Q) x y

@[simp]

theorem QuadraticMap.polar_neg_right {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) : QuadraticMap.polar (⇑Q) x (-y) = -QuadraticMap.polar (⇑Q) x y

@[simp]

theorem QuadraticMap.polar_sub_right {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) (y : M) (y' : M) : QuadraticMap.polar (⇑Q) x (y - y') = QuadraticMap.polar (⇑Q) x y - QuadraticMap.polar (⇑Q) x y'

@[simp]

theorem QuadraticMap.polar_self {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) : LinearMap.BilinMap R M N

QuadraticMap.polar as a bilinear map

Equations

• Q.polarBilin = LinearMap.mk₂ R (QuadraticMap.polar ⇑Q) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem QuadraticMap.polar_smul_left_of_tower {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] [Module S N] [IsScalarTower S R N] (a : S) (x : M) (y : M) : QuadraticMap.polar (⇑Q) (a • x) y = a • QuadraticMap.polar (⇑Q) x y

@[simp]

theorem QuadraticMap.polar_smul_right_of_tower {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] [Module S N] [IsScalarTower S R N] (a : S) (x : M) (y : M) : QuadraticMap.polar (⇑Q) x (a • y) = a • QuadraticMap.polar (⇑Q) x y

@[simp]

theorem QuadraticMap.ofPolar_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (toFun : M → N) (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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (toFun : M → N) (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) : QuadraticMap R M N

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' := ⋯ }

theorem QuadraticMap.choose_exists_companion {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_8} [DecidableEq ι] (Q : QuadraticMap R M N) (s : Finset ι) (f : ι → M) : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_8} (Q : QuadraticMap R M N) (s : Finset ι) (f : ι → M) : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, Sym2.lift ⟨fun (i j : ι) => QuadraticMap.polar (⇑Q) (f i) (f j), ⋯⟩ ij - ∑ i ∈ s, Q (f i)

instance QuadraticMap.instSMul {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Monoid S] [DistribMulAction S N] [SMulCommClass S 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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Monoid S] [DistribMulAction S N] [SMulCommClass S 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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Monoid S] [DistribMulAction S N] [SMulCommClass S 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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Monoid S] [Monoid T] [DistribMulAction S N] [DistribMulAction T N] [SMulCommClass S R N] [SMulCommClass T R N] [SMulCommClass S T N] : SMulCommClass S T (QuadraticMap R M 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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Monoid S] [Monoid T] [DistribMulAction S N] [DistribMulAction T N] [SMulCommClass S R N] [SMulCommClass T R N] [SMul S T] [IsScalarTower S T N] : IsScalarTower S T (QuadraticMap R M N)

Equations

• ⋯ = ⋯

instance QuadraticMap.instZero {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : Zero (QuadraticMap R M 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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : ⇑0 = 0

@[simp]

theorem QuadraticMap.zero_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (x : M) : 0 x = 0

instance QuadraticMap.instInhabited {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : Inhabited (QuadraticMap R M N)

Equations

• QuadraticMap.instInhabited = { default := 0 }

instance QuadraticMap.instAdd {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : Add (QuadraticMap R M 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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : AddCommMonoid (QuadraticMap R M N)

Equations

• QuadraticMap.instAddCommMonoid = Function.Injective.addCommMonoid (fun (f : QuadraticMap R M N) => ⇑f) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem QuadraticMap.coeFnAddMonoidHom_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : ∀ (a : QuadraticMap R M N) (a_1 : M), QuadraticMap.coeFnAddMonoidHom a a_1 = a a_1

def QuadraticMap.coeFnAddMonoidHom {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : QuadraticMap R M N →+ M → N

@CoeFn (QuadraticMap R M) as an AddMonoidHom.

This API mirrors AddMonoidHom.coeFn.

Equations

• QuadraticMap.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem QuadraticMap.evalAddMonoidHom_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) : ∀ (a : QuadraticMap R M N), (QuadraticMap.evalAddMonoidHom m) a = a m

def QuadraticMap.evalAddMonoidHom {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) : QuadraticMap R M N →+ N

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

Equations

• QuadraticMap.evalAddMonoidHom m = (Pi.evalAddMonoidHom (fun (a : M) => N) m).comp QuadraticMap.coeFnAddMonoidHom

@[simp]

theorem QuadraticMap.coeFn_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_8} (Q : ι → QuadraticMap R M N) (s : Finset ι) : ⇑(∑ i ∈ s, Q i) = ∑ i ∈ s, ⇑(Q i)

@[simp]

theorem QuadraticMap.sum_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_8} (Q : ι → QuadraticMap R M N) (s : Finset ι) (x : M) : (∑ i ∈ s, Q i) x = ∑ i ∈ s, (Q i) x

instance QuadraticMap.instDistribMulActionOfSMulCommClass {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Monoid S] [DistribMulAction S N] [SMulCommClass S R N] : DistribMulAction S (QuadraticMap R M N)

Equations

• QuadraticMap.instDistribMulActionOfSMulCommClass = DistribMulAction.mk ⋯ ⋯

instance QuadraticMap.instModuleOfSMulCommClass {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass S R N] : Module S (QuadraticMap R M N)

Equations

• QuadraticMap.instModuleOfSMulCommClass = Module.mk ⋯ ⋯

instance QuadraticMap.instNeg {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : Neg (QuadraticMap R M 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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : Sub (QuadraticMap R M 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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : AddCommGroup (QuadraticMap R M N)

Equations

• QuadraticMap.instAddCommGroup = Function.Injective.addCommGroup (fun (f : QuadraticMap R M N) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem QuadraticMap.restrictScalars_apply {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S M] [Module S N] [Algebra S R] [IsScalarTower S R M] [IsScalarTower S R N] (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} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S M] [Module S N] [Algebra S R] [IsScalarTower S R M] [IsScalarTower S R N] (Q : QuadraticMap R M N) : QuadraticMap S 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' := ⋯ }

def QuadraticMap.comp {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (Q : QuadraticMap R N P) (f : M →ₗ[R] N) : QuadraticMap R M P

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' := ⋯ }

@[simp]

theorem QuadraticMap.comp_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : N →ₗ[R] P) (Q : QuadraticMap R M N) : QuadraticMap R M P

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' := ⋯ }

@[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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [CommSemiring S] [Algebra S R] [Module S N] [Module S M] [IsScalarTower S R N] [IsScalarTower S R 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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [CommSemiring S] [Algebra S R] [Module S N] [Module S M] [IsScalarTower S R N] [IsScalarTower S R M] [Module S P] (f : N →ₗ[S] P) (Q : QuadraticMap R M N) : QuadraticMap S M P

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

Equations

• f.compQuadraticMap' Q = f.compQuadraticMap Q.restrictScalars

def QuadraticMap.linMulLin {R : Type u_3} {M : Type u_4} {A : Type u_7} [CommSemiring R] [NonUnitalNonAssocSemiring A] [AddCommMonoid M] [Module R M] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (f : M →ₗ[R] A) (g : M →ₗ[R] A) : QuadraticMap R M A

The product of linear forms is a quadratic form.

Equations

• QuadraticMap.linMulLin f g = { toFun := ⇑f * ⇑g, toFun_smul := ⋯, exists_companion' := ⋯ }

@[simp]

theorem QuadraticMap.linMulLin_apply {R : Type u_3} {M : Type u_4} {A : Type u_7} [CommSemiring R] [NonUnitalNonAssocSemiring A] [AddCommMonoid M] [Module R M] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (f : M →ₗ[R] A) (g : M →ₗ[R] A) (x : M) : (QuadraticMap.linMulLin f g) x = f x * g x

@[simp]

theorem QuadraticMap.add_linMulLin {R : Type u_3} {M : Type u_4} {A : Type u_7} [CommSemiring R] [NonUnitalNonAssocSemiring A] [AddCommMonoid M] [Module R M] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (f : M →ₗ[R] A) (g : M →ₗ[R] A) (h : M →ₗ[R] A) : QuadraticMap.linMulLin (f + g) h = QuadraticMap.linMulLin f h + QuadraticMap.linMulLin g h

@[simp]

theorem QuadraticMap.linMulLin_add {R : Type u_3} {M : Type u_4} {A : Type u_7} [CommSemiring R] [NonUnitalNonAssocSemiring A] [AddCommMonoid M] [Module R M] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (f : M →ₗ[R] A) (g : M →ₗ[R] A) (h : M →ₗ[R] A) : QuadraticMap.linMulLin f (g + h) = QuadraticMap.linMulLin f g + QuadraticMap.linMulLin f h

@[simp]

theorem QuadraticMap.linMulLin_comp {R : Type u_3} {M : Type u_4} {A : Type u_7} [CommSemiring R] [NonUnitalNonAssocSemiring A] [AddCommMonoid M] [Module R M] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {N' : Type u_8} [AddCommMonoid N'] [Module R N'] (f : M →ₗ[R] A) (g : M →ₗ[R] A) (h : N' →ₗ[R] M) : (QuadraticMap.linMulLin f g).comp h = QuadraticMap.linMulLin (f ∘ₗ h) (g ∘ₗ h)

@[simp]

theorem QuadraticMap.sq_apply {R : Type u_3} {A : Type u_7} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) : QuadraticMap.sq a = a * a

def QuadraticMap.sq {R : Type u_3} {A : Type u_7} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : QuadraticMap R A A

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

Equations

• QuadraticMap.sq = QuadraticMap.linMulLin LinearMap.id LinearMap.id

def QuadraticMap.proj {R : Type u_3} {A : Type u_7} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {n : Type u_9} (i : n) (j : n) : QuadraticMap R (n → A) A

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

Equations

• QuadraticMap.proj i j = QuadraticMap.linMulLin (LinearMap.proj i) (LinearMap.proj j)

@[simp]

theorem QuadraticMap.proj_apply {R : Type u_3} {A : Type u_7} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {n : Type u_9} (i : n) (j : n) (x : n → A) : (QuadraticMap.proj i j) 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 associated quadratic map.

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

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' := ⋯ }

@[simp]

theorem LinearMap.BilinMap.toQuadraticMap_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : LinearMap.BilinMap R M N) (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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {N' : Type u_8} [AddCommMonoid N'] [Module R N'] (B : LinearMap.BilinMap R M N) (f : N' →ₗ[R] M) : LinearMap.BilinMap.toQuadraticMap (LinearMap.compl₁₂ B f f) = B.toQuadraticMap.comp f

@[simp]

theorem LinearMap.BilinMap.toQuadraticMap_zero (R : Type u_3) (M : Type u_4) {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : LinearMap.BilinMap.toQuadraticMap 0 = 0

@[simp]

theorem LinearMap.BilinMap.toQuadraticMap_add {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B₁ : LinearMap.BilinMap R M N) (B₂ : LinearMap.BilinMap R M N) : (B₁ + B₂).toQuadraticMap = B₁.toQuadraticMap + B₂.toQuadraticMap

@[simp]

theorem LinearMap.BilinMap.toQuadraticMap_smul {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Monoid S] [DistribMulAction S N] [SMulCommClass S R N] [SMulCommClass R S N] (a : S) (B : LinearMap.BilinMap R M N) : (a • B).toQuadraticMap = a • B.toQuadraticMap

@[simp]

theorem LinearMap.BilinMap.toQuadraticMapAddMonoidHom_apply (R : Type u_3) (M : Type u_4) {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : LinearMap.BilinMap R M N) : (LinearMap.BilinMap.toQuadraticMapAddMonoidHom R M) B = B.toQuadraticMap

def LinearMap.BilinMap.toQuadraticMapAddMonoidHom (R : Type u_3) (M : Type u_4) {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : LinearMap.BilinMap R M N →+ QuadraticMap R M N

LinearMap.BilinForm.toQuadraticMap as an additive homomorphism

Equations

• LinearMap.BilinMap.toQuadraticMapAddMonoidHom R M = { toFun := LinearMap.BilinMap.toQuadraticMap, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LinearMap.BilinMap.toQuadraticMapLinearMap_apply_apply (S : Type u_1) (R : Type u_3) (M : Type u_4) {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass S R N] [SMulCommClass R S N] (B : LinearMap.BilinMap R M N) (x : M) : ((LinearMap.BilinMap.toQuadraticMapLinearMap S R 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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass S R N] [SMulCommClass R S N] : LinearMap.BilinMap R M N →ₗ[S] QuadraticMap R M N

LinearMap.BilinForm.toQuadraticMap as a linear map

Equations

• LinearMap.BilinMap.toQuadraticMapLinearMap S R M = { toFun := LinearMap.BilinMap.toQuadraticMap, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.BilinMap.toQuadraticMap_list_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : List (LinearMap.BilinMap R M N)) : B.sum.toQuadraticMap = (List.map LinearMap.BilinMap.toQuadraticMap B).sum

@[simp]

theorem LinearMap.BilinMap.toQuadraticMap_multiset_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : Multiset (LinearMap.BilinMap R M N)) : B.sum.toQuadraticMap = (Multiset.map LinearMap.BilinMap.toQuadraticMap B).sum

@[simp]

theorem LinearMap.BilinMap.toQuadraticMap_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_9} (s : Finset ι) (B : ι → LinearMap.BilinMap R M N) : (∑ i ∈ s, B i).toQuadraticMap = ∑ i ∈ s, (B i).toQuadraticMap

@[simp]

theorem LinearMap.BilinMap.toQuadraticMap_eq_zero {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {B : LinearMap.BilinMap R M N} : B.toQuadraticMap = 0 ↔ LinearMap.IsAlt B

@[simp]

theorem LinearMap.BilinMap.toQuadraticMap_neg {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (B : LinearMap.BilinMap R M N) : (-B).toQuadraticMap = -B.toQuadraticMap

@[simp]

theorem LinearMap.BilinMap.toQuadraticMap_sub {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (B₁ : LinearMap.BilinMap R M N) (B₂ : LinearMap.BilinMap R M N) : (B₁ - B₂).toQuadraticMap = B₁.toQuadraticMap - B₂.toQuadraticMap

theorem LinearMap.BilinMap.polar_toQuadraticMap {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {B : LinearMap.BilinMap R M N} (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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {B : LinearMap.BilinMap R M N} : B.toQuadraticMap.polarBilin = B + LinearMap.flip B

@[simp]

theorem QuadraticMap.toQuadraticMap_polarBilin {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) : Q.polarBilin.toQuadraticMap = 2 • Q

theorem QuadraticMap.polarBilin_injective {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (h : IsUnit 2) : Function.Injective QuadraticMap.polarBilin

theorem QuadraticMap.polarBilin_comp {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {N' : Type u_8} [AddCommGroup N'] [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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {N' : Type u_8} [AddCommGroup N'] [CommSemiring S] [Algebra S R] [Module S N] [Module S N'] [IsScalarTower S R N] [Module S M] [IsScalarTower S R M] (f : N →ₗ[S] N') (Q : QuadraticMap R M N) (x : M) (y : M) : QuadraticMap.polar (⇑(f.compQuadraticMap' Q)) x y = f (QuadraticMap.polar (⇑Q) x y)

theorem LinearMap.compQuadraticMap_polarBilin {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {N' : Type u_8} [AddCommGroup N'] [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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] : QuadraticMap R M N →ₗ[S] LinearMap.BilinMap R M 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

• QuadraticMap.associatedHom S = ⟨⅟2, ⋯⟩ • { toFun := QuadraticMap.polarBilin, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem QuadraticMap.associated_apply (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] (Q : QuadraticMap R M N) (x : M) (y : M) : (((QuadraticMap.associatedHom S) 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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] (Q : QuadraticMap R M N) : 2 • (QuadraticMap.associatedHom S) Q = Q.polarBilin

theorem QuadraticMap.associated_isSymm (S : Type u_1) {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] (Q : QuadraticMap R M R) : LinearMap.IsSymm ((QuadraticMap.associatedHom S) Q)

@[simp]

theorem QuadraticMap.associated_comp (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] (Q : QuadraticMap R M N) {N' : Type u_8} [AddCommGroup N'] [Module R N'] (f : N' →ₗ[R] M) : (QuadraticMap.associatedHom S) (Q.comp f) = LinearMap.compl₁₂ ((QuadraticMap.associatedHom S) Q) f f

theorem QuadraticMap.associated_toQuadraticMap (S : Type u_1) {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] (B : LinearMap.BilinMap R M R) (x : M) (y : M) : (((QuadraticMap.associatedHom S) 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} [CommRing R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] {B₁ : LinearMap.BilinMap R M R} (h : LinearMap.IsSymm B₁) : (QuadraticMap.associatedHom S) B₁.toQuadraticMap = B₁

theorem QuadraticMap.associated_eq_self_apply (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] (Q : QuadraticMap R M N) (x : M) : (((QuadraticMap.associatedHom S) 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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] (Q : QuadraticMap R M N) : ((QuadraticMap.associatedHom S) Q).toQuadraticMap = Q

theorem QuadraticMap.associated_rightInverse (S : Type u_1) {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] : Function.RightInverse (⇑(QuadraticMap.associatedHom S)) LinearMap.BilinMap.toQuadraticMap

@[reducible, inline]

abbrev QuadraticMap.associated' {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] : QuadraticMap R M R →ₗ[ℤ] LinearMap.BilinMap R M R

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

Equations

• QuadraticMap.associated' = QuadraticMap.associatedHom ℤ

instance QuadraticMap.canLift {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] : CanLift (LinearMap.BilinMap R M R) (QuadraticForm R M) (⇑(QuadraticMap.associatedHom ℕ)) 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} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Invertible 2] : QuadraticMap R M N →ₗ[R] LinearMap.BilinMap R M N

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

Equations

• QuadraticMap.associated = QuadraticMap.associatedHom R

theorem QuadraticMap.coe_associatedHom (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring S] [CommRing R] [AddCommGroup M] [Algebra S R] [Module R M] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower S R N] [Invertible 2] : ⇑(QuadraticMap.associatedHom S) = ⇑QuadraticMap.associated

@[simp]

theorem QuadraticMap.associated_linMulLin {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (f : M →ₗ[R] R) (g : M →ₗ[R] R) : QuadraticMap.associated (QuadraticMap.linMulLin f g) = ⅟2 • ((LinearMap.mul R R).compl₁₂ f g + (LinearMap.mul R R).compl₁₂ g f)

@[simp]

theorem QuadraticMap.associated_sq {R : Type u_3} [CommRing R] [Invertible 2] : QuadraticMap.associated QuadraticMap.sq = LinearMap.mul R R

Orthogonality

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

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

Equations

• Q.IsOrtho x y = (Q (x + y) = Q x + Q y)

theorem QuadraticMap.isOrtho_def {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (x : M) (y : M) : QuadraticMap.IsOrtho 0 x y

theorem QuadraticMap.IsOrtho.zero_left {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {x : M} {y : M} : Q.IsOrtho x y → Q.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} [CommSemiring R] [AddCommMonoid M] [Module R M] [IsCancelAdd R] [NoZeroDivisors R] [CharZero R] {B : LinearMap.BilinMap R M R} {x : M} {y : M} (h : LinearMap.IsSymm B) : B.toQuadraticMap.IsOrtho x y ↔ LinearMap.IsOrtho B x y

@[simp]

theorem QuadraticMap.isOrtho_polarBilin {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {Q : QuadraticMap R M N} [Invertible 2] {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} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) : Prop

An anisotropic quadratic map is zero only on zero vectors.

Equations

• Q.Anisotropic = ∀ (x : M), Q x = 0 → x = 0

theorem QuadraticMap.not_anisotropic_iff_exists {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [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} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [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} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticMap R M R) (hB : Q.Anisotropic) : LinearMap.SeparatingLeft (QuadraticMap.associated' Q)

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} [CommSemiring R₂] [AddCommMonoid M] [Module R₂ M] [PartialOrder N] [AddCommMonoid N] [Module R₂ N] (Q₂ : QuadraticMap R₂ M N) : Prop

A positive definite quadratic form is positive on nonzero vectors.

Equations

• Q₂.PosDef = ∀ (x : M), x ≠ 0 → 0 < Q₂ x

theorem QuadraticMap.PosDef.smul {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [PartialOrder N] [AddCommMonoid N] {R : Type u_8} [LinearOrderedCommRing R] [Module R M] [Module R N] [PosSMulStrictMono 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} [CommSemiring R₂] [AddCommMonoid M] [Module R₂ M] [PartialOrder N] [AddCommMonoid N] [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} [CommSemiring R₂] [AddCommMonoid M] [Module R₂ M] [PartialOrder N] [AddCommMonoid N] [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} [CommSemiring R₂] [AddCommMonoid M] [Module R₂ M] [PartialOrder N] [AddCommMonoid N] [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} [CommSemiring R₂] [AddCommMonoid M] [Module R₂ M] [PartialOrder N] [AddCommMonoid N] [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} [CommSemiring R₂] [AddCommMonoid M] [Module R₂ M] [PartialOrder N] [AddCommMonoid N] [Module R₂ N] [CovariantClass N N (fun (x x_1 : N) => x + x_1) fun (x x_1 : N) => x < x_1] (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} [AddCommMonoid M] {R : Type u_9} [LinearOrderedCommRing R] [Module R M] [LinearOrderedSemiring A] [ExistsAddOfLE A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (f : M →ₗ[R] A) (hf : LinearMap.ker f = ⊥) : (QuadraticMap.linMulLin f f).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} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : QuadraticMap R (n → R) R

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

Equations

• M.toQuadraticMap' = LinearMap.BilinMap.toQuadraticMap ((Matrix.toLinearMap₂' R) M)

def QuadraticMap.toMatrix' {R : Type u_3} {n : Type w} [Fintype n] [DecidableEq n] [CommRing R] [Invertible 2] (Q : QuadraticMap R (n → R) R) : Matrix n n R

A matrix representation of the quadratic form.

Equations

• Q.toMatrix' = (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q)

theorem QuadraticMap.toMatrix'_smul {R : Type u_3} {n : Type w} [Fintype n] [DecidableEq n] [CommRing R] [Invertible 2] (a : R) (Q : QuadraticMap R (n → R) R) : (a • Q).toMatrix' = a • Q.toMatrix'

theorem QuadraticMap.isSymm_toMatrix' {R : Type u_3} {n : Type w} [Fintype n] [DecidableEq n] [CommRing R] [Invertible 2] (Q : QuadraticMap R (n → R) R) : Q.toMatrix'.IsSymm

@[simp]

theorem QuadraticMap.toMatrix'_comp {R : Type u_3} {n : Type w} [Fintype n] [CommRing R] [DecidableEq n] [Invertible 2] {m : Type w} [DecidableEq m] [Fintype m] (Q : QuadraticMap R (m → R) R) (f : (n → R) →ₗ[R] m → R) : (Q.comp f).toMatrix' = (LinearMap.toMatrix' f).transpose * Q.toMatrix' * LinearMap.toMatrix' f

def QuadraticMap.discr {R : Type u_3} {n : Type w} [Fintype n] [CommRing R] [DecidableEq n] [Invertible 2] (Q : QuadraticMap R (n → R) R) : R

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

Equations

• Q.discr = Q.toMatrix'.det

theorem QuadraticMap.discr_smul {R : Type u_3} {n : Type w} [Fintype n] [CommRing R] [DecidableEq n] [Invertible 2] {Q : QuadraticMap R (n → R) R} (a : R) : (a • Q).discr = a ^ Fintype.card n * Q.discr

theorem QuadraticMap.discr_comp {R : Type u_3} {n : Type w} [Fintype n] [CommRing R] [DecidableEq n] [Invertible 2] {Q : QuadraticMap R (n → R) R} (f : (n → R) →ₗ[R] n → R) : (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} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (hB : (LinearMap.BilinMap.toQuadraticMap B).Anisotropic) : LinearMap.SeparatingLeft B

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} [CommRing R] [AddCommGroup M] [Module R M] [htwo : Invertible 2] {B : LinearMap.BilinForm R M} (hB₁ : B ≠ 0) (hB₂ : LinearMap.IsSymm B) : ∃ (x : M), ¬LinearMap.IsOrtho B x x

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} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [hK : Invertible 2] {B : LinearMap.BilinForm K V} (hB₂ : LinearMap.IsSymm B) : ∃ (v : Basis (Fin (FiniteDimensional.finrank K V)) K V), LinearMap.IsOrthoᵢ B ⇑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} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_8} [Finite ι] (Q : QuadraticMap R M N) (v : Basis ι R M) : QuadraticMap R (ι → R) N

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

Equations

• Q.basisRepr v = Q.comp ↑v.equivFun.symm

@[simp]

theorem QuadraticMap.basisRepr_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_8} [Fintype ι] {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) [CommSemiring R] {ι : Type u_8} [Fintype ι] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) : QuadraticMap R (ι → R) R

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

• QuadraticMap.weightedSumSquares R w = ∑ i : ι, w i • QuadraticMap.proj i i

@[simp]

theorem QuadraticMap.weightedSumSquares_apply {S : Type u_1} {R : Type u_3} [CommSemiring R] {ι : Type u_8} [Fintype ι] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) (v : ι → R) : (QuadraticMap.weightedSumSquares R w) v = ∑ i : ι, w i • (v i * v i)

theorem QuadraticMap.basisRepr_eq_of_iIsOrtho {ι : Type u_8} [Fintype ι] {R : Type u_9} {M : Type u_10} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (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.